:: Subalgebras of the Universal Algebra. Lattices of Subalgebras
:: by Ewa Burakowska
::
:: Received July 8, 1993
:: Copyright (c) 1993 Association of Mizar Users

begin

definition

let U1 be Universal_Algebra;
mode PFuncsDomHQN of U1 is PFuncsDomHQN of the carrier of U1;

end;

definition

let U1 be UAStr ;
mode PartFunc of U1 is PartFunc of ( the carrier of U1 *), the carrier of U1;

end;

definition

canceled;
let U1, U2 be Universal_Algebra;
pred U1,U2 are_similar means :Def2: :: UNIALG_2:def 2
signature U1 = signature U2;
symmetry
for U1, U2 being Universal_Algebra st signature U1 = signature U2 holds
signature U2 = signature U1 ;
reflexivity
for U1 being Universal_Algebra holds signature U1 = signature U1 ;

end;

:: deftheorem UNIALG_2:def 1 :
canceled;

:: deftheorem Def2 defines are_similar UNIALG_2:def 2 :
for U1, U2 being Universal_Algebra holds
( U1,U2 are_similar iff signature U1 = signature U2 );

theorem :: UNIALG_2:1

canceled;

theorem :: UNIALG_2:2

canceled;

theorem :: UNIALG_2:3

for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
len the charact of U1 = len the charact of U2

proof end;

theorem :: UNIALG_2:4

for U1, U2, U3 being Universal_Algebra st U1,U2 are_similar & U2,U3 are_similar holds
U1,U3 are_similar

proof end;

theorem :: UNIALG_2:5

for U0 being Universal_Algebra holds rng the charact of U0 is non empty Subset of (PFuncs (( the carrier of U0 *), the carrier of U0)) by FINSEQ_1:def 4, RELAT_1:64;

definition

let U0 be Universal_Algebra;
func Operations U0 -> PFuncsDomHQN of U0 equals :: UNIALG_2:def 3
rng the charact of U0;
coherence
rng the charact of U0 is PFuncsDomHQN of U0

proof end;

end;

:: deftheorem defines Operations UNIALG_2:def 3 :
for U0 being Universal_Algebra holds Operations U0 = rng the charact of U0;

definition

let U1 be Universal_Algebra;
mode operation of U1 is Element of Operations U1;

end;

definition

let U0 be Universal_Algebra;
let A be Subset of U0;
let o be operation of U0;
pred A is_closed_on o means :Def4: :: UNIALG_2:def 4
for s being FinSequence of A st len s = arity o holds
o . s in A;

end;

:: deftheorem Def4 defines is_closed_on UNIALG_2:def 4 :
for U0 being Universal_Algebra
for A being Subset of U0
for o being operation of U0 holds
( A is_closed_on o iff for s being FinSequence of A st len s = arity o holds
o . s in A );

definition

let U0 be Universal_Algebra;
let A be Subset of U0;
attr A is opers_closed means :Def5: :: UNIALG_2:def 5
for o being operation of U0 holds A is_closed_on o;

end;

:: deftheorem Def5 defines opers_closed UNIALG_2:def 5 :
for U0 being Universal_Algebra
for A being Subset of U0 holds
( A is opers_closed iff for o being operation of U0 holds A is_closed_on o );

definition

let U0 be Universal_Algebra;
let A be non empty Subset of U0;
let o be operation of U0;
assume A1: A is_closed_on o ;
func o /. A -> non empty homogeneous quasi_total PartFunc of (A *),A equals :Def6: :: UNIALG_2:def 6
o | ((arity o) -tuples_on A);
coherence
o | ((arity o) -tuples_on A) is non empty homogeneous quasi_total PartFunc of (A *),A

proof end;

end;

:: deftheorem Def6 defines /. UNIALG_2:def 6 :
for U0 being Universal_Algebra
for A being non empty Subset of U0
for o being operation of U0 st A is_closed_on o holds
o /. A = o | ((arity o) -tuples_on A);

definition

let U0 be Universal_Algebra;
let A be non empty Subset of U0;
func Opers (U0,A) -> PFuncFinSequence of A means :Def7: :: UNIALG_2:def 7
( dom it = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom it & o = the charact of U0 . n holds
it . n = o /. A ) );
existence
ex b₁ being PFuncFinSequence of A st
( dom b₁ = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom b₁ & o = the charact of U0 . n holds
b₁ . n = o /. A ) )

proof end;

