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

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 );
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 )
proof end;
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 ) ) & ( for h being Function of UA,UA holds
( h in b2 iff h is_homomorphism ) ) holds
b1 = b2
proof end;
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 ) );

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

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

theorem Th3: :: ENDALG:3
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
ex b1 being BinOp of (UAEnd UA) st
for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x
proof end;
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
proof end;
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 )
proof end;
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
proof end;
end;

Lm1: now :: thesis: for UA being Universal_Algebra
for x, e being Element of () 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 () st e = id the carrier of UA holds
( x * e = x & e * x = x )

let x, e be Element of (); :: 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 = () . (y,i) by Def3
.= i * y by Def2
.= x by ; :: thesis: e * x = x
thus e * x = () . (i,y) by Def3
.= y * i by Def2
.= x by ; :: thesis: verum
end;

registration
let UA be Universal_Algebra;
coherence
( UAEndMonoid UA is well-unital & UAEndMonoid UA is associative )
proof end;
end;

theorem Th4: :: ENDALG:4
for UA being Universal_Algebra
for x, y being Element of ()
for f, g being Element of UAEnd UA st x = f & y = g holds
x * y = g * f
proof end;

theorem :: ENDALG:5
for UA being Universal_Algebra holds id the carrier of UA = 1_ () 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 ) ) )
proof end;
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
proof end;
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
proof end;

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
proof end;

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)
proof end;

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
proof end;
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
proof end;
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 )
proof end;
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
proof end;
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 () 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 () 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 () st e = id the Sorts of U1 holds
( x * e = x & e * x = x )

set F = MSAEndMonoid U1;
let x, e be Element of (); :: 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 = () . (y,i) by Def6
.= i ** y by Def5
.= x by ; :: thesis: e * x = x
thus e * x = () . (i,y) by Def6
.= y ** i by Def5
.= x by ; :: thesis: verum
end;

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
coherence
proof end;
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 ()
for f, g being Element of MSAEnd U1 st x = f & y = g holds
x * y = g ** f
proof end;

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_ () 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)
proof end;

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

proof end;

registration
existence
ex b1 being non empty multLoopStr st b1 is left_unital
proof end;
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 )
proof end;
end;

definition end;

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

definition
let G, H be non empty well-unital multLoopStr ;
pred G,H are_isomorphic means :: 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
proof end;
end;

:: deftheorem 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 object st x in UAEnd UA holds
h . x = 0 .--> x ) holds
h is Homomorphism of (),(MSAEndMonoid (MSAlg UA))
proof end;

theorem Th15: :: ENDALG:15
for UA being Universal_Algebra
for h being Homomorphism of (),(MSAEndMonoid (MSAlg UA)) st ( for x being object st x in UAEnd UA holds
h . x = 0 .--> x ) holds
h is bijective
proof end;

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