begin
theorem Th1:
definition
let C be
Category;
func C opp -> strict Category equals
CatStr(# the
carrier of
C,the
carrier' of
C,the
Target of
C,the
Source of
C,
(~ the Comp of C),the
Id of
C #);
coherence
CatStr(# the carrier of C,the carrier' of C,the Target of C,the Source of C,(~ the Comp of C),the Id of C #) is strict Category
by Th1;
end;
:: deftheorem defines opp OPPCAT_1:def 1 :
:: deftheorem defines opp OPPCAT_1:def 2 :
:: deftheorem defines opp OPPCAT_1:def 3 :
theorem
canceled;
theorem
theorem
theorem
:: deftheorem defines opp OPPCAT_1:def 4 :
:: deftheorem defines opp OPPCAT_1:def 5 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def6 defines /* OPPCAT_1:def 6 :
theorem
Lm1:
for C, B being Category
for S being Functor of C opp ,B
for c being Object of holds (/* S) . (id c) = id ((Obj S) . (c opp ))
theorem Th29:
theorem
Lm2:
for C, B being Category
for S being Functor of C opp ,B
for c being Object of holds (/* S) . (id c) = id ((Obj (/* S)) . c)
Lm4:
for C, B being Category
for S being Functor of C opp ,B
for f being Morphism of holds
( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) )
Lm6:
for C, B being Category
for S being Functor of C opp ,B
for f, g being Morphism of st dom g = cod f holds
(/* S) . (g * f) = ((/* S) . f) * ((/* S) . g)
:: deftheorem Def7 defines Contravariant_Functor OPPCAT_1:def 7 :
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
Lm7:
for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of holds (/* S) . (id c) = id ((Obj S) . (c opp ))
theorem Th37:
theorem
Lm8:
for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of holds (/* S) . (id c) = id ((Obj (/* S)) . c)
Lm9:
for C, B being Category
for S being Contravariant_Functor of C opp ,B
for f being Morphism of holds
( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) )
theorem
definition
let C,
B be
Category;
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 :
Def8:
for
f being
Morphism of holds
it . f = S . (opp f);
existence
ex b1 being Function of the carrier' of (C opp ),the carrier' of B st
for f being Morphism of holds b1 . f = S . (opp f)
uniqueness
for b1, b2 being Function of the carrier' of (C opp ),the carrier' of B st ( for f being Morphism of holds b1 . f = S . (opp f) ) & ( for f being Morphism of holds b2 . f = S . (opp f) ) holds
b1 = b2
func S *' -> Function of the
carrier' of
C,the
carrier' of
(B opp ) means :
Def9:
for
f being
Morphism of holds
it . f = (S . f) opp ;
existence
ex b1 being Function of the carrier' of C,the carrier' of (B opp ) st
for f being Morphism of holds b1 . f = (S . f) opp
uniqueness
for b1, b2 being Function of the carrier' of C,the carrier' of (B opp ) st ( for f being Morphism of holds b1 . f = (S . f) opp ) & ( for f being Morphism of holds b2 . f = (S . f) opp ) holds
b1 = b2
end;
:: deftheorem Def8 defines *' OPPCAT_1:def 8 :
:: deftheorem Def9 defines *' OPPCAT_1:def 9 :
theorem
Lm10:
for C, B being Category
for S being Functor of C,B
for c being Object of holds (*' S) . (id c) = id ((Obj S) . (opp c))
theorem Th41:
theorem
Lm11:
for C, B being Category
for S being Functor of C,B
for c being Object of holds (S *' ) . (id c) = id (((Obj S) . c) opp )
theorem Th43:
Lm12:
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of holds (*' S) . (id c) = id ((Obj S) . (opp c))
theorem Th44:
theorem
Lm13:
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of holds (S *' ) . (id c) = id (((Obj S) . c) opp )
theorem Th46:
Lm14:
for C, D being Category
for F being Function of the carrier' of C,the carrier' of D
for f being Morphism of holds ((*' F) *' ) . f = (F . (opp f)) opp
theorem Th47:
theorem Th48:
theorem
theorem
theorem
theorem
Lm15:
for C, B, 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)
theorem
theorem
theorem
Lm16:
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of holds (*' S) . (id c) = id ((Obj (*' S)) . c)
Lm17:
for C, B being Category
for S being Contravariant_Functor of C,B
for f being Morphism of holds
( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) )
theorem Th56:
Lm18:
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of holds (S *' ) . (id c) = id ((Obj (S *' )) . c)
Lm19:
for C, B being Category
for S being Contravariant_Functor of C,B
for f being Morphism of holds
( (Obj (S *' )) . (dom f) = dom ((S *' ) . f) & (Obj (S *' )) . (cod f) = cod ((S *' ) . f) )
theorem Th57:
Lm20:
for C, B being Category
for S being Functor of C,B
for c being Object of holds (*' S) . (id c) = id ((Obj (*' S)) . c)
Lm21:
for C, B being Category
for S being Functor of C,B
for f being Morphism of holds
( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) )
theorem Th58:
Lm22:
for C, B being Category
for S being Functor of C,B
for c being Object of holds (S *' ) . (id c) = id ((Obj (S *' )) . c)
Lm23:
for C, B being Category
for S being Functor of C,B
for f being Morphism of holds
( (Obj (S *' )) . (dom f) = cod ((S *' ) . f) & (Obj (S *' )) . (cod f) = dom ((S *' ) . f) )
theorem Th59:
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines id* OPPCAT_1:def 10 :
:: deftheorem defines *id OPPCAT_1:def 11 :
theorem Th66:
theorem
theorem Th68:
theorem
theorem