:: ALG_1 semantic presentation

theorem Th1: :: ALG_1:1

for b₁, b₂ being non empty set
for b₃ being FinSequence of b₁
for b₄ being Function of b₁,b₂ holds
( dom (b₄ * b₃) = dom b₃ & len (b₄ * b₃) = len b₃ & ( for b₅ being Nat st b₅ in dom (b₄ * b₃) holds
(b₄ * b₃) . b₅ = b₄ . (b₃ . b₅) ) )

proof end;

theorem Th2: :: ALG_1:2

for b₁ being Universal_Algebra
for b₂ being non empty Subset of b₁ st b₂ = the carrier of b₁ holds
Opers b₁,b₂ = the charact of b₁

proof end;

theorem Th3: :: ALG_1:3

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ holds b₃ * (<*> the carrier of b₁) = <*> the carrier of b₂

proof end;

theorem Th4: :: ALG_1:4

for b₁ being Universal_Algebra
for b₂ being FinSequence of b₁ holds (id the carrier of b₁) * b₂ = b₂

proof end;

theorem Th5: :: ALG_1:5

for b₁, b₂, b₃ being Universal_Algebra
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃
for b₆ being FinSequence of b₁ holds b₅ * (b₄ * b₆) = (b₅ * b₄) * b₆

proof end;

definition

let c₁, c₂ be Universal_Algebra;
let c₃ be Function of c₁,c₂;
pred c₃ is_homomorphism c₁,c₂ means :Def1: :: ALG_1:def 1
( a₁,a₂ are_similar & ( for b₁ being Nat st b₁ in dom the charact of a₁ holds
for b₂ being operation of a₁
for b₃ being operation of a₂ st b₂ = the charact of a₁ . b₁ & b₃ = the charact of a₂ . b₁ holds
for b₄ being FinSequence of a₁ st b₄ in dom b₂ holds
a₃ . (b₂ . b₄) = b₃ . (a₃ * b₄) ) );

end;

:: deftheorem Def1 defines is_homomorphism ALG_1:def 1 :

definition

let c₁, c₂ be Universal_Algebra;
let c₃ be Function of c₁,c₂;
pred c₃ is_monomorphism c₁,c₂ means :Def2: :: ALG_1:def 2
( a₃ is_homomorphism a₁,a₂ & a₃ is one-to-one );
pred c₃ is_epimorphism c₁,c₂ means :Def3: :: ALG_1:def 3
( a₃ is_homomorphism a₁,a₂ & rng a₃ = the carrier of a₂ );

end;

:: deftheorem Def2 defines is_monomorphism ALG_1:def 2 :

:: deftheorem Def3 defines is_epimorphism ALG_1:def 3 :

definition

let c₁, c₂ be Universal_Algebra;
let c₃ be Function of c₁,c₂;
pred c₃ is_isomorphism c₁,c₂ means :Def4: :: ALG_1:def 4
( a₃ is_monomorphism a₁,a₂ & a₃ is_epimorphism a₁,a₂ );

end;

:: deftheorem Def4 defines is_isomorphism ALG_1:def 4 :

definition

let c₁, c₂ be Universal_Algebra;
pred c₁,c₂ are_isomorphic means :Def5: :: ALG_1:def 5
ex b₁ being Function of a₁,a₂ st b₁ is_isomorphism a₁,a₂;

end;

:: deftheorem Def5 defines are_isomorphic ALG_1:def 5 :

theorem Th6: :: ALG_1:6

for b₁ being Universal_Algebra holds id the carrier of b₁ is_homomorphism b₁,b₁

proof end;

theorem Th7: :: ALG_1:7

for b₁, b₂, b₃ being Universal_Algebra
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is_homomorphism b₁,b₂ & b₅ is_homomorphism b₂,b₃ holds
b₅ * b₄ is_homomorphism b₁,b₃

proof end;

theorem Th8: :: ALG_1:8

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ holds
( b₃ is_isomorphism b₁,b₂ iff ( b₃ is_homomorphism b₁,b₂ & rng b₃ = the carrier of b₂ & b₃ is one-to-one ) )

proof end;

theorem Th9: :: ALG_1:9

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₃ is_isomorphism b₁,b₂ holds
( dom b₃ = the carrier of b₁ & rng b₃ = the carrier of b₂ )

proof end;

theorem Th10: :: ALG_1:10

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₃ is_isomorphism b₁,b₂ & b₄ = b₃ " holds
b₄ is_homomorphism b₂,b₁

