:: Opposite Categories and Contravariant Functors :: by Czes\l aw Byli\'nski :: :: Received February 13, 1991 :: Copyright (c) 1991-2021 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; begin reserve B,C,D for Category; :: Opposite Category definition let C; func C opp -> strict non empty non void CatStr equals :: OPPCAT_1:def 1 CatStr (#the carrier of C, the carrier' of C, the Target of C, the Source of C, ~the Comp of C#); end; definition let C; let c be Object of C; func c opp -> Object of C opp equals :: OPPCAT_1:def 2 c; end; registration let C; cluster C opp -> Category-like transitive associative reflexive with_identities; 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; ::$CT theorem :: OPPCAT_1:2 for c being Object of C holds c opp opp = c; theorem :: OPPCAT_1:3 for c being Object of C holds opp (c opp) = c; theorem :: OPPCAT_1:4 for c being Object of C opp holds (opp c) opp = c; theorem :: OPPCAT_1:5 for a,b being Object of C holds Hom(a,b) = Hom(b opp,a opp); theorem :: OPPCAT_1:6 for a,b being Object of C opp holds Hom(a,b) = Hom(opp b,opp a); 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; definition let C; let a,b be Object of C such that Hom(a,b) <> {}; let f be Morphism of a,b; func f opp -> Morphism of b opp, a opp equals :: OPPCAT_1:def 6 f; end; definition let C; let a,b be Object of C such that Hom(a opp,b opp) <> {}; let f be Morphism of a opp, b opp; func opp f -> Morphism of b, a equals :: OPPCAT_1:def 7 f; end; theorem :: OPPCAT_1:7 for a,b being Object of C st Hom(a,b)<>{} for f being Morphism of a,b holds f opp opp = f; theorem :: OPPCAT_1:8 for a,b being Object of C st Hom(a,b)<>{} for f being Morphism of a,b holds opp(f opp) = f; theorem :: OPPCAT_1:9 for a,b being Object of C opp for f being Morphism of a,b holds (opp f)opp = f; theorem :: OPPCAT_1:10 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; theorem :: OPPCAT_1:11 for a,b being Object of C opp for f being Morphism of a,b holds dom(opp f) = cod f & cod(opp f) = dom f; theorem :: OPPCAT_1:12 for 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); theorem :: OPPCAT_1:13 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 :: OPPCAT_1:15 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:16 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); theorem :: OPPCAT_1:17 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); theorem :: OPPCAT_1:18 for f,g being Morphism of C opp st dom g = cod f holds opp (g(*)f) = (opp f)(*)(opp g); theorem :: OPPCAT_1:19 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:20 for a being Object of C holds (id a) opp = id(a opp); theorem :: OPPCAT_1:21 for a being Object of C opp holds opp id a = id opp a; theorem :: OPPCAT_1:22 for a,b being Object of C for f being Morphism of a,b holds f opp is monic iff f is epi; theorem :: OPPCAT_1:23 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; theorem :: OPPCAT_1:24 for a,b being Object of C for f being Morphism of a,b holds f opp is invertible iff f is invertible; theorem :: OPPCAT_1:25 for c being Object of C holds c is initial iff c opp is terminal; theorem :: OPPCAT_1:26 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 carrier' of C opp,the carrier' of B; func /*S -> Function of the carrier' of C,the carrier' of B means :: OPPCAT_1:def 8 for f being Morphism of C holds it.f = S.(f opp); end; theorem :: OPPCAT_1:27 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; theorem :: OPPCAT_1:28 for S being Functor of C opp,B, c being Object of C holds (Obj /*S).c = (Obj S).(c opp); theorem :: OPPCAT_1:29 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 carrier' of C,the carrier' of D means :: OPPCAT_1:def 9 ( for c being Object of C ex d being Object of D st it.(id c) = id d ) & ( for f being Morphism of C holds it.(id dom f) = id cod (it.f) & it.(id cod f) = id dom (it.f) ) & for f,g being Morphism of C st dom g = cod f holds it.(g(*)f) = (it.f)(*)(it.g); end; theorem :: OPPCAT_1:30 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:31 for S being Contravariant_Functor of C,D,c being Object of C holds S.(id c) = id((Obj S).c); theorem :: OPPCAT_1:32 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:33 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:34 for S being Functor of C opp,B holds /*S is Contravariant_Functor of C,B; theorem :: OPPCAT_1:35 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:36 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:37 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:38 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 carrier' of C,the carrier' of B; func *'S -> Function of the carrier' of C opp,the carrier' of B means :: OPPCAT_1:def 10 for f being Morphism of C opp holds it.f = S.(opp f); func S*' -> Function of the carrier' of C,the carrier' of B opp means :: OPPCAT_1:def 11 for f being Morphism of C holds it.f = (S.f) opp; end; theorem :: OPPCAT_1:39 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; theorem :: OPPCAT_1:40 for S being Functor of C,B, c being Object of C opp holds (Obj *'S).c = (Obj S).(opp c); theorem :: OPPCAT_1:41 for S being Functor of C,B, c being Object of C holds (Obj *'S).(c opp ) = (Obj S).c; theorem :: OPPCAT_1:42 for S being Functor of C,B, c being Object of C holds (Obj S*'). c = ((Obj S).c) opp; theorem :: OPPCAT_1:43 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:44 for S being Contravariant_Functor of C,B, c being Object of C holds ( Obj *'S).(c opp) = (Obj S).c; theorem :: OPPCAT_1:45 for S being Contravariant_Functor of C,B, c being Object of C holds (Obj S*').c = ((Obj S).c) opp; theorem :: OPPCAT_1:46 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; theorem :: OPPCAT_1:47 for S being Function of the carrier' of C,the carrier' of D holds /*(*'S) = S ; theorem :: OPPCAT_1:48 for S being Function of the carrier' of C opp,the carrier' of D holds *'(/*S) = S; theorem :: OPPCAT_1:49 for S being Function of the carrier' of C, the carrier' of D holds *'S *' = *'(S*'); theorem :: OPPCAT_1:50 for D being strict Category, S being Function of the carrier' of C, the carrier' of D holds S*'*' = S; theorem :: OPPCAT_1:51 for C being strict Category, S being Function of the carrier' of C, the carrier' of D holds *'*'S = S; theorem :: OPPCAT_1:52 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) ; theorem :: OPPCAT_1:53 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; theorem :: OPPCAT_1:54 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*'); theorem :: OPPCAT_1:55 for S being Contravariant_Functor of C,D holds *'S is Functor of C opp,D; theorem :: OPPCAT_1:56 for S being Contravariant_Functor of C,D holds S*' is Functor of C, D opp; theorem :: OPPCAT_1:57 for S being Functor of C,D holds *'S is Contravariant_Functor of C opp,D; theorem :: OPPCAT_1:58 for S being Functor of C,D holds S*' is Contravariant_Functor of C, D opp; theorem :: OPPCAT_1:59 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:60 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:61 for F being Functor of C,D, c being Object of C holds (Obj *'F*').(c opp) = ((Obj F).c) opp; theorem :: OPPCAT_1:62 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:63 for F being Functor of C,D holds *'F*' is Functor of C opp,D opp; theorem :: OPPCAT_1:64 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 12 (id C)*'; func *id C -> Contravariant_Functor of C opp,C equals :: OPPCAT_1:def 13 *'(id C); end; theorem :: OPPCAT_1:65 for f being Morphism of C holds (id* C).f = f opp; theorem :: OPPCAT_1:66 for c being Object of C holds (Obj id* C).c = c opp; theorem :: OPPCAT_1:67 for f being Morphism of C opp holds (*id C).f = opp f; theorem :: OPPCAT_1:68 for c being Object of C opp holds (Obj *id C).c = opp c; theorem :: OPPCAT_1:69 for S being Function of the carrier' of C,the carrier' of D holds *'S = S*(*id C) & S*' = (id* D)*S; theorem :: OPPCAT_1:70 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); theorem :: OPPCAT_1:71 for a being Object of C holds id a = id(a opp); theorem :: OPPCAT_1:72 for a being Object of C opp holds id a = id opp a;