:: 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 :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies UNIALG_1, FUNCT_2, STRUCT_0, FUNCT_1, MSUALG_3, SUBSET_1, RELAT_1, XBOOLE_0, TARSKI, BINOP_1, ALGSTR_0, MESFUNC1, VECTSP_1, GROUP_1, MSUALG_1, AUTALG_1, PBOOLE, MEMBER_1, CARD_1, FUNCOP_1, MSUHOM_1, MSSUBFAM, GROUP_6, WELLORD1, ZFMISC_1, ENDALG; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE, CARD_3, BINOP_1, PARTFUN1, FUNCT_2, FUNCOP_1, ORDINAL1, NUMBERS, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, FINSEQ_1, PZFMISC1, UNIALG_1, MSUALG_1, ALG_1, MSUALG_3, MSUHOM_1, AUTALG_1, GROUP_6; constructors BINOP_1, CARD_3, PZFMISC1, VECTSP_1, GROUP_6, ALG_1, MSUALG_3, MSUHOM_1, AUTALG_1, RELSET_1, NUMBERS; registrations XBOOLE_0, FUNCT_1, FUNCT_2, PBOOLE, STRUCT_0, VECTSP_1, MSUALG_1, ALGSTR_0, RELSET_1; requirements SUBSET, BOOLE; begin reserve UA for Universal_Algebra; definition let UA; func UAEnd UA -> FUNCTION_DOMAIN of the carrier of UA, the carrier of UA means :: ENDALG:def 1 for h be Function of UA, UA holds h in it iff h is_homomorphism; end; theorem :: ENDALG:1 UAEnd UA c= Funcs (the carrier of UA, the carrier of UA); theorem :: ENDALG:2 id the carrier of UA in UAEnd UA; theorem :: ENDALG:3 for f1, f2 be Element of UAEnd UA holds f1 * f2 in UAEnd UA; definition let UA; func UAEndComp UA -> BinOp of UAEnd UA means :: ENDALG:def 2 for x, y be Element of UAEnd UA holds it.(x, y) = y * x; end; definition let UA; func UAEndMonoid UA -> strict multLoopStr means :: ENDALG:def 3 the carrier of it = UAEnd UA & the multF of it = UAEndComp UA & 1.it = id the carrier of UA; end; registration let UA; cluster UAEndMonoid UA -> non empty; end; registration let UA; cluster UAEndMonoid UA -> well-unital associative; end; theorem :: ENDALG:4 for x, y be Element of UAEndMonoid UA for f, g be Element of UAEnd UA st x = f & y = g holds x * y = g * f; theorem :: ENDALG:5 id the carrier of UA = 1_UAEndMonoid UA; reserve S for non void non empty ManySortedSign, U1 for non-empty MSAlgebra over S; definition let S, U1; func MSAEnd U1 -> MSFunctionSet of U1,U1 means :: ENDALG:def 4 (for f be Element of it holds f is ManySortedFunction of U1, U1) & for h be ManySortedFunction of U1, U1 holds h in it iff h is_homomorphism U1, U1; end; theorem :: ENDALG:6 MSAEnd U1 c= MSFuncs(the Sorts of U1, the Sorts of U1); theorem :: ENDALG:7 id the Sorts of U1 in MSAEnd U1; theorem :: ENDALG:8 for f1, f2 be Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1; theorem :: ENDALG:9 for F be ManySortedFunction of MSAlg UA, MSAlg UA for f be Element of UAEnd UA st F = 0 .--> f holds F in MSAEnd MSAlg UA; definition let S, U1; func MSAEndComp U1 -> BinOp of MSAEnd U1 means :: ENDALG:def 5 for x, y be Element of MSAEnd U1 holds it.(x, y) = y ** x; end; definition let S, U1; func MSAEndMonoid U1 -> strict multLoopStr means :: ENDALG:def 6 the carrier of it = MSAEnd U1 & the multF of it = MSAEndComp U1 & 1.it = id the Sorts of U1; end; registration let S, U1; cluster MSAEndMonoid U1 -> non empty; end; registration let S,U1; cluster MSAEndMonoid U1 -> well-unital associative; end; theorem :: ENDALG:10 for x, y be Element of MSAEndMonoid U1 for f, g be Element of MSAEnd U1 st x = f & y = g holds x * y = g ** f; theorem :: ENDALG:11 id the Sorts of U1 = 1_MSAEndMonoid U1; theorem :: ENDALG:12 for f be Element of UAEnd UA holds 0 .--> f is ManySortedFunction of MSAlg UA, MSAlg UA; registration cluster left_unital for non empty multLoopStr; end; registration let G,H be well-unital non empty multLoopStr; cluster multiplicative unity-preserving for Function of G,H; end; definition let G,H be well-unital non empty multLoopStr; mode Homomorphism of G,H is multiplicative unity-preserving Function of G,H; end; theorem :: ENDALG:13 for G be well-unital non empty multLoopStr holds id the carrier of G is Homomorphism of G,G; definition let G,H be well-unital non empty multLoopStr; pred G,H are_isomorphic means :: ENDALG:def 7 ex h be Homomorphism of G,H st h is bijective; reflexivity; end; theorem :: ENDALG:14 for h be Function st (dom h = UAEnd UA & for x be object st x in UAEnd UA holds h.x = 0 .--> x) holds h is Homomorphism of UAEndMonoid UA, MSAEndMonoid (MSAlg UA); theorem :: ENDALG:15 for h be Homomorphism of UAEndMonoid UA, MSAEndMonoid (MSAlg UA) st for x be object st x in UAEnd UA holds h.x = 0 .--> x holds h is bijective; theorem :: ENDALG:16 UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic;