:: Birkhoff Theorem for Many Sorted Algebras :: by Artur Korni{\l}owicz :: :: Received June 19, 1997 :: Copyright (c) 1997-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, STRUCT_0, MSUALG_1, RELAT_1, PBOOLE, MSAFREE, MSUALG_3, REALSET1, MEMBER_1, FUNCT_6, TARSKI, FUNCT_1, WELLORD1, MSUALG_2, PRALG_2, CARD_3, SUBSET_1, MSUALG_5, MSUALG_4, FUNCOP_1, RLVECT_2, PRALG_1, EQREL_1, CLOSURE2, SETFAM_1, FUNCT_4, ZFMISC_1, GROUP_6, NUMBERS, EQUATION, ZF_MODEL, ZF_LANG, MCART_1, PZFMISC1, MSAFREE2, FINSET_1, BIRKHOFF, NAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, SETFAM_1, RELAT_1, XTUPLE_0, MCART_1, STRUCT_0, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, CARD_3, FUNCT_6, NAT_1, FUNCOP_1, MSUALG_1, MSUALG_2, PRALG_3, MSUALG_3, MSAFREE, MSAFREE2, PRALG_2, MSUALG_4, PZFMISC1, MSSUBFAM, CLOSURE2, MSUALG_5, EQUATION; constructors BINOP_1, PZFMISC1, MSSUBFAM, MSUALG_3, MSAFREE2, MSUALG_5, CLOSURE2, PRALG_3, EQUATION, RELSET_1, XTUPLE_0; registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_2, MSUALG_4, MSAFREE1, MSAFREE2, EXTENS_1, MSUALG_5, CLOSURE2, PRALG_3, MSUALG_9, EQUATION, MSSUBFAM, AUTALG_1, XTUPLE_0; requirements SUBSET, BOOLE; begin :: Birkhoff Variety Theorem ::------------------------------------------------------------------- :: Acknowledgements: :: ================= :: :: I would like to thank Professor Andrzej Trybulec :: for his help in the preparation of the article. ::------------------------------------------------------------------- definition let S be non empty non void ManySortedSign, X be non-empty ManySortedSet of the carrier of S, A be non-empty MSAlgebra over S, F be ManySortedFunction of X , the Sorts of A; func F-hash -> ManySortedFunction of FreeMSA X, A means :: BIRKHOFF:def 1 it is_homomorphism FreeMSA X, A & it || FreeGen X = F ** Reverse X; end; theorem :: BIRKHOFF:1 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for X being non-empty ManySortedSet of the carrier of S for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs ( F-hash); :: Let P[] be a non empty abstract class of algebras. If P[] is closed under :: subalgebras and products, the free algebras exist in P[]. scheme :: BIRKHOFF:sch 1 ExFreeAlg1 { S() -> non empty non void ManySortedSign, X() -> non-empty MSAlgebra over S(), P[set] } : ex A being strict non-empty MSAlgebra over S(), F being ManySortedFunction of X(), A st P[A] & F is_epimorphism X(), A & for B being non-empty MSAlgebra over S() for G being ManySortedFunction of X(), B st G is_homomorphism X(), B & P[B] ex H being ManySortedFunction of A, B st H is_homomorphism A, B & H ** F = G & for K being ManySortedFunction of A, B st K ** F = G holds H = K provided for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A] holds P[B] and for A being non-empty MSAlgebra over S() for B being strict non-empty MSSubAlgebra of A st P[A] holds P[B] and for I being set, F being MSAlgebra-Family of I, S() st (for i being set st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product F]; scheme :: BIRKHOFF:sch 2 ExFreeAlg2 { S() -> non empty non void ManySortedSign, X() -> non-empty ManySortedSet of the carrier of S(), P[set] } : ex A being strict non-empty MSAlgebra over S(), F being ManySortedFunction of X(), the Sorts of A st P[A] & for B being non-empty MSAlgebra over S() for G being ManySortedFunction of X(), the Sorts of B st P[B] ex H being ManySortedFunction of A, B st H is_homomorphism A, B & H ** F = G & for K being ManySortedFunction of A, B st K is_homomorphism A, B & K ** F = G holds H = K provided for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A] holds P[B] and for A being non-empty MSAlgebra over S() for B being strict non-empty MSSubAlgebra of A st P[A] holds P[B] and for I being set, F being MSAlgebra-Family of I, S() st (for i being set st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product F]; scheme :: BIRKHOFF:sch 3 Exhash { S() -> non empty non void ManySortedSign, F, A() -> non-empty MSAlgebra over S(), fi() -> ManySortedFunction of (the carrier of S()) --> NAT, the Sorts of F(), a() -> ManySortedFunction of (the carrier of S()) --> NAT, the Sorts of A(), P[set] } : ex H being ManySortedFunction of F(), A() st H is_homomorphism F(), A() & a()-hash = H ** (fi()-hash) provided P[A()] and for C being non-empty MSAlgebra over S() :: F() is free in P[] for G being ManySortedFunction of (the carrier of S()) --> NAT, the Sorts of C st P[C] ex h being ManySortedFunction of F(), C st h is_homomorphism F(), C & G = h ** fi(); :: Let P[] be a class of algebras. If a free algebra F() in P[] :: relative to fi() exists, then :: P[] |= [t1(),t2()] iff (F(),fi()) |= [t1(),t2()]. scheme :: BIRKHOFF:sch 4 EqTerms { S() -> non empty non void ManySortedSign, F() -> non-empty MSAlgebra over S(), fi() -> ManySortedFunction of (the carrier of S()) --> NAT, the Sorts of F(), s() -> SortSymbol of S(), t1, t2() -> Element of (the Sorts of TermAlg S()).s(), P[set] } : for B being non-empty MSAlgebra over S() st P[B ] holds B |= t1() '=' t2() provided fi()-hash.s().t1() = fi()-hash.s().t2() and for C being non-empty MSAlgebra over S() for G being ManySortedFunction of (the carrier of S()) --> NAT, the Sorts of C st P[C] ex h being ManySortedFunction of F(), C st h is_homomorphism F(), C & G = h ** fi(); :: Let P[] be an abstract class of algebras such that P[] is closed under :: subalgebras. The free algebra in P[] over X(), if it exists, :: is generated by X(). scheme :: BIRKHOFF:sch 5 FreeIsGen { S() -> non empty non void ManySortedSign, X() -> non-empty ManySortedSet of the carrier of S(), A() -> strict non-empty MSAlgebra over S() , f() -> ManySortedFunction of X(), the Sorts of A(), P[set] } : f().:.:X() is non-empty GeneratorSet of A() provided for C being non-empty MSAlgebra over S() :: A() is free in P[] for G being ManySortedFunction of X(), the Sorts of C st P[C] ex H being ManySortedFunction of A(), C st H is_homomorphism A(), C & H ** f() = G & for K being ManySortedFunction of A(), C st K is_homomorphism A(), C & K ** f() = G holds H = K and P[A()] and for A being non-empty MSAlgebra over S() for B being strict non-empty MSSubAlgebra of A st P[A] holds P[B]; scheme :: BIRKHOFF:sch 6 Hashisonto { S() -> non empty non void ManySortedSign, A() -> strict non-empty MSAlgebra over S(), F() -> ManySortedFunction of (the carrier of S()) --> NAT, the Sorts of A(), P[set] } : F()-hash is_epimorphism FreeMSA ((the carrier of S()) --> NAT), A() provided for C being non-empty MSAlgebra over S() for G being ManySortedFunction of (the carrier of S()) --> NAT, the Sorts of C st P[C] ex H being ManySortedFunction of A(), C st H is_homomorphism A(), C & H ** F() = G & for K being ManySortedFunction of A(), C st K is_homomorphism A(), C & K ** F() = G holds H = K and P[A()] and for A being non-empty MSAlgebra over S() for B being strict non-empty MSSubAlgebra of A st P[A] holds P[B]; scheme :: BIRKHOFF:sch 7 FinGenAlgInVar { S() -> non empty non void ManySortedSign, A() -> strict finitely-generated non-empty MSAlgebra over S(), F() -> non-empty MSAlgebra over S(), fi() -> ManySortedFunction of (the carrier of S()) --> NAT, the Sorts of F(), P, Q[set] } : P[A()] provided Q[A()] and P[F()] and for C being non-empty MSAlgebra over S() :: F() is free in Q[] for G being ManySortedFunction of (the carrier of S()) --> NAT, the Sorts of C st Q[C] ex h being ManySortedFunction of F(), C st h is_homomorphism F(), C & G = h ** fi() and for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A] holds P[B] and for A being non-empty MSAlgebra over S(), R being MSCongruence of A st P[A] holds P[QuotMSAlg (A,R)]; scheme :: BIRKHOFF:sch 8 QuotEpi { S() -> non empty non void ManySortedSign, X, Y() -> non-empty MSAlgebra over S(), P[set] } : P[Y()] provided ex H being ManySortedFunction of X(), Y() st H is_epimorphism X(), Y () and P[X()] and for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A] holds P[B] and for A being non-empty MSAlgebra over S(), R being MSCongruence of A st P[A] holds P[QuotMSAlg (A,R)]; :: An algebra X() belongs to a variety P[] whenever all its finitely :: generated subalgebras are in P[]. scheme :: BIRKHOFF:sch 9 AllFinGen { S() -> non empty non void ManySortedSign, X() -> non-empty MSAlgebra over S(), P[set] } : P[X()] provided for B being strict non-empty finitely-generated MSSubAlgebra of X() holds P[B] and for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A] holds P[B] and for A being non-empty MSAlgebra over S() for B being strict non-empty MSSubAlgebra of A st P[A] holds P[B] and for A being non-empty MSAlgebra over S(), R being MSCongruence of A st P[A] holds P[QuotMSAlg (A,R)] and for I being set, F being MSAlgebra-Family of I, S() st (for i being set st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product F]; scheme :: BIRKHOFF:sch 10 FreeInModIsInVar1 { S() -> non empty non void ManySortedSign, X() -> non-empty MSAlgebra over S(), P, Q[set] } : Q[X()] provided for A being non-empty MSAlgebra over S() holds Q[A] iff for s being SortSymbol of S(), e being Element of (Equations S()).s st (for B being non-empty MSAlgebra over S() st P[B] holds B |= e) holds A |= e and P[X()]; :: If P[] is a non empty variety, then the free algebras in Mod Eq P[] :: belong to P[]. (Q[] = Mod Eq P[]) scheme :: BIRKHOFF:sch 11 FreeInModIsInVar { S() -> non empty non void ManySortedSign, X() -> strict non-empty MSAlgebra over S(), psi() -> ManySortedFunction of (the carrier of S( )) --> NAT, the Sorts of X(), P, Q[set] } : P[X()] provided for A being non-empty MSAlgebra over S() holds Q[A] iff for s being SortSymbol of S(), e being Element of (Equations S()).s st (for B being non-empty MSAlgebra over S() st P[B] holds B |= e) holds A |= e and for C being non-empty MSAlgebra over S() :: X() is free in Q[] for G being ManySortedFunction of (the carrier of S()) --> NAT, the Sorts of C st Q[C] ex H being ManySortedFunction of X(), C st H is_homomorphism X(), C & H ** psi() = G & for K being ManySortedFunction of X(), C st K is_homomorphism X(), C & K ** psi() = G holds H = K and Q[X()] and for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A] holds P[B] and for A being non-empty MSAlgebra over S() for B being strict non-empty MSSubAlgebra of A st P[A] holds P[B] and for I being set, F being MSAlgebra-Family of I, S() st (for i being set st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product F]; :: Let P[] be an abstract class of algebras. Then P[] is an equational class :: if and only if P[] is variety. ::$N Birkhoff Variety Theorem scheme :: BIRKHOFF:sch 12 Birkhoff { S() -> non empty non void ManySortedSign, P[set] } : ex E being EqualSet of S() st for A being non-empty MSAlgebra over S() holds P[A] iff A |= E provided for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A] holds P[B] and for A being non-empty MSAlgebra over S() for B being strict non-empty MSSubAlgebra of A st P[A] holds P[B] and for A being non-empty MSAlgebra over S(), R being MSCongruence of A st P[A] holds P[QuotMSAlg (A,R)] and for I being set, F being MSAlgebra-Family of I, S() st (for i being set st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product F];