:: Birkhoff Theorem for Many Sorted Algebras
:: by Artur Korni{\l}owicz
::
:: Received June 19, 1997
:: Copyright (c) 1997-2021 Association of Mizar Users


::-------------------------------------------------------------------
:: 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 ;
let X be V2() ManySortedSet of the carrier of S;
let A be non-empty MSAlgebra over S;
let F be ManySortedFunction of X, the Sorts of A;
func F -hash -> ManySortedFunction of (FreeMSA X),A means :Def1: :: BIRKHOFF:def 1
( it is_homomorphism FreeMSA X,A & it || (FreeGen X) = F ** (Reverse X) );
existence
ex b1 being ManySortedFunction of (FreeMSA X),A st
( b1 is_homomorphism FreeMSA X,A & b1 || (FreeGen X) = F ** (Reverse X) ) by MSAFREE:def 5;
uniqueness
for b1, b2 being ManySortedFunction of (FreeMSA X),A st b1 is_homomorphism FreeMSA X,A & b1 || (FreeGen X) = F ** (Reverse X) & b2 is_homomorphism FreeMSA X,A & b2 || (FreeGen X) = F ** (Reverse X) holds
b1 = b2 by EXTENS_1:14;
end;

:: deftheorem Def1 defines -hash BIRKHOFF:def 1 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for F being ManySortedFunction of X, the Sorts of A
for b5 being ManySortedFunction of (FreeMSA X),A holds
( b5 = F -hash iff ( b5 is_homomorphism FreeMSA X,A & b5 || (FreeGen X) = F ** (Reverse X) ) );

theorem Th1: :: BIRKHOFF:1
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for X being V2() ManySortedSet of the carrier of S
for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (F -hash)
proof 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 :: BIRKHOFF:sch 1
ExFreeAlg1{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), P1[ set ] } :
ex A being strict non-empty MSAlgebra over F1() ex F being ManySortedFunction of F2(),A st
( P1[A] & F is_epimorphism F2(),A & ( for B being non-empty MSAlgebra over F1()
for G being ManySortedFunction of F2(),B st G is_homomorphism F2(),B & P1[B] holds
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 F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A2: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] and
A3: for I being set
for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds
ex A being MSAlgebra over F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proof end;

scheme :: BIRKHOFF:sch 2
ExFreeAlg2{ F1() -> non empty non void ManySortedSign , F2() -> V2() ManySortedSet of the carrier of F1(), P1[ set ] } :
ex A being strict non-empty MSAlgebra over F1() ex F being ManySortedFunction of F2(), the Sorts of A st
( P1[A] & ( for B being non-empty MSAlgebra over F1()
for G being ManySortedFunction of F2(), the Sorts of B st P1[B] holds
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 F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A2: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] and
A3: for I being set
for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds
ex A being MSAlgebra over F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proof end;

scheme :: BIRKHOFF:sch 3
Exhash{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> non-empty MSAlgebra over F1(), F4() -> ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2(), F5() -> ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F3(), P1[ set ] } :
ex H being ManySortedFunction of F2(),F3() st
( H is_homomorphism F2(),F3() & F5() -hash = H ** (F4() -hash) )
provided
A1: P1[F3()] and
A2: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds
ex h being ManySortedFunction of F2(),C st
( h is_homomorphism F2(),C & G = h ** F4() )
proof 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 :: BIRKHOFF:sch 4
EqTerms{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2(), F4() -> SortSymbol of F1(), F5() -> Element of the Sorts of (TermAlg F1()) . F4(), F6() -> Element of the Sorts of (TermAlg F1()) . F4(), P1[ set ] } :
for B being non-empty MSAlgebra over F1() st P1[B] holds
B |= F5() '=' F6()
provided
A1: ((F3() -hash) . F4()) . F5() = ((F3() -hash) . F4()) . F6() and
A2: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds
ex h being ManySortedFunction of F2(),C st
( h is_homomorphism F2(),C & G = h ** F3() )
proof 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 :: BIRKHOFF:sch 5
FreeIsGen{ F1() -> non empty non void ManySortedSign , F2() -> V2() ManySortedSet of the carrier of F1(), F3() -> strict non-empty MSAlgebra over F1(), F4() -> ManySortedFunction of F2(), the Sorts of F3(), P1[ set ] } :
F4() .:.: F2() is V2() GeneratorSet of F3()
provided
A1: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of F2(), the Sorts of C st P1[C] holds
ex H being ManySortedFunction of F3(),C st
( H is_homomorphism F3(),C & H ** F4() = G & ( for K being ManySortedFunction of F3(),C st K is_homomorphism F3(),C & K ** F4() = G holds
H = K ) ) and
A2: P1[F3()] and
A3: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B]
proof end;

scheme :: BIRKHOFF:sch 6
Hashisonto{ F1() -> non empty non void ManySortedSign , F2() -> strict non-empty MSAlgebra over F1(), F3() -> ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2(), P1[ set ] } :
F3() -hash is_epimorphism FreeMSA ( the carrier of F1() --> NAT),F2()
provided
A1: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds
ex H being ManySortedFunction of F2(),C st
( H is_homomorphism F2(),C & H ** F3() = G & ( for K being ManySortedFunction of F2(),C st K is_homomorphism F2(),C & K ** F3() = G holds
H = K ) ) and
A2: P1[F2()] and
A3: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B]
proof end;

