Processing math: 100%

:: 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 b₁ being ManySortedFunction of (FreeMSA X),A st
( b₁ is_homomorphism FreeMSA X,A & b₁ || (FreeGen X) = F ** (Reverse X) ) by MSAFREE:def 5;
uniqueness
for b₁, b₂ being ManySortedFunction of (FreeMSA X),A st b₁ is_homomorphism FreeMSA X,A & b₁ || (FreeGen X) = F ** (Reverse X) & b₂ is_homomorphism FreeMSA X,A & b₂ || (FreeGen X) = F ** (Reverse X) holds
b₁ = b₂ 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 b₅ being ManySortedFunction of (FreeMSA X),A holds
( b₅ = F -hash iff ( b₅ is_homomorphism FreeMSA X,A & b₅ || (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{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra over F₁(), P₁[ set ] } :

ex A being strict non-empty MSAlgebra over F₁() ex F being ManySortedFunction of F₂(),A st
( P₁[A] & F is_epimorphism F₂(),A & ( for B being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of F₂(),B st G is_homomorphism F₂(),B & P₁[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 F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] and
A2: for A being non-empty MSAlgebra over F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B] and
A3: for I being set
for F being MSAlgebra-Family of I,F₁() st ( for i being set st i in I holds
ex A being MSAlgebra over F₁() st
( A = F . i & P₁[A] ) ) holds
P₁[ product F]

proof end;

scheme :: BIRKHOFF:sch 2
ExFreeAlg2{ F₁() -> non empty non void ManySortedSign , F₂() -> V2() ManySortedSet of the carrier of F₁(), P₁[ set ] } :

ex A being strict non-empty MSAlgebra over F₁() ex F being ManySortedFunction of F₂(), the Sorts of A st
( P₁[A] & ( for B being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of F₂(), the Sorts of B st P₁[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 F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] and
A2: for A being non-empty MSAlgebra over F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B] and
A3: for I being set
for F being MSAlgebra-Family of I,F₁() st ( for i being set st i in I holds
ex A being MSAlgebra over F₁() st
( A = F . i & P₁[A] ) ) holds
P₁[ product F]

proof end;

scheme :: BIRKHOFF:sch 3
Exhash{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra over F₁(), F₃() -> non-empty MSAlgebra over F₁(), F₄() -> ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂(), F₅() -> ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₃(), P₁[ set ] } :

ex H being ManySortedFunction of F₂(),F₃() st
( H is_homomorphism F₂(),F₃() & F₅() -hash = H ** (F₄() -hash) )

provided

A1: P₁[F₃()] and
A2: for C being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of C st P₁[C] holds
ex h being ManySortedFunction of F₂(),C st
( h is_homomorphism F₂(),C & G = h ** F₄() )

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{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra over F₁(), F₃() -> ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂(), F₄() -> SortSymbol of F₁(), F₅() -> Element of the Sorts of (TermAlg F₁()) . F₄(), F₆() -> Element of the Sorts of (TermAlg F₁()) . F₄(), P₁[ set ] } :

for B being non-empty MSAlgebra over F₁() st P₁[B] holds
B |= F₅() '=' F₆()

provided

A1: ((F₃() -hash) . F₄()) . F₅() = ((F₃() -hash) . F₄()) . F₆() and
A2: for C being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of C st P₁[C] holds
ex h being ManySortedFunction of F₂(),C st
( h is_homomorphism F₂(),C & G = h ** F₃() )

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{ F₁() -> non empty non void ManySortedSign , F₂() -> V2() ManySortedSet of the carrier of F₁(), F₃() -> strict non-empty MSAlgebra over F₁(), F₄() -> ManySortedFunction of F₂(), the Sorts of F₃(), P₁[ set ] } :

F₄() .:.: F₂() is V2() GeneratorSet of F₃()

provided

A1: for C being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of F₂(), the Sorts of C st P₁[C] holds
ex H being ManySortedFunction of F₃(),C st
( H is_homomorphism F₃(),C & H ** F₄() = G & ( for K being ManySortedFunction of F₃(),C st K is_homomorphism F₃(),C & K ** F₄() = G holds
H = K ) ) and
A2: P₁[F₃()] and
A3: for A being non-empty MSAlgebra over F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B]

proof end;

scheme :: BIRKHOFF:sch 6
Hashisonto{ F₁() -> non empty non void ManySortedSign , F₂() -> strict non-empty MSAlgebra over F₁(), F₃() -> ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂(), P₁[ set ] } :

F₃() -hash is_epimorphism FreeMSA ( the carrier of F₁() --> NAT),F₂()

provided

A1: for C being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of C st P₁[C] holds
ex H being ManySortedFunction of F₂(),C st
( H is_homomorphism F₂(),C & H ** F₃() = G & ( for K being ManySortedFunction of F₂(),C st K is_homomorphism F₂(),C & K ** F₃() = G holds
H = K ) ) and
A2: P₁[F₂()] and
A3: for A being non-empty MSAlgebra over F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B]

proof end;

scheme :: BIRKHOFF:sch 7
FinGenAlgInVar{ F₁() -> non empty non void ManySortedSign , F₂() -> strict non-empty finitely-generated MSAlgebra over F₁(), F₃() -> non-empty MSAlgebra over F₁(), F₄() -> ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₃(), P₁[ set ], P₂[ set ] } :

P₁[F₂()]

provided

A1: P₂[F₂()] and
A2: P₁[F₃()] and
A3: for C being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of C st P₂[C] holds
ex h being ManySortedFunction of F₃(),C st
( h is_homomorphism F₃(),C & G = h ** F₄() ) and
A4: for A, B being non-empty MSAlgebra over F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] and
A5: for A being non-empty MSAlgebra over F₁()
for R being MSCongruence of A st P₁[A] holds
P₁[ QuotMSAlg (A,R)]

proof end;

scheme :: BIRKHOFF:sch 8
QuotEpi{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra over F₁(), F₃() -> non-empty MSAlgebra over F₁(), P₁[ set ] } :

P₁[F₃()]

provided

A1: ex H being ManySortedFunction of F₂(),F₃() st H is_epimorphism F₂(),F₃() and
A2: P₁[F₂()] and
A3: for A, B being non-empty MSAlgebra over F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] and
A4: for A being non-empty MSAlgebra over F₁()
for R being MSCongruence of A st P₁[A] holds
P₁[ 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{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra over F₁(), P₁[ set ] } :

P₁[F₂()]

provided

A1: for B being strict non-empty finitely-generated MSSubAlgebra of F₂() holds P₁[B] and
A2: for A, B being non-empty MSAlgebra over F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] and
A3: for A being non-empty MSAlgebra over F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B] and
A4: for A being non-empty MSAlgebra over F₁()
for R being MSCongruence of A st P₁[A] holds
P₁[ QuotMSAlg (A,R)] and
A5: for I being set
for F being MSAlgebra-Family of I,F₁() st ( for i being set st i in I holds
ex A being MSAlgebra over F₁() st
( A = F . i & P₁[A] ) ) holds
P₁[ product F]

