:: by Czes\l aw Byli\'nski

::

:: Received February 13, 1991

:: Copyright (c) 1991-2019 Association of Mizar Users

:: Opposite Category

definition

let C be Category;

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) is non empty non void strict CatStr ;

end;
func C opp -> non empty non void strict 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) #);

coherence CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #);

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) is non empty non void strict CatStr ;

:: deftheorem defines opp OPPCAT_1:def 1 :

for C being Category holds C opp = CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #);

for C being Category holds C opp = CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #);

:: deftheorem defines opp OPPCAT_1:def 2 :

for C being Category

for c being Object of C holds c opp = c;

for C being Category

for c being Object of C holds c opp = c;

registration

let C be Category;

( C opp is Category-like & C opp is transitive & C opp is associative & C opp is reflexive & C opp is with_identities )

end;
cluster C opp -> non empty non void strict Category-like transitive associative reflexive with_identities ;

coherence ( C opp is Category-like & C opp is transitive & C opp is associative & C opp is reflexive & C opp is with_identities )

proof end;

:: deftheorem defines opp OPPCAT_1:def 3 :

for C being Category

for c being Object of (C opp) holds opp c = c opp ;

for C being Category

for c being Object of (C opp) holds opp c = c opp ;

::$CT

:: deftheorem defines opp OPPCAT_1:def 4 :

for C being Category

for f being Morphism of C holds f opp = f;

for C being Category

for f being Morphism of C holds f opp = f;

:: deftheorem defines opp OPPCAT_1:def 5 :

for C being Category

for f being Morphism of (C opp) holds opp f = f opp ;

for C being Category

for f being Morphism of (C opp) holds opp f = f opp ;

definition

let C be Category;

let a, b be Object of C;

assume A1: Hom (a,b) <> {} ;

let f be Morphism of a,b;

coherence

f is Morphism of b opp ,a opp

end;
let a, b be Object of C;

assume A1: Hom (a,b) <> {} ;

let f be Morphism of a,b;

coherence

f is Morphism of b opp ,a opp

proof end;

:: deftheorem Def6 defines opp OPPCAT_1:def 6 :

for C being Category

for a, b being Object of C st Hom (a,b) <> {} holds

for f being Morphism of a,b holds f opp = f;

for C being Category

for a, b being Object of C st Hom (a,b) <> {} holds

for f being Morphism of a,b holds f opp = f;

definition

let C be Category;

let a, b be Object of C;

assume A1: Hom ((a opp),(b opp)) <> {} ;

let f be Morphism of a opp ,b opp ;

coherence

f is Morphism of b,a

end;
let a, b be Object of C;

assume A1: Hom ((a opp),(b opp)) <> {} ;

let f be Morphism of a opp ,b opp ;

coherence

f is Morphism of b,a

proof end;

:: deftheorem Def7 defines opp OPPCAT_1:def 7 :

for C being Category

for a, b being Object of C st Hom ((a opp),(b opp)) <> {} holds

for f being Morphism of a opp ,b opp holds opp f = f;

for C being Category

for a, b being Object of C st Hom ((a opp),(b opp)) <> {} holds

for f being Morphism of a opp ,b opp holds opp f = f;

theorem :: OPPCAT_1:7

for C being Category

for a, b being Object of C st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (f opp) opp = f

for a, b being Object of C st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (f opp) opp = f

proof end;

theorem :: OPPCAT_1:8

for C being Category

for a, b being Object of C st Hom (a,b) <> {} holds

for f being Morphism of a,b holds opp (f opp) = f

for a, b being Object of C st Hom (a,b) <> {} holds

for f being Morphism of a,b holds opp (f opp) = f

proof end;

theorem :: OPPCAT_1:9

theorem Th9: :: OPPCAT_1:10

for C being Category

for a, b being Object of C st Hom (a,b) <> {} holds

for f being Morphism of a,b holds

( dom (f opp) = cod f & cod (f opp) = dom f )

for a, b being Object of C st Hom (a,b) <> {} holds

