UNIALG_2: Subalgebras of the Universal Algebra. Lattices of Subalgebras

:: Subalgebras of the Universal Algebra. Lattices of Subalgebras
:: by Ewa Burakowska
::
:: Received July 8, 1993
:: 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 ;
reflexivity ;

end;

:: deftheorem defines are_similar UNIALG_2:def 1 :

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

proof end;

end;

:: deftheorem defines Operations UNIALG_2:def 2 :

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

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 :

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 | ((arity o) -tuples_on A);

proof end;

end;

:: deftheorem Def5 defines /. UNIALG_2:def 5 :

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

proof end;

proof end;

end;

:: deftheorem Def6 defines Opers UNIALG_2:def 6 :

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

proof end;

end;

:: deftheorem Def7 defines SubAlgebra UNIALG_2:def 7 :

registration

let U0 be Universal_Algebra;

cluster non empty strict V87() quasi_total non-empty for SubAlgebra of U0;

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

proof end;

end;

:: deftheorem Def8 defines UniAlgSetClosed UNIALG_2:def 8 :

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

proof end;

proof end;

end;

:: deftheorem Def9 defines /\ UNIALG_2:def 9 :

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

proof end;

end;

:: deftheorem defines Constants UNIALG_2:def 10 :

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 :

registration

cluster non empty strict V87() quasi_total non-empty with_const_op for UAStr ;

proof end;

end;

registration

let U0 be with_const_op Universal_Algebra;

cluster Constants U0 -> non 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 ) );

proof end;

proof end;

end;

:: deftheorem Def12 defines GenUnivAlg UNIALG_2:def 12 :

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;

proof end;

proof end;

end;

:: deftheorem Def13 defines "\/" UNIALG_2:def 13 :

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
(GenUnivAlg A) "\/" 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 );

proof end;

proof end;

end;

:: deftheorem Def14 defines Sub UNIALG_2:def 14 :

registration

let U0 be Universal_Algebra;

cluster Sub U0 -> non 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;

proof end;

proof end;

end;

:: deftheorem Def15 defines UniAlg_join UNIALG_2:def 15 :

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;

proof end;

proof end;

end;

:: deftheorem Def16 defines UniAlg_meet UNIALG_2:def 16 :

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),(UniAlg_join U0),(UniAlg_meet U0) #);

proof end;

end;

:: deftheorem defines UnSubAlLattice UNIALG_2:def 17 :