Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Birkhoff Theorem for Many Sorted Algebras

**by****Artur Kornilowicz**- Received June 19, 1997
- MML identifier: BIRKHOFF

- [ Mizar article, MML identifier index ]

environ vocabulary AMI_1, MSUALG_1, ZF_REFLE, PBOOLE, PRALG_1, MSAFREE, ALG_1, REALSET1, MSUALG_3, FUNCT_6, FUNCT_1, RELAT_1, GROUP_6, WELLORD1, MSUALG_2, PRALG_2, CARD_3, MSUALG_5, MSUALG_4, FUNCOP_1, BOOLE, RLVECT_2, EQREL_1, CLOSURE2, SETFAM_1, FUNCT_4, BORSUK_1, CANTOR_1, EQUATION, ZF_MODEL, MCART_1, FREEALG, NATTRA_1, MSAFREE2, PRE_CIRC, BIRKHOFF; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, SETFAM_1, RELAT_1, MCART_1, STRUCT_0, FUNCT_1, RELSET_1, FUNCT_2, EQREL_1, CARD_3, CANTOR_1, PBOOLE, PRALG_1, MSUALG_1, MSUALG_2, PRALG_3, MSUALG_3, AUTALG_1, MSAFREE, MSAFREE2, PRALG_2, PRE_CIRC, MSUALG_4, PZFMISC1, EXTENS_1, MSSUBFAM, CLOSURE2, MSUALG_5, EQUATION; constructors CANTOR_1, PRALG_3, PRE_CIRC, MSAFREE2, AUTALG_1, EXTENS_1, PZFMISC1, CLOSURE2, MSUALG_5, BINOP_1, EQUATION, MSUALG_6, MSSUBFAM; clusters CANTOR_1, CLOSURE2, FUNCT_1, MSAFREE2, MSUALG_1, MSUALG_2, MSUALG_4, MSUALG_5, MSUALG_9, PBOOLE, PRALG_1, PRALG_3, RELSET_1, STRUCT_0, EQUATION, EXTENS_1, MEMBERED, ORDINAL2; 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 ExFreeAlg_1 { 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 ExFreeAlg_2 { 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 Ex_hash { 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 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() :: 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 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 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 Hash_is_onto { 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() :: A() 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 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 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 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 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 FreeInModIsInVar_1 { 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 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. scheme 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];

Back to top