Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Opposite Categories and Contravariant Functors

**by****Czeslaw Bylinski**- Received February 13, 1991
- MML identifier: OPPCAT_1

- [ Mizar article, 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; 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; end; :: Opposite Category theorem :: OPPCAT_1:1 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; definition let C; func C opp -> strict Category equals :: OPPCAT_1:def 1 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#); end; theorem :: OPPCAT_1:2 C opp opp = the CatStr of C; definition let C; let c be Object of C; func c opp -> Object of C opp equals :: OPPCAT_1:def 2 c; end; definition let C; let c be Object of C opp; func opp c -> Object of C equals :: OPPCAT_1:def 3 c opp; end; theorem :: OPPCAT_1:3 for c being Object of C holds c opp opp = c; theorem :: OPPCAT_1:4 for c being Object of C holds opp (c opp) = c; theorem :: OPPCAT_1:5 for c being Object of C opp holds (opp c) opp = c; definition let C; let f be Morphism of C; func f opp -> Morphism of C opp equals :: OPPCAT_1:def 4 f; end; definition let C; let f be Morphism of C opp; func opp f -> Morphism of C equals :: OPPCAT_1:def 5 f opp; end; theorem :: OPPCAT_1:6 for f being Morphism of C holds f opp opp = f; theorem :: OPPCAT_1:7 for f being Morphism of C holds opp(f opp) = f; theorem :: OPPCAT_1:8 for f being Morphism of C opp holds (opp f)opp = f; theorem :: OPPCAT_1:9 for f being Morphism of C holds dom(f opp) = cod f & cod(f opp) = dom f; theorem :: OPPCAT_1:10 for f being Morphism of C opp holds dom(opp f) = cod f & cod(opp f) = dom f; theorem :: OPPCAT_1:11 for f being Morphism of C holds (dom f) opp = cod (f opp) & (cod f) opp = dom (f opp); theorem :: OPPCAT_1:12 for f being Morphism of C opp holds opp (dom f) = cod (opp f) & opp (cod f) = dom (opp f); theorem :: OPPCAT_1:13 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); theorem :: OPPCAT_1:14 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); theorem :: OPPCAT_1:15 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; theorem :: OPPCAT_1:16 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; theorem :: OPPCAT_1:17 for f,g being Morphism of C st dom g = cod f holds (g*f) opp = (f opp)*(g opp); theorem :: OPPCAT_1:18 for f,g being Morphism of C st cod(g opp) = dom(f opp) holds (g*f) opp = (f opp)*(g opp); theorem :: OPPCAT_1:19 for f,g being Morphism of C opp st dom g = cod f holds opp (g*f) = (opp f)*(opp g); theorem :: OPPCAT_1:20 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); theorem :: OPPCAT_1:21 for a being Object of C holds (id a) opp = id(a opp); theorem :: OPPCAT_1:22 for a being Object of C opp holds opp id a = id opp a; theorem :: OPPCAT_1:23 for f being Morphism of C holds f opp is monic iff f is epi; theorem :: OPPCAT_1:24 for f being Morphism of C holds f opp is epi iff f is monic; theorem :: OPPCAT_1:25 for f being Morphism of C holds f opp is invertible iff f is invertible; theorem :: OPPCAT_1:26 for c being Object of C holds c is initial iff c opp is terminal; theorem :: OPPCAT_1:27 for c being Object of C holds c opp is initial iff c is terminal; :: 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 :: OPPCAT_1:def 6 for f being Morphism of C holds it.f = S.(f opp); end; theorem :: OPPCAT_1:28 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; theorem :: OPPCAT_1:29 for S being Functor of C opp,B, c being Object of C holds (Obj /*S).c = (Obj S).(c opp); theorem :: OPPCAT_1:30 for S being Functor of C opp,B, c being Object of C opp holds (Obj /*S).(opp c) = (Obj S).c; definition let C,D; mode Contravariant_Functor of C,D -> Function of the Morphisms of C,the Morphisms of D means :: OPPCAT_1:def 7 ( 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)); end; theorem :: OPPCAT_1:31 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; theorem :: OPPCAT_1:32 for S being Contravariant_Functor of C,D,c being Object of C holds S.(id c) = id((Obj S).c); theorem :: OPPCAT_1:33 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); theorem :: OPPCAT_1:34 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); theorem :: OPPCAT_1:35 for S being Functor of C opp,B holds /*S is Contravariant_Functor of C,B; theorem :: OPPCAT_1:36 for S1 being Contravariant_Functor of C,B, S2 being Contravariant_Functor of B,D holds S2*S1 is Functor of C,D; theorem :: OPPCAT_1:37 for S being Contravariant_Functor of C opp,B, c being Object of C holds (Obj /*S).c = (Obj S).(c opp); theorem :: OPPCAT_1:38 for S being Contravariant_Functor of C opp,B, c being Object of C opp holds (Obj /*S).(opp c) = (Obj S).c; theorem :: OPPCAT_1:39 for S being Contravariant_Functor of C opp,B holds /*S is Functor of C,B; :: 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 :: OPPCAT_1:def 8 for f being Morphism of C opp holds it.f = S.(opp f); func S*' -> Function of the Morphisms of C,the Morphisms of B opp means :: OPPCAT_1:def 9 for f being Morphism of C holds it.f = (S.f) opp; end; theorem :: OPPCAT_1:40 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; theorem :: OPPCAT_1:41 for S being Functor of C,B, c being Object of C opp holds (Obj *'S).c = (Obj S).(opp c); theorem :: OPPCAT_1:42 for S being Functor of C,B, c being Object of C holds (Obj *'S).(c opp) = (Obj S).c; theorem :: OPPCAT_1:43 for S being Functor of C,B, c being Object of C holds (Obj S*').c = ((Obj S).c) opp; theorem :: OPPCAT_1:44 for S being Contravariant_Functor of C,B, c being Object of C opp holds (Obj *'S).c = (Obj S).(opp c); theorem :: OPPCAT_1:45 for S being Contravariant_Functor of C,B, c being Object of C holds (Obj *'S).(c opp) = (Obj S).c; theorem :: OPPCAT_1:46 for S being Contravariant_Functor of C,B, c being Object of C holds (Obj S*').c = ((Obj S).c) opp; theorem :: OPPCAT_1:47 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; theorem :: OPPCAT_1:48 for S being Function of the Morphisms of C,the Morphisms of D holds /*(*'S) = S; theorem :: OPPCAT_1:49 for S being Function of the Morphisms of C opp,the Morphisms of D holds *'(/*S) = S; theorem :: OPPCAT_1:50 for S being Function of the Morphisms of C, the Morphisms of D holds *'S*' = *'(S*'); theorem :: OPPCAT_1:51 for D being strict Category, S being Function of the Morphisms of C, the Morphisms of D holds S*'*' = S; theorem :: OPPCAT_1:52 for C being strict Category, S being Function of the Morphisms of C, the Morphisms of D holds *'*'S = S; theorem :: OPPCAT_1:53 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); theorem :: OPPCAT_1:54 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; theorem :: OPPCAT_1:55 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*'); theorem :: OPPCAT_1:56 for S being Contravariant_Functor of C,D holds *'S is Functor of C opp,D; theorem :: OPPCAT_1:57 for S being Contravariant_Functor of C,D holds S*' is Functor of C, D opp; theorem :: OPPCAT_1:58 for S being Functor of C,D holds *'S is Contravariant_Functor of C opp,D; theorem :: OPPCAT_1:59 for S being Functor of C,D holds S*' is Contravariant_Functor of C, D opp; theorem :: OPPCAT_1:60 for S1 being Contravariant_Functor of C,B, S2 being Functor of B,D holds S2*S1 is Contravariant_Functor of C,D; theorem :: OPPCAT_1:61 for S1 being Functor of C,B, S2 being Contravariant_Functor of B,D holds S2*S1 is Contravariant_Functor of C,D; theorem :: OPPCAT_1:62 for F being Functor of C,D, c being Object of C holds (Obj *'F*').(c opp) = ((Obj F).c) opp; theorem :: OPPCAT_1:63 for F being Contravariant_Functor of C,D, c being Object of C holds (Obj *'F*').(c opp) = ((Obj F).c) opp; theorem :: OPPCAT_1:64 for F being Functor of C,D holds *'F*' is Functor of C opp,D opp; theorem :: OPPCAT_1:65 for F being Contravariant_Functor of C,D holds *'F*' is Contravariant_Functor of C opp,D opp; :: Duality Functors definition let C; func id* C -> Contravariant_Functor of C,C opp equals :: OPPCAT_1:def 10 (id C)*'; func *id C -> Contravariant_Functor of C opp,C equals :: OPPCAT_1:def 11 *'(id C); end; theorem :: OPPCAT_1:66 for f being Morphism of C holds (id* C).f = f opp; theorem :: OPPCAT_1:67 for c being Object of C holds (Obj id* C).c = c opp; theorem :: OPPCAT_1:68 for f being Morphism of C opp holds (*id C).f = opp f; theorem :: OPPCAT_1:69 for c being Object of C opp holds (Obj *id C).c = opp c; theorem :: OPPCAT_1:70 for S being Function of the Morphisms of C,the Morphisms of D holds *'S = S*(*id C) & S*' = (id* D)*S;

Back to top