ENDALG: On the Monoid of Endomorphisms of Universal Algebra \& Many Sorted Algebra

:: On the Monoid of Endomorphisms of Universal Algebra \& Many Sorted Algebra
:: by Jaros{\l}aw Gryko
::
:: Received October 17, 1995
:: 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 );

proof end;

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

proof end;

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 multF of it = UAEndComp UA & 1. it = id the carrier of UA );

proof end;

end;

:: deftheorem Def3 defines UAEndMonoid ENDALG:def 3 :

registration

let UA be Universal_Algebra;

cluster UAEndMonoid UA -> non empty strict ;

proof end;

end;

Lm1: now :: thesis:

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

end;

registration

let UA be Universal_Algebra;

cluster UAEndMonoid UA -> strict well-unital associative ;

proof end;

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

proof end;

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

proof end;

proof end;

end;

:: deftheorem Def4 defines MSAEnd ENDALG:def 4 :

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;

proof end;

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

proof end;

end;

:: deftheorem Def6 defines MSAEndMonoid ENDALG:def 6 :

registration

let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;

cluster MSAEndMonoid U1 -> non empty strict ;

proof end;

end;

Lm2: now :: thesis:

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

cluster MSAEndMonoid U1 -> strict well-unital associative ;

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 (MSAEndMonoid U1)
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_ (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)

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

cluster non empty left_unital for multLoopStr ;

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:];

proof end;

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

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 ;

proof end;

end;

:: deftheorem defines are_isomorphic ENDALG:def 7 :

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 (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA))

proof end;

theorem Th15: :: ENDALG:15

for UA being Universal_Algebra
for h being Homomorphism of (UAEndMonoid UA),(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;