:: On the Monoid of Endomorphisms of Universal Algebra \& Many Sorted Algebra
:: by Jaros{\l}aw Gryko
::
:: Received October 17, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

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
 ex b1 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st
for h being Function of UA,UA holds
( h in b1 iff h is_homomorphism UA,UA )
proofend;
uniqueness
 for b1, b2 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st ( for h being Function of UA,UA holds
( h in b1 iff h is_homomorphism UA,UA ) ) & ( for h being Function of UA,UA holds
( h in b2 iff h is_homomorphism UA,UA ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines UAEnd ENDALG:def_1_:_
 for UA being Universal_Algebra
for b2 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA holds
( b2 = UAEnd UA iff for h being Function of UA,UA holds
( h in b2 iff h is_homomorphism UA,UA ) );

theorem :: ENDALG:1
for UA being Universal_Algebra holds UAEnd UA c= Funcs ( the carrier of UA, the carrier of UA)
proofend;

theorem Th2: :: ENDALG:2
for UA being Universal_Algebra holds id the carrier of UA in UAEnd UA
proofend;

theorem Th3: :: ENDALG:3
for UA being Universal_Algebra
for f1, f2 being Element of UAEnd UA holds f1 * f2 in UAEnd UA
proofend;

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
 ex b1 being BinOp of (UAEnd UA) st
for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x
proofend;
uniqueness
 for b1, b2 being BinOp of (UAEnd UA) st ( for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x ) & ( for x, y being Element of UAEnd UA holds b2 . (x,y) = y * x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines UAEndComp ENDALG:def_2_:_
 for UA being Universal_Algebra
for b2 being BinOp of (UAEnd UA) holds
( b2 = UAEndComp UA iff for x, y being Element of UAEnd UA holds b2 . (x,y) = y * x );

definition
let UA be Universal_Algebra;
func UAEndMonoid UA ->  strict multLoopStr  means :Def3: :: ENDALG:def 3
( the carrier of it = UAEnd UA & the multF of it = UAEndComp UA & 1. it = id the carrier of UA );
existence
 ex b1 being strict multLoopStr st
( the carrier of b1 = UAEnd UA & the multF of b1 = UAEndComp UA & 1. b1 = id the carrier of UA )
proofend;
uniqueness
 for b1, b2 being strict multLoopStr st the carrier of b1 = UAEnd UA & the multF of b1 = UAEndComp UA & 1. b1 = id the carrier of UA & the carrier of b2 = UAEnd UA & the multF of b2 = UAEndComp UA & 1. b2 = id the carrier of UA holds
b1 = b2 ;
end;

:: deftheorem Def3 defines UAEndMonoid ENDALG:def_3_:_
 for UA being Universal_Algebra
for b2 being strict multLoopStr holds
( b2 = UAEndMonoid UA iff ( the carrier of b2 = UAEnd UA & the multF of b2 = UAEndComp UA & 1. b2 = id the carrier of UA ) );

registration
let UA be Universal_Algebra;
cluster UAEndMonoid UA ->  non empty strict ;
coherence
 not UAEndMonoid UA is empty
proofend;
end;

Lm1: now__::_thesis:_for_UA_being_Universal_Algebra
for_x,_e_being_Element_of_(UAEndMonoid_UA)_st_e_=_id_the_carrier_of_UA_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let UA be Universal_Algebra; ::_thesis: for x, e being Element of (UAEndMonoid UA) st e = id the carrier of UA holds
( x * e = x & e * x = x )
let x, e be Element of (UAEndMonoid UA); ::_thesis: ( e = id the carrier of UA implies ( x * e = x & e * x = x ) )
reconsider i = e, y = x as Element of UAEnd UA by Def3;
assume A1: e = id the carrier of UA ; ::_thesis: ( x * e = x & e * x = x )
thus x * e = (UAEndComp UA) . (y,i) by Def3
.= i * y by Def2
.= x by A1, FUNCT_2:17 ; ::_thesis: e * x = x
thus e * x = (UAEndComp UA) . (i,y) by Def3
.= y * i by Def2
.= x by A1, FUNCT_2:17 ; ::_thesis: verum
end;

registration
let UA be Universal_Algebra;
cluster UAEndMonoid UA ->  strict associative well-unital ;
coherence
 ( UAEndMonoid UA is well-unital & UAEndMonoid UA is associative )
proofend;
end;

theorem Th4: :: ENDALG:4
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
proofend;

theorem :: ENDALG:5
for UA being Universal_Algebra holds id the carrier of UA = 1_ (UAEndMonoid UA) by Def3;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
set T = the Sorts of U1;
func MSAEnd U1 ->  MSFunctionSet of U1,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
 ex b1 being MSFunctionSet of U1,U1 st
( ( for f being Element of b1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b1 iff h is_homomorphism U1,U1 ) ) )
proofend;
uniqueness
 for b1, b2 being MSFunctionSet of U1,U1 st ( for f being Element of b1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b1 iff h is_homomorphism U1,U1 ) ) & ( for f being Element of b2 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b2 iff h is_homomorphism U1,U1 ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines MSAEnd ENDALG:def_4_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for b3 being MSFunctionSet of U1,U1 holds
( b3 = MSAEnd U1 iff ( ( for f being Element of b3 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b3 iff h is_homomorphism U1,U1 ) ) ) );

theorem :: ENDALG:6
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds MSAEnd U1 c= MSFuncs ( the Sorts of U1, the Sorts of U1) ;

theorem Th7: :: ENDALG:7
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSAEnd U1
proofend;

theorem Th8: :: ENDALG:8
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for f1, f2 being Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1
proofend;

theorem Th9: :: ENDALG:9
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)
proofend;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over 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
 ex b1 being BinOp of (MSAEnd U1) st
