:: Homomorphisms of Many Sorted Algebras :: by Ma{\l}gorzata Korolkiewicz :: :: Received April 25, 1994 :: Copyright (c) 1994-2012 Association of Mizar Users begin :: PRELIMINARIES - MANY SORTED FUNCTIONS definition let I be non empty set ; let A, B be ManySortedSet of I; let F be ManySortedFunction of A,B; let i be Element of I; :: original:. redefine funcF . i -> Function of (A . i),(B . i); coherence F . i is Function of (A . i),(B . i) by PBOOLE:def_15; end; definition let S be non empty ManySortedSign ; let U1, U2 be MSAlgebra over S; mode ManySortedFunction of U1,U2 is ManySortedFunction of the Sorts of U1, the Sorts of U2; end; definition let I be set ; let A be ManySortedSet of I; func id A -> ManySortedFunction of A,A means :Def1: :: MSUALG_3:def 1 for i being set st i in I holds it . i = id (A . i); existence ex b1 being ManySortedFunction of A,A st for i being set st i in I holds b1 . i = id (A . i) proofend; uniqueness for b1, b2 being ManySortedFunction of A,A st ( for i being set st i in I holds b1 . i = id (A . i) ) & ( for i being set st i in I holds b2 . i = id (A . i) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines id MSUALG_3:def_1_:_ for I being set for A being ManySortedSet of I for b3 being ManySortedFunction of A,A holds ( b3 = id A iff for i being set st i in I holds b3 . i = id (A . i) ); definition let IT be Function; attrIT is "1-1" means :Def2: :: MSUALG_3:def 2 for i being set for f being Function st i in dom IT & IT . i = f holds f is one-to-one ; end; :: deftheorem Def2 defines "1-1" MSUALG_3:def_2_:_ for IT being Function holds ( IT is "1-1" iff for i being set for f being Function st i in dom IT & IT . i = f holds f is one-to-one ); registration let I be set ; cluster Relation-like I -defined Function-like total V41() V42() "1-1" for set ; existence ex b1 being ManySortedFunction of I st b1 is "1-1" proofend; end; theorem Th1: :: MSUALG_3:1 for I being set for F being ManySortedFunction of I holds ( F is "1-1" iff for i being set st i in I holds F . i is one-to-one ) proofend; definition let I be set ; let A, B be ManySortedSet of I; let IT be ManySortedFunction of A,B; attrIT is "onto" means :Def3: :: MSUALG_3:def 3 for i being set st i in I holds rng (IT . i) = B . i; end; :: deftheorem Def3 defines "onto" MSUALG_3:def_3_:_ for I being set for A, B being ManySortedSet of I for IT being ManySortedFunction of A,B holds ( IT is "onto" iff for i being set st i in I holds rng (IT . i) = B . i ); theorem Th2: :: MSUALG_3:2 for I being set for A, B, C being ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C holds ( dom (G ** F) = I & ( for i being set st i in I holds (G ** F) . i = (G . i) * (F . i) ) ) proofend; definition let I be set ; let A be ManySortedSet of I; let B, C be V2() ManySortedSet of I; let F be ManySortedFunction of A,B; let G be ManySortedFunction of B,C; :: original:** redefine funcG ** F -> ManySortedFunction of A,C; coherence G ** F is ManySortedFunction of A,C proofend; end; theorem :: MSUALG_3:3 for I being set for A, B being ManySortedSet of I for F being ManySortedFunction of A,B holds F ** (id A) = F proofend; theorem Th4: :: MSUALG_3:4 for I being set for A, B being ManySortedSet of I for F being ManySortedFunction of A,B holds (id B) ** F = F proofend; definition let I be set ; let A, B be ManySortedSet of I; let F be ManySortedFunction of A,B; assume that A1: F is "1-1" and A2: F is "onto" ; funcF "" -> ManySortedFunction of B,A means :Def4: :: MSUALG_3:def 4 for i being set st i in I holds it . i = (F . i) " ; existence ex b1 being ManySortedFunction of B,A st for i being set st i in I holds b1 . i = (F . i) " proofend; uniqueness for b1, b2 being ManySortedFunction of B,A st ( for i being set st i in I holds b1 . i = (F . i) " ) & ( for i being set st i in I holds b2 . i = (F . i) " ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines "" MSUALG_3:def_4_:_ for I being set for A, B being ManySortedSet of I for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds for b5 being ManySortedFunction of B,A holds ( b5 = F "" iff for i being set st i in I holds b5 . i = (F . i) " ); theorem Th5: :: MSUALG_3:5 for I being set for A, B being V2() ManySortedSet of I for H being ManySortedFunction of A,B for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds ( H ** H1 = id B & H1 ** H = id A ) proofend; registration let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; let o be OperSymbol of S; cluster Args (o,U1) -> functional ; coherence Args (o,U1) is functional proofend; end; begin :: HOMOMORPHISMS OF MANY SORTED ALGEBRAS theorem Th6: :: MSUALG_3:6 for S being non empty non void ManySortedSign for o being OperSymbol of S for U1 being MSAlgebra over S for x being Function st x in Args (o,U1) holds ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) ) proofend; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; let o be OperSymbol of S; let F be ManySortedFunction of U1,U2; let x be Element of Args (o,U1); assume that A1: Args (o,U1) <> {} and A2: Args (o,U2) <> {} ; funcF # x -> Element of Args (o,U2) equals :Def5: :: MSUALG_3:def 5 (Frege (F * (the_arity_of o))) . x; coherence (Frege (F * (the_arity_of o))) . x is Element of Args (o,U2) proofend; correctness ; end; :: deftheorem Def5 defines # MSUALG_3:def_5_:_ for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for o being OperSymbol of S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) st Args (o,U1) <> {} & Args (o,U2) <> {} holds F # x = (Frege (F * (the_arity_of o))) . x; Lm1: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_ for_U1,_U2_being_MSAlgebra_over_S for_o_being_OperSymbol_of_S for_F_being_ManySortedFunction_of_U1,U2 for_x_being_Element_of_Args_(o,U1) for_f,_u_being_Function_st_x_=_f_&_x_in_Args_(o,U1)_&_u_in_Args_(o,U2)_holds_ (_(_u_=_F_#_x_implies_for_n_being_Nat_st_n_in_dom_f_holds_ u_._n_=_(F_._((the_arity_of_o)_/._n))_._(f_._n)_)_&_(_(_for_n_being_Nat_st_n_in_dom_f_holds_ u_._n_=_(F_._((the_arity_of_o)_/._n))_._(f_._n)_)_implies_u_=_F_#_x_)_) let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being MSAlgebra over S for o being OperSymbol of S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) let U1, U2 be MSAlgebra over S; ::_thesis: for o being OperSymbol of S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) let o be OperSymbol of S; ::_thesis: for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) let F be ManySortedFunction of U1,U2; ::_thesis: for x being Element of Args (o,U1) for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) let x be Element of Args (o,U1); ::_thesis: for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) let f, u be Function; ::_thesis: ( x = f & x in Args (o,U1) & u in Args (o,U2) implies ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) ) assume that A1: x = f and A2: x in Args (o,U1) and A3: u in Args (o,U2) ; ::_thesis: ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) A4: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4; then A5: rng (the_arity_of o) c= dom the Sorts of U1 by PARTFUN1:def_2; A6: F # x = (Frege (F * (the_arity_of o))) . x by A2, A3, Def5; A7: dom ( the Sorts of U1 * (the_arity_of o)) = (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) proof hereby :: according toTARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) c= dom ( the Sorts of U1 * (the_arity_of o)) let e be set ; ::_thesis: ( e in dom ( the Sorts of U1 * (the_arity_of o)) implies e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ) A8: (F * (the_arity_of o)) . e is Function ; assume A9: e in dom ( the Sorts of U1 * (the_arity_of o)) ; ::_thesis: e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) then (the_arity_of o) . e in dom the Sorts of U1 by FUNCT_1:11; then (the_arity_of o) . e in the carrier of S by PARTFUN1:def_2; then A10: (the_arity_of o) . e in dom F by PARTFUN1:def_2; e in dom (the_arity_of o) by A9, FUNCT_1:11; then e in dom (F * (the_arity_of o)) by A10, FUNCT_1:11; hence e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by A8, FUNCT_6:19; ::_thesis: verum end; let e be set ; :: according toTARSKI:def_3 ::_thesis: ( not e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) or e in dom ( the Sorts of U1 * (the_arity_of o)) ) assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; ::_thesis: e in dom ( the Sorts of U1 * (the_arity_of o)) then e in dom (F * (the_arity_of o)) by FUNCT_6:19; then A11: e in dom (the_arity_of o) by FUNCT_1:11; then reconsider f = e as Element of NAT ; (the_arity_of o) . f in the carrier of S by A11, FINSEQ_2:11; then (the_arity_of o) . e in dom the Sorts of U1 by PARTFUN1:def_2; hence e in dom ( the Sorts of U1 * (the_arity_of o)) by A11, FUNCT_1:11; ::_thesis: verum end; A12: Args (o,U2) = product ( the Sorts of U2 * (the_arity_of o)) by PRALG_2:3; then A13: dom u = dom ( the Sorts of U2 * (the_arity_of o)) by A3, CARD_3:9; A14: Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3; then A15: dom f = dom ( the Sorts of U1 * (the_arity_of o)) by A1, A2, CARD_3:9 .= dom (the_arity_of o) by A5, RELAT_1:27 ; rng (the_arity_of o) c= dom the Sorts of U2 by A4, PARTFUN1:def_2; then A16: dom u = dom (the_arity_of o) by A13, RELAT_1:27; now__::_thesis:_for_e_being_set_st_e_in_(F_*_(the_arity_of_o))_"_(SubFuncs_(rng_(F_*_(the_arity_of_o))))_holds_ (_the_Sorts_of_U1_*_(the_arity_of_o))_._e_=_proj1_((F_*_(the_arity_of_o))_._e) let e be set ; ::_thesis: ( e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) implies ( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e) ) assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; ::_thesis: ( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e) then e in dom (F * (the_arity_of o)) by FUNCT_6:19; then A17: e in dom (the_arity_of o) by FUNCT_1:11; then reconsider Foe = F . ((the_arity_of o) . e) as Function of ( the Sorts of U1 . ((the_arity_of o) . e)),( the Sorts of U2 . ((the_arity_of o) . e)) by FINSEQ_2:11, PBOOLE:def_15; ( the Sorts of U2 * (the_arity_of o)) . e in rng ( the Sorts of U2 * (the_arity_of o)) by A13, A16, A17, FUNCT_1:def_3; then A18: ( the Sorts of U2 * (the_arity_of o)) . e <> {} by A3, A12, CARD_3:26; ( ( the Sorts of U1 * (the_arity_of o)) . e = the Sorts of U1 . ((the_arity_of o) . e) & ( the Sorts of U2 * (the_arity_of o)) . e = the Sorts of U2 . ((the_arity_of o) . e) ) by A17, FUNCT_1:13; hence ( the Sorts of U1 * (the_arity_of o)) . e = dom Foe by A18, FUNCT_2:def_1 .= proj1 Foe .= proj1 ((F * (the_arity_of o)) . e) by A17, FUNCT_1:13 ; ::_thesis: verum end; then A19: the Sorts of U1 * (the_arity_of o) = doms (F * (the_arity_of o)) by A7, FUNCT_6:def_2; hereby ::_thesis: ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) assume u = F # x ; ::_thesis: for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) then A20: u = (Frege (F * (the_arity_of o))) . x by A2, A3, Def5; let n be Nat; ::_thesis: ( n in dom f implies u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) assume A21: n in dom f ; ::_thesis: u . n = (F . ((the_arity_of o) /. n)) . (f . n) then (the_arity_of o) . n in the carrier of S by A15, FINSEQ_2:11; then (the_arity_of o) . n in dom F by PARTFUN1:def_2; then A22: n in dom (F * (the_arity_of o)) by A15, A21, FUNCT_1:11; then A23: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:12 .= F . ((the_arity_of o) /. n) by A15, A21, PARTFUN1:def_6 ; thus u . n = ((F * (the_arity_of o)) .. f) . n by A1, A2, A14, A19, A20, PRALG_2:def_2 .= (F . ((the_arity_of o) /. n)) . (f . n) by A22, A23, PRALG_1:def_17 ; ::_thesis: verum end; F # x is Element of product ( the Sorts of U2 * (the_arity_of o)) by PRALG_2:3; then reconsider g = F # x as Function ; A24: rng (the_arity_of o) c= dom F by A4, PARTFUN1:def_2; assume A25: for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ; ::_thesis: u = F # x A26: now__::_thesis:_for_e_being_set_st_e_in_dom_f_holds_ u_._e_=_g_._e let e be set ; ::_thesis: ( e in dom f implies u . e = g . e ) assume A27: e in dom f ; ::_thesis: u . e = g . e then reconsider n = e as Nat by A15; (the_arity_of o) . n in the carrier of S by A15, A27, FINSEQ_2:11; then (the_arity_of o) . n in dom F by PARTFUN1:def_2; then A28: n in dom (F * (the_arity_of o)) by A15, A27, FUNCT_1:11; then A29: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:12 .= F . ((the_arity_of o) /. n) by A15, A27, PARTFUN1:def_6 ; thus u . e = (F . ((the_arity_of o) /. n)) . (f . n) by A25, A27 .= ((F * (the_arity_of o)) .. f) . n by A28, A29, PRALG_1:def_17 .= g . e by A1, A2, A14, A19, A6, PRALG_2:def_2 ; ::_thesis: verum end; F # x = (F * (the_arity_of o)) .. f by A1, A2, A14, A19, A6, PRALG_2:def_2; then dom g = dom (F * (the_arity_of o)) by PRALG_1:def_17 .= dom f by A15, A24, RELAT_1:27 ; hence u = F # x by A15, A16, A26, FUNCT_1:2; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1, U2 be non-empty MSAlgebra over S; let o be OperSymbol of S; let F be ManySortedFunction of U1,U2; let x be Element of Args (o,U1); redefine func F # x means :Def6: :: MSUALG_3:def 6 for n being Nat st n in dom x holds it . n = (F . ((the_arity_of o) /. n)) . (x . n); compatibility for b1 being Element of Args (o,U2) holds ( b1 = F # x iff for n being Nat st n in dom x holds b1 . n = (F . ((the_arity_of o) /. n)) . (x . n) ) by Lm1; end; :: deftheorem Def6 defines # MSUALG_3:def_6_:_ for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for o being OperSymbol of S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for b7 being Element of Args (o,U2) holds ( b7 = F # x iff for n being Nat st n in dom x holds b7 . n = (F . ((the_arity_of o) /. n)) . (x . n) ); theorem Th7: :: MSUALG_3:7 for S being non empty non void ManySortedSign for o being OperSymbol of S for U1 being MSAlgebra over S st Args (o,U1) <> {} holds for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x proofend; theorem Th8: :: MSUALG_3:8 for S being non empty non void ManySortedSign for o being OperSymbol of S for U1, U2, U3 being non-empty MSAlgebra over S for H1 being ManySortedFunction of U1,U2 for H2 being ManySortedFunction of U2,U3 for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x) proofend; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; let F be ManySortedFunction of U1,U2; predF is_homomorphism U1,U2 means :Def7: :: MSUALG_3:def 7 for o being OperSymbol of S st Args (o,U1) <> {} holds for x being Element of Args (o,U1) holds (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x); end; :: deftheorem Def7 defines is_homomorphism MSUALG_3:def_7_:_ for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for F being ManySortedFunction of U1,U2 holds ( F is_homomorphism U1,U2 iff for o being OperSymbol of S st Args (o,U1) <> {} holds for x being Element of Args (o,U1) holds (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) ); theorem Th9: :: MSUALG_3:9 for S being non empty non void ManySortedSign for U1 being MSAlgebra over S holds id the Sorts of U1 is_homomorphism U1,U1 proofend; theorem Th10: :: MSUALG_3:10 for S being non empty non void ManySortedSign for U1, U2, U3 being non-empty MSAlgebra over S for H1 being ManySortedFunction of U1,U2 for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds H2 ** H1 is_homomorphism U1,U3 proofend; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; let F be ManySortedFunction of U1,U2; predF is_epimorphism U1,U2 means :Def8: :: MSUALG_3:def 8 ( F is_homomorphism U1,U2 & F is "onto" ); end; :: deftheorem Def8 defines is_epimorphism MSUALG_3:def_8_:_ for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for F being ManySortedFunction of U1,U2 holds ( F is_epimorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" ) ); theorem Th11: :: MSUALG_3:11 for S being non empty non void ManySortedSign for U1, U2, U3 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds G ** F is_epimorphism U1,U3 proofend; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; let F be ManySortedFunction of U1,U2; predF is_monomorphism U1,U2 means :Def9: :: MSUALG_3:def 9 ( F is_homomorphism U1,U2 & F is "1-1" ); end; :: deftheorem Def9 defines is_monomorphism MSUALG_3:def_9_:_ for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for F being ManySortedFunction of U1,U2 holds ( F is_monomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "1-1" ) ); theorem Th12: :: MSUALG_3:12 for S being non empty non void ManySortedSign for U1, U2, U3 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds G ** F is_monomorphism U1,U3 proofend; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; let F be ManySortedFunction of U1,U2; predF is_isomorphism U1,U2 means :Def10: :: MSUALG_3:def 10 ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ); end; :: deftheorem Def10 defines is_isomorphism MSUALG_3:def_10_:_ for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for F being ManySortedFunction of U1,U2 holds ( F is_isomorphism U1,U2 iff ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ) ); theorem Th13: :: MSUALG_3:13 for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for F being ManySortedFunction of U1,U2 holds ( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ) proofend; Lm2: for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for H being ManySortedFunction of U1,U2 st H is_isomorphism U1,U2 holds H "" is_homomorphism U2,U1 proofend; theorem Th14: :: MSUALG_3:14 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for H being ManySortedFunction of U1,U2 for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds H1 is_isomorphism U2,U1 proofend; theorem Th15: :: MSUALG_3:15 for S being non empty non void ManySortedSign for U1, U2, U3 being non-empty MSAlgebra over S for H being ManySortedFunction of U1,U2 for H1 being ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds H1 ** H is_isomorphism U1,U3 proofend; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; predU1,U2 are_isomorphic means :Def11: :: MSUALG_3:def 11 ex F being ManySortedFunction of U1,U2 st F is_isomorphism U1,U2; end; :: deftheorem Def11 defines are_isomorphic MSUALG_3:def_11_:_ for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S holds ( U1,U2 are_isomorphic iff ex F being ManySortedFunction of U1,U2 st F is_isomorphism U1,U2 ); theorem Th16: :: MSUALG_3:16 for S being non empty non void ManySortedSign for U1 being MSAlgebra over S holds ( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic ) proofend; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; :: original:are_isomorphic redefine predU1,U2 are_isomorphic ; reflexivity for U1 being MSAlgebra over S holds (S,b1,b1) by Th16; end; theorem :: MSUALG_3:17 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S st U1,U2 are_isomorphic holds U2,U1 are_isomorphic proofend; theorem :: MSUALG_3:18 for S being non empty non void ManySortedSign for U1, U2, U3 being non-empty MSAlgebra over S st U1,U2 are_isomorphic & U2,U3 are_isomorphic holds U1,U3 are_isomorphic proofend; definition let S be non empty non void ManySortedSign ; let U1, U2 be non-empty MSAlgebra over S; let F be ManySortedFunction of U1,U2; assume A1: F is_homomorphism U1,U2 ; func Image F -> strict non-empty MSSubAlgebra of U2 means :Def12: :: MSUALG_3:def 12 the Sorts of it = F .:.: the Sorts of U1; existence ex b1 being strict non-empty MSSubAlgebra of U2 st the Sorts of b1 = F .:.: the Sorts of U1 proofend; uniqueness for b1, b2 being strict non-empty MSSubAlgebra of U2 st the Sorts of b1 = F .:.: the Sorts of U1 & the Sorts of b2 = F .:.: the Sorts of U1 holds b1 = b2 by MSUALG_2:9; end; :: deftheorem Def12 defines Image MSUALG_3:def_12_:_ for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds for b5 being strict non-empty MSSubAlgebra of U2 holds ( b5 = Image F iff the Sorts of b5 = F .:.: the Sorts of U1 ); theorem :: MSUALG_3:19 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds ( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ) proofend; Lm3: for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds F is ManySortedFunction of U1,(Image F) proofend; theorem Th20: :: MSUALG_3:20 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds G is_epimorphism U1, Image F proofend; theorem :: MSUALG_3:21 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds ex G being ManySortedFunction of U1,(Image F) st ( F = G & G is_epimorphism U1, Image F ) proofend; Lm4: for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for U3 being non-empty MSSubAlgebra of U2 for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds F is_homomorphism U1,U2 proofend; theorem Th22: :: MSUALG_3:22 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for U2 being non-empty MSSubAlgebra of U1 for G being ManySortedFunction of U2,U1 st G = id the Sorts of U2 holds G is_monomorphism U2,U1 proofend; theorem :: MSUALG_3:23 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st ( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 ) proofend; theorem :: MSUALG_3:24 for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for o being OperSymbol of S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds ( u = F # x iff for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) by Lm1;