### The Mizar article:

### Opposite Categories and Contravariant Functors

**by****Czeslaw Bylinski**

- Received February 13, 1991
Copyright (c) 1991 Association of Mizar Users

- MML identifier: OPPCAT_1
- [ MML identifier index ]

environ vocabulary CAT_1, PARTFUN1, RELAT_1, FUNCT_1, BOOLE, ARYTM_3, OPPCAT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1, FUNCT_4, CAT_1; constructors FUNCT_4, CAT_1, MEMBERED, XBOOLE_0; clusters CAT_1, RELSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions CAT_1; theorems FUNCT_2, FUNCT_4, PARTFUN1, CAT_1, SUBSET_1; schemes FUNCT_2; begin reserve B,C,D for Category; definition let X,Y,Z be non empty set; let f be PartFunc of [:X,Y:],Z; redefine func ~f -> PartFunc of [:Y,X:],Z; coherence by FUNCT_4:49; end; :: Opposite Category theorem Th1: CatStr (#the Objects of C, the Morphisms of C,the Cod of C, the Dom of C, ~(the Comp of C), the Id of C#) is Category proof set M = the Morphisms of C, d = the Cod of C, c = the Dom of C, p = ~(the Comp of C), i = the Id of C; now thus A1: for f,g being Element of M holds [g,f] in dom(p) iff d.g=c.f proof let f,g be Element of M; [g,f] in dom(p) iff [f,g] in dom (the Comp of C) by FUNCT_4:43; hence thesis by CAT_1:def 8; end; A2: 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; assume d.g = c.f; then [g,f] in dom(p) by A1; hence thesis by FUNCT_4:44; end; thus A3: for f,g being Element of M st d.g = c.f holds d.(p.[g,f]) = d.f & c.(p.[g,f]) = c.g proof let f,g be Element of M; d.g = c.f implies p.[g,f] = (the Comp of C).[f,g] by A2; hence thesis by CAT_1:def 8; end; thus for f,g,h being Element of M st d.h = c.g & d.g = c.f holds p.[h,p.[g,f]] = p.[p.[h,g],f] proof let f,g,h be Element of M; assume A4: d.h = c.g & d.g = c.f; then [g,f] in dom p & [h,g] in dom p by A1; then p.[g,f] = (the Comp of C).[f,g] & p.[h,g] = (the Comp of C).[g,h] & c.(p.[g,f]) = c.g & d.(p.[h,g]) = d.g & p.[g,f] is Element of M & p.[h,g] is Element of M by A2,A3,A4,PARTFUN1: 27; then p.[h,p.[g,f]] = (the Comp of C).[(the Comp of C).[f,g],h] & p.[p.[h,g],f] = (the Comp of C).[f,(the Comp of C).[g,h]] by A2,A4; hence thesis by A4,CAT_1:def 8; end; let b be Element of (the Objects of C); thus A5: d.(i.b) = b & c.(i.b) = b by CAT_1:def 8; thus for f being Element of M st c.f = b holds p.[i.b,f] = f proof let f be Element of M; c.f = b implies p.[i.b,f] = (the Comp of C).[f,i.b] by A2,A5; hence thesis by CAT_1:def 8; end; let g be Element of M; d.g = b implies p.[g,i.b] = (the Comp of C).[i.b,g] by A2,A5; hence d.g = b implies p.[g,i.b] = g by CAT_1:def 8; end; hence thesis by CAT_1:def 8; end; definition let C; func C opp -> strict Category equals :Def1: CatStr (#the Objects of C, the Morphisms of C, the Cod of C, the Dom of C, ~(the Comp of C), the Id of C#); coherence by Th1; end; Lm1: the Objects of C opp = the Objects of C & the Morphisms of C opp = the Morphisms of C & the Dom of C opp = the Cod of C & the Cod of C opp = the Dom of C & the Comp of C opp = ~(the Comp of C) & the Id of C opp = the Id of C proof C opp = CatStr (#the Objects of C, the Morphisms of C, the Cod of C, the Dom of C, ~(the Comp of C), the Id of C#) by Def1; hence thesis; end; theorem Th2: C opp opp = the CatStr of C proof the Objects of C opp = the Objects of C & the Morphisms of C opp = the Morphisms of C & the Dom of C opp = the Cod of C & the Cod of C opp = the Dom of C & the Comp of C opp = ~(the Comp of C) & the Id of C opp = the Id of C & the Objects of C opp opp = the Objects of C opp & the Morphisms of C opp opp = the Morphisms of C opp& the Dom of C opp opp = the Cod of C opp & the Cod of C opp opp = the Dom of C opp & the Comp of C opp opp = ~(the Comp of C opp) & the Id of C opp opp = the Id of C opp & ~~(the Comp of C) = the Comp of C by Lm1,FUNCT_4:54; hence C opp opp = the CatStr of C; end; definition let C; let c be Object of C; func c opp -> Object of C opp equals :Def2: c; coherence by Lm1; end; definition let C; let c be Object of C opp; func opp c -> Object of C equals :Def3: c opp; coherence proof the Objects of C opp = the Objects of C & the Objects of C opp opp = the Objects of C opp by Lm1; hence thesis; end; end; theorem for c being Object of C holds c opp opp = c proof let c be Object of C; thus c opp opp = c opp by Def2 .= c by Def2; end; theorem Th4: for c being Object of C holds opp (c opp) = c proof let c be Object of C; thus opp (c opp) = c opp opp by Def3 .= c opp by Def2 .= c by Def2; end; theorem Th5: for c being Object of C opp holds (opp c) opp = c proof let c be Object of C opp; thus (opp c) opp = opp c by Def2 .= c opp by Def3 .= c by Def2; end; definition let C; let f be Morphism of C; func f opp -> Morphism of C opp equals :Def4: f; coherence by Lm1; end; definition let C; let f be Morphism of C opp; func opp f -> Morphism of C equals :Def5: f opp; coherence proof the Morphisms of C opp = the Morphisms of C & the Morphisms of C opp opp = the Morphisms of C opp by Lm1; hence thesis; end; end; theorem Th6: for f being Morphism of C holds f opp opp = f proof let f be Morphism of C; thus f opp opp = f opp by Def4 .= f by Def4; end; theorem Th7: for f being Morphism of C holds opp(f opp) = f proof let f be Morphism of C; thus opp(f opp) = f opp opp by Def5 .= f opp by Def4 .= f by Def4; end; theorem Th8: for f being Morphism of C opp holds (opp f)opp = f proof let f be Morphism of C opp; thus (opp f)opp = opp f by Def4 .= f opp by Def5 .= f by Def4; end; theorem Th9: for f being Morphism of C holds dom(f opp) = cod f & cod(f opp) = dom f proof let f be Morphism of C; thus dom(f opp) = (the Dom of C opp).(f opp) by CAT_1:def 2 .= (the Dom of C opp).f by Def4 .= (the Cod of C).f by Lm1 .= cod f by CAT_1:def 3; thus cod(f opp) = (the Cod of C opp).(f opp) by CAT_1:def 3 .= (the Cod of C opp).f by Def4 .= (the Dom of C).f by Lm1 .= dom f by CAT_1:def 2; end; theorem Th10: for f being Morphism of C opp holds dom(opp f) = cod f & cod(opp f) = dom f proof let f be Morphism of C opp; dom(opp f) = (the Dom of C).(opp f) & cod(opp f) = (the Cod of C).(opp f) & dom(f opp) = (the Dom of C opp opp).(f opp) & cod(f opp) = (the Cod of C opp opp).(f opp) & the Dom of C opp = the Cod of C & the Cod of C opp = the Dom of C & the Dom of C opp = the Cod of C opp opp & the Cod of C opp = the Dom of C opp opp by Lm1,CAT_1:def 2,def 3; then dom(opp f) = dom(f opp) & cod(opp f) = cod(f opp) by Def5; hence thesis by Th9; end; theorem Th11: for f being Morphism of C holds (dom f) opp = cod (f opp) & (cod f) opp = dom (f opp) proof let f be Morphism of C; thus (dom f) opp = dom f by Def2 .= cod (f opp) by Th9; thus (cod f) opp = cod f by Def2 .= dom (f opp) by Th9; end; theorem Th12: for f being Morphism of C opp holds opp (dom f) = cod (opp f) & opp (cod f) = dom (opp f) proof let f be Morphism of C opp; dom(opp f) = (the Dom of C).(opp f) & cod(opp f) = (the Cod of C).(opp f) & dom(f opp) = (the Dom of C opp opp).(f opp) & cod(f opp) = (the Cod of C opp opp).(f opp) & the Dom of C opp = the Cod of C & the Cod of C opp = the Dom of C & the Dom of C opp = the Cod of C opp opp & the Cod of C opp = the Dom of C opp opp by Lm1,CAT_1:def 2,def 3; then opp (dom f) = (dom f) opp & opp (cod f) = (cod f) opp & dom(opp f) = dom(f opp) & cod(opp f) = cod(f opp) by Def3,Def5; hence thesis by Th11; end; theorem Th13: for a,b being Object of C for f being Morphism of C holds f in Hom(a,b) iff f opp in Hom(b opp,a opp) proof let a,b be Object of C; let f be Morphism of C; (dom f = a & cod f = b iff f in Hom(a,b)) & a opp = a & b opp = b & dom(f opp) = cod f & cod(f opp) = dom f & (cod(f opp) = a opp & dom(f opp) = b opp iff f opp in Hom(b opp,a opp)) by Def2,Th9,CAT_1:18; hence thesis; end; theorem Th14: for a,b being Object of C opp, f being Morphism of C opp holds f in Hom(a,b) iff opp f in Hom(opp b,opp a) proof let a,b be Object of C opp, f be Morphism of C opp; now thus dom(opp f) = cod f & cod(opp f) = dom f by Th10; thus opp a = a opp by Def3 .= a by Def2; thus opp b = b opp by Def3 .= b by Def2; thus f in Hom(a,b) iff dom(f)=a & cod(f)=b by CAT_1:18; end; hence thesis by CAT_1:18; end; theorem Th15: for a,b being Object of C, f being Morphism of a,b st Hom(a,b) <> {} holds f opp is Morphism of b opp,a opp proof let a,b be Object of C, f be Morphism of a,b; assume Hom(a,b) <> {}; then f in Hom(a,b) by CAT_1:def 7; then f opp in Hom(b opp,a opp) by Th13; hence thesis by CAT_1:def 7; end; theorem Th16: 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 7; then opp f in Hom(opp b,opp a) by Th14; hence thesis by CAT_1:def 7; end; theorem Th17: for f,g being Morphism of C st dom g = cod f holds (g*f) opp = (f opp)*(g opp) proof let f,g be Morphism of C; assume A1: dom g = cod f; then A2: g*f = ( the Comp of C ).[g,f] by CAT_1:41; A3: dom g = cod(g opp) & cod f = dom(f opp) by Th9; the Comp of C = ~~(the Comp of C) by FUNCT_4:54; then the Comp of C = ~(the Comp of C opp) & f opp = f & g opp = g & [f opp,g opp] in dom(the Comp of C opp) by A1,A3,Def4,Lm1,CAT_1:40; then (the Comp of C ).[g,f] = (the Comp of C opp).[f opp,g opp] by FUNCT_4:def 2; then g*f = (f opp)*(g opp) by A1,A2,A3,CAT_1:41; hence thesis by Def4; end; theorem Th18: for f,g being Morphism of C st cod(g opp) = dom(f opp) holds (g*f) opp = (f opp)*(g opp) proof let f,g be Morphism of C; cod(g opp) = dom g & dom(f opp) = cod f by Th9; hence thesis by Th17; end; theorem Th19: 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 by Th10; then A3: [opp f,opp g] in dom( the Comp of C ) by A1,CAT_1:40; thus opp (g*f) = (g*f) opp by Def5 .= g*f by Def4 .= ( the Comp of C opp ).[g,f] by A1,CAT_1:41 .= ~(the Comp of C).[g,f] by Lm1 .= ~(the Comp of C).[g opp,f] by Def4 .= ~(the Comp of C).[g opp,f opp] by Def4 .= ~(the Comp of C).[opp g,f opp] by Def5 .= ~(the Comp of C).[opp g,opp f] by Def5 .= (the Comp of C).[opp f,opp g] by A3,FUNCT_4:def 2 .= (opp f)*(opp g) by A1,A2,CAT_1:41; 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 Hom(a,b) <> {} & Hom(b,c) <> {}; then cod f = b & dom g = b & g*f = g*(f qua Morphism of C) by CAT_1:23,def 13; hence thesis by Th17; end; theorem Th21: for a being Object of C holds (id a) opp = id(a opp) proof let a be Object of C; (the Id of C).a = id a & (the Id of C opp).(a opp) = id(a opp) & the Id of C = the Id of C opp & a = a opp & (id a) opp = id a by Def2,Def4,Lm1,CAT_1:def 5; hence thesis; end; theorem Th22: for a being Object of C opp holds opp id a = id opp a proof let a be Object of C opp; thus opp id a = (id a) opp by Def5 .= id a by Def4 .= (the Id of C opp).a by CAT_1:def 5 .= (the Id of C).a by Lm1 .= (the Id of C).(a opp) by Def2 .= (the Id of C).(opp a) by Def3 .= id opp a by CAT_1:def 5; end; theorem for f being Morphism of C holds f opp is monic iff f is epi proof let f be Morphism of C; thus f opp is monic implies f is epi proof assume A1: for f1,f2 being Morphism of C opp st dom f1 = dom f2 & cod f1 = dom(f opp) & cod f2 = dom(f opp) & (f opp)*f1 = (f opp)*f2 holds f1 = f2; let g1,g2 be Morphism of C such that A2: dom g1 = cod f & dom g2 = cod f and A3: cod g1 = cod g2 & g1*f = g2*f; dom(f opp) = cod f & dom(g1 opp) = cod g1 & dom(g2 opp) = cod g2 & cod(g1 opp) = dom g1 & cod(g2 opp) = dom g2 & (g1*f) opp = (f opp)*(g1 opp) & (g2*f) opp = (f opp)*(g2 opp) & g1 opp = g1 & g2 opp = g2 by A2,Def4,Th9,Th17; hence g1 = g2 by A1,A2,A3; end; assume A4: for g1,g2 being Morphism of C st dom g1 = cod f & dom g2 = cod f & cod g1 = cod g2 & g1*f=g2*f holds g1=g2; let f1,f2 be Morphism of C opp such that A5: dom f1 = dom f2 and A6: cod f1 = dom(f opp) & cod f2 = dom(f opp) and A7: (f opp)*f1=(f opp)*f2; set g1 = opp f1, g2 = opp f2; A8: g1 opp = f1 & g2 opp = f2 by Th8; A9: dom g1 = cod(g1 opp) & dom g2 = cod(g2 opp) & dom(f opp) = cod f by Th9; then cod g1 = dom(g1 opp) & cod g2 = dom(g2 opp) & (g1*f) opp = g1*f & (g2*f) opp = g2*f & (f opp)*(g1 opp) = (g1*f) opp & (f opp)*(g2 opp) = (g2*f) opp by A6,A8,Def4,Th9,Th17; hence f1=f2 by A4,A5,A6,A7,A8,A9; end; theorem for f being Morphism of C holds f opp is epi iff f is monic proof let f be Morphism of C; thus f opp is epi implies f is monic proof assume A1: for g1,g2 being Morphism of C opp st dom g1 = cod(f opp) & dom g2 = cod(f opp) & cod g1 = cod g2 & g1*(f opp) = g2*(f opp) holds g1=g2; let f1,f2 be Morphism of C such that A2: dom f1 = dom f2 and A3: cod f1 = dom f and A4: cod f2 = dom f and A5: f*f1 = f*f2; set g1 = f1 opp, g2 = f2 opp; now thus dom g1 = dom f by A3,Th9 .= cod(f opp) by Th9; thus dom g2 = dom f by A4,Th9 .= cod(f opp) by Th9; thus cod g1 = dom f2 by A2,Th9 .= cod g2 by Th9; thus g1*(f opp) = (f*f2) opp by A3,A5,Th17 .= g2*(f opp) by A4,Th17; end; then g1 = g2 by A1; hence f1 = g2 by Def4 .= f2 by Def4; end; assume A6: for f1,f2 being Morphism of C st dom f1 = dom f2 & cod f1 = dom f & cod f2 = dom f & f*f1 = f*f2 holds f1 = f2; let g1,g2 be Morphism of C opp such that A7: dom g1 = cod(f opp) and A8: dom g2 = cod(f opp) and A9: cod g1 = cod g2 and A10: g1*(f opp) = g2*(f opp); set f1 = opp g1, f2 = opp g2; now thus dom f1 = cod g2 by A9,Th10 .= dom f2 by Th10; thus A11: cod f1 = dom g1 by Th10 .= dom f by A7,Th9; thus A12: cod f2 = dom g2 by Th10 .= dom f by A8,Th9; thus f*f1 = (f*f1) opp by Def4 .= (f1 opp)*(f opp) by A11,Th17 .= g2*(f opp) by A10,Th8 .= (f2 opp)*(f opp) by Th8 .= (f*f2) opp by A12,Th17 .= f*f2 by Def4; end; then f1 = f2 by A6; hence g1 = f2 opp by Th8 .= g2 by Th8; end; theorem for f being Morphism of C holds f opp is invertible iff f is invertible proof let f be Morphism of C; A1: (id cod f) opp = id cod f & id dom f = (id dom f) opp & id((cod f) opp) = (id cod f) opp & id((dom f)opp) = (id dom f) opp & (cod f) opp = cod f & (dom f) opp = dom f by Def2,Def4,Th21; thus f opp is invertible implies f is invertible proof given g being Morphism of C opp such that A2: dom g = cod(f opp) & cod g = dom(f opp) and A3: (f opp)*g = id cod(f opp) & g*(f opp) = id dom(f opp); take g' = opp g; A4: g' opp = g by Th8; A5: cod(f opp) = dom f & dom(f opp) = cod f by Th9; hence dom g' = cod f & cod g' = dom f by A2,A4,Th9; then (f*g') opp = (g' opp)*(f opp) & (g'*f) opp = (f opp)*(g' opp) & (f*g') opp = f*g' & (g'*f) opp = g'*f by Def4,Th17; hence f*g' = id cod f & g'*f = id dom f by A1,A3,A5,Th8; end; given g being Morphism of C such that A6: dom g = cod f & cod g = dom f and A7: f*g = id cod f & g*f = id dom f; take g opp; dom(g opp) = cod g & cod(g opp) = dom g by Th9; hence dom(g opp) = cod(f opp) & cod(g opp) = dom(f opp) by A6,Th9; then (f*g) opp = (g opp)*(f opp) & (g*f) opp = (f opp)*(g opp) by Th18; hence (f opp)*(g opp) = id cod(f opp) & (g opp)*(f opp) = id dom(f opp) by A1,A7,Th9; 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; A2: Hom(c,opp b)<>{} by A1,CAT_1:def 16; then consider f being Morphism of C such that A3: f in Hom(c,opp b) by SUBSET_1:10; A4: (opp b) opp = b by Th5; hence A5: Hom(b,c opp)<>{} by A3,Th13; consider f being Morphism of c,opp b such that A6: for g being Morphism of c,opp b holds f=g by A1,CAT_1:def 16; reconsider f' = f opp as Morphism of b,c opp by A2,A4,Th15; take f'; let g be Morphism of b,c opp; opp (c opp) = c by Th4; then opp g is Morphism of c,opp b by A5,Th16; hence f' = (opp g)opp by A6 .= g by Th8; end; assume A7: c opp is terminal; let b be Object of C; A8: Hom(b opp,c opp)<>{} by A7,CAT_1:def 15; then consider f being Morphism of C opp such that A9: f in Hom(b opp,c opp) by SUBSET_1:10; A10: opp (c opp) = c & opp (b opp) = b by Th4; hence A11: Hom(c,b)<>{} by A9,Th14; consider f being Morphism of b opp,c opp such that A12: for g being Morphism of b opp,c opp holds f=g by A7,CAT_1:def 15; reconsider f' = opp f as Morphism of c,b by A8,A10,Th16; take f'; let g be Morphism of c,b; g opp is Morphism of b opp,c opp by A11,Th15; hence f' = opp(g opp) by A12 .= g by Th7; 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; A2: Hom(c opp,b opp)<>{} by A1,CAT_1:def 16; then consider f being Morphism of C opp such that A3: f in Hom(c opp,b opp) by SUBSET_1:10; A4: opp(b opp) = b & opp(c opp) = c by Th4; hence A5: Hom(b,c)<>{} by A3,Th14; consider f being Morphism of c opp,b opp such that A6: for g being Morphism of c opp,b opp holds f = g by A1,CAT_1:def 16; reconsider f' = opp f as Morphism of b,c by A2,A4,Th16; take f'; let g be Morphism of b,c; g opp is Morphism of c opp,b opp by A5,Th15; hence f' = opp(g opp) by A6 .= g by Th7; end; assume A7: c is terminal; let b be Object of C opp; A8: Hom(opp b,c)<>{} by A7,CAT_1:def 15; then consider f being Morphism of C such that A9: f in Hom(opp b, c) by SUBSET_1:10; A10: (opp b) opp = b by Th5; hence A11: Hom(c opp,b)<>{} by A9,Th13; consider f being Morphism of opp b ,c such that A12: for g being Morphism of opp b, c holds f = g by A7,CAT_1:def 15; reconsider f' = f opp as Morphism of c opp,b by A8,A10,Th15; take f'; let g be Morphism of c opp,b; opp g is Morphism of opp b,opp (c opp) by A11,Th16; then opp g is Morphism of opp b,c by Th4; hence f' = (opp g) opp by A12 .= g by Th8; end; :: Contravariant Functors definition let C,B; let S be Function of the Morphisms of C opp,the Morphisms of B; func /*S -> Function of the Morphisms of C,the Morphisms of B means :Def6: 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 Morphisms of C,the Morphisms of B st for f being Morphism of C holds F.f = F(f) from LambdaD; end; uniqueness proof let T1,T2 be Function of the Morphisms of C,the Morphisms 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:113; end; end; theorem for S being Function of the Morphisms of C opp,the Morphisms of B for f being Morphism of C opp holds (/*S).(opp f) = S.f proof let S be Function of the Morphisms of C opp,the Morphisms of B; let f be Morphism of C opp; thus (/*S).(opp f) = S.((opp f) opp) by Def6 .= S.f by Th8; end; Lm2: 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; thus (/*S).(id c) = S.((id c) opp) by Def6 .= S.(id(c opp)) by Th21 .= id((Obj S).(c opp)) by CAT_1:104; end; theorem Th29: 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 Lm2; hence ex d being Object of B st (/*S).(id c) = id d; end; (/*S).(id c) = id((Obj S).(c opp)) by Lm2; hence (Obj /*S).c = (Obj S).(c opp) by A1,CAT_1:102; 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 Th29 .= (Obj S).c by Th5; end; Lm3: 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; thus /*S.(id c) = S.((id c) opp) by Def6 .= S.(id(c opp)) by Th21 .= id((Obj S).(c opp)) by CAT_1:104 .= id((Obj /*S).c) by Th29; end; Lm4: 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 Lm3; hence ex d being Object of B st (/*S).(id c) = id d; end; Lm5: 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; now thus (Obj /*S).(dom f) = (Obj S).((dom f) opp) by Th29 .= (Obj S).(cod (f opp)) by Th11 .= cod(S.(f opp)) by CAT_1:105; thus (Obj /*S).(cod f) = (Obj S).((cod f) opp) by Th29 .= (Obj S).(dom (f opp)) by Th11 .= dom(S.(f opp)) by CAT_1:105; end; hence thesis by Def6; end; Lm6: 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 Lm3 .= id cod (/*S.f) by Lm5; thus (/*S).(id cod f) = id((Obj /*S).(cod f)) by Lm3 .= id dom (/*S.f) by Lm5; end; Lm7: for S being Functor of C opp,B, f,g being Morphism of C st dom g = cod f holds /*S.(g*f) = (/*S.f)*(/*S.g) proof let S be Functor of C opp,B, f,g be Morphism of C such that A1: dom g = cod f; A2: dom(f opp) = cod f & cod (g opp) = dom g by Th9; thus /*S.(g*f) = S.((g*f) opp) by Def6 .= S.((f opp)*(g opp)) by A1,Th17 .= (S.(f opp))*(S.(g opp)) by A1,A2,CAT_1:99 .= (/*S.f)*(S.(g opp)) by Def6 .= (/*S.f)*(/*S.g) by Def6; end; definition let C,D; mode Contravariant_Functor of C,D -> Function of the Morphisms of C,the Morphisms of D means :Def7: ( 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 consider S being Functor of C opp,D; take /*S; thus thesis by Lm4,Lm6,Lm7; end; end; theorem Th31: 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 Def7; hence thesis by CAT_1:102; end; theorem Th32: 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 Def7; hence S.(id c) = id((Obj S).c) by Th31; end; theorem Th33: 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 Def7; hence thesis by Th31; end; theorem Th34: 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 Th33 .= cod (S.g) by Th33; end; theorem Th35: 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 Lm4; thus thesis by Lm6,Lm7; end; theorem Th36: 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 Def7; consider d being Object of D such that A2: S2.(id b) = id d by Def7; take d; thus T.(id c) = id d by A1,A2,FUNCT_2:21; 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:21 .= S2.(id cod (S1.f)) by Def7 .= id dom (S2.((S1.f))) by Def7 .= id dom (T.f) by FUNCT_2:21; thus T.(id cod f) = S2.(S1.(id cod f)) by FUNCT_2:21 .= S2.(id dom (S1.f)) by Def7 .= id cod (S2.((S1.f))) by Def7 .= id cod (T.f) by FUNCT_2:21; end; let f,g be Morphism of C; assume A3: dom g = cod f; then A4: cod (S1.g) = dom(S1.f) by Th34; thus T.(g*f) = S2.(S1.(g*f)) by FUNCT_2:21 .= S2.((S1.f)*(S1.g)) by A3,Def7 .= (S2.(S1.g))*(S2.(S1.f)) by A4,Def7 .= (T.g)*(S2.(S1.f)) by FUNCT_2:21 .= (T.g)*(T.f) by FUNCT_2:21; end; hence thesis by CAT_1:96; end; Lm8: 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; thus (/*S).(id c) = S.((id c) opp) by Def6 .= S.(id(c opp)) by Th21 .= id((Obj S).(c opp)) by Th32; end; theorem Th37: 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 Lm8; hence ex d being Object of B st (/*S).(id c) = id d; end; (/*S).(id c) = id((Obj S).(c opp)) by Lm8; hence (Obj /*S).c = (Obj S).(c opp) by A1,CAT_1:102; 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 Th37 .= (Obj S).c by Th5; end; Lm9: 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; thus /*S.(id c) = S.((id c) opp) by Def6 .= S.(id(c opp)) by Th21 .= id((Obj S).(c opp)) by Th32 .= id((Obj /*S).c) by Th37; end; Lm10: 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; now thus (Obj /*S).(dom f) = (Obj S).((dom f) opp) by Th37 .= (Obj S).(cod (f opp)) by Th11 .= dom(S.(f opp)) by Th33; thus (Obj /*S).(cod f) = (Obj S).((cod f) opp) by Th37 .= (Obj S).(dom (f opp)) by Th11 .= cod(S.(f opp)) by Th33; end; hence thesis by Def6; 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 Lm9; hence ex d being Object of B st (/*S).(id c) = id d; 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 Lm9 .= id dom (/*S.f) by Lm10; thus (/*S).(id cod f) = id((Obj /*S).(cod f)) by Lm9 .= id cod (/*S.f) by Lm10; 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 by Th9; thus /*S.(g*f) = S.((g*f) opp) by Def6 .= S.((f opp)*(g opp)) by A1,Th17 .= (S.(g opp))*(S.(f opp)) by A1,A2,Def7 .= (/*S.g)*(S.(f opp)) by Def6 .= (/*S.g)*(/*S.f) by Def6; end; hence thesis by CAT_1:96; end; :: Dualization functors definition let C,B; let S be Function of the Morphisms of C,the Morphisms of B; func *'S -> Function of the Morphisms of C opp,the Morphisms of B means :Def8: 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 Morphisms of C opp,the Morphisms of B st for f being Morphism of C opp holds F.f = F(f) from LambdaD; end; uniqueness proof let T1,T2 be Function of the Morphisms of C opp,the Morphisms 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:113; end; func S*' -> Function of the Morphisms of C,the Morphisms of B opp means :Def9: 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 Morphisms of C,the Morphisms of B opp st for f being Morphism of C holds F.f = F(f) from LambdaD; end; uniqueness proof let T1,T2 be Function of the Morphisms of C,the Morphisms 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:113; end; end; theorem for S being Function of the Morphisms of C,the Morphisms of B for f being Morphism of C holds (*'S).(f opp) = S.f proof let S be Function of the Morphisms of C,the Morphisms of B; let f be Morphism of C; thus (*'S).(f opp) = S.(opp (f opp)) by Def8 .= S.f by Th7; end; Lm11: 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 Def8 .= S.(id opp c) by Th22 .= id((Obj S).(opp c)) by CAT_1:104; end; theorem Th41: 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 Lm11; let c be Object of C opp; (*'S).(id c) = id((Obj S).(opp c)) by Lm11; hence ex d being Object of B st (*'S).(id c) = id d; end; hence (Obj *'S).c = (Obj S).(opp c) by CAT_1:102; 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 Th41 .= (Obj S).c by Th4; end; Lm12: 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; thus (S*').(id c) = (S.(id c)) opp by Def9 .= (id((Obj S).c)) opp by CAT_1:104 .= id(((Obj S).c) opp) by Th21; end; theorem Th43: 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 Lm12; let c be Object of C; (S*').(id c) = id(((Obj S).c) opp) by Lm12; hence ex d being Object of B opp st (S*').(id c) = id d; end; hence (Obj S*').c = ((Obj S).c) opp by CAT_1:102; end; Lm13: 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 Def8 .= S.(id opp c) by Th22 .= id((Obj S).(opp c)) by Th32; end; theorem Th44: 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 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 (Obj *'S).c = (Obj S).(opp c) by CAT_1:102; 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 Th44 .= (Obj S).c by Th4; end; Lm14: 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; thus (S*').(id c) = (S.(id c)) opp by Def9 .= (id((Obj S).c)) opp by Th32 .= id(((Obj S).c) opp) by Th21; end; theorem Th46: 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 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 (Obj S*').c = ((Obj S).c) opp by CAT_1:102; end; Lm15: for F being Function of the Morphisms of C,the Morphisms of D for f being Morphism of C opp holds *'F*'.f = (F.(opp f)) opp proof let F be Function of the Morphisms of C,the Morphisms of D; let f be Morphism of C opp; thus *'F*'.f = (*'F.f) opp by Def9 .= (F.(opp f)) opp by Def8; end; theorem Th47: for F being Function of the Morphisms of C,the Morphisms of D for f being Morphism of C holds *'F*'.(f opp) = (F.f) opp proof let F be Function of the Morphisms of C,the Morphisms of D; let f be Morphism of C; thus *'F*'.(f opp) = (F.(opp(f opp))) opp by Lm15 .= (F.f) opp by Th7; end; theorem Th48: for S being Function of the Morphisms of C,the Morphisms of D holds /*(*'S) = S proof let S be Function of the Morphisms of C,the Morphisms of D; now let f be Morphism of C; thus /*(*'S).f = (*'S).(f opp) by Def6 .= S.(opp (f opp)) by Def8 .= S.f by Th7; end; hence thesis by FUNCT_2:113; end; theorem for S being Function of the Morphisms of C opp,the Morphisms of D holds *'(/*S) = S proof let S be Function of the Morphisms of C opp,the Morphisms of D; now let f be Morphism of C opp; thus *'(/*S).f = (/*S).(opp f) by Def8 .= S.((opp f) opp) by Def6 .= S.f by Th8; end; hence thesis by FUNCT_2:113; end; theorem for S being Function of the Morphisms of C, the Morphisms of D holds *'S*' = *'(S*') proof let S be Function of the Morphisms of C, the Morphisms of D; now let f be Morphism of C opp; thus *'S*'.f = (*'S.f) opp by Def9 .= (S.(opp f)) opp by Def8 .= (S*').(opp f) by Def9 .= *'(S*').f by Def8; end; hence thesis by FUNCT_2:113; end; theorem for D being strict Category, S being Function of the Morphisms of C, the Morphisms of D holds S*'*' = S proof let D be strict Category; let S be Function of the Morphisms of C, the Morphisms of D; now thus D opp opp = D by Th2; let f be Morphism of C; thus S*'*'.f = (S*'.f) opp by Def9 .= (S.f) opp opp by Def9 .= S.f by Th6; end; hence thesis by FUNCT_2:113; end; theorem for C being strict Category, S being Function of the Morphisms of C, the Morphisms of D holds *'*'S = S proof let C be strict Category; let S be Function of the Morphisms of C, the Morphisms of D; now thus C opp opp = C by Th2; let f be Morphism of C opp opp; thus *'*'S.f = *'S.(opp f) by Def8 .= S.(opp opp f) by Def8 .= S.((opp f) opp) by Def5 .= S.f by Th8; end; hence thesis by FUNCT_2:113; end; Lm16: for S being Function of the Morphisms of C opp,the Morphisms of B for T being Function of the Morphisms of B,the Morphisms of D holds /*(T*S) = T*(/*S) proof let S be Function of the Morphisms of C opp,the Morphisms of B; let T be Function of the Morphisms of B,the Morphisms of D; now let f be Morphism of C; thus /*(T*S).f = (T*S).(f opp) by Def6 .= T.(S.(f opp)) by FUNCT_2:21 .= T.(/*S.f) by Def6 .= (T*(/*S)).f by FUNCT_2:21; end; hence thesis by FUNCT_2:113; end; theorem for S being Function of the Morphisms of C,the Morphisms of B for T being Function of the Morphisms of B,the Morphisms of D holds *'(T*S) = T*(*'S) proof let S be Function of the Morphisms of C,the Morphisms of B; let T be Function of the Morphisms of B,the Morphisms of D; now let f be Morphism of C opp; thus (*'(T*S)).f = (T*S).(opp f) by Def8 .= T.(S.(opp f)) by FUNCT_2:21 .= T.(*'S.f) by Def8 .= (T*(*'S)).f by FUNCT_2:21; end; hence thesis by FUNCT_2:113; end; theorem for S being Function of the Morphisms of C,the Morphisms of B for T being Function of the Morphisms of B,the Morphisms of D holds (T*S)*' = T*'*S proof let S be Function of the Morphisms of C,the Morphisms of B; let T be Function of the Morphisms of B,the Morphisms of D; now let f be Morphism of C; thus (T*S)*'.f = ((T*S).f) opp by Def9 .= (T.(S.f)) opp by FUNCT_2:21 .= T*'.(S.f) by Def9 .= (T*'*S).f by FUNCT_2:21; end; hence thesis by FUNCT_2:113; end; theorem for F1 being Function of the Morphisms of C,the Morphisms of B for F2 being Function of the Morphisms of B,the Morphisms of D holds *'(F2*F1)*' = (*'F2*')*(*'F1*') proof let F1 be Function of the Morphisms of C,the Morphisms of B; let F2 be Function of the Morphisms of B,the Morphisms of D; now let f be Morphism of C opp; thus (*'(F2*F1)*').f = ((F2*F1).(opp f)) opp by Lm15 .= (F2.(F1.(opp f))) opp by FUNCT_2:21 .= (*'F2*').((F1.(opp f)) opp) by Th47 .= (*'F2*').((*'F1*').f) by Lm15 .= ((*'F2*')*(*'F1*')).f by FUNCT_2:21; end; hence thesis by FUNCT_2:113; end; Lm17: 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 Def8 .= S.(id opp c) by Th22 .= id((Obj S).(opp c)) by Th32 .= id((Obj *'S).c) by Th44; end; Lm18: 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; now thus (Obj *'S).(dom f) = (Obj S).(opp dom f) by Th44 .= (Obj S).(cod opp f ) by Th12 .= dom(S.(opp f)) by Th33; thus (Obj *'S).(cod f) = (Obj S).(opp cod f) by Th44 .= (Obj S).(dom opp f) by Th12 .= cod(S.(opp f)) by Th33; end; hence thesis by Def8; end; theorem Th56: 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 Lm17; hence ex d being Object of D st (*'S).(id c) = id d; 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 Lm17 .= id dom (*'S.f) by Lm18; thus (*'S).(id cod f) = id((Obj *'S).(cod f)) by Lm17 .= id cod (*'S.f) by Lm18; 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 by Th10; thus *'S.(g*f) = S.(opp (g*f)) by Def8 .= S.((opp f)*(opp g)) by A1,Th19 .= (S.(opp g))*(S.(opp f)) by A1,A2,Def7 .= (*'S.g)*(S.(opp f)) by Def8 .= (*'S.g)*(*'S.f) by Def8; end; hence *'S is Functor of C opp,D by CAT_1:96; end; Lm19: 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; thus S*'.(id c) = (S.(id c)) opp by Def9 .= (id((Obj S).c)) opp by Th32 .= id(((Obj S).c) opp) by Th21 .= id((Obj S*').c) by Th46; end; Lm20: 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; now thus (Obj S*').(dom f) = ((Obj S).(dom f)) opp by Th46 .= (cod(S.f)) opp by Th33 .= dom((S.f) opp) by Th11; thus (Obj S*').(cod f) = ((Obj S).(cod f)) opp by Th46 .= (dom(S.f)) opp by Th33 .= cod((S.f) opp) by Th11; end; hence thesis by Def9; end; theorem Th57: 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 Lm14; hence ex d being Object of D opp st (S*').(id c) = id d; 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 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; assume A1: dom g = cod f; then A2: dom(S.f) = cod (S.g) by Th34; thus S*'.(g*f) = (S.(g*f)) opp by Def9 .= ((S.f)*(S.g)) opp by A1,Def7 .= ((S.g) opp)*((S.f) opp) by A2,Th17 .= (S*'.g)*((S.f) opp) by Def9 .= (S*'.g)*(S*'.f) by Def9; end; hence S*' is Functor of C,D opp by CAT_1:96; end; Lm21: 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 Def8 .= S.(id opp c) by Th22 .= id((Obj S).(opp c)) by CAT_1:104 .= id((Obj *'S).c) by Th41; end; Lm22: 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; now thus (Obj *'S).(dom f) = (Obj S).(opp dom f) by Th41 .= (Obj S).(cod opp f ) by Th12 .= cod(S.(opp f)) by CAT_1:105; thus (Obj *'S).(cod f) = (Obj S).(opp cod f) by Th41 .= (Obj S).(dom opp f) by Th12 .= dom(S.(opp f)) by CAT_1:105; end; hence thesis by Def8; end; theorem Th58: 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 Lm21; hence ex d being Object of D st (*'S).(id c) = id d; 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 Lm21 .= id cod(*'S.f) by Lm22; thus (*'S).(id cod f) = id((Obj *'S).(cod f)) by Lm21 .= id dom(*'S.f) by Lm22; 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 by Th10; thus *'S.(g*f) = S.(opp (g*f)) by Def8 .= S.((opp f)*(opp g)) by A1,Th19 .= (S.(opp f))*(S.(opp g)) by A1,A2,CAT_1:99 .= (*'S.f)*(S.(opp g)) by Def8 .= (*'S.f)*(*'S.g) by Def8; end; Lm23: 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; thus S*'.(id c) = (S.(id c)) opp by Def9 .= (id((Obj S).c)) opp by CAT_1:104 .= id(((Obj S).c) opp) by Th21 .= id((Obj S*').c) by Th43; end; Lm24: 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; now thus (Obj S*').(dom f) = ((Obj S).(dom f)) opp by Th43 .= (dom(S.f)) opp by CAT_1:105 .= cod((S.f) opp) by Th11; thus (Obj S*').(cod f) = ((Obj S).(cod f)) opp by Th43 .= (cod(S.f)) opp by CAT_1:105 .= dom((S.f) opp) by Th11; end; hence thesis by Def9; end; theorem Th59: 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 Lm23; hence ex d being Object of D opp st (S*').(id c) = id d; 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 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; assume A1: dom g = cod f; then A2: dom(S.g) = cod (S.f) by CAT_1:99; thus S*'.(g*f) = (S.(g*f)) opp by Def9 .= ((S.g)*(S.f)) opp by A1,CAT_1:99 .= ((S.f) opp)*((S.g) opp) by A2,Th17 .= (S*'.f)*((S.g) opp) by Def9 .= (S*'.f)*(S*'.g) by Def9; 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 Th56; then S2*(*'S1) is Functor of C opp,D by CAT_1:110; then /*(S2*(*'S1)) is Contravariant_Functor of C,D by Th35; then S2*(/*(*'S1)) is Contravariant_Functor of C,D by Lm16; hence thesis by Th48; 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 Th58; then S2*(*'S1) is Functor of C opp,D by Th36; then /*(S2*(*'S1)) is Contravariant_Functor of C,D by Th35; then S2*(/*(*'S1)) is Contravariant_Functor of C,D by Lm16; hence thesis by Th48; 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 Th58; hence (Obj *'F*').(c opp) = ((Obj *'F).(c opp)) opp by Th46 .= ((Obj F).(opp (c opp))) opp by Th41 .= ((Obj F).c) opp by Th4; 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 Th56; hence (Obj *'F*').(c opp) = ((Obj *'F).(c opp)) opp by Th43 .= ((Obj F).(opp(c opp))) opp by Th44 .= ((Obj F).c) opp by Th4; 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 Th58; hence thesis by Th57; 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 Th56; hence thesis by Th59; end; :: Duality Functors definition let C; func id* C -> Contravariant_Functor of C,C opp equals :Def10: (id C)*'; coherence by Th59; func *id C -> Contravariant_Functor of C opp,C equals :Def11: *'(id C); coherence by Th58; end; theorem Th66: 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 by Def10 .= ((id C).f) opp by Def9 .= f opp by CAT_1:115; 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 by Def10 .= ((Obj id C).c) opp by Th43 .= c opp by CAT_1:116; end; theorem Th68: 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).f by Def11 .= ((id C).(opp f)) by Def8 .= opp f by CAT_1:115; 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)).c by Def11 .= (Obj id C).(opp c) by Th41 .= opp c by CAT_1:116; end; theorem for S being Function of the Morphisms of C,the Morphisms of D holds *'S = S*(*id C) & S*' = (id* D)*S proof let S be Function of the Morphisms of C,the Morphisms of D; now let f be Morphism of C opp; thus *'S.f = S.(opp f) by Def8 .= S.((*id C).f) by Th68 .= (S*(*id C)).f by FUNCT_2:21; end; hence *'S = S*(*id C) by FUNCT_2:113; now let f be Morphism of C; thus S*'.f = (S.f) opp by Def9 .= (id* D).(S.f) by Th66 .= ((id* D)*S).f by FUNCT_2:21; end; hence thesis by FUNCT_2:113; end;

Back to top