uniqueness
for b₁, b₂ being PFuncFinSequence of A st dom b₁ = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom b₁ & o = the charact of U0 . n holds
b₁ . n = o /. A ) & dom b₂ = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom b₂ & o = the charact of U0 . n holds
b₂ . n = o /. A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines Opers UNIALG_2:def 7 :
for U0 being Universal_Algebra
for A being non empty Subset of U0
for b₃ being PFuncFinSequence of A holds
( b₃ = Opers (U0,A) iff ( dom b₃ = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom b₃ & o = the charact of U0 . n holds
b₃ . n = o /. A ) ) );

theorem :: UNIALG_2:6

canceled;

theorem Th7: :: UNIALG_2:7

for U0 being Universal_Algebra
for B being non empty Subset of U0 st B = the carrier of U0 holds
( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) )

proof end;

theorem :: UNIALG_2:8

for U1 being Universal_Algebra
for A being non empty Subset of U1
for o being operation of U1 st A is_closed_on o holds
arity (o /. A) = arity o

proof end;

definition

let U0 be Universal_Algebra;
mode SubAlgebra of U0 -> Universal_Algebra means :Def8: :: UNIALG_2:def 8
( the carrier of it is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of it holds
( the charact of it = Opers (U0,B) & B is opers_closed ) ) );
existence
ex b₁ being Universal_Algebra st
( the carrier of b₁ is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of b₁ holds
( the charact of b₁ = Opers (U0,B) & B is opers_closed ) ) )

proof end;

end;

:: deftheorem Def8 defines SubAlgebra UNIALG_2:def 8 :
for U0, b₂ being Universal_Algebra holds
( b₂ is SubAlgebra of U0 iff ( the carrier of b₂ is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of b₂ holds
( the charact of b₂ = Opers (U0,B) & B is opers_closed ) ) ) );

registration

let U0 be Universal_Algebra;
cluster non empty strict V76() quasi_total non-empty SubAlgebra of U0;
existence
ex b₁ being SubAlgebra of U0 st b₁ is strict

proof end;

end;

theorem Th9: :: UNIALG_2:9

for U0, U1 being Universal_Algebra
for o0 being operation of U0
for o1 being operation of U1
for n being Nat st U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n holds
arity o0 = arity o1

proof end;

theorem Th10: :: UNIALG_2:10

for U0, U1 being Universal_Algebra st U0 is SubAlgebra of U1 holds
dom the charact of U0 = dom the charact of U1

proof end;

theorem :: UNIALG_2:11

for U0 being Universal_Algebra holds U0 is SubAlgebra of U0

proof end;

theorem :: UNIALG_2:12

for U0, U1, U2 being Universal_Algebra st U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 holds
U0 is SubAlgebra of U2

proof end;

theorem Th13: :: UNIALG_2:13

for U1, U2 being Universal_Algebra st U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 holds
U1 = U2

proof end;

theorem Th14: :: UNIALG_2:14

for U0 being Universal_Algebra
for U1, U2 being SubAlgebra of U0 st the carrier of U1 c= the carrier of U2 holds
U1 is SubAlgebra of U2

proof end;

theorem Th15: :: UNIALG_2:15

for U0 being Universal_Algebra
for U1, U2 being strict SubAlgebra of U0 st the carrier of U1 = the carrier of U2 holds
U1 = U2

proof end;

theorem :: UNIALG_2:16

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
U1,U2 are_similar

proof end;

theorem Th17: :: UNIALG_2:17

