:: ENDALG semantic presentation

definition

let UA be Universal_Algebra;
func UAEnd UA -> FUNCTION_DOMAIN of the carrier of UA,the carrier of UA means :Def1: :: ENDALG:def 1
for h being Function of UA,UA holds
( h in it iff h is_homomorphism UA,UA );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines UAEnd ENDALG:def 1 :

theorem :: ENDALG:1

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

proof end;

theorem :: ENDALG:2

canceled;

theorem Th3: :: ENDALG:3

for UA being Universal_Algebra holds id the carrier of UA in UAEnd UA

proof end;

theorem Th4: :: ENDALG:4

for UA being Universal_Algebra
for f1, f2 being Element of UAEnd UA holds f1 * f2 in UAEnd UA

proof end;

definition

let UA be Universal_Algebra;
func UAEndComp UA -> BinOp of UAEnd UA means :Def2: :: ENDALG:def 2
for x, y being Element of UAEnd UA holds it . x,y = y * x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines UAEndComp ENDALG:def 2 :

definition

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

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines UAEndMonoid ENDALG:def 3 :

registration

let UA be Universal_Algebra;
cluster UAEndMonoid UA -> non empty strict ;
coherence

proof end;

end;

Lm1: now

let UA be Universal_Algebra; :: thesis:
set F = UAEndMonoid UA;
let x, e be Element of (UAEndMonoid UA); :: thesis:
assume A1: e = id the carrier of UA ; :: thesis:
reconsider i = e, y = x as Element of UAEnd UA by Def3;
thus x * e = the mult of (UAEndMonoid UA) . x,e
.= (UAEndComp UA) . y,i by Def3
.= i * y by Def2
.= x by A1, FUNCT_2:74 ; :: thesis:
thus e * x = the mult of (UAEndMonoid UA) . e,x
.= (UAEndComp UA) . i,y by Def3
.= y * i by Def2
.= x by A1, FUNCT_2:74 ; :: thesis:

end;

registration

let UA be Universal_Algebra;
cluster UAEndMonoid UA -> non empty unital associative strict ;
coherence

proof end;

end;

theorem Th5: :: ENDALG:5

for UA being Universal_Algebra
for x, y being Element of (UAEndMonoid UA)
for f, g being Element of UAEnd UA st x = f & y = g holds
x * y = g * f

proof end;

theorem Th6: :: ENDALG:6

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

proof end;

definition

let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of S;
func MSAEnd U1 -> MSFunctionSet of the Sorts of U1,the Sorts of U1 means :Def4: :: ENDALG:def 4
( ( for f being Element of it holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in it iff h is_homomorphism U1,U1 ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines MSAEnd ENDALG:def 4 :

theorem :: ENDALG:7

canceled;

theorem :: ENDALG:8

canceled;

theorem :: ENDALG:9

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

proof end;

theorem Th10: :: ENDALG:10

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S holds id the Sorts of U1 in MSAEnd U1

proof end;

theorem Th11: :: ENDALG:11

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for f1, f2 being Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1

proof end;

theorem Th12: :: ENDALG:12

for UA being Universal_Algebra
for F being ManySortedFunction of (MSAlg UA),(MSAlg UA)
for f being Element of UAEnd UA st F = {0} --> f holds
F in MSAEnd (MSAlg UA)

proof end;

definition

let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of S;
func MSAEndComp U1 -> BinOp of MSAEnd U1 means :Def5: :: ENDALG:def 5
for x, y being Element of MSAEnd U1 holds it . x,y = y ** x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines MSAEndComp ENDALG:def 5 :

definition

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

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines MSAEndMonoid ENDALG:def 6 :

registration

let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of S;
cluster MSAEndMonoid U1 -> non empty strict ;
coherence

proof end;

end;

Lm2: now

let S be non empty non void ManySortedSign ; :: thesis:
let U1 be non-empty MSAlgebra of S; :: thesis:
set F = MSAEndMonoid U1;
let x, e be Element of (MSAEndMonoid U1); :: thesis:
assume A1: e = id the Sorts of U1 ; :: thesis:
reconsider i = e, y = x as Element of MSAEnd U1 by Def6;
thus x * e = the mult of (MSAEndMonoid U1) . x,e
.= (MSAEndComp U1) . y,i by Def6
.= i ** y by Def5
.= x by A1, MSUALG_3:4 ; :: thesis:
thus e * x = the mult of (MSAEndMonoid U1) . e,x
.= (MSAEndComp U1) . i,y by Def6
.= y ** i by Def5
.= x by A1, MSUALG_3:3 ; :: thesis:

end;

registration

let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of S;
cluster MSAEndMonoid U1 -> non empty unital associative strict ;
coherence

proof end;

end;

theorem Th13: :: ENDALG:13

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for x, y being Element of (MSAEndMonoid U1)
for f, g being Element of MSAEnd U1 st x = f & y = g holds
x * y = g ** f

proof end;

theorem Th14: :: ENDALG:14

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S holds id the Sorts of U1 = 1. (MSAEndMonoid U1)

proof end;

theorem :: ENDALG:15

canceled;

theorem Th16: :: ENDALG:16

for UA being Universal_Algebra
for f being Element of UAEnd UA holds {0} --> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)

proof end;

Lm3: for UA being Universal_Algebra
for h being Function st dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds
h . x = {0} --> x ) holds
rng h = MSAEnd (MSAlg UA)

proof end;

definition

let G, H be non empty multLoopStr ;
let IT be Function of G,H;
canceled;
attr IT is unity-preserving means :Def8: :: ENDALG:def 8
IT . (1. G) = 1. H;

end;

:: deftheorem ENDALG:def 7 :

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

registration

cluster non empty left_unital multLoopStr ;
existence

proof end;

end;

registration

let G, H be non empty left_unital multLoopStr ;
cluster multiplicative unity-preserving M4(the carrier of G,the carrier of H);
existence

proof end;

end;

definition

let G, H be non empty left_unital multLoopStr ;
mode Homomorphism of G,H is multiplicative unity-preserving Function of G,H;

end;

definition

let G, H be non empty left_unital multLoopStr ;
let h be Function of G,H;
pred h is_monomorphism means :Def9: :: ENDALG:def 9
h is one-to-one;
pred h is_epimorphism means :Def10: :: ENDALG:def 10
rng h = the carrier of H;

end;

:: deftheorem Def9 defines is_monomorphism ENDALG:def 9 :

:: deftheorem Def10 defines is_epimorphism ENDALG:def 10 :

definition

let G, H be non empty left_unital multLoopStr ;
let h be Function of G,H;
pred h is_isomorphism means :Def11: :: ENDALG:def 11
( h is_epimorphism & h is_monomorphism );

end;

:: deftheorem Def11 defines is_isomorphism ENDALG:def 11 :

theorem Th17: :: ENDALG:17

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

proof end;

definition

let G, H be non empty left_unital multLoopStr ;
pred G,H are_isomorphic means :Def12: :: ENDALG:def 12
ex h being Homomorphism of G,H st h is_isomorphism ;
reflexivity

proof end;

end;

:: deftheorem Def12 defines are_isomorphic ENDALG:def 12 :

theorem Th18: :: ENDALG:18

for UA being Universal_Algebra
for h being Function st dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds
h . x = {0} --> x ) holds
h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA))

proof end;

theorem Th19: :: ENDALG:19

for UA being Universal_Algebra
for h being Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) st ( for x being set st x in UAEnd UA holds
h . x = {0} --> x ) holds
h is_isomorphism

proof end;

theorem :: ENDALG:20

for UA being Universal_Algebra holds UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic

proof end;