Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Opposite Categories and Contravariant Functors

by
Czeslaw Bylinski

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;
```