:: ENDALG semantic presentation

definition

let c₁ be Universal_Algebra;
func UAEnd c₁ -> FUNCTION_DOMAIN of the carrier of a₁,the carrier of a₁ means :Def1: :: ENDALG:def 1
for b₁ being Function of a₁,a₁ holds
( b₁ in a₂ iff b₁ is_homomorphism a₁,a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines UAEnd ENDALG:def 1 :

theorem Th1: :: ENDALG:1

for b₁ being Universal_Algebra holds UAEnd b₁ c= Funcs the carrier of b₁,the carrier of b₁

proof end;

theorem Th2: :: ENDALG:2

canceled;

theorem Th3: :: ENDALG:3

for b₁ being Universal_Algebra holds id the carrier of b₁ in UAEnd b₁

proof end;

theorem Th4: :: ENDALG:4

for b₁ being Universal_Algebra
for b₂, b₃ being Element of UAEnd b₁ holds b₂ * b₃ in UAEnd b₁

proof end;

definition

let c₁ be Universal_Algebra;
func UAEndComp c₁ -> BinOp of UAEnd a₁ means :Def2: :: ENDALG:def 2
for b₁, b₂ being Element of UAEnd a₁ holds a₂ . b₁,b₂ = b₂ * b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines UAEndComp ENDALG:def 2 :

definition

let c₁ be Universal_Algebra;
func UAEndMonoid c₁ -> strict multLoopStr means :Def3: :: ENDALG:def 3
( the carrier of a₂ = UAEnd a₁ & the mult of a₂ = UAEndComp a₁ & the unity of a₂ = id the carrier of a₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines UAEndMonoid ENDALG:def 3 :

registration

let c₁ be Universal_Algebra;
cluster UAEndMonoid a₁ -> non empty strict ;
coherence

proof end;

end;

E6: now

let c₁ be Universal_Algebra;
set c₂ = UAEndMonoid c₁;
let c₃, c₄ be Element of (UAEndMonoid c₁);
assume E7: c₄ = id the carrier of c₁ ;
reconsider c₅ = c₄, c₆ = c₃ as Element of UAEnd c₁ by Def3;
thus c₃ * c₄ = the mult of (UAEndMonoid c₁) . c₃,c₄
.= (UAEndComp c₁) . c₆,c₅ by Def3
.= c₅ * c₆ by Def2
.= c₃ by E7, FUNCT_2:74 ;
thus c₄ * c₃ = the mult of (UAEndMonoid c₁) . c₄,c₃
.= (UAEndComp c₁) . c₅,c₆ by Def3
.= c₆ * c₅ by Def2
.= c₃ by E7, FUNCT_2:74 ;

end;

registration

let c₁ be Universal_Algebra;
cluster UAEndMonoid a₁ -> non empty unital associative strict ;
coherence

proof end;

end;

theorem Th5: :: ENDALG:5

for b₁ being Universal_Algebra
for b₂, b₃ being Element of (UAEndMonoid b₁)
for b₄, b₅ being Element of UAEnd b₁ st b₂ = b₄ & b₃ = b₅ holds
b₂ * b₃ = b₅ * b₄

proof end;

theorem Th6: :: ENDALG:6

for b₁ being Universal_Algebra holds id the carrier of b₁ = 1. (UAEndMonoid b₁)

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func MSAEnd c₂ -> MSFunctionSet of the Sorts of a₂,the Sorts of a₂ means :Def4: :: ENDALG:def 4
( ( for b₁ being Element of a₃ holds b₁ is ManySortedFunction of a₂,a₂ ) & ( for b₁ being ManySortedFunction of a₂,a₂ holds
( b₁ in a₃ iff b₁ is_homomorphism a₂,a₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines MSAEnd ENDALG:def 4 :

theorem Th7: :: ENDALG:7

canceled;

theorem Th8: :: ENDALG:8

canceled;

theorem Th9: :: ENDALG:9

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds MSAEnd b₂ c= product (MSFuncs the Sorts of b₂,the Sorts of b₂)

proof end;

theorem Th10: :: ENDALG:10

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds id the Sorts of b₂ in MSAEnd b₂

proof end;

theorem Th11: :: ENDALG:11

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being Element of MSAEnd b₂ holds b₃ ** b₄ in MSAEnd b₂

proof end;

theorem Th12: :: ENDALG:12

for b₁ being Universal_Algebra
for b₂ being ManySortedFunction of (MSAlg b₁),(MSAlg b₁)
for b₃ being Element of UAEnd b₁ st b₂ = {0} --> b₃ holds
b₂ in MSAEnd (MSAlg b₁)

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func MSAEndComp c₂ -> BinOp of MSAEnd a₂ means :Def5: :: ENDALG:def 5
for b₁, b₂ being Element of MSAEnd a₂ holds a₃ . b₁,b₂ = b₂ ** b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines MSAEndComp ENDALG:def 5 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func MSAEndMonoid c₂ -> strict multLoopStr means :Def6: :: ENDALG:def 6
( the carrier of a₃ = MSAEnd a₂ & the mult of a₃ = MSAEndComp a₂ & the unity of a₃ = id the Sorts of a₂ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines MSAEndMonoid ENDALG:def 6 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster MSAEndMonoid a₂ -> non empty strict ;
coherence

proof end;

end;

E15: now

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
set c₃ = MSAEndMonoid c₂;
let c₄, c₅ be Element of (MSAEndMonoid c₂);
assume E16: c₅ = id the Sorts of c₂ ;
reconsider c₆ = c₅, c₇ = c₄ as Element of MSAEnd c₂ by Def6;
thus c₄ * c₅ = the mult of (MSAEndMonoid c₂) . c₄,c₅
.= (MSAEndComp c₂) . c₇,c₆ by Def6
.= c₆ ** c₇ by Def5
.= c₄ by E16, MSUALG_3:4 ;
thus c₅ * c₄ = the mult of (MSAEndMonoid c₂) . c₅,c₄
.= (MSAEndComp c₂) . c₆,c₇ by Def6
.= c₇ ** c₆ by Def5
.= c₄ by E16, MSUALG_3:3 ;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster MSAEndMonoid a₂ -> non empty unital associative strict ;
coherence

proof end;

end;

theorem Th13: :: ENDALG:13

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being Element of (MSAEndMonoid b₂)
for b₅, b₆ being Element of MSAEnd b₂ st b₃ = b₅ & b₄ = b₆ holds
b₃ * b₄ = b₆ ** b₅

proof end;

theorem Th14: :: ENDALG:14

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds id the Sorts of b₂ = 1. (MSAEndMonoid b₂)

proof end;

theorem Th15: :: ENDALG:15

canceled;

theorem Th16: :: ENDALG:16

for b₁ being Universal_Algebra
for b₂ being Element of UAEnd b₁ holds {0} --> b₂ is ManySortedFunction of (MSAlg b₁),(MSAlg b₁)

proof end;

Lemma19: for b₁ being Universal_Algebra
for b₂ being Function st dom b₂ = UAEnd b₁ & ( for b₃ being set st b₃ in UAEnd b₁ holds
b₂ . b₃ = {0} --> b₃ ) holds
rng b₂ = MSAEnd (MSAlg b₁)

proof end;

definition

let c₁, c₂ be non empty multLoopStr ;
let c₃ be Function of c₁,c₂;
canceled;
attr a₃ is unity-preserving means :Def8: :: ENDALG:def 8
a₃ . (1. a₁) = 1. a₂;

end;

:: deftheorem Def7 ENDALG:def 7 :

:: deftheorem Def8 defines unity-preserving ENDALG:def 8 :

registration

cluster non empty left_unital multLoopStr ;
existence

proof end;

end;

registration

let c₁, c₂ be non empty left_unital multLoopStr ;
cluster multiplicative unity-preserving M4(the carrier of a₁,the carrier of a₂);
existence

proof end;

end;

definition

let c₁, c₂ be non empty left_unital multLoopStr ;
mode Homomorphism of a₁,a₂ is multiplicative unity-preserving Function of a₁,a₂;

end;

definition

let c₁, c₂ be non empty left_unital multLoopStr ;
let c₃ be Function of c₁,c₂;
pred c₃ is_monomorphism means :Def9: :: ENDALG:def 9
a₃ is one-to-one;
pred c₃ is_epimorphism means :Def10: :: ENDALG:def 10
rng a₃ = the carrier of a₂;

end;

:: deftheorem Def9 defines is_monomorphism ENDALG:def 9 :

:: deftheorem Def10 defines is_epimorphism ENDALG:def 10 :

definition

let c₁, c₂ be non empty left_unital multLoopStr ;
let c₃ be Function of c₁,c₂;
pred c₃ is_isomorphism means :Def11: :: ENDALG:def 11
( a₃ is_epimorphism & a₃ is_monomorphism );

end;

:: deftheorem Def11 defines is_isomorphism ENDALG:def 11 :

theorem Th17: :: ENDALG:17

for b₁ being non empty left_unital multLoopStr holds id the carrier of b₁ is Homomorphism of b₁,b₁

proof end;

definition

let c₁, c₂ be non empty left_unital multLoopStr ;
pred c₁,c₂ are_isomorphic means :Def12: :: ENDALG:def 12
ex b₁ being Homomorphism of a₁,a₂ st b₁ is_isomorphism ;
reflexivity

proof end;

end;

:: deftheorem Def12 defines are_isomorphic ENDALG:def 12 :

theorem Th18: :: ENDALG:18

for b₁ being Universal_Algebra
for b₂ being Function st dom b₂ = UAEnd b₁ & ( for b₃ being set st b₃ in UAEnd b₁ holds
b₂ . b₃ = {0} --> b₃ ) holds
b₂ is Homomorphism of (UAEndMonoid b₁),(MSAEndMonoid (MSAlg b₁))

proof end;

theorem Th19: :: ENDALG:19

for b₁ being Universal_Algebra
for b₂ being Homomorphism of (UAEndMonoid b₁),(MSAEndMonoid (MSAlg b₁)) st ( for b₃ being set st b₃ in UAEnd b₁ holds
b₂ . b₃ = {0} --> b₃ ) holds
b₂ is_isomorphism

proof end;

theorem Th20: :: ENDALG:20

for b₁ being Universal_Algebra holds UAEndMonoid b₁, MSAEndMonoid (MSAlg b₁) are_isomorphic

proof end;