:: by Artur Korni{\l}owicz

::

:: Received June 19, 1997

:: Copyright (c) 1997-2018 Association of Mizar Users

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;

ex b_{1} being ManySortedFunction of (FreeMSA X),A st

( b_{1} is_homomorphism FreeMSA X,A & b_{1} || (FreeGen X) = F ** (Reverse X) )
by MSAFREE:def 5;

uniqueness

for b_{1}, b_{2} being ManySortedFunction of (FreeMSA X),A st b_{1} is_homomorphism FreeMSA X,A & b_{1} || (FreeGen X) = F ** (Reverse X) & b_{2} is_homomorphism FreeMSA X,A & b_{2} || (FreeGen X) = F ** (Reverse X) holds

b_{1} = b_{2}
by EXTENS_1:14;

end;
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 ( it is_homomorphism FreeMSA X,A & it || (FreeGen X) = F ** (Reverse X) );

ex b

( b

uniqueness

for b

b

:: 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_{5} being ManySortedFunction of (FreeMSA X),A holds

( b_{5} = F -hash iff ( b_{5} is_homomorphism FreeMSA X,A & b_{5} || (FreeGen X) = F ** (Reverse X) ) );

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

( b

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)

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[].

:: subalgebras and products, the free algebras exist in P[].

scheme :: BIRKHOFF:sch 1

ExFreeAlg1{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), P_{1}[ set ] } :