for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x
proofend;
uniqueness
 for b1, b2 being BinOp of (MSAEnd U1) st ( for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x ) & ( for x, y being Element of MSAEnd U1 holds b2 . (x,y) = y ** x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines MSAEndComp ENDALG:def_5_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for b3 being BinOp of (MSAEnd U1) holds
( b3 = MSAEndComp U1 iff for x, y being Element of MSAEnd U1 holds b3 . (x,y) = y ** x );

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
func MSAEndMonoid U1 ->  strict multLoopStr  means :Def6: :: ENDALG:def 6
( the carrier of it = MSAEnd U1 & the multF of it = MSAEndComp U1 & 1. it = id the Sorts of U1 );
existence
 ex b1 being strict multLoopStr st
( the carrier of b1 = MSAEnd U1 & the multF of b1 = MSAEndComp U1 & 1. b1 = id the Sorts of U1 )
proofend;
uniqueness
 for b1, b2 being strict multLoopStr st the carrier of b1 = MSAEnd U1 & the multF of b1 = MSAEndComp U1 & 1. b1 = id the Sorts of U1 & the carrier of b2 = MSAEnd U1 & the multF of b2 = MSAEndComp U1 & 1. b2 = id the Sorts of U1 holds
b1 = b2 ;
end;

:: deftheorem Def6 defines MSAEndMonoid ENDALG:def_6_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for b3 being strict multLoopStr holds
( b3 = MSAEndMonoid U1 iff ( the carrier of b3 = MSAEnd U1 & the multF of b3 = MSAEndComp U1 & 1. b3 = id the Sorts of U1 ) );

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
cluster MSAEndMonoid U1 ->  non empty strict ;
coherence
 not MSAEndMonoid U1 is empty
proofend;
end;

Lm2: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_
for_U1_being_non-empty_MSAlgebra_over_S
for_x,_e_being_Element_of_(MSAEndMonoid_U1)_st_e_=_id_the_Sorts_of_U1_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S
for x, e being Element of (MSAEndMonoid U1) st e = id the Sorts of U1 holds
( x * e = x & e * x = x )
let U1 be non-empty MSAlgebra over S; ::_thesis: for x, e being Element of (MSAEndMonoid U1) st e = id the Sorts of U1 holds
( x * e = x & e * x = x )
set F = MSAEndMonoid U1;
let x, e be Element of (MSAEndMonoid U1); ::_thesis: ( e = id the Sorts of U1 implies ( x * e = x & e * x = x ) )
reconsider i = e, y = x as Element of MSAEnd U1 by Def6;
assume A1: e = id the Sorts of U1 ; ::_thesis: ( x * e = x & e * x = x )
thus x * e = (MSAEndComp U1) . (y,i) by Def6
.= i ** y by Def5
.= x by A1, MSUALG_3:4 ; ::_thesis: e * x = x
thus e * x = (MSAEndComp U1) . (i,y) by Def6
.= y ** i by Def5
.= x by A1, MSUALG_3:3 ; ::_thesis: verum
end;

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
cluster MSAEndMonoid U1 ->  strict associative well-unital ;
coherence
 ( MSAEndMonoid U1 is well-unital & MSAEndMonoid U1 is associative )
proofend;
end;

theorem Th10: :: ENDALG:10
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over 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
proofend;

theorem :: ENDALG:11
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 = 1_ (MSAEndMonoid U1) by Def6;

theorem Th12: :: ENDALG:12
for UA being Universal_Algebra
for f being Element of UAEnd UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)
proofend;

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

registration
cluster non empty left_unital for multLoopStr ;
existence
 ex b1 being non empty multLoopStr st b1 is left_unital
proofend;
end;

registration
let G, H be non empty well-unital multLoopStr ;
cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving multiplicative for Element of bool [: the carrier of G, the carrier of H:];
existence
 ex b1 being Function of G,H st
( b1 is multiplicative & b1 is unity-preserving )
proofend;
end;

definition
let G, H be non empty well-unital multLoopStr ;
mode Homomorphism of G,H is unity-preserving multiplicative Function of G,H;
end;

theorem Th13: :: ENDALG:13
for G being non empty well-unital multLoopStr holds id the carrier of G is Homomorphism of G,G
proofend;

definition
let G, H be non empty well-unital multLoopStr ;
predG,H are_isomorphic  means :Def7: :: ENDALG:def 7
 ex h being Homomorphism of G,H st h is bijective ;
reflexivity
 for G being non empty well-unital multLoopStr ex h being Homomorphism of G,G st h is bijective
proofend;
end;

:: deftheorem Def7 defines are_isomorphic ENDALG:def_7_:_
 for G, H being non empty well-unital multLoopStr holds
( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective );

theorem Th14: :: ENDALG:14
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))
proofend;

theorem Th15: :: ENDALG:15
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 bijective
proofend;

theorem :: ENDALG:16
for UA being Universal_Algebra holds UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic
proofend;