:: Opposite Categories and Contravariant Functors
:: by Czes\l aw Byli\'nski
::
:: Received February 13, 1991
:: Copyright (c) 1991-2016 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;