:: Opposite Categories and Contravariant Functors :: by Czes\l aw Byli\'nski :: :: Received February 13, 1991 :: Copyright (c) 1991-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies CAT_1, XBOOLE_0, PARTFUN1, ZFMISC_1, RELAT_1, STRUCT_0, GRAPH_1, SUBSET_1, FUNCT_1, ARYTM_0, ALGSTR_0, FUNCT_2, ARYTM_3, OPPCAT_1, TARSKI, MONOID_0, RELAT_2, BINOP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, PARTFUN1, FUNCT_4, STRUCT_0, GRAPH_1, CAT_1; constructors PARTFUN1, BINOP_1, FUNCT_4, CAT_1, RELSET_1; registrations XBOOLE_0, RELSET_1, FUNCT_2, CAT_1, STRUCT_0; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0, CAT_1; equalities CAT_1, BINOP_1, GRAPH_1; expansions CAT_1; theorems FUNCT_2, FUNCT_4, PARTFUN1, CAT_1, SUBSET_1, FUNCT_1; schemes FUNCT_2; begin reserve B,C,D for Category; :: Opposite Category definition let C; func C opp -> strict non empty non void CatStr equals CatStr (#the carrier of C, the carrier' of C, the Target of C, the Source of C, ~the Comp of C#); coherence; end; definition let C; let c be Object of C; func c opp -> Object of C opp equals c; coherence; end; registration let C; cluster C opp -> Category-like transitive associative reflexive with_identities; coherence proof set M = the carrier' of C, d = the Target of C, c = the Source of C, p = ~( the Comp of C); set B = C opp; thus A1: B is Category-like proof let f,g be Morphism of B; reconsider ff=f, gg=g as Morphism of C; thus [g,f] in dom(the Comp of B) implies dom g=cod f proof assume [g,f] in dom(the Comp of B); 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; end; assume A2: dom g=cod f; 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 B) by FUNCT_4:42; end; A3: for f,g being Element of M st d.g = c.f holds p.(g,f) = (the Comp of C).(f,g) proof let f,g be Element of M; reconsider ff=f, gg=g as Morphism of B; assume d.g = c.f; then dom gg = cod ff; then [gg,ff] in dom(p) by A1; hence thesis by FUNCT_4:43; end; thus A4: B is transitive proof let ff,gg be Morphism of B; reconsider f=ff, g=gg as Morphism of C; assume A5: dom gg=cod ff; 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 B by A5,A1; then A8: gg(*)ff = p.(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; thus cod(gg(*)ff) = dom(f(*)g) by A8 .= dom g by A6,CAT_1:def 7 .= cod gg; end; thus B is associative proof let ff,gg,hh be Morphism of B; reconsider f=ff, g=gg, h=hh as Morphism of C; assume that A9: dom hh = cod gg and A10: dom gg = cod ff; A11: [h,g] in dom p by A1,A9; then A12: p.(h,g) is Element of M by PARTFUN1:4; A13: [g,f] in dom p by A1,A10; then A14: p.(g,f) is Element of M by PARTFUN1:4; A15: p.(h,g) = (the Comp of C).(g,h) by A3,A9; d.(p.(h,g)) = dom(hh(*)gg) by A11,CAT_1:def 1 .= dom gg by A4,A9; then A16: p.(p.(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: p.(g,f) = (the Comp of C).(f,g) by A3,A10; A19: c.(p.(g,f)) = cod(gg(*)ff) by A13,CAT_1:def 1 .= cod gg by A4,A10; dom(hh(*)gg) = dom gg by A4,A9; then A20: [hh(*)gg,ff] in dom the Comp of B by A1,A10; cod(gg(*)ff) = cod gg by A4,A10; then A21: [hh,gg(*)ff] in dom the Comp of B by A1,A9; [hh,gg] in dom the Comp of B by A9,A1; then A22: hh(*)gg = p.(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 B by A10,A1; then gg(*)ff = p.(g,f) by CAT_1:def 1; hence hh(*)(gg(*)ff) = p.(h,p.(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 .= p.(p.(h,g),f) by A16,A17,A25,A26,CAT_1:16 .= (hh(*)gg)(*)ff by A20,A22,CAT_1:def 1; end; thus B is reflexive proof let bb be Object of B; 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 B; 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)<>{}; end; let a be Element of B; reconsider aa=a as Element of C; reconsider ii = id aa as Morphism of B; A29: dom ii = cod id aa .= aa; A30: cod ii = dom id aa .= aa; then reconsider ii as Morphism of a,a by A29,CAT_1:4; take ii; let b be Element of B; reconsider bb = b as Element of C; thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g proof assume A31: Hom(a,b)<>{}; let g being Morphism of a,b; 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 as Morphism of bb,aa by A32,A33,CAT_1:4; A35: c.ii = aa by A30 .= dom g by A31,CAT_1:5 .= d.g; then dom g = cod ii; then [g,ii] in dom the Comp of B by A1; hence g(*)ii = p.(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; end; assume A36: Hom(b,a)<>{}; let g being Morphism of b,a; 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 as Morphism of aa,bb by A37,A38,CAT_1:4; A40: d.ii = aa by A29 .= cod g by A36,CAT_1:5 .= c.g; then cod g = dom ii; then [ii,g] in dom the Comp of B by A1; hence ii(*)g = p.(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; end; end; definition let C; let c be Object of C opp; func opp c -> Object of C equals c opp; coherence; end; ::\$CT theorem for c being Object of C holds c opp opp = c; theorem for c being Object of C holds opp (c opp) = c; theorem for c being Object of C opp holds (opp c) opp = c; theorem Th4: for a,b being Object of C holds Hom(a,b) = Hom(b opp,a opp) proof let a,b be Object of C; thus Hom(a,b) c= Hom(b opp,a opp) proof let x be object; assume A1: x in Hom(a,b); 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); end; let x be object; assume A2: x in Hom(b opp,a opp); 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); end; theorem Th5: for a,b being Object of C opp holds Hom(a,b) = Hom(opp b,opp a) proof let a,b be Object of C opp; thus Hom(a,b) = Hom((opp a)opp,(opp b) opp) .= Hom(opp b,opp a) by Th4; end; definition let C; let f be Morphism of C; func f opp -> Morphism of C opp equals f; coherence; end; definition let C; let f be Morphism of C opp; func opp f -> Morphism of C equals f opp; coherence; end; definition let C; let a,b be Object of C such that A1: Hom(a,b) <> {}; let f be Morphism of a,b; func f opp -> Morphism of b opp, a opp equals :Def6: f; coherence proof f in Hom(a,b) by A1,CAT_1:def 5; then f in Hom(b opp,a opp) by Th4; hence thesis by CAT_1:def 5; end; end; definition let C; let a,b be Object of C such that A1: Hom(a opp,b opp) <> {}; let f be Morphism of a opp, b opp; func opp f -> Morphism of b, a equals :Def7: f; coherence proof f in Hom(a opp,b opp) by A1,CAT_1:def 5; then f in Hom(b,a) by Th4; hence thesis by CAT_1:def 5; end; end; theorem for a,b being Object of C st Hom(a,b)<>{} for f being Morphism of a,b holds f opp opp = f proof let a,b be Object of C; assume A1: Hom(a,b)<>{}; then A2: Hom(b opp,a opp)<>{} by Th4; let f be Morphism of a,b; thus f opp opp = f opp by A2,Def6 .= f by A1,Def6; end; theorem for a,b being Object of C st Hom(a,b)<>{} for f being Morphism of a,b holds opp(f opp) = f proof let a,b be Object of C; assume A1: Hom(a,b)<>{}; then A2: Hom(b opp,a opp)<>{} by Th4; let f be Morphism of a,b; thus opp(f opp) = f opp by A2,Def7 .= f by A1,Def6; end; theorem for a,b being Object of C opp for f being Morphism of a,b holds (opp f)opp = f; theorem Th9: for a,b being Object of C st Hom(a,b)<>{} for f being Morphism of a,b holds dom(f opp) = cod f & cod(f opp) = dom f proof let a,b be Object of C; assume A1: Hom(a,b)<>{}; then A2: Hom(b opp,a opp)<>{} by Th4; let f be Morphism of a,b; thus dom(f opp) = b by A2,CAT_1:5 .= cod f by A1,CAT_1:5; thus cod(f opp) = a by A2,CAT_1:5 .= dom f by A1,CAT_1:5; end; theorem 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 for a,b being Object of C st Hom(a,b)<>{} for f being Morphism of a,b holds (dom f) opp = cod (f opp) & (cod f)opp = dom (f opp) by Th9; theorem for a,b being Object of C opp st Hom(a,b)<>{} for f being Morphism of a,b holds opp (dom f) = cod (opp f) & opp (cod f) = dom (opp f); ::\$CT theorem Th13: for a,b being Object of C opp,f being Morphism of a,b st Hom(a,b) <> {} holds opp f is Morphism of opp b,opp a proof let a,b be Object of C opp, f be Morphism of a,b; assume Hom(a,b) <> {}; then f in Hom(a,b) by CAT_1:def 5; then opp f in Hom(opp b,opp a) by Th5; hence thesis by CAT_1:def 5; end; theorem Th14: for a,b,c being Object of C st Hom(a,b) <> {} & Hom(b,c) <> {} for f being Morphism of a,b, g being Morphism of b,c holds (g(*)f) opp = (f opp)(*)(g opp) proof let a,b,c be Object of C such that A1: Hom(a,b) <> {} and A2: Hom(b,c) <> {}; A3: Hom(b opp,a opp) <> {} by A1,Th4; A4: Hom(c opp,b opp) <> {} by A2,Th4; let f be Morphism of a,b, g be Morphism of b,c; 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,A8,CAT_1:15,FUNCT_4:53; then (the Comp of C ).(g,f) = (the Comp of C opp).(f opp,g opp) by A7, FUNCT_4:def 2; hence thesis by A5,A6,A8,A9,CAT_1:16; end; theorem for a,b,c being Object of C st Hom(b opp,a opp) <> {} & Hom(c opp,b opp) <> {} for f be Morphism of a,b, g being Morphism of b,c holds (g(*)f) opp = (f opp)(*)(g opp) proof let a,b,c be Object of C; assume Hom(b opp,a opp) <> {} & Hom(c opp,b opp) <> {}; then Hom(a,b) <> {} & Hom(b,c) <> {} by Th4; hence thesis by Th14; end; theorem Th16: for f,g being Morphism of C opp st dom g = cod f holds opp (g(*)f) = (opp f)(*)(opp g) proof let f,g be Morphism of C opp; assume A1: dom g = cod f; 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; end; theorem for a,b,c being Object of C, f being Morphism of a,b, g being Morphism of b, c st Hom(a,b) <> {} & Hom(b,c) <> {} holds (g*f) opp = (f opp)(*)(g opp) proof let a,b,c be Object of C, f be Morphism of a,b, g be Morphism of b,c; assume A1: Hom(a,b) <> {} & Hom(b,c) <> {}; 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,Th14; end; Lm1: 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 a be Object of C; let b be Object of C opp; thus Hom(a opp,b) <> {} implies for f being Morphism of a opp,b holds f(*)((id a) opp) = f proof assume A1: Hom(a opp,b) <> {}; A2: Hom(opp b,opp (a opp)) <> {} by A1,Th5; let f be Morphism of a opp,b; A3: Hom(a,a) <> {}; A4: cod opp(f qua Morphism of C opp) = dom f .= a by A1,CAT_1:5; dom opp(f qua Morphism of C opp) = cod f .= opp b by A1,CAT_1:5; 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,Th14 .= ((id a)*ff)opp by A5,Def6,A2 .= ff opp by A2,CAT_1:28 .= f by A2,Def6; end; assume A6: Hom(b,a opp) <> {}; A7: Hom(opp (a opp),opp b) <> {} by A6,Th5; let f be Morphism of b,a opp; A8: Hom(a,a) <> {}; A9: dom opp(f qua Morphism of C opp) = cod f .= a by A6,CAT_1:5; cod opp(f qua Morphism of C opp) = dom f .= opp b by A6,CAT_1:5; then reconsider ff = opp(f qua Morphism of C opp) 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,Th14 .= (ff*(id a))opp by A10,Def6,A7 .= ff opp by A7,CAT_1:29 .= f by A7,Def6; end; theorem Th18: for a being Object of C holds (id a) opp = id(a opp) proof let a be 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) by Lm1; hence (id a) opp = id(a opp) by CAT_1:def 12; end; Lm2: for a being Object of C holds id a = id(a opp) proof let a be Object of C; Hom(a,a) <> {}; hence id a = (id a)opp by Def6 .= id(a opp) by Th18; end; theorem Th19: for a being Object of C opp holds opp id a = id opp a proof let a be Object of C opp; set b = opp a; thus opp id a = id(b opp) .= id opp a by Lm2; end; Lm3: for a,b,c being Object of C st Hom(a,b) <> {} & Hom(b,c) <> {} for f being Morphism of a,b, g being Morphism of b,c holds g*f = (f opp)*(g opp) proof let a,b,c be Object of C such that A1: Hom(a,b) <> {} and A2: Hom(b,c) <> {}; let f be Morphism of a,b, g be Morphism of b,c; reconsider f1=f as Morphism of C; reconsider g1=g as Morphism of C; A3: Hom(b opp,a opp) <> {} by A1,Th4; A4: Hom(c opp, b opp) <> {} by A2,Th4; g*f = g(*)f opp by A1,A2,CAT_1:def 13 .= (f opp)(*)(g opp) by A1,A2,Th14 .= (f opp)*(g opp) by A3,A4,CAT_1:def 13; hence thesis; end; theorem 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 a,b be Object of C; let f be Morphism of a,b; thus f opp is monic implies f is epi proof assume that A1: Hom(b opp,a opp) <> {} and A2: for c being Object of C opp st Hom(c,b opp) <> {} for f1,f2 being Morphism of c, b opp st (f opp)*f1=(f opp)*f2 holds f1=f2; thus A3: Hom(a,b) <> {} by A1,Th4; let c be Object of C such that A4: Hom(b,c) <> {}; let g1,g2 be Morphism of b,c; assume A5: g1*f = g2*f; reconsider f1=g1 opp, f2=g2 opp as Morphism of c opp, b opp; A6: Hom(c opp,b opp) <> {} by A4,Th4; (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 thesis; end; assume that A8: Hom(a,b) <> {} and A9: for c being Object of C st Hom(b,c) <> {} for g1,g2 being Morphism of b,c st g1*f=g2*f holds g1=g2; thus Hom(b opp,a opp) <> {} by A8,Th4; let c be Object of C opp such that A10: Hom(c,b opp) <> {}; let f1,f2 be Morphism of c, b opp; assume A11: (f opp)*f1=(f opp)*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 Th5; 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,Th5; 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; end; theorem for b,c being Object of C st Hom(b,c) <> {} for f being Morphism of b,c holds f opp is epi iff f is monic proof let b,c be Object of C such that A1: Hom(b,c) <> {}; let f be Morphism of b,c; thus f opp is epi implies f is monic proof assume that Hom(c opp,b opp) <> {} and A2: for a being Object of C opp st Hom(b opp,a) <> {} for g1,g2 being Morphism of b opp,a st g1*(f opp)=g2*(f opp) holds g1=g2; thus Hom(b,c) <> {} by A1; let a be Object of C such that A3: Hom(a,b) <> {}; let f1,f2 be Morphism of a, b; assume A4: f*f1 = f*f2; reconsider g1 = f1 opp,g2 = f2 opp as Morphism of b opp, a opp; A5: Hom(b opp,a opp) <> {} by A3,Th4; 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; end; assume that A6: Hom(b,c) <> {} and A7: for a being Object of C st Hom(a,b) <> {} for f1,f2 being Morphism of a,b st f*f1=f*f2 holds f1=f2; thus Hom(c opp,b opp) <> {} by A6,Th4; let a be Object of C opp such that A8: Hom(b opp,a) <> {}; let g1,g2 be Morphism of b opp,a; assume A9: g1*(f opp) = g2*(f opp); Hom(b opp,a) = Hom(opp a, opp(b opp)) by Th5 .= 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,Th5; 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 thesis by A7,A10; end; theorem 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 a,b be Object of C; let f be Morphism of a,b; thus f opp is invertible implies f is invertible proof assume A1: Hom(b opp,a opp) <> {} & Hom(a opp,b opp) <> {}; given gg being Morphism of a opp, b opp such that A2: (f opp)*gg = id(a opp) & gg*(f opp) = id(b opp); thus A3: Hom(a,b) <> {} & Hom(b,a) <> {} by A1,Th4; reconsider g = opp gg as Morphism of b,a; take g; 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; thus g*f =(f opp)*(g opp) by A3,Lm3 .= id a by A2,A4,Lm2; end; assume A5: Hom(a,b) <> {} & Hom(b,a) <> {}; given g being Morphism of b,a such that A6: f*g = id b & g*f = id a; thus Hom(b opp,a opp) <> {} & Hom(a opp,b opp) <> {} by A5,Th4; take g opp; thus (f opp)*(g opp) = g*f by A5,Lm3 .= id(a opp) by A6,Lm2; thus (g opp)*(f opp) = f*g by A5,Lm3 .= id(b opp) by A6,Lm2; end; theorem for c being Object of C holds c is initial iff c opp is terminal proof let c be Object of C; thus c is initial implies c opp is terminal proof assume A1: c is initial; let b be Object of C opp; consider f being Morphism of c,opp b such that A2: for g being Morphism of c,opp b holds f=g by A1; A3: (opp b) opp = b; A4: Hom(c,opp b)<>{} by A1; reconsider f9 = f opp as Morphism of b,c opp; thus A5: Hom(b,c opp)<>{} by A3,Th4,A4; take f9; let g be Morphism of b,c opp; opp (c opp) = c; then opp g is Morphism of c,opp b by A5,Th13; hence g = f by A2 .= f9 by A4,Def6; end; assume A6: c opp is terminal; let b be Object of C; 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; A8: opp (c opp) = c & opp (b opp) = b; A9: Hom(b opp,c opp)<>{} by A6; reconsider f9 = opp f as Morphism of c,b; thus A10: Hom(c,b)<>{} by A8,Th5,A9; take f9; let g be Morphism of c,b; g opp = f by A7; hence g = f by Def6,A10 .= f9 by A9,Def7; end; theorem for c being Object of C holds c opp is initial iff c is terminal proof let c be Object of C; thus c opp is initial implies c is terminal proof assume A1: c opp is initial; let b be Object of C; 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; A3: opp(b opp) = b & opp(c opp) = c; A4: Hom(c opp,b opp)<>{} by A1; reconsider f9 = opp f as Morphism of b,c; thus A5: Hom(b,c)<>{} by A3,Th5,A4; take f9; let g be Morphism of b,c; g opp = f by A2; hence g = f by A5,Def6 .= f9 by Def7,A4; end; assume A6: c is terminal; let b be Object of C opp; consider f being Morphism of opp b,c such that A7: for g being Morphism of opp b, c holds f = g by A6; A8: (opp b) opp = b; A9: Hom(opp b,c)<>{} by A6; reconsider f9 = f opp as Morphism of c opp,b; thus A10: Hom(c opp,b)<>{} by A8,Th4,A9; take f9; let g be Morphism of c opp,b; opp g is Morphism of opp b,opp (c opp) by A10,Th13; hence g = f by A7 .= f9 by Def6,A9; end; :: Contravariant Functors definition let C,B; 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: for f being Morphism of C holds it.f = S.(f opp); existence proof deffunc F(Morphism of C) = 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 = F(f) from FUNCT_2:sch 4; end; uniqueness proof let T1,T2 be Function of the carrier' of C,the carrier' of B such 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); now let f be Morphism of C; thus T1.f = S.(f opp) by A1 .= T2.f by A2; end; hence thesis by FUNCT_2:63; end; end; theorem 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 S be Function of the carrier' of C opp,the carrier' of B; let f be Morphism of C opp; thus (/*S).(opp f) = S.((opp f) opp) by Def8 .= S.f; end; Lm4: for S being Functor of C opp,B, c being Object of C holds (/*S).(id c) = id((Obj S).(c opp)) proof let S be Functor of C opp,B, c be Object of 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 A1,Def6 .= S.(id(c opp)) by Th18 .= id((Obj S).(c opp)) by CAT_1:68; end; theorem Th26: for S being Functor of C opp,B, c being Object of C holds (Obj /*S).c = (Obj S).(c opp) proof let S be Functor of C opp,B, c be Object of C; A1: now let c be Object of C; (/*S).(id c) = id((Obj S).(c opp)) by Lm4; hence ex d being Object of B st (/*S).(id c) = id d; end; (/*S).(id c) = id((Obj S).(c opp)) by Lm4; hence thesis by A1,CAT_1:66; end; theorem for S being Functor of C opp,B, c being Object of C opp holds (Obj /*S ).(opp c) = (Obj S).c proof let S be Functor of C opp,B, c be Object of C opp; thus (Obj /*S).(opp c) = (Obj S).((opp c) opp) by Th26 .= (Obj S).c; end; Lm5: for S being Functor of C opp,B, c being Object of C holds /*S.(id c) = id ((Obj /*S).c) proof let S be Functor of C opp,B, c be Object of 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 Th18 .= id((Obj S).(c opp)) by CAT_1:68 .= id((Obj /*S).c) by Th26; end; Lm6: now let C,B; let S be Functor of C opp,B, c be Object of C; (/*S).(id c) = id ((Obj /*S).c) by Lm5; hence ex d being Object of B st (/*S).(id c) = id d; end; Lm7: for S being Functor of C opp,B, f being Morphism of C holds (Obj /*S).( dom f) = cod (/*S.f) & (Obj /*S).(cod f) = dom (/*S.f) proof let S be Functor of C opp,B, f be Morphism of C; A1: (Obj /*S).(cod f) = (Obj S).((cod f) opp) by Th26 .= (Obj S).(dom (f opp)) .= dom(S.(f opp)) by CAT_1:69; (Obj /*S).(dom f) = (Obj S).((dom f) opp) by Th26 .= (Obj S).(cod (f opp)) .= cod(S.(f opp)) by CAT_1:69; hence thesis by A1,Def8; end; Lm8: now let C,B; let S be Functor of C opp,B, f be Morphism of C; thus (/*S).(id dom f) = id((Obj /*S).(dom f)) by Lm5 .= id cod (/*S.f) by Lm7; thus (/*S).(id cod f) = id((Obj /*S).(cod f)) by Lm5 .= id dom (/*S.f) by Lm7; end; Lm9: for S being Functor of C opp,B for a,b,c being Object of C st Hom(a,b) <> {} & Hom(b,c) <> {} for f being Morphism of a,b, g being Morphism of b,c holds /*S.(g(*)f) = (/*S.f)(*)(/*S.g) proof let S be Functor of C opp,B; let a,b,c be Object of C such that A1: Hom(a,b) <> {} & Hom(b,c) <> {}; A2: Hom(b opp, a opp) <> {} & Hom(c opp, b opp) <> {} by A1,Th4; let f be Morphism of a,b, g be Morphism of b,c; 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 qua Morphism of C) opp) by A1,Def6 .= /*S.f by Def8; A7: S.(g opp) = S.((g qua Morphism of C) opp) by A1,Def6 .= /*S.g by Def8; thus /*S.(g(*)f) = S.((g(*)f) opp) by Def8 .= S.((f opp)(*)(g opp)) by Th14,A1 .= (/*S.f)(*)(/*S.g) by A7,A6,A5,A3,A4,CAT_1:64; end; definition let C,D; mode Contravariant_Functor of C,D -> Function of the carrier' of C,the carrier' of D means :Def9: ( 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 proof set S = the Functor of C opp,D; take /*S; thus for c being Object of C ex d being Object of D st /*S.(id c) = id d by Lm6; 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; let f,g be Morphism of C such that A1: dom g = cod f; 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 A1,CAT_1:4; 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 thesis; end; end; theorem Th28: for S being Contravariant_Functor of C,D, c being Object of C, d being Object of D st S.(id c) = id d holds (Obj S).c = d proof let S be Contravariant_Functor of C,D; let c be Object of C, d be Object of D; for c being Object of C ex d being Object of D st S.(id c) = id d by Def9; hence thesis by CAT_1:66; end; theorem Th29: for S being Contravariant_Functor of C,D,c being Object of C holds S.(id c) = id((Obj S).c) proof let S be Contravariant_Functor of C,D,c be Object of C; ex d being Object of D st S.(id c) = id d by Def9; hence thesis by Th28; end; theorem Th30: for S being Contravariant_Functor of C,D, f being Morphism of C holds (Obj S).(dom f) = cod (S.f) & (Obj S).(cod f) = dom (S.f) proof let S be Contravariant_Functor of C,D, f be Morphism of C; S.(id dom f) = id cod (S.f) & S.(id cod f) = id dom (S.f) by Def9; hence thesis by Th28; end; theorem Th31: for S being Contravariant_Functor of C,D, f,g being Morphism of C st dom g = cod f holds dom (S.f) = cod (S.g) proof let S be Contravariant_Functor of C,D, f,g be Morphism of C; assume dom g = cod f; hence dom (S.f) = (Obj S).(dom g) by Th30 .= cod (S.g) by Th30; end; theorem Th32: for S being Functor of C opp,B holds /*S is Contravariant_Functor of C,B proof let S be Functor of C opp,B; thus for c being Object of C ex d being Object of B st /*S.(id c) = id d by Lm6; 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; let f,g be Morphism of C such that A1: dom g = cod f; 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 A1,CAT_1:4; 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 thesis; end; theorem Th33: for S1 being Contravariant_Functor of C,B, S2 being Contravariant_Functor of B,D holds S2*S1 is Functor of C,D proof let S1 be Contravariant_Functor of C,B, S2 be Contravariant_Functor of B,D; set T = S2*S1; now thus for c being Object of C ex d being Object of D st T.(id c) = id d proof let c be Object of C; 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; thus thesis by A1,A2,FUNCT_2:15; end; thus for f being Morphism of C holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) proof let f be Morphism of C; thus T.(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 (T.f) by FUNCT_2:15; thus T.(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 (T.f) by FUNCT_2:15; end; let f,g be Morphism of C; assume A3: dom g = cod f; then A4: cod (S1.g) = dom(S1.f) by Th31; thus T.(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 .= (T.g)(*)(S2.(S1.f)) by FUNCT_2:15 .= (T.g)(*)(T.f) by FUNCT_2:15; end; hence thesis by CAT_1:61; end; Lm10: for S being Contravariant_Functor of C opp,B, c being Object of C holds ( /*S).(id c) = id((Obj S).(c opp)) proof let S be Contravariant_Functor of C opp,B, c be Object of 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 Th18 .= id((Obj S).(c opp)) by Th29; end; theorem Th34: for S being Contravariant_Functor of C opp,B, c being Object of C holds (Obj /*S).c = (Obj S).(c opp) proof let S be Contravariant_Functor of C opp,B, c be Object of C; A1: now let c be Object of C; (/*S).(id c) = id((Obj S).(c opp)) by Lm10; hence ex d being Object of B st (/*S).(id c) = id d; end; (/*S).(id c) = id((Obj S).(c opp)) by Lm10; hence thesis by A1,CAT_1:66; end; theorem for S being Contravariant_Functor of C opp,B, c being Object of C opp holds (Obj /*S).(opp c) = (Obj S).c proof let S be Contravariant_Functor of C opp,B, c be Object of C opp; thus (Obj /*S).(opp c) = (Obj S).((opp c) opp) by Th34 .= (Obj S).c; end; Lm11: for S being Contravariant_Functor of C opp,B, c being Object of C holds /*S.(id c) = id((Obj /*S).c) proof let S be Contravariant_Functor of C opp,B, c be Object of 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 Th18 .= id((Obj S).(c opp)) by Th29 .= id((Obj /*S).c) by Th34; end; Lm12: for S being Contravariant_Functor of C opp,B, f being Morphism of C holds (Obj /*S).(dom f) = dom (/*S.f) & (Obj /*S).(cod f) = cod (/*S.f) proof let S be Contravariant_Functor of C opp,B, f be Morphism of C; A1: (Obj /*S).(cod f) = (Obj S).((cod f) opp) by Th34 .= (Obj S).(dom (f opp)) .= cod(S.(f opp)) by Th30; (Obj /*S).(dom f) = (Obj S).((dom f) opp) by Th34 .= (Obj S).(cod (f opp)) .= dom(S.(f opp)) by Th30; hence thesis by A1,Def8; end; theorem for S being Contravariant_Functor of C opp,B holds /*S is Functor of C , B proof let S be Contravariant_Functor of C opp,B; now thus for c being Object of C ex d being Object of B st /*S.(id c) = id d proof let c be Object of C; (/*S).(id c) = id ((Obj /*S).c) by Lm11; hence thesis; 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) proof let f be Morphism of C; thus (/*S).(id dom f) = id((Obj /*S).(dom f)) by Lm11 .= id dom (/*S.f) by Lm12; thus (/*S).(id cod f) = id((Obj /*S).(cod f)) by Lm11 .= id cod (/*S.f) by Lm12; end; let f,g be Morphism of C such that A1: dom g = cod 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 A1,CAT_1:4; 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,Th14 .= (S.(g opp))(*)(S.(f opp)) by A1,A2,Def9 .= (/*S.g)(*)(S.(f opp)) by Def8 .= (/*S.g)(*)(/*S.f) by Def8; end; hence thesis by CAT_1:61; end; :: Dualization functors definition let C,B; 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: for f being Morphism of C opp holds it.f = S.(opp f); existence proof deffunc F(Morphism of C opp) = 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 = F(f) from FUNCT_2:sch 4; end; uniqueness proof let T1,T2 be Function of the carrier' of C opp,the carrier' of B such 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); now let f be Morphism of C opp; thus T1.f = S.(opp f) by A1 .= T2.f by A2; end; hence thesis by FUNCT_2:63; end; func S*' -> Function of the carrier' of C,the carrier' of B opp means :Def11: for f being Morphism of C holds it.f = (S.f) opp; existence proof deffunc F(Morphism of C) = (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 = F(f) from FUNCT_2:sch 4; end; uniqueness proof let T1,T2 be Function of the carrier' of C,the carrier' of B opp such 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; now let f be Morphism of C; thus T1.f = (S.f) opp by A3 .= T2.f by A4; end; hence thesis by FUNCT_2:63; end; end; theorem 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 S be Function of the carrier' of C,the carrier' of B; let f be Morphism of C; thus (*'S).(f opp) = S.(opp (f opp)) by Def10 .= S.f; end; Lm13: for S being Functor of C,B, c being Object of C opp holds (*'S).(id c) = id((Obj S).(opp c)) proof let S be Functor of C,B, c be Object of C opp; thus (*'S).(id c) = S.(opp id c) by Def10 .= S.(id opp c)by Th19 .= id((Obj S).(opp c)) by CAT_1:68; end; theorem Th38: for S being Functor of C,B, c being Object of C opp holds (Obj *'S).c = (Obj S).(opp c) proof let S be Functor of C,B, c be Object of C opp; now thus (*'S).(id c) = id((Obj S).(opp c)) by Lm13; let c be Object of C opp; (*'S).(id c) = id((Obj S).(opp c)) by Lm13; hence ex d being Object of B st (*'S).(id c) = id d; end; hence thesis by CAT_1:66; end; theorem for S being Functor of C,B, c being Object of C holds (Obj *'S).(c opp ) = (Obj S).c proof let S be Functor of C,B, c be Object of C; thus (Obj *'S).(c opp) = (Obj S).(opp (c opp)) by Th38 .= (Obj S).c; end; Lm14: for S being Functor of C,B, c being Object of C holds (S*').(id c) = id( ((Obj S).c) opp) proof let S be Functor of C,B, c be Object of C; A1: Hom((Obj S).c,(Obj S).c) <> {}; thus (S*').(id c) = (S.(id c)) opp by Def11 .= (id((Obj S).c) qua Morphism of B) opp by CAT_1:68 .= (id((Obj S).c)) opp by Def6,A1 .= id(((Obj S).c) opp) by Th18; end; theorem Th40: for S being Functor of C,B, c being Object of C holds (Obj S*'). c = ((Obj S).c) opp proof let S be Functor of C,B, c be Object of C; now thus (S*').(id c) = id(((Obj S).c) opp) by Lm14; let c be Object of C; (S*').(id c) = id(((Obj S).c) opp) by Lm14; hence ex d being Object of B opp st (S*').(id c) = id d; end; hence thesis by CAT_1:66; end; Lm15: for S being Contravariant_Functor of C,B, c being Object of C opp holds (*'S).(id c) = id((Obj S).(opp c)) proof let S be Contravariant_Functor of C,B, c be Object of C opp; thus (*'S).(id c) = S.(opp id c) by Def10 .= S.(id opp c) by Th19 .= id((Obj S).(opp c)) by Th29; end; theorem Th41: for S being Contravariant_Functor of C,B, c being Object of C opp holds (Obj *'S).c = (Obj S).(opp c) proof let S be Contravariant_Functor of C,B, c be Object of C opp; now thus (*'S).(id c) = id((Obj S).(opp c)) by Lm15; let c be Object of C opp; (*'S).(id c) = id((Obj S).(opp c)) by Lm15; hence ex d being Object of B st (*'S).(id c) = id d; end; hence thesis by CAT_1:66; end; theorem for S being Contravariant_Functor of C,B, c being Object of C holds ( Obj *'S).(c opp) = (Obj S).c proof let S be Contravariant_Functor of C,B, c be Object of C; thus (Obj *'S).(c opp) = (Obj S).(opp (c opp)) by Th41 .= (Obj S).c; end; Lm16: for S being Contravariant_Functor of C,B, c being Object of C holds (S*' ).(id c) = id(((Obj S).c) opp) proof let S be Contravariant_Functor of C,B, c be Object of C; A1: Hom((Obj S).c,(Obj S).c) <> {}; thus (S*').(id c) = (S.(id c)) opp by Def11 .= (id((Obj S).c) qua Morphism of B) opp by Th29 .= (id((Obj S).c)) opp by Def6,A1 .= id(((Obj S).c) opp) by Th18; end; theorem Th43: for S being Contravariant_Functor of C,B, c being Object of C holds (Obj S*').c = ((Obj S).c) opp proof let S be Contravariant_Functor of C,B, c be Object of C; now thus (S*').(id c) = id(((Obj S).c) opp) by Lm16; let c be Object of C; (S*').(id c) = id(((Obj S).c) opp) by Lm16; hence ex d being Object of B opp st (S*').(id c) = id d; end; hence thesis by CAT_1:66; end; Lm17: 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 F be Function of the carrier' of C,the carrier' of D; let f be Morphism of C opp; thus *'F*'.f = (*'F.f) opp by Def11 .= (F.(opp f)) opp by Def10; end; theorem Th44: 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 F be Function of the carrier' of C,the carrier' of D; let f be Morphism of C; thus *'F*'.(f opp) = (F.(opp(f opp))) opp by Lm17 .= (F.f) opp; end; theorem Th45: for S being Function of the carrier' of C,the carrier' of D holds /*(*'S) = S proof let S be Function of the carrier' of C,the carrier' of D; now let f be Morphism of C; thus /*(*'S).f = (*'S).(f opp) by Def8 .= S.(opp (f opp)) by Def10 .= S.f; end; hence thesis by FUNCT_2:63; end; theorem for S being Function of the carrier' of C opp,the carrier' of D holds *'(/*S) = S proof let S be Function of the carrier' of C opp,the carrier' of D; now let f be Morphism of C opp; thus *'(/*S).f = (/*S).(opp f) by Def10 .= S.((opp f) opp) by Def8 .= S.f; end; hence thesis by FUNCT_2:63; end; theorem for S being Function of the carrier' of C, the carrier' of D holds *'S *' = *'(S*') proof let S be Function of the carrier' of C, the carrier' of D; now let f be Morphism of C opp; thus *'S*'.f = (*'S.f) opp by Def11 .= (S.(opp f)) opp by Def10 .= (S*').(opp f) by Def11 .= *'(S*').f by Def10; end; hence thesis by FUNCT_2:63; end; theorem for D being strict Category, S being Function of the carrier' of C, the carrier' of D holds S*'*' = S proof let D be strict Category; let S be Function of the carrier' of C, the carrier' of D; now thus D opp opp = D by FUNCT_4:53; let f be Morphism of C; thus S*'*'.f = (S*'.f) opp by Def11 .= (S.f) opp opp by Def11 .= S.f; end; hence thesis by FUNCT_2:63; end; theorem for C being strict Category, S being Function of the carrier' of C, the carrier' of D holds *'*'S = S proof let C be strict Category; let S be Function of the carrier' of C, the carrier' of D; now thus C opp opp = C by FUNCT_4:53; let f be Morphism of C opp opp; thus *'*'S.f = *'S.(opp f) by Def10 .= S.(opp opp f) by Def10 .= S.f; end; hence thesis by FUNCT_2:63; end; Lm18: 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 S be Function of the carrier' of C opp,the carrier' of B; let T be Function of the carrier' of B,the carrier' of D; now let f be Morphism of C; 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; end; hence thesis by FUNCT_2:63; end; theorem 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 S be Function of the carrier' of C,the carrier' of B; let T be Function of the carrier' of B,the carrier' of D; now let f be Morphism of C opp; 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; end; hence thesis by FUNCT_2:63; end; theorem 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 S be Function of the carrier' of C,the carrier' of B; let T be Function of the carrier' of B,the carrier' of D; now let f be Morphism of C; 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; end; hence thesis by FUNCT_2:63; end; theorem 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 F1 be Function of the carrier' of C,the carrier' of B; let F2 be Function of the carrier' of B,the carrier' of D; now let f be Morphism of C opp; 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 Th44 .= (*'F2*').((*'F1*').f) by Lm17 .= ((*'F2*')*(*'F1*')).f by FUNCT_2:15; end; hence thesis by FUNCT_2:63; end; Lm19: for S being Contravariant_Functor of C,B, c being Object of C opp holds *'S.(id c) = id((Obj *'S).c) proof let S be Contravariant_Functor of C,B, c be Object of C opp; thus *'S.(id c) = S.(opp id c) by Def10 .= S.(id opp c) by Th19 .= id((Obj S).(opp c)) by Th29 .= id((Obj *'S).c) by Th41; end; Lm20: for S being Contravariant_Functor of C,B, f being Morphism of C opp holds (Obj *'S).(dom f) = dom (*'S.f) & (Obj *'S).(cod f) = cod (*'S.f) proof let S be Contravariant_Functor of C,B, f be Morphism of C opp; A1: (Obj *'S).(cod f) = (Obj S).(opp cod f) by Th41 .= (Obj S).(dom opp f) .= cod(S.(opp f)) by Th30; (Obj *'S).(dom f) = (Obj S).(opp dom f) by Th41 .= (Obj S).(cod opp f ) .= dom(S.(opp f)) by Th30; hence thesis by A1,Def10; end; theorem Th53: for S being Contravariant_Functor of C,D holds *'S is Functor of C opp,D proof let S be Contravariant_Functor of C,D; now thus for c being Object of C opp ex d being Object of D st *'S.(id c) = id d proof let c be Object of C opp; (*'S).(id c) = id ((Obj *'S).c) by Lm19; hence thesis; 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) proof let f be Morphism of C opp; thus (*'S).(id dom f) = id((Obj *'S).(dom f)) by Lm19 .= id dom (*'S.f) by Lm20; thus (*'S).(id cod f) = id((Obj *'S).(cod f)) by Lm19 .= id cod (*'S.f) by Lm20; end; let f,g be Morphism of C opp such that A1: dom g = cod 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,Th16 .= (S.(opp g))(*)(S.(opp f)) by A1,A2,Def9 .= (*'S.g)(*)(S.(opp f)) by Def10 .= (*'S.g)(*)(*'S.f) by Def10; end; hence thesis by CAT_1:61; end; Lm21: for S being Contravariant_Functor of C,B, c being Object of C holds S*'. (id c) = id((Obj S*').c) proof let S be Contravariant_Functor of C,B, c be Object of C; A1: Hom((Obj S).c,(Obj S).c) <> {}; thus S*'.(id c) = (S.(id c)) opp by Def11 .= (id((Obj S).c) qua Morphism of B) opp by Th29 .= (id((Obj S).c)) opp by Def6,A1 .= id(((Obj S).c) opp) by Th18 .= id((Obj S*').c) by Th43; end; Lm22: for S being Contravariant_Functor of C,B, f being Morphism of C holds ( Obj S*').(dom f) = dom (S*'.f) & (Obj S*').(cod f) = cod (S*'.f) proof let S be Contravariant_Functor of C,B, f be Morphism of C; A1: (Obj S*').(cod f) = ((Obj S).(cod f)) opp by Th43 .= (dom(S.f)) opp by Th30 .= cod((S.f) opp); (Obj S*').(dom f) = ((Obj S).(dom f)) opp by Th43 .= (cod(S.f)) opp by Th30 .= dom((S.f) opp); hence thesis by A1,Def11; end; theorem Th54: for S being Contravariant_Functor of C,D holds S*' is Functor of C, D opp proof let S be Contravariant_Functor of C,D; now thus for c being Object of C ex d being Object of D opp st S*'.(id c) = id d proof let c be Object of C; (S*').(id c) = id(((Obj S).c) opp) by Lm16; hence thesis; 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) proof let f be Morphism of C; thus (S*').(id dom f) = id((Obj S*').(dom f)) by Lm21 .= id dom (S*'.f) by Lm22; thus (S*').(id cod f) = id((Obj S*').(cod f)) by Lm21 .= id cod (S*'.f) by Lm22; end; let f,g be Morphism of C; assume A1: dom g = cod f; then A2: dom(S.f) = cod (S.g) by Th31; 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,Th14 .= (S*'.g)(*)((S.f) opp) by Def11,A4,A5 .= (S*'.g)(*)(S*'.f) by Def11; end; hence thesis by CAT_1:61; end; Lm23: for S being Functor of C,B, c being Object of C opp holds *'S.(id c) = id((Obj *'S).c) proof let S be Functor of C,B, c be Object of C opp; thus *'S.(id c) = S.(opp id c) by Def10 .= S.(id opp c) by Th19 .= id((Obj S).(opp c)) by CAT_1:68 .= id((Obj *'S).c) by Th38; end; Lm24: for S being Functor of C,B, f being Morphism of C opp holds (Obj *'S).( dom f) = cod (*'S.f) & (Obj *'S).(cod f) = dom (*'S.f) proof let S be Functor of C,B, f be Morphism of C opp; A1: (Obj *'S).(cod f) = (Obj S).(opp cod f) by Th38 .= (Obj S).(dom opp f) .= dom(S.(opp f)) by CAT_1:69; (Obj *'S).(dom f) = (Obj S).(opp dom f) by Th38 .= (Obj S).(cod opp f ) .= cod(S.(opp f)) by CAT_1:69; hence thesis by A1,Def10; end; theorem Th55: for S being Functor of C,D holds *'S is Contravariant_Functor of C opp,D proof let S be Functor of C,D; thus for c being Object of C opp ex d being Object of D st *'S.(id c) = id d proof let c be Object of C opp; (*'S).(id c) = id ((Obj *'S).c) by Lm23; hence thesis; 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) proof let f be Morphism of C opp; thus (*'S).(id dom f) = id((Obj *'S).(dom f)) by Lm23 .= id cod(*'S.f) by Lm24; thus (*'S).(id cod f) = id((Obj *'S).(cod f)) by Lm23 .= id dom(*'S.f) by Lm24; end; let f,g be Morphism of C opp such that A1: dom g = cod 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,Th16 .= (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; end; Lm25: for S being Functor of C,B, c being Object of C holds S*'.(id c) = id(( Obj S*').c) proof let S be Functor of C,B, c be Object of C; A1: Hom((Obj S).c,(Obj S).c) <> {}; thus S*'.(id c) = (S.(id c)) opp by Def11 .= (id((Obj S).c) qua Morphism of B) opp by CAT_1:68 .= (id((Obj S).c)) opp by Def6,A1 .= id(((Obj S).c) opp) by Th18 .= id((Obj S*').c) by Th40; end; Lm26: for S being Functor of C,B, f being Morphism of C holds (Obj S*').(dom f ) = cod (S*'.f) & (Obj S*').(cod f) = dom (S*'.f) proof let S be Functor of C,B, f be Morphism of C; A1: (Obj S*').(cod f) = ((Obj S).(cod f)) opp by Th40 .= (cod(S.f)) opp by CAT_1:69 .= dom((S.f) opp); (Obj S*').(dom f) = ((Obj S).(dom f)) opp by Th40 .= (dom(S.f)) opp by CAT_1:69 .= cod((S.f) opp); hence thesis by A1,Def11; end; theorem Th56: for S being Functor of C,D holds S*' is Contravariant_Functor of C, D opp proof let S be Functor of C,D; thus for c being Object of C ex d being Object of D opp st S*'.(id c) = id d proof let c be Object of C; (S*').(id c) = id ((Obj S*').c) by Lm25; hence thesis; 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) proof let f be Morphism of C; thus (S*').(id dom f) = id((Obj S*').(dom f)) by Lm25 .= id cod(S*'.f) by Lm26; thus (S*').(id cod f) = id((Obj S*').(cod f)) by Lm25 .= id dom(S*'.f) by Lm26; end; let f,g be Morphism of C; assume A1: dom g = cod f; 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,Th14,A3 .= (S*'.f)(*)((S.g) opp) by Def11,A4,A5 .= (S*'.f)(*)(S*'.g) by Def11; end; theorem for S1 being Contravariant_Functor of C,B, S2 being Functor of B,D holds S2*S1 is Contravariant_Functor of C,D proof let S1 be Contravariant_Functor of C,B, S2 be Functor of B,D; *'S1 is Functor of C opp,B by Th53; then S2*(*'S1) is Functor of C opp,D by CAT_1:73; then /*(S2*(*'S1)) is Contravariant_Functor of C,D by Th32; then S2*(/*(*'S1)) is Contravariant_Functor of C,D by Lm18; hence thesis by Th45; end; theorem for S1 being Functor of C,B, S2 being Contravariant_Functor of B,D holds S2*S1 is Contravariant_Functor of C,D proof let S1 be Functor of C,B, S2 be Contravariant_Functor of B,D; *'S1 is Contravariant_Functor of C opp,B by Th55; then S2*(*'S1) is Functor of C opp,D by Th33; then /*(S2*(*'S1)) is Contravariant_Functor of C,D by Th32; then S2*(/*(*'S1)) is Contravariant_Functor of C,D by Lm18; hence thesis by Th45; end; theorem for F being Functor of C,D, c being Object of C holds (Obj *'F*').(c opp) = ((Obj F).c) opp proof let F be Functor of C,D, c be Object of C; *'F is Contravariant_Functor of C opp,D by Th55; hence (Obj *'F*').(c opp) = ((Obj *'F).(c opp)) opp by Th43 .= ((Obj F).(opp (c opp))) opp by Th38 .= ((Obj F).c) opp; end; theorem for F being Contravariant_Functor of C,D, c being Object of C holds ( Obj *'F*').(c opp) = ((Obj F).c) opp proof let F be Contravariant_Functor of C,D, c be Object of C; *'F is Functor of C opp,D by Th53; hence (Obj *'F*').(c opp) = ((Obj *'F).(c opp)) opp by Th40 .= ((Obj F).(opp(c opp))) opp by Th41 .= ((Obj F).c) opp; end; theorem for F being Functor of C,D holds *'F*' is Functor of C opp,D opp proof let F be Functor of C,D; *'F is Contravariant_Functor of C opp,D by Th55; hence thesis by Th54; end; theorem for F being Contravariant_Functor of C,D holds *'F*' is Contravariant_Functor of C opp,D opp proof let F be Contravariant_Functor of C,D; *'F is Functor of C opp,D by Th53; hence thesis by Th56; end; :: Duality Functors definition let C; func id* C -> Contravariant_Functor of C,C opp equals (id C)*'; coherence by Th56; func *id C -> Contravariant_Functor of C opp,C equals *'(id C); coherence by Th55; end; theorem Th63: for f being Morphism of C holds (id* C).f = f opp proof let f be Morphism of C; thus (id* C).f = ((id C).f) opp by Def11 .= f opp by FUNCT_1:18; end; theorem for c being Object of C holds (Obj id* C).c = c opp proof let c be Object of C; thus (Obj id* C).c = ((Obj id C).c) opp by Th40 .= c opp by CAT_1:77; end; theorem Th65: for f being Morphism of C opp holds (*id C).f = opp f proof let f be Morphism of C opp; thus (*id C).f = ((id C).(opp f)) by Def10 .= opp f by FUNCT_1:18; end; theorem for c being Object of C opp holds (Obj *id C).c = opp c proof let c be Object of C opp; thus (Obj *id C).c = (Obj id C).(opp c) by Th38 .= opp c by CAT_1:77; end; theorem for S being Function of the carrier' of C,the carrier' of D holds *'S = S*(*id C) & S*' = (id* D)*S proof let S be Function of the carrier' of C,the carrier' of D; now let f be Morphism of C opp; thus *'S.f = S.(opp f) by Def10 .= S.((*id C).f) by Th65 .= (S*(*id C)).f by FUNCT_2:15; end; hence *'S = S*(*id C) by FUNCT_2:63; now let f be Morphism of C; thus S*'.f = (S.f) opp by Def11 .= (id* D).(S.f) by Th63 .= ((id* D)*S).f by FUNCT_2:15; end; hence thesis by FUNCT_2:63; end; theorem for a,b,c being Object of C st Hom(a,b) <> {} & Hom(b,c) <> {} for f being Morphism of a,b, g being Morphism of b,c holds g*f = (f opp)*(g opp) by Lm3; theorem Th69: for a being Object of C holds id a = id(a opp) by Lm2; theorem for a being Object of C opp holds id a = id opp a proof let a be Object of C opp; thus id a = id ((opp a)opp) .= id opp a by Th69; end;