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;