ExFreeAlg1{ F

ex A being strict non-empty MSAlgebra over F_{1}() ex F being ManySortedFunction of F_{2}(),A st

( P_{1}[A] & F is_epimorphism F_{2}(),A & ( for B being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of F_{2}(),B st G is_homomorphism F_{2}(),B & P_{1}[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( P

for G being ManySortedFunction of F

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 ) ) ) )

A1:
for A, B being non-empty MSAlgebra over F_{1}() st A,B are_isomorphic & P_{1}[A] holds

P_{1}[B]
and

A2: for A being non-empty MSAlgebra over F_{1}()

for B being strict non-empty MSSubAlgebra of A st P_{1}[A] holds

P_{1}[B]
and

A3: for I being set

for F being MSAlgebra-Family of I,F_{1}() st ( for i being set st i in I holds

ex A being MSAlgebra over F_{1}() st

( A = F . i & P_{1}[A] ) ) holds

P_{1}[ product F]

P

A2: for A being non-empty MSAlgebra over F

for B being strict non-empty MSSubAlgebra of A st P

P

A3: for I being set

for F being MSAlgebra-Family of I,F

ex A being MSAlgebra over F

( A = F . i & P

P

proof end;

scheme :: BIRKHOFF:sch 2

ExFreeAlg2{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> V2() ManySortedSet of the carrier of F_{1}(), P_{1}[ set ] } :

ExFreeAlg2{ F

ex A being strict non-empty MSAlgebra over F_{1}() ex F being ManySortedFunction of F_{2}(), the Sorts of A st

( P_{1}[A] & ( for B being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of F_{2}(), the Sorts of B st P_{1}[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( P

for G being ManySortedFunction of F

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 ) ) ) )

A1:
for A, B being non-empty MSAlgebra over F_{1}() st A,B are_isomorphic & P_{1}[A] holds

P_{1}[B]
and

A2: for A being non-empty MSAlgebra over F_{1}()

for B being strict non-empty MSSubAlgebra of A st P_{1}[A] holds

P_{1}[B]
and

A3: for I being set

for F being MSAlgebra-Family of I,F_{1}() st ( for i being set st i in I holds

ex A being MSAlgebra over F_{1}() st

( A = F . i & P_{1}[A] ) ) holds

P_{1}[ product F]

P

A2: for A being non-empty MSAlgebra over F

for B being strict non-empty MSSubAlgebra of A st P

P

A3: for I being set

for F being MSAlgebra-Family of I,F

ex A being MSAlgebra over F

( A = F . i & P

P

proof end;

scheme :: BIRKHOFF:sch 3

Exhash{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), F_{3}() -> non-empty MSAlgebra over F_{1}(), F_{4}() -> ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of F_{2}(), F_{5}() -> ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of F_{3}(), P_{1}[ set ] } :

Exhash{ F

ex H being ManySortedFunction of F_{2}(),F_{3}() st

( H is_homomorphism F_{2}(),F_{3}() & F_{5}() -hash = H ** (F_{4}() -hash) )

provided( H is_homomorphism F

A1:
P_{1}[F_{3}()]
and

A2: for C being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of C st P_{1}[C] holds

ex h being ManySortedFunction of F_{2}(),C st

( h is_homomorphism F_{2}(),C & G = h ** F_{4}() )

A2: for C being non-empty MSAlgebra over F

for G being ManySortedFunction of the carrier of F

ex h being ManySortedFunction of F

( h is_homomorphism 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()].

:: relative to fi() exists, then

:: P[] |= [t1(),t2()] iff (F(),fi()) |= [t1(),t2()].

scheme :: BIRKHOFF:sch 4

EqTerms{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), F_{3}() -> ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of F_{2}(), F_{4}() -> SortSymbol of F_{1}(), F_{5}() -> Element of the Sorts of (TermAlg F_{1}()) . F_{4}(), F_{6}() -> Element of the Sorts of (TermAlg F_{1}()) . F_{4}(), P_{1}[ set ] } :

provided

EqTerms{ F

provided

A1:
((F_{3}() -hash) . F_{4}()) . F_{5}() = ((F_{3}() -hash) . F_{4}()) . F_{6}()
and

A2: for C being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of C st P_{1}[C] holds

ex h being ManySortedFunction of F_{2}(),C st

( h is_homomorphism F_{2}(),C & G = h ** F_{3}() )

A2: for C being non-empty MSAlgebra over F

for G being ManySortedFunction of the carrier of F

ex h being ManySortedFunction of F

( h is_homomorphism 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().

:: subalgebras. The free algebra in P[] over X(), if it exists,

:: is generated by X().

scheme :: BIRKHOFF:sch 5

FreeIsGen{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> V2() ManySortedSet of the carrier of F_{1}(), F_{3}() -> strict non-empty MSAlgebra over F_{1}(), F_{4}() -> ManySortedFunction of F_{2}(), the Sorts of F_{3}(), P_{1}[ set ] } :

provided

FreeIsGen{ F

provided

A1:
for C being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of F_{2}(), the Sorts of C st P_{1}[C] holds

ex H being ManySortedFunction of F_{3}(),C st

( H is_homomorphism F_{3}(),C & H ** F_{4}() = G & ( for K being ManySortedFunction of F_{3}(),C st K is_homomorphism F_{3}(),C & K ** F_{4}() = G holds

H = K ) ) and

A2: P_{1}[F_{3}()]
and

A3: for A being non-empty MSAlgebra over F_{1}()

for B being strict non-empty MSSubAlgebra of A st P_{1}[A] holds

P_{1}[B]

for G being ManySortedFunction of F

ex H being ManySortedFunction of F

( H is_homomorphism F

H = K ) ) and

A2: P

A3: for A being non-empty MSAlgebra over F

for B being strict non-empty MSSubAlgebra of A st P

P

proof end;

scheme :: BIRKHOFF:sch 6

Hashisonto{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> strict non-empty MSAlgebra over F_{1}(), F_{3}() -> ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of F_{2}(), P_{1}[ set ] } :

provided

Hashisonto{ F

provided

A1:
for C being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of C st P_{1}[C] holds

ex H being ManySortedFunction of F_{2}(),C st

( H is_homomorphism F_{2}(),C & H ** F_{3}() = G & ( for K being ManySortedFunction of F_{2}(),C st K is_homomorphism F_{2}(),C & K ** F_{3}() = G holds

H = K ) ) and

A2: P_{1}[F_{2}()]
and

A3: for A being non-empty MSAlgebra over F_{1}()

for B being strict non-empty MSSubAlgebra of A st P_{1}[A] holds

P_{1}[B]

for G being ManySortedFunction of the carrier of F

ex H being ManySortedFunction of F

( H is_homomorphism F

H = K ) ) and

A2: P

A3: for A being non-empty MSAlgebra over F

for B being strict non-empty MSSubAlgebra of A st P

P

proof end;

scheme :: BIRKHOFF:sch 7

FinGenAlgInVar{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> strict non-empty finitely-generated MSAlgebra over F_{1}(), F_{3}() -> non-empty MSAlgebra over F_{1}(), F_{4}() -> ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of F_{3}(), P_{1}[ set ], P_{2}[ set ] } :

provided

FinGenAlgInVar{ F

provided

A1:
P_{2}[F_{2}()]
and

A2: P_{1}[F_{3}()]
and

A3: for C being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of C st P_{2}[C] holds

ex h being ManySortedFunction of F_{3}(),C st

( h is_homomorphism F_{3}(),C & G = h ** F_{4}() )
and

A4: for A, B being non-empty MSAlgebra over F_{1}() st A,B are_isomorphic & P_{1}[A] holds

P_{1}[B]
and

A5: for A being non-empty MSAlgebra over F_{1}()

for R being MSCongruence of A st P_{1}[A] holds

P_{1}[ QuotMSAlg (A,R)]

A2: P

A3: for C being non-empty MSAlgebra over F

for G being ManySortedFunction of the carrier of F

ex h being ManySortedFunction of F

( h is_homomorphism F

A4: for A, B being non-empty MSAlgebra over F

P

A5: for A being non-empty MSAlgebra over F

for R being MSCongruence of A st P

P

proof end;

scheme :: BIRKHOFF:sch 8

QuotEpi{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), F_{3}() -> non-empty MSAlgebra over F_{1}(), P_{1}[ set ] } :

provided

QuotEpi{ F

provided

A1:
ex H being ManySortedFunction of F_{2}(),F_{3}() st H is_epimorphism F_{2}(),F_{3}()
and

A2: P_{1}[F_{2}()]
and

A3: for A, B being non-empty MSAlgebra over F_{1}() st A,B are_isomorphic & P_{1}[A] holds

P_{1}[B]
and

A4: for A being non-empty MSAlgebra over F_{1}()

for R being MSCongruence of A st P_{1}[A] holds

P_{1}[ QuotMSAlg (A,R)]

A2: P

A3: for A, B being non-empty MSAlgebra over F

P

A4: for A being non-empty MSAlgebra over F

for R being MSCongruence of A st P

P

proof end;

:: An algebra X() belongs to a variety P[] whenever all its finitely

:: generated subalgebras are in P[].

:: generated subalgebras are in P[].

scheme :: BIRKHOFF:sch 9

AllFinGen{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), P_{1}[ set ] } :

provided

AllFinGen{ F

provided

A1:
for B being strict non-empty finitely-generated MSSubAlgebra of F_{2}() holds P_{1}[B]
and

A2: for A, B being non-empty MSAlgebra over F_{1}() st A,B are_isomorphic & P_{1}[A] holds

P_{1}[B]
and

A3: for A being non-empty MSAlgebra over F_{1}()

for B being strict non-empty MSSubAlgebra of A st P_{1}[A] holds

P_{1}[B]
and

A4: for A being non-empty MSAlgebra over F_{1}()

for R being MSCongruence of A st P_{1}[A] holds

P_{1}[ QuotMSAlg (A,R)]
and

A5: for I being set

for F being MSAlgebra-Family of I,F_{1}() st ( for i being set st i in I holds

ex A being MSAlgebra over F_{1}() st

( A = F . i & P_{1}[A] ) ) holds

P_{1}[ product F]

A2: for A, B being non-empty MSAlgebra over F

P

A3: for A being non-empty MSAlgebra over F

for B being strict non-empty MSSubAlgebra of A st P

P

A4: for A being non-empty MSAlgebra over F

for R being MSCongruence of A st P

P

A5: for I being set

for F being MSAlgebra-Family of I,F

ex A being MSAlgebra over F

( A = F . i & P

P

proof end;

scheme :: BIRKHOFF:sch 10

FreeInModIsInVar1{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), P_{1}[ set ], P_{2}[ set ] } :

provided

FreeInModIsInVar1{ F

provided

A1:
for A being non-empty MSAlgebra over F_{1}() holds

( P_{2}[A] iff for s being SortSymbol of F_{1}()

for e being Element of (Equations F_{1}()) . s st ( for B being non-empty MSAlgebra over F_{1}() st P_{1}[B] holds

B |= e ) holds

A |= e ) and

A2: P_{1}[F_{2}()]

( P

for e being Element of (Equations F

B |= e ) holds

A |= e ) and

A2: P

proof end;

:: If P[] is a non empty variety, then the free algebras in Mod Eq P[]

:: belong to P[]. (Q[] = Mod Eq P[])

:: belong to P[]. (Q[] = Mod Eq P[])

scheme :: BIRKHOFF:sch 11

FreeInModIsInVar{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> strict non-empty MSAlgebra over F_{1}(), F_{3}() -> ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of F_{2}(), P_{1}[ set ], P_{2}[ set ] } :

provided

FreeInModIsInVar{ F

provided

A1:
for A being non-empty MSAlgebra over F_{1}() holds

( P_{2}[A] iff for s being SortSymbol of F_{1}()

for e being Element of (Equations F_{1}()) . s st ( for B being non-empty MSAlgebra over F_{1}() st P_{1}[B] holds

B |= e ) holds

A |= e ) and

A2: for C being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of the carrier of F_{1}() --> NAT, the Sorts of C st P_{2}[C] holds

ex H being ManySortedFunction of F_{2}(),C st

( H is_homomorphism F_{2}(),C & H ** F_{3}() = G & ( for K being ManySortedFunction of F_{2}(),C st K is_homomorphism F_{2}(),C & K ** F_{3}() = G holds

H = K ) ) and

A3: P_{2}[F_{2}()]
and

A4: for A, B being non-empty MSAlgebra over F_{1}() st A,B are_isomorphic & P_{1}[A] holds

P_{1}[B]
and

A5: for A being non-empty MSAlgebra over F_{1}()

for B being strict non-empty MSSubAlgebra of A st P_{1}[A] holds

P_{1}[B]
and

A6: for I being set

for F being MSAlgebra-Family of I,F_{1}() st ( for i being set st i in I holds

ex A being MSAlgebra over F_{1}() st

( A = F . i & P_{1}[A] ) ) holds

P_{1}[ product F]

( P

for e being Element of (Equations F

B |= e ) holds

A |= e ) and

A2: for C being non-empty MSAlgebra over F

for G being ManySortedFunction of the carrier of F

ex H being ManySortedFunction of F

( H is_homomorphism F

H = K ) ) and

A3: P

A4: for A, B being non-empty MSAlgebra over F

P

A5: for A being non-empty MSAlgebra over F

for B being strict non-empty MSSubAlgebra of A st P

P

A6: for I being set

for F being MSAlgebra-Family of I,F

ex A being MSAlgebra over F

( A = F . i & P

P

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

:: if and only if P[] is variety.

:: Birkhoff Variety Theorem

scheme :: BIRKHOFF:sch 12

Birkhoff{ F_{1}() -> non empty non void ManySortedSign , P_{1}[ set ] } :

Birkhoff{ F

ex E being EqualSet of F_{1}() st

for A being non-empty MSAlgebra over F_{1}() holds

( P_{1}[A] iff A |= E )

providedfor A being non-empty MSAlgebra over F

( P

A1:
for A, B being non-empty MSAlgebra over F_{1}() st A,B are_isomorphic & P_{1}[A] holds

P_{1}[B]
and

A2: for A being non-empty MSAlgebra over F_{1}()

for B being strict non-empty MSSubAlgebra of A st P_{1}[A] holds

P_{1}[B]
and

A3: for A being non-empty MSAlgebra over F_{1}()

for R being MSCongruence of A st P_{1}[A] holds

P_{1}[ QuotMSAlg (A,R)]
and

A4: for I being set

for F being MSAlgebra-Family of I,F_{1}() st ( for i being set st i in I holds

ex A being MSAlgebra over F_{1}() st

( A = F . i & P_{1}[A] ) ) holds

P_{1}[ product F]

P

A2: for A being non-empty MSAlgebra over F

for B being strict non-empty MSSubAlgebra of A st P

P

A3: for A being non-empty MSAlgebra over F

for R being MSCongruence of A st P

P

A4: for I being set

for F being MSAlgebra-Family of I,F

ex A being MSAlgebra over F

( A = F . i & P

P

proof end;

:: Acknowledgements:

:: =================

::

:: I would like to thank Professor Andrzej Trybulec

:: for his help in the preparation of the article.

::-------------------------------------------------------------------