:: ISOCAT_1 semantic presentation begin theorem :: ISOCAT_1:1 canceled; theorem :: ISOCAT_1:2 canceled; theorem Th3: :: ISOCAT_1:3 for B, A being Category for F being Functor of A,B for a, b being Object of A for f being Morphism of a,b st f is invertible holds F /. f is invertible proof let B, A be Category; ::_thesis: for F being Functor of A,B for a, b being Object of A for f being Morphism of a,b st f is invertible holds F /. f is invertible let F be Functor of A,B; ::_thesis: for a, b being Object of A for f being Morphism of a,b st f is invertible holds F /. f is invertible let a, b be Object of A; ::_thesis: for f being Morphism of a,b st f is invertible holds F /. f is invertible let f be Morphism of a,b; ::_thesis: ( f is invertible implies F /. f is invertible ) assume A1: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_1:def_16 ::_thesis: ( for b1 being Morphism of b,a holds ( not f * b1 = id b or not b1 * f = id a ) or F /. f is invertible ) given g being Morphism of b,a such that A2: f * g = id b and A3: g * f = id a ; ::_thesis: F /. f is invertible A4: dom g = b by A1, CAT_1:5 .= cod f by A1, CAT_1:5 ; A5: cod g = a by A1, CAT_1:5 .= dom f by A1, CAT_1:5 ; A6: cod f = b by A1, CAT_1:5; A7: dom f = a by A1, CAT_1:5; A8: f (*) g = id (cod f) by A2, A1, A6, CAT_1:def_13; A9: g (*) f = id (dom f) by A3, A1, A7, CAT_1:def_13; thus A10: ( Hom ((F . a),(F . b)) <> {} & Hom ((F . b),(F . a)) <> {} ) by A1, CAT_1:84; :: according to CAT_1:def_16 ::_thesis: ex b1 being Morphism of F . b,F . a st ( (F /. f) * b1 = id (F . b) & b1 * (F /. f) = id (F . a) ) take F /. g ; ::_thesis: ( (F /. f) * (F /. g) = id (F . b) & (F /. g) * (F /. f) = id (F . a) ) A11: F /. f = F . f by A1, CAT_3:def_10; A12: F /. g = F . g by A1, CAT_3:def_10; thus (F /. f) * (F /. g) = (F . f) (*) (F . g) by A10, A11, A12, CAT_1:def_13 .= F . (f (*) g) by A5, CAT_1:64 .= id (cod (F /. f)) by A8, A11, CAT_1:63 .= id (F . b) by A10, CAT_1:5 ; ::_thesis: (F /. g) * (F /. f) = id (F . a) thus (F /. g) * (F /. f) = (F . g) (*) (F . f) by A10, A11, A12, CAT_1:def_13 .= F . (g (*) f) by A4, CAT_1:64 .= id (dom (F /. f)) by A9, A11, CAT_1:63 .= id (F . a) by A10, CAT_1:5 ; ::_thesis: verum end; theorem Th4: :: ISOCAT_1:4 for A, B being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2 for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) ) assume A1: F1 is_transformable_to F2 ; ::_thesis: for t being transformation of F1,F2 for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) let t be transformation of F1,F2; ::_thesis: for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) let a be Object of A; ::_thesis: t . a in Hom ((F1 . a),(F2 . a)) Hom ((F1 . a),(F2 . a)) <> {} by A1, NATTRA_1:def_2; hence t . a in Hom ((F1 . a),(F2 . a)) by CAT_1:def_5; ::_thesis: verum end; theorem Th5: :: ISOCAT_1:5 for A, B, C being Category for F1, F2 being Functor of A,B for G1, G2 being Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds G1 * F1 is_transformable_to G2 * F2 proof let A, B, C be Category; ::_thesis: for F1, F2 being Functor of A,B for G1, G2 being Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds G1 * F1 is_transformable_to G2 * F2 let F1, F2 be Functor of A,B; ::_thesis: for G1, G2 being Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds G1 * F1 is_transformable_to G2 * F2 let G1, G2 be Functor of B,C; ::_thesis: ( F1 is_transformable_to F2 & G1 is_transformable_to G2 implies G1 * F1 is_transformable_to G2 * F2 ) assume that A1: F1 is_transformable_to F2 and A2: G1 is_transformable_to G2 ; ::_thesis: G1 * F1 is_transformable_to G2 * F2 let a be Object of A; :: according to NATTRA_1:def_2 ::_thesis: not Hom (((G1 * F1) . a),((G2 * F2) . a)) = {} Hom ((F1 . a),(F2 . a)) <> {} by A1, NATTRA_1:def_2; then A3: Hom ((G1 . (F1 . a)),(G1 . (F2 . a))) <> {} by CAT_1:84; A4: ( G1 . (F1 . a) = (G1 * F1) . a & G2 . (F2 . a) = (G2 * F2) . a ) by CAT_1:76; Hom ((G1 . (F2 . a)),(G2 . (F2 . a))) <> {} by A2, NATTRA_1:def_2; hence not Hom (((G1 * F1) . a),((G2 * F2) . a)) = {} by A4, A3, CAT_1:24; ::_thesis: verum end; theorem Th6: :: ISOCAT_1:6 for A, B being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 st t is invertible holds for a being Object of A holds F1 . a,F2 . a are_isomorphic proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 st t is invertible holds for a being Object of A holds F1 . a,F2 . a are_isomorphic let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2 st t is invertible holds for a being Object of A holds F1 . a,F2 . a are_isomorphic ) assume F1 is_transformable_to F2 ; ::_thesis: for t being transformation of F1,F2 st t is invertible holds for a being Object of A holds F1 . a,F2 . a are_isomorphic let t be transformation of F1,F2; ::_thesis: ( t is invertible implies for a being Object of A holds F1 . a,F2 . a are_isomorphic ) assume A1: t is invertible ; ::_thesis: for a being Object of A holds F1 . a,F2 . a are_isomorphic let a be Object of A; ::_thesis: F1 . a,F2 . a are_isomorphic take t . a ; :: according to CAT_1:def_20 ::_thesis: t . a is invertible thus t . a is invertible by A1, NATTRA_1:def_10; ::_thesis: verum end; definition let C, D be Category; redefine mode Functor of C,D means :: ISOCAT_1:def 1 ( ( for c being Object of C ex d being Object of D st it . (id c) = id d ) & ( for f being Morphism of C holds ( it . (id (dom f)) = id (dom (it . f)) & it . (id (cod f)) = id (cod (it . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds it . (g (*) f) = (it . g) (*) (it . f) ) ); compatibility for b1 being M2( bool [: the carrier' of C, the carrier' of D:]) holds ( b1 is Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b1 . (id c) = id d ) & ( for f being Morphism of C holds ( b1 . (id (dom f)) = id (dom (b1 . f)) & b1 . (id (cod f)) = id (cod (b1 . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds b1 . (g (*) f) = (b1 . g) (*) (b1 . f) ) ) ) by CAT_1:61, CAT_1:62, CAT_1:63, CAT_1:64; end; :: deftheorem defines Functor ISOCAT_1:def_1_:_ for C, D being Category for b3 being M2( bool [: the carrier' of b1, the carrier' of b2:]) holds ( b3 is Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b3 . (id c) = id d ) & ( for f being Morphism of C holds ( b3 . (id (dom f)) = id (dom (b3 . f)) & b3 . (id (cod f)) = id (cod (b3 . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds b3 . (g (*) f) = (b3 . g) (*) (b3 . f) ) ) ); theorem Th7: :: ISOCAT_1:7 for B, A being Category for F being Functor of A,B st F is isomorphic holds for g being Morphism of B ex f being Morphism of A st F . f = g proof let B, A be Category; ::_thesis: for F being Functor of A,B st F is isomorphic holds for g being Morphism of B ex f being Morphism of A st F . f = g let F be Functor of A,B; ::_thesis: ( F is isomorphic implies for g being Morphism of B ex f being Morphism of A st F . f = g ) assume A1: F is isomorphic ; ::_thesis: for g being Morphism of B ex f being Morphism of A st F . f = g let g be Morphism of B; ::_thesis: ex f being Morphism of A st F . f = g rng F = the carrier' of B by A1, CAT_1:def_25; then consider f being set such that A2: f in dom F and A3: F . f = g by FUNCT_1:def_3; reconsider f = f as Morphism of A by A2; take f ; ::_thesis: F . f = g thus F . f = g by A3; ::_thesis: verum end; theorem Th8: :: ISOCAT_1:8 for B, A being Category for F being Functor of A,B st F is isomorphic holds for b being Object of B ex a being Object of A st F . a = b proof let B, A be Category; ::_thesis: for F being Functor of A,B st F is isomorphic holds for b being Object of B ex a being Object of A st F . a = b let F be Functor of A,B; ::_thesis: ( F is isomorphic implies for b being Object of B ex a being Object of A st F . a = b ) assume A1: F is isomorphic ; ::_thesis: for b being Object of B ex a being Object of A st F . a = b let b be Object of B; ::_thesis: ex a being Object of A st F . a = b rng (Obj F) = the carrier of B by A1, CAT_1:def_25; then consider a being set such that A2: a in dom (Obj F) and A3: (Obj F) . a = b by FUNCT_1:def_3; reconsider a = a as Object of A by A2; take a ; ::_thesis: F . a = b thus F . a = b by A3; ::_thesis: verum end; theorem Th9: :: ISOCAT_1:9 for A, B being Category for F being Functor of A,B st F is one-to-one holds Obj F is one-to-one proof let A, B be Category; ::_thesis: for F being Functor of A,B st F is one-to-one holds Obj F is one-to-one let F be Functor of A,B; ::_thesis: ( F is one-to-one implies Obj F is one-to-one ) assume A1: F is one-to-one ; ::_thesis: Obj F is one-to-one let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (Obj F) or not x2 in dom (Obj F) or not (Obj F) . x1 = (Obj F) . x2 or x1 = x2 ) assume ( x1 in dom (Obj F) & x2 in dom (Obj F) ) ; ::_thesis: ( not (Obj F) . x1 = (Obj F) . x2 or x1 = x2 ) then reconsider a1 = x1, a2 = x2 as Object of A ; assume (Obj F) . x1 = (Obj F) . x2 ; ::_thesis: x1 = x2 then F . a1 = F . a2 ; then A2: F . (id a1) = id (F . a2) by CAT_1:71 .= F . (id a2) by CAT_1:71 ; dom F = the carrier' of A by FUNCT_2:def_1; then id a1 = id a2 by A1, A2, FUNCT_1:def_4; hence x1 = x2 by CAT_1:59; ::_thesis: verum end; definition let A, B be Category; let F be Functor of A,B; assume A1: F is isomorphic ; funcF " -> Functor of B,A equals :Def2: :: ISOCAT_1:def 2 F " ; coherence F " is Functor of B,A proof A2: F is one-to-one by A1, CAT_1:def_25; rng F = the carrier' of B by A1, CAT_1:def_25; then reconsider G = F " as Function of the carrier' of B, the carrier' of A by A2, FUNCT_2:25; A3: dom F = the carrier' of A by FUNCT_2:def_1; A4: Obj F is one-to-one by A2, Th9; G is Functor of B,A proof thus for c being Object of B ex d being Object of A st G . (id c) = id d :: according to ISOCAT_1:def_1 ::_thesis: ( ( for f being Morphism of B holds ( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) ) ) & ( for f, g being Morphism of B st dom g = cod f holds G . (g (*) f) = (G . g) (*) (G . f) ) ) proof let b be Object of B; ::_thesis: ex d being Object of A st G . (id b) = id d consider a being Object of A such that A5: F . a = b by A1, Th8; take a ; ::_thesis: G . (id b) = id a thus G . (id b) = G . (F . (id a)) by A5, CAT_1:71 .= id a by A2, A3, FUNCT_1:34 ; ::_thesis: verum end; thus for f being Morphism of B holds ( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) ) ::_thesis: for f, g being Morphism of B st dom g = cod f holds G . (g (*) f) = (G . g) (*) (G . f) proof let f be Morphism of B; ::_thesis: ( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) ) consider g being Morphism of A such that A6: f = F . g by A1, Th7; thus G . (id (dom f)) = G . (id (F . (dom g))) by A6, CAT_1:72 .= G . (F . (id (dom g))) by CAT_1:71 .= id (dom g) by A2, A3, FUNCT_1:34 .= id (dom (G . f)) by A2, A3, A6, FUNCT_1:34 ; ::_thesis: G . (id (cod f)) = id (cod (G . f)) thus G . (id (cod f)) = G . (id (F . (cod g))) by A6, CAT_1:72 .= G . (F . (id (cod g))) by CAT_1:71 .= id (cod g) by A2, A3, FUNCT_1:34 .= id (cod (G . f)) by A2, A3, A6, FUNCT_1:34 ; ::_thesis: verum end; let f, g be Morphism of B; ::_thesis: ( dom g = cod f implies G . (g (*) f) = (G . g) (*) (G . f) ) A7: dom (Obj F) = the carrier of A by FUNCT_2:def_1; assume A8: dom g = cod f ; ::_thesis: G . (g (*) f) = (G . g) (*) (G . f) consider f9 being Morphism of A such that A9: f = F . f9 by A1, Th7; consider g9 being Morphism of A such that A10: g = F . g9 by A1, Th7; (Obj F) . (dom g9) = F . (dom g9) .= cod f by A10, A8, CAT_1:72 .= F . (cod f9) by A9, CAT_1:72 .= (Obj F) . (cod f9) ; then dom g9 = cod f9 by A4, A7, FUNCT_1:def_4; hence G . (g (*) f) = G . (F . (g9 (*) f9)) by A9, A10, CAT_1:64 .= g9 (*) f9 by A2, A3, FUNCT_1:34 .= g9 (*) (G . f) by A2, A3, A9, FUNCT_1:34 .= (G . g) (*) (G . f) by A2, A3, A10, FUNCT_1:34 ; ::_thesis: verum end; hence F " is Functor of B,A ; ::_thesis: verum end; end; :: deftheorem Def2 defines " ISOCAT_1:def_2_:_ for A, B being Category for F being Functor of A,B st F is isomorphic holds F " = F " ; definition let A, B be Category; let F be Functor of A,B; redefine attr F is isomorphic means :Def3: :: ISOCAT_1:def 3 ( F is one-to-one & rng F = the carrier' of B ); compatibility ( F is isomorphic iff ( F is one-to-one & rng F = the carrier' of B ) ) proof thus ( F is isomorphic implies ( F is one-to-one & rng F = the carrier' of B ) ) by CAT_1:def_25; ::_thesis: ( F is one-to-one & rng F = the carrier' of B implies F is isomorphic ) assume that A1: F is one-to-one and A2: rng F = the carrier' of B ; ::_thesis: F is isomorphic thus ( F is one-to-one & rng F = the carrier' of B ) by A1, A2; :: according to CAT_1:def_25 ::_thesis: rng (Obj F) = the carrier of B thus rng (Obj F) c= the carrier of B ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of B c= rng (Obj F) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of B or x in rng (Obj F) ) assume x in the carrier of B ; ::_thesis: x in rng (Obj F) then reconsider d = x as Object of B ; consider f being set such that A3: f in dom F and A4: id d = F . f by A2, FUNCT_1:def_3; reconsider f = f as Morphism of A by A3; reconsider c = id (dom f) as Morphism of A ; F . c = id (dom (id d)) by A4, CAT_1:63 .= id d ; then ( dom (Obj F) = the carrier of A & (Obj F) . (dom f) = d ) by CAT_1:67, FUNCT_2:def_1; hence x in rng (Obj F) by FUNCT_1:def_3; ::_thesis: verum end; end; :: deftheorem Def3 defines isomorphic ISOCAT_1:def_3_:_ for A, B being Category for F being Functor of A,B holds ( F is isomorphic iff ( F is one-to-one & rng F = the carrier' of B ) ); theorem Th10: :: ISOCAT_1:10 for A, B being Category for F being Functor of A,B st F is isomorphic holds F " is isomorphic proof let A, B be Category; ::_thesis: for F being Functor of A,B st F is isomorphic holds F " is isomorphic let F be Functor of A,B; ::_thesis: ( F is isomorphic implies F " is isomorphic ) assume F is isomorphic ; ::_thesis: F " is isomorphic then A1: ( F is one-to-one & F " = F " ) by Def2, CAT_1:def_25; hence F " is one-to-one by FUNCT_1:40; :: according to ISOCAT_1:def_3 ::_thesis: rng (F ") = the carrier' of A thus rng (F ") = dom F by A1, FUNCT_1:33 .= the carrier' of A by FUNCT_2:def_1 ; ::_thesis: verum end; theorem :: ISOCAT_1:11 for A, B being Category for F being Functor of A,B st F is isomorphic holds (Obj F) " = Obj (F ") proof let A, B be Category; ::_thesis: for F being Functor of A,B st F is isomorphic holds (Obj F) " = Obj (F ") let F be Functor of A,B; ::_thesis: ( F is isomorphic implies (Obj F) " = Obj (F ") ) assume A1: F is isomorphic ; ::_thesis: (Obj F) " = Obj (F ") then A2: F is one-to-one by Def3; A3: rng (Obj F) = the carrier of B by A1, CAT_1:def_25; then reconsider G = (Obj F) " as Function of the carrier of B, the carrier of A by A2, Th9, FUNCT_2:25; A4: Obj F is one-to-one by A2, Th9; now__::_thesis:_for_b_being_Object_of_B_holds_G_._b_=_(Obj_(F_"))_._b let b be Object of B; ::_thesis: G . b = (Obj (F ")) . b F . (id (G . b)) = id ((Obj F) . (G . b)) by CAT_1:68 .= id b by A3, A4, FUNCT_1:35 ; then id (G . b) = (F ") . (id b) by A2, FUNCT_2:26 .= (F ") . (id b) by A1, Def2 ; hence G . b = (Obj (F ")) . b by CAT_1:67; ::_thesis: verum end; hence (Obj F) " = Obj (F ") by FUNCT_2:63; ::_thesis: verum end; theorem :: ISOCAT_1:12 for A, B being Category for F being Functor of A,B st F is isomorphic holds (F ") " = F proof let A, B be Category; ::_thesis: for F being Functor of A,B st F is isomorphic holds (F ") " = F let F be Functor of A,B; ::_thesis: ( F is isomorphic implies (F ") " = F ) reconsider f = F as Function of the carrier' of A, the carrier' of B ; reconsider g = F " as Function of the carrier' of B, the carrier' of A ; assume A1: F is isomorphic ; ::_thesis: (F ") " = F then A2: F is one-to-one by CAT_1:def_25; thus (F ") " = g " by A1, Def2, Th10 .= (f ") " by A1, Def2 .= F by A2, FUNCT_1:43 ; ::_thesis: verum end; theorem Th13: :: ISOCAT_1:13 for B, A being Category for F being Functor of A,B st F is isomorphic holds ( F * (F ") = id B & (F ") * F = id A ) proof let B, A be Category; ::_thesis: for F being Functor of A,B st F is isomorphic holds ( F * (F ") = id B & (F ") * F = id A ) let F be Functor of A,B; ::_thesis: ( F is isomorphic implies ( F * (F ") = id B & (F ") * F = id A ) ) reconsider f = F as Function of the carrier' of A, the carrier' of B ; A1: dom f = the carrier' of A by FUNCT_2:def_1; assume A2: F is isomorphic ; ::_thesis: ( F * (F ") = id B & (F ") * F = id A ) then A3: F is one-to-one by Def3; A4: rng f = the carrier' of B by A2, Def3; thus F * (F ") = f * (f ") by A2, Def2 .= id B by A3, A4, FUNCT_1:39 ; ::_thesis: (F ") * F = id A thus (F ") * F = (f ") * f by A2, Def2 .= id A by A3, A1, FUNCT_1:39 ; ::_thesis: verum end; theorem Th14: :: ISOCAT_1:14 for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st F is isomorphic & G is isomorphic holds G * F is isomorphic proof let A, B, C be Category; ::_thesis: for F being Functor of A,B for G being Functor of B,C st F is isomorphic & G is isomorphic holds G * F is isomorphic let F be Functor of A,B; ::_thesis: for G being Functor of B,C st F is isomorphic & G is isomorphic holds G * F is isomorphic let G be Functor of B,C; ::_thesis: ( F is isomorphic & G is isomorphic implies G * F is isomorphic ) assume that A1: F is one-to-one and A2: rng F = the carrier' of B and A3: G is one-to-one and A4: rng G = the carrier' of C ; :: according to ISOCAT_1:def_3 ::_thesis: G * F is isomorphic thus G * F is one-to-one by A1, A3, FUNCT_1:24; :: according to ISOCAT_1:def_3 ::_thesis: rng (G * F) = the carrier' of C dom G = the carrier' of B by FUNCT_2:def_1; hence rng (G * F) = the carrier' of C by A2, A4, RELAT_1:28; ::_thesis: verum end; definition let A, B be Category; predA,B are_isomorphic means :: ISOCAT_1:def 4 ex F being Functor of A,B st F is isomorphic ; reflexivity for A being Category ex F being Functor of A,A st F is isomorphic proof let A be Category; ::_thesis: ex F being Functor of A,A st F is isomorphic id A is isomorphic by CAT_1:80; hence ex F being Functor of A,A st F is isomorphic ; ::_thesis: verum end; symmetry for A, B being Category st ex F being Functor of A,B st F is isomorphic holds ex F being Functor of B,A st F is isomorphic proof let A, B be Category; ::_thesis: ( ex F being Functor of A,B st F is isomorphic implies ex F being Functor of B,A st F is isomorphic ) given F being Functor of A,B such that A1: F is isomorphic ; ::_thesis: ex F being Functor of B,A st F is isomorphic take F " ; ::_thesis: F " is isomorphic thus F " is isomorphic by A1, Th10; ::_thesis: verum end; end; :: deftheorem defines are_isomorphic ISOCAT_1:def_4_:_ for A, B being Category holds ( A,B are_isomorphic iff ex F being Functor of A,B st F is isomorphic ); notation let A, B be Category; synonym A ~= B for A,B are_isomorphic ; end; theorem :: ISOCAT_1:15 for A, B, C being Category st A ~= B & B ~= C holds A ~= C proof let A, B, C be Category; ::_thesis: ( A ~= B & B ~= C implies A ~= C ) given F1 being Functor of A,B such that A1: F1 is isomorphic ; :: according to ISOCAT_1:def_4 ::_thesis: ( not B ~= C or A ~= C ) given F2 being Functor of B,C such that A2: F2 is isomorphic ; :: according to ISOCAT_1:def_4 ::_thesis: A ~= C take F2 * F1 ; :: according to ISOCAT_1:def_4 ::_thesis: F2 * F1 is isomorphic thus F2 * F1 is isomorphic by A1, A2, Th14; ::_thesis: verum end; theorem :: ISOCAT_1:16 for A being Category for o, m being set holds [:(1Cat (o,m)),A:] ~= A proof let A be Category; ::_thesis: for o, m being set holds [:(1Cat (o,m)),A:] ~= A let o, m be set ; ::_thesis: [:(1Cat (o,m)),A:] ~= A take F = pr2 ((1Cat (o,m)),A); :: according to ISOCAT_1:def_4 ::_thesis: F is isomorphic set X = [: the carrier' of (1Cat (o,m)), the carrier' of A:]; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_[:_the_carrier'_of_(1Cat_(o,m)),_the_carrier'_of_A:]_&_x2_in_[:_the_carrier'_of_(1Cat_(o,m)),_the_carrier'_of_A:]_&_F_._x1_=_F_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] & x2 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] & F . x1 = F . x2 implies x1 = x2 ) assume x1 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] ; ::_thesis: ( x2 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] & F . x1 = F . x2 implies x1 = x2 ) then consider x11, x12 being set such that A1: x11 in the carrier' of (1Cat (o,m)) and A2: x12 in the carrier' of A and A3: x1 = [x11,x12] by ZFMISC_1:def_2; assume x2 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] ; ::_thesis: ( F . x1 = F . x2 implies x1 = x2 ) then consider x21, x22 being set such that A4: x21 in the carrier' of (1Cat (o,m)) and A5: x22 in the carrier' of A and A6: x2 = [x21,x22] by ZFMISC_1:def_2; reconsider f11 = x11, f21 = x21 as Morphism of (1Cat (o,m)) by A1, A4; assume A7: F . x1 = F . x2 ; ::_thesis: x1 = x2 reconsider f12 = x12, f22 = x22 as Morphism of A by A2, A5; A8: f11 = m by TARSKI:def_1 .= f21 by TARSKI:def_1 ; f12 = F . (f11,f12) by FUNCT_3:def_5 .= F . (f21,f22) by A3, A6, A7 .= f22 by FUNCT_3:def_5 ; hence x1 = x2 by A3, A6, A8; ::_thesis: verum end; hence F is one-to-one by FUNCT_2:19; :: according to ISOCAT_1:def_3 ::_thesis: rng F = the carrier' of A thus rng F = the carrier' of A by FUNCT_3:46; ::_thesis: verum end; theorem :: ISOCAT_1:17 for A, B being Category holds [:A,B:] ~= [:B,A:] proof let A, B be Category; ::_thesis: [:A,B:] ~= [:B,A:] take F = <:(pr2 (A,B)),(pr1 (A,B)):>; :: according to ISOCAT_1:def_4 ::_thesis: F is isomorphic A1: ( dom (pr1 (A,B)) = the carrier' of [:A,B:] & dom (pr2 (A,B)) = the carrier' of [:A,B:] ) by FUNCT_2:def_1; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_[:_the_carrier'_of_A,_the_carrier'_of_B:]_&_x2_in_[:_the_carrier'_of_A,_the_carrier'_of_B:]_&_F_._x1_=_F_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in [: the carrier' of A, the carrier' of B:] & x2 in [: the carrier' of A, the carrier' of B:] & F . x1 = F . x2 implies x1 = x2 ) assume x1 in [: the carrier' of A, the carrier' of B:] ; ::_thesis: ( x2 in [: the carrier' of A, the carrier' of B:] & F . x1 = F . x2 implies x1 = x2 ) then consider x11, x12 being set such that A2: x11 in the carrier' of A and A3: x12 in the carrier' of B and A4: x1 = [x11,x12] by ZFMISC_1:def_2; assume x2 in [: the carrier' of A, the carrier' of B:] ; ::_thesis: ( F . x1 = F . x2 implies x1 = x2 ) then consider x21, x22 being set such that A5: x21 in the carrier' of A and A6: x22 in the carrier' of B and A7: x2 = [x21,x22] by ZFMISC_1:def_2; reconsider f12 = x12, f22 = x22 as Morphism of B by A3, A6; reconsider f11 = x11, f21 = x21 as Morphism of A by A2, A5; A8: [f21,f22] in the carrier' of [:A,B:] ; assume A9: F . x1 = F . x2 ; ::_thesis: x1 = x2 A10: [f11,f12] in the carrier' of [:A,B:] ; A11: [f12,f11] = [f12,((pr1 (A,B)) . (f11,f12))] by FUNCT_3:def_4 .= [((pr2 (A,B)) . (f11,f12)),((pr1 (A,B)) . (f11,f12))] by FUNCT_3:def_5 .= F . (f21,f22) by A1, A4, A7, A10, A9, FUNCT_3:49 .= [((pr2 (A,B)) . (f21,f22)),((pr1 (A,B)) . (f21,f22))] by A1, A8, FUNCT_3:49 .= [f22,((pr1 (A,B)) . (f21,f22))] by FUNCT_3:def_5 .= [f22,f21] by FUNCT_3:def_4 ; then x12 = x22 by XTUPLE_0:1; hence x1 = x2 by A4, A7, A11, XTUPLE_0:1; ::_thesis: verum end; hence F is one-to-one by FUNCT_2:19; :: according to ISOCAT_1:def_3 ::_thesis: rng F = the carrier' of [:B,A:] thus rng F c= the carrier' of [:B,A:] ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier' of [:B,A:] c= rng F let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of [:B,A:] or x in rng F ) assume x in the carrier' of [:B,A:] ; ::_thesis: x in rng F then consider x1, x2 being set such that A12: x1 in the carrier' of B and A13: x2 in the carrier' of A and A14: x = [x1,x2] by ZFMISC_1:def_2; reconsider x2 = x2 as Morphism of A by A13; reconsider x1 = x1 as Morphism of B by A12; F . [x2,x1] = [((pr2 (A,B)) . (x2,x1)),((pr1 (A,B)) . (x2,x1))] by A1, FUNCT_3:49 .= [x1,((pr1 (A,B)) . (x2,x1))] by FUNCT_3:def_5 .= [x1,x2] by FUNCT_3:def_4 ; hence x in rng F by A14, FUNCT_2:4; ::_thesis: verum end; theorem :: ISOCAT_1:18 for A, B, C being Category holds [:[:A,B:],C:] ~= [:A,[:B,C:]:] proof let A, B, C be Category; ::_thesis: [:[:A,B:],C:] ~= [:A,[:B,C:]:] set X = (pr1 (A,B)) * (pr1 ([:A,B:],C)); set Y = <:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):>; take F = <:((pr1 (A,B)) * (pr1 ([:A,B:],C))),<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):>:>; :: according to ISOCAT_1:def_4 ::_thesis: F is isomorphic A1: ( dom (pr2 ([:A,B:],C)) = the carrier' of [:[:A,B:],C:] & dom ((pr2 (A,B)) * (pr1 ([:A,B:],C))) = the carrier' of [:[:A,B:],C:] ) by FUNCT_2:def_1; A2: ( dom ((pr1 (A,B)) * (pr1 ([:A,B:],C))) = the carrier' of [:[:A,B:],C:] & dom <:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> = the carrier' of [:[:A,B:],C:] ) by FUNCT_2:def_1; now__::_thesis:_for_x,_y_being_set_st_x_in_[:[:_the_carrier'_of_A,_the_carrier'_of_B:],_the_carrier'_of_C:]_&_y_in_[:[:_the_carrier'_of_A,_the_carrier'_of_B:],_the_carrier'_of_C:]_&_F_._x_=_F_._y_holds_ x_=_y let x, y be set ; ::_thesis: ( x in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] & y in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] & F . x = F . y implies x = y ) assume x in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] ; ::_thesis: ( y in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] & F . x = F . y implies x = y ) then consider x1, x2 being set such that A3: x1 in [: the carrier' of A, the carrier' of B:] and A4: x2 in the carrier' of C and A5: x = [x1,x2] by ZFMISC_1:def_2; assume y in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] ; ::_thesis: ( F . x = F . y implies x = y ) then consider y1, y2 being set such that A6: y1 in [: the carrier' of A, the carrier' of B:] and A7: y2 in the carrier' of C and A8: y = [y1,y2] by ZFMISC_1:def_2; reconsider f2 = x2, g2 = y2 as Morphism of C by A4, A7; assume A9: F . x = F . y ; ::_thesis: x = y consider x11, x12 being set such that A10: x11 in the carrier' of A and A11: x12 in the carrier' of B and A12: x1 = [x11,x12] by A3, ZFMISC_1:def_2; consider y11, y12 being set such that A13: y11 in the carrier' of A and A14: y12 in the carrier' of B and A15: y1 = [y11,y12] by A6, ZFMISC_1:def_2; reconsider f12 = x12, g12 = y12 as Morphism of B by A11, A14; reconsider f11 = x11, g11 = y11 as Morphism of A by A10, A13; A16: [f11,[f12,f2]] = [((pr1 (A,B)) . (f11,f12)),[f12,f2]] by FUNCT_3:def_4 .= [((pr1 (A,B)) . ((pr1 ([:A,B:],C)) . ([f11,f12],f2))),[f12,f2]] by FUNCT_3:def_4 .= [((pr1 (A,B)) . ((pr1 ([:A,B:],C)) . [[f11,f12],f2])),[f12,f2]] .= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . ([f11,f12],f2)),[f12,f2]] by FUNCT_2:15 .= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),[((pr2 (A,B)) . (f11,f12)),f2]] by FUNCT_3:def_5 .= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),[((pr2 (A,B)) . ((pr1 ([:A,B:],C)) . ([f11,f12],f2))),f2]] by FUNCT_3:def_4 .= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),f2]] by FUNCT_2:15 .= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),((pr2 ([:A,B:],C)) . ([f11,f12],f2))]] by FUNCT_3:def_5 .= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[f11,f12],f2])] by A1, FUNCT_3:49 .= F . [[g11,g12],g2] by A2, A5, A12, A8, A15, A9, FUNCT_3:49 .= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[g11,g12],g2])] by A2, FUNCT_3:49 .= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),((pr2 ([:A,B:],C)) . ([g11,g12],g2))]] by A1, FUNCT_3:49 .= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),g2]] by FUNCT_3:def_5 .= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[((pr2 (A,B)) . ((pr1 ([:A,B:],C)) . ([g11,g12],g2))),g2]] by FUNCT_2:15 .= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[((pr2 (A,B)) . (g11,g12)),g2]] by FUNCT_3:def_4 .= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[g12,g2]] by FUNCT_3:def_5 .= [((pr1 (A,B)) . ((pr1 ([:A,B:],C)) . ([g11,g12],g2))),[g12,g2]] by FUNCT_2:15 .= [((pr1 (A,B)) . (g11,g12)),[g12,g2]] by FUNCT_3:def_4 .= [g11,[g12,g2]] by FUNCT_3:def_4 ; then [x12,x2] = [y12,y2] by XTUPLE_0:1; then ( x12 = y12 & x2 = y2 ) by XTUPLE_0:1; hence x = y by A5, A12, A8, A15, A16, XTUPLE_0:1; ::_thesis: verum end; hence F is one-to-one by FUNCT_2:19; :: according to ISOCAT_1:def_3 ::_thesis: rng F = the carrier' of [:A,[:B,C:]:] thus rng F c= the carrier' of [:A,[:B,C:]:] ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier' of [:A,[:B,C:]:] c= rng F let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of [:A,[:B,C:]:] or x in rng F ) assume x in the carrier' of [:A,[:B,C:]:] ; ::_thesis: x in rng F then consider x1, x2 being set such that A17: x1 in the carrier' of A and A18: x2 in the carrier' of [:B,C:] and A19: x = [x1,x2] by ZFMISC_1:def_2; reconsider x1 = x1 as Morphism of A by A17; consider x21, x22 being set such that A20: x21 in the carrier' of B and A21: x22 in the carrier' of C and A22: x2 = [x21,x22] by A18, ZFMISC_1:def_2; reconsider x22 = x22 as Morphism of C by A21; reconsider x21 = x21 as Morphism of B by A20; F . [[x1,x21],x22] = [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[x1,x21],x22]),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[x1,x21],x22])] by A2, FUNCT_3:49 .= [((pr1 (A,B)) . ((pr1 ([:A,B:],C)) . ([x1,x21],x22))),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[x1,x21],x22])] by FUNCT_2:15 .= [((pr1 (A,B)) . (x1,x21)),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[x1,x21],x22])] by FUNCT_3:def_4 .= [x1,(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[x1,x21],x22])] by FUNCT_3:def_4 .= [x1,[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[x1,x21],x22]),((pr2 ([:A,B:],C)) . [[x1,x21],x22])]] by A1, FUNCT_3:49 .= [x1,[((pr2 (A,B)) . ((pr1 ([:A,B:],C)) . ([x1,x21],x22))),((pr2 ([:A,B:],C)) . [[x1,x21],x22])]] by FUNCT_2:15 .= [x1,[((pr2 (A,B)) . (x1,x21)),((pr2 ([:A,B:],C)) . ([x1,x21],x22))]] by FUNCT_3:def_4 .= [x1,[x21,((pr2 ([:A,B:],C)) . ([x1,x21],x22))]] by FUNCT_3:def_5 .= [x1,[x21,x22]] by FUNCT_3:def_5 ; hence x in rng F by A19, A22, FUNCT_2:4; ::_thesis: verum end; theorem :: ISOCAT_1:19 for A, B, C, D being Category st A ~= B & C ~= D holds [:A,C:] ~= [:B,D:] proof let A, B, C, D be Category; ::_thesis: ( A ~= B & C ~= D implies [:A,C:] ~= [:B,D:] ) given F being Functor of A,B such that A1: F is isomorphic ; :: according to ISOCAT_1:def_4 ::_thesis: ( not C ~= D or [:A,C:] ~= [:B,D:] ) A2: F is one-to-one by A1, Def3; given G being Functor of C,D such that A3: G is isomorphic ; :: according to ISOCAT_1:def_4 ::_thesis: [:A,C:] ~= [:B,D:] take [:F,G:] ; :: according to ISOCAT_1:def_4 ::_thesis: [:F,G:] is isomorphic G is one-to-one by A3, Def3; hence [:F,G:] is one-to-one by A2; :: according to ISOCAT_1:def_3 ::_thesis: rng [:F,G:] = the carrier' of [:B,D:] thus rng [:F,G:] = [:(rng F),(rng G):] by FUNCT_3:67 .= [: the carrier' of B,(rng G):] by A1, Def3 .= the carrier' of [:B,D:] by A3, Def3 ; ::_thesis: verum end; definition let A, B, C be Category; let F1, F2 be Functor of A,B; assume B1: F1 is_transformable_to F2 ; let t be transformation of F1,F2; let G be Functor of B,C; funcG * t -> transformation of G * F1,G * F2 equals :Def5: :: ISOCAT_1:def 5 G * t; coherence G * t is transformation of G * F1,G * F2 proof reconsider Gt = G * t as Function of the carrier of A, the carrier' of C ; Gt is transformation of G * F1,G * F2 proof thus G * F1 is_transformable_to G * F2 by B1, Th5; :: according to NATTRA_1:def_3 ::_thesis: for b1 being M2( the carrier of A) holds Gt . b1 is Morphism of (G * F1) . b1,(G * F2) . b1 let a be Object of A; ::_thesis: Gt . a is Morphism of (G * F1) . a,(G * F2) . a A1: ( G . (F1 . a) = (G * F1) . a & G . (F2 . a) = (G * F2) . a ) by CAT_1:76; t . a in Hom ((F1 . a),(F2 . a)) by B1, Th4; then A2: G . (t . a) in Hom (((G * F1) . a),((G * F2) . a)) by A1, CAT_1:81; Gt . a = G . (t . a) by FUNCT_2:15 .= G . (t . a) by B1, NATTRA_1:def_5 ; hence Gt . a is Morphism of (G * F1) . a,(G * F2) . a by A2, CAT_1:def_5; ::_thesis: verum end; hence G * t is transformation of G * F1,G * F2 ; ::_thesis: verum end; correctness ; end; :: deftheorem Def5 defines * ISOCAT_1:def_5_:_ for A, B, C being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 for G being Functor of B,C holds G * t = G * t; definition let A, B, C be Category; let G1, G2 be Functor of B,C; assume B1: G1 is_transformable_to G2 ; let F be Functor of A,B; let t be transformation of G1,G2; funct * F -> transformation of G1 * F,G2 * F equals :Def6: :: ISOCAT_1:def 6 t * (Obj F); coherence t * (Obj F) is transformation of G1 * F,G2 * F proof reconsider tF = t * (Obj F) as Function of the carrier of A, the carrier' of C ; tF is transformation of G1 * F,G2 * F proof thus G1 * F is_transformable_to G2 * F by B1, Th5; :: according to NATTRA_1:def_3 ::_thesis: for b1 being M2( the carrier of A) holds tF . b1 is Morphism of (G1 * F) . b1,(G2 * F) . b1 let a be Object of A; ::_thesis: tF . a is Morphism of (G1 * F) . a,(G2 * F) . a A1: G1 . (F . a) = (G1 * F) . a by CAT_1:76; tF . a = t . ((Obj F) . a) by FUNCT_2:15 .= t . (F . a) by B1, NATTRA_1:def_5 ; hence tF . a is Morphism of (G1 * F) . a,(G2 * F) . a by A1, CAT_1:76; ::_thesis: verum end; hence t * (Obj F) is transformation of G1 * F,G2 * F ; ::_thesis: verum end; correctness ; end; :: deftheorem Def6 defines * ISOCAT_1:def_6_:_ for A, B, C being Category for G1, G2 being Functor of B,C st G1 is_transformable_to G2 holds for F being Functor of A,B for t being transformation of G1,G2 holds t * F = t * (Obj F); theorem Th20: :: ISOCAT_1:20 for B, C, A being Category for G1, G2 being Functor of B,C st G1 is_transformable_to G2 holds for F being Functor of A,B for t being transformation of G1,G2 for a being Object of A holds (t * F) . a = t . (F . a) proof let B, C, A be Category; ::_thesis: for G1, G2 being Functor of B,C st G1 is_transformable_to G2 holds for F being Functor of A,B for t being transformation of G1,G2 for a being Object of A holds (t * F) . a = t . (F . a) let G1, G2 be Functor of B,C; ::_thesis: ( G1 is_transformable_to G2 implies for F being Functor of A,B for t being transformation of G1,G2 for a being Object of A holds (t * F) . a = t . (F . a) ) assume A1: G1 is_transformable_to G2 ; ::_thesis: for F being Functor of A,B for t being transformation of G1,G2 for a being Object of A holds (t * F) . a = t . (F . a) let F be Functor of A,B; ::_thesis: for t being transformation of G1,G2 for a being Object of A holds (t * F) . a = t . (F . a) let t be transformation of G1,G2; ::_thesis: for a being Object of A holds (t * F) . a = t . (F . a) let a be Object of A; ::_thesis: (t * F) . a = t . (F . a) thus (t * F) . a = (t * F) . a by A1, Th5, NATTRA_1:def_5 .= (t * (Obj F)) . a by A1, Def6 .= t . ((Obj F) . a) by FUNCT_2:15 .= t . (F . a) by A1, NATTRA_1:def_5 ; ::_thesis: verum end; theorem Th21: :: ISOCAT_1:21 for A, B, C being Category for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 for G being Functor of B,C for a being Object of A holds (G * t) . a = G /. (t . a) proof let A, B, C be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds for t being transformation of F1,F2 for G being Functor of B,C for a being Object of A holds (G * t) . a = G /. (t . a) let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2 for G being Functor of B,C for a being Object of A holds (G * t) . a = G /. (t . a) ) assume A1: F1 is_transformable_to F2 ; ::_thesis: for t being transformation of F1,F2 for G being Functor of B,C for a being Object of A holds (G * t) . a = G /. (t . a) let t be transformation of F1,F2; ::_thesis: for G being Functor of B,C for a being Object of A holds (G * t) . a = G /. (t . a) let G be Functor of B,C; ::_thesis: for a being Object of A holds (G * t) . a = G /. (t . a) let a be Object of A; ::_thesis: (G * t) . a = G /. (t . a) A2: Hom ((F1 . a),(F2 . a)) <> {} by A1, NATTRA_1:def_2; thus (G * t) . a = (G * t) . a by A1, Th5, NATTRA_1:def_5 .= (G * t) . a by A1, Def5 .= G . (t . a) by FUNCT_2:15 .= G . (t . a) by A1, NATTRA_1:def_5 .= G /. (t . a) by A2, CAT_3:def_10 ; ::_thesis: verum end; theorem Th22: :: ISOCAT_1:22 for A, B, C being Category for F1, F2 being Functor of A,B for G1, G2 being Functor of B,C st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds G1 * F1 is_naturally_transformable_to G2 * F2 proof let A, B, C be Category; ::_thesis: for F1, F2 being Functor of A,B for G1, G2 being Functor of B,C st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds G1 * F1 is_naturally_transformable_to G2 * F2 let F1, F2 be Functor of A,B; ::_thesis: for G1, G2 being Functor of B,C st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds G1 * F1 is_naturally_transformable_to G2 * F2 let G1, G2 be Functor of B,C; ::_thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies G1 * F1 is_naturally_transformable_to G2 * F2 ) assume that A1: F1 is_naturally_transformable_to F2 and A2: G1 is_naturally_transformable_to G2 ; ::_thesis: G1 * F1 is_naturally_transformable_to G2 * F2 set t1 = the natural_transformation of F1,F2; set t2 = the natural_transformation of G1,G2; A3: G1 is_transformable_to G2 by A2, NATTRA_1:def_7; A4: F1 is_transformable_to F2 by A1, NATTRA_1:def_7; hence A5: G1 * F1 is_transformable_to G2 * F2 by A3, Th5; :: according to NATTRA_1:def_7 ::_thesis: ex b1 being transformation of G1 * F1,G2 * F2 st for b2, b3 being M2( the carrier of A) holds ( Hom (b2,b3) = {} or for b4 being Morphism of b2,b3 holds (b1 . b3) * ((G1 * F1) /. b4) = ((G2 * F2) /. b4) * (b1 . b2) ) take t = ( the natural_transformation of G1,G2 * F2) `*` (G1 * the natural_transformation of F1,F2); ::_thesis: for b1, b2 being M2( the carrier of A) holds ( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (t . b2) * ((G1 * F1) /. b3) = ((G2 * F2) /. b3) * (t . b1) ) let a, b be Object of A; ::_thesis: ( Hom (a,b) = {} or for b1 being Morphism of a,b holds (t . b) * ((G1 * F1) /. b1) = ((G2 * F2) /. b1) * (t . a) ) A6: Hom ((G1 . (F2 . b)),(G2 . (F2 . b))) <> {} by A3, NATTRA_1:def_2; A7: Hom (((G1 * F1) . a),((G2 * F2) . a)) <> {} by A5, NATTRA_1:def_2; A8: G1 * F1 is_transformable_to G1 * F2 by A4, Th5; then A9: Hom (((G1 * F1) . b),((G1 * F2) . b)) <> {} by NATTRA_1:def_2; A10: Hom (((G1 * F1) . b),((G2 * F2) . b)) <> {} by A5, NATTRA_1:def_2; assume A11: Hom (a,b) <> {} ; ::_thesis: for b1 being Morphism of a,b holds (t . b) * ((G1 * F1) /. b1) = ((G2 * F2) /. b1) * (t . a) then A12: Hom (((G2 * F2) . a),((G2 * F2) . b)) <> {} by CAT_1:84; A13: Hom ((F1 . b),(F2 . b)) <> {} by A4, NATTRA_1:def_2; then A14: Hom ((G1 . (F1 . b)),(G1 . (F2 . b))) <> {} by CAT_1:84; then A15: Hom ((G1 . (F1 . b)),(G2 . (F2 . b))) <> {} by A6, CAT_1:24; A16: G1 * F2 is_transformable_to G2 * F2 by A3, Th5; then A17: Hom (((G1 * F2) . b),((G2 * F2) . b)) <> {} by NATTRA_1:def_2; A18: Hom (((G1 * F1) . a),((G1 * F2) . a)) <> {} by A8, NATTRA_1:def_2; A19: Hom (((G1 * F2) . a),((G2 * F2) . a)) <> {} by A16, NATTRA_1:def_2; A20: Hom ((F1 . a),(F2 . a)) <> {} by A4, NATTRA_1:def_2; then A21: Hom ((G1 . (F1 . a)),(G1 . (F2 . a))) <> {} by CAT_1:84; let f be Morphism of a,b; ::_thesis: (t . b) * ((G1 * F1) /. f) = ((G2 * F2) /. f) * (t . a) A22: Hom ((F2 . a),(F2 . b)) <> {} by A11, CAT_1:84; then A23: Hom ((G1 . (F2 . a)),(G1 . (F2 . b))) <> {} by CAT_1:84; A24: Hom ((F1 . a),(F1 . b)) <> {} by A11, CAT_1:84; then A25: Hom ((G1 . (F1 . a)),(G1 . (F1 . b))) <> {} by CAT_1:84; A26: Hom ((G1 . (F2 . a)),(G2 . (F2 . a))) <> {} by A3, NATTRA_1:def_2; then A27: Hom ((G1 . (F1 . a)),(G2 . (F2 . a))) <> {} by A21, CAT_1:24; A28: Hom ((G2 . (F2 . a)),(G2 . (F2 . b))) <> {} by A22, CAT_1:84; Hom (((G1 * F1) . a),((G1 * F1) . b)) <> {} by A11, CAT_1:84; hence (t . b) * ((G1 * F1) /. f) = (t . b) (*) ((G1 * F1) /. f) by A10, CAT_1:def_13 .= (t . b) (*) (G1 /. (F1 /. f)) by A11, NATTRA_1:11 .= ((( the natural_transformation of G1,G2 * F2) . b) * ((G1 * the natural_transformation of F1,F2) . b)) (*) (G1 /. (F1 /. f)) by A8, A16, NATTRA_1:def_6 .= ((( the natural_transformation of G1,G2 * F2) . b) (*) ((G1 * the natural_transformation of F1,F2) . b)) (*) (G1 /. (F1 /. f)) by A17, A9, CAT_1:def_13 .= ((( the natural_transformation of G1,G2 * F2) . b) (*) (G1 /. ( the natural_transformation of F1,F2 . b))) (*) (G1 /. (F1 /. f)) by A4, Th21 .= (( the natural_transformation of G1,G2 . (F2 . b)) (*) (G1 /. ( the natural_transformation of F1,F2 . b))) (*) (G1 /. (F1 /. f)) by A3, Th20 .= (( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. ( the natural_transformation of F1,F2 . b))) (*) (G1 /. (F1 /. f)) by A6, A14, CAT_1:def_13 .= (( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. ( the natural_transformation of F1,F2 . b))) * (G1 /. (F1 /. f)) by A25, A15, CAT_1:def_13 .= ( the natural_transformation of G1,G2 . (F2 . b)) * ((G1 /. ( the natural_transformation of F1,F2 . b)) * (G1 /. (F1 /. f))) by A6, A14, A25, CAT_1:25 .= ( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. (( the natural_transformation of F1,F2 . b) * (F1 /. f))) by A13, A24, NATTRA_1:13 .= ( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. ((F2 /. f) * ( the natural_transformation of F1,F2 . a))) by A1, A11, NATTRA_1:def_8 .= ( the natural_transformation of G1,G2 . (F2 . b)) * ((G1 /. (F2 /. f)) * (G1 /. ( the natural_transformation of F1,F2 . a))) by A22, A20, NATTRA_1:13 .= (( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. (F2 /. f))) * (G1 /. ( the natural_transformation of F1,F2 . a)) by A6, A23, A21, CAT_1:25 .= ((G2 /. (F2 /. f)) * ( the natural_transformation of G1,G2 . (F2 . a))) * (G1 /. ( the natural_transformation of F1,F2 . a)) by A2, A22, NATTRA_1:def_8 .= (G2 /. (F2 /. f)) * (( the natural_transformation of G1,G2 . (F2 . a)) * (G1 /. ( the natural_transformation of F1,F2 . a))) by A21, A28, A26, CAT_1:25 .= (G2 /. (F2 /. f)) (*) (( the natural_transformation of G1,G2 . (F2 . a)) * (G1 /. ( the natural_transformation of F1,F2 . a))) by A28, A27, CAT_1:def_13 .= (G2 /. (F2 /. f)) (*) (( the natural_transformation of G1,G2 . (F2 . a)) (*) (G1 /. ( the natural_transformation of F1,F2 . a))) by A21, A26, CAT_1:def_13 .= (G2 /. (F2 /. f)) (*) ((( the natural_transformation of G1,G2 * F2) . a) (*) (G1 /. ( the natural_transformation of F1,F2 . a))) by A3, Th20 .= (G2 /. (F2 /. f)) (*) ((( the natural_transformation of G1,G2 * F2) . a) (*) ((G1 * the natural_transformation of F1,F2) . a)) by A4, Th21 .= (G2 /. (F2 /. f)) (*) ((( the natural_transformation of G1,G2 * F2) . a) * ((G1 * the natural_transformation of F1,F2) . a)) by A19, A18, CAT_1:def_13 .= (G2 /. (F2 /. f)) (*) (t . a) by A8, A16, NATTRA_1:def_6 .= ((G2 * F2) /. f) (*) (t . a) by A11, NATTRA_1:11 .= ((G2 * F2) /. f) * (t . a) by A7, A12, CAT_1:def_13 ; ::_thesis: verum end; definition let A, B, C be Category; let F1, F2 be Functor of A,B; assume B1: F1 is_naturally_transformable_to F2 ; let t be natural_transformation of F1,F2; let G be Functor of B,C; funcG * t -> natural_transformation of G * F1,G * F2 equals :Def7: :: ISOCAT_1:def 7 G * t; coherence G * t is natural_transformation of G * F1,G * F2 proof A1: F1 is_transformable_to F2 by B1, NATTRA_1:def_7; G * t is natural_transformation of G * F1,G * F2 proof thus G * F1 is_naturally_transformable_to G * F2 by B1, Th22; :: according to NATTRA_1:def_8 ::_thesis: for b1, b2 being M2( the carrier of A) holds ( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds ((G * t) . b2) * ((G * F1) /. b3) = ((G * F2) /. b3) * ((G * t) . b1) ) then A2: G * F1 is_transformable_to G * F2 by NATTRA_1:def_7; let a, b be Object of A; ::_thesis: ( Hom (a,b) = {} or for b1 being Morphism of a,b holds ((G * t) . b) * ((G * F1) /. b1) = ((G * F2) /. b1) * ((G * t) . a) ) assume A3: Hom (a,b) <> {} ; ::_thesis: for b1 being Morphism of a,b holds ((G * t) . b) * ((G * F1) /. b1) = ((G * F2) /. b1) * ((G * t) . a) A4: Hom (((G * F1) . a),((G * F1) . b)) <> {} by A3, CAT_1:84; A5: Hom (((G * F2) . a),((G * F2) . b)) <> {} by A3, CAT_1:84; A6: Hom (((G * F1) . a),((G * F2) . a)) <> {} by A2, NATTRA_1:def_2; let f be Morphism of a,b; ::_thesis: ((G * t) . b) * ((G * F1) /. f) = ((G * F2) /. f) * ((G * t) . a) A7: Hom ((F1 . b),(F2 . b)) <> {} by A1, NATTRA_1:def_2; then A8: Hom ((G . (F1 . b)),(G . (F2 . b))) <> {} by CAT_1:84; A9: Hom ((F1 . a),(F2 . a)) <> {} by A1, NATTRA_1:def_2; then A10: Hom ((G . (F1 . a)),(G . (F2 . a))) <> {} by CAT_1:84; A11: Hom ((F2 . a),(F2 . b)) <> {} by A3, CAT_1:84; then A12: Hom ((G . (F2 . a)),(G . (F2 . b))) <> {} by CAT_1:84; A13: Hom ((F1 . a),(F1 . b)) <> {} by A3, CAT_1:84; then A14: Hom ((G . (F1 . a)),(G . (F1 . b))) <> {} by CAT_1:84; Hom (((G * F1) . b),((G * F2) . b)) <> {} by A2, NATTRA_1:def_2; hence ((G * t) . b) * ((G * F1) /. f) = ((G * t) . b) (*) ((G * F1) /. f) by A4, CAT_1:def_13 .= ((G * t) . b) (*) (G /. (F1 /. f)) by A3, NATTRA_1:11 .= (G /. (t . b)) (*) (G /. (F1 /. f)) by A1, Th21 .= (G /. (t . b)) * (G /. (F1 /. f)) by A8, A14, CAT_1:def_13 .= G /. ((t . b) * (F1 /. f)) by A7, A13, NATTRA_1:13 .= G /. ((F2 /. f) * (t . a)) by B1, A3, NATTRA_1:def_8 .= (G /. (F2 /. f)) * (G /. (t . a)) by A9, A11, NATTRA_1:13 .= (G /. (F2 /. f)) (*) (G /. (t . a)) by A12, A10, CAT_1:def_13 .= (G /. (F2 /. f)) (*) ((G * t) . a) by A1, Th21 .= ((G * F2) /. f) (*) ((G * t) . a) by A3, NATTRA_1:11 .= ((G * F2) /. f) * ((G * t) . a) by A6, A5, CAT_1:def_13 ; ::_thesis: verum end; hence G * t is natural_transformation of G * F1,G * F2 ; ::_thesis: verum end; correctness ; end; :: deftheorem Def7 defines * ISOCAT_1:def_7_:_ for A, B, C being Category for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds for t being natural_transformation of F1,F2 for G being Functor of B,C holds G * t = G * t; theorem Th23: :: ISOCAT_1:23 for A, B, C being Category for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds for t being natural_transformation of F1,F2 for G being Functor of B,C for a being Object of A holds (G * t) . a = G /. (t . a) proof let A, B, C be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds for t being natural_transformation of F1,F2 for G being Functor of B,C for a being Object of A holds (G * t) . a = G /. (t . a) let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 for G being Functor of B,C for a being Object of A holds (G * t) . a = G /. (t . a) ) assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 for G being Functor of B,C for a being Object of A holds (G * t) . a = G /. (t . a) then A2: F1 is_transformable_to F2 by NATTRA_1:def_7; let t be natural_transformation of F1,F2; ::_thesis: for G being Functor of B,C for a being Object of A holds (G * t) . a = G /. (t . a) let G be Functor of B,C; ::_thesis: for a being Object of A holds (G * t) . a = G /. (t . a) let a be Object of A; ::_thesis: (G * t) . a = G /. (t . a) thus (G * t) . a = (G * t) . a by A1, Def7 .= G /. (t . a) by A2, Th21 ; ::_thesis: verum end; definition let A, B, C be Category; let G1, G2 be Functor of B,C; assume B1: G1 is_naturally_transformable_to G2 ; let F be Functor of A,B; let t be natural_transformation of G1,G2; funct * F -> natural_transformation of G1 * F,G2 * F equals :Def8: :: ISOCAT_1:def 8 t * F; coherence t * F is natural_transformation of G1 * F,G2 * F proof A1: G1 is_transformable_to G2 by B1, NATTRA_1:def_7; t * F is natural_transformation of G1 * F,G2 * F proof thus G1 * F is_naturally_transformable_to G2 * F by B1, Th22; :: according to NATTRA_1:def_8 ::_thesis: for b1, b2 being M2( the carrier of A) holds ( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds ((t * F) . b2) * ((G1 * F) /. b3) = ((G2 * F) /. b3) * ((t * F) . b1) ) then A2: G1 * F is_transformable_to G2 * F by NATTRA_1:def_7; let a, b be Object of A; ::_thesis: ( Hom (a,b) = {} or for b1 being Morphism of a,b holds ((t * F) . b) * ((G1 * F) /. b1) = ((G2 * F) /. b1) * ((t * F) . a) ) A3: Hom (((G1 * F) . b),((G2 * F) . b)) <> {} by A2, NATTRA_1:def_2; A4: Hom (((G1 * F) . a),((G2 * F) . a)) <> {} by A2, NATTRA_1:def_2; assume A5: Hom (a,b) <> {} ; ::_thesis: for b1 being Morphism of a,b holds ((t * F) . b) * ((G1 * F) /. b1) = ((G2 * F) /. b1) * ((t * F) . a) then A6: Hom (((G2 * F) . a),((G2 * F) . b)) <> {} by CAT_1:84; let f be Morphism of a,b; ::_thesis: ((t * F) . b) * ((G1 * F) /. f) = ((G2 * F) /. f) * ((t * F) . a) A7: Hom ((F . a),(F . b)) <> {} by A5, CAT_1:84; then A8: Hom ((G1 . (F . a)),(G1 . (F . b))) <> {} by CAT_1:84; A9: Hom ((G1 . (F . a)),(G2 . (F . a))) <> {} by A1, NATTRA_1:def_2; A10: Hom ((G1 . (F . b)),(G2 . (F . b))) <> {} by A1, NATTRA_1:def_2; A11: Hom ((G2 . (F . a)),(G2 . (F . b))) <> {} by A7, CAT_1:84; Hom (((G1 * F) . a),((G1 * F) . b)) <> {} by A5, CAT_1:84; hence ((t * F) . b) * ((G1 * F) /. f) = ((t * F) . b) (*) ((G1 * F) /. f) by A3, CAT_1:def_13 .= ((t * F) . b) (*) (G1 /. (F /. f)) by A5, NATTRA_1:11 .= (t . (F . b)) (*) (G1 /. (F /. f)) by A1, Th20 .= (t . (F . b)) * (G1 /. (F /. f)) by A10, A8, CAT_1:def_13 .= (G2 /. (F /. f)) * (t . (F . a)) by B1, A7, NATTRA_1:def_8 .= (G2 /. (F /. f)) (*) (t . (F . a)) by A11, A9, CAT_1:def_13 .= (G2 /. (F /. f)) (*) ((t * F) . a) by A1, Th20 .= ((G2 * F) /. f) (*) ((t * F) . a) by A5, NATTRA_1:11 .= ((G2 * F) /. f) * ((t * F) . a) by A6, A4, CAT_1:def_13 ; ::_thesis: verum end; hence t * F is natural_transformation of G1 * F,G2 * F ; ::_thesis: verum end; correctness ; end; :: deftheorem Def8 defines * ISOCAT_1:def_8_:_ for A, B, C being Category for G1, G2 being Functor of B,C st G1 is_naturally_transformable_to G2 holds for F being Functor of A,B for t being natural_transformation of G1,G2 holds t * F = t * F; theorem Th24: :: ISOCAT_1:24 for B, C, A being Category for G1, G2 being Functor of B,C st G1 is_naturally_transformable_to G2 holds for F being Functor of A,B for t being natural_transformation of G1,G2 for a being Object of A holds (t * F) . a = t . (F . a) proof let B, C, A be Category; ::_thesis: for G1, G2 being Functor of B,C st G1 is_naturally_transformable_to G2 holds for F being Functor of A,B for t being natural_transformation of G1,G2 for a being Object of A holds (t * F) . a = t . (F . a) let G1, G2 be Functor of B,C; ::_thesis: ( G1 is_naturally_transformable_to G2 implies for F being Functor of A,B for t being natural_transformation of G1,G2 for a being Object of A holds (t * F) . a = t . (F . a) ) assume A1: G1 is_naturally_transformable_to G2 ; ::_thesis: for F being Functor of A,B for t being natural_transformation of G1,G2 for a being Object of A holds (t * F) . a = t . (F . a) then A2: G1 is_transformable_to G2 by NATTRA_1:def_7; let F be Functor of A,B; ::_thesis: for t being natural_transformation of G1,G2 for a being Object of A holds (t * F) . a = t . (F . a) let t be natural_transformation of G1,G2; ::_thesis: for a being Object of A holds (t * F) . a = t . (F . a) let a be Object of A; ::_thesis: (t * F) . a = t . (F . a) thus (t * F) . a = (t * F) . a by A1, Def8 .= t . (F . a) by A2, Th20 ; ::_thesis: verum end; theorem Th25: :: ISOCAT_1:25 for B, A being Category for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} proof let B, A be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} ) assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} let a be Object of A; ::_thesis: Hom ((F1 . a),(F2 . a)) <> {} F1 is_transformable_to F2 by A1, NATTRA_1:def_7; hence Hom ((F1 . a),(F2 . a)) <> {} by NATTRA_1:def_2; ::_thesis: verum end; theorem Th26: :: ISOCAT_1:26 for B, A being Category for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds for t1, t2 being natural_transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds t1 = t2 proof let B, A be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds for t1, t2 being natural_transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds t1 = t2 let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t1, t2 being natural_transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds t1 = t2 ) assume F1 is_naturally_transformable_to F2 ; ::_thesis: for t1, t2 being natural_transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds t1 = t2 then F1 is_transformable_to F2 by NATTRA_1:def_7; hence for t1, t2 being natural_transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds t1 = t2 by NATTRA_1:19; ::_thesis: verum end; theorem Th27: :: ISOCAT_1:27 for C, A, B being Category for F1, F2, F3 being Functor of A,B for G being Functor of B,C for s being natural_transformation of F1,F2 for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds G * (s9 `*` s) = (G * s9) `*` (G * s) proof let C, A, B be Category; ::_thesis: for F1, F2, F3 being Functor of A,B for G being Functor of B,C for s being natural_transformation of F1,F2 for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds G * (s9 `*` s) = (G * s9) `*` (G * s) let F1, F2, F3 be Functor of A,B; ::_thesis: for G being Functor of B,C for s being natural_transformation of F1,F2 for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds G * (s9 `*` s) = (G * s9) `*` (G * s) let G be Functor of B,C; ::_thesis: for s being natural_transformation of F1,F2 for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds G * (s9 `*` s) = (G * s9) `*` (G * s) let s be natural_transformation of F1,F2; ::_thesis: for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds G * (s9 `*` s) = (G * s9) `*` (G * s) let s9 be natural_transformation of F2,F3; ::_thesis: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies G * (s9 `*` s) = (G * s9) `*` (G * s) ) assume A1: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) ; ::_thesis: G * (s9 `*` s) = (G * s9) `*` (G * s) then A2: ( G * F1 is_naturally_transformable_to G * F2 & G * F2 is_naturally_transformable_to G * F3 ) by Th22; now__::_thesis:_for_a_being_Object_of_A_holds_(G_*_(s9_`*`_s))_._a_=_((G_*_s9)_`*`_(G_*_s))_._a let a be Object of A; ::_thesis: (G * (s9 `*` s)) . a = ((G * s9) `*` (G * s)) . a A3: ( G . (F1 . a) = (G * F1) . a & G . (F2 . a) = (G * F2) . a ) by CAT_1:76; A4: G . (F3 . a) = (G * F3) . a by CAT_1:76; A5: ( Hom ((F1 . a),(F2 . a)) <> {} & Hom ((F2 . a),(F3 . a)) <> {} ) by A1, Th25; A6: ( G /. (s9 . a) = (G * s9) . a & G /. (s . a) = (G * s) . a ) by A1, Th23; thus (G * (s9 `*` s)) . a = G /. ((s9 `*` s) . a) by A1, Th23, NATTRA_1:23 .= G /. ((s9 . a) * (s . a)) by A1, NATTRA_1:25 .= (G /. (s9 . a)) * (G /. (s . a)) by A5, NATTRA_1:13 .= ((G * s9) `*` (G * s)) . a by A2, A6, A3, A4, NATTRA_1:25 ; ::_thesis: verum end; hence G * (s9 `*` s) = (G * s9) `*` (G * s) by A2, Th26, NATTRA_1:23; ::_thesis: verum end; theorem Th28: :: ISOCAT_1:28 for A, B, C being Category for F being Functor of A,B for G1, G2, G3 being Functor of B,C for t being natural_transformation of G1,G2 for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (t9 `*` t) * F = (t9 * F) `*` (t * F) proof let A, B, C be Category; ::_thesis: for F being Functor of A,B for G1, G2, G3 being Functor of B,C for t being natural_transformation of G1,G2 for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (t9 `*` t) * F = (t9 * F) `*` (t * F) let F be Functor of A,B; ::_thesis: for G1, G2, G3 being Functor of B,C for t being natural_transformation of G1,G2 for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (t9 `*` t) * F = (t9 * F) `*` (t * F) let G1, G2, G3 be Functor of B,C; ::_thesis: for t being natural_transformation of G1,G2 for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (t9 `*` t) * F = (t9 * F) `*` (t * F) let t be natural_transformation of G1,G2; ::_thesis: for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (t9 `*` t) * F = (t9 * F) `*` (t * F) let t9 be natural_transformation of G2,G3; ::_thesis: ( G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 implies (t9 `*` t) * F = (t9 * F) `*` (t * F) ) assume A1: ( G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 ) ; ::_thesis: (t9 `*` t) * F = (t9 * F) `*` (t * F) then A2: ( G1 * F is_naturally_transformable_to G2 * F & G2 * F is_naturally_transformable_to G3 * F ) by Th22; now__::_thesis:_for_a_being_Object_of_A_holds_((t9_`*`_t)_*_F)_._a_=_((t9_*_F)_`*`_(t_*_F))_._a let a be Object of A; ::_thesis: ((t9 `*` t) * F) . a = ((t9 * F) `*` (t * F)) . a A3: ( G1 . (F . a) = (G1 * F) . a & G2 . (F . a) = (G2 * F) . a ) by CAT_1:76; A4: G3 . (F . a) = (G3 * F) . a by CAT_1:76; A5: ( t9 . (F . a) = (t9 * F) . a & t . (F . a) = (t * F) . a ) by A1, Th24; thus ((t9 `*` t) * F) . a = (t9 `*` t) . (F . a) by A1, Th24, NATTRA_1:23 .= (t9 . (F . a)) * (t . (F . a)) by A1, NATTRA_1:25 .= ((t9 * F) `*` (t * F)) . a by A2, A5, A3, A4, NATTRA_1:25 ; ::_thesis: verum end; hence (t9 `*` t) * F = (t9 * F) `*` (t * F) by A2, Th26, NATTRA_1:23; ::_thesis: verum end; theorem Th29: :: ISOCAT_1:29 for A, B, C, D being Category for F being Functor of A,B for G being Functor of B,C for H1, H2 being Functor of C,D for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds (u * G) * F = u * (G * F) proof let A, B, C, D be Category; ::_thesis: for F being Functor of A,B for G being Functor of B,C for H1, H2 being Functor of C,D for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds (u * G) * F = u * (G * F) let F be Functor of A,B; ::_thesis: for G being Functor of B,C for H1, H2 being Functor of C,D for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds (u * G) * F = u * (G * F) let G be Functor of B,C; ::_thesis: for H1, H2 being Functor of C,D for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds (u * G) * F = u * (G * F) let H1, H2 be Functor of C,D; ::_thesis: for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds (u * G) * F = u * (G * F) let u be natural_transformation of H1,H2; ::_thesis: ( H1 is_naturally_transformable_to H2 implies (u * G) * F = u * (G * F) ) assume A1: H1 is_naturally_transformable_to H2 ; ::_thesis: (u * G) * F = u * (G * F) A2: H1 * (G * F) = (H1 * G) * F by RELAT_1:36; then reconsider v = u * (G * F) as natural_transformation of (H1 * G) * F,(H2 * G) * F by RELAT_1:36; A3: H2 * (G * F) = (H2 * G) * F by RELAT_1:36; A4: now__::_thesis:_for_a_being_Object_of_A_holds_((u_*_G)_*_F)_._a_=_v_._a let a be Object of A; ::_thesis: ((u * G) * F) . a = v . a thus ((u * G) * F) . a = (u * G) . (F . a) by A1, Th22, Th24 .= u . (G . (F . a)) by A1, Th24 .= u . ((G * F) . a) by CAT_1:76 .= v . a by A1, A2, A3, Th24 ; ::_thesis: verum end; H1 * G is_naturally_transformable_to H2 * G by A1, Th22; hence (u * G) * F = u * (G * F) by A4, Th22, Th26; ::_thesis: verum end; theorem Th30: :: ISOCAT_1:30 for A, D, B, C being Category for F being Functor of A,B for G1, G2 being Functor of B,C for H being Functor of C,D for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds (H * t) * F = H * (t * F) proof let A, D, B, C be Category; ::_thesis: for F being Functor of A,B for G1, G2 being Functor of B,C for H being Functor of C,D for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds (H * t) * F = H * (t * F) let F be Functor of A,B; ::_thesis: for G1, G2 being Functor of B,C for H being Functor of C,D for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds (H * t) * F = H * (t * F) let G1, G2 be Functor of B,C; ::_thesis: for H being Functor of C,D for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds (H * t) * F = H * (t * F) let H be Functor of C,D; ::_thesis: for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds (H * t) * F = H * (t * F) let t be natural_transformation of G1,G2; ::_thesis: ( G1 is_naturally_transformable_to G2 implies (H * t) * F = H * (t * F) ) assume A1: G1 is_naturally_transformable_to G2 ; ::_thesis: (H * t) * F = H * (t * F) A2: H * (G1 * F) = (H * G1) * F by RELAT_1:36; then reconsider v = H * (t * F) as natural_transformation of (H * G1) * F,(H * G2) * F by RELAT_1:36; A3: H * (G2 * F) = (H * G2) * F by RELAT_1:36; A4: now__::_thesis:_for_a_being_Object_of_A_holds_((H_*_t)_*_F)_._a_=_v_._a let a be Object of A; ::_thesis: ((H * t) * F) . a = v . a A5: ( G1 . (F . a) = (G1 * F) . a & G2 . (F . a) = (G2 * F) . a ) by CAT_1:76; thus ((H * t) * F) . a = (H * t) . (F . a) by A1, Th22, Th24 .= H /. (t . (F . a)) by A1, Th23 .= H /. ((t * F) . a) by A1, A5, Th24 .= v . a by A1, A2, A3, Th22, Th23 ; ::_thesis: verum end; H * G1 is_naturally_transformable_to H * G2 by A1, Th22; hence (H * t) * F = H * (t * F) by A4, Th22, Th26; ::_thesis: verum end; theorem Th31: :: ISOCAT_1:31 for C, D, A, B being Category for F1, F2 being Functor of A,B for G being Functor of B,C for H being Functor of C,D for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds (H * G) * s = H * (G * s) proof let C, D, A, B be Category; ::_thesis: for F1, F2 being Functor of A,B for G being Functor of B,C for H being Functor of C,D for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds (H * G) * s = H * (G * s) let F1, F2 be Functor of A,B; ::_thesis: for G being Functor of B,C for H being Functor of C,D for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds (H * G) * s = H * (G * s) let G be Functor of B,C; ::_thesis: for H being Functor of C,D for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds (H * G) * s = H * (G * s) let H be Functor of C,D; ::_thesis: for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds (H * G) * s = H * (G * s) let s be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 implies (H * G) * s = H * (G * s) ) assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: (H * G) * s = H * (G * s) A2: H * (G * F1) = (H * G) * F1 by RELAT_1:36; then reconsider v = H * (G * s) as natural_transformation of (H * G) * F1,(H * G) * F2 by RELAT_1:36; A3: H * (G * F2) = (H * G) * F2 by RELAT_1:36; now__::_thesis:_for_a_being_Object_of_A_holds_((H_*_G)_*_s)_._a_=_v_._a let a be Object of A; ::_thesis: ((H * G) * s) . a = v . a A4: ( G . (F1 . a) = (G * F1) . a & G . (F2 . a) = (G * F2) . a ) by CAT_1:76; A5: Hom ((F1 . a),(F2 . a)) <> {} by A1, Th25; thus ((H * G) * s) . a = (H * G) /. (s . a) by A1, Th23 .= H /. (G /. (s . a)) by A5, NATTRA_1:11 .= H /. ((G * s) . a) by A1, A4, Th23 .= v . a by A1, A2, A3, Th22, Th23 ; ::_thesis: verum end; hence (H * G) * s = H * (G * s) by A1, Th22, Th26; ::_thesis: verum end; theorem Th32: :: ISOCAT_1:32 for A, B, C being Category for F being Functor of A,B for G being Functor of B,C holds (id G) * F = id (G * F) proof let A, B, C be Category; ::_thesis: for F being Functor of A,B for G being Functor of B,C holds (id G) * F = id (G * F) let F be Functor of A,B; ::_thesis: for G being Functor of B,C holds (id G) * F = id (G * F) let G be Functor of B,C; ::_thesis: (id G) * F = id (G * F) now__::_thesis:_for_a_being_Object_of_A_holds_((id_G)_*_F)_._a_=_(id_(G_*_F))_._a let a be Object of A; ::_thesis: ((id G) * F) . a = (id (G * F)) . a thus ((id G) * F) . a = (id G) . (F . a) by Th24 .= id (G . (F . a)) by NATTRA_1:20 .= id ((G * F) . a) by CAT_1:76 .= (id (G * F)) . a by NATTRA_1:20 ; ::_thesis: verum end; hence (id G) * F = id (G * F) by Th26; ::_thesis: verum end; theorem Th33: :: ISOCAT_1:33 for A, B, C being Category for F being Functor of A,B for G being Functor of B,C holds G * (id F) = id (G * F) proof let A, B, C be Category; ::_thesis: for F being Functor of A,B for G being Functor of B,C holds G * (id F) = id (G * F) let F be Functor of A,B; ::_thesis: for G being Functor of B,C holds G * (id F) = id (G * F) let G be Functor of B,C; ::_thesis: G * (id F) = id (G * F) now__::_thesis:_for_a_being_Object_of_A_holds_(G_*_(id_F))_._a_=_(id_(G_*_F))_._a let a be Object of A; ::_thesis: (G * (id F)) . a = (id (G * F)) . a thus (G * (id F)) . a = G /. ((id F) . a) by Th23 .= G /. (id (F . a)) by NATTRA_1:20 .= id (G . (F . a)) by NATTRA_1:15 .= id ((G * F) . a) by CAT_1:76 .= (id (G * F)) . a by NATTRA_1:20 ; ::_thesis: verum end; hence G * (id F) = id (G * F) by Th26; ::_thesis: verum end; theorem Th34: :: ISOCAT_1:34 for C, B being Category for G1, G2 being Functor of B,C for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds t * (id B) = t proof let C, B be Category; ::_thesis: for G1, G2 being Functor of B,C for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds t * (id B) = t let G1, G2 be Functor of B,C; ::_thesis: for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds t * (id B) = t let t be natural_transformation of G1,G2; ::_thesis: ( G1 is_naturally_transformable_to G2 implies t * (id B) = t ) assume A1: G1 is_naturally_transformable_to G2 ; ::_thesis: t * (id B) = t A2: G1 * (id B) = G1 by FUNCT_2:17; then reconsider s = t * (id B) as natural_transformation of G1,G2 by FUNCT_2:17; A3: G2 * (id B) = G2 by FUNCT_2:17; now__::_thesis:_for_b_being_Object_of_B_holds_s_._b_=_t_._b let b be Object of B; ::_thesis: s . b = t . b thus s . b = t . ((id B) . b) by A1, A2, A3, Th24 .= t . b by CAT_1:79 ; ::_thesis: verum end; hence t * (id B) = t by A1, Th26; ::_thesis: verum end; theorem Th35: :: ISOCAT_1:35 for A, B being Category for F1, F2 being Functor of A,B for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds (id B) * s = s proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds (id B) * s = s let F1, F2 be Functor of A,B; ::_thesis: for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds (id B) * s = s let s be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 implies (id B) * s = s ) assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: (id B) * s = s A2: (id B) * F1 = F1 by FUNCT_2:17; then reconsider t = (id B) * s as natural_transformation of F1,F2 by FUNCT_2:17; A3: (id B) * F2 = F2 by FUNCT_2:17; now__::_thesis:_for_a_being_Object_of_A_holds_t_._a_=_s_._a let a be Object of A; ::_thesis: t . a = s . a A4: Hom ((F1 . a),(F2 . a)) <> {} by A1, Th25; thus t . a = (id B) /. (s . a) by A1, A2, A3, Th23 .= (id B) . (s . a) by A4, CAT_3:def_10 .= s . a by FUNCT_1:18 ; ::_thesis: verum end; hence (id B) * s = s by A1, Th26; ::_thesis: verum end; definition let A, B, C be Category; let F1, F2 be Functor of A,B; let G1, G2 be Functor of B,C; let s be natural_transformation of F1,F2; let t be natural_transformation of G1,G2; funct (#) s -> natural_transformation of G1 * F1,G2 * F2 equals :: ISOCAT_1:def 9 (t * F2) `*` (G1 * s); correctness coherence (t * F2) `*` (G1 * s) is natural_transformation of G1 * F1,G2 * F2; ; end; :: deftheorem defines (#) ISOCAT_1:def_9_:_ for A, B, C being Category for F1, F2 being Functor of A,B for G1, G2 being Functor of B,C for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 holds t (#) s = (t * F2) `*` (G1 * s); theorem Th36: :: ISOCAT_1:36 for A, B, C being Category for F1, F2 being Functor of A,B for G1, G2 being Functor of B,C for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds t (#) s = (G2 * s) `*` (t * F1) proof let A, B, C be Category; ::_thesis: for F1, F2 being Functor of A,B for G1, G2 being Functor of B,C for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds t (#) s = (G2 * s) `*` (t * F1) let F1, F2 be Functor of A,B; ::_thesis: for G1, G2 being Functor of B,C for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds t (#) s = (G2 * s) `*` (t * F1) let G1, G2 be Functor of B,C; ::_thesis: for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds t (#) s = (G2 * s) `*` (t * F1) let s be natural_transformation of F1,F2; ::_thesis: for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds t (#) s = (G2 * s) `*` (t * F1) let t be natural_transformation of G1,G2; ::_thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies t (#) s = (G2 * s) `*` (t * F1) ) assume that A1: F1 is_naturally_transformable_to F2 and A2: G1 is_naturally_transformable_to G2 ; ::_thesis: t (#) s = (G2 * s) `*` (t * F1) A3: ( G1 * F1 is_naturally_transformable_to G1 * F2 & G1 * F2 is_naturally_transformable_to G2 * F2 ) by A1, A2, Th22; A4: ( G2 * F1 is_naturally_transformable_to G2 * F2 & G1 * F1 is_naturally_transformable_to G2 * F1 ) by A1, A2, Th22; now__::_thesis:_for_a_being_Object_of_A_holds_((t_*_F2)_`*`_(G1_*_s))_._a_=_((G2_*_s)_`*`_(t_*_F1))_._a let a be Object of A; ::_thesis: ((t * F2) `*` (G1 * s)) . a = ((G2 * s) `*` (t * F1)) . a A5: ( (G1 * F1) . a = G1 . (F1 . a) & (G1 * F2) . a = G1 . (F2 . a) ) by CAT_1:76; A6: (G2 * F2) . a = G2 . (F2 . a) by CAT_1:76; A7: ( (G2 * s) . a = G2 /. (s . a) & (G1 * F1) . a = G1 . (F1 . a) ) by A1, Th23, CAT_1:76; A8: ( Hom ((F1 . a),(F2 . a)) <> {} & (t * F1) . a = t . (F1 . a) ) by A1, A2, Th24, Th25; A9: ( (G2 * F1) . a = G2 . (F1 . a) & (G2 * F2) . a = G2 . (F2 . a) ) by CAT_1:76; ( (t * F2) . a = t . (F2 . a) & (G1 * s) . a = G1 /. (s . a) ) by A1, A2, Th23, Th24; hence ((t * F2) `*` (G1 * s)) . a = (t . (F2 . a)) * (G1 /. (s . a)) by A3, A5, A6, NATTRA_1:25 .= ((G2 * s) . a) * ((t * F1) . a) by A2, A8, A7, A9, NATTRA_1:def_8 .= ((G2 * s) `*` (t * F1)) . a by A4, NATTRA_1:25 ; ::_thesis: verum end; hence t (#) s = (G2 * s) `*` (t * F1) by A3, Th26, NATTRA_1:23; ::_thesis: verum end; theorem :: ISOCAT_1:37 for A, B being Category for F1, F2 being Functor of A,B for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds (id (id B)) (#) s = s proof let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds (id (id B)) (#) s = s let F1, F2 be Functor of A,B; ::_thesis: for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds (id (id B)) (#) s = s let s be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 implies (id (id B)) (#) s = s ) assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: (id (id B)) (#) s = s then A2: (id B) * F1 is_naturally_transformable_to (id B) * F2 by Th22; thus (id (id B)) (#) s = (id ((id B) * F2)) `*` ((id B) * s) by Th32 .= (id B) * s by A2, NATTRA_1:24 .= s by A1, Th35 ; ::_thesis: verum end; theorem :: ISOCAT_1:38 for C, B being Category for G1, G2 being Functor of B,C for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds t (#) (id (id B)) = t proof let C, B be Category; ::_thesis: for G1, G2 being Functor of B,C for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds t (#) (id (id B)) = t let G1, G2 be Functor of B,C; ::_thesis: for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds t (#) (id (id B)) = t let t be natural_transformation of G1,G2; ::_thesis: ( G1 is_naturally_transformable_to G2 implies t (#) (id (id B)) = t ) assume A1: G1 is_naturally_transformable_to G2 ; ::_thesis: t (#) (id (id B)) = t then A2: G1 * (id B) is_naturally_transformable_to G2 * (id B) by Th22; thus t (#) (id (id B)) = (t * (id B)) `*` (id (G1 * (id B))) by Th33 .= t * (id B) by A2, NATTRA_1:24 .= t by A1, Th34 ; ::_thesis: verum end; theorem :: ISOCAT_1:39 for A, B, C, D being Category for F1, F2 being Functor of A,B for G1, G2 being Functor of B,C for H1, H2 being Functor of C,D for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds u (#) (t (#) s) = (u (#) t) (#) s proof let A, B, C, D be Category; ::_thesis: for F1, F2 being Functor of A,B for G1, G2 being Functor of B,C for H1, H2 being Functor of C,D for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds u (#) (t (#) s) = (u (#) t) (#) s let F1, F2 be Functor of A,B; ::_thesis: for G1, G2 being Functor of B,C for H1, H2 being Functor of C,D for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds u (#) (t (#) s) = (u (#) t) (#) s let G1, G2 be Functor of B,C; ::_thesis: for H1, H2 being Functor of C,D for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds u (#) (t (#) s) = (u (#) t) (#) s let H1, H2 be Functor of C,D; ::_thesis: for s being natural_transformation of F1,F2 for t being natural_transformation of G1,G2 for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds u (#) (t (#) s) = (u (#) t) (#) s let s be natural_transformation of F1,F2; ::_thesis: for t being natural_transformation of G1,G2 for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds u (#) (t (#) s) = (u (#) t) (#) s let t be natural_transformation of G1,G2; ::_thesis: for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds u (#) (t (#) s) = (u (#) t) (#) s let u be natural_transformation of H1,H2; ::_thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 implies u (#) (t (#) s) = (u (#) t) (#) s ) assume that A1: F1 is_naturally_transformable_to F2 and A2: G1 is_naturally_transformable_to G2 and A3: H1 is_naturally_transformable_to H2 ; ::_thesis: u (#) (t (#) s) = (u (#) t) (#) s A4: ( u * (G2 * F2) = (u * G2) * F2 & H1 * (t * F2) = (H1 * t) * F2 ) by A2, A3, Th29, Th30; A5: H1 * G1 is_naturally_transformable_to H1 * G2 by A2, Th22; then A6: (H1 * G1) * F2 is_naturally_transformable_to (H1 * G2) * F2 by Th22; A7: ( H1 * (G1 * s) = (H1 * G1) * s & (H1 * G1) * F1 is_naturally_transformable_to (H1 * G1) * F2 ) by A1, Th22, Th31; A8: ( (H1 * G1) * F1 = H1 * (G1 * F1) & (H1 * G1) * F2 = H1 * (G1 * F2) ) by RELAT_1:36; A9: H1 * G2 is_naturally_transformable_to H2 * G2 by A3, Th22; then A10: (H1 * G2) * F2 is_naturally_transformable_to (H2 * G2) * F2 by Th22; A11: ( (H1 * G2) * F2 = H1 * (G2 * F2) & (H2 * G2) * F2 = H2 * (G2 * F2) ) by RELAT_1:36; ( G1 * F2 is_naturally_transformable_to G2 * F2 & G1 * F1 is_naturally_transformable_to G1 * F2 ) by A1, A2, Th22; hence u (#) (t (#) s) = (u * (G2 * F2)) `*` ((H1 * (t * F2)) `*` (H1 * (G1 * s))) by Th27 .= (((u * G2) * F2) `*` ((H1 * t) * F2)) `*` ((H1 * G1) * s) by A8, A11, A4, A7, A6, A10, NATTRA_1:26 .= (u (#) t) (#) s by A5, A9, Th28 ; ::_thesis: verum end; theorem :: ISOCAT_1:40 for A, B, C being Category for F being Functor of A,B for G1, G2 being Functor of B,C for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds t * F = t (#) (id F) proof let A, B, C be Category; ::_thesis: for F being Functor of A,B for G1, G2 being Functor of B,C for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds t * F = t (#) (id F) let F be Functor of A,B; ::_thesis: for G1, G2 being Functor of B,C for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds t * F = t (#) (id F) let G1, G2 be Functor of B,C; ::_thesis: for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds t * F = t (#) (id F) let t be natural_transformation of G1,G2; ::_thesis: ( G1 is_naturally_transformable_to G2 implies t * F = t (#) (id F) ) assume G1 is_naturally_transformable_to G2 ; ::_thesis: t * F = t (#) (id F) then G1 * F is_naturally_transformable_to G2 * F by Th22; hence t * F = (t * F) `*` (id (G1 * F)) by NATTRA_1:24 .= t (#) (id F) by Th33 ; ::_thesis: verum end; theorem :: ISOCAT_1:41 for C, A, B being Category for F1, F2 being Functor of A,B for G being Functor of B,C for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds G * s = (id G) (#) s proof let C, A, B be Category; ::_thesis: for F1, F2 being Functor of A,B for G being Functor of B,C for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds G * s = (id G) (#) s let F1, F2 be Functor of A,B; ::_thesis: for G being Functor of B,C for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds G * s = (id G) (#) s let G be Functor of B,C; ::_thesis: for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds G * s = (id G) (#) s let s be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 implies G * s = (id G) (#) s ) assume F1 is_naturally_transformable_to F2 ; ::_thesis: G * s = (id G) (#) s then G * F1 is_naturally_transformable_to G * F2 by Th22; hence G * s = (id (G * F2)) `*` (G * s) by NATTRA_1:24 .= (id G) (#) s by Th32 ; ::_thesis: verum end; theorem :: ISOCAT_1:42 for A, B, C being Category for F1, F2, F3 being Functor of A,B for G1, G2, G3 being Functor of B,C for s being natural_transformation of F1,F2 for s9 being natural_transformation of F2,F3 for t being natural_transformation of G1,G2 for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s) proof let A, B, C be Category; ::_thesis: for F1, F2, F3 being Functor of A,B for G1, G2, G3 being Functor of B,C for s being natural_transformation of F1,F2 for s9 being natural_transformation of F2,F3 for t being natural_transformation of G1,G2 for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s) let F1, F2, F3 be Functor of A,B; ::_thesis: for G1, G2, G3 being Functor of B,C for s being natural_transformation of F1,F2 for s9 being natural_transformation of F2,F3 for t being natural_transformation of G1,G2 for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s) let G1, G2, G3 be Functor of B,C; ::_thesis: for s being natural_transformation of F1,F2 for s9 being natural_transformation of F2,F3 for t being natural_transformation of G1,G2 for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s) let s be natural_transformation of F1,F2; ::_thesis: for s9 being natural_transformation of F2,F3 for t being natural_transformation of G1,G2 for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s) let s9 be natural_transformation of F2,F3; ::_thesis: for t being natural_transformation of G1,G2 for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s) let t be natural_transformation of G1,G2; ::_thesis: for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s) let t9 be natural_transformation of G2,G3; ::_thesis: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 implies (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s) ) assume that A1: F1 is_naturally_transformable_to F2 and A2: F2 is_naturally_transformable_to F3 and A3: G1 is_naturally_transformable_to G2 and A4: G2 is_naturally_transformable_to G3 ; ::_thesis: (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s) A5: ( t9 (#) s9 = (G3 * s9) `*` (t9 * F2) & t (#) s = (G2 * s) `*` (t * F1) ) by A1, A2, A3, A4, Th36; A6: G1 * F1 is_naturally_transformable_to G2 * F1 by A3, Th22; A7: G2 * F1 is_naturally_transformable_to G2 * F2 by A1, Th22; then A8: G1 * F1 is_naturally_transformable_to G2 * F2 by A6, NATTRA_1:23; A9: G2 * F2 is_naturally_transformable_to G3 * F2 by A4, Th22; A10: G1 is_naturally_transformable_to G3 by A3, A4, NATTRA_1:23; then A11: G1 * F1 is_naturally_transformable_to G3 * F1 by Th22; A12: G3 * F1 is_naturally_transformable_to G3 * F2 by A1, Th22; A13: G2 * F1 is_naturally_transformable_to G3 * F1 by A4, Th22; A14: G3 * F2 is_naturally_transformable_to G3 * F3 by A2, Th22; F1 is_naturally_transformable_to F3 by A1, A2, NATTRA_1:23; hence (t9 `*` t) (#) (s9 `*` s) = (G3 * (s9 `*` s)) `*` ((t9 `*` t) * F1) by A10, Th36 .= ((G3 * s9) `*` (G3 * s)) `*` ((t9 `*` t) * F1) by A1, A2, Th27 .= ((G3 * s9) `*` (G3 * s)) `*` ((t9 * F1) `*` (t * F1)) by A3, A4, Th28 .= (G3 * s9) `*` ((G3 * s) `*` ((t9 * F1) `*` (t * F1))) by A14, A12, A11, NATTRA_1:26 .= (G3 * s9) `*` (((G3 * s) `*` (t9 * F1)) `*` (t * F1)) by A12, A6, A13, NATTRA_1:26 .= (G3 * s9) `*` ((t9 (#) s) `*` (t * F1)) by A1, A4, Th36 .= (G3 * s9) `*` ((t9 * F2) `*` ((G2 * s) `*` (t * F1))) by A6, A9, A7, NATTRA_1:26 .= (t9 (#) s9) `*` (t (#) s) by A14, A9, A8, A5, NATTRA_1:26 ; ::_thesis: verum end; theorem Th43: :: ISOCAT_1:43 for A, B, C, D being Category for F being Functor of A,B for G being Functor of C,D for I, J being Functor of B,C st I ~= J holds ( G * I ~= G * J & I * F ~= J * F ) proof let A, B, C, D be Category; ::_thesis: for F being Functor of A,B for G being Functor of C,D for I, J being Functor of B,C st I ~= J holds ( G * I ~= G * J & I * F ~= J * F ) let F be Functor of A,B; ::_thesis: for G being Functor of C,D for I, J being Functor of B,C st I ~= J holds ( G * I ~= G * J & I * F ~= J * F ) let G be Functor of C,D; ::_thesis: for I, J being Functor of B,C st I ~= J holds ( G * I ~= G * J & I * F ~= J * F ) let I, J be Functor of B,C; ::_thesis: ( I ~= J implies ( G * I ~= G * J & I * F ~= J * F ) ) assume A1: I is_naturally_transformable_to J ; :: according to NATTRA_1:def_11 ::_thesis: ( for b1 being natural_transformation of I,J holds not b1 is invertible or ( G * I ~= G * J & I * F ~= J * F ) ) given t being natural_transformation of I,J such that A2: t is invertible ; ::_thesis: ( G * I ~= G * J & I * F ~= J * F ) thus G * I ~= G * J ::_thesis: I * F ~= J * F proof thus G * I is_naturally_transformable_to G * J by A1, Th22; :: according to NATTRA_1:def_11 ::_thesis: ex b1 being natural_transformation of G * I,G * J st b1 is invertible take G * t ; ::_thesis: G * t is invertible let b be Object of B; :: according to NATTRA_1:def_10 ::_thesis: (G * t) . b is invertible A3: t . b is invertible by A2, NATTRA_1:def_10; A4: ( G . (I . b) = (G * I) . b & G . (J . b) = (G * J) . b ) by CAT_1:76; (G * t) . b = G /. (t . b) by A1, Th23; hence (G * t) . b is invertible by A3, Th3, A4; ::_thesis: verum end; thus I * F is_naturally_transformable_to J * F by A1, Th22; :: according to NATTRA_1:def_11 ::_thesis: ex b1 being natural_transformation of I * F,J * F st b1 is invertible take t * F ; ::_thesis: t * F is invertible let a be Object of A; :: according to NATTRA_1:def_10 ::_thesis: (t * F) . a is invertible A5: ( I . (F . a) = (I * F) . a & J . (F . a) = (J * F) . a ) by CAT_1:76; (t * F) . a = t . (F . a) by A1, Th24; hence (t * F) . a is invertible by A2, A5, NATTRA_1:def_10; ::_thesis: verum end; theorem Th44: :: ISOCAT_1:44 for A, B being Category for F being Functor of A,B for G being Functor of B,A for I being Functor of A,A st I ~= id A holds ( F * I ~= F & I * G ~= G ) proof let A, B be Category; ::_thesis: for F being Functor of A,B for G being Functor of B,A for I being Functor of A,A st I ~= id A holds ( F * I ~= F & I * G ~= G ) let F be Functor of A,B; ::_thesis: for G being Functor of B,A for I being Functor of A,A st I ~= id A holds ( F * I ~= F & I * G ~= G ) let G be Functor of B,A; ::_thesis: for I being Functor of A,A st I ~= id A holds ( F * I ~= F & I * G ~= G ) let I be Functor of A,A; ::_thesis: ( I ~= id A implies ( F * I ~= F & I * G ~= G ) ) ( F * (id A) = F & (id A) * G = G ) by FUNCT_2:17; hence ( I ~= id A implies ( F * I ~= F & I * G ~= G ) ) by Th43; ::_thesis: verum end; definition let A, B be Category; predA is_equivalent_with B means :Def10: :: ISOCAT_1:def 10 ex F being Functor of A,B ex G being Functor of B,A st ( G * F ~= id A & F * G ~= id B ); reflexivity for A being Category ex F, G being Functor of A,A st ( G * F ~= id A & F * G ~= id A ) proof let A be Category; ::_thesis: ex F, G being Functor of A,A st ( G * F ~= id A & F * G ~= id A ) take id A ; ::_thesis: ex G being Functor of A,A st ( G * (id A) ~= id A & (id A) * G ~= id A ) take id A ; ::_thesis: ( (id A) * (id A) ~= id A & (id A) * (id A) ~= id A ) thus ( (id A) * (id A) ~= id A & (id A) * (id A) ~= id A ) by FUNCT_2:17; ::_thesis: verum end; symmetry for A, B being Category st ex F being Functor of A,B ex G being Functor of B,A st ( G * F ~= id A & F * G ~= id B ) holds ex F being Functor of B,A ex G being Functor of A,B st ( G * F ~= id B & F * G ~= id A ) ; end; :: deftheorem Def10 defines is_equivalent_with ISOCAT_1:def_10_:_ for A, B being Category holds ( A is_equivalent_with B iff ex F being Functor of A,B ex G being Functor of B,A st ( G * F ~= id A & F * G ~= id B ) ); notation let A, B be Category; synonym A,B are_equivalent for A is_equivalent_with B; end; theorem :: ISOCAT_1:45 for A, B being Category st A ~= B holds A is_equivalent_with B proof let A, B be Category; ::_thesis: ( A ~= B implies A is_equivalent_with B ) given F being Functor of A,B such that A1: F is isomorphic ; :: according to ISOCAT_1:def_4 ::_thesis: A is_equivalent_with B take F ; :: according to ISOCAT_1:def_10 ::_thesis: ex G being Functor of B,A st ( G * F ~= id A & F * G ~= id B ) take F " ; ::_thesis: ( (F ") * F ~= id A & F * (F ") ~= id B ) thus ( (F ") * F ~= id A & F * (F ") ~= id B ) by A1, Th13; ::_thesis: verum end; theorem Th46: :: ISOCAT_1:46 for A, B, C being Category st A,B are_equivalent & B,C are_equivalent holds A,C are_equivalent proof let A, B, C be Category; ::_thesis: ( A,B are_equivalent & B,C are_equivalent implies A,C are_equivalent ) given F1 being Functor of A,B, G1 being Functor of B,A such that A1: G1 * F1 ~= id A and A2: F1 * G1 ~= id B ; :: according to ISOCAT_1:def_10 ::_thesis: ( not B,C are_equivalent or A,C are_equivalent ) given F2 being Functor of B,C, G2 being Functor of C,B such that A3: G2 * F2 ~= id B and A4: F2 * G2 ~= id C ; :: according to ISOCAT_1:def_10 ::_thesis: A,C are_equivalent take F2 * F1 ; :: according to ISOCAT_1:def_10 ::_thesis: ex G being Functor of C,A st ( G * (F2 * F1) ~= id A & (F2 * F1) * G ~= id C ) take G1 * G2 ; ::_thesis: ( (G1 * G2) * (F2 * F1) ~= id A & (F2 * F1) * (G1 * G2) ~= id C ) (G1 * G2) * F2 = G1 * (G2 * F2) by RELAT_1:36; then A5: (G1 * G2) * F2 ~= G1 by A3, Th44; (G1 * G2) * (F2 * F1) = ((G1 * G2) * F2) * F1 by RELAT_1:36; then (G1 * G2) * (F2 * F1) ~= G1 * F1 by A5, Th43; hence (G1 * G2) * (F2 * F1) ~= id A by A1, NATTRA_1:29; ::_thesis: (F2 * F1) * (G1 * G2) ~= id C (F2 * F1) * G1 = F2 * (F1 * G1) by RELAT_1:36; then A6: (F2 * F1) * G1 ~= F2 by A2, Th44; (F2 * F1) * (G1 * G2) = ((F2 * F1) * G1) * G2 by RELAT_1:36; then (F2 * F1) * (G1 * G2) ~= F2 * G2 by A6, Th43; hence (F2 * F1) * (G1 * G2) ~= id C by A4, NATTRA_1:29; ::_thesis: verum end; definition let A, B be Category; assume A1: A,B are_equivalent ; mode Equivalence of A,B -> Functor of A,B means :Def11: :: ISOCAT_1:def 11 ex G being Functor of B,A st ( G * it ~= id A & it * G ~= id B ); existence ex b1 being Functor of A,B ex G being Functor of B,A st ( G * b1 ~= id A & b1 * G ~= id B ) by A1, Def10; end; :: deftheorem Def11 defines Equivalence ISOCAT_1:def_11_:_ for A, B being Category st A,B are_equivalent holds for b3 being Functor of A,B holds ( b3 is Equivalence of A,B iff ex G being Functor of B,A st ( G * b3 ~= id A & b3 * G ~= id B ) ); theorem :: ISOCAT_1:47 for A being Category holds id A is Equivalence of A,A proof let A be Category; ::_thesis: id A is Equivalence of A,A thus A is_equivalent_with A ; :: according to ISOCAT_1:def_11 ::_thesis: ex G being Functor of A,A st ( G * (id A) ~= id A & (id A) * G ~= id A ) take id A ; ::_thesis: ( (id A) * (id A) ~= id A & (id A) * (id A) ~= id A ) thus ( (id A) * (id A) ~= id A & (id A) * (id A) ~= id A ) by FUNCT_2:17; ::_thesis: verum end; theorem :: ISOCAT_1:48 for A, B, C being Category st A,B are_equivalent & B,C are_equivalent holds for F being Equivalence of A,B for G being Equivalence of B,C holds G * F is Equivalence of A,C proof let A, B, C be Category; ::_thesis: ( A,B are_equivalent & B,C are_equivalent implies for F being Equivalence of A,B for G being Equivalence of B,C holds G * F is Equivalence of A,C ) assume that A1: A,B are_equivalent and A2: B,C are_equivalent ; ::_thesis: for F being Equivalence of A,B for G being Equivalence of B,C holds G * F is Equivalence of A,C let F be Equivalence of A,B; ::_thesis: for G being Equivalence of B,C holds G * F is Equivalence of A,C let G be Equivalence of B,C; ::_thesis: G * F is Equivalence of A,C thus A,C are_equivalent by A1, A2, Th46; :: according to ISOCAT_1:def_11 ::_thesis: ex G being Functor of C,A st ( G * (G * F) ~= id A & (G * F) * G ~= id C ) consider F9 being Functor of B,A such that A3: F9 * F ~= id A and A4: F * F9 ~= id B by A1, Def11; (G * F) * F9 = G * (F * F9) by RELAT_1:36; then A5: (G * F) * F9 ~= G by A4, Th44; consider G9 being Functor of C,B such that A6: G9 * G ~= id B and A7: G * G9 ~= id C by A2, Def11; take F9 * G9 ; ::_thesis: ( (F9 * G9) * (G * F) ~= id A & (G * F) * (F9 * G9) ~= id C ) (F9 * G9) * G = F9 * (G9 * G) by RELAT_1:36; then A8: (F9 * G9) * G ~= F9 by A6, Th44; (F9 * G9) * (G * F) = ((F9 * G9) * G) * F by RELAT_1:36; then (F9 * G9) * (G * F) ~= F9 * F by A8, Th43; hence (F9 * G9) * (G * F) ~= id A by A3, NATTRA_1:29; ::_thesis: (G * F) * (F9 * G9) ~= id C (G * F) * (F9 * G9) = ((G * F) * F9) * G9 by RELAT_1:36; then (G * F) * (F9 * G9) ~= G * G9 by A5, Th43; hence (G * F) * (F9 * G9) ~= id C by A7, NATTRA_1:29; ::_thesis: verum end; theorem Th49: :: ISOCAT_1:49 for A, B being Category st A,B are_equivalent holds for F being Equivalence of A,B ex G being Equivalence of B,A st ( G * F ~= id A & F * G ~= id B ) proof let A, B be Category; ::_thesis: ( A,B are_equivalent implies for F being Equivalence of A,B ex G being Equivalence of B,A st ( G * F ~= id A & F * G ~= id B ) ) assume A1: A,B are_equivalent ; ::_thesis: for F being Equivalence of A,B ex G being Equivalence of B,A st ( G * F ~= id A & F * G ~= id B ) let F be Equivalence of A,B; ::_thesis: ex G being Equivalence of B,A st ( G * F ~= id A & F * G ~= id B ) consider G being Functor of B,A such that A2: ( G * F ~= id A & F * G ~= id B ) by A1, Def11; G is Equivalence of B,A proof thus B,A are_equivalent by A1; :: according to ISOCAT_1:def_11 ::_thesis: ex G being Functor of A,B st ( G * G ~= id B & G * G ~= id A ) take F ; ::_thesis: ( F * G ~= id B & G * F ~= id A ) thus ( F * G ~= id B & G * F ~= id A ) by A2; ::_thesis: verum end; hence ex G being Equivalence of B,A st ( G * F ~= id A & F * G ~= id B ) by A2; ::_thesis: verum end; theorem Th50: :: ISOCAT_1:50 for A, B being Category for F being Functor of A,B for G being Functor of B,A st G * F ~= id A holds F is faithful proof let A, B be Category; ::_thesis: for F being Functor of A,B for G being Functor of B,A st G * F ~= id A holds F is faithful let F be Functor of A,B; ::_thesis: for G being Functor of B,A st G * F ~= id A holds F is faithful let G be Functor of B,A; ::_thesis: ( G * F ~= id A implies F is faithful ) assume G * F ~= id A ; ::_thesis: F is faithful then A1: id A ~= G * F by NATTRA_1:28; then A2: id A is_naturally_transformable_to G * F by NATTRA_1:def_11; consider s being natural_transformation of id A,G * F such that A3: s is invertible by A1, NATTRA_1:def_11; thus F is faithful ::_thesis: verum proof let a, a9 be Object of A; :: according to CAT_1:def_27 ::_thesis: ( Hom (a,a9) = {} or for b1, b2 being Morphism of a,a9 holds ( not F . b1 = F . b2 or b1 = b2 ) ) assume A4: Hom (a,a9) <> {} ; ::_thesis: for b1, b2 being Morphism of a,a9 holds ( not F . b1 = F . b2 or b1 = b2 ) then A5: Hom (((id A) . a),((id A) . a9)) <> {} by CAT_1:84; let f1, f2 be Morphism of a,a9; ::_thesis: ( not F . f1 = F . f2 or f1 = f2 ) assume A6: F . f1 = F . f2 ; ::_thesis: f1 = f2 A7: (G * F) /. f1 = (G * F) . f1 by A4, CAT_3:def_10 .= G . (F . f2) by A6, FUNCT_2:15 .= (G * F) . f2 by FUNCT_2:15 .= (G * F) /. f2 by A4, CAT_3:def_10 ; A8: (s . a9) * ((id A) /. f1) = ((G * F) /. f1) * (s . a) by A2, A4, NATTRA_1:def_8 .= (s . a9) * ((id A) /. f2) by A2, A4, A7, NATTRA_1:def_8 ; A9: Hom (((id A) . a9),((G * F) . a9)) <> {} by A2, Th25; s . a9 is invertible by A3, NATTRA_1:def_10; then A10: s . a9 is monic by CAT_1:43; thus f1 = (id A) /. f1 by A4, NATTRA_1:16 .= (id A) /. f2 by A5, A9, A10, A8, CAT_1:31 .= f2 by A4, NATTRA_1:16 ; ::_thesis: verum end; end; theorem :: ISOCAT_1:51 for A, B being Category st A,B are_equivalent holds for F being Equivalence of A,B holds ( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) ) proof let A, B be Category; ::_thesis: ( A,B are_equivalent implies for F being Equivalence of A,B holds ( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) ) ) assume A1: A,B are_equivalent ; ::_thesis: for F being Equivalence of A,B holds ( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) ) let F be Equivalence of A,B; ::_thesis: ( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) ) consider G being Equivalence of B,A such that A2: G * F ~= id A and A3: F * G ~= id B by A1, Th49; A4: id A ~= G * F by A2, NATTRA_1:28; then A5: id A is_naturally_transformable_to G * F by NATTRA_1:def_11; consider s being natural_transformation of id A,G * F such that A6: s is invertible by A4, NATTRA_1:def_11; A7: G is faithful by A3, Th50; thus F is full ::_thesis: ( F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) ) proof let a, a9 be Object of A; :: according to CAT_1:def_26 ::_thesis: ( Hom ((F . a),(F . a9)) = {} or for b1 being Morphism of F . a,F . a9 holds ( not Hom (a,a9) = {} & ex b2 being Morphism of a,a9 st b1 = F . b2 ) ) assume A8: Hom ((F . a),(F . a9)) <> {} ; ::_thesis: for b1 being Morphism of F . a,F . a9 holds ( not Hom (a,a9) = {} & ex b2 being Morphism of a,a9 st b1 = F . b2 ) reconsider f2 = s . a9 as Morphism of a9,(G * F) . a9 by CAT_1:79; reconsider f1 = s . a as Morphism of a,(G * F) . a by CAT_1:79; A9: s . a9 is invertible by A6, NATTRA_1:def_10; A10: Hom (((id A) . a9),((G * F) . a9)) <> {} by A5, Th25; let g be Morphism of F . a,F . a9; ::_thesis: ( not Hom (a,a9) = {} & ex b1 being Morphism of a,a9 st g = F . b1 ) A11: (G * F) . a = G . (F . a) by CAT_1:76; then reconsider h = G /. g as Morphism of (G * F) . a,(G * F) . a9 by CAT_1:76; A12: Hom (((id A) . a),((G * F) . a)) <> {} by A5, Th25; (G * F) . a9 = G . (F . a9) by CAT_1:76; then A13: Hom (((G * F) . a),((G * F) . a9)) <> {} by A8, A11, CAT_1:84; then A14: Hom (((id A) . a),((G * F) . a9)) <> {} by A12, CAT_1:24; s . a is invertible by A6, NATTRA_1:def_10; then A15: s . a is epi by CAT_1:43; G * F is_naturally_transformable_to id A by A2, NATTRA_1:def_11; then A16: Hom (((G * F) . a9),((id A) . a9)) <> {} by Th25; A17: ( (id A) . a = a & (id A) . a9 = a9 ) by CAT_1:79; hence A18: Hom (a,a9) <> {} by A16, A14, CAT_1:24; ::_thesis: ex b1 being Morphism of a,a9 st g = F . b1 take f = (f2 ") * (h * f1); ::_thesis: g = F . f A19: (id A) /. f = ((s . a9) ") * (h * (s . a)) by A17, A18, NATTRA_1:16; h * (s . a) = (id ((G * F) . a9)) * (h * (s . a)) by A14, CAT_1:28 .= ((s . a9) * ((s . a9) ")) * (h * (s . a)) by A9, CAT_1:def_17 .= (s . a9) * ((id A) /. f) by A16, A14, A10, A19, CAT_1:25 .= ((G * F) /. f) * (s . a) by A5, A18, NATTRA_1:def_8 ; then A20: h = (G * F) /. f by A12, A13, A15, CAT_1:36; G . g = G /. g by A8, CAT_3:def_10 .= (G * F) . f by A18, A20, CAT_3:def_10 .= G . (F . f) by FUNCT_2:15 .= G . (F /. f) by A18, CAT_3:def_10 ; hence g = F /. f by A7, A8, CAT_1:def_27 .= F . f by A18, CAT_3:def_10 ; ::_thesis: verum end; thus F is faithful by A2, Th50; ::_thesis: for b being Object of B ex a being Object of A st b,F . a are_isomorphic let b be Object of B; ::_thesis: ex a being Object of A st b,F . a are_isomorphic take G . b ; ::_thesis: b,F . (G . b) are_isomorphic A21: ( F . (G . b) = (F * G) . b & (id B) . b = b ) by CAT_1:76, CAT_1:79; A22: id B ~= F * G by A3, NATTRA_1:28; then id B is_naturally_transformable_to F * G by NATTRA_1:def_11; then A23: id B is_transformable_to F * G by NATTRA_1:def_7; ex t being natural_transformation of id B,F * G st t is invertible by A22, NATTRA_1:def_11; hence b,F . (G . b) are_isomorphic by A21, A23, Th6; ::_thesis: verum end; definition let C be Category; deffunc H1( Object of C) -> Morphism of \$1,\$1 = id \$1; func IdMap C -> Function of the carrier of C, the carrier' of C means :: ISOCAT_1:def 12 for o being Object of C holds it . o = id o; existence ex b1 being Function of the carrier of C, the carrier' of C st for o being Object of C holds b1 . o = id o proof deffunc H2( Object of C) -> Morphism of \$1,\$1 = id \$1; consider f being Function of the carrier of C, the carrier' of C such that A1: for o being Object of C holds f . o = H2(o) from FUNCT_2:sch_4(); take f ; ::_thesis: for o being Object of C holds f . o = id o thus for o being Object of C holds f . o = id o by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of the carrier of C, the carrier' of C st ( for o being Object of C holds b1 . o = id o ) & ( for o being Object of C holds b2 . o = id o ) holds b1 = b2 proof let F, G be Function of the carrier of C, the carrier' of C; ::_thesis: ( ( for o being Object of C holds F . o = id o ) & ( for o being Object of C holds G . o = id o ) implies F = G ) assume that A2: for o being Object of C holds F . o = id o and A3: for o being Object of C holds G . o = id o ; ::_thesis: F = G let o be Object of C; :: according to FUNCT_2:def_8 ::_thesis: F . o = G . o thus F . o = id o by A2 .= G . o by A3 ; ::_thesis: verum end; end; :: deftheorem defines IdMap ISOCAT_1:def_12_:_ for C being Category for b2 being Function of the carrier of C, the carrier' of C holds ( b2 = IdMap C iff for o being Object of C holds b2 . o = id o );