for f being Morphism of a,b holds

( dom (f opp) = cod f & cod (f opp) = dom f )

proof end;

theorem :: OPPCAT_1:11

theorem :: OPPCAT_1:12

theorem :: OPPCAT_1:13

::$CT

theorem Th13: :: OPPCAT_1:15

for C being Category

for a, b being Object of (C opp)

for f being Morphism of a,b st Hom (a,b) <> {} holds

opp f is Morphism of opp b, opp a

for a, b being Object of (C opp)

for f being Morphism of a,b st Hom (a,b) <> {} holds

opp f is Morphism of opp b, opp a

proof end;

theorem Th14: :: OPPCAT_1:16

for C being Category

for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)

for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)

proof end;

theorem :: OPPCAT_1:17

for C being Category

for a, b, c being Object of C st Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)

for a, b, c being Object of C st Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)

proof end;

theorem Th16: :: OPPCAT_1:18

for C being Category

for f, g being Morphism of (C opp) st dom g = cod f holds

opp (g (*) f) = (opp f) (*) (opp g)

for f, g being Morphism of (C opp) st dom g = cod f holds

opp (g (*) f) = (opp f) (*) (opp g)

proof end;

theorem :: OPPCAT_1:19

for C being Category

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds

(g * f) opp = (f opp) (*) (g opp)

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds

(g * f) opp = (f opp) (*) (g opp)

proof end;

Lm1: for C being Category

for a being Object of C

for b being Object of (C opp) holds

( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) )

proof end;

Lm2: for C being Category

for a being Object of C holds id a = id (a opp)

proof end;

Lm3: for C being Category

for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = (f opp) * (g opp)

proof end;

theorem :: OPPCAT_1:22

for C being Category

for a, b being Object of C

for f being Morphism of a,b holds

( f opp is monic iff f is epi )

for a, b being Object of C

for f being Morphism of a,b holds

( f opp is monic iff f is epi )

proof end;

theorem :: OPPCAT_1:23

for C being Category

for b, c being Object of C st Hom (b,c) <> {} holds

for f being Morphism of b,c holds

( f opp is epi iff f is monic )

for b, c being Object of C st Hom (b,c) <> {} holds

for f being Morphism of b,c holds

( f opp is epi iff f is monic )

proof end;

theorem :: OPPCAT_1:24

for C being Category

for a, b being Object of C

for f being Morphism of a,b holds

( f opp is invertible iff f is invertible )

for a, b being Object of C

for f being Morphism of a,b holds

( f opp is invertible iff f is invertible )

proof end;

:: Contravariant Functors

definition

let C, B be Category;

let S be Function of the carrier' of (C opp), the carrier' of B;

ex b_{1} being Function of the carrier' of C, the carrier' of B st

for f being Morphism of C holds b_{1} . f = S . (f opp)

for b_{1}, b_{2} being Function of the carrier' of C, the carrier' of B st ( for f being Morphism of C holds b_{1} . f = S . (f opp) ) & ( for f being Morphism of C holds b_{2} . f = S . (f opp) ) holds

b_{1} = b_{2}

end;
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 :Def8: :: OPPCAT_1:def 8

for f being Morphism of C holds it . f = S . (f opp);

existence for f being Morphism of C holds it . f = S . (f opp);

ex b

