:: UNIALG_3 semantic presentation

definition

let c₁ be Universal_Algebra;
mode SubAlgebra-Family of c₁ -> set means :Def1: :: UNIALG_3:def 1
for b₁ being set st b₁ in a₂ holds
b₁ is SubAlgebra of a₁;
existence

proof end;

end;

:: deftheorem Def1 defines SubAlgebra-Family UNIALG_3:def 1 :

registration

let c₁ be Universal_Algebra;
cluster non empty SubAlgebra-Family of a₁;
existence

proof end;

end;

definition

let c₁ be Universal_Algebra;
redefine func Sub as Sub c₁ -> non empty SubAlgebra-Family of a₁;
coherence

proof end;

let c₂ be non empty SubAlgebra-Family of c₁;
redefine mode Element as Element of c₂ -> SubAlgebra of a₁;
coherence by Def1;

end;

definition

let c₁ be Universal_Algebra;
redefine func UniAlg_join as UniAlg_join c₁ -> BinOp of Sub a₁;
coherence ;
redefine func UniAlg_meet as UniAlg_meet c₁ -> BinOp of Sub a₁;
coherence ;

end;

definition

let c₁ be Universal_Algebra;
let c₂ be Element of Sub c₁;
func carr c₂ -> Subset of a₁ means :Def2: :: UNIALG_3:def 2
ex b₁ being SubAlgebra of a₁ st
( a₂ = b₁ & a₃ = the carrier of b₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines carr UNIALG_3:def 2 :

definition

let c₁ be Universal_Algebra;
func Carr c₁ -> Function of Sub a₁, bool the carrier of a₁ means :Def3: :: UNIALG_3:def 3
for b₁ being Element of Sub a₁ holds a₂ . b₁ = carr b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Carr UNIALG_3:def 3 :

theorem Th1: :: UNIALG_3:1

for b₁ being Universal_Algebra
for b₂ being set holds
( b₂ in Sub b₁ iff ex b₃ being strict SubAlgebra of b₁ st b₂ = b₃ )

proof end;

theorem Th2: :: UNIALG_3:2

for b₁ being Universal_Algebra
for b₂ being non empty Subset of b₁
for b₃ being operation of b₁ st arity b₃ = 0 holds
( b₂ is_closed_on b₃ iff b₃ . {} in b₂ )

proof end;

theorem Th3: :: UNIALG_3:3

for b₁ being Universal_Algebra
for b₂ being SubAlgebra of b₁ holds the carrier of b₂ c= the carrier of b₁

proof end;

theorem Th4: :: UNIALG_3:4

for b₁ being Universal_Algebra
for b₂ being non empty Subset of b₁
for b₃ being operation of b₁ st b₂ is_closed_on b₃ & arity b₃ = 0 holds
b₃ /. b₂ = b₃

proof end;

theorem Th5: :: UNIALG_3:5

for b₁ being Universal_Algebra holds Constants b₁ = { (b₂ . {} ) where B is operation of b₁ : arity b₂ = 0 }

proof end;

theorem Th6: :: UNIALG_3:6

for b₁ being with_const_op Universal_Algebra
for b₂ being SubAlgebra of b₁ holds Constants b₁ = Constants b₂

proof end;

registration

let c₁ be with_const_op Universal_Algebra;
cluster -> with_const_op SubAlgebra of a₁;
coherence

proof end;

end;

theorem Th7: :: UNIALG_3:7

for b₁ being with_const_op Universal_Algebra
for b₂, b₃ being SubAlgebra of b₁ holds Constants b₂ = Constants b₃

proof end;

definition

let c₁ be Universal_Algebra;
redefine func Carr as Carr c₁ -> Function of Sub a₁, bool the carrier of a₁ means :Def4: :: UNIALG_3:def 4
for b₁ being Element of Sub a₁
for b₂ being SubAlgebra of a₁ st b₁ = b₂ holds
a₂ . b₁ = the carrier of b₂;
coherence ;
compatibility

proof end;

end;

:: deftheorem Def4 defines Carr UNIALG_3:def 4 :

theorem Th8: :: UNIALG_3:8

for b₁ being Universal_Algebra
for b₂ being strict SubAlgebra of b₁
for b₃ being Element of b₁ holds
( b₃ in (Carr b₁) . b₂ iff b₃ in b₂ )

proof end;

theorem Th9: :: UNIALG_3:9

for b₁ being Universal_Algebra
for b₂ being non empty Subset of (Sub b₁) holds not (Carr b₁) .: b₂ is empty

proof end;

theorem Th10: :: UNIALG_3:10

for b₁ being with_const_op Universal_Algebra
for b₂ being strict SubAlgebra of b₁ holds Constants b₁ c= (Carr b₁) . b₂

proof end;

theorem Th11: :: UNIALG_3:11

for b₁ being with_const_op Universal_Algebra
for b₂ being SubAlgebra of b₁
for b₃ being set st b₃ is Element of Constants b₁ holds
b₃ in the carrier of b₂

proof end;

theorem Th12: :: UNIALG_3:12

for b₁ being with_const_op Universal_Algebra
for b₂ being non empty Subset of (Sub b₁) holds meet ((Carr b₁) .: b₂) is non empty Subset of b₁

proof end;

theorem Th13: :: UNIALG_3:13

for b₁ being with_const_op Universal_Algebra holds the carrier of (UnSubAlLattice b₁) = Sub b₁ ;

theorem Th14: :: UNIALG_3:14

for b₁ being with_const_op Universal_Algebra
for b₂ being non empty Subset of (Sub b₁)
for b₃ being non empty Subset of b₁ st b₃ = meet ((Carr b₁) .: b₂) holds
b₃ is opers_closed

proof end;

definition

let c₁ be strict with_const_op Universal_Algebra;
let c₂ be non empty Subset of (Sub c₁);
func meet c₂ -> strict SubAlgebra of a₁ means :Def5: :: UNIALG_3:def 5
the carrier of a₃ = meet ((Carr a₁) .: a₂);
existence

proof end;

uniqueness by UNIALG_2:15;

end;

:: deftheorem Def5 defines meet UNIALG_3:def 5 :

theorem Th15: :: UNIALG_3:15

for b₁ being with_const_op Universal_Algebra
for b₂, b₃ being Element of (UnSubAlLattice b₁)
for b₄, b₅ being strict SubAlgebra of b₁ st b₂ = b₄ & b₃ = b₅ holds
b₂ "\/" b₃ = b₄ "\/" b₅ by UNIALG_2:def 16;

theorem Th16: :: UNIALG_3:16

for b₁ being with_const_op Universal_Algebra
for b₂, b₃ being Element of (UnSubAlLattice b₁)
for b₄, b₅ being strict SubAlgebra of b₁ st b₂ = b₄ & b₃ = b₅ holds
b₂ "/\" b₃ = b₄ /\ b₅ by UNIALG_2:def 17;

theorem Th17: :: UNIALG_3:17

for b₁ being with_const_op Universal_Algebra
for b₂, b₃ being Element of (UnSubAlLattice b₁)
for b₄, b₅ being strict SubAlgebra of b₁ st b₂ = b₄ & b₃ = b₅ holds
( b₂ [= b₃ iff the carrier of b₄ c= the carrier of b₅ )

proof end;

theorem Th18: :: UNIALG_3:18

for b₁ being with_const_op Universal_Algebra
for b₂, b₃ being Element of (UnSubAlLattice b₁)
for b₄, b₅ being strict SubAlgebra of b₁ st b₂ = b₄ & b₃ = b₅ holds
( b₂ [= b₃ iff b₄ is SubAlgebra of b₅ )

proof end;

theorem Th19: :: UNIALG_3:19

for b₁ being strict with_const_op Universal_Algebra holds UnSubAlLattice b₁ is bounded

proof end;

registration

let c₁ be strict with_const_op Universal_Algebra;
cluster UnSubAlLattice a₁ -> bounded ;
coherence by Th19;

end;

theorem Th20: :: UNIALG_3:20

for b₁ being strict with_const_op Universal_Algebra
for b₂ being strict SubAlgebra of b₁ holds (GenUnivAlg (Constants b₁)) /\ b₂ = GenUnivAlg (Constants b₁)

proof end;

theorem Th21: :: UNIALG_3:21

for b₁ being strict with_const_op Universal_Algebra holds Bottom (UnSubAlLattice b₁) = GenUnivAlg (Constants b₁)

proof end;

theorem Th22: :: UNIALG_3:22

for b₁ being strict with_const_op Universal_Algebra
for b₂ being SubAlgebra of b₁
for b₃ being Subset of b₁ st b₃ = the carrier of b₁ holds
(GenUnivAlg b₃) "\/" b₂ = GenUnivAlg b₃

proof end;

theorem Th23: :: UNIALG_3:23

for b₁ being strict with_const_op Universal_Algebra
for b₂ being Subset of b₁ st b₂ = the carrier of b₁ holds
Top (UnSubAlLattice b₁) = GenUnivAlg b₂

proof end;

theorem Th24: :: UNIALG_3:24

for b₁ being strict with_const_op Universal_Algebra holds Top (UnSubAlLattice b₁) = b₁

proof end;

theorem Th25: :: UNIALG_3:25

for b₁ being strict with_const_op Universal_Algebra holds UnSubAlLattice b₁ is complete

proof end;

definition

let c₁, c₂ be with_const_op Universal_Algebra;
let c₃ be Function of the carrier of c₁,the carrier of c₂;
func FuncLatt c₃ -> Function of the carrier of (UnSubAlLattice a₁),the carrier of (UnSubAlLattice a₂) means :Def6: :: UNIALG_3:def 6
for b₁ being strict SubAlgebra of a₁
for b₂ being Subset of a₂ st b₂ = a₃ .: the carrier of b₁ holds
a₄ . b₁ = GenUnivAlg b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines FuncLatt UNIALG_3:def 6 :

theorem Th26: :: UNIALG_3:26

for b₁ being strict with_const_op Universal_Algebra
for b₂ being Function of the carrier of b₁,the carrier of b₁ st b₂ = id the carrier of b₁ holds
FuncLatt b₂ = id the carrier of (UnSubAlLattice b₁)

proof end;