proof end;

scheme :: BIRKHOFF:sch 10
FreeInModIsInVar1{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra over F₁(), P₁[ set ], P₂[ set ] } :

P₂[F₂()]

provided

A1: for A being non-empty MSAlgebra over F₁() holds
( P₂[A] iff for s being SortSymbol of F₁()
for e being Element of (Equations F₁()) . s st ( for B being non-empty MSAlgebra over F₁() st P₁[B] holds
B |= e ) holds
A |= e ) and
A2: P₁[F₂()]

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{ F₁() -> non empty non void ManySortedSign , F₂() -> strict non-empty MSAlgebra over F₁(), F₃() -> ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂(), P₁[ set ], P₂[ set ] } :

P₁[F₂()]

provided

A1: for A being non-empty MSAlgebra over F₁() holds
( P₂[A] iff for s being SortSymbol of F₁()
for e being Element of (Equations F₁()) . s st ( for B being non-empty MSAlgebra over F₁() st P₁[B] holds
B |= e ) holds
A |= e ) and
A2: for C being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of C st P₂[C] holds
ex H being ManySortedFunction of F₂(),C st
( H is_homomorphism F₂(),C & H ** F₃() = G & ( for K being ManySortedFunction of F₂(),C st K is_homomorphism F₂(),C & K ** F₃() = G holds
H = K ) ) and
A3: P₂[F₂()] and
A4: for A, B being non-empty MSAlgebra over F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] and
A5: for A being non-empty MSAlgebra over F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B] and
A6: for I being set
for F being MSAlgebra-Family of I,F₁() st ( for i being set st i in I holds
ex A being MSAlgebra over F₁() st
( A = F . i & P₁[A] ) ) holds
P₁[ 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.
:: Birkhoff Variety Theorem

scheme :: BIRKHOFF:sch 12
Birkhoff{ F₁() -> non empty non void ManySortedSign , P₁[ set ] } :

ex E being EqualSet of F₁() st
for A being non-empty MSAlgebra over F₁() holds
( P₁[A] iff A |= E )

provided

A1: for A, B being non-empty MSAlgebra over F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] and
A2: for A being non-empty MSAlgebra over F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B] and
A3: for A being non-empty MSAlgebra over F₁()
for R being MSCongruence of A st P₁[A] holds
P₁[ QuotMSAlg (A,R)] and
A4: for I being set
for F being MSAlgebra-Family of I,F₁() st ( for i being set st i in I holds
ex A being MSAlgebra over F₁() st
( A = F . i & P₁[A] ) ) holds
P₁[ product F]

proof end;