proof end;

theorem Th11: :: ALG_1:11

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₃ is_isomorphism b₁,b₂ & b₄ = b₃ " holds
b₄ is_isomorphism b₂,b₁

proof end;

theorem Th12: :: ALG_1:12

for b₁, b₂, b₃ being Universal_Algebra
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is_isomorphism b₁,b₂ & b₅ is_isomorphism b₂,b₃ holds
b₅ * b₄ is_isomorphism b₁,b₃

proof end;

theorem Th13: :: ALG_1:13

for b₁ being Universal_Algebra holds b₁,b₁ are_isomorphic

proof end;

theorem Th14: :: ALG_1:14

for b₁, b₂ being Universal_Algebra st b₁,b₂ are_isomorphic holds
b₂,b₁ are_isomorphic

proof end;

theorem Th15: :: ALG_1:15

for b₁, b₂, b₃ being Universal_Algebra st b₁,b₂ are_isomorphic & b₂,b₃ are_isomorphic holds
b₁,b₃ are_isomorphic

proof end;

definition

let c₁, c₂ be Universal_Algebra;
let c₃ be Function of c₁,c₂;
assume E17: c₃ is_homomorphism c₁,c₂ ;
func Image c₃ -> strict SubAlgebra of a₂ means :Def6: :: ALG_1:def 6
the carrier of a₄ = a₃ .: the carrier of a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Image ALG_1:def 6 :

theorem Th16: :: ALG_1:16

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₃ is_homomorphism b₁,b₂ holds
rng b₃ = the carrier of (Image b₃)

proof end;

theorem Th17: :: ALG_1:17

for b₁ being Universal_Algebra
for b₂ being strict Universal_Algebra
for b₃ being Function of b₁,b₂ st b₃ is_homomorphism b₁,b₂ holds
( b₃ is_epimorphism b₁,b₂ iff Image b₃ = b₂ )

proof end;

definition

let c₁ be 1-sorted ;
mode Relation of a₁ is Relation of the carrier of a₁;
mode Equivalence_Relation of a₁ is Equivalence_Relation of the carrier of a₁;

end;

definition

