:: 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-2021 Association of Mizar Users

theorem Th1: :: MSSUBLAT:1

for a being set holds (*--> a) . 0 = {}

proof end;

theorem :: MSSUBLAT:2

for a being set holds (*--> a) . 1 = <*a*>

proof end;

theorem :: MSSUBLAT:3

for a being set holds (*--> a) . 2 = <*a,a*>

proof end;

theorem :: MSSUBLAT:4

for a being set holds (*--> a) . 3 = <*a,a,a*>

proof end;

theorem Th5: :: MSSUBLAT:5

for i being Nat
for f being FinSequence of {0} holds
( f = i |-> 0 iff len f = i )

proof end;

theorem Th6: :: MSSUBLAT:6

for i being Nat
for f being FinSequence st f = (*--> 0) . i holds
len f = i

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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)

proof end;

theorem Th12: :: MSSUBLAT:12

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
MSAlg U1 is MSSubAlgebra of MSAlg U2

proof end;

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

proof end;

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

proof end;

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)

proof end;

theorem Th16: :: MSSUBLAT:16

for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
U1 is SubAlgebra of U2

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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

proof end;

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

proof end;

theorem :: MSSUBLAT:22

for A, B being Universal_Algebra holds
( signature A = signature B iff MSSign A = MSSign B )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

:: 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 & b2 = MSAlg b1 holds
the Sorts of a2 (\/) the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1)

proof end;

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 & b2 = MSAlg b1 holds
the Sorts of a2 (/\) the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1)

proof end;

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 & b2 = MSAlg b1 holds
MSAlg (a1 "\/" b1) = a2 "\/" b2

proof end;

registration

let A be with_const_op Universal_Algebra;

cluster MSSign A -> all-with_const_op ;

coherence
( not MSSign A is void & MSSign A is strict & MSSign A is segmental & MSSign A is trivial & MSSign A is all-with_const_op )

proof end;

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 & b2 = MSAlg b1 holds
MSAlg (a1 /\ b1) = a2 /\ b2

proof end;

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 ;

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 ;

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 ;

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

proof end;

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

proof end;