scheme :: BIRKHOFF:sch 7
FinGenAlgInVar{ F1() -> non empty non void ManySortedSign , F2() -> strict non-empty finitely-generated MSAlgebra over F1(), F3() -> non-empty MSAlgebra over F1(), F4() -> ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F3(), P1[ set ], P2[ set ] } :
P1[F2()]
provided
A1: P2[F2()] and
A2: P1[F3()] and
A3: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P2[C] holds
ex h being ManySortedFunction of F3(),C st
( h is_homomorphism F3(),C & G = h ** F4() ) and
A4: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A5: for A being non-empty MSAlgebra over F1()
for R being MSCongruence of A st P1[A] holds
P1[ QuotMSAlg (A,R)]
proof end;

scheme :: BIRKHOFF:sch 8
QuotEpi{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> non-empty MSAlgebra over F1(), P1[ set ] } :
P1[F3()]
provided
A1: ex H being ManySortedFunction of F2(),F3() st H is_epimorphism F2(),F3() and
A2: P1[F2()] and
A3: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A4: for A being non-empty MSAlgebra over F1()
for R being MSCongruence of A st P1[A] holds
P1[ QuotMSAlg (A,R)]
proof end;

:: An algebra X() belongs to a variety P[] whenever all its finitely
:: generated subalgebras are in P[].
scheme :: BIRKHOFF:sch 9
AllFinGen{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), P1[ set ] } :
P1[F2()]
provided
A1: for B being strict non-empty finitely-generated MSSubAlgebra of F2() holds P1[B] and
A2: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A3: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] and
A4: for A being non-empty MSAlgebra over F1()
for R being MSCongruence of A st P1[A] holds
P1[ QuotMSAlg (A,R)] and
A5: for I being set
for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds
ex A being MSAlgebra over F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proof end;

scheme :: BIRKHOFF:sch 10
FreeInModIsInVar1{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), P1[ set ], P2[ set ] } :
P2[F2()]
provided
A1: for A being non-empty MSAlgebra over F1() holds
( P2[A] iff for s being SortSymbol of F1()
for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds
B |= e ) holds
A |= e ) and
A2: P1[F2()]
proof end;

:: 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{ F1() -> non empty non void ManySortedSign , F2() -> strict non-empty MSAlgebra over F1(), F3() -> ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2(), P1[ set ], P2[ set ] } :
P1[F2()]
provided
A1: for A being non-empty MSAlgebra over F1() holds
( P2[A] iff for s being SortSymbol of F1()
for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds
B |= e ) holds
A |= e ) and
A2: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P2[C] holds
ex H being ManySortedFunction of F2(),C st
( H is_homomorphism F2(),C & H ** F3() = G & ( for K being ManySortedFunction of F2(),C st K is_homomorphism F2(),C & K ** F3() = G holds
H = K ) ) and
A3: P2[F2()] and
A4: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A5: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] and
A6: for I being set
for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds
ex A being MSAlgebra over F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proof end;

:: Let P[] be an abstract class of algebras. Then P[] is an equational class
:: if and only if P[] is variety.
:: WP: Birkhoff Variety Theorem
scheme :: BIRKHOFF:sch 12
Birkhoff{ F1() -> non empty non void ManySortedSign , P1[ set ] } :
ex E being EqualSet of F1() st
for A being non-empty MSAlgebra over F1() holds
( P1[A] iff A |= E )
provided
A1: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A2: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] and
A3: for A being non-empty MSAlgebra over F1()
for R being MSCongruence of A st P1[A] holds
P1[ QuotMSAlg (A,R)] and
A4: for I being set
for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds
ex A being MSAlgebra over F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proof end;