:: CAT_1 semantic presentation begin definition attrc1 is strict ; struct CatStr -> MultiGraphStruct ; aggrCatStr(# carrier, carrier', Source, Target, Comp #) -> CatStr ; sel Comp c1 -> PartFunc of [: the carrier' of c1, the carrier' of c1:], the carrier' of c1; end; definition let C be CatStr ; mode Object of C is Element of C; mode Morphism of C is Element of the carrier' of C; end; registration cluster non empty non void for CatStr ; existence ex b1 being CatStr st ( not b1 is void & not b1 is empty ) proof take CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1) #) ; ::_thesis: ( not CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1) #) is void & not CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1) #) is empty ) thus ( not CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1) #) is void & not CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1) #) is empty ) ; ::_thesis: verum end; end; definition let C be CatStr ; let f, g be Morphism of C; assume A1: [g,f] in dom the Comp of C ; funcg (*) f -> Morphism of C equals :Def1: :: CAT_1:def 1 the Comp of C . (g,f); coherence the Comp of C . (g,f) is Morphism of C by A1, PARTFUN1:4; end; :: deftheorem Def1 defines (*) CAT_1:def_1_:_ for C being CatStr for f, g being Morphism of C st [g,f] in dom the Comp of C holds g (*) f = the Comp of C . (g,f); definition canceled; canceled; let C be non empty non void CatStr ; let a, b be Object of C; func Hom (a,b) -> Subset of the carrier' of C equals :: CAT_1:def 4 { f where f is Morphism of C : ( dom f = a & cod f = b ) } ; correctness coherence { f where f is Morphism of C : ( dom f = a & cod f = b ) } is Subset of the carrier' of C; proof set M = { f where f is Morphism of C : ( dom f = a & cod f = b ) } ; { f where f is Morphism of C : ( dom f = a & cod f = b ) } c= the carrier' of C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { f where f is Morphism of C : ( dom f = a & cod f = b ) } or x in the carrier' of C ) assume x in { f where f is Morphism of C : ( dom f = a & cod f = b ) } ; ::_thesis: x in the carrier' of C then ex f being Morphism of C st ( x = f & dom f = a & cod f = b ) ; hence x in the carrier' of C ; ::_thesis: verum end; hence { f where f is Morphism of C : ( dom f = a & cod f = b ) } is Subset of the carrier' of C ; ::_thesis: verum end; end; :: deftheorem CAT_1:def_2_:_ canceled; :: deftheorem CAT_1:def_3_:_ canceled; :: deftheorem defines Hom CAT_1:def_4_:_ for C being non empty non void CatStr for a, b being Object of C holds Hom (a,b) = { f where f is Morphism of C : ( dom f = a & cod f = b ) } ; theorem Th1: :: CAT_1:1 for C being non empty non void CatStr for f being Morphism of C for a, b being Object of C holds ( f in Hom (a,b) iff ( dom f = a & cod f = b ) ) proof let C be non empty non void CatStr ; ::_thesis: for f being Morphism of C for a, b being Object of C holds ( f in Hom (a,b) iff ( dom f = a & cod f = b ) ) let f be Morphism of C; ::_thesis: for a, b being Object of C holds ( f in Hom (a,b) iff ( dom f = a & cod f = b ) ) let a, b be Object of C; ::_thesis: ( f in Hom (a,b) iff ( dom f = a & cod f = b ) ) thus ( f in Hom (a,b) implies ( dom f = a & cod f = b ) ) ::_thesis: ( dom f = a & cod f = b implies f in Hom (a,b) ) proof assume f in Hom (a,b) ; ::_thesis: ( dom f = a & cod f = b ) then ex g being Morphism of C st ( f = g & dom g = a & cod g = b ) ; hence ( dom f = a & cod f = b ) ; ::_thesis: verum end; thus ( dom f = a & cod f = b implies f in Hom (a,b) ) ; ::_thesis: verum end; theorem :: CAT_1:2 for C being non empty non void CatStr for f being Morphism of C holds Hom ((dom f),(cod f)) <> {} by Th1; definition let C be non empty non void CatStr ; let a, b be Object of C; assume A1: Hom (a,b) <> {} ; mode Morphism of a,b -> Morphism of C means :Def4: :: CAT_1:def 5 it in Hom (a,b); existence ex b1 being Morphism of C st b1 in Hom (a,b) by A1, SUBSET_1:4; end; :: deftheorem Def4 defines Morphism CAT_1:def_5_:_ for C being non empty non void CatStr for a, b being Object of C st Hom (a,b) <> {} holds for b4 being Morphism of C holds ( b4 is Morphism of a,b iff b4 in Hom (a,b) ); theorem :: CAT_1:3 canceled; theorem Th4: :: CAT_1:4 for C being non empty non void CatStr for f being Morphism of C holds f is Morphism of dom f, cod f proof let C be non empty non void CatStr ; ::_thesis: for f being Morphism of C holds f is Morphism of dom f, cod f let f be Morphism of C; ::_thesis: f is Morphism of dom f, cod f f in Hom ((dom f),(cod f)) ; hence f is Morphism of dom f, cod f by Def4; ::_thesis: verum end; theorem Th5: :: CAT_1:5 for C being non empty non void CatStr for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} holds ( dom f = a & cod f = b ) proof let C be non empty non void CatStr ; ::_thesis: for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} holds ( dom f = a & cod f = b ) let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds ( dom f = a & cod f = b ) let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies ( dom f = a & cod f = b ) ) assume Hom (a,b) <> {} ; ::_thesis: ( dom f = a & cod f = b ) then f in Hom (a,b) by Def4; hence ( dom f = a & cod f = b ) by Th1; ::_thesis: verum end; theorem :: CAT_1:6 for C being non empty non void CatStr for a, b, c, d being Object of C for f being Morphism of a,b for h being Morphism of c,d st Hom (a,b) <> {} & Hom (c,d) <> {} & f = h holds ( a = c & b = d ) proof let C be non empty non void CatStr ; ::_thesis: for a, b, c, d being Object of C for f being Morphism of a,b for h being Morphism of c,d st Hom (a,b) <> {} & Hom (c,d) <> {} & f = h holds ( a = c & b = d ) let a, b, c, d be Object of C; ::_thesis: for f being Morphism of a,b for h being Morphism of c,d st Hom (a,b) <> {} & Hom (c,d) <> {} & f = h holds ( a = c & b = d ) let f be Morphism of a,b; ::_thesis: for h being Morphism of c,d st Hom (a,b) <> {} & Hom (c,d) <> {} & f = h holds ( a = c & b = d ) let h be Morphism of c,d; ::_thesis: ( Hom (a,b) <> {} & Hom (c,d) <> {} & f = h implies ( a = c & b = d ) ) assume that A1: Hom (a,b) <> {} and A2: Hom (c,d) <> {} ; ::_thesis: ( not f = h or ( a = c & b = d ) ) ( dom f = a & cod f = b ) by A1, Th5; hence ( not f = h or ( a = c & b = d ) ) by A2, Th5; ::_thesis: verum end; theorem Th7: :: CAT_1:7 for C being non empty non void CatStr for a, b being Object of C for f being Morphism of a,b st Hom (a,b) = {f} holds for g being Morphism of a,b holds f = g proof let C be non empty non void CatStr ; ::_thesis: for a, b being Object of C for f being Morphism of a,b st Hom (a,b) = {f} holds for g being Morphism of a,b holds f = g let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) = {f} holds for g being Morphism of a,b holds f = g let f be Morphism of a,b; ::_thesis: ( Hom (a,b) = {f} implies for g being Morphism of a,b holds f = g ) assume A1: Hom (a,b) = {f} ; ::_thesis: for g being Morphism of a,b holds f = g let g be Morphism of a,b; ::_thesis: f = g g in {f} by A1, Def4; hence f = g by TARSKI:def_1; ::_thesis: verum end; theorem Th8: :: CAT_1:8 for C being non empty non void CatStr for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds Hom (a,b) = {f} proof let C be non empty non void CatStr ; ::_thesis: for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds Hom (a,b) = {f} let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds Hom (a,b) = {f} let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) implies Hom (a,b) = {f} ) assume that A1: Hom (a,b) <> {} and A2: for g being Morphism of a,b holds f = g ; ::_thesis: Hom (a,b) = {f} for x being set holds ( x in Hom (a,b) iff x = f ) proof let x be set ; ::_thesis: ( x in Hom (a,b) iff x = f ) thus ( x in Hom (a,b) implies x = f ) ::_thesis: ( x = f implies x in Hom (a,b) ) proof assume x in Hom (a,b) ; ::_thesis: x = f then consider g being Morphism of C such that A3: x = g and A4: ( dom g = a & cod g = b ) ; g is Morphism of a,b by A4, Th4; hence x = f by A2, A3; ::_thesis: verum end; thus ( x = f implies x in Hom (a,b) ) by A1, Def4; ::_thesis: verum end; hence Hom (a,b) = {f} by TARSKI:def_1; ::_thesis: verum end; theorem :: CAT_1:9 for C being non empty non void CatStr for a, b, c, d being Object of C for f being Morphism of a,b st Hom (a,b), Hom (c,d) are_equipotent & Hom (a,b) = {f} holds ex h being Morphism of c,d st Hom (c,d) = {h} proof let C be non empty non void CatStr ; ::_thesis: for a, b, c, d being Object of C for f being Morphism of a,b st Hom (a,b), Hom (c,d) are_equipotent & Hom (a,b) = {f} holds ex h being Morphism of c,d st Hom (c,d) = {h} let a, b, c, d be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b), Hom (c,d) are_equipotent & Hom (a,b) = {f} holds ex h being Morphism of c,d st Hom (c,d) = {h} let f be Morphism of a,b; ::_thesis: ( Hom (a,b), Hom (c,d) are_equipotent & Hom (a,b) = {f} implies ex h being Morphism of c,d st Hom (c,d) = {h} ) assume Hom (a,b), Hom (c,d) are_equipotent ; ::_thesis: ( not Hom (a,b) = {f} or ex h being Morphism of c,d st Hom (c,d) = {h} ) then consider F being Function such that F is one-to-one and A1: ( dom F = Hom (a,b) & rng F = Hom (c,d) ) by WELLORD2:def_4; assume Hom (a,b) = {f} ; ::_thesis: ex h being Morphism of c,d st Hom (c,d) = {h} then A2: Hom (c,d) = {(F . f)} by A1, FUNCT_1:4; then F . f in Hom (c,d) by TARSKI:def_1; then F . f is Morphism of c,d by Def4; hence ex h being Morphism of c,d st Hom (c,d) = {h} by A2; ::_thesis: verum end; definition let C be non empty non void CatStr ; attrC is Category-like means :Def5a: :: CAT_1:def 6 for f, g being Morphism of C holds ( [g,f] in dom the Comp of C iff dom g = cod f ); attrC is transitive means :Def5b: :: CAT_1:def 7 for f, g being Morphism of C st dom g = cod f holds ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ); attrC is associative means :Def5c: :: CAT_1:def 8 for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds h (*) (g (*) f) = (h (*) g) (*) f; attrC is reflexive means :Def5d: :: CAT_1:def 9 for b being Element of C holds Hom (b,b) <> {} ; attrC is with_identities means :Def5e: :: CAT_1:def 10 for a being Element of C ex i being Morphism of a,a st for b being Element of C holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ); end; :: deftheorem Def5a defines Category-like CAT_1:def_6_:_ for C being non empty non void CatStr holds ( C is Category-like iff for f, g being Morphism of C holds ( [g,f] in dom the Comp of C iff dom g = cod f ) ); :: deftheorem Def5b defines transitive CAT_1:def_7_:_ for C being non empty non void CatStr holds ( C is transitive iff for f, g being Morphism of C st dom g = cod f holds ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) ); :: deftheorem Def5c defines associative CAT_1:def_8_:_ for C being non empty non void CatStr holds ( C is associative iff for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds h (*) (g (*) f) = (h (*) g) (*) f ); :: deftheorem Def5d defines reflexive CAT_1:def_9_:_ for C being non empty non void CatStr holds ( C is reflexive iff for b being Element of C holds Hom (b,b) <> {} ); :: deftheorem Def5e defines with_identities CAT_1:def_10_:_ for C being non empty non void CatStr holds ( C is with_identities iff for a being Element of C ex i being Morphism of a,a st for b being Element of C holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) ); definition let o, m be set ; func 1Cat (o,m) -> strict CatStr equals :: CAT_1:def 11 CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #); correctness coherence CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #) is strict CatStr ; ; end; :: deftheorem defines 1Cat CAT_1:def_11_:_ for o, m being set holds 1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #); registration let o, m be set ; cluster 1Cat (o,m) -> non empty trivial non void trivial' strict ; coherence ( not 1Cat (o,m) is empty & 1Cat (o,m) is trivial & not 1Cat (o,m) is void & 1Cat (o,m) is trivial' ) ; end; registration cluster non empty trivial non void -> non empty non void transitive reflexive for CatStr ; coherence for b1 being non empty non void CatStr st not b1 is empty & b1 is trivial holds ( b1 is transitive & b1 is reflexive ) proof let C be non empty non void CatStr ; ::_thesis: ( not C is empty & C is trivial implies ( C is transitive & C is reflexive ) ) assume Z: ( not C is empty & C is trivial ) ; ::_thesis: ( C is transitive & C is reflexive ) thus for f, g being Morphism of C st dom g = cod f holds ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by Z, ZFMISC_1:def_10; :: according to CAT_1:def_7 ::_thesis: C is reflexive let b be Element of C; :: according to CAT_1:def_9 ::_thesis: Hom (b,b) <> {} set i = the Morphism of C; ( cod the Morphism of C = b & dom the Morphism of C = b ) by Z, ZFMISC_1:def_10; hence Hom (b,b) <> {} by Th1; ::_thesis: verum end; end; registration cluster non empty non void trivial' -> non empty non void associative with_identities for CatStr ; coherence for b1 being non empty non void CatStr st not b1 is void & b1 is trivial' holds ( b1 is associative & b1 is with_identities ) proof let C be non empty non void CatStr ; ::_thesis: ( not C is void & C is trivial' implies ( C is associative & C is with_identities ) ) assume Z: ( not C is void & C is trivial' ) ; ::_thesis: ( C is associative & C is with_identities ) thus for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds h (*) (g (*) f) = (h (*) g) (*) f by Z, ZFMISC_1:def_10; :: according to CAT_1:def_8 ::_thesis: C is with_identities let a be Element of C; :: according to CAT_1:def_10 ::_thesis: ex i being Morphism of a,a st for b being Element of C holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) take i = the Morphism of a,a; ::_thesis: for b being Element of C holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let b be Element of C; ::_thesis: ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) by Z, ZFMISC_1:def_10; ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) by Z, ZFMISC_1:def_10; ::_thesis: verum end; end; registration let o, m be set ; cluster 1Cat (o,m) -> strict Category-like ; coherence 1Cat (o,m) is Category-like proof let f, g be Morphism of (1Cat (o,m)); :: according to CAT_1:def_6 ::_thesis: ( [g,f] in dom the Comp of (1Cat (o,m)) iff dom g = cod f ) thus ( [g,f] in dom the Comp of (1Cat (o,m)) implies dom g = cod f ) by ZFMISC_1:def_10; ::_thesis: ( dom g = cod f implies [g,f] in dom the Comp of (1Cat (o,m)) ) assume dom g = cod f ; ::_thesis: [g,f] in dom the Comp of (1Cat (o,m)) A2: dom the Comp of (1Cat (o,m)) = {[m,m]} by FUNCOP_1:13; ( f = m & g = m ) by TARSKI:def_1; hence [g,f] in dom the Comp of (1Cat (o,m)) by A2, TARSKI:def_1; ::_thesis: verum end; end; registration cluster non empty non void V59() strict Category-like transitive associative reflexive with_identities for CatStr ; existence ex b1 being non empty non void CatStr st ( b1 is reflexive & b1 is transitive & b1 is associative & b1 is with_identities & b1 is Category-like & not b1 is void & not b1 is empty & b1 is strict ) proof take 1Cat (0,0) ; ::_thesis: ( 1Cat (0,0) is reflexive & 1Cat (0,0) is transitive & 1Cat (0,0) is associative & 1Cat (0,0) is with_identities & 1Cat (0,0) is Category-like & not 1Cat (0,0) is void & not 1Cat (0,0) is empty & 1Cat (0,0) is strict ) thus ( 1Cat (0,0) is reflexive & 1Cat (0,0) is transitive & 1Cat (0,0) is associative & 1Cat (0,0) is with_identities & 1Cat (0,0) is Category-like & not 1Cat (0,0) is void & not 1Cat (0,0) is empty & 1Cat (0,0) is strict ) ; ::_thesis: verum end; end; definition mode Category is non empty non void Category-like transitive associative reflexive with_identities CatStr ; end; registration let C be non empty non void reflexive CatStr ; let a be Object of C; cluster Hom (a,a) -> non empty ; coherence not Hom (a,a) is empty by Def5d; end; definition let C be non empty non void reflexive with_identities CatStr ; let a be Object of C; func id a -> Morphism of a,a means :Defid: :: CAT_1:def 12 for b being Object of C holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) it = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds it (*) f = f ) ); existence ex b1 being Morphism of a,a st for b being Object of C holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b1 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b1 (*) f = f ) ) by Def5e; uniqueness for b1, b2 being Morphism of a,a st ( for b being Object of C holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b1 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b1 (*) f = f ) ) ) & ( for b being Object of C holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b2 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b2 (*) f = f ) ) ) holds b1 = b2 proof let m1, m2 be Morphism of a,a; ::_thesis: ( ( for b being Object of C holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m1 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m1 (*) f = f ) ) ) & ( for b being Object of C holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m2 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m2 (*) f = f ) ) ) implies m1 = m2 ) assume that Z1: for b being Object of C holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m1 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m1 (*) f = f ) ) and Z2: for b being Object of C holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m2 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m2 (*) f = f ) ) ; ::_thesis: m1 = m2 A: Hom (a,a) <> {} ; hence m1 = m1 (*) m2 by Z2 .= m2 by A, Z1 ; ::_thesis: verum end; end; :: deftheorem Defid defines id CAT_1:def_12_:_ for C being non empty non void reflexive with_identities CatStr for a being Object of C for b3 being Morphism of a,a holds ( b3 = id a iff for b being Object of C holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b3 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b3 (*) f = f ) ) ); theorem :: CAT_1:10 canceled; theorem Th11: :: CAT_1:11 for o, m being set for a, b being Object of (1Cat (o,m)) for f being Morphism of (1Cat (o,m)) holds f in Hom (a,b) proof let o, m be set ; ::_thesis: for a, b being Object of (1Cat (o,m)) for f being Morphism of (1Cat (o,m)) holds f in Hom (a,b) let a, b be Object of (1Cat (o,m)); ::_thesis: for f being Morphism of (1Cat (o,m)) holds f in Hom (a,b) let f be Morphism of (1Cat (o,m)); ::_thesis: f in Hom (a,b) dom f = o by TARSKI:def_1; then ( dom f = a & cod f = b ) by TARSKI:def_1; hence f in Hom (a,b) ; ::_thesis: verum end; theorem :: CAT_1:12 for o, m being set for a, b being Object of (1Cat (o,m)) for f being Morphism of (1Cat (o,m)) holds f is Morphism of a,b proof let o, m be set ; ::_thesis: for a, b being Object of (1Cat (o,m)) for f being Morphism of (1Cat (o,m)) holds f is Morphism of a,b let a, b be Object of (1Cat (o,m)); ::_thesis: for f being Morphism of (1Cat (o,m)) holds f is Morphism of a,b let f be Morphism of (1Cat (o,m)); ::_thesis: f is Morphism of a,b f in Hom (a,b) by Th11; hence f is Morphism of a,b by Def4; ::_thesis: verum end; theorem :: CAT_1:13 for o, m being set for a, b being Object of (1Cat (o,m)) holds Hom (a,b) <> {} by Th11; theorem :: CAT_1:14 for o, m being set for a, b, c, d being Object of (1Cat (o,m)) for f being Morphism of a,b for g being Morphism of c,d holds f = g proof let o, m be set ; ::_thesis: for a, b, c, d being Object of (1Cat (o,m)) for f being Morphism of a,b for g being Morphism of c,d holds f = g let a, b, c, d be Object of (1Cat (o,m)); ::_thesis: for f being Morphism of a,b for g being Morphism of c,d holds f = g let f be Morphism of a,b; ::_thesis: for g being Morphism of c,d holds f = g let g be Morphism of c,d; ::_thesis: f = g f = m by TARSKI:def_1; hence f = g by TARSKI:def_1; ::_thesis: verum end; theorem :: CAT_1:15 for C being Category for g, f being Morphism of C holds ( dom g = cod f iff [g,f] in dom the Comp of C ) by Def5a; theorem Th16: :: CAT_1:16 for C being Category for g, f being Morphism of C st dom g = cod f holds g (*) f = the Comp of C . (g,f) proof let C be Category; ::_thesis: for g, f being Morphism of C st dom g = cod f holds g (*) f = the Comp of C . (g,f) let g, f be Morphism of C; ::_thesis: ( dom g = cod f implies g (*) f = the Comp of C . (g,f) ) assume dom g = cod f ; ::_thesis: g (*) f = the Comp of C . (g,f) then [g,f] in dom the Comp of C by Def5a; hence g (*) f = the Comp of C . (g,f) by Def1; ::_thesis: verum end; theorem :: CAT_1:17 for C being Category for f, g being Morphism of C st dom g = cod f holds ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by Def5b; theorem :: CAT_1:18 for C being Category for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds h (*) (g (*) f) = (h (*) g) (*) f by Def5c; theorem :: CAT_1:19 canceled; theorem :: CAT_1:20 canceled; theorem :: CAT_1:21 for C being Category for b being Object of C for f being Morphism of C st cod f = b holds (id b) (*) f = f proof let C be Category; ::_thesis: for b being Object of C for f being Morphism of C st cod f = b holds (id b) (*) f = f let b be Object of C; ::_thesis: for f being Morphism of C st cod f = b holds (id b) (*) f = f let f be Morphism of C; ::_thesis: ( cod f = b implies (id b) (*) f = f ) assume Z: cod f = b ; ::_thesis: (id b) (*) f = f then reconsider ff = f as Morphism of dom f,b by Th4; Hom ((dom f),b) <> {} by Z, Th1; then (id b) (*) ff = ff by Defid; hence (id b) (*) f = f ; ::_thesis: verum end; theorem :: CAT_1:22 for C being Category for b being Object of C for g being Morphism of C st dom g = b holds g (*) (id b) = g proof let C be Category; ::_thesis: for b being Object of C for g being Morphism of C st dom g = b holds g (*) (id b) = g let b be Object of C; ::_thesis: for g being Morphism of C st dom g = b holds g (*) (id b) = g let f be Morphism of C; ::_thesis: ( dom f = b implies f (*) (id b) = f ) assume Z: dom f = b ; ::_thesis: f (*) (id b) = f then reconsider ff = f as Morphism of b, cod f by Th4; Hom (b,(cod f)) <> {} by Z, Th1; then ff (*) (id b) = ff by Defid; hence f (*) (id b) = f ; ::_thesis: verum end; theorem Th23: :: CAT_1:23 for C being Category for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds g (*) f in Hom (a,c) proof let C be Category; ::_thesis: for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds g (*) f in Hom (a,c) let a, b, c be Object of C; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds g (*) f in Hom (a,c) let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds g (*) f in Hom (a,c) let g be Morphism of b,c; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies g (*) f in Hom (a,c) ) assume that A1: Hom (a,b) <> {} and A2: Hom (b,c) <> {} ; ::_thesis: g (*) f in Hom (a,c) A3: f in Hom (a,b) by A1, Def4; then A4: cod f = b by Th1; A5: g in Hom (b,c) by A2, Def4; then A6: dom g = b by Th1; cod g = c by A5, Th1; then A7: cod (g (*) f) = c by A6, A4, Def5b; dom f = a by A3, Th1; then dom (g (*) f) = a by A6, A4, Def5b; hence g (*) f in Hom (a,c) by A7; ::_thesis: verum end; definition let C be Category; let a, b, c be Object of C; let f be Morphism of a,b; let g be Morphism of b,c; assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; funcg * f -> Morphism of a,c equals :Def10: :: CAT_1:def 13 g (*) f; correctness coherence g (*) f is Morphism of a,c; proof g (*) f in Hom (a,c) by A1, Th23; hence g (*) f is Morphism of a,c by Def4; ::_thesis: verum end; end; :: deftheorem Def10 defines * CAT_1:def_13_:_ for C being Category for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds g * f = g (*) f; theorem :: CAT_1:24 for C being Category for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds Hom (a,c) <> {} by Th23; theorem Th25: :: CAT_1:25 for C being Category for a, b, c, d being Object of C for f being Morphism of a,b for g being Morphism of b,c for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds (h * g) * f = h * (g * f) proof let C be Category; ::_thesis: for a, b, c, d being Object of C for f being Morphism of a,b for g being Morphism of b,c for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds (h * g) * f = h * (g * f) let a, b, c, d be Object of C; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds (h * g) * f = h * (g * f) let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds (h * g) * f = h * (g * f) let g be Morphism of b,c; ::_thesis: for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds (h * g) * f = h * (g * f) let h be Morphism of c,d; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} implies (h * g) * f = h * (g * f) ) assume that A1: Hom (a,b) <> {} and A2: Hom (b,c) <> {} and A3: Hom (c,d) <> {} ; ::_thesis: (h * g) * f = h * (g * f) A4: Hom (a,c) <> {} by A1, A2, Th23; h in Hom (c,d) by A3, Def4; then A5: dom h = c by Th1; g in Hom (b,c) by A2, Def4; then A6: ( cod g = c & dom g = b ) by Th1; reconsider hh = h as Morphism of C ; reconsider gg = g as Morphism of C ; reconsider ff = f as Morphism of C ; f in Hom (a,b) by A1, Def4; then A7: cod f = b by Th1; Hom (b,d) <> {} by A2, A3, Th23; hence (h * g) * f = (h * g) (*) ff by A1, Def10 .= (hh (*) gg) (*) ff by A2, A3, Def10 .= hh (*) (gg (*) ff) by A5, A6, A7, Def5c .= hh (*) (g * f) by A1, A2, Def10 .= h * (g * f) by A3, A4, Def10 ; ::_thesis: verum end; theorem :: CAT_1:26 canceled; theorem :: CAT_1:27 for C being Category for a being Object of C holds id a in Hom (a,a) by Def4; theorem Th28: :: CAT_1:28 for C being Category for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} holds (id b) * f = f proof let C be Category; ::_thesis: for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} holds (id b) * f = f let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds (id b) * f = f let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies (id b) * f = f ) assume A1: Hom (a,b) <> {} ; ::_thesis: (id b) * f = f A2: (id b) (*) f = f by A1, Defid; Hom (b,b) <> {} ; hence (id b) * f = f by A1, A2, Def10; ::_thesis: verum end; theorem Th29: :: CAT_1:29 for C being Category for b, c being Object of C for g being Morphism of b,c st Hom (b,c) <> {} holds g * (id b) = g proof let C be Category; ::_thesis: for b, c being Object of C for g being Morphism of b,c st Hom (b,c) <> {} holds g * (id b) = g let b, c be Object of C; ::_thesis: for g being Morphism of b,c st Hom (b,c) <> {} holds g * (id b) = g let g be Morphism of b,c; ::_thesis: ( Hom (b,c) <> {} implies g * (id b) = g ) assume A1: Hom (b,c) <> {} ; ::_thesis: g * (id b) = g A2: g (*) (id b) = g by A1, Defid; Hom (b,b) <> {} ; hence g * (id b) = g by A1, A2, Def10; ::_thesis: verum end; registration let C be Category; let a be Object of C; let f be Morphism of a,a; X: Hom (a,a) <> {} ; reducef * (id a) to f; reducibility f * (id a) = f by X, Th29; reduce(id a) * f to f; reducibility (id a) * f = f by X, Th28; end; theorem :: CAT_1:30 for C being Category for a being Object of C holds (id a) * (id a) = id a ; definition let C be Category; let b, c be Object of C; let g be Morphism of b,c; attrg is monic means :Defm: :: CAT_1:def 14 ( Hom (b,c) <> {} & ( for a being Object of C st Hom (a,b) <> {} holds for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds f1 = f2 ) ); end; :: deftheorem Defm defines monic CAT_1:def_14_:_ for C being Category for b, c being Object of C for g being Morphism of b,c holds ( g is monic iff ( Hom (b,c) <> {} & ( for a being Object of C st Hom (a,b) <> {} holds for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds f1 = f2 ) ) ); definition let C be Category; let a, b be Object of C; let f be Morphism of a,b; attrf is epi means :Defe: :: CAT_1:def 15 ( Hom (a,b) <> {} & ( for c being Object of C st Hom (b,c) <> {} holds for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds g1 = g2 ) ); end; :: deftheorem Defe defines epi CAT_1:def_15_:_ for C being Category for a, b being Object of C for f being Morphism of a,b holds ( f is epi iff ( Hom (a,b) <> {} & ( for c being Object of C st Hom (b,c) <> {} holds for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds g1 = g2 ) ) ); definition let C be Category; let a, b be Object of C; let f be Morphism of a,b; attrf is invertible means :Dfi: :: CAT_1:def 16 ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) ); end; :: deftheorem Dfi defines invertible CAT_1:def_16_:_ for C being Category for a, b being Object of C for f being Morphism of a,b holds ( f is invertible iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) ) ); theorem Th31: :: CAT_1:31 for C being Category for b, c being Object of C for g being Morphism of b,c st Hom (b,c) <> {} holds ( g is monic iff for a being Object of C for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds f1 = f2 ) proof let C be Category; ::_thesis: for b, c being Object of C for g being Morphism of b,c st Hom (b,c) <> {} holds ( g is monic iff for a being Object of C for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds f1 = f2 ) let b, c be Object of C; ::_thesis: for g being Morphism of b,c st Hom (b,c) <> {} holds ( g is monic iff for a being Object of C for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds f1 = f2 ) let g be Morphism of b,c; ::_thesis: ( Hom (b,c) <> {} implies ( g is monic iff for a being Object of C for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds f1 = f2 ) ) assume A1: Hom (b,c) <> {} ; ::_thesis: ( g is monic iff for a being Object of C for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds f1 = f2 ) thus ( g is monic implies for a being Object of C for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds f1 = f2 ) by Defm; ::_thesis: ( ( for a being Object of C for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds f1 = f2 ) implies g is monic ) assume A7: for a being Object of C for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds f1 = f2 ; ::_thesis: g is monic thus Hom (b,c) <> {} by A1; :: according to CAT_1:def_14 ::_thesis: for a being Object of C st Hom (a,b) <> {} holds for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds f1 = f2 thus for a being Object of C st Hom (a,b) <> {} holds for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds f1 = f2 by A7; ::_thesis: verum end; theorem :: CAT_1:32 for C being Category for b, c, d being Object of C for g being Morphism of b,c for h being Morphism of c,d st g is monic & h is monic holds h * g is monic proof let C be Category; ::_thesis: for b, c, d being Object of C for g being Morphism of b,c for h being Morphism of c,d st g is monic & h is monic holds h * g is monic let b, c, d be Object of C; ::_thesis: for g being Morphism of b,c for h being Morphism of c,d st g is monic & h is monic holds h * g is monic let g be Morphism of b,c; ::_thesis: for h being Morphism of c,d st g is monic & h is monic holds h * g is monic let h be Morphism of c,d; ::_thesis: ( g is monic & h is monic implies h * g is monic ) assume that A3: g is monic and A4: h is monic ; ::_thesis: h * g is monic A1: Hom (b,c) <> {} by A3, Defm; A2: Hom (c,d) <> {} by A4, Defm; A5: now__::_thesis:_for_a_being_Object_of_C for_f1,_f2_being_Morphism_of_a,b_st_Hom_(a,b)_<>_{}_&_(h_*_g)_*_f1_=_(h_*_g)_*_f2_holds_ f1_=_f2 let a be Object of C; ::_thesis: for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & (h * g) * f1 = (h * g) * f2 holds f1 = f2 let f1, f2 be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & (h * g) * f1 = (h * g) * f2 implies f1 = f2 ) assume that A6: Hom (a,b) <> {} and A7: (h * g) * f1 = (h * g) * f2 ; ::_thesis: f1 = f2 A8: Hom (a,c) <> {} by A1, A6, Th23; ( h * (g * f1) = (h * g) * f1 & (h * g) * f2 = h * (g * f2) ) by A1, A2, A6, Th25; then g * f1 = g * f2 by Defm, A4, A7, A8; hence f1 = f2 by Defm, A3, A6; ::_thesis: verum end; Hom (b,d) <> {} by A1, A2, Th23; hence h * g is monic by A5, Th31; ::_thesis: verum end; theorem :: CAT_1:33 for C being Category for b, c, d being Object of C for g being Morphism of b,c for h being Morphism of c,d st Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic holds g is monic proof let C be Category; ::_thesis: for b, c, d being Object of C for g being Morphism of b,c for h being Morphism of c,d st Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic holds g is monic let b, c, d be Object of C; ::_thesis: for g being Morphism of b,c for h being Morphism of c,d st Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic holds g is monic let g be Morphism of b,c; ::_thesis: for h being Morphism of c,d st Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic holds g is monic let h be Morphism of c,d; ::_thesis: ( Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic implies g is monic ) assume that A1: Hom (b,c) <> {} and A2: Hom (c,d) <> {} and A3: h * g is monic ; ::_thesis: g is monic now__::_thesis:_for_a_being_Object_of_C for_f1,_f2_being_Morphism_of_a,b_st_Hom_(a,b)_<>_{}_&_g_*_f1_=_g_*_f2_holds_ f1_=_f2 let a be Object of C; ::_thesis: for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds f1 = f2 let f1, f2 be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & g * f1 = g * f2 implies f1 = f2 ) A4: Hom (b,d) <> {} by A1, A2, Th23; assume A5: Hom (a,b) <> {} ; ::_thesis: ( g * f1 = g * f2 implies f1 = f2 ) then ( h * (g * f1) = (h * g) * f1 & h * (g * f2) = (h * g) * f2 ) by A1, A2, Th25; hence ( g * f1 = g * f2 implies f1 = f2 ) by A3, A5, A4, Th31; ::_thesis: verum end; hence g is monic by A1, Th31; ::_thesis: verum end; theorem :: CAT_1:34 for C being Category for a, b being Object of C for h being Morphism of a,b for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds g is monic proof let C be Category; ::_thesis: for a, b being Object of C for h being Morphism of a,b for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds g is monic let a, b be Object of C; ::_thesis: for h being Morphism of a,b for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds g is monic let h be Morphism of a,b; ::_thesis: for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds g is monic let g be Morphism of b,a; ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b implies g is monic ) assume that A1: Hom (a,b) <> {} and A2: Hom (b,a) <> {} and A3: h * g = id b ; ::_thesis: g is monic now__::_thesis:_for_c_being_Object_of_C for_g1,_g2_being_Morphism_of_c,b_st_Hom_(c,b)_<>_{}_&_g_*_g1_=_g_*_g2_holds_ g1_=_g2 let c be Object of C; ::_thesis: for g1, g2 being Morphism of c,b st Hom (c,b) <> {} & g * g1 = g * g2 holds g1 = g2 let g1, g2 be Morphism of c,b; ::_thesis: ( Hom (c,b) <> {} & g * g1 = g * g2 implies g1 = g2 ) assume that A4: Hom (c,b) <> {} and A5: g * g1 = g * g2 ; ::_thesis: g1 = g2 thus g1 = (h * g) * g1 by A3, A4, Th28 .= h * (g * g2) by A1, A2, A4, A5, Th25 .= (h * g) * g2 by A1, A2, A4, Th25 .= g2 by A3, A4, Th28 ; ::_thesis: verum end; hence g is monic by A2, Th31; ::_thesis: verum end; theorem :: CAT_1:35 for C being Category for b being Object of C holds id b is monic proof let C be Category; ::_thesis: for b being Object of C holds id b is monic let b be Object of C; ::_thesis: id b is monic A1: now__::_thesis:_for_a_being_Object_of_C for_f1,_f2_being_Morphism_of_a,b_st_Hom_(a,b)_<>_{}_&_(id_b)_*_f1_=_(id_b)_*_f2_holds_ f1_=_f2 let a be Object of C; ::_thesis: for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & (id b) * f1 = (id b) * f2 holds f1 = f2 let f1, f2 be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & (id b) * f1 = (id b) * f2 implies f1 = f2 ) assume A2: Hom (a,b) <> {} ; ::_thesis: ( (id b) * f1 = (id b) * f2 implies f1 = f2 ) then (id b) * f1 = f1 by Th28; hence ( (id b) * f1 = (id b) * f2 implies f1 = f2 ) by A2, Th28; ::_thesis: verum end; Hom (b,b) <> {} ; hence id b is monic by A1, Th31; ::_thesis: verum end; theorem Th36: :: CAT_1:36 for C being Category for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} holds ( f is epi iff for c being Object of C for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds g1 = g2 ) proof let C be Category; ::_thesis: for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} holds ( f is epi iff for c being Object of C for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds g1 = g2 ) let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds ( f is epi iff for c being Object of C for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds g1 = g2 ) let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies ( f is epi iff for c being Object of C for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds g1 = g2 ) ) assume A1: Hom (a,b) <> {} ; ::_thesis: ( f is epi iff for c being Object of C for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds g1 = g2 ) thus ( f is epi implies for c being Object of C for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds g1 = g2 ) ::_thesis: ( ( for c being Object of C for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds g1 = g2 ) implies f is epi ) proof assume that Hom (a,b) <> {} and A2: for c being Object of C st Hom (b,c) <> {} holds for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds g1 = g2 ; :: according to CAT_1:def_15 ::_thesis: for c being Object of C for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds g1 = g2 let c be Object of C; ::_thesis: for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds g1 = g2 let g1, g2 be Morphism of b,c; ::_thesis: ( Hom (b,c) <> {} & g1 * f = g2 * f implies g1 = g2 ) thus ( Hom (b,c) <> {} & g1 * f = g2 * f implies g1 = g2 ) by A2; ::_thesis: verum end; assume A7: for c being Object of C for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds g1 = g2 ; ::_thesis: f is epi thus Hom (a,b) <> {} by A1; :: according to CAT_1:def_15 ::_thesis: for c being Object of C st Hom (b,c) <> {} holds for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds g1 = g2 thus for c being Object of C st Hom (b,c) <> {} holds for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds g1 = g2 by A7; ::_thesis: verum end; theorem :: CAT_1:37 for C being Category for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st f is epi & g is epi holds g * f is epi proof let C be Category; ::_thesis: for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st f is epi & g is epi holds g * f is epi let a, b, c be Object of C; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c st f is epi & g is epi holds g * f is epi let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st f is epi & g is epi holds g * f is epi let g be Morphism of b,c; ::_thesis: ( f is epi & g is epi implies g * f is epi ) assume that A3: f is epi and A4: g is epi ; ::_thesis: g * f is epi A1: Hom (a,b) <> {} by A3, Defe; A2: Hom (b,c) <> {} by A4, Defe; A5: now__::_thesis:_for_d_being_Object_of_C for_h1,_h2_being_Morphism_of_c,d_st_Hom_(c,d)_<>_{}_&_h1_*_(g_*_f)_=_h2_*_(g_*_f)_holds_ h1_=_h2 let d be Object of C; ::_thesis: for h1, h2 being Morphism of c,d st Hom (c,d) <> {} & h1 * (g * f) = h2 * (g * f) holds h1 = h2 let h1, h2 be Morphism of c,d; ::_thesis: ( Hom (c,d) <> {} & h1 * (g * f) = h2 * (g * f) implies h1 = h2 ) assume that A6: Hom (c,d) <> {} and A7: h1 * (g * f) = h2 * (g * f) ; ::_thesis: h1 = h2 A8: Hom (b,d) <> {} by A2, A6, Th23; ( h1 * (g * f) = (h1 * g) * f & (h2 * g) * f = h2 * (g * f) ) by A1, A2, A6, Th25; then h1 * g = h2 * g by Defe, A3, A7, A8; hence h1 = h2 by Defe, A4, A6; ::_thesis: verum end; Hom (a,c) <> {} by A1, A2, Th23; hence g * f is epi by A5, Th36; ::_thesis: verum end; theorem :: CAT_1:38 for C being Category for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds g is epi proof let C be Category; ::_thesis: for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds g is epi let a, b, c be Object of C; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds g is epi let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds g is epi let g be Morphism of b,c; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi implies g is epi ) assume that A1: Hom (a,b) <> {} and A2: Hom (b,c) <> {} and A3: g * f is epi ; ::_thesis: g is epi now__::_thesis:_for_d_being_Object_of_C for_h1,_h2_being_Morphism_of_c,d_st_Hom_(c,d)_<>_{}_&_h1_*_g_=_h2_*_g_holds_ h1_=_h2 let d be Object of C; ::_thesis: for h1, h2 being Morphism of c,d st Hom (c,d) <> {} & h1 * g = h2 * g holds h1 = h2 let h1, h2 be Morphism of c,d; ::_thesis: ( Hom (c,d) <> {} & h1 * g = h2 * g implies h1 = h2 ) A4: Hom (a,c) <> {} by A1, A2, Th23; assume A5: Hom (c,d) <> {} ; ::_thesis: ( h1 * g = h2 * g implies h1 = h2 ) then ( h1 * (g * f) = (h1 * g) * f & h2 * (g * f) = (h2 * g) * f ) by A1, A2, Th25; hence ( h1 * g = h2 * g implies h1 = h2 ) by A3, A5, A4, Th36; ::_thesis: verum end; hence g is epi by A2, Th36; ::_thesis: verum end; theorem :: CAT_1:39 for C being Category for a, b being Object of C for h being Morphism of a,b for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds h is epi proof let C be Category; ::_thesis: for a, b being Object of C for h being Morphism of a,b for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds h is epi let a, b be Object of C; ::_thesis: for h being Morphism of a,b for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds h is epi let h be Morphism of a,b; ::_thesis: for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds h is epi let g be Morphism of b,a; ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b implies h is epi ) assume that A1: Hom (a,b) <> {} and A2: Hom (b,a) <> {} and A3: h * g = id b ; ::_thesis: h is epi now__::_thesis:_for_c_being_Object_of_C for_h1,_h2_being_Morphism_of_b,c_st_Hom_(b,c)_<>_{}_&_h1_*_h_=_h2_*_h_holds_ h1_=_h2 let c be Object of C; ::_thesis: for h1, h2 being Morphism of b,c st Hom (b,c) <> {} & h1 * h = h2 * h holds h1 = h2 let h1, h2 be Morphism of b,c; ::_thesis: ( Hom (b,c) <> {} & h1 * h = h2 * h implies h1 = h2 ) assume that A4: Hom (b,c) <> {} and A5: h1 * h = h2 * h ; ::_thesis: h1 = h2 thus h1 = h1 * (h * g) by A3, A4, Th29 .= (h2 * h) * g by A1, A2, A4, A5, Th25 .= h2 * (h * g) by A1, A2, A4, Th25 .= h2 by A3, A4, Th29 ; ::_thesis: verum end; hence h is epi by A1, Th36; ::_thesis: verum end; theorem :: CAT_1:40 for C being Category for b being Object of C holds id b is epi proof let C be Category; ::_thesis: for b being Object of C holds id b is epi let b be Object of C; ::_thesis: id b is epi A1: now__::_thesis:_for_c_being_Object_of_C for_g1,_g2_being_Morphism_of_b,c_st_Hom_(b,c)_<>_{}_&_g1_*_(id_b)_=_g2_*_(id_b)_holds_ g1_=_g2 let c be Object of C; ::_thesis: for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * (id b) = g2 * (id b) holds g1 = g2 let g1, g2 be Morphism of b,c; ::_thesis: ( Hom (b,c) <> {} & g1 * (id b) = g2 * (id b) implies g1 = g2 ) assume A2: Hom (b,c) <> {} ; ::_thesis: ( g1 * (id b) = g2 * (id b) implies g1 = g2 ) then g1 * (id b) = g1 by Th29; hence ( g1 * (id b) = g2 * (id b) implies g1 = g2 ) by A2, Th29; ::_thesis: verum end; Hom (b,b) <> {} ; hence id b is epi by A1, Th36; ::_thesis: verum end; theorem Th41: :: CAT_1:41 for C being Category for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} holds ( f is invertible iff ( Hom (b,a) <> {} & ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) ) ) proof let C be Category; ::_thesis: for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} holds ( f is invertible iff ( Hom (b,a) <> {} & ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) ) ) let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds ( f is invertible iff ( Hom (b,a) <> {} & ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) ) ) let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies ( f is invertible iff ( Hom (b,a) <> {} & ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) ) ) ) assume A1: Hom (a,b) <> {} ; ::_thesis: ( f is invertible iff ( Hom (b,a) <> {} & ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) ) ) thus ( f is invertible implies ( Hom (b,a) <> {} & ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) ) ) ::_thesis: ( Hom (b,a) <> {} & ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) implies f is invertible ) proof assume A2: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_1:def_16 ::_thesis: ( for g being Morphism of b,a holds ( not f * g = id b or not g * f = id a ) or ( Hom (b,a) <> {} & ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) ) ) given g being Morphism of b,a such that A3: ( f * g = id b & g * f = id a ) ; ::_thesis: ( Hom (b,a) <> {} & ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) ) thus Hom (b,a) <> {} by A2; ::_thesis: ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) take g ; ::_thesis: ( f * g = id b & g * f = id a ) thus ( f * g = id b & g * f = id a ) by A3; ::_thesis: verum end; assume A6: Hom (b,a) <> {} ; ::_thesis: ( for g being Morphism of b,a holds ( not f * g = id b or not g * f = id a ) or f is invertible ) given g being Morphism of b,a such that A7: ( f * g = id b & g * f = id a ) ; ::_thesis: f is invertible thus ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1, A6; :: according to CAT_1:def_16 ::_thesis: ex g being Morphism of b,a st ( f * g = id b & g * f = id a ) take g ; ::_thesis: ( f * g = id b & g * f = id a ) thus ( f * g = id b & g * f = id a ) by A7; ::_thesis: verum end; theorem Th42: :: CAT_1:42 for C being Category for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} & Hom (b,a) <> {} holds for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds g1 = g2 proof let C be Category; ::_thesis: for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} & Hom (b,a) <> {} holds for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds g1 = g2 let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} & Hom (b,a) <> {} holds for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds g1 = g2 let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} implies for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds g1 = g2 ) assume that A1: Hom (a,b) <> {} and A2: Hom (b,a) <> {} ; ::_thesis: for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds g1 = g2 let g1, g2 be Morphism of b,a; ::_thesis: ( f * g1 = id b & g2 * f = id a implies g1 = g2 ) assume A3: f * g1 = id b ; ::_thesis: ( not g2 * f = id a or g1 = g2 ) assume g2 * f = id a ; ::_thesis: g1 = g2 hence g1 = (g2 * f) * g1 by A2, Th28 .= g2 * (id b) by A1, A2, A3, Th25 .= g2 by A2, Th29 ; ::_thesis: verum end; definition let C be Category; let a, b be Object of C; let f be Morphism of a,b; assume A2: f is invertible ; A1: Hom (a,b) <> {} by A2, Dfi; funcf " -> Morphism of b,a means :Def11: :: CAT_1:def 17 ( f * it = id b & it * f = id a ); existence ex b1 being Morphism of b,a st ( f * b1 = id b & b1 * f = id a ) by Dfi, A2; uniqueness for b1, b2 being Morphism of b,a st f * b1 = id b & b1 * f = id a & f * b2 = id b & b2 * f = id a holds b1 = b2 proof Hom (b,a) <> {} by Dfi, A2; hence for b1, b2 being Morphism of b,a st f * b1 = id b & b1 * f = id a & f * b2 = id b & b2 * f = id a holds b1 = b2 by A1, Th42; ::_thesis: verum end; end; :: deftheorem Def11 defines " CAT_1:def_17_:_ for C being Category for a, b being Object of C for f being Morphism of a,b st f is invertible holds for b5 being Morphism of b,a holds ( b5 = f " iff ( f * b5 = id b & b5 * f = id a ) ); theorem :: CAT_1:43 for C being Category for a, b being Object of C for f being Morphism of a,b st f is invertible holds ( f is monic & f is epi ) proof let C be Category; ::_thesis: for a, b being Object of C for f being Morphism of a,b st f is invertible holds ( f is monic & f is epi ) let a, b be Object of C; ::_thesis: for f being Morphism of a,b st f is invertible holds ( f is monic & f is epi ) let f be Morphism of a,b; ::_thesis: ( f is invertible implies ( f is monic & f is epi ) ) assume A2: f is invertible ; ::_thesis: ( f is monic & f is epi ) A1: Hom (a,b) <> {} by A2, Dfi; consider k being Morphism of b,a such that A3: f * k = id b and A4: k * f = id a by Dfi, A2; A5: Hom (b,a) <> {} by Dfi, A2; now__::_thesis:_for_c_being_Object_of_C for_g,_h_being_Morphism_of_c,a_st_Hom_(c,a)_<>_{}_&_f_*_g_=_f_*_h_holds_ g_=_h let c be Object of C; ::_thesis: for g, h being Morphism of c,a st Hom (c,a) <> {} & f * g = f * h holds g = h let g, h be Morphism of c,a; ::_thesis: ( Hom (c,a) <> {} & f * g = f * h implies g = h ) assume that A6: Hom (c,a) <> {} and A7: f * g = f * h ; ::_thesis: g = h g = (k * f) * g by A4, A6, Th28 .= k * (f * h) by A1, A5, A6, A7, Th25 .= (id a) * h by A1, A5, A4, A6, Th25 ; hence g = h by A6, Th28; ::_thesis: verum end; hence f is monic by A1, Th31; ::_thesis: f is epi now__::_thesis:_for_c_being_Object_of_C for_g,_h_being_Morphism_of_b,c_st_Hom_(b,c)_<>_{}_&_g_*_f_=_h_*_f_holds_ g_=_h let c be Object of C; ::_thesis: for g, h being Morphism of b,c st Hom (b,c) <> {} & g * f = h * f holds g = h let g, h be Morphism of b,c; ::_thesis: ( Hom (b,c) <> {} & g * f = h * f implies g = h ) assume that A8: Hom (b,c) <> {} and A9: g * f = h * f ; ::_thesis: g = h g = g * (f * k) by A3, A8, Th29 .= (h * f) * k by A1, A5, A8, A9, Th25 .= h * (id b) by A1, A5, A3, A8, Th25 ; hence g = h by A8, Th29; ::_thesis: verum end; hence f is epi by A1, Th36; ::_thesis: verum end; theorem :: CAT_1:44 for C being Category for a being Object of C holds id a is invertible proof let C be Category; ::_thesis: for a being Object of C holds id a is invertible let a be Object of C; ::_thesis: id a is invertible ( Hom (a,a) <> {} & (id a) * (id a) = id a ) ; hence id a is invertible by Th41; ::_thesis: verum end; theorem Th45: :: CAT_1:45 for C being Category for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st f is invertible & g is invertible holds g * f is invertible proof let C be Category; ::_thesis: for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st f is invertible & g is invertible holds g * f is invertible let a, b, c be Object of C; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c st f is invertible & g is invertible holds g * f is invertible let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st f is invertible & g is invertible holds g * f is invertible let g be Morphism of b,c; ::_thesis: ( f is invertible & g is invertible implies g * f is invertible ) assume A3: f is invertible ; ::_thesis: ( not g is invertible or g * f is invertible ) then A4: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by Dfi; consider f1 being Morphism of b,a such that A5: f * f1 = id b and A6: f1 * f = id a by Dfi, A3; assume A7: g is invertible ; ::_thesis: g * f is invertible then A8: ( Hom (b,c) <> {} & Hom (c,b) <> {} ) by Dfi; consider g1 being Morphism of c,b such that A9: g * g1 = id c and A10: g1 * g = id b by Dfi, A7; A11: now__::_thesis:_(_Hom_(c,a)_<>_{}_&_ex_f1g1_being_Morphism_of_c,a_st_ (_(g_*_f)_*_f1g1_=_id_c_&_f1g1_*_(g_*_f)_=_id_a_)_) thus A12: Hom (c,a) <> {} by A4, A8, Th23; ::_thesis: ex f1g1 being Morphism of c,a st ( (g * f) * f1g1 = id c & f1g1 * (g * f) = id a ) take f1g1 = f1 * g1; ::_thesis: ( (g * f) * f1g1 = id c & f1g1 * (g * f) = id a ) thus (g * f) * f1g1 = g * (f * (f1 * g1)) by A4, A8, A12, Th25 .= g * ((id b) * g1) by A4, A5, A8, Th25 .= id c by A8, A9, Th28 ; ::_thesis: f1g1 * (g * f) = id a Hom (a,c) <> {} by A4, A8, Th23; hence f1g1 * (g * f) = f1 * (g1 * (g * f)) by A4, A8, Th25 .= f1 * ((id b) * f) by A4, A8, A10, Th25 .= id a by A4, A6, Th28 ; ::_thesis: verum end; Hom (a,c) <> {} by A4, A8, Th23; hence g * f is invertible by A11, Th41; ::_thesis: verum end; theorem :: CAT_1:46 for C being Category for a, b being Object of C for f being Morphism of a,b st f is invertible holds f " is invertible proof let C be Category; ::_thesis: for a, b being Object of C for f being Morphism of a,b st f is invertible holds f " is invertible let a, b be Object of C; ::_thesis: for f being Morphism of a,b st f is invertible holds f " is invertible let f be Morphism of a,b; ::_thesis: ( f is invertible implies f " is invertible ) assume A2: f is invertible ; ::_thesis: f " is invertible then A3: f * (f ") = id b by Def11; A1: Hom (a,b) <> {} by A2, Dfi; ( Hom (b,a) <> {} & (f ") * f = id a ) by Dfi, A2, Def11; hence f " is invertible by A1, A3, Th41; ::_thesis: verum end; theorem :: CAT_1:47 for C being Category for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st f is invertible & g is invertible holds (g * f) " = (f ") * (g ") proof let C be Category; ::_thesis: for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st f is invertible & g is invertible holds (g * f) " = (f ") * (g ") let a, b, c be Object of C; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c st f is invertible & g is invertible holds (g * f) " = (f ") * (g ") let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st f is invertible & g is invertible holds (g * f) " = (f ") * (g ") let g be Morphism of b,c; ::_thesis: ( f is invertible & g is invertible implies (g * f) " = (f ") * (g ") ) assume that A3: f is invertible and A4: g is invertible ; ::_thesis: (g * f) " = (f ") * (g ") A1: Hom (a,b) <> {} by A3, Dfi; A2: Hom (b,c) <> {} by A4, Dfi; A5: Hom (c,b) <> {} by Dfi, A4; A6: Hom (b,a) <> {} by Dfi, A3; then A7: Hom (c,a) <> {} by A5, Th23; then A8: ((f ") * (g ")) * (g * f) = (((f ") * (g ")) * g) * f by A1, A2, Th25 .= ((f ") * ((g ") * g)) * f by A2, A6, A5, Th25 .= ((f ") * (id b)) * f by A4, Def11 .= (f ") * f by A6, Th29 .= id a by A3, Def11 ; A9: ( Hom (a,c) <> {} & g * f is invertible ) by A1, A2, A3, A4, Th23, Th45; (g * f) * ((f ") * (g ")) = g * (f * ((f ") * (g "))) by A1, A2, A7, Th25 .= g * ((f * (f ")) * (g ")) by A1, A6, A5, Th25 .= g * ((id b) * (g ")) by A3, Def11 .= g * (g ") by A5, Th28 .= id c by A4, Def11 ; hence (g * f) " = (f ") * (g ") by A8, A9, Def11; ::_thesis: verum end; definition let C be Category; let a be Object of C; attra is terminal means :Def12: :: CAT_1:def 18 for b being Object of C holds ( Hom (b,a) <> {} & ex f being Morphism of b,a st for g being Morphism of b,a holds f = g ); attra is initial means :Def13: :: CAT_1:def 19 for b being Object of C holds ( Hom (a,b) <> {} & ex f being Morphism of a,b st for g being Morphism of a,b holds f = g ); let b be Object of C; preda,b are_isomorphic means :: CAT_1:def 20 ex f being Morphism of a,b st f is invertible ; reflexivity for a being Object of C ex f being Morphism of a,a st f is invertible proof let a be Object of C; ::_thesis: ex f being Morphism of a,a st f is invertible A1: Hom (a,a) <> {} ; take id a ; ::_thesis: id a is invertible (id a) * (id a) = id a ; hence id a is invertible by A1, Th41; ::_thesis: verum end; symmetry for a, b being Object of C st ex f being Morphism of a,b st f is invertible holds ex f being Morphism of b,a st f is invertible proof let a, b be Object of C; ::_thesis: ( ex f being Morphism of a,b st f is invertible implies ex f being Morphism of b,a st f is invertible ) given f being Morphism of a,b such that A2: f is invertible ; ::_thesis: ex f being Morphism of b,a st f is invertible A3: ( Hom (b,a) <> {} & Hom (a,b) <> {} ) by A2, Dfi; consider g being Morphism of b,a such that A4: ( f * g = id b & g * f = id a ) by A2, Dfi; take g ; ::_thesis: g is invertible thus g is invertible by A3, A4, Dfi; ::_thesis: verum end; end; :: deftheorem Def12 defines terminal CAT_1:def_18_:_ for C being Category for a being Object of C holds ( a is terminal iff for b being Object of C holds ( Hom (b,a) <> {} & ex f being Morphism of b,a st for g being Morphism of b,a holds f = g ) ); :: deftheorem Def13 defines initial CAT_1:def_19_:_ for C being Category for a being Object of C holds ( a is initial iff for b being Object of C holds ( Hom (a,b) <> {} & ex f being Morphism of a,b st for g being Morphism of a,b holds f = g ) ); :: deftheorem defines are_isomorphic CAT_1:def_20_:_ for C being Category for a, b being Object of C holds ( a,b are_isomorphic iff ex f being Morphism of a,b st f is invertible ); theorem :: CAT_1:48 for C being Category for a, b being Object of C holds ( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) ) ) proof let C be Category; ::_thesis: for a, b being Object of C holds ( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) ) ) let a, b be Object of C; ::_thesis: ( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) ) ) thus ( a,b are_isomorphic implies ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) ) ) ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) implies a,b are_isomorphic ) proof given f being Morphism of a,b such that A2: f is invertible ; :: according to CAT_1:def_20 ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) ) thus ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A2, Dfi; ::_thesis: ex f being Morphism of a,b ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) take f ; ::_thesis: ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) thus ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) by A2, Dfi; ::_thesis: verum end; assume that A3: Hom (a,b) <> {} and A4: Hom (b,a) <> {} ; ::_thesis: ( for f being Morphism of a,b for f9 being Morphism of b,a holds ( not f * f9 = id b or not f9 * f = id a ) or a,b are_isomorphic ) given f being Morphism of a,b such that A5: ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) ; ::_thesis: a,b are_isomorphic take f ; :: according to CAT_1:def_20 ::_thesis: f is invertible thus f is invertible by A3, A4, A5, Th41; ::_thesis: verum end; theorem :: CAT_1:49 for C being Category for a being Object of C holds ( a is initial iff for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) proof let C be Category; ::_thesis: for a being Object of C holds ( a is initial iff for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) let a be Object of C; ::_thesis: ( a is initial iff for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) thus ( a is initial implies for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) ::_thesis: ( ( for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) implies a is initial ) proof assume A1: a is initial ; ::_thesis: for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} let b be Object of C; ::_thesis: ex f being Morphism of a,b st Hom (a,b) = {f} consider f being Morphism of a,b such that A2: for g being Morphism of a,b holds f = g by A1, Def13; take f ; ::_thesis: Hom (a,b) = {f} thus Hom (a,b) = {f} by A2, Th8, A1, Def13; ::_thesis: verum end; assume A3: for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ; ::_thesis: a is initial let b be Object of C; :: according to CAT_1:def_19 ::_thesis: ( Hom (a,b) <> {} & ex f being Morphism of a,b st for g being Morphism of a,b holds f = g ) consider f being Morphism of a,b such that A4: Hom (a,b) = {f} by A3; thus Hom (a,b) <> {} by A4; ::_thesis: ex f being Morphism of a,b st for g being Morphism of a,b holds f = g take f ; ::_thesis: for g being Morphism of a,b holds f = g thus for g being Morphism of a,b holds f = g by A4, Th7; ::_thesis: verum end; theorem Th50: :: CAT_1:50 for C being Category for a being Object of C st a is initial holds for h being Morphism of a,a holds id a = h proof let C be Category; ::_thesis: for a being Object of C st a is initial holds for h being Morphism of a,a holds id a = h let a be Object of C; ::_thesis: ( a is initial implies for h being Morphism of a,a holds id a = h ) assume a is initial ; ::_thesis: for h being Morphism of a,a holds id a = h then consider f being Morphism of a,a such that A1: for g being Morphism of a,a holds f = g by Def13; let h be Morphism of a,a; ::_thesis: id a = h id a = f by A1; hence id a = h by A1; ::_thesis: verum end; theorem :: CAT_1:51 for C being Category for a, b being Object of C st a is initial & b is initial holds a,b are_isomorphic proof let C be Category; ::_thesis: for a, b being Object of C st a is initial & b is initial holds a,b are_isomorphic let a, b be Object of C; ::_thesis: ( a is initial & b is initial implies a,b are_isomorphic ) assume that A1: a is initial and A2: b is initial ; ::_thesis: a,b are_isomorphic set g = the Morphism of b,a; set f = the Morphism of a,b; A3: Hom (a,b) <> {} by A1, Def13; take the Morphism of a,b ; :: according to CAT_1:def_20 ::_thesis: the Morphism of a,b is invertible now__::_thesis:_(_Hom_(b,a)_<>_{}_&_ex_g_being_Morphism_of_b,a_st_ (_the_Morphism_of_a,b_*_g_=_id_b_&_g_*_the_Morphism_of_a,b_=_id_a_)_) thus Hom (b,a) <> {} by A2, Def13; ::_thesis: ex g being Morphism of b,a st ( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a ) take g = the Morphism of b,a; ::_thesis: ( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a ) thus ( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a ) by A1, A2, Th50; ::_thesis: verum end; hence the Morphism of a,b is invertible by A3, Th41; ::_thesis: verum end; theorem :: CAT_1:52 for C being Category for a, b being Object of C st a is initial & a,b are_isomorphic holds b is initial proof let C be Category; ::_thesis: for a, b being Object of C st a is initial & a,b are_isomorphic holds b is initial let a, b be Object of C; ::_thesis: ( a is initial & a,b are_isomorphic implies b is initial ) assume A1: a is initial ; ::_thesis: ( not a,b are_isomorphic or b is initial ) given f being Morphism of a,b such that A2: f is invertible ; :: according to CAT_1:def_20 ::_thesis: b is initial A3: Hom (b,a) <> {} by A2, Dfi; let c be Object of C; :: according to CAT_1:def_19 ::_thesis: ( Hom (b,c) <> {} & ex f being Morphism of b,c st for g being Morphism of b,c holds f = g ) consider h being Morphism of a,c such that A4: for g being Morphism of a,c holds h = g by A1, Def13; Hom (a,c) <> {} by A1, Def13; hence A5: Hom (b,c) <> {} by A3, Th23; ::_thesis: ex f being Morphism of b,c st for g being Morphism of b,c holds f = g consider f9 being Morphism of b,a such that A6: f * f9 = id b and f9 * f = id a by A2, Dfi; A7: Hom (a,b) <> {} by A2, Dfi; take h * f9 ; ::_thesis: for g being Morphism of b,c holds h * f9 = g let h9 be Morphism of b,c; ::_thesis: h * f9 = h9 thus h9 = h9 * (f * f9) by A6, A5, Th29 .= (h9 * f) * f9 by A3, A5, A7, Th25 .= h * f9 by A4 ; ::_thesis: verum end; theorem :: CAT_1:53 for C being Category for b being Object of C holds ( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) proof let C be Category; ::_thesis: for b being Object of C holds ( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) let b be Object of C; ::_thesis: ( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) thus ( b is terminal implies for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) ::_thesis: ( ( for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) implies b is terminal ) proof assume A1: b is terminal ; ::_thesis: for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} let a be Object of C; ::_thesis: ex f being Morphism of a,b st Hom (a,b) = {f} consider f being Morphism of a,b such that A2: for g being Morphism of a,b holds f = g by A1, Def12; take f ; ::_thesis: Hom (a,b) = {f} thus Hom (a,b) = {f} by A2, Th8, A1, Def12; ::_thesis: verum end; assume A3: for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ; ::_thesis: b is terminal let a be Object of C; :: according to CAT_1:def_18 ::_thesis: ( Hom (a,b) <> {} & ex f being Morphism of a,b st for g being Morphism of a,b holds f = g ) consider f being Morphism of a,b such that A4: Hom (a,b) = {f} by A3; thus Hom (a,b) <> {} by A4; ::_thesis: ex f being Morphism of a,b st for g being Morphism of a,b holds f = g take f ; ::_thesis: for g being Morphism of a,b holds f = g thus for g being Morphism of a,b holds f = g by A4, Th7; ::_thesis: verum end; theorem Th54: :: CAT_1:54 for C being Category for a being Object of C st a is terminal holds for h being Morphism of a,a holds id a = h proof let C be Category; ::_thesis: for a being Object of C st a is terminal holds for h being Morphism of a,a holds id a = h let a be Object of C; ::_thesis: ( a is terminal implies for h being Morphism of a,a holds id a = h ) assume a is terminal ; ::_thesis: for h being Morphism of a,a holds id a = h then consider f being Morphism of a,a such that A1: for g being Morphism of a,a holds f = g by Def12; let h be Morphism of a,a; ::_thesis: id a = h id a = f by A1; hence id a = h by A1; ::_thesis: verum end; theorem :: CAT_1:55 for C being Category for a, b being Object of C st a is terminal & b is terminal holds a,b are_isomorphic proof let C be Category; ::_thesis: for a, b being Object of C st a is terminal & b is terminal holds a,b are_isomorphic let a, b be Object of C; ::_thesis: ( a is terminal & b is terminal implies a,b are_isomorphic ) assume that A1: a is terminal and A2: b is terminal ; ::_thesis: a,b are_isomorphic set g = the Morphism of b,a; set f = the Morphism of a,b; A3: Hom (a,b) <> {} by A2, Def12; take the Morphism of a,b ; :: according to CAT_1:def_20 ::_thesis: the Morphism of a,b is invertible now__::_thesis:_(_Hom_(b,a)_<>_{}_&_ex_g_being_Morphism_of_b,a_st_ (_the_Morphism_of_a,b_*_g_=_id_b_&_g_*_the_Morphism_of_a,b_=_id_a_)_) thus Hom (b,a) <> {} by A1, Def12; ::_thesis: ex g being Morphism of b,a st ( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a ) take g = the Morphism of b,a; ::_thesis: ( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a ) thus ( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a ) by A1, A2, Th54; ::_thesis: verum end; hence the Morphism of a,b is invertible by A3, Th41; ::_thesis: verum end; theorem :: CAT_1:56 for C being Category for b, a being Object of C st b is terminal & a,b are_isomorphic holds a is terminal proof let C be Category; ::_thesis: for b, a being Object of C st b is terminal & a,b are_isomorphic holds a is terminal let b, a be Object of C; ::_thesis: ( b is terminal & a,b are_isomorphic implies a is terminal ) assume A1: b is terminal ; ::_thesis: ( not a,b are_isomorphic or a is terminal ) given f being Morphism of a,b such that A2: f is invertible ; :: according to CAT_1:def_20 ::_thesis: a is terminal A3: Hom (b,a) <> {} by A2, Dfi; let c be Object of C; :: according to CAT_1:def_18 ::_thesis: ( Hom (c,a) <> {} & ex f being Morphism of c,a st for g being Morphism of c,a holds f = g ) consider h being Morphism of c,b such that A4: for g being Morphism of c,b holds h = g by A1, Def12; Hom (c,b) <> {} by A1, Def12; hence A5: Hom (c,a) <> {} by A3, Th23; ::_thesis: ex f being Morphism of c,a st for g being Morphism of c,a holds f = g consider f9 being Morphism of b,a such that f * f9 = id b and A6: f9 * f = id a by A2, Dfi; A7: Hom (a,b) <> {} by A2, Dfi; take f9 * h ; ::_thesis: for g being Morphism of c,a holds f9 * h = g let h9 be Morphism of c,a; ::_thesis: f9 * h = h9 thus f9 * h = f9 * (f * h9) by A4 .= (f9 * f) * h9 by A3, A5, A7, Th25 .= h9 by A6, A5, Th28 ; ::_thesis: verum end; theorem :: CAT_1:57 for C being Category for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} & a is terminal holds f is monic proof let C be Category; ::_thesis: for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} & a is terminal holds f is monic let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} & a is terminal holds f is monic let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & a is terminal implies f is monic ) assume that A1: Hom (a,b) <> {} and A2: a is terminal ; ::_thesis: f is monic now__::_thesis:_for_c_being_Object_of_C for_g,_h_being_Morphism_of_c,a_st_Hom_(c,a)_<>_{}_&_f_*_g_=_f_*_h_holds_ g_=_h let c be Object of C; ::_thesis: for g, h being Morphism of c,a st Hom (c,a) <> {} & f * g = f * h holds g = h let g, h be Morphism of c,a; ::_thesis: ( Hom (c,a) <> {} & f * g = f * h implies g = h ) assume that Hom (c,a) <> {} and f * g = f * h ; ::_thesis: g = h consider ff being Morphism of c,a such that A3: for gg being Morphism of c,a holds ff = gg by A2, Def12; ff = g by A3; hence g = h by A3; ::_thesis: verum end; hence f is monic by A1, Th31; ::_thesis: verum end; registration let C be Category; let a be Object of C; reduce dom (id a) to a; reducibility dom (id a) = a proof id a in Hom (a,a) by Def4; hence dom (id a) = a by Th1; ::_thesis: verum end; reduce cod (id a) to a; reducibility cod (id a) = a proof id a in Hom (a,a) by Def4; hence cod (id a) = a by Th1; ::_thesis: verum end; end; theorem Th58: :: CAT_1:58 for C being Category for a being Object of C holds ( dom (id a) = a & cod (id a) = a ) ; theorem Th59: :: CAT_1:59 for C being Category for a, b being Object of C st id a = id b holds a = b proof let C be Category; ::_thesis: for a, b being Object of C st id a = id b holds a = b let a, b be Object of C; ::_thesis: ( id a = id b implies a = b ) assume Z: id a = id b ; ::_thesis: a = b thus a = dom (id a) .= b by Th58, Z ; ::_thesis: verum end; theorem :: CAT_1:60 for C being Category for a, b, c being Object of C st a,b are_isomorphic & b,c are_isomorphic holds a,c are_isomorphic proof let C be Category; ::_thesis: for a, b, c being Object of C st a,b are_isomorphic & b,c are_isomorphic holds a,c are_isomorphic let a, b, c be Object of C; ::_thesis: ( a,b are_isomorphic & b,c are_isomorphic implies a,c are_isomorphic ) given f being Morphism of a,b such that A2: f is invertible ; :: according to CAT_1:def_20 ::_thesis: ( not b,c are_isomorphic or a,c are_isomorphic ) given g being Morphism of b,c such that A4: g is invertible ; :: according to CAT_1:def_20 ::_thesis: a,c are_isomorphic take g * f ; :: according to CAT_1:def_20 ::_thesis: g * f is invertible thus g * f is invertible by A2, A4, Th45; ::_thesis: verum end; definition let C, D be Category; mode Functor of C,D -> Function of the carrier' of C, the carrier' of D means :Def15: :: CAT_1:def 21 ( ( for c being Element of C ex d being Element of D st it . (id c) = id d ) & ( for f being Element of the carrier' of C holds ( it . (id (dom f)) = id (dom (it . f)) & it . (id (cod f)) = id (cod (it . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds it . (g (*) f) = (it . g) (*) (it . f) ) ); existence ex b1 being Function of the carrier' of C, the carrier' of D st ( ( for c being Element of C ex d being Element of D st b1 . (id c) = id d ) & ( for f being Element of the carrier' of C holds ( b1 . (id (dom f)) = id (dom (b1 . f)) & b1 . (id (cod f)) = id (cod (b1 . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds b1 . (g (*) f) = (b1 . g) (*) (b1 . f) ) ) proof set d = the Element of D; reconsider F = the carrier' of C --> (id the Element of D) as Function of the carrier' of C, the carrier' of D ; take F ; ::_thesis: ( ( for c being Element of C ex d being Element of D st F . (id c) = id d ) & ( for f being Element of the carrier' of C holds ( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds F . (g (*) f) = (F . g) (*) (F . f) ) ) thus for c being Element of C ex d being Element of D st F . (id c) = id d by FUNCOP_1:7; ::_thesis: ( ( for f being Element of the carrier' of C holds ( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds F . (g (*) f) = (F . g) (*) (F . f) ) ) A1: Hom ( the Element of D, the Element of D) <> {} ; thus for f being Element of the carrier' of C holds ( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ::_thesis: for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds F . (g (*) f) = (F . g) (*) (F . f) proof let f be Element of the carrier' of C; ::_thesis: ( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) A2: F . f = id the Element of D by FUNCOP_1:7; thus F . (id (dom f)) = id the Element of D by FUNCOP_1:7 .= id (dom (F . f)) by A2, Th58 ; ::_thesis: F . (id (cod f)) = id (cod (F . f)) thus F . (id (cod f)) = id the Element of D by FUNCOP_1:7 .= id (cod (F . f)) by A2, Th58 ; ::_thesis: verum end; let f, g be Element of the carrier' of C; ::_thesis: ( [g,f] in dom the Comp of C implies F . (g (*) f) = (F . g) (*) (F . f) ) assume [g,f] in dom the Comp of C ; ::_thesis: F . (g (*) f) = (F . g) (*) (F . f) thus F . (g (*) f) = (id the Element of D) * (id the Element of D) by FUNCOP_1:7 .= (id the Element of D) (*) (id the Element of D) by A1, Def10 .= (id the Element of D) (*) (F . f) by FUNCOP_1:7 .= (F . g) (*) (F . f) by FUNCOP_1:7 ; ::_thesis: verum end; end; :: deftheorem Def15 defines Functor CAT_1:def_21_:_ for C, D being Category for b3 being Function of the carrier' of C, the carrier' of D holds ( b3 is Functor of C,D iff ( ( for c being Element of C ex d being Element of D st b3 . (id c) = id d ) & ( for f being Element of the carrier' of C holds ( b3 . (id (dom f)) = id (dom (b3 . f)) & b3 . (id (cod f)) = id (cod (b3 . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds b3 . (g (*) f) = (b3 . g) (*) (b3 . f) ) ) ); theorem Th61: :: CAT_1:61 for C, D being Category for T being Function of the carrier' of C, the carrier' of D st ( for c being Object of C ex d being Object of D st T . (id c) = id d ) & ( for f being Morphism of C holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ) holds T is Functor of C,D proof let C, D be Category; ::_thesis: for T being Function of the carrier' of C, the carrier' of D st ( for c being Object of C ex d being Object of D st T . (id c) = id d ) & ( for f being Morphism of C holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ) holds T is Functor of C,D let T be Function of the carrier' of C, the carrier' of D; ::_thesis: ( ( for c being Object of C ex d being Object of D st T . (id c) = id d ) & ( for f being Morphism of C holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ) implies T is Functor of C,D ) assume that A1: for c being Object of C ex d being Object of D st T . (id c) = id d and A2: for f being Morphism of C holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) and A3: for f, g being Morphism of C st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ; ::_thesis: T is Functor of C,D thus for c being Element of C ex d being Element of D st T . (id c) = id d by A1; :: according to CAT_1:def_21 ::_thesis: ( ( for f being Element of the carrier' of C holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds T . (g (*) f) = (T . g) (*) (T . f) ) ) thus for f being Element of the carrier' of C holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by A2; ::_thesis: for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds T . (g (*) f) = (T . g) (*) (T . f) let f, g be Element of the carrier' of C; ::_thesis: ( [g,f] in dom the Comp of C implies T . (g (*) f) = (T . g) (*) (T . f) ) assume [g,f] in dom the Comp of C ; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f) then A5: dom g = cod f by Def5a; thus T . (g (*) f) = (T . g) (*) (T . f) by A3, A5; ::_thesis: verum end; theorem :: CAT_1:62 for C, D being Category for T being Functor of C,D for c being Object of C ex d being Object of D st T . (id c) = id d by Def15; theorem :: CAT_1:63 for C, D being Category for T being Functor of C,D for f being Morphism of C holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by Def15; theorem Th64: :: CAT_1:64 for C, D being Category for T being Functor of C,D for f, g being Morphism of C st dom g = cod f holds ( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) ) proof let C, D be Category; ::_thesis: for T being Functor of C,D for f, g being Morphism of C st dom g = cod f holds ( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) ) let T be Functor of C,D; ::_thesis: for f, g being Morphism of C st dom g = cod f holds ( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) ) let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies ( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) ) ) assume A1: dom g = cod f ; ::_thesis: ( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) ) then A2: ( the Comp of C . (g,f) = g (*) f & [g,f] in dom the Comp of C ) by Def5a, Th16; id (dom (T . g)) = T . (id (cod f)) by A1, Def15 .= id (cod (T . f)) by Def15 ; hence dom (T . g) = cod (T . f) by Th59; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f) thus T . (g (*) f) = (T . g) (*) (T . f) by A2, Def15; ::_thesis: verum end; theorem Th65: :: CAT_1:65 for C, D being Category for T being Function of the carrier' of C, the carrier' of D for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds ( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ) holds T is Functor of C,D proof let C, D be Category; ::_thesis: for T being Function of the carrier' of C, the carrier' of D for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds ( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ) holds T is Functor of C,D let T be Function of the carrier' of C, the carrier' of D; ::_thesis: for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds ( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ) holds T is Functor of C,D let F be Function of the carrier of C, the carrier of D; ::_thesis: ( ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds ( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ) implies T is Functor of C,D ) assume that A1: for c being Object of C holds T . (id c) = id (F . c) and A2: for f being Morphism of C holds ( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) and A3: for f, g being Morphism of C st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ; ::_thesis: T is Functor of C,D A4: for c being Object of C ex d being Object of D st T . (id c) = id d proof let c be Object of C; ::_thesis: ex d being Object of D st T . (id c) = id d take F . c ; ::_thesis: T . (id c) = id (F . c) thus T . (id c) = id (F . c) by A1; ::_thesis: verum end; for f being Morphism of C holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) proof let f be Morphism of C; ::_thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) thus T . (id (dom f)) = id (F . (dom f)) by A1 .= id (dom (T . f)) by A2 ; ::_thesis: T . (id (cod f)) = id (cod (T . f)) thus T . (id (cod f)) = id (F . (cod f)) by A1 .= id (cod (T . f)) by A2 ; ::_thesis: verum end; hence T is Functor of C,D by A3, A4, Th61; ::_thesis: verum end; definition let C, D be Category; let F be Function of the carrier' of C, the carrier' of D; assume A1: for c being Element of C ex d being Element of D st F . (id c) = id d ; func Obj F -> Function of the carrier of C, the carrier of D means :Def16: :: CAT_1:def 22 for c being Element of C for d being Element of D st F . (id c) = id d holds it . c = d; existence ex b1 being Function of the carrier of C, the carrier of D st for c being Element of C for d being Element of D st F . (id c) = id d holds b1 . c = d proof defpred S1[ Object of C, Object of D] means for d being Element of D st F . (id \$1) = id d holds \$2 = d; A2: for c being Element of C ex y being Element of D st S1[c,y] proof let c be Element of C; ::_thesis: ex y being Element of D st S1[c,y] consider y being Element of D such that A3: F . (id c) = id y by A1; take y ; ::_thesis: S1[c,y] let d be Element of D; ::_thesis: ( F . (id c) = id d implies y = d ) assume F . (id c) = id d ; ::_thesis: y = d hence y = d by A3, Th59; ::_thesis: verum end; thus ex f being Function of the carrier of C, the carrier of D st for x being Element of C holds S1[x,f . x] from FUNCT_2:sch_3(A2); ::_thesis: verum end; uniqueness for b1, b2 being Function of the carrier of C, the carrier of D st ( for c being Element of C for d being Element of D st F . (id c) = id d holds b1 . c = d ) & ( for c being Element of C for d being Element of D st F . (id c) = id d holds b2 . c = d ) holds b1 = b2 proof let F1, F2 be Function of the carrier of C, the carrier of D; ::_thesis: ( ( for c being Element of C for d being Element of D st F . (id c) = id d holds F1 . c = d ) & ( for c being Element of C for d being Element of D st F . (id c) = id d holds F2 . c = d ) implies F1 = F2 ) assume that A5: for c being Element of C for d being Element of D st F . (id c) = id d holds F1 . c = d and A6: for c being Element of C for d being Element of D st F . (id c) = id d holds F2 . c = d ; ::_thesis: F1 = F2 for c being Element of C holds F1 . c = F2 . c proof let c be Element of C; ::_thesis: F1 . c = F2 . c consider d1 being Element of D such that A7: F . (id c) = id d1 by A1; F1 . c = d1 by A5, A7; hence F1 . c = F2 . c by A6, A7; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def16 defines Obj CAT_1:def_22_:_ for C, D being Category for F being Function of the carrier' of C, the carrier' of D st ( for c being Element of C ex d being Element of D st F . (id c) = id d ) holds for b4 being Function of the carrier of C, the carrier of D holds ( b4 = Obj F iff for c being Element of C for d being Element of D st F . (id c) = id d holds b4 . c = d ); theorem :: CAT_1:66 for C, D being Category for T being Function of the carrier' of C, the carrier' of D st ( for c being Object of C ex d being Object of D st T . (id c) = id d ) holds for c being Object of C for d being Object of D st T . (id c) = id d holds (Obj T) . c = d by Def16; theorem Th67: :: CAT_1:67 for C, D being Category for T being Functor of C,D for c being Object of C for d being Object of D st T . (id c) = id d holds (Obj T) . c = d proof let C, D be Category; ::_thesis: for T being Functor of C,D for c being Object of C for d being Object of D st T . (id c) = id d holds (Obj T) . c = d let T be Functor of C,D; ::_thesis: for c being Object of C for d being Object of D st T . (id c) = id d holds (Obj T) . c = d for c being Object of C ex d being Object of D st T . (id c) = id d by Def15; hence for c being Object of C for d being Object of D st T . (id c) = id d holds (Obj T) . c = d by Def16; ::_thesis: verum end; theorem Th68: :: CAT_1:68 for C, D being Category for T being Functor of C,D for c being Object of C holds T . (id c) = id ((Obj T) . c) proof let C, D be Category; ::_thesis: for T being Functor of C,D for c being Object of C holds T . (id c) = id ((Obj T) . c) let T be Functor of C,D; ::_thesis: for c being Object of C holds T . (id c) = id ((Obj T) . c) let c be Object of C; ::_thesis: T . (id c) = id ((Obj T) . c) ex d being Object of D st T . (id c) = id d by Def15; hence T . (id c) = id ((Obj T) . c) by Th67; ::_thesis: verum end; theorem Th69: :: CAT_1:69 for C, D being Category for T being Functor of C,D for f being Morphism of C holds ( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) ) proof let C, D be Category; ::_thesis: for T being Functor of C,D for f being Morphism of C holds ( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) ) let T be Functor of C,D; ::_thesis: for f being Morphism of C holds ( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) ) let f be Morphism of C; ::_thesis: ( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) ) ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by Def15; hence ( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) ) by Th67; ::_thesis: verum end; definition let C, D be Category; let T be Functor of C,D; let c be Object of C; funcT . c -> Object of D equals :: CAT_1:def 23 (Obj T) . c; correctness coherence (Obj T) . c is Object of D; ; end; :: deftheorem defines . CAT_1:def_23_:_ for C, D being Category for T being Functor of C,D for c being Object of C holds T . c = (Obj T) . c; theorem :: CAT_1:70 for C, D being Category for T being Functor of C,D for c being Object of C for d being Object of D st T . (id c) = id d holds T . c = d by Th67; theorem :: CAT_1:71 for C, D being Category for T being Functor of C,D for c being Object of C holds T . (id c) = id (T . c) by Th68; theorem :: CAT_1:72 for C, D being Category for T being Functor of C,D for f being Morphism of C holds ( T . (dom f) = dom (T . f) & T . (cod f) = cod (T . f) ) by Th69; theorem Th73: :: CAT_1:73 for B, C, D being Category for T being Functor of B,C for S being Functor of C,D holds S * T is Functor of B,D proof let B, C, D be Category; ::_thesis: for T being Functor of B,C for S being Functor of C,D holds S * T is Functor of B,D let T be Functor of B,C; ::_thesis: for S being Functor of C,D holds S * T is Functor of B,D let S be Functor of C,D; ::_thesis: S * T is Functor of B,D reconsider FF = (Obj S) * (Obj T) as Function of the carrier of B, the carrier of D ; reconsider TT = S * T as Function of the carrier' of B, the carrier' of D ; now__::_thesis:_(_(_for_b_being_Object_of_B_holds_TT_._(id_b)_=_id_(FF_._b)_)_&_(_for_f_being_Morphism_of_B_holds_ (_FF_._(dom_f)_=_dom_(TT_._f)_&_FF_._(cod_f)_=_cod_(TT_._f)_)_)_&_(_for_f,_g_being_Morphism_of_B_st_dom_g_=_cod_f_holds_ TT_._(g_(*)_f)_=_(TT_._g)_(*)_(TT_._f)_)_) thus for b being Object of B holds TT . (id b) = id (FF . b) ::_thesis: ( ( for f being Morphism of B holds ( FF . (dom f) = dom (TT . f) & FF . (cod f) = cod (TT . f) ) ) & ( for f, g being Morphism of B st dom g = cod f holds TT . (g (*) f) = (TT . g) (*) (TT . f) ) ) proof let b be Object of B; ::_thesis: TT . (id b) = id (FF . b) thus TT . (id b) = S . (T . (id b)) by FUNCT_2:15 .= S . (id (T . b)) by Th68 .= id (S . ((Obj T) . b)) by Th68 .= id (FF . b) by FUNCT_2:15 ; ::_thesis: verum end; thus for f being Morphism of B holds ( FF . (dom f) = dom (TT . f) & FF . (cod f) = cod (TT . f) ) ::_thesis: for f, g being Morphism of B st dom g = cod f holds TT . (g (*) f) = (TT . g) (*) (TT . f) proof let f be Morphism of B; ::_thesis: ( FF . (dom f) = dom (TT . f) & FF . (cod f) = cod (TT . f) ) thus FF . (dom f) = (Obj S) . ((Obj T) . (dom f)) by FUNCT_2:15 .= (Obj S) . (dom (T . f)) by Th69 .= dom (S . (T . f)) by Th69 .= dom (TT . f) by FUNCT_2:15 ; ::_thesis: FF . (cod f) = cod (TT . f) thus FF . (cod f) = (Obj S) . ((Obj T) . (cod f)) by FUNCT_2:15 .= (Obj S) . (cod (T . f)) by Th69 .= cod (S . (T . f)) by Th69 .= cod (TT . f) by FUNCT_2:15 ; ::_thesis: verum end; let f, g be Morphism of B; ::_thesis: ( dom g = cod f implies TT . (g (*) f) = (TT . g) (*) (TT . f) ) assume A1: dom g = cod f ; ::_thesis: TT . (g (*) f) = (TT . g) (*) (TT . f) then A2: dom (T . g) = cod (T . f) by Th64; thus TT . (g (*) f) = S . (T . (g (*) f)) by FUNCT_2:15 .= S . ((T . g) (*) (T . f)) by A1, Th64 .= (S . (T . g)) (*) (S . (T . f)) by A2, Th64 .= (TT . g) (*) (S . (T . f)) by FUNCT_2:15 .= (TT . g) (*) (TT . f) by FUNCT_2:15 ; ::_thesis: verum end; hence S * T is Functor of B,D by Th65; ::_thesis: verum end; definition let B, C, D be Category; let T be Functor of B,C; let S be Functor of C,D; :: original: * redefine funcS * T -> Functor of B,D; coherence T * S is Functor of B,D by Th73; end; theorem Th74: :: CAT_1:74 for C being Category holds id the carrier' of C is Functor of C,C proof let C be Category; ::_thesis: id the carrier' of C is Functor of C,C set F = id the carrier of C; set T = id the carrier' of C; now__::_thesis:_(_(_for_c_being_Object_of_C_holds_(id_the_carrier'_of_C)_._(id_c)_=_id_((id_the_carrier_of_C)_._c)_)_&_(_for_f_being_Morphism_of_C_holds_ (_(id_the_carrier_of_C)_._(dom_f)_=_dom_((id_the_carrier'_of_C)_._f)_&_(id_the_carrier_of_C)_._(cod_f)_=_cod_((id_the_carrier'_of_C)_._f)_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_ (id_the_carrier'_of_C)_._(g_(*)_f)_=_((id_the_carrier'_of_C)_._g)_(*)_((id_the_carrier'_of_C)_._f)_)_) thus for c being Object of C holds (id the carrier' of C) . (id c) = id ((id the carrier of C) . c) ::_thesis: ( ( for f being Morphism of C holds ( (id the carrier of C) . (dom f) = dom ((id the carrier' of C) . f) & (id the carrier of C) . (cod f) = cod ((id the carrier' of C) . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds (id the carrier' of C) . (g (*) f) = ((id the carrier' of C) . g) (*) ((id the carrier' of C) . f) ) ) proof let c be Object of C; ::_thesis: (id the carrier' of C) . (id c) = id ((id the carrier of C) . c) (id the carrier of C) . c = c by FUNCT_1:18; hence (id the carrier' of C) . (id c) = id ((id the carrier of C) . c) by FUNCT_1:18; ::_thesis: verum end; thus for f being Morphism of C holds ( (id the carrier of C) . (dom f) = dom ((id the carrier' of C) . f) & (id the carrier of C) . (cod f) = cod ((id the carrier' of C) . f) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds (id the carrier' of C) . (g (*) f) = ((id the carrier' of C) . g) (*) ((id the carrier' of C) . f) proof let f be Morphism of C; ::_thesis: ( (id the carrier of C) . (dom f) = dom ((id the carrier' of C) . f) & (id the carrier of C) . (cod f) = cod ((id the carrier' of C) . f) ) (id the carrier' of C) . f = f by FUNCT_1:18; hence ( (id the carrier of C) . (dom f) = dom ((id the carrier' of C) . f) & (id the carrier of C) . (cod f) = cod ((id the carrier' of C) . f) ) by FUNCT_1:18; ::_thesis: verum end; let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (id the carrier' of C) . (g (*) f) = ((id the carrier' of C) . g) (*) ((id the carrier' of C) . f) ) assume dom g = cod f ; ::_thesis: (id the carrier' of C) . (g (*) f) = ((id the carrier' of C) . g) (*) ((id the carrier' of C) . f) thus (id the carrier' of C) . (g (*) f) = g (*) f by FUNCT_1:18 .= ((id the carrier' of C) . g) (*) f by FUNCT_1:18 .= ((id the carrier' of C) . g) (*) ((id the carrier' of C) . f) by FUNCT_1:18 ; ::_thesis: verum end; hence id the carrier' of C is Functor of C,C by Th65; ::_thesis: verum end; theorem Th75: :: CAT_1:75 for B, C, D being Category for T being Functor of B,C for S being Functor of C,D for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b) proof let B, C, D be Category; ::_thesis: for T being Functor of B,C for S being Functor of C,D for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b) let T be Functor of B,C; ::_thesis: for S being Functor of C,D for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b) let S be Functor of C,D; ::_thesis: for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b) let b be Object of B; ::_thesis: (Obj (S * T)) . b = (Obj S) . ((Obj T) . b) A1: (S * T) . (id b) = S . (T . (id b)) by FUNCT_2:15; consider d being Object of D such that A2: (S * T) . (id b) = id d by Def15; consider c being Object of C such that A3: T . (id b) = id c by Def15; thus (Obj (S * T)) . b = d by A2, Th67 .= (Obj S) . c by A2, A3, A1, Th67 .= (Obj S) . ((Obj T) . b) by A3, Th67 ; ::_thesis: verum end; theorem :: CAT_1:76 for B, C, D being Category for T being Functor of B,C for S being Functor of C,D for b being Object of B holds (S * T) . b = S . (T . b) by Th75; definition let C be Category; func id C -> Functor of C,C equals :: CAT_1:def 24 id the carrier' of C; coherence id the carrier' of C is Functor of C,C by Th74; end; :: deftheorem defines id CAT_1:def_24_:_ for C being Category holds id C = id the carrier' of C; theorem Th77: :: CAT_1:77 for C being Category for c being Object of C holds (Obj (id C)) . c = c proof let C be Category; ::_thesis: for c being Object of C holds (Obj (id C)) . c = c let c be Object of C; ::_thesis: (Obj (id C)) . c = c (id C) . (id c) = id c by FUNCT_1:18; hence (Obj (id C)) . c = c by Th67; ::_thesis: verum end; theorem Th78: :: CAT_1:78 for C being Category holds Obj (id C) = id the carrier of C proof let C be Category; ::_thesis: Obj (id C) = id the carrier of C ( dom (Obj (id C)) = the carrier of C & ( for x being set st x in the carrier of C holds (Obj (id C)) . x = x ) ) by Th77, FUNCT_2:def_1; hence Obj (id C) = id the carrier of C by FUNCT_1:17; ::_thesis: verum end; theorem :: CAT_1:79 for C being Category for c being Object of C holds (id C) . c = c by Th77; definition let C, D be Category; let T be Functor of C,D; attrT is isomorphic means :: CAT_1:def 25 ( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D ); attrT is full means :Def20: :: CAT_1:def 26 for c, c9 being Object of C st Hom ((T . c),(T . c9)) <> {} holds for g being Morphism of T . c,T . c9 holds ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ); attrT is faithful means :Def21: :: CAT_1:def 27 for c, c9 being Object of C st Hom (c,c9) <> {} holds for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds f1 = f2; end; :: deftheorem defines isomorphic CAT_1:def_25_:_ for C, D being Category for T being Functor of C,D holds ( T is isomorphic iff ( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D ) ); :: deftheorem Def20 defines full CAT_1:def_26_:_ for C, D being Category for T being Functor of C,D holds ( T is full iff for c, c9 being Object of C st Hom ((T . c),(T . c9)) <> {} holds for g being Morphism of T . c,T . c9 holds ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) ); :: deftheorem Def21 defines faithful CAT_1:def_27_:_ for C, D being Category for T being Functor of C,D holds ( T is faithful iff for c, c9 being Object of C st Hom (c,c9) <> {} holds for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds f1 = f2 ); theorem :: CAT_1:80 for C being Category holds id C is isomorphic proof let C be Category; ::_thesis: id C is isomorphic rng (id the carrier of C) = the carrier of C ; hence ( id C is one-to-one & rng (id C) = the carrier' of C & rng (Obj (id C)) = the carrier of C ) by Th78, RELAT_1:45; :: according to CAT_1:def_25 ::_thesis: verum end; theorem Th81: :: CAT_1:81 for C, D being Category for T being Functor of C,D for c, c9 being Object of C for f being set st f in Hom (c,c9) holds T . f in Hom ((T . c),(T . c9)) proof let C, D be Category; ::_thesis: for T being Functor of C,D for c, c9 being Object of C for f being set st f in Hom (c,c9) holds T . f in Hom ((T . c),(T . c9)) let T be Functor of C,D; ::_thesis: for c, c9 being Object of C for f being set st f in Hom (c,c9) holds T . f in Hom ((T . c),(T . c9)) let c, c9 be Object of C; ::_thesis: for f being set st f in Hom (c,c9) holds T . f in Hom ((T . c),(T . c9)) let f be set ; ::_thesis: ( f in Hom (c,c9) implies T . f in Hom ((T . c),(T . c9)) ) assume A1: f in Hom (c,c9) ; ::_thesis: T . f in Hom ((T . c),(T . c9)) then reconsider f9 = f as Morphism of c,c9 by Def4; cod f9 = c9 by A1, Th1; then A2: T . c9 = cod (T . f9) by Th69; dom f9 = c by A1, Th1; then T . c = dom (T . f9) by Th69; hence T . f in Hom ((T . c),(T . c9)) by A2; ::_thesis: verum end; theorem Th82: :: CAT_1:82 for C, D being Category for T being Functor of C,D for c, c9 being Object of C st Hom (c,c9) <> {} holds for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9)) proof let C, D be Category; ::_thesis: for T being Functor of C,D for c, c9 being Object of C st Hom (c,c9) <> {} holds for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9)) let T be Functor of C,D; ::_thesis: for c, c9 being Object of C st Hom (c,c9) <> {} holds for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9)) let c, c9 be Object of C; ::_thesis: ( Hom (c,c9) <> {} implies for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9)) ) assume A1: Hom (c,c9) <> {} ; ::_thesis: for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9)) let f be Morphism of c,c9; ::_thesis: T . f in Hom ((T . c),(T . c9)) f in Hom (c,c9) by A1, Def4; hence T . f in Hom ((T . c),(T . c9)) by Th81; ::_thesis: verum end; theorem Th83: :: CAT_1:83 for C, D being Category for T being Functor of C,D for c, c9 being Object of C st Hom (c,c9) <> {} holds for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9 proof let C, D be Category; ::_thesis: for T being Functor of C,D for c, c9 being Object of C st Hom (c,c9) <> {} holds for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9 let T be Functor of C,D; ::_thesis: for c, c9 being Object of C st Hom (c,c9) <> {} holds for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9 let c, c9 be Object of C; ::_thesis: ( Hom (c,c9) <> {} implies for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9 ) assume A1: Hom (c,c9) <> {} ; ::_thesis: for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9 let f be Morphism of c,c9; ::_thesis: T . f is Morphism of T . c,T . c9 T . f in Hom ((T . c),(T . c9)) by A1, Th82; hence T . f is Morphism of T . c,T . c9 by Def4; ::_thesis: verum end; theorem Th84: :: CAT_1:84 for C, D being Category for T being Functor of C,D for c, c9 being Object of C st Hom (c,c9) <> {} holds Hom ((T . c),(T . c9)) <> {} proof let C, D be Category; ::_thesis: for T being Functor of C,D for c, c9 being Object of C st Hom (c,c9) <> {} holds Hom ((T . c),(T . c9)) <> {} let T be Functor of C,D; ::_thesis: for c, c9 being Object of C st Hom (c,c9) <> {} holds Hom ((T . c),(T . c9)) <> {} let c, c9 be Object of C; ::_thesis: ( Hom (c,c9) <> {} implies Hom ((T . c),(T . c9)) <> {} ) set f = the Element of Hom (c,c9); assume Hom (c,c9) <> {} ; ::_thesis: Hom ((T . c),(T . c9)) <> {} then the Element of Hom (c,c9) in Hom (c,c9) ; hence Hom ((T . c),(T . c9)) <> {} by Th81; ::_thesis: verum end; theorem :: CAT_1:85 for B, C, D being Category for T being Functor of B,C for S being Functor of C,D st T is full & S is full holds S * T is full proof let B, C, D be Category; ::_thesis: for T being Functor of B,C for S being Functor of C,D st T is full & S is full holds S * T is full let T be Functor of B,C; ::_thesis: for S being Functor of C,D st T is full & S is full holds S * T is full let S be Functor of C,D; ::_thesis: ( T is full & S is full implies S * T is full ) assume that A1: T is full and A2: S is full ; ::_thesis: S * T is full let b, b9 be Object of B; :: according to CAT_1:def_26 ::_thesis: ( Hom (((S * T) . b),((S * T) . b9)) <> {} implies for g being Morphism of (S * T) . b,(S * T) . b9 holds ( Hom (b,b9) <> {} & ex f being Morphism of b,b9 st g = (S * T) . f ) ) assume A3: Hom (((S * T) . b),((S * T) . b9)) <> {} ; ::_thesis: for g being Morphism of (S * T) . b,(S * T) . b9 holds ( Hom (b,b9) <> {} & ex f being Morphism of b,b9 st g = (S * T) . f ) let g be Morphism of (S * T) . b,(S * T) . b9; ::_thesis: ( Hom (b,b9) <> {} & ex f being Morphism of b,b9 st g = (S * T) . f ) A4: ( (S * T) . b = S . (T . b) & (S * T) . b9 = S . (T . b9) ) by Th75; then consider f being Morphism of T . b,T . b9 such that A5: g = S . f by A2, A3, Def20; A6: Hom ((T . b),(T . b9)) <> {} by A2, A3, A4, Def20; hence Hom (b,b9) <> {} by A1, Def20; ::_thesis: ex f being Morphism of b,b9 st g = (S * T) . f consider h being Morphism of b,b9 such that A7: f = T . h by A1, A6, Def20; take h ; ::_thesis: g = (S * T) . h thus g = (S * T) . h by A5, A7, FUNCT_2:15; ::_thesis: verum end; theorem :: CAT_1:86 for B, C, D being Category for T being Functor of B,C for S being Functor of C,D st T is faithful & S is faithful holds S * T is faithful proof let B, C, D be Category; ::_thesis: for T being Functor of B,C for S being Functor of C,D st T is faithful & S is faithful holds S * T is faithful let T be Functor of B,C; ::_thesis: for S being Functor of C,D st T is faithful & S is faithful holds S * T is faithful let S be Functor of C,D; ::_thesis: ( T is faithful & S is faithful implies S * T is faithful ) assume that A1: T is faithful and A2: S is faithful ; ::_thesis: S * T is faithful let b, b9 be Object of B; :: according to CAT_1:def_27 ::_thesis: ( Hom (b,b9) <> {} implies for f1, f2 being Morphism of b,b9 st (S * T) . f1 = (S * T) . f2 holds f1 = f2 ) assume A3: Hom (b,b9) <> {} ; ::_thesis: for f1, f2 being Morphism of b,b9 st (S * T) . f1 = (S * T) . f2 holds f1 = f2 let f1, f2 be Morphism of b,b9; ::_thesis: ( (S * T) . f1 = (S * T) . f2 implies f1 = f2 ) A4: T . f2 is Morphism of T . b,T . b9 by A3, Th83; assume A5: (S * T) . f1 = (S * T) . f2 ; ::_thesis: f1 = f2 A6: ( (S * T) . f1 = S . (T . f1) & (S * T) . f2 = S . (T . f2) ) by FUNCT_2:15; ( Hom ((T . b),(T . b9)) <> {} & T . f1 is Morphism of T . b,T . b9 ) by A3, Th83, Th84; then T . f1 = T . f2 by A2, A5, A6, A4, Def21; hence f1 = f2 by A1, A3, Def21; ::_thesis: verum end; theorem Th87: :: CAT_1:87 for C, D being Category for T being Functor of C,D for c, c9 being Object of C holds T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9)) proof let C, D be Category; ::_thesis: for T being Functor of C,D for c, c9 being Object of C holds T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9)) let T be Functor of C,D; ::_thesis: for c, c9 being Object of C holds T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9)) let c, c9 be Object of C; ::_thesis: T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9)) let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in T .: (Hom (c,c9)) or f in Hom ((T . c),(T . c9)) ) assume f in T .: (Hom (c,c9)) ; ::_thesis: f in Hom ((T . c),(T . c9)) then ex g being Element of the carrier' of C st ( g in Hom (c,c9) & f = T . g ) by FUNCT_2:65; hence f in Hom ((T . c),(T . c9)) by Th81; ::_thesis: verum end; definition let C, D be Category; let T be Functor of C,D; let c, c9 be Object of C; func hom (T,c,c9) -> Function of (Hom (c,c9)),(Hom ((T . c),(T . c9))) equals :: CAT_1:def 28 T | (Hom (c,c9)); correctness coherence T | (Hom (c,c9)) is Function of (Hom (c,c9)),(Hom ((T . c),(T . c9))); proof T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9)) by Th87; hence T | (Hom (c,c9)) is Function of (Hom (c,c9)),(Hom ((T . c),(T . c9))) by FUNCT_2:101; ::_thesis: verum end; end; :: deftheorem defines hom CAT_1:def_28_:_ for C, D being Category for T being Functor of C,D for c, c9 being Object of C holds hom (T,c,c9) = T | (Hom (c,c9)); theorem Th88: :: CAT_1:88 for C, D being Category for T being Functor of C,D for c, c9 being Object of C st Hom (c,c9) <> {} holds for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f proof let C, D be Category; ::_thesis: for T being Functor of C,D for c, c9 being Object of C st Hom (c,c9) <> {} holds for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f let T be Functor of C,D; ::_thesis: for c, c9 being Object of C st Hom (c,c9) <> {} holds for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f let c, c9 be Object of C; ::_thesis: ( Hom (c,c9) <> {} implies for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f ) assume A1: Hom (c,c9) <> {} ; ::_thesis: for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f let f be Morphism of c,c9; ::_thesis: (hom (T,c,c9)) . f = T . f f in Hom (c,c9) by A1, Def4; hence (hom (T,c,c9)) . f = T . f by FUNCT_1:49; ::_thesis: verum end; theorem :: CAT_1:89 for C, D being Category for T being Functor of C,D holds ( T is full iff for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) ) proof let C, D be Category; ::_thesis: for T being Functor of C,D holds ( T is full iff for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) ) let T be Functor of C,D; ::_thesis: ( T is full iff for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) ) thus ( T is full implies for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) ) ::_thesis: ( ( for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) ) implies T is full ) proof assume A1: T is full ; ::_thesis: for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) let c, c9 be Object of C; ::_thesis: rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) now__::_thesis:_(_Hom_((T_._c),(T_._c9))_<>_{}_implies_rng_(hom_(T,c,c9))_=_Hom_((T_._c),(T_._c9))_) assume A2: Hom ((T . c),(T . c9)) <> {} ; ::_thesis: rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) for g being set holds ( g in rng (hom (T,c,c9)) iff g in Hom ((T . c),(T . c9)) ) proof let g be set ; ::_thesis: ( g in rng (hom (T,c,c9)) iff g in Hom ((T . c),(T . c9)) ) thus ( g in rng (hom (T,c,c9)) implies g in Hom ((T . c),(T . c9)) ) ::_thesis: ( g in Hom ((T . c),(T . c9)) implies g in rng (hom (T,c,c9)) ) proof assume g in rng (hom (T,c,c9)) ; ::_thesis: g in Hom ((T . c),(T . c9)) then consider f being set such that A3: f in dom (hom (T,c,c9)) and A4: (hom (T,c,c9)) . f = g by FUNCT_1:def_3; f in Hom (c,c9) by A2, A3, FUNCT_2:def_1; hence g in Hom ((T . c),(T . c9)) by A2, A4, FUNCT_2:5; ::_thesis: verum end; assume g in Hom ((T . c),(T . c9)) ; ::_thesis: g in rng (hom (T,c,c9)) then g is Morphism of T . c,T . c9 by Def4; then consider f being Morphism of c,c9 such that A5: g = T . f by A1, A2, Def20; Hom (c,c9) <> {} by A1, A2, Def20; then f in Hom (c,c9) by Def4; then (hom (T,c,c9)) . f in rng (hom (T,c,c9)) by A2, FUNCT_2:4; hence g in rng (hom (T,c,c9)) by A5, A1, A2, Def20, Th88; ::_thesis: verum end; hence rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) by TARSKI:1; ::_thesis: verum end; hence rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) ; ::_thesis: verum end; assume A7: for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) ; ::_thesis: T is full let c, c9 be Object of C; :: according to CAT_1:def_26 ::_thesis: ( Hom ((T . c),(T . c9)) <> {} implies for g being Morphism of T . c,T . c9 holds ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) ) assume A8: Hom ((T . c),(T . c9)) <> {} ; ::_thesis: for g being Morphism of T . c,T . c9 holds ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) let g be Morphism of T . c,T . c9; ::_thesis: ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) g in Hom ((T . c),(T . c9)) by A8, Def4; then g in rng (hom (T,c,c9)) by A7; then consider f being set such that A9: f in dom (hom (T,c,c9)) and A10: (hom (T,c,c9)) . f = g by FUNCT_1:def_3; thus Hom (c,c9) <> {} by A9; ::_thesis: ex f being Morphism of c,c9 st g = T . f A11: f in Hom (c,c9) by A8, A9, FUNCT_2:def_1; then reconsider f = f as Morphism of c,c9 by Def4; take f ; ::_thesis: g = T . f thus g = T . f by A10, A11, Th88; ::_thesis: verum end; theorem :: CAT_1:90 for C, D being Category for T being Functor of C,D holds ( T is faithful iff for c, c9 being Object of C holds hom (T,c,c9) is one-to-one ) proof let C, D be Category; ::_thesis: for T being Functor of C,D holds ( T is faithful iff for c, c9 being Object of C holds hom (T,c,c9) is one-to-one ) let T be Functor of C,D; ::_thesis: ( T is faithful iff for c, c9 being Object of C holds hom (T,c,c9) is one-to-one ) thus ( T is faithful implies for c, c9 being Object of C holds hom (T,c,c9) is one-to-one ) ::_thesis: ( ( for c, c9 being Object of C holds hom (T,c,c9) is one-to-one ) implies T is faithful ) proof assume A1: T is faithful ; ::_thesis: for c, c9 being Object of C holds hom (T,c,c9) is one-to-one let c, c9 be Object of C; ::_thesis: hom (T,c,c9) is one-to-one now__::_thesis:_(_Hom_((T_._c),(T_._c9))_<>_{}_implies_hom_(T,c,c9)_is_one-to-one_) A2: now__::_thesis:_for_f1,_f2_being_set_st_f1_in_Hom_(c,c9)_&_f2_in_Hom_(c,c9)_&_(hom_(T,c,c9))_._f1_=_(hom_(T,c,c9))_._f2_holds_ f1_=_f2 let f1, f2 be set ; ::_thesis: ( f1 in Hom (c,c9) & f2 in Hom (c,c9) & (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 implies f1 = f2 ) assume that A3: f1 in Hom (c,c9) and A4: f2 in Hom (c,c9) ; ::_thesis: ( (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 implies f1 = f2 ) A5: f2 is Morphism of c,c9 by A4, Def4; then A6: T . f2 = (hom (T,c,c9)) . f2 by A3, Th88; A7: f1 is Morphism of c,c9 by A3, Def4; then T . f1 = (hom (T,c,c9)) . f1 by A3, Th88; hence ( (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 implies f1 = f2 ) by A1, A3, A7, A5, A6, Def21; ::_thesis: verum end; assume Hom ((T . c),(T . c9)) <> {} ; ::_thesis: hom (T,c,c9) is one-to-one hence hom (T,c,c9) is one-to-one by A2, FUNCT_2:19; ::_thesis: verum end; hence hom (T,c,c9) is one-to-one ; ::_thesis: verum end; assume A8: for c, c9 being Object of C holds hom (T,c,c9) is one-to-one ; ::_thesis: T is faithful let c, c9 be Object of C; :: according to CAT_1:def_27 ::_thesis: ( Hom (c,c9) <> {} implies for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds f1 = f2 ) assume A9: Hom (c,c9) <> {} ; ::_thesis: for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds f1 = f2 let f1, f2 be Morphism of c,c9; ::_thesis: ( T . f1 = T . f2 implies f1 = f2 ) A10: T . f2 = (hom (T,c,c9)) . f2 by A9, Th88; A11: ( f2 in Hom (c,c9) & T . f1 = (hom (T,c,c9)) . f1 ) by A9, Def4, Th88; A12: hom (T,c,c9) is one-to-one by A8; ( Hom ((T . c),(T . c9)) <> {} & f1 in Hom (c,c9) ) by A9, Def4, Th84; hence ( T . f1 = T . f2 implies f1 = f2 ) by A12, A11, A10, FUNCT_2:19; ::_thesis: verum end;