:: Subalgebras of the Universal Algebra. Lattices of Subalgebras
:: by Ewa Burakowska
::
:: Copyright (c) 1993-2021 Association of Mizar Users

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
let U1, U2 be Universal_Algebra;
pred U1,U2 are_similar means :: UNIALG_2:def 1
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 defines are_similar UNIALG_2:def 1 :
for U1, U2 being Universal_Algebra holds
( U1,U2 are_similar iff signature U1 = signature U2 );

theorem :: UNIALG_2:1
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:2
for U1, U2, U3 being Universal_Algebra st U1,U2 are_similar & U2,U3 are_similar holds
U1,U3 are_similar ;

theorem :: UNIALG_2:3
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 ;

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

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

definition 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 :: UNIALG_2:def 3
for s being FinSequence of A st len s = arity o holds
o . s in A;
end;

:: deftheorem defines is_closed_on UNIALG_2:def 3 :
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 :: UNIALG_2:def 4
for o being operation of U0 holds A is_closed_on o;
end;

:: deftheorem defines opers_closed UNIALG_2:def 4 :
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 :Def5: :: UNIALG_2:def 5
o | (() -tuples_on A);
coherence
o | (() -tuples_on A) is non empty homogeneous quasi_total PartFunc of (A *),A
proof end;
end;

:: deftheorem Def5 defines /. UNIALG_2:def 5 :
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 | (() -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 :Def6: :: UNIALG_2:def 6
( 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 b1 being PFuncFinSequence of A st
( dom b1 = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom b1 & o = the charact of U0 . n holds
b1 . n = o /. A ) )
proof end;
uniqueness
for b1, b2 being PFuncFinSequence of A st dom b1 = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom b1 & o = the charact of U0 . n holds
b1 . n = o /. A ) & dom b2 = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom b2 & o = the charact of U0 . n holds
b2 . n = o /. A ) holds
b1 = b2
proof end;
end;

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

theorem Th4: :: UNIALG_2:4
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:5
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 :Def7: :: UNIALG_2:def 7
( 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 b1 being Universal_Algebra st
( the carrier of b1 is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of b1 holds
( the charact of b1 = Opers (U0,B) & B is opers_closed ) ) )
proof end;
end;

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

registration
let U0 be Universal_Algebra;
cluster non empty strict V87() quasi_total non-empty for SubAlgebra of U0;
existence
ex b1 being SubAlgebra of U0 st b1 is strict
proof end;
end;

theorem Th6: :: UNIALG_2:6
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 Th7: :: UNIALG_2:7
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:8
for U0 being Universal_Algebra holds U0 is SubAlgebra of U0
proof end;

theorem :: UNIALG_2:9
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 Th10: :: UNIALG_2:10
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 Th11: :: UNIALG_2:11
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 Th12: :: UNIALG_2:12
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:13
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
U1,U2 are_similar
proof end;

theorem Th14: :: UNIALG_2:14
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 :Def8: :: UNIALG_2:def 8
UAStr(# A,(Opers (U0,A)) #);
coherence
UAStr(# A,(Opers (U0,A)) #) is strict SubAlgebra of U0
proof end;
end;

:: deftheorem Def8 defines UniAlgSetClosed UNIALG_2:def 8 :
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 :Def9: :: UNIALG_2:def 9
( 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 b1 being strict SubAlgebra of U0 st
( the carrier of b1 = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b1 holds
( the charact of b1 = Opers (U0,B) & B is opers_closed ) ) )
proof end;
uniqueness
for b1, b2 being strict SubAlgebra of U0 st the carrier of b1 = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b1 holds
( the charact of b1 = Opers (U0,B) & B is opers_closed ) ) & the carrier of b2 = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b2 holds
( the charact of b2 = Opers (U0,B) & B is opers_closed ) ) holds
b1 = b2
proof end;
end;

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

