:: Birkhoff Theorem for Many Sorted Algebras
:: by Artur Korni{\l}owicz
::
:: Received June 19, 1997
:: Copyright (c) 1997-2026 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;
definitions FUNCT_1, RELAT_1, TARSKI, PBOOLE, PRALG_2, EQUATION, FUNCOP_1;
equalities PRALG_2, EQUATION;
expansions PBOOLE, MSUALG_4, EQUATION, PZFMISC1;
theorems CARD_3, CLOSURE2, EXTENS_1, FUNCOP_1, FUNCT_1, FUNCT_2, MSAFREE,
MSAFREE2, MSSCYC_1, MSSUBFAM, MSUALG_2, MSUALG_3, MSUALG_4, MSUALG_5,
MSUALG_7, MSUALG_9, PBOOLE, PRALG_2, PRALG_3, EQUATION, RELAT_1,
ZFMISC_1, SETFAM_1;
schemes DOMAIN_1, PBOOLE;
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
: Def1:
it is_homomorphism FreeMSA X, A & it || FreeGen X = F ** Reverse X;
existence by MSAFREE:def 5;
uniqueness by EXTENS_1:14;
end;
theorem Th1:
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)
proof
let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S,
X be non-empty ManySortedSet of the carrier of S, F be ManySortedFunction of X,
the Sorts of A;
set R = Reverse X;
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
let y be object;
A1: dom (R.s) = (FreeGen X).s by FUNCT_2:def 1;
FreeGen X c= the Sorts of FreeMSA X by PBOOLE:def 18;
then
A2: (FreeGen X).s c= (the Sorts of FreeMSA X).s;
assume y in (rngs F).i;
then y in rng (F.s) by MSSUBFAM:13;
then consider x being object such that
A3: x in dom (F.s) and
A4: y = F.s.x by FUNCT_1:def 3;
rngs R = X by EXTENS_1:10;
then R is "onto" by EXTENS_1:9;
then rng (R.s) = X.s by MSUALG_3:def 3;
then consider a being object such that
A5: a in dom (R.s) and
A6: x = R.s.a by A3,FUNCT_1:def 3;
A7: dom ((F-hash).s) = (the Sorts of FreeMSA X).s by FUNCT_2:def 1;
y = (F.s*R.s).a by A4,A5,A6,FUNCT_1:13
.= (F**R).s.a by MSUALG_3:2
.= (F-hash || FreeGen X).s.a by Def1
.= (((F-hash).s) | ((FreeGen X).s)).a by MSAFREE:def 1
.= (F-hash).s.a by A5,FUNCT_1:49;
then y in rng ((F-hash).s) by A5,A1,A7,A2,FUNCT_1:def 3;
hence thesis by MSSUBFAM:13;
end;
:: 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
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
A1: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A2: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B] and
A3: 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]
proof
set EMF = the MSAlgebra-Family of {}, S();
set CC = { C where C is Element of CongrLatt X() : ex R being MSCongruence
of X() st R = C & P[QuotMSAlg (X(),R)] };
set SF = the Sorts of X(), I = the carrier of S();
consider Xi being ManySortedSet of I such that
A4: {Xi} = I --> {{}} by MSUALG_9:5;
now
let i be object;
assume i in I;
then reconsider s = i as SortSymbol of S();
thus (the Sorts of product EMF).i = product Carrier(EMF,s) by
PRALG_2:def 10
.= {{}} by CARD_3:10,PRALG_2:def 9
.= (I --> {{}}).s
.= {Xi}.i by A4;
end;
then
A5: the Sorts of product EMF = {Xi};
reconsider R = [|SF,SF|] as MSCongruence of X() by MSUALG_5:18;
[|SF,SF|] is MSCongruence of X() by MSUALG_5:18;
then
A6: [|SF,SF|] is Element of CongrLatt X() by MSUALG_5:def 6;
the Sorts of QuotMSAlg (X(),R) = {SF} by MSUALG_9:29;
then
A7: QuotMSAlg (X(),R), Trivial_Algebra S() are_isomorphic by MSUALG_9:26;
for i being set st i in {} ex A being MSAlgebra over S() st A = EMF.i & P[A];
then P[product EMF] by A3;
then P[Trivial_Algebra S()] by A1,A5,MSUALG_9:26;
then P[QuotMSAlg (X(),R)] by A1,A7,MSUALG_3:17;
then
A8: [|SF,SF|] in CC by A6;
defpred P[object,object] means
ex R being MSCongruence of X() st R = $1 & $2 = QuotMSAlg (X(),R);
defpred P1[set] means ex R being MSCongruence of X() st R = $1 & P[QuotMSAlg
(X(),R)];
A9: now
let q be object;
assume q in CC;
then
ex C be Element of CongrLatt X() st q = C & ex R being MSCongruence
of X() st R = C & P[QuotMSAlg (X(),R)];
hence q is MSCongruence of X();
end;
A10: CC c= the carrier of EqRelLatt SF
proof
let q be object;
assume q in CC;
then q is Equivalence_Relation of SF by A9;
hence thesis by MSUALG_5:def 5;
end;
then reconsider CC as non empty SubsetFamily of [|SF,SF|] by A8,MSUALG_7:5;
set R0 = meet |:CC:|;
A11: R0 is MSEquivalence_Relation-like ManySortedRelation of SF by A10,
MSUALG_7:8;
reconsider R0 as ManySortedRelation of X() by A10,MSUALG_7:8;
R0 is MSEquivalence-like
by A11;
then reconsider R0 as MSEquivalence-like ManySortedRelation of X();
{ C where C is Element of CongrLatt X() : P1[C] } is Subset of CongrLatt
X() from DOMAIN_1:sch 7;
then reconsider R0 as MSCongruence of X() by MSUALG_9:28;
take A = QuotMSAlg (X(),R0);
reconsider F = MSNat_Hom(X(),R0) as ManySortedFunction of X(), A;
take F;
A12: now
let c be object;
assume c in CC;
then reconsider cc = c as MSCongruence of X() by A9;
reconsider w = QuotMSAlg (X(),cc) as object;
take w;
thus P[c,w];
end;
consider FF being ManySortedSet of CC such that
A13: for c being object st c in CC holds P[c,FF.c] from PBOOLE:sch 3(A12);
FF is MSAlgebra-Family of CC, S()
proof
let c be object;
assume c in CC;
then ex R being MSCongruence of X() st R = c & FF.c = QuotMSAlg (X(),R)
by A13;
hence thesis;
end;
then reconsider FF as MSAlgebra-Family of CC, S();
defpred P[Element of CC,object] means
ex F1 being ManySortedFunction of X(),FF.
$1 st F1 = $2 & F1 is_homomorphism X(),FF.$1 & ex R being MSCongruence of X()
st $1 = R & F1 = MSNat_Hom(X(),R);
A14: for c being Element of CC ex j being object st P[c,j]
proof
let c be Element of CC;
consider R being MSCongruence of X() such that
A15: R = c and
A16: FF.c = QuotMSAlg (X(),R) by A13;
set j = MSNat_Hom(X(),R);
reconsider F1 = j as ManySortedFunction of X(),FF.c by A16;
take j;
take F1;
thus F1 = j;
MSNat_Hom(X(),R) is_epimorphism X(),QuotMSAlg (X(),R) by MSUALG_4:3;
hence F1 is_homomorphism X(),FF.c by A16,MSUALG_3:def 8;
take R;
thus thesis by A15;
end;
consider FofI1 being ManySortedSet of CC such that
A17: for c being Element of CC holds P[c,FofI1.c] from PBOOLE:sch 6(A14);
A18: for c being Element of CC ex F1 being ManySortedFunction of X(),FF.c st
F1 = FofI1.c & F1 is_homomorphism X(),FF.c
proof
let c be Element of CC;
consider F1 being ManySortedFunction of X(),FF.c such that
A19: F1 = FofI1.c and
A20: F1 is_homomorphism X(),FF.c and
ex R being MSCongruence of X() st c = R & F1 = MSNat_Hom(X(),R) by A17;
take F1;
thus thesis by A19,A20;
end;
FofI1 is Function-yielding
proof
let c be object;
assume c in dom FofI1;
then reconsider cc = c as Element of CC;
ex F1 being ManySortedFunction of X(),FF.cc st F1 = FofI1. cc & F1
is_homomorphism X(),FF.cc by A18;
hence thesis;
end;
then reconsider FofI1 as ManySortedFunction of CC;
consider H being ManySortedFunction of X(),product FF such that
A21: H is_homomorphism X(),product FF and
A22: for c being Element of CC holds proj(FF,c) ** H = FofI1.c by A18,
PRALG_3:29;
now
let i be object;
assume i in I;
then reconsider s = i as SortSymbol of S();
consider Q being Subset-Family of ([|SF,SF|].s) such that
A23: Q = |:CC:|.s and
A24: (meet |:CC:|).s = Intersect Q by MSSUBFAM:def 1;
A25: |:CC:|.s = { t.s where t is Element of Bool [|SF,SF|] : t in CC } by
CLOSURE2:14;
(MSCng H).s = R0.s
proof
let a, b be object;
hereby
assume
A26: [a,b] in (MSCng H).s;
then
A27: a in SF.s by ZFMISC_1:87;
A28: b in SF.s by A26,ZFMISC_1:87;
A29: [a,b] in MSCng (H,s) by A21,A26,MSUALG_4:def 18;
A30: for Y being set st Y in Q holds [a,b] in Y
proof
let Y be set;
assume Y in Q;
then consider t being Element of Bool [|SF,SF|] such that
A31: Y = t.s and
A32: t in CC by A23,A25;
reconsider t1 = t as Element of CC by A32;
consider F1 being ManySortedFunction of X(),FF.t1 such that
A33: F1 = FofI1.t1 and
F1 is_homomorphism X(),FF.t1 and
A34: ex R being MSCongruence of X() st t1 = R & F1 = MSNat_Hom(X
(),R) by A17;
F1.s.a = (proj(FF,t1) ** H).s.a by A22,A33
.= ((proj(FF,t1)).s * H.s).a by MSUALG_3:2
.= (proj(FF,t1).s).((H.s).a) by A27,FUNCT_2:15
.= (proj(FF,t1).s).((H.s).b) by A27,A28,A29,MSUALG_4:def 17
.= ((proj(FF,t1)).s * H.s).b by A28,FUNCT_2:15
.= (proj(FF,t1) ** H).s.b by MSUALG_3:2
.= F1.s.b by A22,A33;
hence thesis by A27,A28,A31,A34,MSUALG_9:33;
end;
[a,b] in [:SF.s,SF.s:] by A26;
then [a,b] in [|SF,SF|].s by PBOOLE:def 16;
hence [a,b] in R0.s by A24,A30,SETFAM_1:43;
end;
assume
A35: [a,b] in R0.s;
then
A36: a in SF.s by ZFMISC_1:87;
A37: b in SF.s by A35,ZFMISC_1:87;
A38: for c being Element of CC holds proj(Carrier(FF,s),c).(H.s.a) =
proj(Carrier(FF,s),c).(H.s.b)
proof
let c be Element of CC;
reconsider t1 = c as MSCongruence of X() by A9;
consider F1 being ManySortedFunction of X(),FF.c such that
A39: F1 = FofI1.c and
F1 is_homomorphism X(),FF.c and
A40: ex R being MSCongruence of X() st c = R & F1 = MSNat_Hom(X(),
R) by A17;
t1 is Element of Bool [|SF,SF|] by CLOSURE2:def 1;
then t1.s in |:CC:|.s by A25;
then
A41: [a,b] in t1.s by A23,A24,A35,SETFAM_1:43;
thus proj(Carrier(FF,s),c).(H.s.a) = (proj(FF,c).s).(H.s.a) by
PRALG_3:def 2
.= ((proj(FF,c)).s * H.s).a by A36,FUNCT_2:15
.= (proj(FF,c) ** H).s.a by MSUALG_3:2
.= F1.s.a by A22,A39
.= F1.s.b by A36,A37,A41,A40,MSUALG_9:33
.= (proj(FF,c) ** H).s.b by A22,A39
.= ((proj(FF,c)).s * H.s).b by MSUALG_3:2
.= (proj(FF,c).s).(H.s.b) by A37,FUNCT_2:15
.= proj(Carrier(FF,s),c).(H.s.b) by PRALG_3:def 2;
end;
H.s.b in (the Sorts of product FF).s by A37,FUNCT_2:5;
then
A42: H.s.b in product Carrier(FF,s) by PRALG_2:def 10;
H.s.a in (the Sorts of product FF).s by A36,FUNCT_2:5;
then H.s.a in product Carrier(FF,s) by PRALG_2:def 10;
then H.s.a = H.s.b by A42,A38,MSUALG_9:14;
then [a,b] in MSCng (H,s) by A36,A37,MSUALG_4:def 17;
hence thesis by A21,MSUALG_4:def 18;
end;
hence (MSCng H).i = R0.i;
end;
then
A43: MSCng H = R0;
QuotMSAlg (X(),MSCng H), Image MSHomQuot H are_isomorphic by A21,MSUALG_4:4
,MSUALG_9:16;
then consider XX being strict non-empty MSSubAlgebra of product FF such that
A44: A, XX are_isomorphic by A43;
for cc being set st cc in CC ex A being MSAlgebra over S() st A = FF.cc
& P[A]
proof
let cc be set;
assume
A45: cc in CC;
then reconsider c = cc as Element of CC;
take FF.c;
A46: ex C be Element of CongrLatt X() st cc = C & ex R being
MSCongruence of X() st R = C & P[QuotMSAlg (X(),R)] by A45;
ex R being MSCongruence of X() st R = cc & FF.cc = QuotMSAlg (X(),R
) by A13,A45;
hence thesis by A46;
end;
then P[XX] by A2,A3;
hence P[A] by A1,A44,MSUALG_3:17;
thus F is_epimorphism X(), A by MSUALG_4:3;
then
A47: F is "onto" by MSUALG_3:def 8;
let B be non-empty MSAlgebra over S(), G be ManySortedFunction of X(), B
such that
A48: G is_homomorphism X(), B and
A49: P[B];
reconsider C = Image MSHomQuot G as strict non-empty MSSubAlgebra of B;
A50: QuotMSAlg (X(),MSCng G), C are_isomorphic by A48,MSUALG_4:4,MSUALG_9:16;
A51: MSCng G is Element of CongrLatt X() by MSUALG_5:def 6;
P[C] by A2,A49;
then P[QuotMSAlg (X(),MSCng G)] by A1,A50,MSUALG_3:17;
then MSCng(G) in CC by A51;
then R0 c= MSCng(G) by CLOSURE2:21,MSSUBFAM:43;
then consider H being ManySortedFunction of A, B such that
A52: H is_homomorphism A, B and
A53: G = H ** F by A48,MSUALG_9:36;
take H;
thus H is_homomorphism A, B by A52;
thus G = H ** F by A53;
let K be ManySortedFunction of A, B;
assume K ** F = G;
hence thesis by A53,A47,EXTENS_1:12;
end;
scheme
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
A1: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A2: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B] and
A3: 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]
proof
A4: for A being non-empty MSAlgebra over S() for B being strict non-empty
MSSubAlgebra of A st P[A] holds P[B] by A2;
A5: 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]
by A3;
set FM = FreeMSA X();
A6: Reverse X() is "1-1" by MSUALG_9:11;
A7: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A
] holds P[B] by A1;
consider A being strict non-empty MSAlgebra over S(), F being
ManySortedFunction of FM, A such that
A8: P[A] and
A9: F is_epimorphism FM, A and
A10: for B being non-empty MSAlgebra over S() for G being
ManySortedFunction of FM, B st G is_homomorphism FM, 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 from ExFreeAlg1(A7,A4,A5);
reconsider R = (F || FreeGen X()) ** ((Reverse X())"") as ManySortedFunction
of X(), the Sorts of A;
take A;
take R;
thus P[A] by A8;
let B be non-empty MSAlgebra over S(), G be ManySortedFunction of X(), the
Sorts of B such that
A11: P[B];
consider GG being ManySortedFunction of FM, B such that
A12: GG is_homomorphism FM, B and
A13: GG || FreeGen X() = G ** Reverse X() by MSAFREE:def 5;
consider H being ManySortedFunction of A, B such that
A14: H is_homomorphism A, B and
A15: H ** F = GG and
for K being ManySortedFunction of A, B st K ** F = GG holds H = K by A10,A11
,A12;
take H;
thus H is_homomorphism A, B by A14;
A16: H ** (F || FreeGen X()) = GG || FreeGen X() by A15,EXTENS_1:4;
A17: F is "onto" by A9,MSUALG_3:def 8;
rngs Reverse X() = X() by EXTENS_1:10;
then
A18: Reverse X() is "onto" by EXTENS_1:9;
R ** Reverse X() = (F || FreeGen X()) ** (((Reverse X())"")**Reverse X(
)) by PBOOLE:140
.= (F || FreeGen X()) ** (id FreeGen X()) by A18,A6,MSUALG_3:5
.= F || FreeGen X() by MSUALG_3:3;
then
A19: H ** R ** Reverse X() = G ** Reverse X() by A13,A16,PBOOLE:140;
hence H ** R = G by A18,EXTENS_1:12;
let K be ManySortedFunction of A, B;
assume
A20: K is_homomorphism A, B;
assume K ** R = G;
then
K ** (((F || FreeGen X()) ** ((Reverse X())"")) ** Reverse X()) = H** (
(F || FreeGen X()) ** ((Reverse X())"")) ** Reverse X() by A19,PBOOLE:140;
then
K ** (((F || FreeGen X()) ** ((Reverse X())"")) ** Reverse X()) = H** (
((F || FreeGen X()) ** ((Reverse X())"")) ** Reverse X()) by PBOOLE:140;
then
K ** ((F || FreeGen X()) ** (((Reverse X()"")) ** Reverse X())) = H** (
((F || FreeGen X()) ** ((Reverse X())"")) ** Reverse X()) by PBOOLE:140;
then
K ** ((F || FreeGen X()) ** (((Reverse X()"")) ** Reverse X())) = H** (
(F || FreeGen X()) ** (((Reverse X()"")) ** Reverse X())) by PBOOLE:140;
then K ** (F || FreeGen X() ** id FreeGen X()) = H** ((F || FreeGen X()) **
(((Reverse X()"")) ** Reverse X())) by A18,A6,MSUALG_3:5;
then
K ** (F || FreeGen X() ** id FreeGen X()) = H** (F || FreeGen X() ** id
FreeGen X()) by A18,A6,MSUALG_3:5;
then K ** (F || FreeGen X()) = H** (F || FreeGen X() ** id FreeGen X()) by
MSUALG_3:3;
then K ** (F || FreeGen X()) = H** (F || FreeGen X()) by MSUALG_3:3;
then (K ** F) || FreeGen X() = H** (F || FreeGen X()) by EXTENS_1:4;
then
A21: (K ** F) || FreeGen X() = (H** F) || FreeGen X() by EXTENS_1:4;
F is_homomorphism FM, A by A9,MSUALG_3:def 8;
then K ** F is_homomorphism FM, B by A20,MSUALG_3:10;
then K ** F = H ** F by A12,A15,A21,EXTENS_1:14;
hence thesis by A17,EXTENS_1:12;
end;
scheme
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
A1: P[A()] and
A2: 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()
proof
consider H being ManySortedFunction of F(), A() such that
A3: H is_homomorphism F(), A() and
A4: a() = H ** fi() by A1,A2;
take H;
thus H is_homomorphism F(), A() by A3;
fi()-hash is_homomorphism FreeMSA ((the carrier of S()) --> NAT), F() by Def1
;
then
A5: H ** (fi()-hash) is_homomorphism FreeMSA ((the carrier of S()) --> NAT),
A() by A3,MSUALG_3:10;
reconsider SN = (the carrier of S()) --> NAT as non-empty ManySortedSet of
the carrier of S();
reconsider h1 = a() as ManySortedFunction of SN, the Sorts of A();
A6: h1-hash is_homomorphism FreeMSA SN, A() by Def1;
h1-hash || FreeGen SN = a() ** Reverse SN by Def1
.= H ** (fi() ** Reverse SN) by A4,PBOOLE:140
.= H ** (fi()-hash || FreeGen ((the carrier of S()) --> NAT)) by Def1
.= (H ** (fi()-hash)) || FreeGen ((the carrier of S()) --> NAT) by
EXTENS_1:4;
hence thesis by A6,A5,EXTENS_1:14;
end;
:: 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
A1: fi()-hash.s().t1() = fi()-hash.s().t2() and
A2: 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()
proof
reconsider fi1 = fi() as ManySortedFunction of (the carrier of S()) --> NAT,
the Sorts of F();
reconsider SN = (the carrier of S()) --> NAT as non-empty ManySortedSet of (
the carrier of S());
let B be non-empty MSAlgebra over S();
assume P[B];
then
A3: P[B];
let h be ManySortedFunction of TermAlg S(), B such that
A4: h is_homomorphism TermAlg S(), B;
reconsider h1 = h as ManySortedFunction of FreeMSA SN, B;
set alfa = (h1 || FreeGen SN) ** ((Reverse SN)"");
A5: alfa-hash is_homomorphism FreeMSA SN, B by Def1;
reconsider alfa1 = alfa as ManySortedFunction of (the carrier of S()) -->
NAT, the Sorts of B;
A6: 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 ** fi1 by A2;
consider H being ManySortedFunction of F(), B such that
H is_homomorphism F(), B and
A7: alfa1-hash = H ** (fi1-hash) from Exhash(A3,A6);
A8: alfa-hash.s().t1() = (H.s() * (fi()-hash).s()).t1() by A7,MSUALG_3:2
.= H.s().(fi()-hash.s().t2()) by A1,FUNCT_2:15
.= (H.s() * (fi()-hash).s()).t2() by FUNCT_2:15
.= alfa-hash.s().t2() by A7,MSUALG_3:2;
rngs Reverse SN = SN by EXTENS_1:10;
then
A9: Reverse SN is "1-1" "onto" by EXTENS_1:9,MSUALG_9:11;
alfa-hash || FreeGen SN = alfa ** Reverse SN by Def1
.= (h1 || FreeGen SN) ** (((Reverse SN)"") ** Reverse SN) by PBOOLE:140
.= (h1 || FreeGen SN) ** id FreeGen SN by A9,MSUALG_3:5
.= h1 || FreeGen SN by MSUALG_3:3;
then
A10: alfa-hash = h1 by A4,A5,EXTENS_1:14;
thus h.s().([t1(),t2()]`1) = h.s().t1()
.= h.s().([t1(),t2()]`2) by A10,A8;
end;
:: 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
A1: 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
A2: P[A()] and
A3: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B]
proof
set I = the carrier of S ();
A4: f().:.:X() is non-empty
proof
let i be object;
assume
A5: i in I;
then reconsider fi = f().i as Function of X().i, (the Sorts of A()).i by
PBOOLE:def 15;
A6: (f().:.:X()).i = fi.:(X().i) by A5,PBOOLE:def 20;
reconsider Xi = X().i as non empty set by A5;
A7: Xi meets Xi;
dom fi = Xi by A5,FUNCT_2:def 1;
hence thesis by A7,A6,RELAT_1:118;
end;
f().:.:X() is ManySortedSubset of the Sorts of A()
proof
let i be object;
assume
A8: i in I;
then reconsider fi = f().i as Function of X().i, (the Sorts of A()).i by
PBOOLE:def 15;
(f().:.:X()).i = fi.:(X().i) by A8,PBOOLE:def 20;
hence thesis;
end;
then reconsider Gen = f().:.:X() as non-empty MSSubset of A() by A4;
set AA = GenMSAlg Gen;
A9: X() is_transformable_to the Sorts of AA;
X() is_transformable_to the Sorts of A();
then
A10: doms f() = X() by MSSUBFAM:17;
then rngs f() = f().:.:X() by EQUATION:13;
then rngs f() is ManySortedSubset of the Sorts of AA by MSUALG_2:def 17;
then rngs f() c= the Sorts of AA by PBOOLE:def 18;
then reconsider
iN = f() as ManySortedFunction of X(), the Sorts of AA by A9,A10,EQUATION:4;
consider IN being ManySortedFunction of A(), AA such that
A11: IN is_homomorphism A(), AA and
A12: IN ** f() = iN and
for K being ManySortedFunction of A(), AA st K is_homomorphism A(), AA &
K ** f() = iN holds IN = K by A1,A2,A3;
the Sorts of AA is ManySortedSubset of the Sorts of A() by MSUALG_2:def 9;
then reconsider h = id the Sorts of AA as ManySortedFunction of AA, A() by
EXTENS_1:5;
consider HIN being ManySortedFunction of A(), A() such that
HIN is_homomorphism A(), A() and
HIN ** f() = h ** iN and
A13: for K being ManySortedFunction of A(), A() st K is_homomorphism A()
, A() & K ** f() = h ** iN holds HIN = K by A1,A2;
h is_monomorphism AA, A() by MSUALG_3:22;
then
A14: h is_homomorphism AA, A() by MSUALG_3:def 9;
reconsider hIN = h ** IN as ManySortedFunction of A(), A();
h ** iN = (h ** IN) ** f() by A12,PBOOLE:140;
then
A15: HIN = hIN by A11,A13,A14,MSUALG_3:10;
A16: A() is MSSubAlgebra of A() by MSUALG_2:5;
f() = h ** iN by MSUALG_3:4;
then (id the Sorts of A()) ** f() = h ** iN by MSUALG_3:4;
then HIN = id the Sorts of A() by A13,MSUALG_3:9;
then
A17: HIN is "onto";
the Sorts of AA = h.:.:(the Sorts of AA) by EQUATION:15
.= the Sorts of A() by A15,A17,EQUATION:2,9;
then AA = A() by A16,MSUALG_2:9;
hence thesis by MSAFREE:3;
end;
scheme
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
A1: 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
A2: P[A()] and
A3: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B]
proof
A4: P[A()] by A2;
set V = (the carrier of S()) --> NAT;
reconsider Gen = the Sorts of FreeMSA V as GeneratorSet of FreeMSA V by
MSAFREE2:6;
A5: F().:.:V c= rngs F() by EQUATION:12;
the Sorts of FreeMSA V is_transformable_to the Sorts of A();
then doms (F()-hash) = the Sorts of FreeMSA V by MSSUBFAM:17;
then
A6: F()-hash.:.:(the Sorts of FreeMSA V) = rngs (F()-hash) by EQUATION:13;
rngs F() c= rngs (F()-hash) by Th1;
then
A7: F().:.:V c= F()-hash.:.:Gen by A6,A5,PBOOLE:13;
A8: F()-hash is_homomorphism FreeMSA V, A() by Def1;
A9: for A being non-empty MSAlgebra over S() for B being strict non-empty
MSSubAlgebra of A st P[A] holds P[B] by A3;
A10: 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 by A1;
F().:.:V is non-empty GeneratorSet of A() from FreeIsGen(A10,A4,A9);
hence thesis by A7,A8,EQUATION:23;
end;
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
A1: Q[A()] and
A2: P[F()] and
A3: 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
A4: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A5: for A being non-empty MSAlgebra over S(), R being MSCongruence of A
st P[A] holds P[QuotMSAlg (A,R)]
proof
set I = the carrier of S(), sA = the Sorts of A();
consider Gen being GeneratorSet of A() such that
A6: Gen is finite-yielding by MSAFREE2:def 10;
reconsider Gen as finite-yielding ManySortedSubset of sA by A6;
consider GEN being non-empty finite-yielding ManySortedSubset of sA such
that
A7: Gen c= GEN by MSUALG_9:7;
consider F being ManySortedFunction of I --> NAT, GEN such that
A8: F is "onto" by MSUALG_9:12;
I --> NAT is_transformable_to GEN;
then reconsider G = F as ManySortedFunction of I --> NAT, sA by EXTENS_1:5;
consider h being ManySortedFunction of F(), A() such that
A9: h is_homomorphism F(), A() and
A10: G = h ** fi() by A1,A3;
reconsider sI1 = the Sorts of Image h as MSSubset of Image h by PBOOLE:def 18
;
A11: GEN is GeneratorSet of A() by A7,MSSCYC_1:21;
reconsider sI = the Sorts of Image h as MSSubset of A() by MSUALG_2:def 9;
GEN is ManySortedSubset of sI
proof
let i be object;
assume i in I;
then reconsider s = i as SortSymbol of S();
let g be object;
assume
A12: g in GEN.i;
reconsider fi = fi().s as sequence of (the Sorts of F()).s;
dom ((h.s)*fi) = NAT by FUNCT_2:def 1
.= dom fi by FUNCT_2:def 1;
then
A14: rng fi c= dom (h.s) by FUNCT_1:15;
rng (F.s) = GEN.s by A8,MSUALG_3:def 3;
then consider x being object such that
A15: x in dom (F.s) and
A16: g = F.s.x by A12,FUNCT_1:def 3;
dom (F.s) = NAT by FUNCT_2:def 1
.= dom fi by FUNCT_2:def 1;
then
A17: fi.x in rng fi by A15,FUNCT_1:def 3;
g = ((h.s)*fi).x by A10,A16,MSUALG_3:2
.= (h.s).(fi.x) by A15,FUNCT_2:15;
then g in (h.s).:((the Sorts of F()).s) by A17,A14,FUNCT_1:def 6;
then g in (h.:.:(the Sorts of F())).s by PBOOLE:def 20;
hence thesis by A9,MSUALG_3:def 12;
end;
then
A18: GenMSAlg GEN is MSSubAlgebra of GenMSAlg sI by EXTENS_1:17;
GenMSAlg sI = GenMSAlg sI1 by EXTENS_1:18;
then GenMSAlg GEN is MSSubAlgebra of Image h by A18,MSUALG_2:21;
then A() is MSSubAlgebra of Image h by A11,MSAFREE:3;
then A() = Image h by MSUALG_2:7;
then
A19: h is_epimorphism F(), A() by A9,MSUALG_3:19;
P[QuotMSAlg (F(),MSCng h)] by A2,A5;
hence thesis by A4,A19,MSUALG_4:6;
end;
scheme
QuotEpi { S() -> non empty non void ManySortedSign, X, Y() -> non-empty
MSAlgebra over S(), P[set] } : P[Y()]
provided
A1: ex H being ManySortedFunction of X(), Y() st H is_epimorphism X(), Y () and
A2: P[X()] and
A3: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A4: for A being non-empty MSAlgebra over S(), R being MSCongruence of A
st P[A] holds P[QuotMSAlg (A,R)]
proof
consider H being ManySortedFunction of X(), Y() such that
A5: H is_epimorphism X(), Y() by A1;
P[QuotMSAlg (X(),MSCng H)] by A2,A4;
hence thesis by A3,A5,MSUALG_4:6;
end;
:: 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
A1: for B being strict non-empty finitely-generated MSSubAlgebra of X()
holds P[B] and
A2: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A3: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B] and
A4: for A being non-empty MSAlgebra over S(), R being MSCongruence of A
st P[A] holds P[QuotMSAlg (A,R)] and
A5: 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]
proof
A6: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[
A] holds P[B] by A2;
set T = the strict non-empty finitely-generated MSSubAlgebra of X();
set CC = { C where C is Element of MSSub X() : ex R being strict non-empty
finitely-generated MSSubAlgebra of X() st R = C };
T in MSSub X() by MSUALG_2:def 19;
then T in CC;
then reconsider CC as non empty set;
defpred P[object,object] means $1 = $2;
:: id C ??? !!!
A7: for c being object st c in CC ex j being object st P[c,j];
consider FF being ManySortedSet of CC such that
A8: for c being object st c in CC holds P[c,FF.c] from PBOOLE:sch 3(A7);
FF is MSAlgebra-Family of CC, S()
proof
let c be object;
assume
A9: c in CC;
then ex Q being Element of MSSub X() st c = Q & ex R being strict
non-empty finitely-generated MSSubAlgebra of X() st R = Q;
hence thesis by A8,A9;
end;
then reconsider FF as MSAlgebra-Family of CC, S();
consider prSOR being strict non-empty MSSubAlgebra of product FF such that
A10: ex BA being ManySortedFunction of prSOR, X() st BA is_epimorphism
prSOR, X() by A8,EQUATION:27;
A11: for A being non-empty MSAlgebra over S(), R being MSCongruence of A st
P[A] holds P[QuotMSAlg (A,R)] by A4;
for i being set st i in CC ex A being MSAlgebra over S() st A = FF.i & P[A]
proof
let i be set;
assume
A12: i in CC;
then consider Q being Element of MSSub X() such that
A13: i = Q and
A14: ex R being strict non-empty finitely-generated MSSubAlgebra of X(
) st R = Q;
consider R being strict non-empty finitely-generated MSSubAlgebra of X()
such that
A15: R = Q by A14;
take R;
thus thesis by A1,A8,A12,A13,A15;
end;
then
A16: P[prSOR] by A3,A5;
thus P[X()] from QuotEpi(A10, A16, A6, A11);
end;
scheme
FreeInModIsInVar1 { S() -> non empty non void ManySortedSign, X() ->
non-empty MSAlgebra over S(), P, Q[set] } : Q[X()]
provided
A1: 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
A2: P[X()]
proof
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 X() |= e
by A2;
hence thesis by A1;
end;
:: 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
A1: 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
A2: 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
A3: Q[X()] and
A4: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A5: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B] and
A6: 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]
proof
A7: 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]
by A6;
set V = (the carrier of S()) --> NAT;
A8: for A being non-empty MSAlgebra over S() for B being strict non-empty
MSSubAlgebra of A st P[A] holds P[B] by A5;
A9: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A
] holds P[B] by A4;
consider A being strict non-empty MSAlgebra over S(), fi being
ManySortedFunction of V, the Sorts of A such that
A10: P[A] and
A11: for B being non-empty MSAlgebra over S() for G being
ManySortedFunction of V, the Sorts of B st P[B] ex H being ManySortedFunction
of A, B st H is_homomorphism A, B & H ** fi = G & for K being
ManySortedFunction of A, B st K is_homomorphism A, B & K ** fi = G holds H = K
from ExFreeAlg2(A9,A8, A7);
A12: for C being non-empty MSAlgebra over S() 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 by A2;
A13: for C being non-empty MSAlgebra over S() 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 & G = h ** psi()
proof
let C be non-empty MSAlgebra over S(), G be ManySortedFunction of V, the
Sorts of C;
assume Q[C];
then consider h being ManySortedFunction of X(), C such that
A14: h is_homomorphism X(), C and
A15: G = h ** psi() and
for K being ManySortedFunction of X(), C st K is_homomorphism X(), C &
K ** psi() = G holds h = K by A2;
take h;
thus thesis by A14,A15;
end;
A16: Q[X()] by A3;
A17: 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 by A1;
A18: Q[A] from FreeInModIsInVar1(A17,A10);
consider H being ManySortedFunction of X(), A such that
A19: H is_homomorphism X(), A and
A20: fi-hash = H ** (psi()-hash) from Exhash(A18,A13);
A21: psi()-hash is_homomorphism FreeMSA V, X() by Def1;
now
let i be set;
assume i in the carrier of S();
then reconsider s = i as SortSymbol of S();
thus H.i is one-to-one
proof
A22: for D being non-empty MSAlgebra over S() for E being strict
non-empty MSSubAlgebra of D holds Q[D] implies Q[E]
proof
let D be non-empty MSAlgebra over S(), E be strict non-empty
MSSubAlgebra of D such that
A23: Q[D];
for s be SortSymbol of S(), e be Element of (Equations S()).s
st for B being non-empty MSAlgebra over S() st P[B] holds B |= e
holds E |= e by A1,A23,EQUATION:31;
hence thesis by A1;
end;
psi()-hash is_epimorphism FreeMSA V, X() from Hashisonto(A12, A16,
A22);
then
A24: psi()-hash is "onto" by MSUALG_3:def 8;
A25: for C being non-empty MSAlgebra over S() for G being
ManySortedFunction of V, the Sorts of C st P[C] ex H being ManySortedFunction
of A, C st H is_homomorphism A, C & G = H ** fi
proof
let C be non-empty MSAlgebra over S(), G be ManySortedFunction of V,
the Sorts of C;
assume P[C];
then consider H being ManySortedFunction of A, C such that
A26: H is_homomorphism A, C and
A27: H ** fi = G and
for K being ManySortedFunction of A, C st K is_homomorphism A, C &
K ** fi = G holds H = K by A11;
take H;
thus thesis by A26,A27;
end;
let a, b be object such that
A28: a in dom (H.i) and
A29: b in dom (H.i) and
A30: H.i.a = H.i.b;
A31: dom (H.s) = (the Sorts of X()).s by FUNCT_2:def 1
.= rng((psi()-hash).s) by A24,MSUALG_3:def 3;
then consider t1 being object such that
A32: t1 in dom (psi()-hash.s) and
A33: psi()-hash.s.t1 = a by A28,FUNCT_1:def 3;
consider t2 being object such that
A34: t2 in dom (psi()-hash.s) and
A35: psi()-hash.s.t2 = b by A29,A31,FUNCT_1:def 3;
reconsider t1, t2 as Element of (the Sorts of TermAlg S()).s by A32,A34;
set e = t1 '=' t2;
A36: fi-hash.s.t1 = ((H.s)*(psi()-hash.s)).t1 by A20,MSUALG_3:2
.= H.s.a by A33,FUNCT_2:15
.= ((H.s)*(psi()-hash.s)).t2 by A30,A35,FUNCT_2:15
.= fi-hash.s.t2 by A20,MSUALG_3:2;
for B being non-empty MSAlgebra over S() st P[B] holds B |= t1 '='
t2 from EqTerms(A36,A25);
then
A37: X() |= e by A1,A3;
thus a = psi()-hash.s.(e`1) by A33
.= psi()-hash.s.(e`2) by A21,A37
.= b by A35;
end;
end;
then H is "1-1" by MSUALG_3:1;
then H is_monomorphism X(), A by A19,MSUALG_3:def 9;
then
A38: X(), Image H are_isomorphic by MSUALG_9:16;
P[Image H] by A5,A10;
hence thesis by A4,A38,MSUALG_3:17;
end;
:: 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 { 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
A1: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A2: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B] and
A3: for A being non-empty MSAlgebra over S(), R being MSCongruence of A
st P[A] holds P[QuotMSAlg (A,R)] and
A4: 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]
proof
A5: for A being non-empty MSAlgebra over S() for B being strict non-empty
MSSubAlgebra of A st P[A] holds P[B] by A2;
set XX = (the carrier of S()) --> NAT;
set I = the carrier of S();
defpred R[object,object] means
ex s being SortSymbol of S() st $1 = s & $2 = {e
where e is Element of (Equations S()).s : for A being non-empty MSAlgebra over
S() holds P[A] implies A |= e};
A6: now
let w be object;
assume w in I;
then consider s being SortSymbol of S() such that
A7: s = w;
reconsider d = {e where e is Element of (Equations S()).s : for A being
non-empty MSAlgebra over S() holds P[A] implies A |= e} as object;
take d;
thus R[w,d] by A7;
end;
consider E being ManySortedSet of I such that
A8: for i being object st i in I holds R[i,E.i] from PBOOLE:sch 3(A6);
E is ManySortedSubset of Equations S()
proof
let j be object;
assume j in I;
then consider s being SortSymbol of S() such that
A9: j = s and
A10: E.j = {e where e is Element of (Equations S()).s : for A being
non-empty MSAlgebra over S() holds P[A] implies A |= e} by A8;
let q be object;
assume q in E.j;
then ex z being Element of (Equations S()).s st q = z & for A being
non-empty MSAlgebra over S() holds P[A] implies A |= z by A10;
hence thesis by A9;
end;
then reconsider E as EqualSet of S();
A11: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A
] holds P[B] by A1;
defpred Q[MSAlgebra over S()] means $1 |= E;
A12: for D being non-empty MSAlgebra over S() holds Q[D] iff for s being
SortSymbol of S(), e being Element of (Equations S()).s st (for M being
non-empty MSAlgebra over S() st P[M] holds M |= e) holds D |= e
proof
let D be non-empty MSAlgebra over S();
thus Q[D] implies 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 D |= e
proof
assume
A13: Q[D];
let s be SortSymbol of S(), e be Element of (Equations S()).s such that
A14: for B being non-empty MSAlgebra over S() st P[B] holds B |= e;
R[s,E.s] by A8;
then e in E.s by A14;
hence thesis by A13,EQUATION:def 6;
end;
assume
A15: 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 D
|= e;
let s be SortSymbol of S(), e be Element of (Equations S()).s such that
A16: e in E.s;
R[s,E.s] by A8;
then ex f being Element of (Equations S()).s st e = f & for A being
non-empty MSAlgebra over S() holds P[A] implies A |= f by A16;
hence thesis by A15;
end;
A17: for A being non-empty MSAlgebra over S() for B being strict non-empty
MSSubAlgebra of A holds Q[A] implies Q[B] by EQUATION:32;
A18: for I being set, F being MSAlgebra-Family of I, S() holds (for i being
set st i in I ex A being MSAlgebra over S() st A = F.i & Q[A]) implies Q[
product F] by EQUATION:38;
A19: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic
holds Q[A] implies Q[B] by EQUATION:34;
consider K being strict non-empty MSAlgebra over S(), F being
ManySortedFunction of XX, the Sorts of K such that
A20: Q[K] and
A21: for B being non-empty MSAlgebra over S() for G being
ManySortedFunction of XX, the Sorts of B st Q[B] ex H being ManySortedFunction
of K, B st H is_homomorphism K, B & H ** F = G & for W being ManySortedFunction
of K, B st W is_homomorphism K, B & W ** F = G holds H = W from ExFreeAlg2(A19,
A17,A18);
A22: for M being non-empty MSAlgebra over S() for G being ManySortedFunction
of (the carrier of S()) --> NAT, the Sorts of M st Q[M] ex H being
ManySortedFunction of K, M st H is_homomorphism K, M & G = H ** F
proof
let M be non-empty MSAlgebra over S(), G be ManySortedFunction of (the
carrier of S()) --> NAT, the Sorts of M;
assume Q[M];
then ex H being ManySortedFunction of K, M st H is_homomorphism K, M & H
** F = G & for W being ManySortedFunction of K, M st W is_homomorphism K, M & W
** F = G holds H = W by A21;
hence ex H being ManySortedFunction of K, M st H is_homomorphism K, M & H
** F = G;
end;
A23: 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]
by A4;
take E;
let A be non-empty MSAlgebra over S();
hereby
assume
A24: P[A];
thus A |= E
proof
let s1 be SortSymbol of S();
A25: R[s1,E.s1] by A8;
let e be Element of (Equations S()).s1;
assume e in E.s1;
then consider x being Element of (Equations S()).s1 such that
A26: e = x and
A27: for A being non-empty MSAlgebra over S() holds P[A] implies A
|= x by A25;
A28: A |= x by A24,A27;
let h be ManySortedFunction of TermAlg S(), A;
assume h is_homomorphism TermAlg S(), A;
hence thesis by A26,A28;
end;
end;
assume
A29: A |= E;
A30: for A being non-empty MSAlgebra over S(), R being MSCongruence of A st P
[A] holds P[QuotMSAlg (A,R)] by A3;
A31: Q[K] by A20;
A32: P[K] from FreeInModIsInVar(A12,A21,A31,A11,A5,A23);
A33: for B being strict non-empty finitely-generated MSSubAlgebra of A holds
P[B]
proof
let B be strict non-empty finitely-generated MSSubAlgebra of A;
A34: Q[B] by A29,EQUATION:32;
thus P[B] from FinGenAlgInVar(A34,A32,A22,A11,A30);
end;
thus P[A] from AllFinGen(A33,A11,A5,A30,A23);
end;