:: The Correspondence Between Lattices of Subalgebras of Universal Algebras and Many Sorted Algebras
:: by Adam Naumowicz and Agnieszka Julia Marasik
::
:: Received September 22, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

theorem Th1: :: MSSUBLAT:1
for a being set holds (*--> a) . 0 = {}
proofend;

theorem :: MSSUBLAT:2
for a being set holds (*--> a) . 1 = <*a*>
proofend;

theorem :: MSSUBLAT:3
for a being set holds (*--> a) . 2 = <*a,a*>
proofend;

theorem :: MSSUBLAT:4
for a being set holds (*--> a) . 3 = <*a,a,a*>
proofend;

theorem Th5: :: MSSUBLAT:5
for i being Nat
for f being FinSequence of {0} holds
( f = i |-> 0 iff len f = i )
proofend;

theorem Th6: :: MSSUBLAT:6
for i being Nat
for f being FinSequence st f = (*--> 0) . i holds
len f = i
proofend;

begin

reconsider z = 0 as Element of {0} by TARSKI:def_1;

theorem Th7: :: MSSUBLAT:7
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
MSSign U1 = MSSign U2
proofend;

theorem Th8: :: MSSUBLAT:8
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
for o being OperSymbol of (MSSign U2)
for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))
proofend;

theorem Th9: :: MSSUBLAT:9
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2)
proofend;

theorem Th10: :: MSSUBLAT:10
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
B is opers_closed
proofend;

theorem Th11: :: MSSUBLAT:11
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
the Charact of (MSAlg U1) = Opers ((MSAlg U2),B)
proofend;

theorem Th12: :: MSSUBLAT:12
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
MSAlg U1 is MSSubAlgebra of MSAlg U2
proofend;

theorem Th13: :: MSSUBLAT:13
for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
the carrier of U1 is Subset of U2
proofend;

theorem Th14: :: MSSUBLAT:14
for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
for B being non empty Subset of U2 st B = the carrier of U1 holds
B is opers_closed
proofend;

theorem Th15: :: MSSUBLAT:15
for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
for B being non empty Subset of U2 st B = the carrier of U1 holds
the charact of U1 = Opers (U2,B)
proofend;

theorem Th16: :: MSSUBLAT:16
for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
U1 is SubAlgebra of U2
proofend;

theorem Th17: :: MSSUBLAT:17
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A)
proofend;

theorem Th18: :: MSSUBLAT:18
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
S is opers_closed
proofend;

theorem Th19: :: MSSUBLAT:19
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
the charact of (1-Alg B) = Opers ((1-Alg A),S)
proofend;

theorem Th20: :: MSSUBLAT:20
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A holds 1-Alg B is SubAlgebra of 1-Alg A
proofend;

theorem Th21: :: MSSUBLAT:21
for S being non empty non void ManySortedSign
for A, B being MSAlgebra over S holds
( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) )
proofend;

theorem :: MSSUBLAT:22
for A, B being Universal_Algebra holds
( signature A = signature B iff MSSign A = MSSign B )
proofend;

theorem Th23: :: MSSUBLAT:23
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #)
proofend;

theorem Th24: :: MSSUBLAT:24
for MS being non void 1 -element segmental ManySortedSign
for A, B being non-empty MSAlgebra over MS st 1-Alg A = 1-Alg B holds
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
proofend;

theorem :: MSSUBLAT:25
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
the Sorts of A = the Sorts of (MSAlg (1-Alg A))
proofend;

theorem Th26: :: MSSUBLAT:26
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #)
proofend;

theorem :: MSSUBLAT:27
for A being Universal_Algebra
for B being strict non-empty MSSubAlgebra of MSAlg A st the carrier of (MSSign A) = {0} holds
1-Alg B is SubAlgebra of A
proofend;

begin

:: The Correspondence Between Lattices of Subalgebras of
:: Universal and Many Sorted Algebras
theorem Th28: :: MSSUBLAT:28
for A being Universal_Algebra
for a1, b1 being strict SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 &amp; b2 = MSAlg b1 holds
the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1)
proofend;

theorem Th29: :: MSSUBLAT:29
for A being Universal_Algebra
for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 &amp; b2 = MSAlg b1 holds
the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1)
proofend;

theorem Th30: :: MSSUBLAT:30
for A being strict Universal_Algebra
for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 &amp; b2 = MSAlg b1 holds
MSAlg (a1 "\/" b1) = a2 "\/" b2
proofend;

registration
let A be with_const_op Universal_Algebra;
cluster MSSign A ->  all-with_const_op ;
coherence
 ( not MSSign A is void &amp; MSSign A is strict &amp; MSSign A is segmental &amp; MSSign A is trivial &amp; MSSign A is all-with_const_op )
proofend;
end;

theorem Th31: :: MSSUBLAT:31
for A being with_const_op Universal_Algebra
for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 &amp; b2 = MSAlg b1 holds
MSAlg (a1 /\ b1) = a2 /\ b2
proofend;

registration
let A be quasi_total UAStr ;
cluster UAStr(# the carrier of A, the charact of A #) ->  quasi_total ;
coherence
 UAStr(# the carrier of A, the charact of A #) is quasi_total
proofend;
end;

registration
let A be partial UAStr ;
cluster UAStr(# the carrier of A, the charact of A #) ->  partial ;
coherence
 UAStr(# the carrier of A, the charact of A #) is partial
proofend;
end;

registration
let A be non-empty UAStr ;
cluster UAStr(# the carrier of A, the charact of A #) ->  non-empty ;
coherence
 UAStr(# the carrier of A, the charact of A #) is non-empty
proofend;
end;

registration
let A be with_const_op Universal_Algebra;
cluster UAStr(# the carrier of A, the charact of A #) ->  with_const_op ;
coherence
 UAStr(# the carrier of A, the charact of A #) is with_const_op
proofend;
end;

theorem :: MSSUBLAT:32
for A being with_const_op Universal_Algebra holds UnSubAlLattice UAStr(# the carrier of A, the charact of A #), MSSubAlLattice (MSAlg UAStr(# the carrier of A, the charact of A #)) are_isomorphic
proofend;