for U0 being Universal_Algebra
for A being non empty Subset of U0 holds UAStr(# A,(Opers (U0,A)) #) is strict Universal_Algebra

proof end;

definition

let U0 be Universal_Algebra;
let A be non empty Subset of U0;
assume A1: A is opers_closed ;
func UniAlgSetClosed A -> strict SubAlgebra of U0 equals :Def9: :: UNIALG_2:def 9
UAStr(# A,(Opers (U0,A)) #);
coherence
UAStr(# A,(Opers (U0,A)) #) is strict SubAlgebra of U0

proof end;

end;

:: deftheorem Def9 defines UniAlgSetClosed UNIALG_2:def 9 :
for U0 being Universal_Algebra
for A being non empty Subset of U0 st A is opers_closed holds
UniAlgSetClosed A = UAStr(# A,(Opers (U0,A)) #);

definition

let U0 be Universal_Algebra;
let U1, U2 be SubAlgebra of U0;
assume A1: the carrier of U1 meets the carrier of U2 ;
func U1 /\ U2 -> strict SubAlgebra of U0 means :Def10: :: UNIALG_2:def 10
( the carrier of it = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of it holds
( the charact of it = Opers (U0,B) & B is opers_closed ) ) );
existence
ex b₁ being strict SubAlgebra of U0 st
( the carrier of b₁ = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b₁ holds
( the charact of b₁ = Opers (U0,B) & B is opers_closed ) ) )

proof end;

uniqueness
for b₁, b₂ being strict SubAlgebra of U0 st the carrier of b₁ = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b₁ holds
( the charact of b₁ = Opers (U0,B) & B is opers_closed ) ) & the carrier of b₂ = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b₂ holds
( the charact of b₂ = Opers (U0,B) & B is opers_closed ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines /\ UNIALG_2:def 10 :
for U0 being Universal_Algebra
for U1, U2 being SubAlgebra of U0 st the carrier of U1 meets the carrier of U2 holds
for b₄ being strict SubAlgebra of U0 holds
( b₄ = U1 /\ U2 iff ( the carrier of b₄ = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b₄ holds
( the charact of b₄ = Opers (U0,B) & B is opers_closed ) ) ) );

definition

let U0 be Universal_Algebra;
func Constants U0 -> Subset of U0 equals :: UNIALG_2:def 11
{ a where a is Element of U0 : ex o being operation of U0 st
( arity o = 0 & a in rng o ) } ;
coherence
{ a where a is Element of U0 : ex o being operation of U0 st
( arity o = 0 & a in rng o ) } is Subset of U0

proof end;

end;

:: deftheorem defines Constants UNIALG_2:def 11 :
for U0 being Universal_Algebra holds Constants U0 = { a where a is Element of U0 : ex o being operation of U0 st
( arity o = 0 & a in rng o ) } ;

definition

let IT be Universal_Algebra;
attr IT is with_const_op means :Def12: :: UNIALG_2:def 12
ex o being operation of IT st arity o = 0 ;

end;

:: deftheorem Def12 defines with_const_op UNIALG_2:def 12 :
for IT being Universal_Algebra holds
( IT is with_const_op iff ex o being operation of IT st arity o = 0 );

registration

cluster non empty strict V76() quasi_total non-empty with_const_op UAStr ;
existence
ex b₁ being Universal_Algebra st
( b₁ is with_const_op & b₁ is strict )

proof end;

end;

registration

let U0 be with_const_op Universal_Algebra;
cluster Constants U0 -> non empty ;
coherence
not Constants U0 is empty

proof end;

end;

theorem Th18: :: UNIALG_2:18

for U0 being Universal_Algebra
for U1 being SubAlgebra of U0 holds Constants U0 is Subset of U1

proof end;

theorem :: UNIALG_2:19

for U0 being with_const_op Universal_Algebra
for U1 being SubAlgebra of U0 holds Constants U0 is non empty Subset of U1 by Th18;

theorem Th20: :: UNIALG_2:20

for U0 being with_const_op Universal_Algebra
for U1, U2 being SubAlgebra of U0 holds the carrier of U1 meets the carrier of U2

proof end;

definition

let U0 be Universal_Algebra;
let A be Subset of U0;
assume A1: ( Constants U0 <> {} or A <> {} ) ;
func GenUnivAlg A -> strict SubAlgebra of U0 means :Def13: :: UNIALG_2:def 13
( A c= the carrier of it & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
it is SubAlgebra of U1 ) );
existence
ex b₁ being strict SubAlgebra of U0 st
( A c= the carrier of b₁ & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
b₁ is SubAlgebra of U1 ) )

proof end;

uniqueness
for b₁, b₂ being strict SubAlgebra of U0 st A c= the carrier of b₁ & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
b₁ is SubAlgebra of U1 ) & A c= the carrier of b₂ & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
b₂ is SubAlgebra of U1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines GenUnivAlg UNIALG_2:def 13 :
for U0 being Universal_Algebra
for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds
for b₃ being strict SubAlgebra of U0 holds
( b₃ = GenUnivAlg A iff ( A c= the carrier of b₃ & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
b₃ is SubAlgebra of U1 ) ) );

theorem :: UNIALG_2:21