let c₁ be non empty set ;
let c₂ be Relation of c₁;
canceled;
canceled;
func ExtendRel c₂ -> Relation of a₁ * means :Def9: :: ALG_1:def 9
for b₁, b₂ being FinSequence of a₁ holds
( [b₁,b₂] in a₃ iff ( len b₁ = len b₂ & ( for b₃ being Nat st b₃ in dom b₁ holds
[(b₁ . b₃),(b₂ . b₃)] in a₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 ALG_1:def 7 :

:: deftheorem Def8 ALG_1:def 8 :

:: deftheorem Def9 defines ExtendRel ALG_1:def 9 :

theorem Th18: :: ALG_1:18

for b₁ being non empty set holds ExtendRel (id b₁) = id (b₁ * )

proof end;

definition

let c₁ be Universal_Algebra;
mode Congruence of c₁ -> Equivalence_Relation of a₁ means :Def10: :: ALG_1:def 10
for b₁ being Nat
for b₂ being operation of a₁ st b₁ in dom the charact of a₁ & b₂ = the charact of a₁ . b₁ holds
for b₃, b₄ being FinSequence of a₁ st b₃ in dom b₂ & b₄ in dom b₂ & [b₃,b₄] in ExtendRel a₂ holds
[(b₂ . b₃),(b₂ . b₄)] in a₂;
existence

proof end;

end;

:: deftheorem Def10 defines Congruence ALG_1:def 10 :

definition

let c₁ be non empty set ;
let c₂ be Equivalence_Relation of c₁;
let c₃ be FinSequence of Class c₂;
let c₄ be FinSequence of c₁;
pred c₄ is_representatives_FS c₃ means :Def11: :: ALG_1:def 11
( len a₄ = len a₃ & ( for b₁ being Nat st b₁ in dom a₄ holds
Class a₂,(a₄ . b₁) = a₃ . b₁ ) );

end;

:: deftheorem Def11 defines is_representatives_FS ALG_1:def 11 :

theorem Th19: :: ALG_1:19

for b₁ being non empty set
for b₂ being Equivalence_Relation of b₁
for b₃ being FinSequence of Class b₂ ex b₄ being FinSequence of b₁ st b₄ is_representatives_FS b₃

proof end;

definition

let c₁ be Universal_Algebra;
let c₂ be Congruence of c₁;
let c₃ be operation of c₁;
func QuotOp c₃,c₂ -> non empty homogeneous quasi_total PartFunc of (Class a₂) * , Class a₂ means :Def12: :: ALG_1:def 12
( dom a₄ = (arity a₃) -tuples_on (Class a₂) & ( for b₁ being FinSequence of Class a₂ st b₁ in dom a₄ holds
for b₂ being FinSequence of the carrier of a₁ st b₂ is_representatives_FS b₁ holds
a₄ . b₁ = Class a₂,(a₃ . b₂) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines QuotOp ALG_1:def 12 :

definition

let c₁ be Universal_Algebra;
let c₂ be Congruence of c₁;
func QuotOpSeq c₁,c₂ -> PFuncFinSequence of (Class a₂) means :Def13: :: ALG_1:def 13
( len a₃ = len the charact of a₁ & ( for b₁ being Nat st b₁ in dom a₃ holds
for b₂ being operation of a₁ st the charact of a₁ . b₁ = b₂ holds
a₃ . b₁ = QuotOp b₂,a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines QuotOpSeq ALG_1:def 13 :

theorem Th20: :: ALG_1:20

for b₁ being Universal_Algebra
for b₂ being Congruence of b₁ holds UAStr(# (Class b₂),(QuotOpSeq b₁,b₂) #) is strict Universal_Algebra

proof end;

definition

let c₁ be Universal_Algebra;
let c₂ be Congruence of c₁;
func QuotUnivAlg c₁,c₂ -> strict Universal_Algebra equals :: ALG_1:def 14
UAStr(# (Class a₂),(QuotOpSeq a₁,a₂) #);
coherence by Th20;

end;

:: deftheorem Def14 defines QuotUnivAlg ALG_1:def 14 :

definition

let c₁ be Universal_Algebra;
let c₂ be Congruence of c₁;
func Nat_Hom c₁,c₂ -> Function of a₁,(QuotUnivAlg a₁,a₂) means :Def15: :: ALG_1:def 15
for b₁ being Element of a₁ holds a₃ . b₁ = Class a₂,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines Nat_Hom ALG_1:def 15 :

theorem Th21: :: ALG_1:21

for b₁ being Universal_Algebra
for b₂ being Congruence of b₁ holds Nat_Hom b₁,b₂ is_homomorphism b₁, QuotUnivAlg b₁,b₂

proof end;

theorem Th22: :: ALG_1:22

for b₁ being Universal_Algebra
for b₂ being Congruence of b₁ holds Nat_Hom b₁,b₂ is_epimorphism b₁, QuotUnivAlg b₁,b₂

proof end;

definition

let c₁, c₂ be Universal_Algebra;
let c₃ be Function of c₁,c₂;
assume E28: c₃ is_homomorphism c₁,c₂ ;
func Cng c₃ -> Congruence of a₁ means :Def16: :: ALG_1:def 16
for b₁, b₂ being Element of a₁ holds
( [b₁,b₂] in a₄ iff a₃ . b₁ = a₃ . b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines Cng ALG_1:def 16 :

definition

let c₁, c₂ be Universal_Algebra;
let c₃ be Function of c₁,c₂;
assume E29: c₃ is_homomorphism c₁,c₂ ;
func HomQuot c₃ -> Function of (QuotUnivAlg a₁,(Cng a₃)),a₂ means :Def17: :: ALG_1:def 17
for b₁ being Element of a₁ holds a₄ . (Class (Cng a₃),b₁) = a₃ . b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines HomQuot ALG_1:def 17 :

theorem Th23: :: ALG_1:23

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₃ is_homomorphism b₁,b₂ holds
( HomQuot b₃ is_homomorphism QuotUnivAlg b₁,(Cng b₃),b₂ & HomQuot b₃ is_monomorphism QuotUnivAlg b₁,(Cng b₃),b₂ )

proof end;

theorem Th24: :: ALG_1:24

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₃ is_epimorphism b₁,b₂ holds
HomQuot b₃ is_isomorphism QuotUnivAlg b₁,(Cng b₃),b₂

proof end;

theorem Th25: :: ALG_1:25

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₃ is_epimorphism b₁,b₂ holds
QuotUnivAlg b₁,(Cng b₃),b₂ are_isomorphic

proof end;