definition
let U0 be Universal_Algebra;
func Constants U0 -> Subset of U0 equals :: UNIALG_2:def 10
{ 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 10 :
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 :Def11: :: UNIALG_2:def 11
ex o being operation of IT st arity o = 0 ;
end;

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

registration
existence
ex b1 being Universal_Algebra st
( b1 is with_const_op & b1 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 Th15: :: UNIALG_2:15
for U0 being Universal_Algebra
for U1 being SubAlgebra of U0 holds Constants U0 is Subset of U1
proof end;

theorem :: UNIALG_2:16
for U0 being with_const_op Universal_Algebra
for U1 being SubAlgebra of U0 holds Constants U0 is non empty Subset of U1 by Th15;

theorem Th17: :: UNIALG_2:17
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 :Def12: :: UNIALG_2:def 12
( 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 b1 being strict SubAlgebra of U0 st
( A c= the carrier of b1 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
b1 is SubAlgebra of U1 ) )
proof end;
uniqueness
for b1, b2 being strict SubAlgebra of U0 st A c= the carrier of b1 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
b1 is SubAlgebra of U1 ) & A c= the carrier of b2 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
b2 is SubAlgebra of U1 ) holds
b1 = b2
proof end;
end;

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

theorem :: UNIALG_2:18
for U0 being strict Universal_Algebra holds GenUnivAlg ([#] the carrier of U0) = U0
proof end;

theorem Th19: :: UNIALG_2:19
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 :Def13: :: UNIALG_2:def 13
for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds
it = GenUnivAlg A;
existence
ex b1 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
b1 = GenUnivAlg A
proof end;
uniqueness
for b1, b2 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
b1 = GenUnivAlg A ) & ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds
b2 = GenUnivAlg A ) holds
b1 = b2
proof end;
end;

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

theorem Th20: :: UNIALG_2:20
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
() "\/" U1 = GenUnivAlg B
proof end;

theorem Th21: :: UNIALG_2:21
for U0 being Universal_Algebra
for U1, U2 being SubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1
proof end;

theorem Th22: :: UNIALG_2:22
for U0 being with_const_op Universal_Algebra
for U1, U2 being strict SubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = U1
proof end;

theorem Th23: :: UNIALG_2:23
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 :Def14: :: UNIALG_2:def 14
for x being object holds
( x in it iff x is strict SubAlgebra of U0 );
existence
ex b1 being set st
for x being object holds
( x in b1 iff x is strict SubAlgebra of U0 )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff x is strict SubAlgebra of U0 ) ) & ( for x being object holds
( x in b2 iff x is strict SubAlgebra of U0 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines Sub UNIALG_2:def 14 :
for U0 being Universal_Algebra
for b2 being set holds
( b2 = Sub U0 iff for x being object holds
( x in b2 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 :Def15: :: UNIALG_2:def 15
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 b1 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
b1 . (x,y) = U1 "\/" U2
proof end;
uniqueness
for b1, b2 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
b1 . (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
b2 . (x,y) = U1 "\/" U2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines UniAlg_join UNIALG_2:def 15 :
for U0 being Universal_Algebra
for b2 being BinOp of (Sub U0) holds
( b2 = 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
b2 . (x,y) = U1 "\/" U2 );

definition
let U0 be Universal_Algebra;
func UniAlg_meet 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 b1 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
b1 . (x,y) = U1 /\ U2
proof end;
uniqueness
for b1, b2 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
b1 . (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
b2 . (x,y) = U1 /\ U2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines UniAlg_meet UNIALG_2:def 16 :
for U0 being Universal_Algebra
for b2 being BinOp of (Sub U0) holds
( b2 = 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
b2 . (x,y) = U1 /\ U2 );

theorem Th24: :: UNIALG_2:24
for U0 being Universal_Algebra holds UniAlg_join U0 is commutative
proof end;

theorem Th25: :: UNIALG_2:25
for U0 being Universal_Algebra holds UniAlg_join U0 is associative
proof end;

theorem Th26: :: UNIALG_2:26
for U0 being with_const_op Universal_Algebra holds UniAlg_meet U0 is commutative
proof end;

theorem Th27: :: UNIALG_2:27
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 17
LattStr(# (Sub U0),(),() #);
coherence
LattStr(# (Sub U0),(),() #) is strict Lattice
proof end;
end;

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