for U0 being strict Universal_Algebra holds GenUnivAlg ([#] the carrier of U0) = U0

proof end;

theorem Th22: :: UNIALG_2:22

for U0 being Universal_Algebra
for U1 being strict SubAlgebra of U0
for B being non empty Subset of U0 st B = the carrier of U1 holds
GenUnivAlg B = U1

proof end;

definition

let U0 be Universal_Algebra;
let U1, U2 be SubAlgebra of U0;
func U1 "\/" U2 -> strict SubAlgebra of U0 means :Def14: :: UNIALG_2:def 14
for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds
it = GenUnivAlg A;
existence
ex b₁ being strict SubAlgebra of U0 st
for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds
b₁ = GenUnivAlg A

proof end;

uniqueness
for b₁, b₂ being strict SubAlgebra of U0 st ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds
b₁ = GenUnivAlg A ) & ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds
b₂ = GenUnivAlg A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines "\/" UNIALG_2:def 14 :
for U0 being Universal_Algebra
for U1, U2 being SubAlgebra of U0
for b₄ being strict SubAlgebra of U0 holds
( b₄ = U1 "\/" U2 iff for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds
b₄ = GenUnivAlg A );

theorem Th23: :: UNIALG_2:23

for U0 being Universal_Algebra
for U1 being SubAlgebra of U0
for A, B being Subset of U0 st ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 holds
(GenUnivAlg A) "\/" U1 = GenUnivAlg B

proof end;

theorem Th24: :: UNIALG_2:24

for U0 being Universal_Algebra
for U1, U2 being SubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1

proof end;

theorem Th25: :: UNIALG_2:25

for U0 being with_const_op Universal_Algebra
for U1, U2 being strict SubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = U1

proof end;

theorem Th26: :: UNIALG_2:26

for U0 being with_const_op Universal_Algebra
for U1, U2 being strict SubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = U2

proof end;

definition

let U0 be Universal_Algebra;
func Sub U0 -> set means :Def15: :: UNIALG_2:def 15
for x being set holds
( x in it iff x is strict SubAlgebra of U0 );
existence
ex b₁ being set st
for x being set holds
( x in b₁ iff x is strict SubAlgebra of U0 )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is strict SubAlgebra of U0 ) ) & ( for x being set holds
( x in b₂ iff x is strict SubAlgebra of U0 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines Sub UNIALG_2:def 15 :
for U0 being Universal_Algebra
for b₂ being set holds
( b₂ = Sub U0 iff for x being set holds
( x in b₂ iff x is strict SubAlgebra of U0 ) );

registration

let U0 be Universal_Algebra;
cluster Sub U0 -> non empty ;
coherence
not Sub U0 is empty

proof end;

end;

definition

let U0 be Universal_Algebra;
func UniAlg_join U0 -> BinOp of (Sub U0) means :Def16: :: UNIALG_2:def 16
for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
it . (x,y) = U1 "\/" U2;
existence
ex b₁ being BinOp of (Sub U0) st
for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b₁ . (x,y) = U1 "\/" U2

proof end;

uniqueness
for b₁, b₂ being BinOp of (Sub U0) st ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b₁ . (x,y) = U1 "\/" U2 ) & ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b₂ . (x,y) = U1 "\/" U2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines UniAlg_join UNIALG_2:def 16 :
for U0 being Universal_Algebra
for b₂ being BinOp of (Sub U0) holds
( b₂ = UniAlg_join U0 iff for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b₂ . (x,y) = U1 "\/" U2 );

definition

let U0 be Universal_Algebra;
func UniAlg_meet U0 -> BinOp of (Sub U0) means :Def17: :: UNIALG_2:def 17
for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
it . (x,y) = U1 /\ U2;
existence
ex b₁ being BinOp of (Sub U0) st
for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b₁ . (x,y) = U1 /\ U2

proof end;

uniqueness
for b₁, b₂ being BinOp of (Sub U0) st ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b₁ . (x,y) = U1 /\ U2 ) & ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b₂ . (x,y) = U1 /\ U2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines UniAlg_meet UNIALG_2:def 17 :
for U0 being Universal_Algebra
for b₂ being BinOp of (Sub U0) holds
( b₂ = UniAlg_meet U0 iff for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b₂ . (x,y) = U1 /\ U2 );

theorem Th27: :: UNIALG_2:27

for U0 being Universal_Algebra holds UniAlg_join U0 is commutative

proof end;

theorem Th28: :: UNIALG_2:28

for U0 being Universal_Algebra holds UniAlg_join U0 is associative

proof end;

theorem Th29: :: UNIALG_2:29

for U0 being with_const_op Universal_Algebra holds UniAlg_meet U0 is commutative

proof end;

theorem Th30: :: UNIALG_2:30

for U0 being with_const_op Universal_Algebra holds UniAlg_meet U0 is associative

proof end;

definition

let U0 be with_const_op Universal_Algebra;
func UnSubAlLattice U0 -> strict Lattice equals :: UNIALG_2:def 18
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #);
coherence
LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is strict Lattice

proof end;

end;

:: deftheorem defines UnSubAlLattice UNIALG_2:def 18 :
for U0 being with_const_op Universal_Algebra holds UnSubAlLattice U0 = LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #);