:: OPPCAT_1 semantic presentation begin definition let X, Y, Z be non empty set ; let f be PartFunc of [:X,Y:],Z; :: original: ~ redefine func ~ f -> PartFunc of [:Y,X:],Z; coherence ~ f is PartFunc of [:Y,X:],Z by FUNCT_4:48; end; definition let C be Category; funcC opp -> non empty non void strict CatStr equals :: OPPCAT_1:def 1 CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #); coherence CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) is non empty non void strict CatStr ; end; :: deftheorem defines opp OPPCAT_1:def_1_:_ for C being Category holds C opp = CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #); definition let C be Category; let c be Object of C; funcc opp -> Object of (C opp) equals :: OPPCAT_1:def 2 c; coherence c is Object of (C opp) ; end; :: deftheorem defines opp OPPCAT_1:def_2_:_ for C being Category for c being Object of C holds c opp = c; registration let C be Category; clusterC opp -> non empty non void strict Category-like transitive associative reflexive with_identities ; coherence ( C opp is Category-like & C opp is transitive & C opp is associative & C opp is reflexive & C opp is with_identities ) proof set M = the carrier' of C; set d = the Target of C; set c = the Source of C; set p = ~ the Comp of C; set B = C opp ; thus A1: C opp is Category-like ::_thesis: ( C opp is transitive & C opp is associative & C opp is reflexive & C opp is with_identities ) proof let f, g be Morphism of (C opp); :: according to CAT_1:def_6 ::_thesis: ( ( not [g,f] in dom the Comp of (C opp) or dom g = cod f ) & ( not dom g = cod f or [g,f] in dom the Comp of (C opp) ) ) reconsider ff = f, gg = g as Morphism of C ; thus ( [g,f] in dom the Comp of (C opp) implies dom g = cod f ) ::_thesis: ( not dom g = cod f or [g,f] in dom the Comp of (C opp) ) proof assume [g,f] in dom the Comp of (C opp) ; ::_thesis: dom g = cod f then [ff,gg] in dom the Comp of C by FUNCT_4:42; then dom ff = cod gg by CAT_1:def_6; hence dom g = cod f ; ::_thesis: verum end; assume A2: dom g = cod f ; ::_thesis: [g,f] in dom the Comp of (C opp) cod gg = dom ff by A2; then [ff,gg] in dom the Comp of C by CAT_1:def_6; hence [g,f] in dom the Comp of (C opp) by FUNCT_4:42; ::_thesis: verum end; A3: for f, g being Element of the carrier' of C st the Target of C . g = the Source of C . f holds (~ the Comp of C) . (g,f) = the Comp of C . (f,g) proof let f, g be Element of the carrier' of C; ::_thesis: ( the Target of C . g = the Source of C . f implies (~ the Comp of C) . (g,f) = the Comp of C . (f,g) ) reconsider ff = f, gg = g as Morphism of (C opp) ; assume the Target of C . g = the Source of C . f ; ::_thesis: (~ the Comp of C) . (g,f) = the Comp of C . (f,g) then dom gg = cod ff ; then [gg,ff] in dom (~ the Comp of C) by A1, CAT_1:def_6; hence (~ the Comp of C) . (g,f) = the Comp of C . (f,g) by FUNCT_4:43; ::_thesis: verum end; thus A4: C opp is transitive ::_thesis: ( C opp is associative & C opp is reflexive & C opp is with_identities ) proof let ff, gg be Morphism of (C opp); :: according to CAT_1:def_7 ::_thesis: ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) ) reconsider f = ff, g = gg as Morphism of C ; assume A5: dom gg = cod ff ; ::_thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) then A6: cod g = dom f ; then A7: [f,g] in dom the Comp of C by CAT_1:def_6; [gg,ff] in dom the Comp of (C opp) by A5, A1, CAT_1:def_6; then A8: gg (*) ff = (~ the Comp of C) . (g,f) by CAT_1:def_1 .= the Comp of C . (f,g) by A3, A5 .= f (*) g by A7, CAT_1:def_1 ; hence dom (gg (*) ff) = cod (f (*) g) .= cod f by A6, CAT_1:def_7 .= dom ff ; ::_thesis: cod (gg (*) ff) = cod gg thus cod (gg (*) ff) = dom (f (*) g) by A8 .= dom g by A6, CAT_1:def_7 .= cod gg ; ::_thesis: verum end; thus C opp is associative ::_thesis: ( C opp is reflexive & C opp is with_identities ) proof let ff, gg, hh be Morphism of (C opp); :: according to CAT_1:def_8 ::_thesis: ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff ) reconsider f = ff, g = gg, h = hh as Morphism of C ; assume that A9: dom hh = cod gg and A10: dom gg = cod ff ; ::_thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff A11: [h,g] in dom (~ the Comp of C) by A1, CAT_1:def_6, A9; then A12: (~ the Comp of C) . (h,g) is Element of the carrier' of C by PARTFUN1:4; A13: [g,f] in dom (~ the Comp of C) by A1, CAT_1:def_6, A10; then A14: (~ the Comp of C) . (g,f) is Element of the carrier' of C by PARTFUN1:4; A15: (~ the Comp of C) . (h,g) = the Comp of C . (g,h) by A3, A9; the Target of C . ((~ the Comp of C) . (h,g)) = dom (hh (*) gg) by A11, CAT_1:def_1 .= dom gg by A4, CAT_1:def_7, A9 ; then A16: (~ the Comp of C) . (((~ the Comp of C) . (h,g)),f) = the Comp of C . (f,( the Comp of C . (g,h))) by A3, A10, A12, A15; A17: ( cod h = dom g & cod g = dom f ) by A9, A10; A18: (~ the Comp of C) . (g,f) = the Comp of C . (f,g) by A3, A10; A19: the Source of C . ((~ the Comp of C) . (g,f)) = cod (gg (*) ff) by A13, CAT_1:def_1 .= cod gg by A4, CAT_1:def_7, A10 ; dom (hh (*) gg) = dom gg by A4, CAT_1:def_7, A9; then A20: [(hh (*) gg),ff] in dom the Comp of (C opp) by A1, CAT_1:def_6, A10; cod (gg (*) ff) = cod gg by A4, CAT_1:def_7, A10; then A21: [hh,(gg (*) ff)] in dom the Comp of (C opp) by A1, CAT_1:def_6, A9; [hh,gg] in dom the Comp of (C opp) by A9, A1, CAT_1:def_6; then A22: hh (*) gg = (~ the Comp of C) . (h,g) by CAT_1:def_1; A23: f (*) g = the Comp of C . (f,g) by A17, CAT_1:16; A24: dom (f (*) g) = dom g by A17, CAT_1:def_7; A25: g (*) h = the Comp of C . (g,h) by A17, CAT_1:16; A26: cod (g (*) h) = cod g by A17, CAT_1:def_7; [gg,ff] in dom the Comp of (C opp) by A10, A1, CAT_1:def_6; then gg (*) ff = (~ the Comp of C) . (g,f) by CAT_1:def_1; hence hh (*) (gg (*) ff) = (~ the Comp of C) . (h,((~ the Comp of C) . (g,f))) by A21, CAT_1:def_1 .= the Comp of C . (( the Comp of C . (f,g)),h) by A3, A9, A14, A18, A19 .= (f (*) g) (*) h by A23, A17, A24, CAT_1:16 .= f (*) (g (*) h) by A17, CAT_1:def_8 .= (~ the Comp of C) . (((~ the Comp of C) . (h,g)),f) by A16, A17, A25, A26, CAT_1:16 .= (hh (*) gg) (*) ff by A20, A22, CAT_1:def_1 ; ::_thesis: verum end; thus C opp is reflexive ::_thesis: C opp is with_identities proof let bb be Object of (C opp); :: according to CAT_1:def_9 ::_thesis: not Hom (bb,bb) = {} reconsider b = bb as Element of C ; consider f being Morphism of C such that A27: f in Hom (b,b) by SUBSET_1:4; reconsider ff = f as Morphism of (C opp) ; A28: dom ff = cod f .= bb by A27, CAT_1:1 ; cod ff = dom f .= bb by A27, CAT_1:1 ; then ff in Hom (bb,bb) by A28; hence Hom (bb,bb) <> {} ; ::_thesis: verum end; let a be Element of (C opp); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st for b2 being Element of the carrier of (C opp) holds ( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) ) reconsider aa = a as Element of C ; reconsider ii = id aa as Morphism of (C opp) ; A29: dom ii = cod (id aa) .= aa ; A30: cod ii = dom (id aa) .= aa ; then reconsider ii = ii as Morphism of a,a by A29, CAT_1:4; take ii ; ::_thesis: for b1 being Element of the carrier of (C opp) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) let b be Element of (C opp); ::_thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) ) reconsider bb = b as Element of C ; thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) ::_thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) proof assume A31: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) ii = g let g be Morphism of a,b; ::_thesis: g (*) ii = g reconsider gg = g as Morphism of C ; A32: dom gg = cod g .= bb by A31, CAT_1:5 ; A33: cod gg = dom g .= aa by A31, CAT_1:5 ; then A34: cod gg = dom (id aa) ; reconsider gg = gg as Morphism of bb,aa by A32, A33, CAT_1:4; A35: the Source of C . ii = aa by A30 .= dom g by A31, CAT_1:5 .= the Target of C . g ; then dom g = cod ii ; then [g,ii] in dom the Comp of (C opp) by A1, CAT_1:def_6; hence g (*) ii = (~ the Comp of C) . (g,ii) by CAT_1:def_1 .= the Comp of C . (ii,g) by A35, A3 .= (id aa) (*) gg by A34, CAT_1:16 .= g by A33, CAT_1:21 ; ::_thesis: verum end; assume A36: Hom (b,a) <> {} ; ::_thesis: for b1 being Morphism of b,a holds ii (*) b1 = b1 let g be Morphism of b,a; ::_thesis: ii (*) g = g reconsider gg = g as Morphism of C ; A37: cod gg = dom g .= bb by A36, CAT_1:5 ; A38: dom gg = cod g .= aa by A36, CAT_1:5 ; then A39: dom gg = cod (id aa) ; reconsider gg = gg as Morphism of aa,bb by A37, A38, CAT_1:4; A40: the Target of C . ii = aa by A29 .= cod g by A36, CAT_1:5 .= the Source of C . g ; then cod g = dom ii ; then [ii,g] in dom the Comp of (C opp) by A1, CAT_1:def_6; hence ii (*) g = (~ the Comp of C) . (ii,g) by CAT_1:def_1 .= the Comp of C . (g,ii) by A40, A3 .= gg (*) (id aa) by A39, CAT_1:16 .= g by A38, CAT_1:22 ; ::_thesis: verum end; end; definition let C be Category; let c be Object of (C opp); func opp c -> Object of C equals :: OPPCAT_1:def 3 c opp ; coherence c opp is Object of C ; end; :: deftheorem defines opp OPPCAT_1:def_3_:_ for C being Category for c being Object of (C opp) holds opp c = c opp ; theorem :: OPPCAT_1:1 canceled; theorem :: OPPCAT_1:2 for C being Category for c being Object of C holds (c opp) opp = c ; theorem :: OPPCAT_1:3 for C being Category for c being Object of C holds opp (c opp) = c ; theorem :: OPPCAT_1:4 for C being Category for c being Object of (C opp) holds (opp c) opp = c ; theorem Th5: :: OPPCAT_1:5 for C being Category for a, b being Object of C holds Hom (a,b) = Hom ((b opp),(a opp)) proof let C be Category; ::_thesis: for a, b being Object of C holds Hom (a,b) = Hom ((b opp),(a opp)) let a, b be Object of C; ::_thesis: Hom (a,b) = Hom ((b opp),(a opp)) thus Hom (a,b) c= Hom ((b opp),(a opp)) :: according to XBOOLE_0:def_10 ::_thesis: Hom ((b opp),(a opp)) c= Hom (a,b) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Hom (a,b) or x in Hom ((b opp),(a opp)) ) assume A1: x in Hom (a,b) ; ::_thesis: x in Hom ((b opp),(a opp)) then reconsider f = x as Morphism of C ; reconsider g = f as Morphism of (C opp) ; ( dom f = a & cod f = b ) by A1, CAT_1:1; then ( dom g = b opp & cod g = a opp ) ; hence x in Hom ((b opp),(a opp)) ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Hom ((b opp),(a opp)) or x in Hom (a,b) ) assume A2: x in Hom ((b opp),(a opp)) ; ::_thesis: x in Hom (a,b) then reconsider f = x as Morphism of (C opp) ; reconsider g = f as Morphism of C ; ( dom f = b opp & cod f = a opp ) by A2, CAT_1:1; then ( dom g = a & cod g = b ) ; hence x in Hom (a,b) ; ::_thesis: verum end; theorem Th6: :: OPPCAT_1:6 for C being Category for a, b being Object of (C opp) holds Hom (a,b) = Hom ((opp b),(opp a)) proof let C be Category; ::_thesis: for a, b being Object of (C opp) holds Hom (a,b) = Hom ((opp b),(opp a)) let a, b be Object of (C opp); ::_thesis: Hom (a,b) = Hom ((opp b),(opp a)) thus Hom (a,b) = Hom (((opp a) opp),((opp b) opp)) .= Hom ((opp b),(opp a)) by Th5 ; ::_thesis: verum end; definition let C be Category; let f be Morphism of C; funcf opp -> Morphism of (C opp) equals :: OPPCAT_1:def 4 f; coherence f is Morphism of (C opp) ; end; :: deftheorem defines opp OPPCAT_1:def_4_:_ for C being Category for f being Morphism of C holds f opp = f; definition let C be Category; let f be Morphism of (C opp); func opp f -> Morphism of C equals :: OPPCAT_1:def 5 f opp ; coherence f opp is Morphism of C ; end; :: deftheorem defines opp OPPCAT_1:def_5_:_ for C being Category for f being Morphism of (C opp) holds opp f = f opp ; definition let C be Category; let a, b be Object of C; assume Z: Hom (a,b) <> {} ; let f be Morphism of a,b; funcf opp -> Morphism of b opp ,a opp equals :Def6: :: OPPCAT_1:def 6 f; coherence f is Morphism of b opp ,a opp proof f in Hom (a,b) by Z, CAT_1:def_5; then f in Hom ((b opp),(a opp)) by Th5; hence f is Morphism of b opp ,a opp by CAT_1:def_5; ::_thesis: verum end; end; :: deftheorem Def6 defines opp OPPCAT_1:def_6_:_ for C being Category for a, b being Object of C st Hom (a,b) <> {} holds for f being Morphism of a,b holds f opp = f; definition let C be Category; let a, b be Object of C; assume Z: Hom ((a opp),(b opp)) <> {} ; let f be Morphism of a opp ,b opp ; func opp f -> Morphism of b,a equals :Def7: :: OPPCAT_1:def 7 f; coherence f is Morphism of b,a proof f in Hom ((a opp),(b opp)) by Z, CAT_1:def_5; then f in Hom (b,a) by Th5; hence f is Morphism of b,a by CAT_1:def_5; ::_thesis: verum end; end; :: deftheorem Def7 defines opp OPPCAT_1:def_7_:_ for C being Category for a, b being Object of C st Hom ((a opp),(b opp)) <> {} holds for f being Morphism of a opp ,b opp holds opp f = f; theorem :: OPPCAT_1:7 for C being Category for a, b being Object of C st Hom (a,b) <> {} holds for f being Morphism of a,b holds (f opp) opp = f proof let C be Category; ::_thesis: for a, b being Object of C st Hom (a,b) <> {} holds for f being Morphism of a,b holds (f opp) opp = f let a, b be Object of C; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (f opp) opp = f ) assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds (f opp) opp = f then A2: Hom ((b opp),(a opp)) <> {} by Th5; let f be Morphism of a,b; ::_thesis: (f opp) opp = f thus (f opp) opp = f opp by A2, Def6 .= f by A1, Def6 ; ::_thesis: verum end; theorem :: OPPCAT_1:8 for C being Category for a, b being Object of C st Hom (a,b) <> {} holds for f being Morphism of a,b holds opp (f opp) = f proof let C be Category; ::_thesis: for a, b being Object of C st Hom (a,b) <> {} holds for f being Morphism of a,b holds opp (f opp) = f let a, b be Object of C; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds opp (f opp) = f ) assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds opp (f opp) = f then A2: Hom ((b opp),(a opp)) <> {} by Th5; let f be Morphism of a,b; ::_thesis: opp (f opp) = f thus opp (f opp) = f opp by A2, Def7 .= f by A1, Def6 ; ::_thesis: verum end; theorem :: OPPCAT_1:9 for C being Category for a, b being Object of (C opp) for f being Morphism of a,b holds (opp f) opp = f ; theorem Th10: :: OPPCAT_1:10 for C being Category for a, b being Object of C st Hom (a,b) <> {} holds for f being Morphism of a,b holds ( dom (f opp) = cod f & cod (f opp) = dom f ) proof let C be Category; ::_thesis: for a, b being Object of C st Hom (a,b) <> {} holds for f being Morphism of a,b holds ( dom (f opp) = cod f & cod (f opp) = dom f ) let a, b be Object of C; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds ( dom (f opp) = cod f & cod (f opp) = dom f ) ) assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds ( dom (f opp) = cod f & cod (f opp) = dom f ) then A2: Hom ((b opp),(a opp)) <> {} by Th5; let f be Morphism of a,b; ::_thesis: ( dom (f opp) = cod f & cod (f opp) = dom f ) thus dom (f opp) = b by A2, CAT_1:5 .= cod f by A1, CAT_1:5 ; ::_thesis: cod (f opp) = dom f thus cod (f opp) = a by A2, CAT_1:5 .= dom f by A1, CAT_1:5 ; ::_thesis: verum end; theorem :: OPPCAT_1:11 for C being Category for a, b being Object of (C opp) for f being Morphism of a,b holds ( dom (opp f) = cod f & cod (opp f) = dom f ) ; theorem :: OPPCAT_1:12 for C being Category for a, b being Object of C st Hom (a,b) <> {} holds for f being Morphism of a,b holds ( (dom f) opp = cod (f opp) & (cod f) opp = dom (f opp) ) by Th10; theorem :: OPPCAT_1:13 for C being Category for a, b being Object of (C opp) st Hom (a,b) <> {} holds for f being Morphism of a,b holds ( opp (dom f) = cod (opp f) & opp (cod f) = dom (opp f) ) ; theorem :: OPPCAT_1:14 canceled; theorem Th15: :: OPPCAT_1:15 for C being Category for a, b being Object of (C opp) for f being Morphism of a,b st Hom (a,b) <> {} holds opp f is Morphism of opp b, opp a proof let C be Category; ::_thesis: for a, b being Object of (C opp) for f being Morphism of a,b st Hom (a,b) <> {} holds opp f is Morphism of opp b, opp a let a, b be Object of (C opp); ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds opp f is Morphism of opp b, opp a let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies opp f is Morphism of opp b, opp a ) assume Hom (a,b) <> {} ; ::_thesis: opp f is Morphism of opp b, opp a then f in Hom (a,b) by CAT_1:def_5; then opp f in Hom ((opp b),(opp a)) by Th6; hence opp f is Morphism of opp b, opp a by CAT_1:def_5; ::_thesis: verum end; theorem Th16: :: OPPCAT_1:16 for C being Category for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) proof let C be Category; ::_thesis: for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) let a, b, c be Object of C; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) ) assume that A1: Hom (a,b) <> {} and A2: Hom (b,c) <> {} ; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) A3: Hom ((b opp),(a opp)) <> {} by A1, Th5; A4: Hom ((c opp),(b opp)) <> {} by A2, Th5; let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) let g be Morphism of b,c; ::_thesis: (g (*) f) opp = (f opp) (*) (g opp) A5: dom g = b by A2, CAT_1:5 .= cod f by A1, CAT_1:5 ; then A6: g (*) f = the Comp of C . (g,f) by CAT_1:16; A7: ( f opp = f & g opp = g ) by A1, A2, Def6; A8: dom g = b opp by A2, CAT_1:5 .= cod (g opp) by A4, CAT_1:5 ; A9: cod f = b opp by A1, CAT_1:5 .= dom (f opp) by A3, CAT_1:5 ; then ( the Comp of C = ~ the Comp of (C opp) & [(f opp),(g opp)] in dom the Comp of (C opp) ) by A5, CAT_1:15, FUNCT_4:53, A8; then the Comp of C . (g,f) = the Comp of (C opp) . ((f opp),(g opp)) by FUNCT_4:def_2, A7; hence (g (*) f) opp = (f opp) (*) (g opp) by A5, A6, A8, CAT_1:16, A9; ::_thesis: verum end; theorem :: OPPCAT_1:17 for C being Category for a, b, c being Object of C st Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) proof let C be Category; ::_thesis: for a, b, c being Object of C st Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) let a, b, c be Object of C; ::_thesis: ( Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} implies for f being Morphism of a,b for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) ) assume ( Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} ) ; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) then ( Hom (a,b) <> {} & Hom (b,c) <> {} ) by Th5; hence for f being Morphism of a,b for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) by Th16; ::_thesis: verum end; theorem Th18: :: OPPCAT_1:18 for C being Category for f, g being Morphism of (C opp) st dom g = cod f holds opp (g (*) f) = (opp f) (*) (opp g) proof let C be Category; ::_thesis: for f, g being Morphism of (C opp) st dom g = cod f holds opp (g (*) f) = (opp f) (*) (opp g) let f, g be Morphism of (C opp); ::_thesis: ( dom g = cod f implies opp (g (*) f) = (opp f) (*) (opp g) ) assume A1: dom g = cod f ; ::_thesis: opp (g (*) f) = (opp f) (*) (opp g) A2: ( cod (opp g) = dom g & dom (opp f) = cod f ) ; then A3: [(opp f),(opp g)] in dom the Comp of C by A1, CAT_1:15; thus opp (g (*) f) = (~ the Comp of C) . ((opp g),(opp f)) by A1, CAT_1:16 .= the Comp of C . ((opp f),(opp g)) by A3, FUNCT_4:def_2 .= (opp f) (*) (opp g) by A1, A2, CAT_1:16 ; ::_thesis: verum end; theorem :: OPPCAT_1:19 for C being Category for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds (g * f) opp = (f opp) (*) (g opp) proof let C be Category; ::_thesis: for a, b, c being Object of C for f being Morphism of a,b for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds (g * f) opp = (f opp) (*) (g opp) let a, b, c be Object of C; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds (g * f) opp = (f opp) (*) (g opp) let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds (g * f) opp = (f opp) (*) (g opp) let g be Morphism of b,c; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies (g * f) opp = (f opp) (*) (g opp) ) assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; ::_thesis: (g * f) opp = (f opp) (*) (g opp) A2: Hom (a,c) <> {} by A1, CAT_1:24; thus (g * f) opp = g * f by A2, Def6 .= (g (*) f) opp by A1, CAT_1:def_13 .= (f opp) (*) (g opp) by A1, Th16 ; ::_thesis: verum end; Lm1: for C being Category for a being Object of C for b being Object of (C opp) holds ( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) ) proof let C be Category; ::_thesis: for a being Object of C for b being Object of (C opp) holds ( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) ) let a be Object of C; ::_thesis: for b being Object of (C opp) holds ( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) ) let b be Object of (C opp); ::_thesis: ( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) ) thus ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) ::_thesis: ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) proof assume A1: Hom ((a opp),b) <> {} ; ::_thesis: for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f A2: Hom ((opp b),(opp (a opp))) <> {} by A1, Th6; let f be Morphism of a opp ,b; ::_thesis: f (*) ((id a) opp) = f A3: Hom (a,a) <> {} ; A4: cod (opp f) = dom f .= a by CAT_1:5, A1 ; dom (opp f) = cod f .= opp b by CAT_1:5, A1 ; then reconsider ff = opp f as Morphism of opp b,a by A4, CAT_1:4; A5: (id a) (*) ff = (id a) * ff by A3, A2, CAT_1:def_13; thus f (*) ((id a) opp) = (ff opp) (*) ((id a) opp) by A2, Def6 .= ((id a) (*) ff) opp by A2, A3, Th16 .= ((id a) * ff) opp by A5, Def6, A2 .= ff opp by CAT_1:28, A2 .= f by A2, Def6 ; ::_thesis: verum end; assume A6: Hom (b,(a opp)) <> {} ; ::_thesis: for f being Morphism of b,a opp holds ((id a) opp) (*) f = f A7: Hom ((opp (a opp)),(opp b)) <> {} by A6, Th6; let f be Morphism of b,a opp ; ::_thesis: ((id a) opp) (*) f = f A8: Hom (a,a) <> {} ; A9: dom (opp f) = cod f .= a by CAT_1:5, A6 ; cod (opp f) = dom f .= opp b by CAT_1:5, A6 ; then reconsider ff = opp f as Morphism of a, opp b by A9, CAT_1:4; A10: ff (*) (id a) = ff * (id a) by A8, A7, CAT_1:def_13; thus ((id a) opp) (*) f = ((id a) opp) (*) (ff opp) by A7, Def6 .= (ff (*) (id a)) opp by A8, A7, Th16 .= (ff * (id a)) opp by A10, Def6, A7 .= ff opp by CAT_1:29, A7 .= f by A7, Def6 ; ::_thesis: verum end; theorem Th20: :: OPPCAT_1:20 for C being Category for a being Object of C holds (id a) opp = id (a opp) proof let C be Category; ::_thesis: for a being Object of C holds (id a) opp = id (a opp) let a be Object of C; ::_thesis: (id a) opp = id (a opp) for b being Object of (C opp) holds ( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) ) by Lm1; hence (id a) opp = id (a opp) by CAT_1:def_12; ::_thesis: verum end; Lm2: for C being Category for a being Object of C holds id a = id (a opp) proof let C be Category; ::_thesis: for a being Object of C holds id a = id (a opp) let a be Object of C; ::_thesis: id a = id (a opp) Hom (a,a) <> {} ; hence id a = (id a) opp by Def6 .= id (a opp) by Th20 ; ::_thesis: verum end; theorem Th21: :: OPPCAT_1:21 for C being Category for a being Object of (C opp) holds opp (id a) = id (opp a) proof let C be Category; ::_thesis: for a being Object of (C opp) holds opp (id a) = id (opp a) let a be Object of (C opp); ::_thesis: opp (id a) = id (opp a) set b = opp a; thus opp (id a) = id ((opp a) opp) .= id (opp a) by Lm2 ; ::_thesis: verum end; Lm3: for C being Category for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds g * f = (f opp) * (g opp) proof let C be Category; ::_thesis: for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds g * f = (f opp) * (g opp) let a, b, c be Object of C; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b for g being Morphism of b,c holds g * f = (f opp) * (g opp) ) assume that A1: Hom (a,b) <> {} and A2: Hom (b,c) <> {} ; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c holds g * f = (f opp) * (g opp) let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c holds g * f = (f opp) * (g opp) let g be Morphism of b,c; ::_thesis: g * f = (f opp) * (g opp) reconsider f1 = f as Morphism of C ; reconsider g1 = g as Morphism of C ; A3: Hom ((b opp),(a opp)) <> {} by A1, Th5; A4: Hom ((c opp),(b opp)) <> {} by A2, Th5; g * f = (g (*) f) opp by A1, A2, CAT_1:def_13 .= (f opp) (*) (g opp) by A1, A2, Th16 .= (f opp) * (g opp) by A3, A4, CAT_1:def_13 ; hence g * f = (f opp) * (g opp) ; ::_thesis: verum end; theorem :: OPPCAT_1:22 for C being Category for a, b being Object of C for f being Morphism of a,b holds ( f opp is monic iff f is epi ) proof let C be Category; ::_thesis: for a, b being Object of C for f being Morphism of a,b holds ( f opp is monic iff f is epi ) let a, b be Object of C; ::_thesis: for f being Morphism of a,b holds ( f opp is monic iff f is epi ) let f be Morphism of a,b; ::_thesis: ( f opp is monic iff f is epi ) thus ( f opp is monic implies f is epi ) ::_thesis: ( f is epi implies f opp is monic ) proof assume that A1: Hom ((b opp),(a opp)) <> {} and A2: for c being Object of (C opp) st Hom (c,(b opp)) <> {} holds for f1, f2 being Morphism of c,b opp st (f opp) * f1 = (f opp) * f2 holds f1 = f2 ; :: according to CAT_1:def_14 ::_thesis: f is epi thus A3: Hom (a,b) <> {} by A1, Th5; :: according to CAT_1:def_15 ::_thesis: for b1 being Element of the carrier of C holds ( Hom (b,b1) = {} or for b2, b3 being Morphism of b,b1 holds ( not b2 * f = b3 * f or b2 = b3 ) ) let c be Object of C; ::_thesis: ( Hom (b,c) = {} or for b1, b2 being Morphism of b,c holds ( not b1 * f = b2 * f or b1 = b2 ) ) assume A4: Hom (b,c) <> {} ; ::_thesis: for b1, b2 being Morphism of b,c holds ( not b1 * f = b2 * f or b1 = b2 ) let g1, g2 be Morphism of b,c; ::_thesis: ( not g1 * f = g2 * f or g1 = g2 ) assume A5: g1 * f = g2 * f ; ::_thesis: g1 = g2 reconsider f1 = g1 opp , f2 = g2 opp as Morphism of c opp ,b opp ; A6: Hom ((c opp),(b opp)) <> {} by A4, Th5; (f opp) * f1 = g1 * f by A4, Lm3, A3 .= (f opp) * f2 by A4, Lm3, A3, A5 ; then A7: f1 = f2 by A2, A6; g1 = f1 by A4, Def6 .= g2 by A7, A4, Def6 ; hence g1 = g2 ; ::_thesis: verum end; assume that A8: Hom (a,b) <> {} and A9: for c being Object of C st Hom (b,c) <> {} holds for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds g1 = g2 ; :: according to CAT_1:def_15 ::_thesis: f opp is monic thus Hom ((b opp),(a opp)) <> {} by A8, Th5; :: according to CAT_1:def_14 ::_thesis: for b1 being Element of the carrier of (C opp) holds ( Hom (b1,(b opp)) = {} or for b2, b3 being Morphism of b1,b opp holds ( not (f opp) * b2 = (f opp) * b3 or b2 = b3 ) ) let c be Object of (C opp); ::_thesis: ( Hom (c,(b opp)) = {} or for b1, b2 being Morphism of c,b opp holds ( not (f opp) * b1 = (f opp) * b2 or b1 = b2 ) ) assume A10: Hom (c,(b opp)) <> {} ; ::_thesis: for b1, b2 being Morphism of c,b opp holds ( not (f opp) * b1 = (f opp) * b2 or b1 = b2 ) let f1, f2 be Morphism of c,b opp ; ::_thesis: ( not (f opp) * f1 = (f opp) * f2 or f1 = f2 ) assume A11: (f opp) * f1 = (f opp) * f2 ; ::_thesis: f1 = f2 ( f1 in Hom (c,(b opp)) & f2 in Hom (c,(b opp)) ) by A10, CAT_1:def_5; then ( f1 in Hom ((opp (b opp)),(opp c)) & f2 in Hom ((opp (b opp)),(opp c)) ) by Th6; then reconsider g1 = opp f1, g2 = opp f2 as Morphism of b, opp c by CAT_1:def_5; A12: Hom ((opp (b opp)),(opp c)) <> {} by A10, Th6; A13: g1 opp = f1 by Def6, A12; A14: g2 opp = f2 by Def6, A12; g1 * f = (f opp) * f2 by A11, A13, A8, Lm3, A12 .= g2 * f by A8, Lm3, A12, A14 ; hence f1 = f2 by A9, A12; ::_thesis: verum end; theorem :: OPPCAT_1:23 for C being Category for b, c being Object of C st Hom (b,c) <> {} holds for f being Morphism of b,c holds ( f opp is epi iff f is monic ) proof let C be Category; ::_thesis: for b, c being Object of C st Hom (b,c) <> {} holds for f being Morphism of b,c holds ( f opp is epi iff f is monic ) let b, c be Object of C; ::_thesis: ( Hom (b,c) <> {} implies for f being Morphism of b,c holds ( f opp is epi iff f is monic ) ) assume A1: Hom (b,c) <> {} ; ::_thesis: for f being Morphism of b,c holds ( f opp is epi iff f is monic ) let f be Morphism of b,c; ::_thesis: ( f opp is epi iff f is monic ) thus ( f opp is epi implies f is monic ) ::_thesis: ( f is monic implies f opp is epi ) proof assume that Hom ((c opp),(b opp)) <> {} and A2: for a being Object of (C opp) st Hom ((b opp),a) <> {} holds for g1, g2 being Morphism of b opp ,a st g1 * (f opp) = g2 * (f opp) holds g1 = g2 ; :: according to CAT_1:def_15 ::_thesis: f is monic thus Hom (b,c) <> {} by A1; :: according to CAT_1:def_14 ::_thesis: for b1 being Element of the carrier of C holds ( Hom (b1,b) = {} or for b2, b3 being Morphism of b1,b holds ( not f * b2 = f * b3 or b2 = b3 ) ) let a be Object of C; ::_thesis: ( Hom (a,b) = {} or for b1, b2 being Morphism of a,b holds ( not f * b1 = f * b2 or b1 = b2 ) ) assume A3: Hom (a,b) <> {} ; ::_thesis: for b1, b2 being Morphism of a,b holds ( not f * b1 = f * b2 or b1 = b2 ) let f1, f2 be Morphism of a,b; ::_thesis: ( not f * f1 = f * f2 or f1 = f2 ) assume A4: f * f1 = f * f2 ; ::_thesis: f1 = f2 reconsider g1 = f1 opp , g2 = f2 opp as Morphism of b opp ,a opp ; A5: Hom ((b opp),(a opp)) <> {} by A3, Th5; g1 * (f opp) = f * f1 by Lm3, A1, A3 .= g2 * (f opp) by Lm3, A1, A3, A4 ; then g1 = g2 by A2, A5; hence f1 = g2 by Def6, A3 .= f2 by Def6, A3 ; ::_thesis: verum end; assume that A6: Hom (b,c) <> {} and A7: for a being Object of C st Hom (a,b) <> {} holds for f1, f2 being Morphism of a,b st f * f1 = f * f2 holds f1 = f2 ; :: according to CAT_1:def_14 ::_thesis: f opp is epi thus Hom ((c opp),(b opp)) <> {} by A6, Th5; :: according to CAT_1:def_15 ::_thesis: for b1 being Element of the carrier of (C opp) holds ( Hom ((b opp),b1) = {} or for b2, b3 being Morphism of b opp ,b1 holds ( not b2 * (f opp) = b3 * (f opp) or b2 = b3 ) ) let a be Object of (C opp); ::_thesis: ( Hom ((b opp),a) = {} or for b1, b2 being Morphism of b opp ,a holds ( not b1 * (f opp) = b2 * (f opp) or b1 = b2 ) ) assume A8: Hom ((b opp),a) <> {} ; ::_thesis: for b1, b2 being Morphism of b opp ,a holds ( not b1 * (f opp) = b2 * (f opp) or b1 = b2 ) let g1, g2 be Morphism of b opp ,a; ::_thesis: ( not g1 * (f opp) = g2 * (f opp) or g1 = g2 ) assume A9: g1 * (f opp) = g2 * (f opp) ; ::_thesis: g1 = g2 Hom ((b opp),a) = Hom ((opp a),(opp (b opp))) by Th6 .= Hom ((opp a),b) ; then ( opp g1 in Hom ((opp a),b) & opp g2 in Hom ((opp a),b) ) by A8, CAT_1:def_5; then reconsider f1 = opp g1, f2 = opp g2 as Morphism of opp a,b by CAT_1:def_5; A10: Hom ((opp a),(opp (b opp))) <> {} by A8, Th6; f * f1 = (f1 opp) * (f opp) by A6, Lm3, A10 .= g2 * (f opp) by A9, Def6, A10 .= (f2 opp) * (f opp) by Def6, A10 .= f * f2 by A6, Lm3, A10 ; hence g1 = g2 by A7, A10; ::_thesis: verum end; theorem :: OPPCAT_1:24 for C being Category for a, b being Object of C for f being Morphism of a,b holds ( f opp is invertible iff f is invertible ) proof let C be Category; ::_thesis: for a, b being Object of C for f being Morphism of a,b holds ( f opp is invertible iff f is invertible ) let a, b be Object of C; ::_thesis: for f being Morphism of a,b holds ( f opp is invertible iff f is invertible ) let f be Morphism of a,b; ::_thesis: ( f opp is invertible iff f is invertible ) thus ( f opp is invertible implies f is invertible ) ::_thesis: ( f is invertible implies f opp is invertible ) proof assume A1: ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) ; :: according to CAT_1:def_16 ::_thesis: ( for b1 being Morphism of a opp ,b opp holds ( not (f opp) * b1 = id (a opp) or not b1 * (f opp) = id (b opp) ) or f is invertible ) given gg being Morphism of a opp ,b opp such that A2: ( (f opp) * gg = id (a opp) & gg * (f opp) = id (b opp) ) ; ::_thesis: f is invertible thus A3: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1, Th5; :: according to CAT_1:def_16 ::_thesis: ex b1 being Morphism of b,a st ( f * b1 = id b & b1 * f = id a ) reconsider g = opp gg as Morphism of b,a ; take g ; ::_thesis: ( f * g = id b & g * f = id a ) A4: g opp = g by Def6, A3 .= gg by Def7, A1 ; thus f * g = (g opp) * (f opp) by A3, Lm3 .= id (b opp) by A2, A4 .= id b by Lm2 ; ::_thesis: g * f = id a thus g * f = (f opp) * (g opp) by A3, Lm3 .= id a by A2, A4, Lm2 ; ::_thesis: verum end; assume A5: ( 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 opp is invertible ) given g being Morphism of b,a such that A6: ( f * g = id b & g * f = id a ) ; ::_thesis: f opp is invertible thus ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) by A5, Th5; :: according to CAT_1:def_16 ::_thesis: ex b1 being Morphism of a opp ,b opp st ( (f opp) * b1 = id (a opp) & b1 * (f opp) = id (b opp) ) take g opp ; ::_thesis: ( (f opp) * (g opp) = id (a opp) & (g opp) * (f opp) = id (b opp) ) thus (f opp) * (g opp) = g * f by A5, Lm3 .= id (a opp) by A6, Lm2 ; ::_thesis: (g opp) * (f opp) = id (b opp) thus (g opp) * (f opp) = f * g by A5, Lm3 .= id (b opp) by A6, Lm2 ; ::_thesis: verum end; theorem :: OPPCAT_1:25 for C being Category for c being Object of C holds ( c is initial iff c opp is terminal ) proof let C be Category; ::_thesis: for c being Object of C holds ( c is initial iff c opp is terminal ) let c be Object of C; ::_thesis: ( c is initial iff c opp is terminal ) thus ( c is initial implies c opp is terminal ) ::_thesis: ( c opp is terminal implies c is initial ) proof assume A1: c is initial ; ::_thesis: c opp is terminal let b be Object of (C opp); :: according to CAT_1:def_18 ::_thesis: ( not Hom (b,(c opp)) = {} & ex b1 being Morphism of b,c opp st for b2 being Morphism of b,c opp holds b1 = b2 ) consider f being Morphism of c, opp b such that A2: for g being Morphism of c, opp b holds f = g by A1, CAT_1:def_19; A3: (opp b) opp = b ; A4: Hom (c,(opp b)) <> {} by A1, CAT_1:def_19; reconsider f9 = f opp as Morphism of b,c opp ; thus A5: Hom (b,(c opp)) <> {} by A3, Th5, A4; ::_thesis: ex b1 being Morphism of b,c opp st for b2 being Morphism of b,c opp holds b1 = b2 take f9 ; ::_thesis: for b1 being Morphism of b,c opp holds f9 = b1 let g be Morphism of b,c opp ; ::_thesis: f9 = g opp (c opp) = c ; then opp g is Morphism of c, opp b by A5, Th15; hence g = f by A2 .= f9 by A4, Def6 ; ::_thesis: verum end; assume A6: c opp is terminal ; ::_thesis: c is initial let b be Object of C; :: according to CAT_1:def_19 ::_thesis: ( not Hom (c,b) = {} & ex b1 being Morphism of c,b st for b2 being Morphism of c,b holds b1 = b2 ) consider f being Morphism of b opp ,c opp such that A7: for g being Morphism of b opp ,c opp holds f = g by A6, CAT_1:def_18; A8: ( opp (c opp) = c & opp (b opp) = b ) ; A9: Hom ((b opp),(c opp)) <> {} by A6, CAT_1:def_18; reconsider f9 = opp f as Morphism of c,b ; thus A10: Hom (c,b) <> {} by A8, Th6, A9; ::_thesis: ex b1 being Morphism of c,b st for b2 being Morphism of c,b holds b1 = b2 take f9 ; ::_thesis: for b1 being Morphism of c,b holds f9 = b1 let g be Morphism of c,b; ::_thesis: f9 = g g opp = f by A7; hence g = f by Def6, A10 .= f9 by A9, Def7 ; ::_thesis: verum end; theorem :: OPPCAT_1:26 for C being Category for c being Object of C holds ( c opp is initial iff c is terminal ) proof let C be Category; ::_thesis: for c being Object of C holds ( c opp is initial iff c is terminal ) let c be Object of C; ::_thesis: ( c opp is initial iff c is terminal ) thus ( c opp is initial implies c is terminal ) ::_thesis: ( c is terminal implies c opp is initial ) proof assume A1: c opp is initial ; ::_thesis: c is terminal let b be Object of C; :: according to CAT_1:def_18 ::_thesis: ( not Hom (b,c) = {} & ex b1 being Morphism of b,c st for b2 being Morphism of b,c holds b1 = b2 ) consider f being Morphism of c opp ,b opp such that A2: for g being Morphism of c opp ,b opp holds f = g by A1, CAT_1:def_19; A3: ( opp (b opp) = b & opp (c opp) = c ) ; A4: Hom ((c opp),(b opp)) <> {} by A1, CAT_1:def_19; reconsider f9 = opp f as Morphism of b,c ; thus A5: Hom (b,c) <> {} by A3, Th6, A4; ::_thesis: ex b1 being Morphism of b,c st for b2 being Morphism of b,c holds b1 = b2 take f9 ; ::_thesis: for b1 being Morphism of b,c holds f9 = b1 let g be Morphism of b,c; ::_thesis: f9 = g g opp = f by A2; hence g = f by A5, Def6 .= f9 by Def7, A4 ; ::_thesis: verum end; assume A6: c is terminal ; ::_thesis: c opp is initial let b be Object of (C opp); :: according to CAT_1:def_19 ::_thesis: ( not Hom ((c opp),b) = {} & ex b1 being Morphism of c opp ,b st for b2 being Morphism of c opp ,b holds b1 = b2 ) consider f being Morphism of opp b,c such that A7: for g being Morphism of opp b,c holds f = g by A6, CAT_1:def_18; A8: (opp b) opp = b ; A9: Hom ((opp b),c) <> {} by A6, CAT_1:def_18; reconsider f9 = f opp as Morphism of c opp ,b ; thus A10: Hom ((c opp),b) <> {} by A8, Th5, A9; ::_thesis: ex b1 being Morphism of c opp ,b st for b2 being Morphism of c opp ,b holds b1 = b2 take f9 ; ::_thesis: for b1 being Morphism of c opp ,b holds f9 = b1 let g be Morphism of c opp ,b; ::_thesis: f9 = g opp g is Morphism of opp b, opp (c opp) by A10, Th15; hence g = f by A7 .= f9 by Def6, A9 ; ::_thesis: verum end; definition let C, B be Category; let S be Function of the carrier' of (C opp), the carrier' of B; func /* S -> Function of the carrier' of C, the carrier' of B means :Def8: :: OPPCAT_1:def 8 for f being Morphism of C holds it . f = S . (f opp); existence ex b1 being Function of the carrier' of C, the carrier' of B st for f being Morphism of C holds b1 . f = S . (f opp) proof deffunc H1( Morphism of C) -> Element of the carrier' of B = S . (\$1 opp); thus ex F being Function of the carrier' of C, the carrier' of B st for f being Morphism of C holds F . f = H1(f) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of the carrier' of C, the carrier' of B st ( for f being Morphism of C holds b1 . f = S . (f opp) ) & ( for f being Morphism of C holds b2 . f = S . (f opp) ) holds b1 = b2 proof let T1, T2 be Function of the carrier' of C, the carrier' of B; ::_thesis: ( ( for f being Morphism of C holds T1 . f = S . (f opp) ) & ( for f being Morphism of C holds T2 . f = S . (f opp) ) implies T1 = T2 ) assume that A1: for f being Morphism of C holds T1 . f = S . (f opp) and A2: for f being Morphism of C holds T2 . f = S . (f opp) ; ::_thesis: T1 = T2 now__::_thesis:_for_f_being_Morphism_of_C_holds_T1_._f_=_T2_._f let f be Morphism of C; ::_thesis: T1 . f = T2 . f thus T1 . f = S . (f opp) by A1 .= T2 . f by A2 ; ::_thesis: verum end; hence T1 = T2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def8 defines /* OPPCAT_1:def_8_:_ for C, B being Category for S being Function of the carrier' of (C opp), the carrier' of B for b4 being Function of the carrier' of C, the carrier' of B holds ( b4 = /* S iff for f being Morphism of C holds b4 . f = S . (f opp) ); theorem :: OPPCAT_1:27 for C, B being Category for S being Function of the carrier' of (C opp), the carrier' of B for f being Morphism of (C opp) holds (/* S) . (opp f) = S . f proof let C, B be Category; ::_thesis: for S being Function of the carrier' of (C opp), the carrier' of B for f being Morphism of (C opp) holds (/* S) . (opp f) = S . f let S be Function of the carrier' of (C opp), the carrier' of B; ::_thesis: for f being Morphism of (C opp) holds (/* S) . (opp f) = S . f let f be Morphism of (C opp); ::_thesis: (/* S) . (opp f) = S . f thus (/* S) . (opp f) = S . ((opp f) opp) by Def8 .= S . f ; ::_thesis: verum end; Lm4: for C, B being Category for S being Functor of C opp ,B for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp)) proof let C, B be Category; ::_thesis: for S being Functor of C opp ,B for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp)) let S be Functor of C opp ,B; ::_thesis: for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp)) let c be Object of C; ::_thesis: (/* S) . (id c) = id ((Obj S) . (c opp)) reconsider i = id c as Morphism of C ; A1: Hom (c,c) <> {} ; thus (/* S) . (id c) = S . (i opp) by Def8 .= S . ((id c) opp) by A1, Def6 .= S . (id (c opp)) by Th20 .= id ((Obj S) . (c opp)) by CAT_1:68 ; ::_thesis: verum end; theorem Th28: :: OPPCAT_1:28 for C, B being Category for S being Functor of C opp ,B for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp) proof let C, B be Category; ::_thesis: for S being Functor of C opp ,B for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp) let S be Functor of C opp ,B; ::_thesis: for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp) let c be Object of C; ::_thesis: (Obj (/* S)) . c = (Obj S) . (c opp) A1: now__::_thesis:_for_c_being_Object_of_C_ex_d_being_Object_of_B_st_(/*_S)_._(id_c)_=_id_d let c be Object of C; ::_thesis: ex d being Object of B st (/* S) . (id c) = id d (/* S) . (id c) = id ((Obj S) . (c opp)) by Lm4; hence ex d being Object of B st (/* S) . (id c) = id d ; ::_thesis: verum end; (/* S) . (id c) = id ((Obj S) . (c opp)) by Lm4; hence (Obj (/* S)) . c = (Obj S) . (c opp) by A1, CAT_1:66; ::_thesis: verum end; theorem :: OPPCAT_1:29 for C, B being Category for S being Functor of C opp ,B for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c proof let C, B be Category; ::_thesis: for S being Functor of C opp ,B for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c let S be Functor of C opp ,B; ::_thesis: for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c let c be Object of (C opp); ::_thesis: (Obj (/* S)) . (opp c) = (Obj S) . c thus (Obj (/* S)) . (opp c) = (Obj S) . ((opp c) opp) by Th28 .= (Obj S) . c ; ::_thesis: verum end; Lm5: for C, B being Category for S being Functor of C opp ,B for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c) proof let C, B be Category; ::_thesis: for S being Functor of C opp ,B for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c) let S be Functor of C opp ,B; ::_thesis: for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c) let c be Object of C; ::_thesis: (/* S) . (id c) = id ((Obj (/* S)) . c) reconsider i = id c as Morphism of C ; A1: Hom (c,c) <> {} ; thus (/* S) . (id c) = S . (i opp) by Def8 .= S . ((id c) opp) by Def6, A1 .= S . (id (c opp)) by Th20 .= id ((Obj S) . (c opp)) by CAT_1:68 .= id ((Obj (/* S)) . c) by Th28 ; ::_thesis: verum end; Lm6: now__::_thesis:_for_C,_B_being_Category for_S_being_Functor_of_C_opp_,B for_c_being_Object_of_C_ex_d_being_Object_of_B_st_(/*_S)_._(id_c)_=_id_d let C, B be Category; ::_thesis: for S being Functor of C opp ,B for c being Object of C ex d being Object of B st (/* S) . (id c) = id d let S be Functor of C opp ,B; ::_thesis: for c being Object of C ex d being Object of B st (/* S) . (id c) = id d let c be Object of C; ::_thesis: ex d being Object of B st (/* S) . (id c) = id d (/* S) . (id c) = id ((Obj (/* S)) . c) by Lm5; hence ex d being Object of B st (/* S) . (id c) = id d ; ::_thesis: verum end; Lm7: for C, B being Category for S being Functor of C opp ,B for f being Morphism of C holds ( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) ) proof let C, B be Category; ::_thesis: for S being Functor of C opp ,B for f being Morphism of C holds ( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) ) let S be Functor of C opp ,B; ::_thesis: for f being Morphism of C holds ( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) ) let f be Morphism of C; ::_thesis: ( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) ) A1: (Obj (/* S)) . (cod f) = (Obj S) . ((cod f) opp) by Th28 .= (Obj S) . (dom (f opp)) .= dom (S . (f opp)) by CAT_1:69 ; (Obj (/* S)) . (dom f) = (Obj S) . ((dom f) opp) by Th28 .= (Obj S) . (cod (f opp)) .= cod (S . (f opp)) by CAT_1:69 ; hence ( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) ) by A1, Def8; ::_thesis: verum end; Lm8: now__::_thesis:_for_C,_B_being_Category for_S_being_Functor_of_C_opp_,B for_f_being_Morphism_of_C_holds_ (_(/*_S)_._(id_(dom_f))_=_id_(cod_((/*_S)_._f))_&_(/*_S)_._(id_(cod_f))_=_id_(dom_((/*_S)_._f))_) let C, B be Category; ::_thesis: for S being Functor of C opp ,B for f being Morphism of C holds ( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) ) let S be Functor of C opp ,B; ::_thesis: for f being Morphism of C holds ( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) ) let f be Morphism of C; ::_thesis: ( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) ) thus (/* S) . (id (dom f)) = id ((Obj (/* S)) . (dom f)) by Lm5 .= id (cod ((/* S) . f)) by Lm7 ; ::_thesis: (/* S) . (id (cod f)) = id (dom ((/* S) . f)) thus (/* S) . (id (cod f)) = id ((Obj (/* S)) . (cod f)) by Lm5 .= id (dom ((/* S) . f)) by Lm7 ; ::_thesis: verum end; Lm9: for C, B being Category for S being Functor of C opp ,B for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) proof let C, B be Category; ::_thesis: for S being Functor of C opp ,B for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) let S be Functor of C opp ,B; ::_thesis: for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) let a, b, c be Object of C; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) ) assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; ::_thesis: for f being Morphism of a,b for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) A2: ( Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} ) by A1, Th5; let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) let g be Morphism of b,c; ::_thesis: (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) A3: dom g = b by A1, CAT_1:5 .= cod f by A1, CAT_1:5 ; A4: dom (f opp) = b opp by A2, CAT_1:5 .= cod f by A1, CAT_1:5 ; A5: cod (g opp) = b opp by A2, CAT_1:5 .= dom g by A1, CAT_1:5 ; A6: S . (f opp) = S . (f opp) by A1, Def6 .= (/* S) . f by Def8 ; A7: S . (g opp) = S . (g opp) by A1, Def6 .= (/* S) . g by Def8 ; thus (/* S) . (g (*) f) = S . ((g (*) f) opp) by Def8 .= S . ((f opp) (*) (g opp)) by Th16, A1 .= ((/* S) . f) (*) ((/* S) . g) by A7, A6, A5, A3, A4, CAT_1:64 ; ::_thesis: verum end; definition let C, D be Category; mode Contravariant_Functor of C,D -> Function of the carrier' of C, the carrier' of D means :Def9: :: OPPCAT_1:def 9 ( ( 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 (cod (it . f)) & it . (id (cod f)) = id (dom (it . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds it . (g (*) f) = (it . f) (*) (it . g) ) ); existence ex b1 being Function of the carrier' of C, the carrier' of D st ( ( for c being Object of C ex d being Object of D st b1 . (id c) = id d ) & ( for f being Morphism of C holds ( b1 . (id (dom f)) = id (cod (b1 . f)) & b1 . (id (cod f)) = id (dom (b1 . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds b1 . (g (*) f) = (b1 . f) (*) (b1 . g) ) ) proof set S = the Functor of C opp ,D; take /* the Functor of C opp ,D ; ::_thesis: ( ( for c being Object of C ex d being Object of D st (/* the Functor of C opp ,D) . (id c) = id d ) & ( for f being Morphism of C holds ( (/* the Functor of C opp ,D) . (id (dom f)) = id (cod ((/* the Functor of C opp ,D) . f)) & (/* the Functor of C opp ,D) . (id (cod f)) = id (dom ((/* the Functor of C opp ,D) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ) ) thus for c being Object of C ex d being Object of D st (/* the Functor of C opp ,D) . (id c) = id d by Lm6; ::_thesis: ( ( for f being Morphism of C holds ( (/* the Functor of C opp ,D) . (id (dom f)) = id (cod ((/* the Functor of C opp ,D) . f)) & (/* the Functor of C opp ,D) . (id (cod f)) = id (dom ((/* the Functor of C opp ,D) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ) ) thus for f being Morphism of C holds ( (/* the Functor of C opp ,D) . (id (dom f)) = id (cod ((/* the Functor of C opp ,D) . f)) & (/* the Functor of C opp ,D) . (id (cod f)) = id (dom ((/* the Functor of C opp ,D) . f)) ) by Lm8; ::_thesis: for f, g being Morphism of C st dom g = cod f holds (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ) assume A1: dom g = cod f ; ::_thesis: (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) reconsider ff = f as Morphism of dom f, cod f by CAT_1:4; reconsider gg = g as Morphism of cod f, cod g by CAT_1:4, A1; ( Hom ((dom f),(cod f)) <> {} & Hom ((dom g),(cod g)) <> {} ) by CAT_1:2; then (/* the Functor of C opp ,D) . (gg (*) ff) = ((/* the Functor of C opp ,D) . ff) (*) ((/* the Functor of C opp ,D) . gg) by A1, Lm9; hence (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ; ::_thesis: verum end; end; :: deftheorem Def9 defines Contravariant_Functor OPPCAT_1:def_9_:_ for C, D being Category for b3 being Function of the carrier' of C, the carrier' of D holds ( b3 is Contravariant_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 (cod (b3 . f)) & b3 . (id (cod f)) = id (dom (b3 . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds b3 . (g (*) f) = (b3 . f) (*) (b3 . g) ) ) ); theorem Th30: :: OPPCAT_1:30 for C, D being Category for S being Contravariant_Functor of C,D for c being Object of C for d being Object of D st S . (id c) = id d holds (Obj S) . c = d proof let C, D be Category; ::_thesis: for S being Contravariant_Functor of C,D for c being Object of C for d being Object of D st S . (id c) = id d holds (Obj S) . c = d let S be Contravariant_Functor of C,D; ::_thesis: for c being Object of C for d being Object of D st S . (id c) = id d holds (Obj S) . c = d let c be Object of C; ::_thesis: for d being Object of D st S . (id c) = id d holds (Obj S) . c = d let d be Object of D; ::_thesis: ( S . (id c) = id d implies (Obj S) . c = d ) for c being Object of C ex d being Object of D st S . (id c) = id d by Def9; hence ( S . (id c) = id d implies (Obj S) . c = d ) by CAT_1:66; ::_thesis: verum end; theorem Th31: :: OPPCAT_1:31 for C, D being Category for S being Contravariant_Functor of C,D for c being Object of C holds S . (id c) = id ((Obj S) . c) proof let C, D be Category; ::_thesis: for S being Contravariant_Functor of C,D for c being Object of C holds S . (id c) = id ((Obj S) . c) let S be Contravariant_Functor of C,D; ::_thesis: for c being Object of C holds S . (id c) = id ((Obj S) . c) let c be Object of C; ::_thesis: S . (id c) = id ((Obj S) . c) ex d being Object of D st S . (id c) = id d by Def9; hence S . (id c) = id ((Obj S) . c) by Th30; ::_thesis: verum end; theorem Th32: :: OPPCAT_1:32 for C, D being Category for S being Contravariant_Functor of C,D for f being Morphism of C holds ( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) ) proof let C, D be Category; ::_thesis: for S being Contravariant_Functor of C,D for f being Morphism of C holds ( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) ) let S be Contravariant_Functor of C,D; ::_thesis: for f being Morphism of C holds ( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) ) let f be Morphism of C; ::_thesis: ( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) ) ( S . (id (dom f)) = id (cod (S . f)) & S . (id (cod f)) = id (dom (S . f)) ) by Def9; hence ( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) ) by Th30; ::_thesis: verum end; theorem Th33: :: OPPCAT_1:33 for C, D being Category for S being Contravariant_Functor of C,D for f, g being Morphism of C st dom g = cod f holds dom (S . f) = cod (S . g) proof let C, D be Category; ::_thesis: for S being Contravariant_Functor of C,D for f, g being Morphism of C st dom g = cod f holds dom (S . f) = cod (S . g) let S be Contravariant_Functor of C,D; ::_thesis: for f, g being Morphism of C st dom g = cod f holds dom (S . f) = cod (S . g) let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies dom (S . f) = cod (S . g) ) assume dom g = cod f ; ::_thesis: dom (S . f) = cod (S . g) hence dom (S . f) = (Obj S) . (dom g) by Th32 .= cod (S . g) by Th32 ; ::_thesis: verum end; theorem Th34: :: OPPCAT_1:34 for C, B being Category for S being Functor of C opp ,B holds /* S is Contravariant_Functor of C,B proof let C, B be Category; ::_thesis: for S being Functor of C opp ,B holds /* S is Contravariant_Functor of C,B let S be Functor of C opp ,B; ::_thesis: /* S is Contravariant_Functor of C,B thus for c being Object of C ex d being Object of B st (/* S) . (id c) = id d by Lm6; :: according to OPPCAT_1:def_9 ::_thesis: ( ( for f being Morphism of C holds ( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) ) ) thus for f being Morphism of C holds ( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) ) by Lm8; ::_thesis: for f, g being Morphism of C st dom g = cod f holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) ) assume A1: dom g = cod f ; ::_thesis: (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) reconsider ff = f as Morphism of dom f, cod f by CAT_1:4; reconsider gg = g as Morphism of cod f, cod g by CAT_1:4, A1; ( Hom ((dom f),(cod f)) <> {} & Hom ((dom g),(cod g)) <> {} ) by CAT_1:2; then (/* S) . (gg (*) ff) = ((/* S) . ff) (*) ((/* S) . gg) by A1, Lm9; hence (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) ; ::_thesis: verum end; theorem Th35: :: OPPCAT_1:35 for C, B, D being Category for S1 being Contravariant_Functor of C,B for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D proof let C, B, D be Category; ::_thesis: for S1 being Contravariant_Functor of C,B for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D let S1 be Contravariant_Functor of C,B; ::_thesis: for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D let S2 be Contravariant_Functor of B,D; ::_thesis: S2 * S1 is Functor of C,D set T = S2 * S1; now__::_thesis:_(_(_for_c_being_Object_of_C_ex_d_being_Object_of_D_st_(S2_*_S1)_._(id_c)_=_id_d_)_&_(_for_f_being_Morphism_of_C_holds_ (_(S2_*_S1)_._(id_(dom_f))_=_id_(dom_((S2_*_S1)_._f))_&_(S2_*_S1)_._(id_(cod_f))_=_id_(cod_((S2_*_S1)_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_ (S2_*_S1)_._(g_(*)_f)_=_((S2_*_S1)_._g)_(*)_((S2_*_S1)_._f)_)_) thus for c being Object of C ex d being Object of D st (S2 * S1) . (id c) = id d ::_thesis: ( ( for f being Morphism of C holds ( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds (S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f) ) ) proof let c be Object of C; ::_thesis: ex d being Object of D st (S2 * S1) . (id c) = id d consider b being Object of B such that A1: S1 . (id c) = id b by Def9; consider d being Object of D such that A2: S2 . (id b) = id d by Def9; take d ; ::_thesis: (S2 * S1) . (id c) = id d thus (S2 * S1) . (id c) = id d by A1, A2, FUNCT_2:15; ::_thesis: verum end; thus for f being Morphism of C holds ( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds (S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f) proof let f be Morphism of C; ::_thesis: ( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) ) thus (S2 * S1) . (id (dom f)) = S2 . (S1 . (id (dom f))) by FUNCT_2:15 .= S2 . (id (cod (S1 . f))) by Def9 .= id (dom (S2 . (S1 . f))) by Def9 .= id (dom ((S2 * S1) . f)) by FUNCT_2:15 ; ::_thesis: (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) thus (S2 * S1) . (id (cod f)) = S2 . (S1 . (id (cod f))) by FUNCT_2:15 .= S2 . (id (dom (S1 . f))) by Def9 .= id (cod (S2 . (S1 . f))) by Def9 .= id (cod ((S2 * S1) . f)) by FUNCT_2:15 ; ::_thesis: verum end; let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f) ) assume A3: dom g = cod f ; ::_thesis: (S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f) then A4: cod (S1 . g) = dom (S1 . f) by Th33; thus (S2 * S1) . (g (*) f) = S2 . (S1 . (g (*) f)) by FUNCT_2:15 .= S2 . ((S1 . f) (*) (S1 . g)) by A3, Def9 .= (S2 . (S1 . g)) (*) (S2 . (S1 . f)) by A4, Def9 .= ((S2 * S1) . g) (*) (S2 . (S1 . f)) by FUNCT_2:15 .= ((S2 * S1) . g) (*) ((S2 * S1) . f) by FUNCT_2:15 ; ::_thesis: verum end; hence S2 * S1 is Functor of C,D by CAT_1:61; ::_thesis: verum end; Lm10: for C, B being Category for S being Contravariant_Functor of C opp ,B for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp)) proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C opp ,B for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp)) let S be Contravariant_Functor of C opp ,B; ::_thesis: for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp)) let c be Object of C; ::_thesis: (/* S) . (id c) = id ((Obj S) . (c opp)) reconsider i = id c as Morphism of C ; A1: Hom (c,c) <> {} ; thus (/* S) . (id c) = S . (i opp) by Def8 .= S . ((id c) opp) by Def6, A1 .= S . (id (c opp)) by Th20 .= id ((Obj S) . (c opp)) by Th31 ; ::_thesis: verum end; theorem Th36: :: OPPCAT_1:36 for C, B being Category for S being Contravariant_Functor of C opp ,B for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp) proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C opp ,B for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp) let S be Contravariant_Functor of C opp ,B; ::_thesis: for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp) let c be Object of C; ::_thesis: (Obj (/* S)) . c = (Obj S) . (c opp) A1: now__::_thesis:_for_c_being_Object_of_C_ex_d_being_Object_of_B_st_(/*_S)_._(id_c)_=_id_d let c be Object of C; ::_thesis: ex d being Object of B st (/* S) . (id c) = id d (/* S) . (id c) = id ((Obj S) . (c opp)) by Lm10; hence ex d being Object of B st (/* S) . (id c) = id d ; ::_thesis: verum end; (/* S) . (id c) = id ((Obj S) . (c opp)) by Lm10; hence (Obj (/* S)) . c = (Obj S) . (c opp) by A1, CAT_1:66; ::_thesis: verum end; theorem :: OPPCAT_1:37 for C, B being Category for S being Contravariant_Functor of C opp ,B for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C opp ,B for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c let S be Contravariant_Functor of C opp ,B; ::_thesis: for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c let c be Object of (C opp); ::_thesis: (Obj (/* S)) . (opp c) = (Obj S) . c thus (Obj (/* S)) . (opp c) = (Obj S) . ((opp c) opp) by Th36 .= (Obj S) . c ; ::_thesis: verum end; Lm11: for C, B being Category for S being Contravariant_Functor of C opp ,B for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c) proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C opp ,B for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c) let S be Contravariant_Functor of C opp ,B; ::_thesis: for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c) let c be Object of C; ::_thesis: (/* S) . (id c) = id ((Obj (/* S)) . c) reconsider i = id c as Morphism of C ; A1: Hom (c,c) <> {} ; thus (/* S) . (id c) = S . (i opp) by Def8 .= S . ((id c) opp) by Def6, A1 .= S . (id (c opp)) by Th20 .= id ((Obj S) . (c opp)) by Th31 .= id ((Obj (/* S)) . c) by Th36 ; ::_thesis: verum end; Lm12: for C, B being Category for S being Contravariant_Functor of C opp ,B for f being Morphism of C holds ( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) ) proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C opp ,B for f being Morphism of C holds ( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) ) let S be Contravariant_Functor of C opp ,B; ::_thesis: for f being Morphism of C holds ( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) ) let f be Morphism of C; ::_thesis: ( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) ) A1: (Obj (/* S)) . (cod f) = (Obj S) . ((cod f) opp) by Th36 .= (Obj S) . (dom (f opp)) .= cod (S . (f opp)) by Th32 ; (Obj (/* S)) . (dom f) = (Obj S) . ((dom f) opp) by Th36 .= (Obj S) . (cod (f opp)) .= dom (S . (f opp)) by Th32 ; hence ( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) ) by A1, Def8; ::_thesis: verum end; theorem :: OPPCAT_1:38 for C, B being Category for S being Contravariant_Functor of C opp ,B holds /* S is Functor of C,B proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C opp ,B holds /* S is Functor of C,B let S be Contravariant_Functor of C opp ,B; ::_thesis: /* S is Functor of C,B now__::_thesis:_(_(_for_c_being_Object_of_C_ex_d_being_Object_of_B_st_(/*_S)_._(id_c)_=_id_d_)_&_(_for_f_being_Morphism_of_C_holds_ (_(/*_S)_._(id_(dom_f))_=_id_(dom_((/*_S)_._f))_&_(/*_S)_._(id_(cod_f))_=_id_(cod_((/*_S)_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_ (/*_S)_._(g_(*)_f)_=_((/*_S)_._g)_(*)_((/*_S)_._f)_)_) thus for c being Object of C ex d being Object of B st (/* S) . (id c) = id d ::_thesis: ( ( for f being Morphism of C holds ( (/* S) . (id (dom f)) = id (dom ((/* S) . f)) & (/* S) . (id (cod f)) = id (cod ((/* S) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds (/* S) . (g (*) f) = ((/* S) . g) (*) ((/* S) . f) ) ) proof let c be Object of C; ::_thesis: ex d being Object of B st (/* S) . (id c) = id d (/* S) . (id c) = id ((Obj (/* S)) . c) by Lm11; hence ex d being Object of B st (/* S) . (id c) = id d ; ::_thesis: verum end; thus for f being Morphism of C holds ( (/* S) . (id (dom f)) = id (dom ((/* S) . f)) & (/* S) . (id (cod f)) = id (cod ((/* S) . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds (/* S) . (g (*) f) = ((/* S) . g) (*) ((/* S) . f) proof let f be Morphism of C; ::_thesis: ( (/* S) . (id (dom f)) = id (dom ((/* S) . f)) & (/* S) . (id (cod f)) = id (cod ((/* S) . f)) ) thus (/* S) . (id (dom f)) = id ((Obj (/* S)) . (dom f)) by Lm11 .= id (dom ((/* S) . f)) by Lm12 ; ::_thesis: (/* S) . (id (cod f)) = id (cod ((/* S) . f)) thus (/* S) . (id (cod f)) = id ((Obj (/* S)) . (cod f)) by Lm11 .= id (cod ((/* S) . f)) by Lm12 ; ::_thesis: verum end; let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (/* S) . (g (*) f) = ((/* S) . g) (*) ((/* S) . f) ) assume A1: dom g = cod f ; ::_thesis: (/* S) . (g (*) f) = ((/* S) . g) (*) ((/* S) . f) A2: ( dom (f opp) = cod f & cod (g opp) = dom g ) ; reconsider ff = f as Morphism of dom f, cod f by CAT_1:4; reconsider gg = g as Morphism of cod f, cod g by CAT_1:4, A1; A3: ( Hom ((dom f),(cod f)) <> {} & Hom ((dom g),(cod g)) <> {} ) by CAT_1:2; then A4: ff opp = f opp by Def6; A5: gg opp = g opp by Def6, A3, A1; thus (/* S) . (g (*) f) = S . ((g (*) f) opp) by Def8 .= S . ((f opp) (*) (g opp)) by A4, A5, A3, A1, Th16 .= (S . (g opp)) (*) (S . (f opp)) by A1, A2, Def9 .= ((/* S) . g) (*) (S . (f opp)) by Def8 .= ((/* S) . g) (*) ((/* S) . f) by Def8 ; ::_thesis: verum end; hence /* S is Functor of C,B by CAT_1:61; ::_thesis: verum end; definition let C, B be Category; let S be Function of the carrier' of C, the carrier' of B; func *' S -> Function of the carrier' of (C opp), the carrier' of B means :Def10: :: OPPCAT_1:def 10 for f being Morphism of (C opp) holds it . f = S . (opp f); existence ex b1 being Function of the carrier' of (C opp), the carrier' of B st for f being Morphism of (C opp) holds b1 . f = S . (opp f) proof deffunc H1( Morphism of (C opp)) -> Element of the carrier' of B = S . (opp \$1); thus ex F being Function of the carrier' of (C opp), the carrier' of B st for f being Morphism of (C opp) holds F . f = H1(f) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of the carrier' of (C opp), the carrier' of B st ( for f being Morphism of (C opp) holds b1 . f = S . (opp f) ) & ( for f being Morphism of (C opp) holds b2 . f = S . (opp f) ) holds b1 = b2 proof let T1, T2 be Function of the carrier' of (C opp), the carrier' of B; ::_thesis: ( ( for f being Morphism of (C opp) holds T1 . f = S . (opp f) ) & ( for f being Morphism of (C opp) holds T2 . f = S . (opp f) ) implies T1 = T2 ) assume that A1: for f being Morphism of (C opp) holds T1 . f = S . (opp f) and A2: for f being Morphism of (C opp) holds T2 . f = S . (opp f) ; ::_thesis: T1 = T2 now__::_thesis:_for_f_being_Morphism_of_(C_opp)_holds_T1_._f_=_T2_._f let f be Morphism of (C opp); ::_thesis: T1 . f = T2 . f thus T1 . f = S . (opp f) by A1 .= T2 . f by A2 ; ::_thesis: verum end; hence T1 = T2 by FUNCT_2:63; ::_thesis: verum end; funcS *' -> Function of the carrier' of C, the carrier' of (B opp) means :Def11: :: OPPCAT_1:def 11 for f being Morphism of C holds it . f = (S . f) opp ; existence ex b1 being Function of the carrier' of C, the carrier' of (B opp) st for f being Morphism of C holds b1 . f = (S . f) opp proof deffunc H1( Morphism of C) -> Morphism of (B opp) = (S . \$1) opp ; thus ex F being Function of the carrier' of C, the carrier' of (B opp) st for f being Morphism of C holds F . f = H1(f) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of the carrier' of C, the carrier' of (B opp) st ( for f being Morphism of C holds b1 . f = (S . f) opp ) & ( for f being Morphism of C holds b2 . f = (S . f) opp ) holds b1 = b2 proof let T1, T2 be Function of the carrier' of C, the carrier' of (B opp); ::_thesis: ( ( for f being Morphism of C holds T1 . f = (S . f) opp ) & ( for f being Morphism of C holds T2 . f = (S . f) opp ) implies T1 = T2 ) assume that A3: for f being Morphism of C holds T1 . f = (S . f) opp and A4: for f being Morphism of C holds T2 . f = (S . f) opp ; ::_thesis: T1 = T2 now__::_thesis:_for_f_being_Morphism_of_C_holds_T1_._f_=_T2_._f let f be Morphism of C; ::_thesis: T1 . f = T2 . f thus T1 . f = (S . f) opp by A3 .= T2 . f by A4 ; ::_thesis: verum end; hence T1 = T2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def10 defines *' OPPCAT_1:def_10_:_ for C, B being Category for S being Function of the carrier' of C, the carrier' of B for b4 being Function of the carrier' of (C opp), the carrier' of B holds ( b4 = *' S iff for f being Morphism of (C opp) holds b4 . f = S . (opp f) ); :: deftheorem Def11 defines *' OPPCAT_1:def_11_:_ for C, B being Category for S being Function of the carrier' of C, the carrier' of B for b4 being Function of the carrier' of C, the carrier' of (B opp) holds ( b4 = S *' iff for f being Morphism of C holds b4 . f = (S . f) opp ); theorem :: OPPCAT_1:39 for C, B being Category for S being Function of the carrier' of C, the carrier' of B for f being Morphism of C holds (*' S) . (f opp) = S . f proof let C, B be Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of B for f being Morphism of C holds (*' S) . (f opp) = S . f let S be Function of the carrier' of C, the carrier' of B; ::_thesis: for f being Morphism of C holds (*' S) . (f opp) = S . f let f be Morphism of C; ::_thesis: (*' S) . (f opp) = S . f thus (*' S) . (f opp) = S . (opp (f opp)) by Def10 .= S . f ; ::_thesis: verum end; Lm13: for C, B being Category for S being Functor of C,B for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c)) proof let C, B be Category; ::_thesis: for S being Functor of C,B for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c)) let S be Functor of C,B; ::_thesis: for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c)) let c be Object of (C opp); ::_thesis: (*' S) . (id c) = id ((Obj S) . (opp c)) thus (*' S) . (id c) = S . (opp (id c)) by Def10 .= S . (id (opp c)) by Th21 .= id ((Obj S) . (opp c)) by CAT_1:68 ; ::_thesis: verum end; theorem Th40: :: OPPCAT_1:40 for C, B being Category for S being Functor of C,B for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c) proof let C, B be Category; ::_thesis: for S being Functor of C,B for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c) let S be Functor of C,B; ::_thesis: for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c) let c be Object of (C opp); ::_thesis: (Obj (*' S)) . c = (Obj S) . (opp c) now__::_thesis:_(_(*'_S)_._(id_c)_=_id_((Obj_S)_._(opp_c))_&_(_for_c_being_Object_of_(C_opp)_ex_d_being_Object_of_B_st_(*'_S)_._(id_c)_=_id_d_)_) thus (*' S) . (id c) = id ((Obj S) . (opp c)) by Lm13; ::_thesis: for c being Object of (C opp) ex d being Object of B st (*' S) . (id c) = id d let c be Object of (C opp); ::_thesis: ex d being Object of B st (*' S) . (id c) = id d (*' S) . (id c) = id ((Obj S) . (opp c)) by Lm13; hence ex d being Object of B st (*' S) . (id c) = id d ; ::_thesis: verum end; hence (Obj (*' S)) . c = (Obj S) . (opp c) by CAT_1:66; ::_thesis: verum end; theorem :: OPPCAT_1:41 for C, B being Category for S being Functor of C,B for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c proof let C, B be Category; ::_thesis: for S being Functor of C,B for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c let S be Functor of C,B; ::_thesis: for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c let c be Object of C; ::_thesis: (Obj (*' S)) . (c opp) = (Obj S) . c thus (Obj (*' S)) . (c opp) = (Obj S) . (opp (c opp)) by Th40 .= (Obj S) . c ; ::_thesis: verum end; Lm14: for C, B being Category for S being Functor of C,B for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp) proof let C, B be Category; ::_thesis: for S being Functor of C,B for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp) let S be Functor of C,B; ::_thesis: for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp) let c be Object of C; ::_thesis: (S *') . (id c) = id (((Obj S) . c) opp) A1: Hom (((Obj S) . c),((Obj S) . c)) <> {} ; thus (S *') . (id c) = (S . (id c)) opp by Def11 .= (id ((Obj S) . c)) opp by CAT_1:68 .= (id ((Obj S) . c)) opp by Def6, A1 .= id (((Obj S) . c) opp) by Th20 ; ::_thesis: verum end; theorem Th42: :: OPPCAT_1:42 for C, B being Category for S being Functor of C,B for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp proof let C, B be Category; ::_thesis: for S being Functor of C,B for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp let S be Functor of C,B; ::_thesis: for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp let c be Object of C; ::_thesis: (Obj (S *')) . c = ((Obj S) . c) opp now__::_thesis:_(_(S_*')_._(id_c)_=_id_(((Obj_S)_._c)_opp)_&_(_for_c_being_Object_of_C_ex_d_being_Object_of_(B_opp)_st_(S_*')_._(id_c)_=_id_d_)_) thus (S *') . (id c) = id (((Obj S) . c) opp) by Lm14; ::_thesis: for c being Object of C ex d being Object of (B opp) st (S *') . (id c) = id d let c be Object of C; ::_thesis: ex d being Object of (B opp) st (S *') . (id c) = id d (S *') . (id c) = id (((Obj S) . c) opp) by Lm14; hence ex d being Object of (B opp) st (S *') . (id c) = id d ; ::_thesis: verum end; hence (Obj (S *')) . c = ((Obj S) . c) opp by CAT_1:66; ::_thesis: verum end; Lm15: for C, B being Category for S being Contravariant_Functor of C,B for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c)) proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c)) let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c)) let c be Object of (C opp); ::_thesis: (*' S) . (id c) = id ((Obj S) . (opp c)) thus (*' S) . (id c) = S . (opp (id c)) by Def10 .= S . (id (opp c)) by Th21 .= id ((Obj S) . (opp c)) by Th31 ; ::_thesis: verum end; theorem Th43: :: OPPCAT_1:43 for C, B being Category for S being Contravariant_Functor of C,B for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c) proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c) let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c) let c be Object of (C opp); ::_thesis: (Obj (*' S)) . c = (Obj S) . (opp c) now__::_thesis:_(_(*'_S)_._(id_c)_=_id_((Obj_S)_._(opp_c))_&_(_for_c_being_Object_of_(C_opp)_ex_d_being_Object_of_B_st_(*'_S)_._(id_c)_=_id_d_)_) thus (*' S) . (id c) = id ((Obj S) . (opp c)) by Lm15; ::_thesis: for c being Object of (C opp) ex d being Object of B st (*' S) . (id c) = id d let c be Object of (C opp); ::_thesis: ex d being Object of B st (*' S) . (id c) = id d (*' S) . (id c) = id ((Obj S) . (opp c)) by Lm15; hence ex d being Object of B st (*' S) . (id c) = id d ; ::_thesis: verum end; hence (Obj (*' S)) . c = (Obj S) . (opp c) by CAT_1:66; ::_thesis: verum end; theorem :: OPPCAT_1:44 for C, B being Category for S being Contravariant_Functor of C,B for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c let c be Object of C; ::_thesis: (Obj (*' S)) . (c opp) = (Obj S) . c thus (Obj (*' S)) . (c opp) = (Obj S) . (opp (c opp)) by Th43 .= (Obj S) . c ; ::_thesis: verum end; Lm16: for C, B being Category for S being Contravariant_Functor of C,B for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp) proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp) let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp) let c be Object of C; ::_thesis: (S *') . (id c) = id (((Obj S) . c) opp) A1: Hom (((Obj S) . c),((Obj S) . c)) <> {} ; thus (S *') . (id c) = (S . (id c)) opp by Def11 .= (id ((Obj S) . c)) opp by Th31 .= (id ((Obj S) . c)) opp by Def6, A1 .= id (((Obj S) . c) opp) by Th20 ; ::_thesis: verum end; theorem Th45: :: OPPCAT_1:45 for C, B being Category for S being Contravariant_Functor of C,B for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp let c be Object of C; ::_thesis: (Obj (S *')) . c = ((Obj S) . c) opp now__::_thesis:_(_(S_*')_._(id_c)_=_id_(((Obj_S)_._c)_opp)_&_(_for_c_being_Object_of_C_ex_d_being_Object_of_(B_opp)_st_(S_*')_._(id_c)_=_id_d_)_) thus (S *') . (id c) = id (((Obj S) . c) opp) by Lm16; ::_thesis: for c being Object of C ex d being Object of (B opp) st (S *') . (id c) = id d let c be Object of C; ::_thesis: ex d being Object of (B opp) st (S *') . (id c) = id d (S *') . (id c) = id (((Obj S) . c) opp) by Lm16; hence ex d being Object of (B opp) st (S *') . (id c) = id d ; ::_thesis: verum end; hence (Obj (S *')) . c = ((Obj S) . c) opp by CAT_1:66; ::_thesis: verum end; Lm17: for C, D being Category for F being Function of the carrier' of C, the carrier' of D for f being Morphism of (C opp) holds ((*' F) *') . f = (F . (opp f)) opp proof let C, D be Category; ::_thesis: for F being Function of the carrier' of C, the carrier' of D for f being Morphism of (C opp) holds ((*' F) *') . f = (F . (opp f)) opp let F be Function of the carrier' of C, the carrier' of D; ::_thesis: for f being Morphism of (C opp) holds ((*' F) *') . f = (F . (opp f)) opp let f be Morphism of (C opp); ::_thesis: ((*' F) *') . f = (F . (opp f)) opp thus ((*' F) *') . f = ((*' F) . f) opp by Def11 .= (F . (opp f)) opp by Def10 ; ::_thesis: verum end; theorem Th46: :: OPPCAT_1:46 for C, D being Category for F being Function of the carrier' of C, the carrier' of D for f being Morphism of C holds ((*' F) *') . (f opp) = (F . f) opp proof let C, D be Category; ::_thesis: for F being Function of the carrier' of C, the carrier' of D for f being Morphism of C holds ((*' F) *') . (f opp) = (F . f) opp let F be Function of the carrier' of C, the carrier' of D; ::_thesis: for f being Morphism of C holds ((*' F) *') . (f opp) = (F . f) opp let f be Morphism of C; ::_thesis: ((*' F) *') . (f opp) = (F . f) opp thus ((*' F) *') . (f opp) = (F . (opp (f opp))) opp by Lm17 .= (F . f) opp ; ::_thesis: verum end; theorem Th47: :: OPPCAT_1:47 for C, D being Category for S being Function of the carrier' of C, the carrier' of D holds /* (*' S) = S proof let C, D be Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of D holds /* (*' S) = S let S be Function of the carrier' of C, the carrier' of D; ::_thesis: /* (*' S) = S now__::_thesis:_for_f_being_Morphism_of_C_holds_(/*_(*'_S))_._f_=_S_._f let f be Morphism of C; ::_thesis: (/* (*' S)) . f = S . f thus (/* (*' S)) . f = (*' S) . (f opp) by Def8 .= S . (opp (f opp)) by Def10 .= S . f ; ::_thesis: verum end; hence /* (*' S) = S by FUNCT_2:63; ::_thesis: verum end; theorem :: OPPCAT_1:48 for C, D being Category for S being Function of the carrier' of (C opp), the carrier' of D holds *' (/* S) = S proof let C, D be Category; ::_thesis: for S being Function of the carrier' of (C opp), the carrier' of D holds *' (/* S) = S let S be Function of the carrier' of (C opp), the carrier' of D; ::_thesis: *' (/* S) = S now__::_thesis:_for_f_being_Morphism_of_(C_opp)_holds_(*'_(/*_S))_._f_=_S_._f let f be Morphism of (C opp); ::_thesis: (*' (/* S)) . f = S . f thus (*' (/* S)) . f = (/* S) . (opp f) by Def10 .= S . ((opp f) opp) by Def8 .= S . f ; ::_thesis: verum end; hence *' (/* S) = S by FUNCT_2:63; ::_thesis: verum end; theorem :: OPPCAT_1:49 for C, D being Category for S being Function of the carrier' of C, the carrier' of D holds (*' S) *' = *' (S *') proof let C, D be Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of D holds (*' S) *' = *' (S *') let S be Function of the carrier' of C, the carrier' of D; ::_thesis: (*' S) *' = *' (S *') now__::_thesis:_for_f_being_Morphism_of_(C_opp)_holds_((*'_S)_*')_._f_=_(*'_(S_*'))_._f let f be Morphism of (C opp); ::_thesis: ((*' S) *') . f = (*' (S *')) . f thus ((*' S) *') . f = ((*' S) . f) opp by Def11 .= (S . (opp f)) opp by Def10 .= (S *') . (opp f) by Def11 .= (*' (S *')) . f by Def10 ; ::_thesis: verum end; hence (*' S) *' = *' (S *') by FUNCT_2:63; ::_thesis: verum end; theorem :: OPPCAT_1:50 for C being Category for D being strict Category for S being Function of the carrier' of C, the carrier' of D holds (S *') *' = S proof let C be Category; ::_thesis: for D being strict Category for S being Function of the carrier' of C, the carrier' of D holds (S *') *' = S let D be strict Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of D holds (S *') *' = S let S be Function of the carrier' of C, the carrier' of D; ::_thesis: (S *') *' = S now__::_thesis:_(_(D_opp)_opp_=_D_&_(_for_f_being_Morphism_of_C_holds_((S_*')_*')_._f_=_S_._f_)_) thus (D opp) opp = D by FUNCT_4:53; ::_thesis: for f being Morphism of C holds ((S *') *') . f = S . f let f be Morphism of C; ::_thesis: ((S *') *') . f = S . f thus ((S *') *') . f = ((S *') . f) opp by Def11 .= ((S . f) opp) opp by Def11 .= S . f ; ::_thesis: verum end; hence (S *') *' = S by FUNCT_2:63; ::_thesis: verum end; theorem :: OPPCAT_1:51 for D being Category for C being strict Category for S being Function of the carrier' of C, the carrier' of D holds *' (*' S) = S proof let D be Category; ::_thesis: for C being strict Category for S being Function of the carrier' of C, the carrier' of D holds *' (*' S) = S let C be strict Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of D holds *' (*' S) = S let S be Function of the carrier' of C, the carrier' of D; ::_thesis: *' (*' S) = S now__::_thesis:_(_(C_opp)_opp_=_C_&_(_for_f_being_Morphism_of_((C_opp)_opp)_holds_(*'_(*'_S))_._f_=_S_._f_)_) thus (C opp) opp = C by FUNCT_4:53; ::_thesis: for f being Morphism of ((C opp) opp) holds (*' (*' S)) . f = S . f let f be Morphism of ((C opp) opp); ::_thesis: (*' (*' S)) . f = S . f thus (*' (*' S)) . f = (*' S) . (opp f) by Def10 .= S . (opp (opp f)) by Def10 .= S . f ; ::_thesis: verum end; hence *' (*' S) = S by FUNCT_2:63; ::_thesis: verum end; Lm18: for C, B, D being Category for S being Function of the carrier' of (C opp), the carrier' of B for T being Function of the carrier' of B, the carrier' of D holds /* (T * S) = T * (/* S) proof let C, B, D be Category; ::_thesis: for S being Function of the carrier' of (C opp), the carrier' of B for T being Function of the carrier' of B, the carrier' of D holds /* (T * S) = T * (/* S) let S be Function of the carrier' of (C opp), the carrier' of B; ::_thesis: for T being Function of the carrier' of B, the carrier' of D holds /* (T * S) = T * (/* S) let T be Function of the carrier' of B, the carrier' of D; ::_thesis: /* (T * S) = T * (/* S) now__::_thesis:_for_f_being_Morphism_of_C_holds_(/*_(T_*_S))_._f_=_(T_*_(/*_S))_._f let f be Morphism of C; ::_thesis: (/* (T * S)) . f = (T * (/* S)) . f thus (/* (T * S)) . f = (T * S) . (f opp) by Def8 .= T . (S . (f opp)) by FUNCT_2:15 .= T . ((/* S) . f) by Def8 .= (T * (/* S)) . f by FUNCT_2:15 ; ::_thesis: verum end; hence /* (T * S) = T * (/* S) by FUNCT_2:63; ::_thesis: verum end; theorem :: OPPCAT_1:52 for C, B, D being Category for S being Function of the carrier' of C, the carrier' of B for T being Function of the carrier' of B, the carrier' of D holds *' (T * S) = T * (*' S) proof let C, B, D be Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of B for T being Function of the carrier' of B, the carrier' of D holds *' (T * S) = T * (*' S) let S be Function of the carrier' of C, the carrier' of B; ::_thesis: for T being Function of the carrier' of B, the carrier' of D holds *' (T * S) = T * (*' S) let T be Function of the carrier' of B, the carrier' of D; ::_thesis: *' (T * S) = T * (*' S) now__::_thesis:_for_f_being_Morphism_of_(C_opp)_holds_(*'_(T_*_S))_._f_=_(T_*_(*'_S))_._f let f be Morphism of (C opp); ::_thesis: (*' (T * S)) . f = (T * (*' S)) . f thus (*' (T * S)) . f = (T * S) . (opp f) by Def10 .= T . (S . (opp f)) by FUNCT_2:15 .= T . ((*' S) . f) by Def10 .= (T * (*' S)) . f by FUNCT_2:15 ; ::_thesis: verum end; hence *' (T * S) = T * (*' S) by FUNCT_2:63; ::_thesis: verum end; theorem :: OPPCAT_1:53 for C, B, D being Category for S being Function of the carrier' of C, the carrier' of B for T being Function of the carrier' of B, the carrier' of D holds (T * S) *' = (T *') * S proof let C, B, D be Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of B for T being Function of the carrier' of B, the carrier' of D holds (T * S) *' = (T *') * S let S be Function of the carrier' of C, the carrier' of B; ::_thesis: for T being Function of the carrier' of B, the carrier' of D holds (T * S) *' = (T *') * S let T be Function of the carrier' of B, the carrier' of D; ::_thesis: (T * S) *' = (T *') * S now__::_thesis:_for_f_being_Morphism_of_C_holds_((T_*_S)_*')_._f_=_((T_*')_*_S)_._f let f be Morphism of C; ::_thesis: ((T * S) *') . f = ((T *') * S) . f thus ((T * S) *') . f = ((T * S) . f) opp by Def11 .= (T . (S . f)) opp by FUNCT_2:15 .= (T *') . (S . f) by Def11 .= ((T *') * S) . f by FUNCT_2:15 ; ::_thesis: verum end; hence (T * S) *' = (T *') * S by FUNCT_2:63; ::_thesis: verum end; theorem :: OPPCAT_1:54 for C, B, D being Category for F1 being Function of the carrier' of C, the carrier' of B for F2 being Function of the carrier' of B, the carrier' of D holds (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *') proof let C, B, D be Category; ::_thesis: for F1 being Function of the carrier' of C, the carrier' of B for F2 being Function of the carrier' of B, the carrier' of D holds (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *') let F1 be Function of the carrier' of C, the carrier' of B; ::_thesis: for F2 being Function of the carrier' of B, the carrier' of D holds (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *') let F2 be Function of the carrier' of B, the carrier' of D; ::_thesis: (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *') now__::_thesis:_for_f_being_Morphism_of_(C_opp)_holds_((*'_(F2_*_F1))_*')_._f_=_(((*'_F2)_*')_*_((*'_F1)_*'))_._f let f be Morphism of (C opp); ::_thesis: ((*' (F2 * F1)) *') . f = (((*' F2) *') * ((*' F1) *')) . f thus ((*' (F2 * F1)) *') . f = ((F2 * F1) . (opp f)) opp by Lm17 .= (F2 . (F1 . (opp f))) opp by FUNCT_2:15 .= ((*' F2) *') . ((F1 . (opp f)) opp) by Th46 .= ((*' F2) *') . (((*' F1) *') . f) by Lm17 .= (((*' F2) *') * ((*' F1) *')) . f by FUNCT_2:15 ; ::_thesis: verum end; hence (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *') by FUNCT_2:63; ::_thesis: verum end; Lm19: for C, B being Category for S being Contravariant_Functor of C,B for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c) proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c) let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c) let c be Object of (C opp); ::_thesis: (*' S) . (id c) = id ((Obj (*' S)) . c) thus (*' S) . (id c) = S . (opp (id c)) by Def10 .= S . (id (opp c)) by Th21 .= id ((Obj S) . (opp c)) by Th31 .= id ((Obj (*' S)) . c) by Th43 ; ::_thesis: verum end; Lm20: for C, B being Category for S being Contravariant_Functor of C,B for f being Morphism of (C opp) holds ( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) ) proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B for f being Morphism of (C opp) holds ( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) ) let S be Contravariant_Functor of C,B; ::_thesis: for f being Morphism of (C opp) holds ( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) ) let f be Morphism of (C opp); ::_thesis: ( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) ) A1: (Obj (*' S)) . (cod f) = (Obj S) . (opp (cod f)) by Th43 .= (Obj S) . (dom (opp f)) .= cod (S . (opp f)) by Th32 ; (Obj (*' S)) . (dom f) = (Obj S) . (opp (dom f)) by Th43 .= (Obj S) . (cod (opp f)) .= dom (S . (opp f)) by Th32 ; hence ( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) ) by A1, Def10; ::_thesis: verum end; theorem Th55: :: OPPCAT_1:55 for C, D being Category for S being Contravariant_Functor of C,D holds *' S is Functor of C opp ,D proof let C, D be Category; ::_thesis: for S being Contravariant_Functor of C,D holds *' S is Functor of C opp ,D let S be Contravariant_Functor of C,D; ::_thesis: *' S is Functor of C opp ,D now__::_thesis:_(_(_for_c_being_Object_of_(C_opp)_ex_d_being_Object_of_D_st_(*'_S)_._(id_c)_=_id_d_)_&_(_for_f_being_Morphism_of_(C_opp)_holds_ (_(*'_S)_._(id_(dom_f))_=_id_(dom_((*'_S)_._f))_&_(*'_S)_._(id_(cod_f))_=_id_(cod_((*'_S)_._f))_)_)_&_(_for_f,_g_being_Morphism_of_(C_opp)_st_dom_g_=_cod_f_holds_ (*'_S)_._(g_(*)_f)_=_((*'_S)_._g)_(*)_((*'_S)_._f)_)_) thus for c being Object of (C opp) ex d being Object of D st (*' S) . (id c) = id d ::_thesis: ( ( for f being Morphism of (C opp) holds ( (*' S) . (id (dom f)) = id (dom ((*' S) . f)) & (*' S) . (id (cod f)) = id (cod ((*' S) . f)) ) ) & ( for f, g being Morphism of (C opp) st dom g = cod f holds (*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . f) ) ) proof let c be Object of (C opp); ::_thesis: ex d being Object of D st (*' S) . (id c) = id d (*' S) . (id c) = id ((Obj (*' S)) . c) by Lm19; hence ex d being Object of D st (*' S) . (id c) = id d ; ::_thesis: verum end; thus for f being Morphism of (C opp) holds ( (*' S) . (id (dom f)) = id (dom ((*' S) . f)) & (*' S) . (id (cod f)) = id (cod ((*' S) . f)) ) ::_thesis: for f, g being Morphism of (C opp) st dom g = cod f holds (*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . f) proof let f be Morphism of (C opp); ::_thesis: ( (*' S) . (id (dom f)) = id (dom ((*' S) . f)) & (*' S) . (id (cod f)) = id (cod ((*' S) . f)) ) thus (*' S) . (id (dom f)) = id ((Obj (*' S)) . (dom f)) by Lm19 .= id (dom ((*' S) . f)) by Lm20 ; ::_thesis: (*' S) . (id (cod f)) = id (cod ((*' S) . f)) thus (*' S) . (id (cod f)) = id ((Obj (*' S)) . (cod f)) by Lm19 .= id (cod ((*' S) . f)) by Lm20 ; ::_thesis: verum end; let f, g be Morphism of (C opp); ::_thesis: ( dom g = cod f implies (*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . f) ) assume A1: dom g = cod f ; ::_thesis: (*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . f) A2: ( dom (opp f) = cod f & cod (opp g) = dom g ) ; thus (*' S) . (g (*) f) = S . (opp (g (*) f)) by Def10 .= S . ((opp f) (*) (opp g)) by A1, Th18 .= (S . (opp g)) (*) (S . (opp f)) by A1, A2, Def9 .= ((*' S) . g) (*) (S . (opp f)) by Def10 .= ((*' S) . g) (*) ((*' S) . f) by Def10 ; ::_thesis: verum end; hence *' S is Functor of C opp ,D by CAT_1:61; ::_thesis: verum end; Lm21: for C, B being Category for S being Contravariant_Functor of C,B for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c) proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c) let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c) let c be Object of C; ::_thesis: (S *') . (id c) = id ((Obj (S *')) . c) A1: Hom (((Obj S) . c),((Obj S) . c)) <> {} ; thus (S *') . (id c) = (S . (id c)) opp by Def11 .= (id ((Obj S) . c)) opp by Th31 .= (id ((Obj S) . c)) opp by Def6, A1 .= id (((Obj S) . c) opp) by Th20 .= id ((Obj (S *')) . c) by Th45 ; ::_thesis: verum end; Lm22: for C, B being Category for S being Contravariant_Functor of C,B for f being Morphism of C holds ( (Obj (S *')) . (dom f) = dom ((S *') . f) & (Obj (S *')) . (cod f) = cod ((S *') . f) ) proof let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B for f being Morphism of C holds ( (Obj (S *')) . (dom f) = dom ((S *') . f) & (Obj (S *')) . (cod f) = cod ((S *') . f) ) let S be Contravariant_Functor of C,B; ::_thesis: for f being Morphism of C holds ( (Obj (S *')) . (dom f) = dom ((S *') . f) & (Obj (S *')) . (cod f) = cod ((S *') . f) ) let f be Morphism of C; ::_thesis: ( (Obj (S *')) . (dom f) = dom ((S *') . f) & (Obj (S *')) . (cod f) = cod ((S *') . f) ) A1: (Obj (S *')) . (cod f) = ((Obj S) . (cod f)) opp by Th45 .= (dom (S . f)) opp by Th32 .= cod ((S . f) opp) ; (Obj (S *')) . (dom f) = ((Obj S) . (dom f)) opp by Th45 .= (cod (S . f)) opp by Th32 .= dom ((S . f) opp) ; hence ( (Obj (S *')) . (dom f) = dom ((S *') . f) & (Obj (S *')) . (cod f) = cod ((S *') . f) ) by A1, Def11; ::_thesis: verum end; theorem Th56: :: OPPCAT_1:56 for C, D being Category for S being Contravariant_Functor of C,D holds S *' is Functor of C,D opp proof let C, D be Category; ::_thesis: for S being Contravariant_Functor of C,D holds S *' is Functor of C,D opp let S be Contravariant_Functor of C,D; ::_thesis: S *' is Functor of C,D opp now__::_thesis:_(_(_for_c_being_Object_of_C_ex_d_being_Object_of_(D_opp)_st_(S_*')_._(id_c)_=_id_d_)_&_(_for_f_being_Morphism_of_C_holds_ (_(S_*')_._(id_(dom_f))_=_id_(dom_((S_*')_._f))_&_(S_*')_._(id_(cod_f))_=_id_(cod_((S_*')_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_ (S_*')_._(g_(*)_f)_=_((S_*')_._g)_(*)_((S_*')_._f)_)_) thus for c being Object of C ex d being Object of (D opp) st (S *') . (id c) = id d ::_thesis: ( ( for f being Morphism of C holds ( (S *') . (id (dom f)) = id (dom ((S *') . f)) & (S *') . (id (cod f)) = id (cod ((S *') . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds (S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f) ) ) proof let c be Object of C; ::_thesis: ex d being Object of (D opp) st (S *') . (id c) = id d (S *') . (id c) = id (((Obj S) . c) opp) by Lm16; hence ex d being Object of (D opp) st (S *') . (id c) = id d ; ::_thesis: verum end; thus for f being Morphism of C holds ( (S *') . (id (dom f)) = id (dom ((S *') . f)) & (S *') . (id (cod f)) = id (cod ((S *') . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds (S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f) proof let f be Morphism of C; ::_thesis: ( (S *') . (id (dom f)) = id (dom ((S *') . f)) & (S *') . (id (cod f)) = id (cod ((S *') . f)) ) thus (S *') . (id (dom f)) = id ((Obj (S *')) . (dom f)) by Lm21 .= id (dom ((S *') . f)) by Lm22 ; ::_thesis: (S *') . (id (cod f)) = id (cod ((S *') . f)) thus (S *') . (id (cod f)) = id ((Obj (S *')) . (cod f)) by Lm21 .= id (cod ((S *') . f)) by Lm22 ; ::_thesis: verum end; let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f) ) assume A1: dom g = cod f ; ::_thesis: (S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f) then A2: dom (S . f) = cod (S . g) by Th33; reconsider Sff = S . f as Morphism of dom (S . f), cod (S . f) by CAT_1:4; reconsider Sgg = S . g as Morphism of dom (S . g), cod (S . g) by CAT_1:4; A3: ( Hom ((dom (S . f)),(cod (S . f))) <> {} & Hom ((dom (S . g)),(cod (S . g))) <> {} ) by CAT_1:2; then A4: Sff opp = (S . f) opp by Def6; A5: Sgg opp = (S . g) opp by A3, Def6; thus (S *') . (g (*) f) = (S . (g (*) f)) opp by Def11 .= (Sff (*) Sgg) opp by A1, Def9 .= (Sgg opp) (*) (Sff opp) by A3, A2, Th16 .= ((S *') . g) (*) ((S . f) opp) by Def11, A4, A5 .= ((S *') . g) (*) ((S *') . f) by Def11 ; ::_thesis: verum end; hence S *' is Functor of C,D opp by CAT_1:61; ::_thesis: verum end; Lm23: for C, B being Category for S being Functor of C,B for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c) proof let C, B be Category; ::_thesis: for S being Functor of C,B for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c) let S be Functor of C,B; ::_thesis: for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c) let c be Object of (C opp); ::_thesis: (*' S) . (id c) = id ((Obj (*' S)) . c) thus (*' S) . (id c) = S . (opp (id c)) by Def10 .= S . (id (opp c)) by Th21 .= id ((Obj S) . (opp c)) by CAT_1:68 .= id ((Obj (*' S)) . c) by Th40 ; ::_thesis: verum end; Lm24: for C, B being Category for S being Functor of C,B for f being Morphism of (C opp) holds ( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) ) proof let C, B be Category; ::_thesis: for S being Functor of C,B for f being Morphism of (C opp) holds ( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) ) let S be Functor of C,B; ::_thesis: for f being Morphism of (C opp) holds ( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) ) let f be Morphism of (C opp); ::_thesis: ( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) ) A1: (Obj (*' S)) . (cod f) = (Obj S) . (opp (cod f)) by Th40 .= (Obj S) . (dom (opp f)) .= dom (S . (opp f)) by CAT_1:69 ; (Obj (*' S)) . (dom f) = (Obj S) . (opp (dom f)) by Th40 .= (Obj S) . (cod (opp f)) .= cod (S . (opp f)) by CAT_1:69 ; hence ( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) ) by A1, Def10; ::_thesis: verum end; theorem Th57: :: OPPCAT_1:57 for C, D being Category for S being Functor of C,D holds *' S is Contravariant_Functor of C opp ,D proof let C, D be Category; ::_thesis: for S being Functor of C,D holds *' S is Contravariant_Functor of C opp ,D let S be Functor of C,D; ::_thesis: *' S is Contravariant_Functor of C opp ,D thus for c being Object of (C opp) ex d being Object of D st (*' S) . (id c) = id d :: according to OPPCAT_1:def_9 ::_thesis: ( ( for f being Morphism of (C opp) holds ( (*' S) . (id (dom f)) = id (cod ((*' S) . f)) & (*' S) . (id (cod f)) = id (dom ((*' S) . f)) ) ) & ( for f, g being Morphism of (C opp) st dom g = cod f holds (*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g) ) ) proof let c be Object of (C opp); ::_thesis: ex d being Object of D st (*' S) . (id c) = id d (*' S) . (id c) = id ((Obj (*' S)) . c) by Lm23; hence ex d being Object of D st (*' S) . (id c) = id d ; ::_thesis: verum end; thus for f being Morphism of (C opp) holds ( (*' S) . (id (dom f)) = id (cod ((*' S) . f)) & (*' S) . (id (cod f)) = id (dom ((*' S) . f)) ) ::_thesis: for f, g being Morphism of (C opp) st dom g = cod f holds (*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g) proof let f be Morphism of (C opp); ::_thesis: ( (*' S) . (id (dom f)) = id (cod ((*' S) . f)) & (*' S) . (id (cod f)) = id (dom ((*' S) . f)) ) thus (*' S) . (id (dom f)) = id ((Obj (*' S)) . (dom f)) by Lm23 .= id (cod ((*' S) . f)) by Lm24 ; ::_thesis: (*' S) . (id (cod f)) = id (dom ((*' S) . f)) thus (*' S) . (id (cod f)) = id ((Obj (*' S)) . (cod f)) by Lm23 .= id (dom ((*' S) . f)) by Lm24 ; ::_thesis: verum end; let f, g be Morphism of (C opp); ::_thesis: ( dom g = cod f implies (*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g) ) assume A1: dom g = cod f ; ::_thesis: (*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g) A2: ( dom (opp f) = cod f & cod (opp g) = dom g ) ; thus (*' S) . (g (*) f) = S . (opp (g (*) f)) by Def10 .= S . ((opp f) (*) (opp g)) by A1, Th18 .= (S . (opp f)) (*) (S . (opp g)) by A1, A2, CAT_1:64 .= ((*' S) . f) (*) (S . (opp g)) by Def10 .= ((*' S) . f) (*) ((*' S) . g) by Def10 ; ::_thesis: verum end; Lm25: for C, B being Category for S being Functor of C,B for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c) proof let C, B be Category; ::_thesis: for S being Functor of C,B for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c) let S be Functor of C,B; ::_thesis: for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c) let c be Object of C; ::_thesis: (S *') . (id c) = id ((Obj (S *')) . c) A1: Hom (((Obj S) . c),((Obj S) . c)) <> {} ; thus (S *') . (id c) = (S . (id c)) opp by Def11 .= (id ((Obj S) . c)) opp by CAT_1:68 .= (id ((Obj S) . c)) opp by Def6, A1 .= id (((Obj S) . c) opp) by Th20 .= id ((Obj (S *')) . c) by Th42 ; ::_thesis: verum end; Lm26: for C, B being Category for S being Functor of C,B for f being Morphism of C holds ( (Obj (S *')) . (dom f) = cod ((S *') . f) & (Obj (S *')) . (cod f) = dom ((S *') . f) ) proof let C, B be Category; ::_thesis: for S being Functor of C,B for f being Morphism of C holds ( (Obj (S *')) . (dom f) = cod ((S *') . f) & (Obj (S *')) . (cod f) = dom ((S *') . f) ) let S be Functor of C,B; ::_thesis: for f being Morphism of C holds ( (Obj (S *')) . (dom f) = cod ((S *') . f) & (Obj (S *')) . (cod f) = dom ((S *') . f) ) let f be Morphism of C; ::_thesis: ( (Obj (S *')) . (dom f) = cod ((S *') . f) & (Obj (S *')) . (cod f) = dom ((S *') . f) ) A1: (Obj (S *')) . (cod f) = ((Obj S) . (cod f)) opp by Th42 .= (cod (S . f)) opp by CAT_1:69 .= dom ((S . f) opp) ; (Obj (S *')) . (dom f) = ((Obj S) . (dom f)) opp by Th42 .= (dom (S . f)) opp by CAT_1:69 .= cod ((S . f) opp) ; hence ( (Obj (S *')) . (dom f) = cod ((S *') . f) & (Obj (S *')) . (cod f) = dom ((S *') . f) ) by A1, Def11; ::_thesis: verum end; theorem Th58: :: OPPCAT_1:58 for C, D being Category for S being Functor of C,D holds S *' is Contravariant_Functor of C,D opp proof let C, D be Category; ::_thesis: for S being Functor of C,D holds S *' is Contravariant_Functor of C,D opp let S be Functor of C,D; ::_thesis: S *' is Contravariant_Functor of C,D opp thus for c being Object of C ex d being Object of (D opp) st (S *') . (id c) = id d :: according to OPPCAT_1:def_9 ::_thesis: ( ( for f being Morphism of C holds ( (S *') . (id (dom f)) = id (cod ((S *') . f)) & (S *') . (id (cod f)) = id (dom ((S *') . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds (S *') . (g (*) f) = ((S *') . f) (*) ((S *') . g) ) ) proof let c be Object of C; ::_thesis: ex d being Object of (D opp) st (S *') . (id c) = id d (S *') . (id c) = id ((Obj (S *')) . c) by Lm25; hence ex d being Object of (D opp) st (S *') . (id c) = id d ; ::_thesis: verum end; thus for f being Morphism of C holds ( (S *') . (id (dom f)) = id (cod ((S *') . f)) & (S *') . (id (cod f)) = id (dom ((S *') . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds (S *') . (g (*) f) = ((S *') . f) (*) ((S *') . g) proof let f be Morphism of C; ::_thesis: ( (S *') . (id (dom f)) = id (cod ((S *') . f)) & (S *') . (id (cod f)) = id (dom ((S *') . f)) ) thus (S *') . (id (dom f)) = id ((Obj (S *')) . (dom f)) by Lm25 .= id (cod ((S *') . f)) by Lm26 ; ::_thesis: (S *') . (id (cod f)) = id (dom ((S *') . f)) thus (S *') . (id (cod f)) = id ((Obj (S *')) . (cod f)) by Lm25 .= id (dom ((S *') . f)) by Lm26 ; ::_thesis: verum end; let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (S *') . (g (*) f) = ((S *') . f) (*) ((S *') . g) ) assume A1: dom g = cod f ; ::_thesis: (S *') . (g (*) f) = ((S *') . f) (*) ((S *') . g) then A2: dom (S . g) = cod (S . f) by CAT_1:64; reconsider Sff = S . f as Morphism of dom (S . f), cod (S . f) by CAT_1:4; reconsider Sgg = S . g as Morphism of dom (S . g), cod (S . g) by CAT_1:4; A3: ( Hom ((dom (S . f)),(cod (S . f))) <> {} & Hom ((dom (S . g)),(cod (S . g))) <> {} ) by CAT_1:2; then A4: Sff opp = (S . f) opp by Def6; A5: Sgg opp = (S . g) opp by Def6, A3; thus (S *') . (g (*) f) = (S . (g (*) f)) opp by Def11 .= (Sgg (*) Sff) opp by A1, CAT_1:64 .= (Sff opp) (*) (Sgg opp) by A2, Th16, A3 .= ((S *') . f) (*) ((S . g) opp) by Def11, A4, A5 .= ((S *') . f) (*) ((S *') . g) by Def11 ; ::_thesis: verum end; theorem :: OPPCAT_1:59 for C, B, D being Category for S1 being Contravariant_Functor of C,B for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D proof let C, B, D be Category; ::_thesis: for S1 being Contravariant_Functor of C,B for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D let S1 be Contravariant_Functor of C,B; ::_thesis: for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D let S2 be Functor of B,D; ::_thesis: S2 * S1 is Contravariant_Functor of C,D *' S1 is Functor of C opp ,B by Th55; then S2 * (*' S1) is Functor of C opp ,D by CAT_1:73; then /* (S2 * (*' S1)) is Contravariant_Functor of C,D by Th34; then S2 * (/* (*' S1)) is Contravariant_Functor of C,D by Lm18; hence S2 * S1 is Contravariant_Functor of C,D by Th47; ::_thesis: verum end; theorem :: OPPCAT_1:60 for C, B, D being Category for S1 being Functor of C,B for S2 being Contravariant_Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D proof let C, B, D be Category; ::_thesis: for S1 being Functor of C,B for S2 being Contravariant_Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D let S1 be Functor of C,B; ::_thesis: for S2 being Contravariant_Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D let S2 be Contravariant_Functor of B,D; ::_thesis: S2 * S1 is Contravariant_Functor of C,D *' S1 is Contravariant_Functor of C opp ,B by Th57; then S2 * (*' S1) is Functor of C opp ,D by Th35; then /* (S2 * (*' S1)) is Contravariant_Functor of C,D by Th34; then S2 * (/* (*' S1)) is Contravariant_Functor of C,D by Lm18; hence S2 * S1 is Contravariant_Functor of C,D by Th47; ::_thesis: verum end; theorem :: OPPCAT_1:61 for C, D being Category for F being Functor of C,D for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp proof let C, D be Category; ::_thesis: for F being Functor of C,D for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp let F be Functor of C,D; ::_thesis: for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp let c be Object of C; ::_thesis: (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp *' F is Contravariant_Functor of C opp ,D by Th57; hence (Obj ((*' F) *')) . (c opp) = ((Obj (*' F)) . (c opp)) opp by Th45 .= ((Obj F) . (opp (c opp))) opp by Th40 .= ((Obj F) . c) opp ; ::_thesis: verum end; theorem :: OPPCAT_1:62 for C, D being Category for F being Contravariant_Functor of C,D for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp proof let C, D be Category; ::_thesis: for F being Contravariant_Functor of C,D for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp let F be Contravariant_Functor of C,D; ::_thesis: for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp let c be Object of C; ::_thesis: (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp *' F is Functor of C opp ,D by Th55; hence (Obj ((*' F) *')) . (c opp) = ((Obj (*' F)) . (c opp)) opp by Th42 .= ((Obj F) . (opp (c opp))) opp by Th43 .= ((Obj F) . c) opp ; ::_thesis: verum end; theorem :: OPPCAT_1:63 for C, D being Category for F being Functor of C,D holds (*' F) *' is Functor of C opp ,D opp proof let C, D be Category; ::_thesis: for F being Functor of C,D holds (*' F) *' is Functor of C opp ,D opp let F be Functor of C,D; ::_thesis: (*' F) *' is Functor of C opp ,D opp *' F is Contravariant_Functor of C opp ,D by Th57; hence (*' F) *' is Functor of C opp ,D opp by Th56; ::_thesis: verum end; theorem :: OPPCAT_1:64 for C, D being Category for F being Contravariant_Functor of C,D holds (*' F) *' is Contravariant_Functor of C opp ,D opp proof let C, D be Category; ::_thesis: for F being Contravariant_Functor of C,D holds (*' F) *' is Contravariant_Functor of C opp ,D opp let F be Contravariant_Functor of C,D; ::_thesis: (*' F) *' is Contravariant_Functor of C opp ,D opp *' F is Functor of C opp ,D by Th55; hence (*' F) *' is Contravariant_Functor of C opp ,D opp by Th58; ::_thesis: verum end; definition let C be Category; func id* C -> Contravariant_Functor of C,C opp equals :: OPPCAT_1:def 12 (id C) *' ; coherence (id C) *' is Contravariant_Functor of C,C opp by Th58; func *id C -> Contravariant_Functor of C opp ,C equals :: OPPCAT_1:def 13 *' (id C); coherence *' (id C) is Contravariant_Functor of C opp ,C by Th57; end; :: deftheorem defines id* OPPCAT_1:def_12_:_ for C being Category holds id* C = (id C) *' ; :: deftheorem defines *id OPPCAT_1:def_13_:_ for C being Category holds *id C = *' (id C); theorem Th65: :: OPPCAT_1:65 for C being Category for f being Morphism of C holds (id* C) . f = f opp proof let C be Category; ::_thesis: for f being Morphism of C holds (id* C) . f = f opp let f be Morphism of C; ::_thesis: (id* C) . f = f opp thus (id* C) . f = ((id C) . f) opp by Def11 .= f opp by FUNCT_1:18 ; ::_thesis: verum end; theorem :: OPPCAT_1:66 for C being Category for c being Object of C holds (Obj (id* C)) . c = c opp proof let C be Category; ::_thesis: for c being Object of C holds (Obj (id* C)) . c = c opp let c be Object of C; ::_thesis: (Obj (id* C)) . c = c opp thus (Obj (id* C)) . c = ((Obj (id C)) . c) opp by Th42 .= c opp by CAT_1:77 ; ::_thesis: verum end; theorem Th67: :: OPPCAT_1:67 for C being Category for f being Morphism of (C opp) holds (*id C) . f = opp f proof let C be Category; ::_thesis: for f being Morphism of (C opp) holds (*id C) . f = opp f let f be Morphism of (C opp); ::_thesis: (*id C) . f = opp f thus (*id C) . f = (id C) . (opp f) by Def10 .= opp f by FUNCT_1:18 ; ::_thesis: verum end; theorem :: OPPCAT_1:68 for C being Category for c being Object of (C opp) holds (Obj (*id C)) . c = opp c proof let C be Category; ::_thesis: for c being Object of (C opp) holds (Obj (*id C)) . c = opp c let c be Object of (C opp); ::_thesis: (Obj (*id C)) . c = opp c thus (Obj (*id C)) . c = (Obj (id C)) . (opp c) by Th40 .= opp c by CAT_1:77 ; ::_thesis: verum end; theorem :: OPPCAT_1:69 for C, D being Category for S being Function of the carrier' of C, the carrier' of D holds ( *' S = S * (*id C) & S *' = (id* D) * S ) proof let C, D be Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of D holds ( *' S = S * (*id C) & S *' = (id* D) * S ) let S be Function of the carrier' of C, the carrier' of D; ::_thesis: ( *' S = S * (*id C) & S *' = (id* D) * S ) now__::_thesis:_for_f_being_Morphism_of_(C_opp)_holds_(*'_S)_._f_=_(S_*_(*id_C))_._f let f be Morphism of (C opp); ::_thesis: (*' S) . f = (S * (*id C)) . f thus (*' S) . f = S . (opp f) by Def10 .= S . ((*id C) . f) by Th67 .= (S * (*id C)) . f by FUNCT_2:15 ; ::_thesis: verum end; hence *' S = S * (*id C) by FUNCT_2:63; ::_thesis: S *' = (id* D) * S now__::_thesis:_for_f_being_Morphism_of_C_holds_(S_*')_._f_=_((id*_D)_*_S)_._f let f be Morphism of C; ::_thesis: (S *') . f = ((id* D) * S) . f thus (S *') . f = (S . f) opp by Def11 .= (id* D) . (S . f) by Th65 .= ((id* D) * S) . f by FUNCT_2:15 ; ::_thesis: verum end; hence S *' = (id* D) * S by FUNCT_2:63; ::_thesis: verum end; theorem :: OPPCAT_1:70 for C being Category for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds for f being Morphism of a,b for g being Morphism of b,c holds g * f = (f opp) * (g opp) by Lm3; theorem Th71: :: OPPCAT_1:71 for C being Category for a being Object of C holds id a = id (a opp) by Lm2; theorem :: OPPCAT_1:72 for C being Category for a being Object of (C opp) holds id a = id (opp a) proof let C be Category; ::_thesis: for a being Object of (C opp) holds id a = id (opp a) let a be Object of (C opp); ::_thesis: id a = id (opp a) thus id a = id ((opp a) opp) .= id (opp a) by Th71 ; ::_thesis: verum end;