:: by Jaros{\l}aw Gryko

::

:: Received October 17, 1995

:: Copyright (c) 1995-2019 Association of Mizar Users

definition

let UA be Universal_Algebra;

ex b_{1} being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st

for h being Function of UA,UA holds

( h in b_{1} iff h is_homomorphism )

for b_{1}, b_{2} being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st ( for h being Function of UA,UA holds

( h in b_{1} iff h is_homomorphism ) ) & ( for h being Function of UA,UA holds

( h in b_{2} iff h is_homomorphism ) ) holds

b_{1} = b_{2}

end;
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 for h being Function of UA,UA holds

( h in it iff h is_homomorphism );

ex b

for h being Function of UA,UA holds

( h in b

proof end;

uniqueness for b

( h in b

( h in b

b

proof end;

:: deftheorem Def1 defines UAEnd ENDALG:def 1 :

for UA being Universal_Algebra

for b_{2} being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA holds

( b_{2} = UAEnd UA iff for h being Function of UA,UA holds

( h in b_{2} iff h is_homomorphism ) );

for UA being Universal_Algebra

for b

( b

( h in b

definition

let UA be Universal_Algebra;

ex b_{1} being BinOp of (UAEnd UA) st

for x, y being Element of UAEnd UA holds b_{1} . (x,y) = y * x

for b_{1}, b_{2} being BinOp of (UAEnd UA) st ( for x, y being Element of UAEnd UA holds b_{1} . (x,y) = y * x ) & ( for x, y being Element of UAEnd UA holds b_{2} . (x,y) = y * x ) holds

b_{1} = b_{2}

end;
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 for x, y being Element of UAEnd UA holds it . (x,y) = y * x;

ex b

for x, y being Element of UAEnd UA holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines UAEndComp ENDALG:def 2 :

for UA being Universal_Algebra

for b_{2} being BinOp of (UAEnd UA) holds

( b_{2} = UAEndComp UA iff for x, y being Element of UAEnd UA holds b_{2} . (x,y) = y * x );

for UA being Universal_Algebra

for b

( b

definition

let UA be Universal_Algebra;

ex b_{1} being strict multLoopStr st

( the carrier of b_{1} = UAEnd UA & the multF of b_{1} = UAEndComp UA & 1. b_{1} = id the carrier of UA )

for b_{1}, b_{2} being strict multLoopStr st the carrier of b_{1} = UAEnd UA & the multF of b_{1} = UAEndComp UA & 1. b_{1} = id the carrier of UA & the carrier of b_{2} = UAEnd UA & the multF of b_{2} = UAEndComp UA & 1. b_{2} = id the carrier of UA holds

b_{1} = b_{2}
;

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

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def3 defines UAEndMonoid ENDALG:def 3 :

for UA being Universal_Algebra

for b_{2} being strict multLoopStr holds

( b_{2} = UAEndMonoid UA iff ( the carrier of b_{2} = UAEnd UA & the multF of b_{2} = UAEndComp UA & 1. b_{2} = id the carrier of UA ) );

for UA being Universal_Algebra

for b

( b

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 )

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

registration

let UA be Universal_Algebra;

coherence

( UAEndMonoid UA is well-unital & UAEndMonoid UA is associative )

end;
coherence

( UAEndMonoid UA is well-unital & UAEndMonoid UA is associative )

proof 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

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

definition

let S be non empty non void ManySortedSign ;

let U1 be non-empty MSAlgebra over S;

set T = the Sorts of U1;

ex b_{1} being MSFunctionSet of U1,U1 st

( ( for f being Element of b_{1} holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds

( h in b_{1} iff h is_homomorphism U1,U1 ) ) )

for b_{1}, b_{2} being MSFunctionSet of U1,U1 st ( for f being Element of b_{1} holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds

( h in b_{1} iff h is_homomorphism U1,U1 ) ) & ( for f being Element of b_{2} holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds

( h in b_{2} iff h is_homomorphism U1,U1 ) ) holds

b_{1} = b_{2}

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

ex b

( ( for f being Element of b

( h in b

proof end;

uniqueness for b

( h in b

( h in b

b

proof 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 b_{3} being MSFunctionSet of U1,U1 holds

( b_{3} = MSAEnd U1 iff ( ( for f being Element of b_{3} holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds

( h in b_{3} iff h is_homomorphism U1,U1 ) ) ) );

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for b

( b

( h in b

theorem :: ENDALG:6

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

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

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)

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;

ex b_{1} being BinOp of (MSAEnd U1) st

for x, y being Element of MSAEnd U1 holds b_{1} . (x,y) = y ** x

for b_{1}, b_{2} being BinOp of (MSAEnd U1) st ( for x, y being Element of MSAEnd U1 holds b_{1} . (x,y) = y ** x ) & ( for x, y being Element of MSAEnd U1 holds b_{2} . (x,y) = y ** x ) holds

b_{1} = b_{2}

end;
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 for x, y being Element of MSAEnd U1 holds it . (x,y) = y ** x;

ex b

for x, y being Element of MSAEnd U1 holds b

proof end;

uniqueness for b

b

proof 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 b_{3} being BinOp of (MSAEnd U1) holds

( b_{3} = MSAEndComp U1 iff for x, y being Element of MSAEnd U1 holds b_{3} . (x,y) = y ** x );

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for b

( b

definition

let S be non empty non void ManySortedSign ;

let U1 be non-empty MSAlgebra over S;

ex b_{1} being strict multLoopStr st

( the carrier of b_{1} = MSAEnd U1 & the multF of b_{1} = MSAEndComp U1 & 1. b_{1} = id the Sorts of U1 )

for b_{1}, b_{2} being strict multLoopStr st the carrier of b_{1} = MSAEnd U1 & the multF of b_{1} = MSAEndComp U1 & 1. b_{1} = id the Sorts of U1 & the carrier of b_{2} = MSAEnd U1 & the multF of b_{2} = MSAEndComp U1 & 1. b_{2} = id the Sorts of U1 holds

b_{1} = b_{2}
;

end;
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 ( the carrier of it = MSAEnd U1 & the multF of it = MSAEndComp U1 & 1. it = id the Sorts of U1 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def6 defines MSAEndMonoid ENDALG:def 6 :

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for b_{3} being strict multLoopStr holds

( b_{3} = MSAEndMonoid U1 iff ( the carrier of b_{3} = MSAEnd U1 & the multF of b_{3} = MSAEndComp U1 & 1. b_{3} = id the Sorts of U1 ) );

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for b

( b

registration

let S be non empty non void ManySortedSign ;

let U1 be non-empty MSAlgebra over S;

coherence

not MSAEndMonoid U1 is empty

end;
let U1 be non-empty MSAlgebra over S;

coherence

not MSAEndMonoid U1 is empty

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

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

registration

let S be non empty non void ManySortedSign ;

let U1 be non-empty MSAlgebra over S;

coherence

( MSAEndMonoid U1 is well-unital & MSAEndMonoid U1 is associative )

end;
let U1 be non-empty MSAlgebra over S;

coherence

( MSAEndMonoid U1 is well-unital & MSAEndMonoid U1 is associative )

proof 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

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

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)

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

let G, H be non empty well-unital multLoopStr ;

ex b_{1} being Function of G,H st

( b_{1} is multiplicative & b_{1} is unity-preserving )

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

( b

proof 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;
mode Homomorphism of G,H is unity-preserving multiplicative Function of G,H;

definition

let G, H be non empty well-unital multLoopStr ;

reflexivity

for G being non empty well-unital multLoopStr ex h being Homomorphism of G,G st h is bijective

end;
reflexivity

for G being non empty well-unital multLoopStr ex h being Homomorphism of G,G st h is bijective

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

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

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

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;