:: Opposite Categories and Contravariant Functors
:: by Czes\l aw Byli\'nski
::
:: Received February 13, 1991
:: Copyright (c) 1991-2026 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;
definitions TARSKI, XBOOLE_0, CAT_1;
equalities CAT_1, BINOP_1, GRAPH_1;
expansions CAT_1;
theorems FUNCT_2, FUNCT_4, PARTFUN1, CAT_1, SUBSET_1, FUNCT_1;
schemes FUNCT_2;
begin
reserve B,C,D for Category;
:: Opposite Category
definition
let C;
func C opp -> strict non empty non void CatStr equals
CatStr (#the carrier of C, the carrier' of C,
the Target of C, the Source of C, ~the Comp of C#);
coherence;
end;
definition
let C;
let c be Object of C;
func c opp -> Object of C opp equals
c;
coherence;
end;
registration let C;
cluster C opp -> Category-like
transitive associative reflexive with_identities;
coherence
proof
set M = the carrier' of C, d = the Target of C, c = the Source of C, p = ~(
the Comp of C);
set B = C opp;
thus A1: B is Category-like
proof
let f,g be Morphism of B;
reconsider ff=f, gg=g as Morphism of C;
thus [g,f] in dom(the Comp of B) implies dom g=cod f
proof
assume [g,f] in dom(the Comp of B);
then [ff,gg] in dom the Comp of C by FUNCT_4:42;
then dom ff = cod gg by CAT_1:def 6;
hence dom g=cod f;
end;
assume
A2: dom g=cod f;
cod gg = dom ff by A2;
then [ff,gg] in dom(the Comp of C) by CAT_1:def 6;
hence [g,f] in dom(the Comp of B) by FUNCT_4:42;
end;
A3: for f,g being Element of M st d.g = c.f
holds p.(g,f) = (the Comp of C).(f,g)
proof
let f,g be Element of M;
reconsider ff=f, gg=g as Morphism of B;
assume d.g = c.f;
then dom gg = cod ff;
then [gg,ff] in dom(p) by A1;
hence thesis by FUNCT_4:43;
end;
thus A4: B is transitive
proof
let ff,gg be Morphism of B;
reconsider f=ff, g=gg as Morphism of C;
assume
A5: dom gg=cod ff;
then
A6: cod g = dom f;
then
A7: [f,g] in dom the Comp of C by CAT_1:def 6;
[gg,ff] in dom the Comp of B by A5,A1;
then
A8: gg(*)ff = p.(g,f) by CAT_1:def 1
.= (the Comp of C).(f,g) by A3,A5
.= f(*)g by A7,CAT_1:def 1;
hence dom(gg(*)ff)
= cod(f(*)g)
.= cod f by A6,CAT_1:def 7
.= dom ff;
thus cod(gg(*)ff)
= dom(f(*)g) by A8
.= dom g by A6,CAT_1:def 7
.= cod gg;
end;
thus B is associative
proof
let ff,gg,hh be Morphism of B;
reconsider f=ff, g=gg, h=hh as Morphism of C;
assume that
A9: dom hh = cod gg and
A10: dom gg = cod ff;
A11: [h,g] in dom p by A1,A9;
then
A12: p.(h,g) is Element of M by PARTFUN1:4;
A13: [g,f] in dom p by A1,A10;
then
A14: p.(g,f) is Element of M by PARTFUN1:4;
A15: p.(h,g) = (the Comp of C).(g,h) by A3,A9;
d.(p.(h,g)) = dom(hh(*)gg) by A11,CAT_1:def 1
.= dom gg by A4,A9;
then
A16: p.(p.(h,g),f) = (the Comp of C).(f,(the Comp of C).(g,h))
by A3,A10,A12,A15;
A17: cod h = dom g & cod g = dom f by A9,A10;
A18: p.(g,f) = (the Comp of C).(f,g) by A3,A10;
A19: c.(p.(g,f)) = cod(gg(*)ff) by A13,CAT_1:def 1
.= cod gg by A4,A10;
dom(hh(*)gg) = dom gg by A4,A9;
then
A20: [hh(*)gg,ff] in dom the Comp of B by A1,A10;
cod(gg(*)ff) = cod gg by A4,A10;
then
A21: [hh,gg(*)ff] in dom the Comp of B by A1,A9;
[hh,gg] in dom the Comp of B by A9,A1;
then
A22: hh(*)gg = p.(h,g) by CAT_1:def 1;
A23: f(*)g = (the Comp of C).(f,g) by A17,CAT_1:16;
A24: dom(f(*)g) = dom g by A17,CAT_1:def 7;
A25: g(*)h = (the Comp of C).(g,h) by A17,CAT_1:16;
A26: cod(g(*)h) = cod g by A17,CAT_1:def 7;
[gg,ff] in dom the Comp of B by A10,A1;
then gg(*)ff = p.(g,f) by CAT_1:def 1;
hence hh(*)(gg(*)ff)
= p.(h,p.(g,f)) by A21,CAT_1:def 1
.= (the Comp of C).((the Comp of C).(f,g),h) by A3,A9,A14,A18,A19
.= f(*)g(*)h by A23,A17,A24,CAT_1:16
.= f(*)(g(*)h) by A17,CAT_1:def 8
.= p.(p.(h,g),f) by A16,A17,A25,A26,CAT_1:16
.= (hh(*)gg)(*)ff by A20,A22,CAT_1:def 1;
end;
thus B is reflexive
proof
let bb be Object of B;
reconsider b=bb as Element of C;
consider f being Morphism of C such that
A27: f in Hom(b,b) by SUBSET_1:4;
reconsider ff = f as Morphism of B;
A28: dom ff = cod f
.= bb by A27,CAT_1:1;
cod ff = dom f
.= bb by A27,CAT_1:1;
then ff in Hom(bb,bb) by A28;
hence Hom(bb,bb)<>{};
end;
let a be Element of B;
reconsider aa=a as Element of C;
reconsider ii = id aa as Morphism of B;
A29: dom ii = cod id aa
.= aa;
A30: cod ii = dom id aa
.= aa;
then reconsider ii as Morphism of a,a by A29,CAT_1:4;
take ii;
let b be Element of B;
reconsider bb = b as Element of C;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g
proof assume
A31: Hom(a,b)<>{};
let g being Morphism of a,b;
reconsider gg=g as Morphism of C;
A32: dom gg = cod g .= bb by A31,CAT_1:5;
A33: cod gg = dom g .= aa by A31,CAT_1:5;
then
A34: cod gg = dom id aa;
reconsider gg as Morphism of bb,aa by A32,A33,CAT_1:4;
A35: c.ii = aa by A30 .= dom g by A31,CAT_1:5
.= d.g;
then dom g = cod ii;
then [g,ii] in dom the Comp of B by A1;
hence g(*)ii = p.(g,ii) by CAT_1:def 1
.= (the Comp of C).(ii,g) by A35,A3
.= (id aa)(*)gg by A34,CAT_1:16
.= g by A33,CAT_1:21;
end;
assume
A36: Hom(b,a)<>{};
let g being Morphism of b,a;
reconsider gg=g as Morphism of C;
A37: cod gg = dom g .= bb by A36,CAT_1:5;
A38: dom gg = cod g .= aa by A36,CAT_1:5;
then
A39: dom gg = cod id aa;
reconsider gg as Morphism of aa,bb by A37,A38,CAT_1:4;
A40: d.ii = aa by A29 .= cod g by A36,CAT_1:5
.= c.g;
then cod g = dom ii;
then [ii,g] in dom the Comp of B by A1;
hence ii(*)g = p.(ii,g) by CAT_1:def 1
.= (the Comp of C).(g,ii) by A40,A3
.= gg(*)(id aa) by A39,CAT_1:16
.= g by A38,CAT_1:22;
end;
end;
definition
let C;
let c be Object of C opp;
func opp c -> Object of C equals
c opp;
coherence;
end;
::$CT
theorem
for c being Object of C holds c opp opp = c;
theorem
for c being Object of C holds opp (c opp) = c;
theorem
for c being Object of C opp holds (opp c) opp = c;
theorem Th4:
for a,b being Object of C
holds Hom(a,b) = Hom(b opp,a opp)
proof
let a,b be Object of C;
thus Hom(a,b) c= Hom(b opp,a opp)
proof let x be object;
assume
A1: x in Hom(a,b);
then reconsider f = x as Morphism of C;
reconsider g = f as Morphism of C opp;
dom f = a & cod f = b by A1,CAT_1:1;
then dom g = b opp & cod g = a opp;
hence x in Hom(b opp,a opp);
end;
let x be object;
assume
A2: x in Hom(b opp,a opp);
then reconsider f = x as Morphism of C opp;
reconsider g = f as Morphism of C;
dom f = b opp & cod f = a opp by A2,CAT_1:1;
then dom g = a & cod g = b;
hence x in Hom(a,b);
end;
theorem Th5:
for a,b being Object of C opp
holds Hom(a,b) = Hom(opp b,opp a)
proof let a,b be Object of C opp;
thus Hom(a,b)
= Hom((opp a)opp,(opp b) opp)
.= Hom(opp b,opp a) by Th4;
end;
definition
let C;
let f be Morphism of C;
func f opp -> Morphism of C opp equals
f;
coherence;
end;
definition
let C;
let f be Morphism of C opp;
func opp f -> Morphism of C equals
f opp;
coherence;
end;
definition let C; let a,b be Object of C such that
A1: Hom(a,b) <> {};
let f be Morphism of a,b;
func f opp -> Morphism of b opp, a opp equals
:Def6: f;
coherence
proof
f in Hom(a,b) by A1,CAT_1:def 5;
then f in Hom(b opp,a opp) by Th4;
hence thesis by CAT_1:def 5;
end;
end;
definition let C; let a,b be Object of C such that
A1: Hom(a opp,b opp) <> {};
let f be Morphism of a opp, b opp;
func opp f -> Morphism of b, a equals
:Def7: f;
coherence
proof
f in Hom(a opp,b opp) by A1,CAT_1:def 5;
then f in Hom(b,a) by Th4;
hence thesis by CAT_1:def 5;
end;
end;
theorem
for a,b being Object of C st Hom(a,b)<>{}
for f being Morphism of a,b holds f opp opp = f
proof let a,b be Object of C;
assume
A1: Hom(a,b)<>{};
then
A2: Hom(b opp,a opp)<>{} by Th4;
let f be Morphism of a,b;
thus f opp opp = f opp by A2,Def6
.= f by A1,Def6;
end;
theorem
for a,b being Object of C st Hom(a,b)<>{}
for f being Morphism of a,b holds opp(f opp) = f
proof let a,b be Object of C;
assume
A1: Hom(a,b)<>{};
then
A2: Hom(b opp,a opp)<>{} by Th4;
let f be Morphism of a,b;
thus opp(f opp) = f opp by A2,Def7
.= f by A1,Def6;
end;
theorem
for a,b being Object of C opp
for f being Morphism of a,b holds (opp f)opp = f;
theorem Th9:
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
proof let a,b be Object of C;
assume
A1: Hom(a,b)<>{};
then
A2: Hom(b opp,a opp)<>{} by Th4;
let f be Morphism of a,b;
thus dom(f opp) = b by A2,CAT_1:5
.= cod f by A1,CAT_1:5;
thus cod(f opp) = a by A2,CAT_1:5
.= dom f by A1,CAT_1:5;
end;
theorem
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
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) by Th9;
theorem
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 Th13:
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
proof
let a,b be Object of C opp, f be Morphism of a,b;
assume Hom(a,b) <> {};
then f in Hom(a,b) by CAT_1:def 5;
then opp f in Hom(opp b,opp a) by Th5;
hence thesis by CAT_1:def 5;
end;
theorem Th14:
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)
proof
let a,b,c be Object of C such that
A1: Hom(a,b) <> {} and
A2: Hom(b,c) <> {};
A3: Hom(b opp,a opp) <> {} by A1,Th4;
A4: Hom(c opp,b opp) <> {} by A2,Th4;
let f be Morphism of a,b, g be Morphism of b,c;
A5: dom g = b by A2,CAT_1:5 .= cod f by A1,CAT_1:5;
then
A6: g(*)f = ( the Comp of C ).(g,f) by CAT_1:16;
A7: f opp = f & g opp = g by A1,A2,Def6;
A8: dom g = b opp by A2,CAT_1:5 .= cod(g opp) by A4,CAT_1:5;
A9: cod f = b opp by A1,CAT_1:5 .= dom(f opp) by A3,CAT_1:5;
then
the Comp of C = ~(the Comp of C opp) & [f opp,g opp] in dom(the Comp of
C opp) by A5,A8,CAT_1:15,FUNCT_4:53;
then (the Comp of C ).(g,f) = (the Comp of C opp).(f opp,g opp) by A7,
FUNCT_4:def 2;
hence thesis by A5,A6,A8,A9,CAT_1:16;
end;
theorem
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)
proof let a,b,c be Object of C;
assume Hom(b opp,a opp) <> {} & Hom(c opp,b opp) <> {};
then Hom(a,b) <> {} & Hom(b,c) <> {} by Th4;
hence thesis by Th14;
end;
theorem Th16:
for f,g being Morphism of C opp st dom g = cod f holds opp (g(*)f)
= (opp f)(*)(opp g)
proof
let f,g be Morphism of C opp;
assume
A1: dom g = cod f;
A2: cod(opp g) = dom g & dom(opp f) = cod f;
then
A3: [opp f,opp g] in dom( the Comp of C ) by A1,CAT_1:15;
thus opp (g(*)f) = ~(the Comp of C).(opp g,opp f) by A1,CAT_1:16
.= (the Comp of C).(opp f,opp g) by A3,FUNCT_4:def 2
.= (opp f)(*)(opp g) by A1,A2,CAT_1:16;
end;
theorem
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)
proof
let a,b,c be Object of C, f be Morphism of a,b, g be Morphism of b,c;
assume
A1: Hom(a,b) <> {} & Hom(b,c) <> {};
A2: Hom(a,c) <> {} by A1,CAT_1:24;
thus (g*f) opp = g*f by A2,Def6 .= (g(*)f) opp by A1,CAT_1:def 13
.= (f opp)(*)(g opp) by A1,Th14;
end;
Lm1:
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 let a be Object of C;
let b be Object of C opp;
thus Hom(a opp,b) <> {} implies
for f being Morphism of a opp,b holds f(*)((id a) opp) = f
proof assume
A1: Hom(a opp,b) <> {};
A2: Hom(opp b,opp (a opp)) <> {} by A1,Th5;
let f be Morphism of a opp,b;
A3: Hom(a,a) <> {};
A4: cod opp(f qua Morphism of C opp) = dom f
.= a by A1,CAT_1:5;
dom opp(f qua Morphism of C opp) = cod f
.= opp b by A1,CAT_1:5;
then reconsider ff = opp f as Morphism of opp b,a
by A4,CAT_1:4;
A5: (id a)(*)ff = (id a)*ff by A3,A2,CAT_1:def 13;
thus f(*)((id a) opp)
= (ff opp)(*)((id a) opp) by A2,Def6
.= ((id a)(*)ff)opp by A2,A3,Th14
.= ((id a)*ff)opp by A5,Def6,A2
.= ff opp by A2,CAT_1:28
.= f by A2,Def6;
end;
assume
A6: Hom(b,a opp) <> {};
A7: Hom(opp (a opp),opp b) <> {} by A6,Th5;
let f be Morphism of b,a opp;
A8: Hom(a,a) <> {};
A9: dom opp(f qua Morphism of C opp) = cod f
.= a by A6,CAT_1:5;
cod opp(f qua Morphism of C opp) = dom f
.= opp b by A6,CAT_1:5;
then reconsider ff = opp(f qua Morphism of C opp) as Morphism of a,opp b
by A9,CAT_1:4;
A10: ff(*)(id a) = ff*(id a) by A8,A7,CAT_1:def 13;
thus ((id a) opp)(*)f
= ((id a) opp) (*) (ff opp) by A7,Def6
.= (ff(*)(id a))opp by A8,A7,Th14
.= (ff*(id a))opp by A10,Def6,A7
.= ff opp by A7,CAT_1:29
.= f by A7,Def6;
end;
theorem Th18:
for a being Object of C holds (id a) opp = id(a opp)
proof let a be 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)
by Lm1;
hence (id a) opp = id(a opp) by CAT_1:def 12;
end;
Lm2:
for a being Object of C holds id a = id(a opp)
proof let a be Object of C;
Hom(a,a) <> {};
hence id a = (id a)opp by Def6
.= id(a opp) by Th18;
end;
theorem Th19:
for a being Object of C opp holds opp id a = id opp a
proof let a be Object of C opp;
set b = opp a;
thus opp id a = id(b opp)
.= id opp a by Lm2;
end;
Lm3:
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)
proof let a,b,c be Object of C such that
A1: Hom(a,b) <> {} and
A2: Hom(b,c) <> {};
let f be Morphism of a,b, g be Morphism of b,c;
reconsider f1=f as Morphism of C;
reconsider g1=g as Morphism of C;
A3: Hom(b opp,a opp) <> {} by A1,Th4;
A4: Hom(c opp, b opp) <> {} by A2,Th4;
g*f = g(*)f opp by A1,A2,CAT_1:def 13
.= (f opp)(*)(g opp) by A1,A2,Th14
.= (f opp)*(g opp) by A3,A4,CAT_1:def 13;
hence thesis;
end;
theorem
for a,b being Object of C
for f being Morphism of a,b holds f opp is monic iff f is epi
proof let a,b be Object of C;
let f be Morphism of a,b;
thus f opp is monic implies f is epi
proof
assume that
A1: Hom(b opp,a opp) <> {} and
A2: for c being Object of C opp st Hom(c,b opp) <> {}
for f1,f2 being Morphism of c, b opp
st (f opp)*f1=(f opp)*f2 holds f1=f2;
thus
A3: Hom(a,b) <> {} by A1,Th4;
let c be Object of C such that
A4: Hom(b,c) <> {};
let g1,g2 be Morphism of b,c;
assume
A5: g1*f = g2*f;
reconsider f1=g1 opp, f2=g2 opp as Morphism of c opp, b opp;
A6: Hom(c opp,b opp) <> {} by A4,Th4;
(f opp)*f1 = g1*f by A4,Lm3,A3
.=(f opp)*f2 by A4,Lm3,A3,A5;
then
A7: f1=f2 by A2,A6;
g1 = f1 by A4,Def6
.=g2 by A7,A4,Def6;
hence thesis;
end;
assume that
A8: Hom(a,b) <> {} and
A9: for c being Object of C st Hom(b,c) <> {}
for g1,g2 being Morphism of b,c st g1*f=g2*f holds g1=g2;
thus
Hom(b opp,a opp) <> {} by A8,Th4;
let c be Object of C opp such that
A10: Hom(c,b opp) <> {};
let f1,f2 be Morphism of c, b opp;
assume
A11: (f opp)*f1=(f opp)*f2;
f1 in Hom(c,b opp) & f2 in Hom(c,b opp) by A10,CAT_1:def 5;
then f1 in Hom(opp(b opp), opp c) & f2 in Hom(opp(b opp), opp c)
by Th5;
then reconsider g1 = opp f1, g2 = opp f2 as Morphism of b, opp c
by CAT_1:def 5;
A12: Hom(opp(b opp),opp c) <> {} by A10,Th5;
A13: g1 opp = f1 by Def6,A12;
A14: g2 opp = f2 by Def6,A12;
g1*f = (f opp)*f2 by A11,A13,A8,Lm3,A12
.=g2*f by A8,Lm3,A12,A14;
hence f1 = f2 by A9,A12;
end;
theorem
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
proof let b,c be Object of C such that
A1: Hom(b,c) <> {};
let f be Morphism of b,c;
thus f opp is epi implies f is monic
proof
assume that
Hom(c opp,b opp) <> {} and
A2: for a being Object of C opp st Hom(b opp,a) <> {}
for g1,g2 being Morphism of b opp,a st g1*(f opp)=g2*(f opp) holds g1=g2;
thus Hom(b,c) <> {} by A1;
let a be Object of C such that
A3: Hom(a,b) <> {};
let f1,f2 be Morphism of a, b;
assume
A4: f*f1 = f*f2;
reconsider g1 = f1 opp,g2 = f2 opp as Morphism of b opp, a opp;
A5: Hom(b opp,a opp) <> {} by A3,Th4;
g1*(f opp) = f*f1 by Lm3,A1,A3
.= g2*(f opp) by Lm3,A1,A3,A4;
then g1=g2 by A2,A5;
hence f1 = g2 by Def6,A3
.=f2 by Def6,A3;
end;
assume that
A6: Hom(b,c) <> {} and
A7: for a being Object of C st Hom(a,b) <> {}
for f1,f2 being Morphism of a,b
st f*f1=f*f2 holds f1=f2;
thus Hom(c opp,b opp) <> {} by A6,Th4;
let a be Object of C opp such that
A8: Hom(b opp,a) <> {};
let g1,g2 be Morphism of b opp,a;
assume
A9: g1*(f opp) = g2*(f opp);
Hom(b opp,a) = Hom(opp a, opp(b opp)) by Th5
.= Hom(opp a,b);
then opp g1 in Hom(opp a,b) & opp g2 in Hom(opp a,b) by A8,CAT_1:def 5;
then
reconsider f1 = opp g1,f2 = opp g2 as Morphism of opp a,b by CAT_1:def 5;
A10: Hom(opp a,opp(b opp)) <> {} by A8,Th5;
f*f1 = (f1 opp)*(f opp) by A6,Lm3,A10
.= g2*(f opp) by A9,Def6,A10
.= (f2 opp)*(f opp) by Def6,A10
.=f*f2 by A6,Lm3,A10;
hence thesis by A7,A10;
end;
theorem
for a,b being Object of C
for f being Morphism of a,b holds f opp is invertible iff f is invertible
proof let a,b be Object of C;
let f be Morphism of a,b;
thus f opp is invertible implies f is invertible
proof assume
A1: Hom(b opp,a opp) <> {} & Hom(a opp,b opp) <> {};
given gg being Morphism of a opp, b opp such that
A2: (f opp)*gg = id(a opp) & gg*(f opp) = id(b opp);
thus
A3: Hom(a,b) <> {} & Hom(b,a) <> {} by A1,Th4;
reconsider g = opp gg as Morphism of b,a;
take g;
A4: g opp = g by Def6,A3
.= gg by Def7,A1;
thus f*g =(g opp)*(f opp) by A3,Lm3
.= id(b opp) by A2,A4
.= id b by Lm2;
thus g*f =(f opp)*(g opp) by A3,Lm3
.= id a by A2,A4,Lm2;
end;
assume
A5: Hom(a,b) <> {} & Hom(b,a) <> {};
given g being Morphism of b,a such that
A6: f*g = id b & g*f = id a;
thus Hom(b opp,a opp) <> {} & Hom(a opp,b opp) <> {} by A5,Th4;
take g opp;
thus (f opp)*(g opp) = g*f by A5,Lm3
.= id(a opp) by A6,Lm2;
thus (g opp)*(f opp) = f*g by A5,Lm3
.= id(b opp) by A6,Lm2;
end;
theorem
for c being Object of C holds c is initial iff c opp is terminal
proof
let c be Object of C;
thus c is initial implies c opp is terminal
proof
assume
A1: c is initial;
let b be Object of C opp;
consider f being Morphism of c,opp b such that
A2: for g being Morphism of c,opp b holds f=g by A1;
A3: (opp b) opp = b;
A4: Hom(c,opp b)<>{} by A1;
reconsider f9 = f opp as Morphism of b,c opp;
thus
A5: Hom(b,c opp)<>{} by A3,Th4,A4;
take f9;
let g be Morphism of b,c opp;
opp (c opp) = c;
then opp g is Morphism of c,opp b by A5,Th13;
hence g = f by A2
.= f9 by A4,Def6;
end;
assume
A6: c opp is terminal;
let b be Object of C;
consider f being Morphism of b opp,c opp such that
A7: for g being Morphism of b opp,c opp holds f=g by A6;
A8: opp (c opp) = c & opp (b opp) = b;
A9: Hom(b opp,c opp)<>{} by A6;
reconsider f9 = opp f as Morphism of c,b;
thus
A10: Hom(c,b)<>{} by A8,Th5,A9;
take f9;
let g be Morphism of c,b;
g opp = f by A7;
hence g = f by Def6,A10
.= f9 by A9,Def7;
end;
theorem
for c being Object of C holds c opp is initial iff c is terminal
proof
let c be Object of C;
thus c opp is initial implies c is terminal
proof
assume
A1: c opp is initial;
let b be Object of C;
consider f being Morphism of c opp,b opp such that
A2: for g being Morphism of c opp,b opp holds f = g by A1;
A3: opp(b opp) = b & opp(c opp) = c;
A4: Hom(c opp,b opp)<>{} by A1;
reconsider f9 = opp f as Morphism of b,c;
thus
A5: Hom(b,c)<>{} by A3,Th5,A4;
take f9;
let g be Morphism of b,c;
g opp = f by A2;
hence g = f by A5,Def6
.= f9 by Def7,A4;
end;
assume
A6: c is terminal;
let b be Object of C opp;
consider f being Morphism of opp b,c such that
A7: for g being Morphism of opp b, c holds f = g by A6;
A8: (opp b) opp = b;
A9: Hom(opp b,c)<>{} by A6;
reconsider f9 = f opp as Morphism of c opp,b;
thus
A10: Hom(c opp,b)<>{} by A8,Th4,A9;
take f9;
let g be Morphism of c opp,b;
opp g is Morphism of opp b,opp (c opp) by A10,Th13;
hence g = f by A7
.= f9 by Def6,A9;
end;
:: 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
:Def8:
for f being Morphism of C holds it.f = S.(f opp);
existence
proof
deffunc F(Morphism of C) = S.($1 opp);
thus ex F being Function of the carrier' of C,the carrier' of B st for f
being Morphism of C holds F.f = F(f) from FUNCT_2:sch 4;
end;
uniqueness
proof
let T1,T2 be Function of the carrier' of C,the carrier' of B such that
A1: for f being Morphism of C holds T1.f = S.(f opp) and
A2: for f being Morphism of C holds T2.f = S.(f opp);
now
let f be Morphism of C;
thus T1.f = S.(f opp) by A1
.= T2.f by A2;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem
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
let S be Function of the carrier' of C opp,the carrier' of B;
let f be Morphism of C opp;
thus (/*S).(opp f) = S.((opp f) opp) by Def8
.= S.f;
end;
Lm4: for S being Functor of C opp,B, c being Object of C holds (/*S).(id c) =
id((Obj S).(c opp))
proof
let S be Functor of C opp,B, c be Object of C;
reconsider i = id c as Morphism of C;
A1: Hom(c,c) <> {};
thus (/*S).(id c) = S.(i opp) by Def8
.= S.(id c)opp by A1,Def6
.= S.(id(c opp)) by Th18
.= id((Obj S).(c opp)) by CAT_1:68;
end;
theorem Th26:
for S being Functor of C opp,B, c being Object of C holds (Obj
/*S).c = (Obj S).(c opp)
proof
let S be Functor of C opp,B, c be Object of C;
A1: now
let c be Object of C;
(/*S).(id c) = id((Obj S).(c opp)) by Lm4;
hence ex d being Object of B st (/*S).(id c) = id d;
end;
(/*S).(id c) = id((Obj S).(c opp)) by Lm4;
hence thesis by A1,CAT_1:66;
end;
theorem
for S being Functor of C opp,B, c being Object of C opp holds (Obj /*S
).(opp c) = (Obj S).c
proof
let S be Functor of C opp,B, c be Object of C opp;
thus (Obj /*S).(opp c) = (Obj S).((opp c) opp) by Th26
.= (Obj S).c;
end;
Lm5: for S being Functor of C opp,B, c being Object of C holds /*S.(id c) = id
((Obj /*S).c)
proof
let S be Functor of C opp,B, c be Object of C;
reconsider i = id c as Morphism of C;
A1: Hom(c,c) <> {};
thus /*S.(id c) = S.(i opp) by Def8
.= S.((id c)opp) by Def6,A1
.= S.(id(c opp)) by Th18
.= id((Obj S).(c opp)) by CAT_1:68
.= id((Obj /*S).c) by Th26;
end;
Lm6: now
let C,B;
let S be Functor of C opp,B, c be Object of C;
(/*S).(id c) = id ((Obj /*S).c) by Lm5;
hence ex d being Object of B st (/*S).(id c) = id d;
end;
Lm7: for S being Functor of C opp,B, f being Morphism of C holds (Obj /*S).(
dom f) = cod (/*S.f) & (Obj /*S).(cod f) = dom (/*S.f)
proof
let S be Functor of C opp,B, f be Morphism of C;
A1: (Obj /*S).(cod f) = (Obj S).((cod f) opp) by Th26
.= (Obj S).(dom (f opp))
.= dom(S.(f opp)) by CAT_1:69;
(Obj /*S).(dom f) = (Obj S).((dom f) opp) by Th26
.= (Obj S).(cod (f opp))
.= cod(S.(f opp)) by CAT_1:69;
hence thesis by A1,Def8;
end;
Lm8: now
let C,B;
let S be Functor of C opp,B, f be Morphism of C;
thus (/*S).(id dom f) = id((Obj /*S).(dom f)) by Lm5
.= id cod (/*S.f) by Lm7;
thus (/*S).(id cod f) = id((Obj /*S).(cod f)) by Lm5
.= id dom (/*S.f) by Lm7;
end;
Lm9: for S being Functor of C opp,B
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 /*S.(g(*)f) = (/*S.f)(*)(/*S.g)
proof
let S be Functor of C opp,B;
let a,b,c be Object of C such that
A1: Hom(a,b) <> {} & Hom(b,c) <> {};
A2: Hom(b opp, a opp) <> {} & Hom(c opp, b opp) <> {} by A1,Th4;
let f be Morphism of a,b,
g be Morphism of b,c;
A3: dom g = b by A1,CAT_1:5 .= cod f by A1,CAT_1:5;
A4: dom(f opp) = b opp by A2,CAT_1:5 .= cod f by A1,CAT_1:5;
A5: cod (g opp) = b opp by A2,CAT_1:5 .= dom g by A1,CAT_1:5;
A6: S.(f opp) = S.((f qua Morphism of C) opp) by A1,Def6
.= /*S.f by Def8;
A7: S.(g opp) = S.((g qua Morphism of C) opp) by A1,Def6
.= /*S.g by Def8;
thus /*S.(g(*)f) = S.((g(*)f) opp) by Def8
.= S.((f opp)(*)(g opp)) by Th14,A1
.= (/*S.f)(*)(/*S.g) by A7,A6,A5,A3,A4,CAT_1:64;
end;
definition
let C,D;
mode Contravariant_Functor of C,D -> Function of the carrier' of C,the
carrier' of D means
:Def9:
( 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
proof
set S = the Functor of C opp,D;
take /*S;
thus for c being Object of C ex d being Object of D st /*S.(id c) = id d
by Lm6;
thus for f being Morphism of C
holds /*S.(id dom f) = id cod (/*S.f) &
/*S.(id cod f) = id dom (/*S.f) by Lm8;
let f,g be Morphism of C such that
A1: dom g = cod f;
reconsider ff=f as Morphism of dom f,cod f by CAT_1:4;
reconsider gg=g as Morphism of cod f,cod g by A1,CAT_1:4;
Hom(dom f,cod f)<>{} & Hom(dom g,cod g)<>{} by CAT_1:2;
then /*S.(gg(*)ff) = (/*S.ff)(*)(/*S.gg) by A1,Lm9;
hence thesis;
end;
end;
theorem Th28:
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
proof
let S be Contravariant_Functor of C,D;
let c be Object of C, d be Object of D;
for c being Object of C ex d being Object of D st S.(id c) = id d by Def9;
hence thesis by CAT_1:66;
end;
theorem Th29:
for S being Contravariant_Functor of C,D,c being Object of C
holds S.(id c) = id((Obj S).c)
proof
let S be Contravariant_Functor of C,D,c be Object of C;
ex d being Object of D st S.(id c) = id d by Def9;
hence thesis by Th28;
end;
theorem Th30:
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)
proof
let S be Contravariant_Functor of C,D, f be Morphism of C;
S.(id dom f) = id cod (S.f) & S.(id cod f) = id dom (S.f) by Def9;
hence thesis by Th28;
end;
theorem Th31:
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)
proof
let S be Contravariant_Functor of C,D, f,g be Morphism of C;
assume dom g = cod f;
hence dom (S.f) = (Obj S).(dom g) by Th30
.= cod (S.g) by Th30;
end;
theorem Th32:
for S being Functor of C opp,B holds /*S is Contravariant_Functor of C,B
proof
let S be Functor of C opp,B;
thus for c being Object of C ex d being Object of B st /*S.(id c) = id d
by Lm6;
thus for f being Morphism of C holds /*S.(id dom f) = id cod (/*S.f) &
/*S.(id cod f) = id dom (/*S.f) by Lm8;
let f,g be Morphism of C such that
A1: dom g = cod f;
reconsider ff=f as Morphism of dom f,cod f by CAT_1:4;
reconsider gg=g as Morphism of cod f,cod g by A1,CAT_1:4;
Hom(dom f,cod f)<>{} & Hom(dom g,cod g)<>{} by CAT_1:2;
then /*S.(gg(*)ff) = (/*S.ff)(*)(/*S.gg) by A1,Lm9;
hence thesis;
end;
theorem Th33:
for S1 being Contravariant_Functor of C,B, S2 being
Contravariant_Functor of B,D holds S2*S1 is Functor of C,D
proof
let S1 be Contravariant_Functor of C,B, S2 be Contravariant_Functor of B,D;
set T = S2*S1;
now
thus for c being Object of C ex d being Object of D st T.(id c) = id d
proof
let c be Object of C;
consider b being Object of B such that
A1: S1.(id c) = id b by Def9;
consider d being Object of D such that
A2: S2.(id b) = id d by Def9;
take d;
thus thesis by A1,A2,FUNCT_2:15;
end;
thus for f being Morphism of C holds T.(id dom f) = id dom (T.f) & T.(id
cod f) = id cod (T.f)
proof
let f be Morphism of C;
thus T.(id dom f) = S2.(S1.(id dom f)) by FUNCT_2:15
.= S2.(id cod (S1.f)) by Def9
.= id dom (S2.((S1.f))) by Def9
.= id dom (T.f) by FUNCT_2:15;
thus T.(id cod f) = S2.(S1.(id cod f)) by FUNCT_2:15
.= S2.(id dom (S1.f)) by Def9
.= id cod (S2.((S1.f))) by Def9
.= id cod (T.f) by FUNCT_2:15;
end;
let f,g be Morphism of C;
assume
A3: dom g = cod f;
then
A4: cod (S1.g) = dom(S1.f) by Th31;
thus T.(g(*)f) = S2.(S1.(g(*)f)) by FUNCT_2:15
.= S2.((S1.f)(*)(S1.g)) by A3,Def9
.= (S2.(S1.g))(*)(S2.(S1.f)) by A4,Def9
.= (T.g)(*)(S2.(S1.f)) by FUNCT_2:15
.= (T.g)(*)(T.f) by FUNCT_2:15;
end;
hence thesis by CAT_1:61;
end;
Lm10: for S being Contravariant_Functor of C opp,B, c being Object of C holds (
/*S).(id c) = id((Obj S).(c opp))
proof
let S be Contravariant_Functor of C opp,B, c be Object of C;
reconsider i = id c as Morphism of C;
A1: Hom(c,c) <> {};
thus (/*S).(id c) = S.(i opp) by Def8
.= S.((id c)opp) by Def6,A1
.= S.(id(c opp)) by Th18
.= id((Obj S).(c opp)) by Th29;
end;
theorem Th34:
for S being Contravariant_Functor of C opp,B, c being Object of
C holds (Obj /*S).c = (Obj S).(c opp)
proof
let S be Contravariant_Functor of C opp,B, c be Object of C;
A1: now
let c be Object of C;
(/*S).(id c) = id((Obj S).(c opp)) by Lm10;
hence ex d being Object of B st (/*S).(id c) = id d;
end;
(/*S).(id c) = id((Obj S).(c opp)) by Lm10;
hence thesis by A1,CAT_1:66;
end;
theorem
for S being Contravariant_Functor of C opp,B, c being Object of C opp
holds (Obj /*S).(opp c) = (Obj S).c
proof
let S be Contravariant_Functor of C opp,B, c be Object of C opp;
thus (Obj /*S).(opp c) = (Obj S).((opp c) opp) by Th34
.= (Obj S).c;
end;
Lm11: for S being Contravariant_Functor of C opp,B, c being Object of C holds
/*S.(id c) = id((Obj /*S).c)
proof
let S be Contravariant_Functor of C opp,B, c be Object of C;
reconsider i = id c as Morphism of C;
A1: Hom(c,c) <> {};
thus /*S.(id c) = S.(i opp) by Def8
.= S.((id c)opp) by Def6,A1
.= S.(id(c opp)) by Th18
.= id((Obj S).(c opp)) by Th29
.= id((Obj /*S).c) by Th34;
end;
Lm12: for S being Contravariant_Functor of C opp,B, f being Morphism of C holds
(Obj /*S).(dom f) = dom (/*S.f) & (Obj /*S).(cod f) = cod (/*S.f)
proof
let S be Contravariant_Functor of C opp,B, f be Morphism of C;
A1: (Obj /*S).(cod f) = (Obj S).((cod f) opp) by Th34
.= (Obj S).(dom (f opp))
.= cod(S.(f opp)) by Th30;
(Obj /*S).(dom f) = (Obj S).((dom f) opp) by Th34
.= (Obj S).(cod (f opp))
.= dom(S.(f opp)) by Th30;
hence thesis by A1,Def8;
end;
theorem
for S being Contravariant_Functor of C opp,B holds /*S is Functor of C , B
proof
let S be Contravariant_Functor of C opp,B;
now
thus for c being Object of C ex d being Object of B st /*S.(id c) = id d
proof
let c be Object of C;
(/*S).(id c) = id ((Obj /*S).c) by Lm11;
hence thesis;
end;
thus for f being Morphism of C holds (/*S).(id dom f) = id dom (/*S.f) & (
/*S).(id cod f) = id cod (/*S.f)
proof
let f be Morphism of C;
thus (/*S).(id dom f) = id((Obj /*S).(dom f)) by Lm11
.= id dom (/*S.f) by Lm12;
thus (/*S).(id cod f) = id((Obj /*S).(cod f)) by Lm11
.= id cod (/*S.f) by Lm12;
end;
let f,g be Morphism of C such that
A1: dom g = cod f;
A2: dom(f opp) = cod f & cod (g opp) = dom g;
reconsider ff=f as Morphism of dom f,cod f by CAT_1:4;
reconsider gg=g as Morphism of cod f,cod g by A1,CAT_1:4;
A3: Hom(dom f,cod f)<>{} & Hom(dom g,cod g)<>{} by CAT_1:2;
then
A4: ff opp = f opp by Def6;
A5: gg opp = g opp by Def6,A3,A1;
thus /*S.(g(*)f) = S.((g(*)f) opp) by Def8
.= S.((f opp)(*)(g opp)) by A4,A5,A3,A1,Th14
.= (S.(g opp))(*)(S.(f opp)) by A1,A2,Def9
.= (/*S.g)(*)(S.(f opp)) by Def8
.= (/*S.g)(*)(/*S.f) by Def8;
end;
hence thesis by CAT_1:61;
end;
:: 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
:Def10:
for f being Morphism of C opp holds it.f = S.(opp f);
existence
proof
deffunc F(Morphism of C opp) = S.(opp $1);
thus ex F being Function of the carrier' of C opp,the carrier' of B st for
f being Morphism of C opp holds F.f = F(f) from FUNCT_2:sch 4;
end;
uniqueness
proof
let T1,T2 be Function of the carrier' of C opp,the carrier' of B such that
A1: for f being Morphism of C opp holds T1.f = S.(opp f) and
A2: for f being Morphism of C opp holds T2.f = S.(opp f);
now
let f be Morphism of C opp;
thus T1.f = S.(opp f) by A1
.= T2.f by A2;
end;
hence thesis by FUNCT_2:63;
end;
func S*' -> Function of the carrier' of C,the carrier' of B opp means
:Def11:
for f being Morphism of C holds it.f = (S.f) opp;
existence
proof
deffunc F(Morphism of C) = (S.$1) opp;
thus ex F being Function of the carrier' of C,the carrier' of B opp st for
f being Morphism of C holds F.f = F(f) from FUNCT_2:sch 4;
end;
uniqueness
proof
let T1,T2 be Function of the carrier' of C,the carrier' of B opp such that
A3: for f being Morphism of C holds T1.f = (S.f) opp and
A4: for f being Morphism of C holds T2.f = (S.f) opp;
now
let f be Morphism of C;
thus T1.f = (S.f) opp by A3
.= T2.f by A4;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem
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
let S be Function of the carrier' of C,the carrier' of B;
let f be Morphism of C;
thus (*'S).(f opp) = S.(opp (f opp)) by Def10
.= S.f;
end;
Lm13: for S being Functor of C,B, c being Object of C opp holds (*'S).(id c) =
id((Obj S).(opp c))
proof
let S be Functor of C,B, c be Object of C opp;
thus (*'S).(id c) = S.(opp id c) by Def10
.= S.(id opp c)by Th19
.= id((Obj S).(opp c)) by CAT_1:68;
end;
theorem Th38:
for S being Functor of C,B, c being Object of C opp holds (Obj
*'S).c = (Obj S).(opp c)
proof
let S be Functor of C,B, c be Object of C opp;
now
thus (*'S).(id c) = id((Obj S).(opp c)) by Lm13;
let c be Object of C opp;
(*'S).(id c) = id((Obj S).(opp c)) by Lm13;
hence ex d being Object of B st (*'S).(id c) = id d;
end;
hence thesis by CAT_1:66;
end;
theorem
for S being Functor of C,B, c being Object of C holds (Obj *'S).(c opp
) = (Obj S).c
proof
let S be Functor of C,B, c be Object of C;
thus (Obj *'S).(c opp) = (Obj S).(opp (c opp)) by Th38
.= (Obj S).c;
end;
Lm14: for S being Functor of C,B, c being Object of C holds (S*').(id c) = id(
((Obj S).c) opp)
proof
let S be Functor of C,B, c be Object of C;
A1: Hom((Obj S).c,(Obj S).c) <> {};
thus (S*').(id c) = (S.(id c)) opp by Def11
.= (id((Obj S).c) qua Morphism of B) opp by CAT_1:68
.= (id((Obj S).c)) opp by Def6,A1
.= id(((Obj S).c) opp) by Th18;
end;
theorem Th40:
for S being Functor of C,B, c being Object of C holds (Obj S*').
c = ((Obj S).c) opp
proof
let S be Functor of C,B, c be Object of C;
now
thus (S*').(id c) = id(((Obj S).c) opp) by Lm14;
let c be Object of C;
(S*').(id c) = id(((Obj S).c) opp) by Lm14;
hence ex d being Object of B opp st (S*').(id c) = id d;
end;
hence thesis by CAT_1:66;
end;
Lm15: for S being Contravariant_Functor of C,B, c being Object of C opp holds
(*'S).(id c) = id((Obj S).(opp c))
proof
let S be Contravariant_Functor of C,B, c be Object of C opp;
thus (*'S).(id c) = S.(opp id c) by Def10
.= S.(id opp c) by Th19
.= id((Obj S).(opp c)) by Th29;
end;
theorem Th41:
for S being Contravariant_Functor of C,B, c being Object of C
opp holds (Obj *'S).c = (Obj S).(opp c)
proof
let S be Contravariant_Functor of C,B, c be Object of C opp;
now
thus (*'S).(id c) = id((Obj S).(opp c)) by Lm15;
let c be Object of C opp;
(*'S).(id c) = id((Obj S).(opp c)) by Lm15;
hence ex d being Object of B st (*'S).(id c) = id d;
end;
hence thesis by CAT_1:66;
end;
theorem
for S being Contravariant_Functor of C,B, c being Object of C holds (
Obj *'S).(c opp) = (Obj S).c
proof
let S be Contravariant_Functor of C,B, c be Object of C;
thus (Obj *'S).(c opp) = (Obj S).(opp (c opp)) by Th41
.= (Obj S).c;
end;
Lm16: for S being Contravariant_Functor of C,B, c being Object of C holds (S*'
).(id c) = id(((Obj S).c) opp)
proof
let S be Contravariant_Functor of C,B, c be Object of C;
A1: Hom((Obj S).c,(Obj S).c) <> {};
thus (S*').(id c) = (S.(id c)) opp by Def11
.= (id((Obj S).c) qua Morphism of B) opp by Th29
.= (id((Obj S).c)) opp by Def6,A1
.= id(((Obj S).c) opp) by Th18;
end;
theorem Th43:
for S being Contravariant_Functor of C,B, c being Object of C
holds (Obj S*').c = ((Obj S).c) opp
proof
let S be Contravariant_Functor of C,B, c be Object of C;
now
thus (S*').(id c) = id(((Obj S).c) opp) by Lm16;
let c be Object of C;
(S*').(id c) = id(((Obj S).c) opp) by Lm16;
hence ex d being Object of B opp st (S*').(id c) = id d;
end;
hence thesis by CAT_1:66;
end;
Lm17: 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
let F be Function of the carrier' of C,the carrier' of D;
let f be Morphism of C opp;
thus *'F*'.f = (*'F.f) opp by Def11
.= (F.(opp f)) opp by Def10;
end;
theorem Th44:
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
let F be Function of the carrier' of C,the carrier' of D;
let f be Morphism of C;
thus *'F*'.(f opp) = (F.(opp(f opp))) opp by Lm17
.= (F.f) opp;
end;
theorem Th45:
for S being Function of the carrier' of C,the carrier' of D holds /*(*'S) = S
proof
let S be Function of the carrier' of C,the carrier' of D;
now
let f be Morphism of C;
thus /*(*'S).f = (*'S).(f opp) by Def8
.= S.(opp (f opp)) by Def10
.= S.f;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for S being Function of the carrier' of C opp,the carrier' of D holds
*'(/*S) = S
proof
let S be Function of the carrier' of C opp,the carrier' of D;
now
let f be Morphism of C opp;
thus *'(/*S).f = (/*S).(opp f) by Def10
.= S.((opp f) opp) by Def8
.= S.f;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for S being Function of the carrier' of C, the carrier' of D holds *'S
*' = *'(S*')
proof
let S be Function of the carrier' of C, the carrier' of D;
now
let f be Morphism of C opp;
thus *'S*'.f = (*'S.f) opp by Def11
.= (S.(opp f)) opp by Def10
.= (S*').(opp f) by Def11
.= *'(S*').f by Def10;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for D being strict Category, S being Function of the carrier' of C,
the carrier' of D holds S*'*' = S
proof
let D be strict Category;
let S be Function of the carrier' of C, the carrier' of D;
now
thus D opp opp = D by FUNCT_4:53;
let f be Morphism of C;
thus S*'*'.f = (S*'.f) opp by Def11
.= (S.f) opp opp by Def11
.= S.f;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for C being strict Category, S being Function of the carrier' of C,
the carrier' of D holds *'*'S = S
proof
let C be strict Category;
let S be Function of the carrier' of C, the carrier' of D;
now
thus C opp opp = C by FUNCT_4:53;
let f be Morphism of C opp opp;
thus *'*'S.f = *'S.(opp f) by Def10
.= S.(opp opp f) by Def10
.= S.f;
end;
hence thesis by FUNCT_2:63;
end;
Lm18: 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
let S be Function of the carrier' of C opp,the carrier' of B;
let T be Function of the carrier' of B,the carrier' of D;
now
let f be Morphism of C;
thus /*(T*S).f = (T*S).(f opp) by Def8
.= T.(S.(f opp)) by FUNCT_2:15
.= T.(/*S.f) by Def8
.= (T*(/*S)).f by FUNCT_2:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem
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
let S be Function of the carrier' of C,the carrier' of B;
let T be Function of the carrier' of B,the carrier' of D;
now
let f be Morphism of C opp;
thus (*'(T*S)).f = (T*S).(opp f) by Def10
.= T.(S.(opp f)) by FUNCT_2:15
.= T.(*'S.f) by Def10
.= (T*(*'S)).f by FUNCT_2:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem
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
let S be Function of the carrier' of C,the carrier' of B;
let T be Function of the carrier' of B,the carrier' of D;
now
let f be Morphism of C;
thus (T*S)*'.f = ((T*S).f) opp by Def11
.= (T.(S.f)) opp by FUNCT_2:15
.= T*'.(S.f) by Def11
.= (T*'*S).f by FUNCT_2:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem
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
let F1 be Function of the carrier' of C,the carrier' of B;
let F2 be Function of the carrier' of B,the carrier' of D;
now
let f be Morphism of C opp;
thus (*'(F2*F1)*').f = ((F2*F1).(opp f)) opp by Lm17
.= (F2.(F1.(opp f))) opp by FUNCT_2:15
.= (*'F2*').((F1.(opp f)) opp) by Th44
.= (*'F2*').((*'F1*').f) by Lm17
.= ((*'F2*')*(*'F1*')).f by FUNCT_2:15;
end;
hence thesis by FUNCT_2:63;
end;
Lm19: for S being Contravariant_Functor of C,B, c being Object of C opp holds
*'S.(id c) = id((Obj *'S).c)
proof
let S be Contravariant_Functor of C,B, c be Object of C opp;
thus *'S.(id c) = S.(opp id c) by Def10
.= S.(id opp c) by Th19
.= id((Obj S).(opp c)) by Th29
.= id((Obj *'S).c) by Th41;
end;
Lm20: for S being Contravariant_Functor of C,B, f being Morphism of C opp
holds (Obj *'S).(dom f) = dom (*'S.f) & (Obj *'S).(cod f) = cod (*'S.f)
proof
let S be Contravariant_Functor of C,B, f be Morphism of C opp;
A1: (Obj *'S).(cod f) = (Obj S).(opp cod f) by Th41
.= (Obj S).(dom opp f)
.= cod(S.(opp f)) by Th30;
(Obj *'S).(dom f) = (Obj S).(opp dom f) by Th41
.= (Obj S).(cod opp f )
.= dom(S.(opp f)) by Th30;
hence thesis by A1,Def10;
end;
theorem Th53:
for S being Contravariant_Functor of C,D holds *'S is Functor of C opp,D
proof
let S be Contravariant_Functor of C,D;
now
thus for c being Object of C opp ex d being Object of D st *'S.(id c) = id
d
proof
let c be Object of C opp;
(*'S).(id c) = id ((Obj *'S).c) by Lm19;
hence thesis;
end;
thus for f being Morphism of C opp holds *'S.(id dom f) = id dom (*'S.f) &
*'S.(id cod f) = id cod (*'S.f)
proof
let f be Morphism of C opp;
thus (*'S).(id dom f) = id((Obj *'S).(dom f)) by Lm19
.= id dom (*'S.f) by Lm20;
thus (*'S).(id cod f) = id((Obj *'S).(cod f)) by Lm19
.= id cod (*'S.f) by Lm20;
end;
let f,g be Morphism of C opp such that
A1: dom g = cod f;
A2: dom(opp f) = cod f & cod (opp g) = dom g;
thus *'S.(g(*)f) = S.(opp (g(*)f)) by Def10
.= S.((opp f)(*)(opp g)) by A1,Th16
.= (S.(opp g))(*)(S.(opp f)) by A1,A2,Def9
.= (*'S.g)(*)(S.(opp f)) by Def10
.= (*'S.g)(*)(*'S.f) by Def10;
end;
hence thesis by CAT_1:61;
end;
Lm21: for S being Contravariant_Functor of C,B, c being Object of C holds S*'.
(id c) = id((Obj S*').c)
proof
let S be Contravariant_Functor of C,B, c be Object of C;
A1: Hom((Obj S).c,(Obj S).c) <> {};
thus S*'.(id c) = (S.(id c)) opp by Def11
.= (id((Obj S).c) qua Morphism of B) opp by Th29
.= (id((Obj S).c)) opp by Def6,A1
.= id(((Obj S).c) opp) by Th18
.= id((Obj S*').c) by Th43;
end;
Lm22: for S being Contravariant_Functor of C,B, f being Morphism of C holds (
Obj S*').(dom f) = dom (S*'.f) & (Obj S*').(cod f) = cod (S*'.f)
proof
let S be Contravariant_Functor of C,B, f be Morphism of C;
A1: (Obj S*').(cod f) = ((Obj S).(cod f)) opp by Th43
.= (dom(S.f)) opp by Th30
.= cod((S.f) opp);
(Obj S*').(dom f) = ((Obj S).(dom f)) opp by Th43
.= (cod(S.f)) opp by Th30
.= dom((S.f) opp);
hence thesis by A1,Def11;
end;
theorem Th54:
for S being Contravariant_Functor of C,D holds S*' is Functor of C, D opp
proof
let S be Contravariant_Functor of C,D;
now
thus for c being Object of C ex d being Object of D opp st S*'.(id c) = id
d
proof
let c be Object of C;
(S*').(id c) = id(((Obj S).c) opp) by Lm16;
hence thesis;
end;
thus for f being Morphism of C holds S*'.(id dom f) = id dom (S*'.f) & S*'
.(id cod f) = id cod (S*'.f)
proof
let f be Morphism of C;
thus (S*').(id dom f) = id((Obj S*').(dom f)) by Lm21
.= id dom (S*'.f) by Lm22;
thus (S*').(id cod f) = id((Obj S*').(cod f)) by Lm21
.= id cod (S*'.f) by Lm22;
end;
let f,g be Morphism of C;
assume
A1: dom g = cod f;
then
A2: dom(S.f) = cod (S.g) by Th31;
reconsider Sff=S.f as Morphism of dom(S.f),cod(S.f) by CAT_1:4;
reconsider Sgg=S.g as Morphism of dom(S.g),cod(S.g) by CAT_1:4;
A3: Hom(dom(S.f),cod(S.f))<>{} & Hom(dom(S.g),cod(S.g))<>{} by CAT_1:2;
then
A4: Sff opp = (S.f)opp by Def6;
A5: Sgg opp = (S.g)opp by A3,Def6;
thus S*'.(g(*)f) = (S.(g(*)f)) opp by Def11
.= ((Sff)(*)(Sgg)) opp by A1,Def9
.= ((Sgg) opp)(*)((Sff) opp) by A3,A2,Th14
.= (S*'.g)(*)((S.f) opp) by Def11,A4,A5
.= (S*'.g)(*)(S*'.f) by Def11;
end;
hence thesis by CAT_1:61;
end;
Lm23: for S being Functor of C,B, c being Object of C opp holds *'S.(id c) =
id((Obj *'S).c)
proof
let S be Functor of C,B, c be Object of C opp;
thus *'S.(id c) = S.(opp id c) by Def10
.= S.(id opp c) by Th19
.= id((Obj S).(opp c)) by CAT_1:68
.= id((Obj *'S).c) by Th38;
end;
Lm24: for S being Functor of C,B, f being Morphism of C opp holds (Obj *'S).(
dom f) = cod (*'S.f) & (Obj *'S).(cod f) = dom (*'S.f)
proof
let S be Functor of C,B, f be Morphism of C opp;
A1: (Obj *'S).(cod f) = (Obj S).(opp cod f) by Th38
.= (Obj S).(dom opp f)
.= dom(S.(opp f)) by CAT_1:69;
(Obj *'S).(dom f) = (Obj S).(opp dom f) by Th38
.= (Obj S).(cod opp f )
.= cod(S.(opp f)) by CAT_1:69;
hence thesis by A1,Def10;
end;
theorem Th55:
for S being Functor of C,D holds *'S is Contravariant_Functor of C opp,D
proof
let S be Functor of C,D;
thus for c being Object of C opp ex d being Object of D st *'S.(id c) = id d
proof
let c be Object of C opp;
(*'S).(id c) = id ((Obj *'S).c) by Lm23;
hence thesis;
end;
thus for f being Morphism of C opp holds *'S.(id dom f) = id cod (*'S.f) &
*'S.(id cod f) = id dom (*'S.f)
proof
let f be Morphism of C opp;
thus (*'S).(id dom f) = id((Obj *'S).(dom f)) by Lm23
.= id cod(*'S.f) by Lm24;
thus (*'S).(id cod f) = id((Obj *'S).(cod f)) by Lm23
.= id dom(*'S.f) by Lm24;
end;
let f,g be Morphism of C opp
such that
A1: dom g = cod f;
A2: dom(opp f) = cod f & cod (opp g) = dom g;
thus *'S.(g(*)f) = S.(opp (g(*)f)) by Def10
.= S.((opp f)(*)(opp g)) by A1,Th16
.= (S.(opp f))(*)(S.(opp g)) by A1,A2,CAT_1:64
.= (*'S.f)(*)(S.(opp g)) by Def10
.= (*'S.f)(*)(*'S.g) by Def10;
end;
Lm25: for S being Functor of C,B, c being Object of C holds S*'.(id c) = id((
Obj S*').c)
proof
let S be Functor of C,B, c be Object of C;
A1: Hom((Obj S).c,(Obj S).c) <> {};
thus S*'.(id c) = (S.(id c)) opp by Def11
.= (id((Obj S).c) qua Morphism of B) opp by CAT_1:68
.= (id((Obj S).c)) opp by Def6,A1
.= id(((Obj S).c) opp) by Th18
.= id((Obj S*').c) by Th40;
end;
Lm26: for S being Functor of C,B, f being Morphism of C holds (Obj S*').(dom f
) = cod (S*'.f) & (Obj S*').(cod f) = dom (S*'.f)
proof
let S be Functor of C,B, f be Morphism of C;
A1: (Obj S*').(cod f) = ((Obj S).(cod f)) opp by Th40
.= (cod(S.f)) opp by CAT_1:69
.= dom((S.f) opp);
(Obj S*').(dom f) = ((Obj S).(dom f)) opp by Th40
.= (dom(S.f)) opp by CAT_1:69
.= cod((S.f) opp);
hence thesis by A1,Def11;
end;
theorem Th56:
for S being Functor of C,D holds S*' is Contravariant_Functor of C, D opp
proof
let S be Functor of C,D;
thus for c being Object of C ex d being Object of D opp st S*'.(id c) = id d
proof
let c be Object of C;
(S*').(id c) = id ((Obj S*').c) by Lm25;
hence thesis;
end;
thus for f being Morphism of C holds S*'.(id dom f) = id cod (S*'.f) & S*'.(
id cod f) = id dom (S*'.f)
proof
let f be Morphism of C;
thus (S*').(id dom f) = id((Obj S*').(dom f)) by Lm25
.= id cod(S*'.f) by Lm26;
thus (S*').(id cod f) = id((Obj S*').(cod f)) by Lm25
.= id dom(S*'.f) by Lm26;
end;
let f,g be Morphism of C;
assume
A1: dom g = cod f;
then
A2: dom(S.g) = cod (S.f) by CAT_1:64;
reconsider Sff=S.f as Morphism of dom(S.f),cod(S.f) by CAT_1:4;
reconsider Sgg=S.g as Morphism of dom(S.g),cod(S.g) by CAT_1:4;
A3: Hom(dom(S.f),cod(S.f))<>{} & Hom(dom(S.g),cod(S.g))<>{} by CAT_1:2;
then
A4: Sff opp = (S.f)opp by Def6;
A5: Sgg opp = (S.g)opp by Def6,A3;
thus S*'.(g(*)f) = (S.(g(*)f)) opp by Def11
.= ((Sgg)(*)(Sff)) opp by A1,CAT_1:64
.= ((Sff) opp)(*)((Sgg) opp) by A2,Th14,A3
.= (S*'.f)(*)((S.g) opp) by Def11,A4,A5
.= (S*'.f)(*)(S*'.g) by Def11;
end;
theorem
for S1 being Contravariant_Functor of C,B, S2 being Functor of B,D
holds S2*S1 is Contravariant_Functor of C,D
proof
let S1 be Contravariant_Functor of C,B, S2 be Functor of B,D;
*'S1 is Functor of C opp,B by Th53;
then S2*(*'S1) is Functor of C opp,D by CAT_1:73;
then /*(S2*(*'S1)) is Contravariant_Functor of C,D by Th32;
then S2*(/*(*'S1)) is Contravariant_Functor of C,D by Lm18;
hence thesis by Th45;
end;
theorem
for S1 being Functor of C,B, S2 being Contravariant_Functor of B,D
holds S2*S1 is Contravariant_Functor of C,D
proof
let S1 be Functor of C,B, S2 be Contravariant_Functor of B,D;
*'S1 is Contravariant_Functor of C opp,B by Th55;
then S2*(*'S1) is Functor of C opp,D by Th33;
then /*(S2*(*'S1)) is Contravariant_Functor of C,D by Th32;
then S2*(/*(*'S1)) is Contravariant_Functor of C,D by Lm18;
hence thesis by Th45;
end;
theorem
for F being Functor of C,D, c being Object of C holds (Obj *'F*').(c
opp) = ((Obj F).c) opp
proof
let F be Functor of C,D, c be Object of C;
*'F is Contravariant_Functor of C opp,D by Th55;
hence (Obj *'F*').(c opp) = ((Obj *'F).(c opp)) opp by Th43
.= ((Obj F).(opp (c opp))) opp by Th38
.= ((Obj F).c) opp;
end;
theorem
for F being Contravariant_Functor of C,D, c being Object of C holds (
Obj *'F*').(c opp) = ((Obj F).c) opp
proof
let F be Contravariant_Functor of C,D, c be Object of C;
*'F is Functor of C opp,D by Th53;
hence (Obj *'F*').(c opp) = ((Obj *'F).(c opp)) opp by Th40
.= ((Obj F).(opp(c opp))) opp by Th41
.= ((Obj F).c) opp;
end;
theorem
for F being Functor of C,D holds *'F*' is Functor of C opp,D opp
proof
let F be Functor of C,D;
*'F is Contravariant_Functor of C opp,D by Th55;
hence thesis by Th54;
end;
theorem
for F being Contravariant_Functor of C,D holds *'F*' is
Contravariant_Functor of C opp,D opp
proof
let F be Contravariant_Functor of C,D;
*'F is Functor of C opp,D by Th53;
hence thesis by Th56;
end;
:: Duality Functors
definition
let C;
func id* C -> Contravariant_Functor of C,C opp equals
(id C)*';
coherence by Th56;
func *id C -> Contravariant_Functor of C opp,C equals
*'(id C);
coherence by Th55;
end;
theorem Th63:
for f being Morphism of C holds (id* C).f = f opp
proof
let f be Morphism of C;
thus (id* C).f = ((id C).f) opp by Def11
.= f opp by FUNCT_1:18;
end;
theorem
for c being Object of C holds (Obj id* C).c = c opp
proof
let c be Object of C;
thus (Obj id* C).c = ((Obj id C).c) opp by Th40
.= c opp by CAT_1:77;
end;
theorem Th65:
for f being Morphism of C opp holds (*id C).f = opp f
proof
let f be Morphism of C opp;
thus (*id C).f = ((id C).(opp f)) by Def10
.= opp f by FUNCT_1:18;
end;
theorem
for c being Object of C opp holds (Obj *id C).c = opp c
proof
let c be Object of C opp;
thus (Obj *id C).c = (Obj id C).(opp c) by Th38
.= opp c by CAT_1:77;
end;
theorem
for S being Function of the carrier' of C,the carrier' of D holds *'S
= S*(*id C) & S*' = (id* D)*S
proof
let S be Function of the carrier' of C,the carrier' of D;
now
let f be Morphism of C opp;
thus *'S.f = S.(opp f) by Def10
.= S.((*id C).f) by Th65
.= (S*(*id C)).f by FUNCT_2:15;
end;
hence *'S = S*(*id C) by FUNCT_2:63;
now
let f be Morphism of C;
thus S*'.f = (S.f) opp by Def11
.= (id* D).(S.f) by Th63
.= ((id* D)*S).f by FUNCT_2:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem
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) by Lm3;
theorem Th69:
for a being Object of C holds id a = id(a opp) by Lm2;
theorem
for a being Object of C opp holds id a = id opp a
proof let a be Object of C opp;
thus id a = id ((opp a)opp)
.= id opp a by Th69;
end;