:: Subalgebras of the Universal Algebra. Lattices of Subalgebras
:: by Ewa Burakowska
::
:: Received July 8, 1993
:: Copyright (c) 1993-2012 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
let U1, U2 be Universal_Algebra;
predU1,U2 are_similar  means :Def1: :: 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 Def1 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
proofend;

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
proofend;

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 FINSEQ_1:def_4, RELAT_1:41;

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
proofend;
end;

:: deftheorem  defines Operations UNIALG_2:def_2_:_
 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;
predA is_closed_on o means :Def3: :: UNIALG_2:def 3
 for s being FinSequence of A st len s = arity o holds
o . s in A;
end;

:: deftheorem Def3 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;
attrA is opers_closed  means :Def4: :: UNIALG_2:def 4
 for o being operation of U0 holds A is_closed_on o;
end;

:: deftheorem Def4 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 ;
funco /. A ->  non empty homogeneous quasi_total PartFunc of (A *),A equals :Def5: :: UNIALG_2:def 5
o | ((arity o) -tuples_on A);
coherence
 o | ((arity o) -tuples_on A) is non empty homogeneous quasi_total PartFunc of (A *),A
proofend;
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 | ((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 :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 ) )
proofend;
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
proofend;
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 ) )
proofend;

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
proofend;

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 ) ) )
proofend;
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 V84() quasi_total non-empty for SubAlgebra of U0;
existence
 ex b1 being SubAlgebra of U0 st b1 is strict
proofend;
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
proofend;

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
proofend;

theorem :: UNIALG_2:8
for U0 being Universal_Algebra holds U0 is SubAlgebra of U0
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

theorem :: UNIALG_2:13
for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
U1,U2 are_similar
proofend;

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
proofend;

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
proofend;
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 ;
funcU1 /\ 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 ) ) )
proofend;
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
proofend;
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
proofend;
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;
attrIT 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
cluster non empty strict V84() quasi_total non-empty with_const_op for UAStr ;
existence
 ex b1 being Universal_Algebra st
( b1 is with_const_op & b1 is strict )
proofend;
end;

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

theorem Th15: :: UNIALG_2:15
for U0 being Universal_Algebra
for U1 being SubAlgebra of U0 holds Constants U0 is Subset of U1
proofend;

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
proofend;

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 &amp; ( 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 &amp; ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
b1 is SubAlgebra of U1 ) )
proofend;
uniqueness
 for b1, b2 being strict SubAlgebra of U0 st A c= the carrier of b1 &amp; ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
b1 is SubAlgebra of U1 ) &amp; A c= the carrier of b2 &amp; ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
b2 is SubAlgebra of U1 ) holds
b1 = b2
proofend;
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 &amp; ( 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
proofend;

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
proofend;

definition
let U0 be Universal_Algebra;
let U1, U2 be SubAlgebra of U0;
funcU1 "\/" 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
proofend;
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 ) &amp; ( 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
proofend;
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 <> {} ) &amp; B = A \/ the carrier of U1 holds
(GenUnivAlg A) "\/" U1 = GenUnivAlg B
proofend;

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

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
proofend;

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
proofend;

definition
let U0 be Universal_Algebra;
func Sub U0 ->  set  means :Def14: :: UNIALG_2:def 14
 for x being set holds
( x in it iff x is strict SubAlgebra of U0 );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is strict SubAlgebra of U0 )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict SubAlgebra of U0 ) ) &amp; ( for x being set holds
( x in b2 iff x is strict SubAlgebra of U0 ) ) holds
b1 = b2
proofend;
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 set 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
proofend;
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 &amp; 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 &amp; y = U2 holds
b1 . (x,y) = U1 "\/" U2
proofend;
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 &amp; y = U2 holds
b1 . (x,y) = U1 "\/" U2 ) &amp; ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 &amp; y = U2 holds
b2 . (x,y) = U1 "\/" U2 ) holds
b1 = b2
proofend;
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 &amp; 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 &amp; 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 &amp; y = U2 holds
b1 . (x,y) = U1 /\ U2
proofend;
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 &amp; y = U2 holds
b1 . (x,y) = U1 /\ U2 ) &amp; ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 &amp; y = U2 holds
b2 . (x,y) = U1 /\ U2 ) holds
b1 = b2
proofend;
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 &amp; y = U2 holds
b2 . (x,y) = U1 /\ U2 );

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

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

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

theorem Th27: :: UNIALG_2:27
for U0 being with_const_op Universal_Algebra holds UniAlg_meet U0 is associative
proofend;

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

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