for f being Morphism of C holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines /* OPPCAT_1:def 8 :

for C, B being Category

for S being Function of the carrier' of (C opp), the carrier' of B

for b_{4} being Function of the carrier' of C, the carrier' of B holds

( b_{4} = /* S iff for f being Morphism of C holds b_{4} . f = S . (f opp) );

for C, B being Category

for S being Function of the carrier' of (C opp), the carrier' of B

for b

( b

theorem :: OPPCAT_1:27

for B, C being Category

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

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

proof end;

Lm4: for B, C being Category

for S being Functor of C opp ,B

for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp))

proof end;

theorem Th26: :: OPPCAT_1:28

for B, C being Category

for S being Functor of C opp ,B

for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp)

for S being Functor of C opp ,B

for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp)

proof end;

theorem :: OPPCAT_1:29

for B, C being Category

for S being Functor of C opp ,B

for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c

for S being Functor of C opp ,B

for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c

proof end;

Lm5: for B, C being Category

for S being Functor of C opp ,B

for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)

proof end;

Lm6: now :: thesis: for C, B being Category

for S being Functor of C opp ,B

for c being Object of C ex d being Object of B st (/* S) . (id c) = id d

for S being Functor of C opp ,B

for c being Object of C ex d being Object of B st (/* S) . (id c) = id d

let C, B be Category; :: thesis: for S being Functor of C opp ,B

for c being Object of C ex d being Object of B st (/* S) . (id c) = id d

let S be Functor of C opp ,B; :: thesis: for c being Object of C ex d being Object of B st (/* S) . (id c) = id d

let c be Object of C; :: thesis: ex d being Object of B st (/* S) . (id c) = id d

(/* S) . (id c) = id ((Obj (/* S)) . c) by Lm5;

hence ex d being Object of B st (/* S) . (id c) = id d ; :: thesis: verum

end;
for c being Object of C ex d being Object of B st (/* S) . (id c) = id d

let S be Functor of C opp ,B; :: thesis: for c being Object of C ex d being Object of B st (/* S) . (id c) = id d

let c be Object of C; :: thesis: ex d being Object of B st (/* S) . (id c) = id d

(/* S) . (id c) = id ((Obj (/* S)) . c) by Lm5;

hence ex d being Object of B st (/* S) . (id c) = id d ; :: thesis: verum

Lm7: for B, C being Category

for S being Functor of C opp ,B

for f being Morphism of C holds

( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) )

proof end;

Lm8: now :: thesis: for C, B being Category

for S being Functor of C opp ,B

for f being Morphism of C holds

( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )

for S being Functor of C opp ,B

for f being Morphism of C holds

( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )

let C, B be Category; :: thesis: for S being Functor of C opp ,B

for f being Morphism of C holds

( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )

let S be Functor of C opp ,B; :: thesis: for f being Morphism of C holds

( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )

let f be Morphism of C; :: thesis: ( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )

thus (/* S) . (id (dom f)) = id ((Obj (/* S)) . (dom f)) by Lm5

.= id (cod ((/* S) . f)) by Lm7 ; :: thesis: (/* S) . (id (cod f)) = id (dom ((/* S) . f))

thus (/* S) . (id (cod f)) = id ((Obj (/* S)) . (cod f)) by Lm5

.= id (dom ((/* S) . f)) by Lm7 ; :: thesis: verum

end;
for f being Morphism of C holds

( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )

let S be Functor of C opp ,B; :: thesis: for f being Morphism of C holds

( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )

let f be Morphism of C; :: thesis: ( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )

thus (/* S) . (id (dom f)) = id ((Obj (/* S)) . (dom f)) by Lm5

.= id (cod ((/* S) . f)) by Lm7 ; :: thesis: (/* S) . (id (cod f)) = id (dom ((/* S) . f))

thus (/* S) . (id (cod f)) = id ((Obj (/* S)) . (cod f)) by Lm5

.= id (dom ((/* S) . f)) by Lm7 ; :: thesis: verum

Lm9: for B, C being Category

for S being Functor of C opp ,B

for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

proof end;

definition

let C, D be Category;

ex b_{1} being Function of the carrier' of C, the carrier' of D st

( ( for c being Object of C ex d being Object of D st b_{1} . (id c) = id d ) & ( for f being Morphism of C holds

( b_{1} . (id (dom f)) = id (cod (b_{1} . f)) & b_{1} . (id (cod f)) = id (dom (b_{1} . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

b_{1} . (g (*) f) = (b_{1} . f) (*) (b_{1} . g) ) )

end;
mode Contravariant_Functor of C,D -> Function of the carrier' of C, the carrier' of D means :Def9: :: 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) ) );

existence ( ( 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) ) );

ex b

( ( for c being Object of C ex d being Object of D st b

( b

b

proof end;

:: deftheorem Def9 defines Contravariant_Functor OPPCAT_1:def 9 :

for C, D being Category

for b_{3} being Function of the carrier' of C, the carrier' of D holds

( b_{3} is Contravariant_Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b_{3} . (id c) = id d ) & ( for f being Morphism of C holds

( b_{3} . (id (dom f)) = id (cod (b_{3} . f)) & b_{3} . (id (cod f)) = id (dom (b_{3} . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

b_{3} . (g (*) f) = (b_{3} . f) (*) (b_{3} . g) ) ) );

for C, D being Category

for b

( b

( b

b

theorem Th28: :: OPPCAT_1:30

for C, D being Category

for S being Contravariant_Functor of C,D

for c being Object of C

for d being Object of D st S . (id c) = id d holds

(Obj S) . c = d

for S being Contravariant_Functor of C,D

for c being Object of C

for d being Object of D st S . (id c) = id d holds

(Obj S) . c = d

proof end;

theorem Th29: :: OPPCAT_1:31

for C, D being Category

for S being Contravariant_Functor of C,D

for c being Object of C holds S . (id c) = id ((Obj S) . c)

for S being Contravariant_Functor of C,D

for c being Object of C holds S . (id c) = id ((Obj S) . c)

proof end;

theorem Th30: :: OPPCAT_1:32

for C, D being Category

for S being Contravariant_Functor of C,D

for f being Morphism of C holds

( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) )

for S being Contravariant_Functor of C,D

for f being Morphism of C holds

( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) )

proof end;

theorem Th31: :: OPPCAT_1:33

for C, D being Category

for S being Contravariant_Functor of C,D

for f, g being Morphism of C st dom g = cod f holds

dom (S . f) = cod (S . g)

for S being Contravariant_Functor of C,D

for f, g being Morphism of C st dom g = cod f holds

dom (S . f) = cod (S . g)

proof end;

theorem Th33: :: OPPCAT_1:35

for B, C, D being Category

for S1 being Contravariant_Functor of C,B

for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D

for S1 being Contravariant_Functor of C,B

for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D

proof end;

Lm10: for B, C being Category

for S being Contravariant_Functor of C opp ,B

for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp))

proof end;

theorem Th34: :: OPPCAT_1:36

for B, C being Category

for S being Contravariant_Functor of C opp ,B

for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp)

for S being Contravariant_Functor of C opp ,B

for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp)

proof end;

theorem :: OPPCAT_1:37

for B, C being Category

for S being Contravariant_Functor of C opp ,B

for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c

for S being Contravariant_Functor of C opp ,B

for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c

proof end;

Lm11: for B, C being Category

for S being Contravariant_Functor of C opp ,B

for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)

proof end;

Lm12: for B, C being Category

for S being Contravariant_Functor of C opp ,B

for f being Morphism of C holds

( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) )

proof end;

:: Dualization functors

definition

let C, B be Category;

let S be Function of the carrier' of C, the carrier' of B;

ex b_{1} being Function of the carrier' of (C opp), the carrier' of B st

for f being Morphism of (C opp) holds b_{1} . f = S . (opp f)

for b_{1}, b_{2} being Function of the carrier' of (C opp), the carrier' of B st ( for f being Morphism of (C opp) holds b_{1} . f = S . (opp f) ) & ( for f being Morphism of (C opp) holds b_{2} . f = S . (opp f) ) holds

b_{1} = b_{2}

ex b_{1} being Function of the carrier' of C, the carrier' of (B opp) st

for f being Morphism of C holds b_{1} . f = (S . f) opp

for b_{1}, b_{2} being Function of the carrier' of C, the carrier' of (B opp) st ( for f being Morphism of C holds b_{1} . f = (S . f) opp ) & ( for f being Morphism of C holds b_{2} . f = (S . f) opp ) holds

b_{1} = b_{2}

end;
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 :Def10: :: OPPCAT_1:def 10

for f being Morphism of (C opp) holds it . f = S . (opp f);

existence for f being Morphism of (C opp) holds it . f = S . (opp f);

ex b

for f being Morphism of (C opp) holds b

proof end;

uniqueness for b

b

proof end;

func S *' -> Function of the carrier' of C, the carrier' of (B opp) means :Def11: :: OPPCAT_1:def 11

for f being Morphism of C holds it . f = (S . f) opp ;

existence for f being Morphism of C holds it . f = (S . f) opp ;

ex b

for f being Morphism of C holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines *' OPPCAT_1:def 10 :

for C, B being Category

for S being Function of the carrier' of C, the carrier' of B

for b_{4} being Function of the carrier' of (C opp), the carrier' of B holds

( b_{4} = *' S iff for f being Morphism of (C opp) holds b_{4} . f = S . (opp f) );

for C, B being Category

for S being Function of the carrier' of C, the carrier' of B

for b

( b

:: deftheorem Def11 defines *' OPPCAT_1:def 11 :

for C, B being Category

for S being Function of the carrier' of C, the carrier' of B

for b_{4} being Function of the carrier' of C, the carrier' of (B opp) holds

( b_{4} = S *' iff for f being Morphism of C holds b_{4} . f = (S . f) opp );

for C, B being Category

for S being Function of the carrier' of C, the carrier' of B

for b

( b

theorem :: OPPCAT_1:39

for B, C being Category

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

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

proof end;

Lm13: for B, C being Category

for S being Functor of C,B

for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c))

proof end;

theorem Th38: :: OPPCAT_1:40

for B, C being Category

for S being Functor of C,B

for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c)

for S being Functor of C,B

for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c)

proof end;

theorem :: OPPCAT_1:41

for B, C being Category

for S being Functor of C,B

for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c

for S being Functor of C,B

for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c

proof end;

Lm14: for B, C being Category

for S being Functor of C,B

for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp)

proof end;

theorem Th40: :: OPPCAT_1:42

for B, C being Category

for S being Functor of C,B

for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp

for S being Functor of C,B

for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp

proof end;

Lm15: for B, C being Category

for S being Contravariant_Functor of C,B

for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c))

proof end;

theorem Th41: :: OPPCAT_1:43

for B, C being Category

for S being Contravariant_Functor of C,B

for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c)

for S being Contravariant_Functor of C,B

for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c)

proof end;

theorem :: OPPCAT_1:44

for B, C being Category

for S being Contravariant_Functor of C,B

for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c

for S being Contravariant_Functor of C,B

for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c

proof end;

Lm16: for B, C being Category

for S being Contravariant_Functor of C,B

for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp)

proof end;

theorem Th43: :: OPPCAT_1:45

for B, C being Category

for S being Contravariant_Functor of C,B

for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp

for S being Contravariant_Functor of C,B

for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp

proof end;

Lm17: for C, D being Category

for F being Function of the carrier' of C, the carrier' of D

for f being Morphism of (C opp) holds ((*' F) *') . f = (F . (opp f)) opp

proof end;

theorem Th44: :: OPPCAT_1:46

for C, D being Category

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

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

proof end;

theorem Th45: :: OPPCAT_1:47

for C, D being Category

for S being Function of the carrier' of C, the carrier' of D holds /* (*' S) = S

for S being Function of the carrier' of C, the carrier' of D holds /* (*' S) = S

proof end;

theorem :: OPPCAT_1:48

for C, D being Category

for S being Function of the carrier' of (C opp), the carrier' of D holds *' (/* S) = S

for S being Function of the carrier' of (C opp), the carrier' of D holds *' (/* S) = S

proof end;

theorem :: OPPCAT_1:49

for C, D being Category

for S being Function of the carrier' of C, the carrier' of D holds (*' S) *' = *' (S *')

for S being Function of the carrier' of C, the carrier' of D holds (*' S) *' = *' (S *')

proof end;

theorem :: OPPCAT_1:50

for C being Category

for D being strict Category

for S being Function of the carrier' of C, the carrier' of D holds (S *') *' = S

for D being strict Category

for S being Function of the carrier' of C, the carrier' of D holds (S *') *' = S

proof end;

theorem :: OPPCAT_1:51

for D being Category

for C being strict Category

for S being Function of the carrier' of C, the carrier' of D holds *' (*' S) = S

for C being strict Category

for S being Function of the carrier' of C, the carrier' of D holds *' (*' S) = S

proof end;

Lm18: for B, C, D being Category

for S being Function of the carrier' of (C opp), the carrier' of B

for T being Function of the carrier' of B, the carrier' of D holds /* (T * S) = T * (/* S)

proof end;

theorem :: OPPCAT_1:52

for B, C, D being Category

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)

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)

proof end;

theorem :: OPPCAT_1:53

for B, C, D being Category

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

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

proof end;

theorem :: OPPCAT_1:54

for B, C, D being Category

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) *')

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) *')

proof end;

Lm19: for B, C being Category

for S being Contravariant_Functor of C,B

for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c)

proof end;

Lm20: for B, C being Category

for S being Contravariant_Functor of C,B

for f being Morphism of (C opp) holds

( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) )

proof end;

Lm21: for B, C being Category

for S being Contravariant_Functor of C,B

for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c)

proof end;

Lm22: for B, C being Category

for S being Contravariant_Functor of C,B

for f being Morphism of C holds

( (Obj (S *')) . (dom f) = dom ((S *') . f) & (Obj (S *')) . (cod f) = cod ((S *') . f) )

proof end;

Lm23: for B, C being Category

for S being Functor of C,B

for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c)

proof end;

Lm24: for B, C being Category

for S being Functor of C,B

for f being Morphism of (C opp) holds

( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) )

proof end;

Lm25: for B, C being Category

for S being Functor of C,B

for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c)

proof end;

Lm26: for B, C being Category

for S being Functor of C,B

for f being Morphism of C holds

( (Obj (S *')) . (dom f) = cod ((S *') . f) & (Obj (S *')) . (cod f) = dom ((S *') . f) )

proof end;

theorem :: OPPCAT_1:59

for B, C, D being Category

for S1 being Contravariant_Functor of C,B

for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D

for S1 being Contravariant_Functor of C,B

for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D

proof end;

theorem :: OPPCAT_1:60

for B, C, D being Category

for S1 being Functor of C,B

for S2 being Contravariant_Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D

for S1 being Functor of C,B

for S2 being Contravariant_Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D

proof end;

theorem :: OPPCAT_1:61

for C, D being Category

for F being Functor of C,D

for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp

for F being Functor of C,D

for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp

proof end;

theorem :: OPPCAT_1:62

for C, D being Category

for F being Contravariant_Functor of C,D

for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp

for F being Contravariant_Functor of C,D

for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp

proof end;

theorem :: OPPCAT_1:64

for C, D being Category

for F being Contravariant_Functor of C,D holds (*' F) *' is Contravariant_Functor of C opp ,D opp

for F being Contravariant_Functor of C,D holds (*' F) *' is Contravariant_Functor of C opp ,D opp

proof end;

:: Duality Functors

definition

let C be Category;

coherence

(id C) *' is Contravariant_Functor of C,C opp by Th56;

coherence

*' (id C) is Contravariant_Functor of C opp ,C by Th55;

end;
coherence

(id C) *' is Contravariant_Functor of C,C opp by Th56;

coherence

*' (id C) is Contravariant_Functor of C opp ,C by Th55;

theorem :: OPPCAT_1:69

for C, D being Category

for S being Function of the carrier' of C, the carrier' of D holds

( *' S = S * (*id C) & S *' = (id* D) * S )

for S being Function of the carrier' of C, the carrier' of D holds

( *' S = S * (*id C) & S *' = (id* D) * S )

proof end;

theorem :: OPPCAT_1:70