:: Subcategories and Products of Categories
:: by Czes{\l}aw Byli\'nski
::
:: Received May 31, 1990
:: Copyright (c) 1990-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 XBOOLE_0, SUBSET_1, FUNCT_2, FUNCT_1, ZFMISC_1, FUNCT_5, RELAT_1,
TARSKI, CAT_1, FUNCOP_1, STRUCT_0, GRAPH_1, FUNCT_3, REALSET1, PARTFUN1,
FUNCT_4, MCART_1, CAT_2, MONOID_0, RELAT_2, BINOP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
FUNCT_2, BINOP_1, PARTFUN1, FUNCT_3, FUNCT_4, FUNCT_5, REALSET1,
FUNCOP_1, STRUCT_0, GRAPH_1, CAT_1;
constructors PARTFUN1, BINOP_1, FUNCT_3, FUNCT_4, FUNCT_5, REALSET1, CAT_1,
FUNCOP_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, CAT_1, STRUCT_0,
RELAT_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, CAT_1;
equalities CAT_1, REALSET1, FUNCOP_1, BINOP_1, GRAPH_1;
expansions CAT_1;
theorems TARSKI, ZFMISC_1, MCART_1, DOMAIN_1, FUNCT_1, FUNCT_2, FUNCT_3,
FUNCT_4, FUNCT_5, PARTFUN1, FUNCOP_1, CAT_1, GRFUNC_1, RELAT_1, RELSET_1,
XBOOLE_0, XBOOLE_1, XTUPLE_0;
schemes XBOOLE_0, BINOP_1;
begin
::$CT 4
reserve B,C,D,C9,D9 for Category;
:: Auxiliary theorems on Functors
definition
let B,C;
let c be Object of C;
func B --> c -> Functor of B,C equals
(the carrier' of B) --> (id c);
coherence
proof
reconsider T = (the carrier' of B) --> id c as Function of the carrier' of
B,the carrier' of C;
now
thus for b being Object of B ex d being Object of C st T.(id b) = id d
by FUNCOP_1:7;
thus for f being Morphism of B holds T.(id dom f) = id dom (T.f) & T.(id
cod f) = id cod (T.f)
proof
let f be Morphism of B;
T.(id cod f) = id c by FUNCOP_1:7;
then
A1: T.(id cod f) = id cod id c;
T.(id dom f) = id c by FUNCOP_1:7;
then T.(id dom f) = id dom id c;
hence thesis by A1,FUNCOP_1:7;
end;
let f,g be Morphism of B such that
dom g = cod f;
Hom(c,c) <> {};
then
A2: T.f = id c & (id c)*(id c) = (id c)(*)((id c)) by CAT_1:def 13,FUNCOP_1:7
;
T.(g(*)f) = id c & T.g = id c by FUNCOP_1:7;
hence T.(g(*)f) = (T.g)(*)(T.f) by A2;
end;
hence thesis by CAT_1:61;
end;
end;
theorem
for c being Object of C, b being Object of B holds (Obj (B --> c)).b = c
proof
let c be Object of C, b be Object of B;
(B --> c).(id b) = id c by FUNCOP_1:7;
hence thesis by CAT_1:67;
end;
definition
let C,D;
func Funct(C,D) -> set means
:Def2:
for x being set holds x in it iff x is Functor of C,D;
existence
proof
defpred P[object] means $1 is Functor of C,D;
consider F being set such that
A1: for x being object holds x in F iff x in Funcs(the carrier' of C,the
carrier' of D) & P[x] from XBOOLE_0:sch 1;
take F;
let x be set;
thus x in F implies x is Functor of C,D by A1;
assume
A2: x is Functor of C,D;
then x in Funcs(the carrier' of C,the carrier' of D) by FUNCT_2:8;
hence thesis by A1,A2;
end;
uniqueness
proof
let F1,F2 be set such that
A3: for x being set holds x in F1 iff x is Functor of C,D and
A4: for x being set holds x in F2 iff x is Functor of C,D;
now
let x be object;
x in F1 iff x is Functor of C,D by A3;
hence x in F1 iff x in F2 by A4;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let C,D;
cluster Funct(C,D) -> non empty;
coherence
proof
set x = the Functor of C,D;
x in Funct(C,D) by Def2;
hence thesis;
end;
end;
definition
let C,D;
mode FUNCTOR-DOMAIN of C,D -> non empty set means
:Def3:
for x being Element of it holds x is Functor of C,D;
existence
proof
take Funct(C,D);
thus thesis by Def2;
end;
end;
definition
let C,D;
let F be FUNCTOR-DOMAIN of C,D;
redefine mode Element of F -> Functor of C,D; :: redefines Element (SUBSET_1, definition)
coherence by Def3;
end;
definition
let A be non empty set;
let C,D;
let F be FUNCTOR-DOMAIN of C,D, T be Function of A,F, x be Element of A;
redefine func T.x -> Element of F; :: redefines . (FUNCT_1, definition)
coherence
proof
thus T.x is Element of F;
end;
end;
definition
let C,D;
redefine func Funct(C,D) -> FUNCTOR-DOMAIN of C,D; :: redefines Funct (CAT_2, definition)
coherence
proof
let x be Element of Funct(C,D);
thus thesis by Def2;
end;
end;
:: Subcategory
definition
let C;
mode Subcategory of C -> Category means
:Def4:
the carrier of it c= the carrier of C &
(for a,b being Object of it, a9,b9 being Object of C
st a = a9 & b = b9
holds Hom(a,b) c= Hom(a9,b9)) & the Comp of it c= the Comp of C &
for a being Object of it, a9 being Object of C st a = a9
holds id a = id a9;
existence
proof
take C;
thus thesis;
end;
end;
registration
let C;
cluster strict for Subcategory of C;
existence
proof
set c = the Object of C;
set E = 1Cat(c,id c);
now
thus the carrier of E c= the carrier of C
proof
let a be object;
assume a in the carrier of E;
then a = c by TARSKI:def 1;
hence thesis;
end;
thus for a,b being Object of E, a9,b9 being Object of C st a = a9 & b =
b9 holds Hom(a,b) c= Hom(a9,b9)
proof
let a,b be Object of E, a9,b9 be Object of C;
assume a = a9 & b = b9;
then
A1: a9 = c & b9 = c by TARSKI:def 1;
let x be object;
assume x in Hom(a,b);
then x = id c by TARSKI:def 1;
hence thesis by A1,CAT_1:27;
end;
thus the Comp of E c= the Comp of C
proof
reconsider i = id c as Morphism of C;
A2: Hom(c,c) <> {};
A3: dom id c = c & cod id c = c;
then
A4: [id c,id c] in dom the Comp of C by CAT_1:15;
the Comp of E = (id c,id c).-->((id c)*(id c))
.= (id c,id c).-->((id c)(*)i) by A2,CAT_1:def 13
.= [id c,id c].-->(the Comp of C).(id c,id c) by A3,CAT_1:16;
hence thesis by A4,FUNCT_4:7;
end;
let a be Object of E, a9 be Object of C;
assume a = a9;
then a9 = c by TARSKI:def 1;
hence id a = id a9 by TARSKI:def 1;
end;
then E is Subcategory of C by Def4;
hence thesis;
end;
end;
reserve E for Subcategory of C;
theorem Th2:
for e being Object of E holds e is Object of C
proof
let e be Object of E;
e in the carrier of E & the carrier of E c= the carrier of C by Def4;
hence thesis;
end;
theorem Th3:
the carrier' of E c= the carrier' of C
proof
let x be object;
assume x in the carrier' of E;
then reconsider f = x as Morphism of E;
set a = dom f, b = cod f;
reconsider a9 = a, b9 = b as Object of C by Th2;
f in Hom(a,b) & Hom(a,b) c= Hom(a9,b9) by Def4;
then f in Hom(a9,b9) & Hom(a9,b9) <> {};
hence thesis;
end;
theorem Th4:
for f being Morphism of E holds f is Morphism of C
proof
let f be Morphism of E;
f in the carrier' of E & the carrier' of E c= the carrier' of C by Th3;
hence thesis;
end;
theorem Th5:
for f being (Morphism of E), f9 being Morphism of C st f = f9
holds dom f = dom f9 & cod f = cod f9
proof
let f be (Morphism of E), f9 be Morphism of C such that
A1: f = f9;
set a = dom f, b = cod f;
reconsider a9 = a, b9 = b as Object of C by Th2;
f in Hom(a,b) & Hom(a,b) c= Hom(a9,b9) by Def4;
hence thesis by A1,CAT_1:1;
end;
theorem
for a,b being Object of E, a9,b9 being Object of C,f being Morphism of
a, b st a = a9 & b = b9 & Hom(a,b)<>{} holds f is Morphism of a9,b9
proof
let a,b be Object of E, a9,b9 be Object of C, f be Morphism of a,b;
assume a = a9 & b = b9 & Hom(a,b)<>{};
then f in Hom(a,b) & Hom(a,b) c= Hom(a9,b9) by Def4,CAT_1:def 5;
then f in Hom(a9,b9) & Hom(a9,b9) <> {};
hence thesis by CAT_1:def 5;
end;
theorem Th7:
for f,g being (Morphism of E), f9,g9 being Morphism of C st f =
f9 & g = g9 & dom g = cod f holds g(*)f = g9(*)f9
proof
let f,g be (Morphism of E), f9,g9 be Morphism of C such that
A1: f = f9 & g = g9 and
A2: dom g = cod f;
dom g = dom g9 & cod f = cod f9 by A1,Th5;
then
A3: g9(*)f9 = (the Comp of C).(g9,f9) by A2,CAT_1:16;
A4: the Comp of E c= the Comp of C by Def4;
g(*)f = (the Comp of E).(g,f) & [g,f] in dom(the Comp of E)
by A2,CAT_1:15,16;
hence thesis by A1,A3,A4,GRFUNC_1:2;
end;
theorem Th8:
C is Subcategory of C
proof
thus the carrier of C c= the carrier of C;
thus thesis;
end;
theorem Th9:
id E is Functor of E,C
proof
rng id E c= the carrier' of C by Th3;
then reconsider
T = id E as Function of the carrier' of E,the carrier' of C by FUNCT_2:6;
now
thus for e being Object of E ex c being Object of C st T.(id e) = id c
proof
let e be Object of E;
reconsider c = e as Object of C by Th2;
T.(id e) = id e by FUNCT_1:18
.= id c by Def4;
hence thesis;
end;
thus for f being Morphism of E holds T.(id dom f) = id dom (T.f) & T.(id
cod f) = id cod (T.f)
proof
let f be Morphism of E;
A1: T.(id dom f) = id dom f by FUNCT_1:18
.= id dom ((id E).f) by FUNCT_1:18;
A2: T.(id cod f) = id cod f by FUNCT_1:18
.= id cod ((id E).f) by FUNCT_1:18;
dom (T.f) = dom((id E).f) & cod (T.f) = cod((id E).f) by Th5;
hence thesis by A1,A2,Def4;
end;
let f,g be Morphism of E;
A3: T.f = f & T.g = g by FUNCT_1:18;
assume
A4: dom g = cod f;
then T.(g(*)f) = ((id E).g)(*)((id E).f) by CAT_1:64;
hence T.(g(*)f) = (T.g)(*)(T.f) by A4,A3,Th7;
end;
hence thesis by CAT_1:61;
end;
definition
let C,E;
func incl(E) -> Functor of E,C equals
id E;
coherence by Th9;
end;
theorem Th10:
for a being Object of E holds (Obj incl E).a = a
proof
let a be Object of E;
reconsider a9 = a as Object of C by Th2;
id a9 = id a by Def4
.= (incl E).(id a) by FUNCT_1:18
.= id((Obj incl E).a) by CAT_1:68;
hence thesis by CAT_1:59;
end;
theorem
for a being Object of E holds (incl E).a = a by Th10;
theorem
incl E is faithful
proof
let a,b be Object of E such that
Hom(a,b) <> {};
let f1,f2 be Morphism of a,b;
(incl E).f1 = f1 by FUNCT_1:18;
hence thesis by FUNCT_1:18;
end;
theorem Th13:
incl E is full iff for a,b being Object of E, a9,b9 being Object
of C st a = a9 & b = b9 holds Hom(a,b) = Hom(a9,b9)
proof
set T = incl E;
thus T is full implies for a,b being Object of E, a9,b9 being Object of C st
a = a9 & b = b9 holds Hom(a,b) = Hom(a9,b9)
proof
assume
A1: for a,b being Object of E st Hom(T.a,T.b) <> {} for g being
Morphism of T.a,T.b holds Hom(a,b) <> {} & ex f being Morphism of a,b st g = T.
f;
let a,b be Object of E, a9,b9 be Object of C such that
A2: a = a9 & b = b9;
now
let x be object;
Hom(a,b) c= Hom(a9,b9) by A2,Def4;
hence x in Hom(a,b) implies x in Hom(a9,b9);
assume
A3: x in Hom(a9,b9);
A4: T.a = a9 & T.b = b9 by A2,Th10;
then reconsider g = x as Morphism of T.a,T.b by A3,CAT_1:def 5;
consider f being Morphism of a,b such that
A5: g = T.f by A1,A4,A3;
A6: g = f by A5,FUNCT_1:18;
Hom(a,b) <> {} by A1,A4,A3;
hence x in Hom(a,b) by A6,CAT_1:def 5;
end;
hence thesis by TARSKI:2;
end;
assume
A7: for a,b being Object of E, a9,b9 being Object of C st a = a9 & b =
b9 holds Hom(a,b) = Hom(a9,b9);
let a,b be Object of E such that
A8: Hom(T.a,T.b) <> {};
let g be Morphism of T.a,T.b;
A9: g in Hom(T.a,T.b) by A8,CAT_1:def 5;
A10: a = T.a & b = T.b by Th10;
hence Hom(a,b) <> {} by A7,A8;
Hom(a,b) = Hom(T.a,T.b) by A7,A10;
then reconsider f = g as Morphism of a,b by A9,CAT_1:def 5;
take f;
thus thesis by FUNCT_1:18;
end;
definition let D;
let C be Subcategory of D;
attr C is full means
:Def6: for c1,c2 being Object of C, d1,d2 being Object of D
st c1 = d1 & c2 = d2
holds Hom(c1,c2) = Hom(d1,d2);
end;
registration let D;
cluster full for Subcategory of D;
existence
proof
reconsider C = D as Subcategory of D by Th8;
take C;
let c1,c2 be Object of C, d1,d2 being Object of D;
assume c1 = d1 & c2 = d2;
hence Hom(c1,c2) = Hom(d1,d2);
end;
end;
theorem
E is full iff incl(E) is full
by Th13;
theorem Th15:
for O being non empty Subset of the carrier of C holds union{Hom
(a,b) where a is Object of C,b is Object of C: a in O & b in O} is non empty
Subset of the carrier' of C
proof
let O be non empty Subset of the carrier of C;
set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O};
set M = union H;
A1: M c= the carrier' of C
proof
let x be object;
assume x in M;
then consider X being set such that
A2: x in X and
A3: X in H by TARSKI:def 4;
ex a,b being Object of C st X = Hom(a,b) & a in O & b in O by A3;
hence thesis by A2;
end;
now
set a = the Element of O;
reconsider a as Object of C;
id a in Hom(a,a) & Hom(a,a) in H by CAT_1:27;
then id a in M by TARSKI:def 4;
hence ex f being set st f in M;
end;
hence thesis by A1;
end;
theorem Th16:
for O being non empty Subset of the carrier of C, M being non
empty set st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O
& b in O} holds (the Source of C)|M is Function of M,O & (the Target of C)|M is
Function of M,O & (the Comp of C)||M is PartFunc of [:M,M:],M
proof
let O be non empty Subset of the carrier of C;
set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O};
A1: dom the Source of C = the carrier' of C by FUNCT_2:def 1;
let M be non empty set such that
A2: M = union H;
A3: now
let f be Morphism of C;
assume f in M;
then consider X being set such that
A4: f in X and
A5: X in H by A2,TARSKI:def 4;
ex a,b being Object of C st X = Hom(a,b) & a in O & b in O by A5;
hence dom f in O & cod f in O by A4,CAT_1:1;
end;
set d = (the Source of C)|M, c = (the Target of C)|M, p = (the Comp of C)||M;
A6: dom the Target of C = the carrier' of C by FUNCT_2:def 1;
A7: dom d = (dom the Source of C) /\ M by RELAT_1:61;
A8: rng d c= O
proof
let y be object;
assume y in rng d;
then consider x being object such that
A9: x in dom d and
A10: y = d.x by FUNCT_1:def 3;
reconsider f = x as Morphism of C by A1,A7,A9,XBOOLE_0:def 4;
d.f = dom f & f in M by A7,A9,FUNCT_1:47,XBOOLE_0:def 4;
hence thesis by A3,A10;
end;
A11: M is non empty Subset of the carrier' of C by A2,Th15;
then
A12: dom c = M by A6,RELAT_1:62;
A13: dom c = (dom the Target of C) /\ M by RELAT_1:61;
A14: rng c c= O
proof
let y be object;
assume y in rng c;
then consider x being object such that
A15: x in dom c and
A16: y = c.x by FUNCT_1:def 3;
reconsider f = x as Morphism of C by A6,A13,A15,XBOOLE_0:def 4;
c.f = cod f & f in M by A13,A15,FUNCT_1:47,XBOOLE_0:def 4;
hence thesis by A3,A16;
end;
dom d = M by A1,A11,RELAT_1:62;
hence d is Function of M,O & c is Function of M,O by A8,A14,A12,FUNCT_2:def 1
,RELSET_1:4;
A17: dom p = (dom the Comp of C) /\ [:M,M:] by RELAT_1:61;
A18: dom the Comp of C c= [:the carrier' of C,the carrier' of C:] by
RELAT_1:def 18;
rng p c= M
proof
let y be object;
assume y in rng p;
then consider x being object such that
A19: x in dom p and
A20: y = p.x by FUNCT_1:def 3;
A21: x in dom the Comp of C by A17,A19,XBOOLE_0:def 4;
then consider g,f being Morphism of C such that
A22: x = [g,f] by A18,DOMAIN_1:1;
A23: [g,f] in [:M,M:] by A17,A19,A22,XBOOLE_0:def 4;
then g in M by ZFMISC_1:87;
then
A24: cod g in O by A3;
dom g = cod f by A21,A22,CAT_1:15;
then
A25: dom(g(*)f) = dom f & cod(g(*)f) = cod g by CAT_1:17;
f in M by A23,ZFMISC_1:87;
then dom f in O by A3;
then
A26: Hom(dom(g(*)f),cod(g(*)f)) in H by A24,A25;
A27: g(*)f in Hom(dom(g(*)f),cod(g(*)f ));
p.x = (the Comp of C).(g,f) by A19,A22,FUNCT_1:47
.= g(*)f by A21,A22,CAT_1:def 1;
hence thesis by A2,A20,A26,A27,TARSKI:def 4;
end;
hence p is PartFunc of [:M,M:],M by A17,RELSET_1:4,XBOOLE_1:17;
thus thesis;
end;
registration
let O, M be non empty set, d,c being Function of M,O, p being PartFunc of [:
M,M:],M;
cluster CatStr(#O,M,d,c,p#) -> non void non empty;
coherence;
end;
Lm1:
for O being non empty Subset of the carrier of C, M being non empty
set, d,c being Function of M,O, p being PartFunc of [:M,M:],M, i being Function
of O,M st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O &
b in O} & d = (the Source of C)|M & c = (the Target of C)|M & p = (the Comp of
C)||M
holds CatStr(#O,M,d,c,p#) is Category
proof
let O be non empty Subset of the carrier of C, M be non empty set, d,c be
Function of M,O, p be PartFunc of [:M,M:],M, i be Function of O,M;
set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O};
assume that
A1: M = union H and
A2: d = (the Source of C)|M and
A3: c = (the Target of C)|M and
A4: p = (the Comp of C)||M;
set B = CatStr(#O,M,d,c,p#);
A5: now
let f be Morphism of B;
consider X being set such that
A6: f in X and
A7: X in H by A1,TARSKI:def 4;
ex a,b being Object of C st X = Hom(a,b) & a in O & b in O by A7;
hence f is Morphism of C by A6;
end;
A8: for f,g being Morphism of B holds [g,f] in dom(p) iff d.g=c.f
proof
let f,g be Morphism of B;
reconsider gg=g, ff=f as Morphism of C by A5;
A9: d.g = dom gg & c.f = cod ff by A2,A3,FUNCT_1:49;
thus [g,f] in dom(p) implies d.g = c.f
proof
assume [g,f] in dom(p);
then [g,f] in (dom the Comp of C) /\ [:M,M:] by A4,RELAT_1:61;
then [gg,ff] in (dom the Comp of C) by XBOOLE_0:def 4;
hence thesis by A9,CAT_1:def 6;
end;
assume d.g=c.f;
then [g,f] in dom the Comp of C by A9,CAT_1:def 6;
then [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def 4;
hence thesis by A4,RELAT_1:61;
end;
A10: B is Category-like
by A8;
A11: B is transitive
proof
thus
for f,g being Morphism of B st dom g = cod f
holds dom(g(*)f) = dom f & cod(g(*)f) = cod g
proof
let f,g be Morphism of B;
reconsider ff=f, gg=g as Morphism of C by A5;
A12: d.g = dom gg & c.f = cod ff by A2,A3,FUNCT_1:49;
assume
A13: dom g = cod f;
A14: [g,f] in dom the Comp of B by A13,A8;
A15: p.(g,f) = g(*)f by A13,A8,CAT_1:def 1;
A16: dom p c= dom the Comp of C by A4,RELAT_1:60;
A17: p.[g,f] = (the Comp of C).(g,f) by A4,A8,A13,FUNCT_1:47
.= gg(*)ff by A16,A14,CAT_1:def 1;
thus dom(g(*)f)
= dom(gg(*)ff) by A17,A2,A15,FUNCT_1:49
.= dom ff by A13,A12,CAT_1:def 7
.= dom f by A2,FUNCT_1:49;
thus cod(g(*)f)
= cod(gg(*)ff) by A17,A3,A15,FUNCT_1:49
.= cod gg by A13,A12,CAT_1:def 7
.= cod g by A3,FUNCT_1:49;
end;
end;
A18: B is associative
proof
thus for f,g,h being Morphism of B
st dom h = cod g & dom g = cod f
holds h(*)(g(*)f) = (h(*)g)(*)f
proof
let f,g,h be Morphism of B;
reconsider ff=f, gg=g, hh=h as Morphism of C by A5;
assume that
A19: dom h = cod g and
A20: dom g = cod f;
A21: h(*)g = (the Comp of B).(h,g) by A19,A8,CAT_1:def 1;
A22: g(*)f = (the Comp of B).(g,f) by A20,A8,CAT_1:def 1;
A23: dom(h(*)g) = dom g by A11,A19;
A24: c.g = cod gg & d.g = dom gg by A2,A3,FUNCT_1:49;
A25: c.f = cod ff by A3,FUNCT_1:49;
A26: f is Morphism of C & d.h = dom hh by A2,A5,FUNCT_1:49;
A27: dom gg = d.g by A2,FUNCT_1:49
.= cod ff by A3,A20,FUNCT_1:49;
then
A28: gg(*)ff = (the Comp of C).(gg,ff) by CAT_1:16;
A29: dom hh = d.h by A2,FUNCT_1:49
.= cod gg by A3,A19,FUNCT_1:49;
then
A30: cod(gg(*)ff) = dom hh by A27,CAT_1:def 7;
A31: hh(*)gg = (the Comp of C).(hh,gg) by A29,CAT_1:16;
A32: cod ff= dom(hh(*)gg) by A27,A29,CAT_1:def 7;
A33: cod(g(*)f) = cod g by A11,A20;
hence h(*)(g(*)f)
= (the Comp of B).(h,(the Comp of B).(g,f)) by A22,A19,A8
,CAT_1:def 1
.= (the Comp of C).[h,p.[g,f]] by A4,A8,A19,A33,A22,FUNCT_1:47
.= (the Comp of C).(hh,gg(*)ff) by A4,A8,A20,A28,FUNCT_1:47
.= hh(*)(gg(*)ff) by A30,CAT_1:16
.= (hh(*)gg)(*)ff
by A19,A20,A26,A24,A25,CAT_1:def 8
.= (the Comp of C).((the Comp of C).(hh,gg),ff)
by A31,A32,CAT_1:16
.= (the Comp of C).[p.[h,g],f] by A4,A8,A19,FUNCT_1:47
.= (the Comp of B).((the Comp of B).(h,g),f)
by A4,A8,A20,A23,A21,FUNCT_1:47
.= h(*)g(*)f by A21,A20,A8,A23,CAT_1:def 1;
end;
end;
A34: B is reflexive
proof
let b be Object of B;
b in O;
then reconsider bb = b as Object of C;
A35: Hom(bb,bb) in H;
id bb in Hom(bb,bb) by CAT_1:27;
then reconsider ii = id bb as Morphism of B by A35,A1,TARSKI:def 4;
A36: dom ii = dom id bb by A2,FUNCT_1:49
.= bb;
cod ii = cod id bb by A3,FUNCT_1:49
.= bb;
then ii in Hom(b,b) by A36;
hence Hom(b,b)<>{};
end;
B is with_identities
proof let a be Element of B;
a in O;
then reconsider aa = a as Object of C;
A37: Hom(aa,aa) in H;
id aa in Hom(aa,aa) by CAT_1:27;
then reconsider ii = id aa as Morphism of B by A37,A1,TARSKI:def 4;
A38: dom ii = dom id aa by A2,FUNCT_1:49
.= aa;
A39: cod ii = cod id aa by A3,FUNCT_1:49
.= aa;
then reconsider ii as Morphism of a,a by A38,CAT_1:4;
take ii;
let b be Element of B;
b in O;
then reconsider bb = b as Object of C;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g
proof assume
A40: Hom(a,b)<>{};
let g be Morphism of a,b;
reconsider gg = g as Morphism of C by A5;
A41: dom gg = dom g by A2,FUNCT_1:49
.= aa by A40,CAT_1:5;
A42: cod id aa = aa;
cod gg = cod g by A3,FUNCT_1:49
.= bb by A40,CAT_1:5;
then reconsider gg as Morphism of aa,bb by A41,CAT_1:4;
A43: dom g = a by A40,CAT_1:5;
hence g(*)ii = p.(g,ii) by A39,A8,CAT_1:def 1
.= (the Comp of C).(gg,id aa) by A43,A4,A39,A8,FUNCT_1:47
.= gg(*)id aa by A41,A42,CAT_1:16
.= g by A41,CAT_1:22;
end;
thus
Hom(b,a)<>{} implies for f being Morphism of b,a holds ii(*)f = f
proof assume
A44: Hom(b,a)<>{};
let g be Morphism of b,a;
reconsider gg = g as Morphism of C by A5;
A45: cod gg = cod g by A3,FUNCT_1:49
.= aa by A44,CAT_1:5;
A46: dom id aa = aa;
dom gg = dom g by A2,FUNCT_1:49
.= bb by A44,CAT_1:5;
then reconsider gg as Morphism of bb,aa by A45,CAT_1:4;
A47: cod g = a by A44,CAT_1:5;
hence ii(*)g = p.(ii,g) by A38,A8,CAT_1:def 1
.= (the Comp of C).(id aa,gg) by A4,A47,A38,A8,FUNCT_1:47
.= (id aa)(*)gg by A45,A46,CAT_1:16
.= g by A45,CAT_1:21;
end;
end;
hence B is Category by A10,A11,A18,A34;
end;
Lm2:
for O being non empty Subset of the carrier of C, M being non empty
set, d,c being Function of M,O, p being PartFunc of [:M,M:],M, i being Function
of O,M st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O &
b in O} & d = (the Source of C)|M & c = (the Target of C)|M & p = (the Comp of
C)||M
holds CatStr(#O,M,d,c,p#) is Subcategory of C
proof
let O be non empty Subset of the carrier of C, M be non empty set, d,c be
Function of M,O, p be PartFunc of [:M,M:],M, i be Function of O,M;
set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O};
assume that
A1: M = union H and
A2: d = (the Source of C)|M and
A3: c = (the Target of C)|M and
A4: p = (the Comp of C)||M;
set B = CatStr(#O,M,d,c,p#);
A5: now
let f be Morphism of B;
consider X being set such that
A6: f in X and
A7: X in H by A1,TARSKI:def 4;
ex a,b being Object of C st X = Hom(a,b) & a in O & b in O by A7;
hence f is Morphism of C by A6;
end;
A8: for a,b being Object of B, a9,b9 being Object of C st a = a9 & b = b9
holds Hom(a,b) = Hom(a9,b9)
proof
let a,b be Object of B, a9,b9 be Object of C such that
A9: a = a9 & b = b9;
now
let x be object;
thus x in Hom(a,b) implies x in Hom(a9,b9)
proof
assume
A10: x in Hom(a,b);
then reconsider f = x as Morphism of B;
reconsider f9 = f as Morphism of C by A5;
cod f = cod f9 by A3,FUNCT_1:49;
then
A11: b = cod f9 by A10,CAT_1:1;
dom f = dom f9 by A2,FUNCT_1:49;
then a = dom f9 by A10,CAT_1:1;
hence thesis by A9,A11;
end;
assume
A12: x in Hom(a9,b9);
then reconsider f9 = x as Morphism of C;
Hom(a9,b9) in H by A9;
then reconsider f = f9 as Morphism of B by A1,A12,TARSKI:def 4;
cod f = cod f9 by A3,FUNCT_1:49;
then
A13: cod f = b9 by A12,CAT_1:1;
dom f = dom f9 by A2,FUNCT_1:49;
then dom f = a9 by A12,CAT_1:1;
hence x in Hom(a,b) by A9,A13;
end;
hence thesis by TARSKI:2;
end;
reconsider B as Category by Lm1,A1,A2,A3,A4;
A14: for a be Object of B, a9 be Object of C st a = a9 holds id a = id a9
proof let a be Object of B, a9 be Object of C such that
A15: a = a9;
A16: Hom(a9,a9) in H by A15;
A17: id a9 in Hom(a9,a9) by CAT_1:27;
then reconsider ii = id a9 as Morphism of B by A16,A1,TARSKI:def 4;
A18: dom ii = dom id a9 by A2,FUNCT_1:49
.= a9;
A19: cod ii = cod id a9 by A3,FUNCT_1:49
.= a9;
ii in Hom(a,a) by A17,A8,A15;
then reconsider ii as Morphism of a,a by CAT_1:def 5;
A20: for f,g being Morphism of B holds [g,f] in dom(p) iff d.g=c.f
proof
let f,g be Morphism of B;
reconsider gg=g, ff=f as Morphism of C by A5;
A21: d.g = dom gg & c.f = cod ff by A2,A3,FUNCT_1:49;
thus [g,f] in dom(p) implies d.g = c.f
proof
assume [g,f] in dom(p);
then [g,f] in (dom the Comp of C) /\ [:M,M:] by A4,RELAT_1:61;
then [gg,ff] in (dom the Comp of C) by XBOOLE_0:def 4;
hence thesis by A21,CAT_1:def 6;
end;
assume d.g=c.f;
then [g,f] in dom the Comp of C by A21,CAT_1:def 6;
then [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def 4;
hence thesis by A4,RELAT_1:61;
end;
for b being Object of B holds
(Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)ii = f)
& (Hom(b,a) <> {} implies
for f being Morphism of b,a holds ii(*)f = f)
proof let b be Object of B;
b in O;
then reconsider bb = b as Element of C;
thus Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)ii = f
proof assume
A22: Hom(a,b)<>{};
let g be Morphism of a,b;
reconsider gg = g as Morphism of C by A5;
A23: dom gg = dom g by A2,FUNCT_1:49
.= a9 by A15,A22,CAT_1:5;
A24: cod id a9 = a9;
cod gg = cod g by A3,FUNCT_1:49
.= bb by A22,CAT_1:5;
then reconsider gg as Morphism of a9,bb by A23,CAT_1:4;
A25: dom g = a by A22,CAT_1:5;
hence g(*)ii = p.(g,ii) by A19,A20,A15,CAT_1:def 1
.= (the Comp of C).(gg,id a9) by A19,A20,A15,A4,A25,FUNCT_1:47
.= gg(*)id a9 by A23,A24,CAT_1:16
.= g by A23,CAT_1:22;
end;
assume
A26: Hom(b,a)<>{};
let g be Morphism of b,a;
reconsider gg = g as Morphism of C by A5;
A27: cod gg = cod g by A3,FUNCT_1:49
.= a9 by A15,A26,CAT_1:5;
A28: dom id a9 = a9;
dom gg = dom g by A2,FUNCT_1:49
.= bb by A26,CAT_1:5;
then reconsider gg as Morphism of bb,a9 by A27,CAT_1:4;
A29: cod g = a by A26,CAT_1:5;
hence ii(*)g = p.(ii,g) by A18,A20,A15,CAT_1:def 1
.= (the Comp of C).(id a9,gg) by A18,A20,A15,A4,A29,FUNCT_1:47
.= (id a9)(*)gg by A27,A28,CAT_1:16
.= g by A27,CAT_1:21;
end;
hence id a = id a9 by CAT_1:def 12;
end;
( for a,b being Object of B, a9,b9 being Object of C st a = a9 & b =
b9 holds Hom(a,b) c= Hom(a9,b9))& the Comp of B c= the Comp of C
by A4,A8,RELAT_1:59;
hence thesis by A14,Def4;
end;
theorem
for O being non empty Subset of the carrier of C, M being non empty
set, d,c being Function of M,O, p being PartFunc of [:M,M:],M, i being Function
of O,M st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O &
b in O} & d = (the Source of C)|M & c = (the Target of C)|M & p = (the Comp of
C)||M
holds CatStr(#O,M,d,c,p#) is full Subcategory of C
proof
let O be non empty Subset of the carrier of C, M be non empty set, d,c be
Function of M,O, p be PartFunc of [:M,M:],M, i be Function of O,M;
set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O};
assume that
A1: M = union H and
A2: d = (the Source of C)|M and
A3: c = (the Target of C)|M and
A4: p = (the Comp of C)||M;
set B = CatStr(#O,M,d,c,p#);
A5: now
let f be Morphism of B;
consider X being set such that
A6: f in X and
A7: X in H by A1,TARSKI:def 4;
ex a,b being Object of C st X = Hom(a,b) & a in O & b in O by A7;
hence f is Morphism of C by A6;
end;
A8: for a,b being Object of B, a9,b9 being Object of C st a = a9 & b = b9
holds Hom(a,b) = Hom(a9,b9)
proof
let a,b be Object of B, a9,b9 be Object of C such that
A9: a = a9 & b = b9;
now
let x be object;
thus x in Hom(a,b) implies x in Hom(a9,b9)
proof
assume
A10: x in Hom(a,b);
then reconsider f = x as Morphism of B;
reconsider f9 = f as Morphism of C by A5;
cod f = cod f9 by A3,FUNCT_1:49;
then
A11: b = cod f9 by A10,CAT_1:1;
dom f = dom f9 by A2,FUNCT_1:49;
then a = dom f9 by A10,CAT_1:1;
hence thesis by A9,A11;
end;
assume
A12: x in Hom(a9,b9);
then reconsider f9 = x as Morphism of C;
Hom(a9,b9) in H by A9;
then reconsider f = f9 as Morphism of B by A1,A12,TARSKI:def 4;
cod f = cod f9 by A3,FUNCT_1:49;
then
A13: cod f = b9 by A12,CAT_1:1;
dom f = dom f9 by A2,FUNCT_1:49;
then dom f = a9 by A12,CAT_1:1;
hence x in Hom(a,b) by A9,A13;
end;
hence thesis by TARSKI:2;
end;
reconsider B as Subcategory of C by Lm2,A1,A2,A3,A4;
B is full by A8;
hence thesis;
end;
theorem
for O being non empty Subset of the carrier of C, M being non empty
set , d,c being Function of M,O, p being PartFunc of [:M,M:],M
st CatStr(#O,M,d,c,p#) is full Subcategory of C
holds M =
union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} & d =
(the Source of C)|M & c = (the Target of C)|M & p = (the Comp of C)||M
proof
let O be non empty Subset of the carrier of C, M be non empty set, d,c be
Function of M,O, p be PartFunc of [:M,M:],M;
set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O};
set B = CatStr(#O,M,d,c,p#);
assume
A1: B is full Subcategory of C;
A2: for f being Morphism of B holds d.f = (the Source of C).f & c.f = (the
Target of C).f
proof
let f be Morphism of B;
reconsider f9 = f as Morphism of C by A1,Th4;
dom f = dom f9 & cod f = cod f9 by A1,Th5;
hence thesis;
end;
now
let x be object;
thus x in M implies x in union H
proof
assume x in M;
then reconsider f = x as Morphism of B;
reconsider f9 = f as Morphism of C by A1,Th4;
set a9 = dom f9, b9 = cod f9;
(the Source of B).f = (the Source of C).f9 & (the Target of B).f = (
the Target of C).f9 by A2;
then f in Hom(a9,b9) & Hom(a9,b9) in H;
hence thesis by TARSKI:def 4;
end;
assume x in union H;
then consider X being set such that
A3: x in X and
A4: X in H by TARSKI:def 4;
consider a9,b9 being Object of C such that
A5: X = Hom(a9,b9) and
A6: a9 in O & b9 in O by A4;
reconsider a = a9, b = b9 as Object of B by A6;
Hom(a,b) = Hom(a9,b9) by A1,Def6;
hence x in M by A3,A5;
end;
hence
M = union H by TARSKI:2;
then reconsider
d9 = (the Source of C)|M, c9 = (the Target of C)|M as Function of
M,O by Th16;
set p9 = (the Comp of C)||M;
now
let f be Element of M;
d.f = (the Source of C).f by A2;
hence d.f = d9.f by FUNCT_1:49;
end;
hence d = (the Source of C)|M by FUNCT_2:63;
now
let f be Element of M;
c.f = (the Target of C).f by A2;
hence c.f = c9.f by FUNCT_1:49;
end;
hence c = (the Target of C)|M by FUNCT_2:63;
now
A7: dom p c= [:M,M:] by RELAT_1:def 18;
A8: dom p9 = (dom the Comp of C) /\ [:M,M:] by RELAT_1:61;
the Comp of B c= the Comp of C by A1,Def4;
then dom p c= dom the Comp of C by GRFUNC_1:2;
then
A9: dom p c= dom p9 by A7,A8,XBOOLE_1:19;
dom p9 c= dom p
proof
let x be object;
assume
A10: x in dom p9;
then x in [:M,M:] by A8,XBOOLE_0:def 4;
then consider g,f being Element of M such that
A11: x = [g,f] by DOMAIN_1:1;
reconsider f,g as Morphism of B;
reconsider f9 = f,g9 = g as Morphism of C by A1,Th4;
[g,f] in dom the Comp of C by A8,A10,A11,XBOOLE_0:def 4;
then
A12: dom g9 = cod f9 by CAT_1:15;
cod f = cod f9 & dom g = dom g9 by A1,Th5;
hence thesis by A1,A11,A12,CAT_1:15;
end;
hence dom p = dom p9 by A9,XBOOLE_0:def 10;
let x be object;
assume
A13: x in dom p;
then consider g,f being Element of M such that
A14: x = [g,f] by A7,DOMAIN_1:1;
reconsider f,g as Morphism of B;
A15: dom g = cod f by A1,A13,A14,CAT_1:15;
reconsider f9 = f,g9 = g as Morphism of C by A1,Th4;
A16: cod f = cod f9 & dom g = dom g9 by A1,Th5;
p.x = p.(g,f) by A14;
hence p.x = g(*)f by A1,A15,CAT_1:16
.= g9(*)f9 by A1,A15,Th7
.= (the Comp of C).(g9,f9) by A16,A1,A13,A14,CAT_1:15,16
.= p9.x by A9,A13,A14,FUNCT_1:47;
end;
hence p = (the Comp of C)||M by FUNCT_1:2;
end;
:: Product of Categories
definition
let C,D;
func [:C,D:] -> Category equals
CatStr (# [:the carrier of C,the carrier of D:],
[:the carrier' of C,the carrier' of D:],
[:the Source of C,the Source of D:],
[:the Target of C,the Target of D:],
|:the Comp of C, the Comp of D:| #);
coherence
proof
set O = [:the carrier of C,the carrier of D:],
M = [:the carrier' of C,the carrier' of D:],
d = [:the Source of C,the Source of D:],
c = [:the Target of C,the Target of D:],
p = |:the Comp of C, the Comp of D:|;
A1: for f,g being Element of M st d.g = c.f holds
[g`1,f`1] in dom(the Comp of C) & [g`2,f`2] in dom(the Comp of D)
proof
let f,g be Element of M;
A2: d.(g`1,g`2) = [(the Source of C).g`1,(the Source of D).g`2] & c.(f`1
,f`2) = [(the Target of C).f`1,(the Target of D).f`2] by FUNCT_3:75;
assume
A3: d.g = c.f;
g = [g`1,g`2] & f = [f`1,f`2] by MCART_1:21;
then
dom(g`1) = cod(f`1) &
dom(g`2) = cod(f`2) by A2,A3,XTUPLE_0:1;
hence thesis by CAT_1:def 6;
end;
A4: for f,g being Element of M st [g,f] in dom(p)
holds dom(g`1) = cod(f`1) & dom(g`2) = cod(f`2)
proof
let f,g be Element of M;
assume
A5: [g,f] in dom(p);
g = [g`1,g`2] & f = [f`1,f`2] by MCART_1:21;
then [g`1,f`1] in dom(the Comp of C) & [g`2,f`2] in dom(the Comp of D)
by A5,FUNCT_4:54;
hence thesis by CAT_1:def 6;
end;
set B = CatStr(#O,M,d,c,p#);
A6: B is Category-like
proof
let ff,gg be Morphism of B;
reconsider f = ff, g=gg as Element of M;
A7: g = [g`1,g`2] & f = [f`1,f`2] by MCART_1:21;
thus [gg,ff] in dom(the Comp of B) implies
dom gg = cod ff
proof
A8: d.(g`1,g`2) = [dom(g`1),dom(g`2)] & c.(
f`1,f`2) = [cod(f`1),cod(f`2)] by FUNCT_3:75;
assume
A9: [gg,ff] in dom(the Comp of B);
then dom(g`1) = cod(f`1) by A4;
hence thesis by A4,A7,A9,A8;
end;
assume dom gg = cod ff;
then [g`1,f`1] in dom(the Comp of C) & [g`2,f`2] in dom(the Comp of D)
by A1;
hence thesis by A7,FUNCT_4:54;
end;
A10: for f,g being Morphism of B
holds [g,f] in dom(the Comp of B) iff dom g = cod f by A6;
A11: for f,g being Element of M st d.g = c.f
holds p.(g,f) = [(the Comp of C).(g`1,f`1),(the Comp of D).(g`2,f`2)]
proof
let f,g be Element of M;
reconsider ff=f, gg=g as Morphism of B;
assume d.g = c.f;
then
A12: dom gg = cod ff;
g = [g`1,g`2] & f = [f`1,f`2] by MCART_1:21;
hence thesis by A12,A10,FUNCT_4:55;
end;
A13: for f,g being Element of M st d.g = c.f
holds d.(p.(g,f)) = d.f & c.(p.(g,f)) = c.g
proof
let f,g be Element of M;
reconsider ff=f, gg=g as Morphism of B;
A14: f = [f`1,f`2] & d.(f`1,f`2) = [dom(f`1),dom(f`2)]
by FUNCT_3:75,MCART_1:21;
assume
A15: d.g = c.f;
then
A16: (the Comp of C).[g`1,f`1] in the carrier' of C by A1,PARTFUN1:4;
then
A17: (the Comp of C).(g`1,f`1) in dom(the Source of C) by FUNCT_2:def 1;
dom gg = cod ff by A15;
then
A18: [gg,ff] in dom(p) by A6;
then
A19: dom(g`1) = cod(f`1) by A4;
then [g`1,f`1] in dom the Comp of C by CAT_1:def 6;
then
A20: (the Comp of C).(g`1,f`1) = (g`1)(*)(f`1) by CAT_1:def 1;
A21: dom((g`1)(*)(f`1)) = dom(f`1) by A19,CAT_1:def 7;
A22: (the Comp of D).[g`2,f`2] in the carrier' of D by A1,A15,PARTFUN1:4;
then
A23: (the Comp of D).(g`2,f`2) in dom(the Source of D) by FUNCT_2:def 1;
A24: dom(g`2) = cod(f`2) by A4,A18;
then [g`2,f`2] in dom the Comp of D by CAT_1:def 6;
then
A25: (the Comp of D).(g`2,f`2) = (g`2)(*)(f`2) by CAT_1:def 1;
A26: dom((g`2)(*)(f`2)) = dom(f`2) by A24,CAT_1:def 7;
thus d.(p.(g,f)) = d.((the Comp of C).(g`1,f`1),(the Comp of D).(g`2,f`2
)) by A11,A15
.= d.f by A14,A21,A26,A17,A23,A20,A25,FUNCT_3:def 8;
A27: g = [g`1,g`2] & c.(g`1,g`2) = [(the Target of C).g`1,(the Target of
D).g`2] by FUNCT_3:75,MCART_1:21;
A28: cod((g`2)(*)(f`2)) = cod(g`2) by A24,CAT_1:def 7;
A29: cod((g`1)(*)(f`1)) = cod(g`1) by A19,CAT_1:def 7;
A30: (the Comp of D).(g`2,f`2) in dom(the Target of D) by A22,FUNCT_2:def 1;
A31: (the Comp of C).(g`1,f`1) in dom(the Target of C) by A16,FUNCT_2:def 1;
thus c.(p.(g,f))
= c.((the Comp of C).(g`1,f`1),(the Comp of D).(g`2,f`2)) by A11,A15
.= c.g by A27,A29,A28,A31,A30,A20,A25,FUNCT_3:def 8;
end;
A32: B is transitive
proof
let ff,gg be Morphism of B;
reconsider f=ff, g=gg as Element of M;
assume
A33: dom gg = cod ff;
then
A34: (the Comp of B).(gg,ff) = gg(*)ff by A10,CAT_1:def 1;
thus dom(gg(*)ff) = dom ff by A13,A33,A34;
thus cod(gg(*)ff) = cod gg by A13,A33,A34;
end;
A35: B is associative
proof
let ff,gg,hh be Morphism of B;
reconsider f=ff, g=gg, h=hh as Element of M;
assume that
A36: dom hh = cod gg and
A37: dom gg = cod ff;
A38: (the Comp of C).[h`1,g`1] in the carrier' of C & (the Comp of D).[h
`2,g`2] in the carrier' of D by A1,A36,PARTFUN1:4;
(the Comp of C).[g`1,f`1] in the carrier' of C & (the Comp of D).[g
`2,f`2] in the carrier' of D by A1,A37,PARTFUN1:4;
then reconsider
pgf = [(the Comp of C).[g`1,f`1],(the Comp of D).[g`2,f`2]],
phg = [(the Comp of C).[h`1,g`1],(the Comp of D).[h`2,g`2]]
as Element of M by A38,ZFMISC_1:87;
set pgf2 = pgf`2, phg2 = phg`2;
set pgf1 = pgf`1, phg1 = phg`1;
A39: p.(g,f) = [(the Comp of C).(g`1,f`1),(the Comp of D).(g`2,f`2)]
by A11,A37;
A40: d.h = c.(p.(g,f)) by A13,A36,A37;
A41: p.(h,g) = [(the Comp of C).(h`1,g`1),(the Comp of D).(h`2,g`2)]
by A11,A36;
[h`2,g`2] in dom(the Comp of D) by A1,A36;
then
A42: dom(h`2) = cod(g`2) by CAT_1:def 6;
[h`1,g`1] in dom(the Comp of C) by A1,A36;
then
A43: dom(h`1) = cod(g`1) by CAT_1:def 6;
[g`2,f`2] in dom(the Comp of D) by A1,A37;
then
A44: dom(g`2) = cod(f`2) by CAT_1:def 6;
[g`1,f`1] in dom(the Comp of C) by A1,A37;
then
A45: dom(g`1) = cod(f`1) by CAT_1:def 6;
A46: d.(p.(h,g)) = c.f by A13,A36,A37;
A47: pgf`1 = (the Comp of C).(g`1,f`1) &
phg`1 = (the Comp of C).(h`1,g`1);
A48: pgf`2 = (the Comp of D).(g`2,f`2) &
phg`2 = (the Comp of D).(h`2,g`2);
A49: h`2(*)(g`2(*)f`2) = h`2(*)g`2(*)f`2 by A42,A44,CAT_1:def 8;
A50: gg(*)ff = p.(g,f) by A37,A10,CAT_1:def 1;
then
A51: cod(gg(*)ff) = dom hh by A13,A36,A37;
A52: hh(*)gg = p.(h,g) by A36,A10,CAT_1:def 1;
then
A53: dom(hh(*)gg) = cod ff by A13,A36,A37;
A54: cod(g`1(*)f`1) = cod g`1 by A45,CAT_1:def 7;
A55: pgf1 = g`1(*)f`1 by A47,A45,CAT_1:16;
A56: cod(g`2(*)f`2) = cod g`2 by A44,CAT_1:def 7;
pgf2 = g`2(*)f`2 by A48,A44,CAT_1:16;
then
A57: (the Comp of D).(h`2, pgf2) = h`2(*)(g`2(*)f`2) by A42,A56,CAT_1:16;
A58: dom(h`1(*)g`1) = dom g`1 by A43,CAT_1:def 7;
A59: phg1 = h`1(*)g`1 by A47,A43,CAT_1:16;
A60: dom(h`2(*)g`2) = dom g`2 by A42,CAT_1:def 7;
phg2 = h`2(*)g`2 by A48,A42,CAT_1:16;
then
A61: (the Comp of D).(phg2,f`2) = h`2(*)g`2(*)f`2 by A44,A60,CAT_1:16;
thus hh(*)(gg(*)ff)
= p.(h,p.(g,f)) by A51,A50,A10,CAT_1:def 1
.= [(the Comp of C).(h`1,pgf1), (the Comp of D).(h`2, pgf2)]
by A40,A11,A39
.= [h`1(*)(g`1(*)f`1),h`2(*)(g`2(*)f`2)] by A55,A57,A43,A54,CAT_1:16
.= [h`1(*)g`1(*)f`1,h`2(*)g`2(*)f`2] by A43,A45,A49,CAT_1:def 8
.= [(the Comp of C).(phg1,f`1), (the Comp of D).(phg2,f`2)]
by A59,A61,A45,A58,CAT_1:16
.= p.(p.(h,g),f) by A46,A11,A41
.= (hh(*)gg)(*)ff by A53,A10,A52,CAT_1:def 1;
end;
A62: B is reflexive
proof let b be Element of B;
reconsider bb=b as Element of O;
reconsider ii = [id bb`1, id bb`2] as Morphism of B;
A63: cod ii = c.(id bb`1, id bb`2)
.= [cod id bb`1,cod id bb`2] by FUNCT_3:75
.= [bb`1,cod id bb`2]
.= [bb`1,bb`2]
.= bb by MCART_1:21;
dom ii = d.(id bb`1, id bb`2)
.= [dom id bb`1,dom id bb`2] by FUNCT_3:75
.= [bb`1,dom id bb`2]
.= [bb`1,bb`2]
.= bb by MCART_1:21;
then [id bb`1,id bb`2] in Hom(b,b) by A63;
hence Hom(b,b)<>{};
end;
B is with_identities
proof let a be Element of B;
reconsider aa=a as Element of O;
reconsider ii = [id aa`1, id aa`2] as Morphism of B;
A64: cod ii = c.(id aa`1, id aa`2)
.= [cod id aa`1,cod id aa`2] by FUNCT_3:75
.= [aa`1,cod id aa`2]
.= [aa`1,aa`2]
.= aa by MCART_1:21;
A65: dom ii = d.(id aa`1, id aa`2)
.= [dom id aa`1,dom id aa`2] by FUNCT_3:75
.= [aa`1,dom id aa`2]
.= [aa`1,aa`2]
.= aa by MCART_1:21;
then reconsider ii = [id aa`1, id aa`2] as Morphism of a,a by A64,CAT_1:4;
take ii;
let b be Element of B;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g
proof assume
A66: Hom(a,b)<>{};
let g be Morphism of a,b;
reconsider gg = g as Element of M;
cod ii = dom g by A66,A64,CAT_1:5;
then
A67: [g,ii] in dom p by A6;
then
A68: dom gg`1 = cod [id aa`1, id aa`2]`1 by A4
.= cod id aa`1;
A69: (the Comp of C).(gg`1,id aa`1) = (gg`1)(*)id aa`1 by A68,CAT_1:16
.= gg`1 by A68,CAT_1:22;
A70: dom gg`2 = cod [id aa`1, id aa`2]`2 by A4,A67
.= cod id aa`2;
A71: (the Comp of D).(gg`2,id aa`2) = (gg`2)(*)id aa`2 by A70,CAT_1:16
.= gg`2 by A70,CAT_1:22;
A72: cod ii = dom g by A64,A66,CAT_1:5;
then [g,ii] in dom the Comp of B by A6;
hence g(*)ii = p.(g,ii) by CAT_1:def 1
.= [(the Comp of C).(gg`1,[id aa`1, id aa`2]`1),
(the Comp of D).(gg`2,[id aa`1, id aa`2]`2)]
by A11,A72
.= g by A69,A71,MCART_1:21;
end;
assume
A73: Hom(b,a)<>{};
let g be Morphism of b,a;
reconsider gg = g as Element of M;
dom ii = cod g by A73,A65,CAT_1:5;
then
A74: [ii,g] in dom p by A6;
then
A75: cod gg`1 = dom [id aa`1, id aa`2]`1 by A4
.= dom id aa`1;
A76: (the Comp of C).(id aa`1,gg`1) = (id aa`1)(*)gg`1 by A75,CAT_1:16
.= gg`1 by A75,CAT_1:21;
A77: cod gg`2 = dom [id aa`1, id aa`2]`2 by A4,A74
.= dom id aa`2;
A78: (the Comp of D).(id aa`2,gg`2) = (id aa`2)(*)gg`2 by A77,CAT_1:16
.= gg`2 by A77,CAT_1:21;
A79: dom ii = cod g by A65,A73,CAT_1:5;
then [ii,g] in dom the Comp of B by A6;
hence ii(*)g = p.(ii,g) by CAT_1:def 1
.= [(the Comp of C).([id aa`1, id aa`2]`1,gg`1),
(the Comp of D).([id aa`1, id aa`2]`2,gg`2)]
by A11,A79
.= g by A76,A78,MCART_1:21;
end;
hence thesis by A6,A32,A35,A62;
end;
end;
theorem
the carrier of [:C,D:] = [:the carrier of C,the carrier of D:] & the
carrier' of [:C,D:] = [:the carrier' of C,the carrier' of D:] & the Source of
[:C,D:] = [:the Source of C,the Source of D:] & the Target of [:C,D:] = [:the
Target of C,the Target of D:] & the Comp of [:C,D:] = |:the Comp of C, the Comp
of D:|;
definition
let C,D;
let c be Object of C;
let d be Object of D;
redefine func [c,d] -> Object of [:C,D:]; :: redefines [ (TARSKI, definition)
coherence
proof
thus [c,d] is Object of [:C,D:];
end;
end;
::$CT
theorem
for cd being Object of [:C,D:] ex c being Object of C, d being Object
of D st cd = [c,d] by DOMAIN_1:1;
definition
let C,D;
let f be Morphism of C;
let g be Morphism of D;
redefine func [f,g] -> Morphism of [:C,D:]; :: redefines [ (TARSKI, definition)
coherence
proof
thus [f,g] is Morphism of [:C,D:];
end;
end;
::$CT
theorem
for fg being Morphism of [:C,D:] ex f being (Morphism of C), g being
Morphism of D st fg = [f,g] by DOMAIN_1:1;
theorem Th22:
for f being Morphism of C for g being Morphism of D
holds dom [f,g] = [dom f,dom g] & cod [f,g] = [cod f,cod g]
proof
let f be Morphism of C;
let g be Morphism of D;
thus dom [f,g] = [:the Source of C,the Source of D:].(f,g)
.= [dom f,dom g] by FUNCT_3:75;
thus cod [f,g] = [:the Target of C,the Target of D:].(f,g)
.= [cod f,cod g] by FUNCT_3:75;
end;
theorem Th23:
for f,f9 being Morphism of C for g,g9 being Morphism of D st dom
f9 = cod f & dom g9 = cod g holds [f9,g9](*)[f,g] = [f9(*)f,g9(*)g]
proof
let f,f9 be Morphism of C;
let g,g9 be Morphism of D;
assume that
A1: dom f9 = cod f and
A2: dom g9 = cod g;
A3: [f9,f] in dom(the Comp of C) & [g9,g] in dom(the Comp of D) by A1,A2,
CAT_1:15;
dom [f9,g9] = [dom f9,dom g9] & cod [f,g] = [cod f,cod g] by Th22;
hence
[f9,g9](*)[f,g] = |:the Comp of C, the Comp of D:|.([f9,g9],[f,g])
by A1,A2,CAT_1:16
.= [(the Comp of C).(f9,f),(the Comp of D).(g9,g)] by A3,FUNCT_4:def 3
.= [f9(*)f,(the Comp of D).(g9,g)] by A1,CAT_1:16
.= [f9(*)f,g9(*)g] by A2,CAT_1:16;
end;
theorem Th24:
for f,f9 being Morphism of C for g,g9 being Morphism of D st dom
[f9,g9] = cod [f,g] holds [f9,g9](*)[f,g] = [f9(*)f,g9(*)g]
proof
let f,f9 be Morphism of C;
let g,g9 be Morphism of D such that
A1: dom [f9,g9] = cod [f,g];
[dom f9,dom g9] = dom [f9,g9] & cod [f,g] = [cod f,cod g] by Th22;
then dom f9 = cod f & dom g9 = cod g by A1,XTUPLE_0:1;
hence thesis by Th23;
end;
theorem Th25:
for c being Object of C, d being Object of D holds id [c,d] = [id c,id d]
proof
let c being Object of C;
let d being Object of D;
A1: dom [id c,id d] = [dom id c,dom id d] by Th22
.= [c,dom id d]
.= [c,d];
cod [id c,id d] = [cod id c,cod id d] by Th22
.= [c,cod id d]
.= [c,d];
then reconsider m = [id c,id d] as Morphism of [c,d],[c,d] by A1,CAT_1:4;
for b being Object of [:C,D:] holds
(Hom([c,d],b) <> {} implies
for f being Morphism of [c,d],b holds f(*)[id c,id d] = f)
& (Hom(b,[c,d]) <> {} implies
for f being Morphism of b,[c,d] holds [id c,id d](*)f = f)
proof let b be Object of [:C,D:];
thus Hom([c,d],b) <> {} implies
for f being Morphism of [c,d],b holds f(*)[id c,id d] = f
proof assume
A2: Hom([c,d],b) <> {};
let f be Morphism of [c,d],b;
consider fc being (Morphism of C), fd being Morphism of D such that
A3: f = [fc,fd] by DOMAIN_1:1;
A4: [c,d] = dom f by A2,CAT_1:5 .= [dom fc,dom fd] by A3,Th22;
then
A5: c = dom fc by XTUPLE_0:1;
then
A6: cod id c = dom fc;
A7: d = dom fd by A4,XTUPLE_0:1;
then cod id d = dom fd;
hence f(*)[id c,id d] = [fc(*)id c,fd(*)id d] by A3,A6,Th23
.= [fc,fd(*)id d] by A5,CAT_1:22
.= f by A3,A7,CAT_1:22;
end;
assume
A8: Hom(b,[c,d]) <> {};
let f be Morphism of b,[c,d];
consider fc being (Morphism of C), fd being Morphism of D such that
A9: f = [fc,fd] by DOMAIN_1:1;
A10: [c,d] = cod f by A8,CAT_1:5 .= [cod fc,cod fd] by A9,Th22;
then
A11: c = cod fc by XTUPLE_0:1;
then
A12: dom id c = cod fc;
A13: d = cod fd by A10,XTUPLE_0:1;
then dom id d = cod fd;
hence [id c,id d](*)f = [(id c)(*)fc,(id d)(*)fd] by A9,A12,Th23
.= [fc,(id d)(*)fd] by A11,CAT_1:21
.= f by A9,A13,CAT_1:21;
end;
then m = id[c,d] by CAT_1:def 12;
hence thesis;
end;
theorem
for c,c9 being Object of C, d,d9 being Object of D
holds Hom([c,d],[c9,d9]) = [:Hom(c,c9),Hom(d,d9):]
proof
let c,c9 be Object of C, d,d9 be Object of D;
now
let x be object;
thus x in Hom([c,d],[c9,d9]) implies x in [:Hom(c,c9),Hom(d,d9):]
proof
assume
A1: x in Hom([c,d],[c9,d9]);
then reconsider fg = x as Morphism of [c,d],[c9,d9] by CAT_1:def 5;
A2: dom fg = [c,d] by A1,CAT_1:1;
A3: cod fg = [c9,d9] by A1,CAT_1:1;
consider x1,x2 being object such that
A4: x1 in the carrier' of C and
A5: x2 in the carrier' of D and
A6: fg = [x1,x2] by ZFMISC_1:def 2;
reconsider g = x2 as Morphism of D by A5;
reconsider f = x1 as Morphism of C by A4;
A7: cod fg = [cod f,cod g] by A6,Th22;
then
A8: cod f = c9 by A3,XTUPLE_0:1;
A9: cod g = d9 by A3,A7,XTUPLE_0:1;
A10: dom fg = [dom f,dom g] by A6,Th22;
then dom g = d by A2,XTUPLE_0:1;
then
A11: g in Hom(d,d9) by A9;
dom f = c by A2,A10,XTUPLE_0:1;
then f in Hom(c,c9) by A8;
hence thesis by A6,A11,ZFMISC_1:87;
end;
assume x in [:Hom(c,c9),Hom(d,d9):];
then consider x1,x2 being object such that
A12: x1 in Hom(c,c9) and
A13: x2 in Hom(d,d9) and
A14: x = [x1,x2] by ZFMISC_1:def 2;
reconsider g = x2 as Morphism of d,d9 by A13,CAT_1:def 5;
reconsider f = x1 as Morphism of c,c9 by A12,CAT_1:def 5;
cod f = c9 & cod g = d9 by A12,A13,CAT_1:1;
then
A15: cod [f,g] = [c9,d9] by Th22;
dom f = c & dom g = d by A12,A13,CAT_1:1;
then dom [f,g] = [c,d] by Th22;
hence x in Hom([c,d],[c9,d9]) by A14,A15;
end;
hence thesis by TARSKI:2;
end;
theorem
for c,c9 being Object of C, f being Morphism of c,c9, d,d9 being
Object of D, g being Morphism of d,d9 st Hom(c,c9) <> {} & Hom(d,d9) <> {}
holds [f,g] is Morphism of [c,d],[c9,d9]
proof
let c,c9 be Object of C, f be Morphism of c,c9, d,d9 be Object of D, g be
Morphism of d,d9;
assume
A1: Hom(c,c9) <> {} & Hom(d,d9) <> {};
then cod f = c9 & cod g = d9 by CAT_1:5;
then
A2: cod [f,g] = [c9,d9] by Th22;
dom f = c & dom g = d by A1,CAT_1:5;
then dom [f,g] = [c,d] by Th22;
hence thesis by A2,CAT_1:4;
end;
:: Bifunctors
definition
let C,C9,D;
let S being Functor of [:C,C9:],D;
let m be Morphism of C;
let m9 be Morphism of C9;
redefine func S.(m,m9) -> Morphism of D; :: redefines . (BINOP_1, definition)
coherence
proof
S.(m,m9) = S.[m,m9];
hence thesis;
end;
end;
theorem Th28:
for S being Functor of [:C,C9:],D, c being Object of C holds (
curry S).(id c) is Functor of C9,D
proof
let S be Functor of [:C,C9:],D, c be Object of C;
reconsider S9 = S as Function of [:the carrier' of C,the carrier' of C9:],
the carrier' of D;
reconsider T = (curry S9).(id c) as Function of the carrier' of C9,the
carrier' of D;
now
thus for c9 being Object of C9 ex d being Object of D st T.(id c9) = id d
proof
let c9 be Object of C9;
consider d being Object of D such that
A1: S.(id [c,c9]) = id d by CAT_1:62;
take d;
thus T.(id c9) = S.(id c,id c9) by FUNCT_5:69
.= id d by A1,Th25;
end;
A2: dom id c = c & cod id c = c;
thus for f being Morphism of C9 holds T.(id dom f) = id dom (T.f) & T.(id
cod f) = id cod (T.f)
proof
let f be Morphism of C9;
thus T.(id dom f) = S.(id c,id dom f) by FUNCT_5:69
.= S.(id [c,dom f]) by Th25
.= S.(id [dom id c,dom f])
.= S.(id dom [id c,f]) by Th22
.= id dom (S.(id c,f)) by CAT_1:63
.= id dom (T.f) by FUNCT_5:69;
thus T.(id cod f) = S.(id c,id cod f) by FUNCT_5:69
.= S.(id [c,cod f]) by Th25
.= S.(id [cod id c,cod f])
.= S.(id cod [id c,f]) by Th22
.= id cod (S.(id c,f)) by CAT_1:63
.= id cod (T.f) by FUNCT_5:69;
end;
let f,g be Morphism of C9 such that
A3: dom g = cod f;
Hom(c,c) <> {};
then
A4: (id c)*(id c) = (id c)(*)(id c) by CAT_1:def 13;
A5: dom [id c,g] = [dom id c,dom g] & cod [id c,f] = [cod id c, cod f] by Th22;
thus T.(g(*)f) = S.((id c)*(id c),g(*)f) by FUNCT_5:69
.= S.([id c,g](*)[id c,f]) by A3,A2,A4,Th23
.= (S.(id c,g))(*)(S.(id c,f)) by A3,A5,CAT_1:64
.= (T.g)(*)(S.(id c,f)) by FUNCT_5:69
.= (T.g)(*)(T.f) by FUNCT_5:69;
end;
hence thesis by CAT_1:61;
end;
theorem Th29:
for S being Functor of [:C,C9:],D, c9 being Object of C9 holds (
curry' S).(id c9) is Functor of C,D
proof
let S be Functor of [:C,C9:],D, c9 be Object of C9;
reconsider S9 = S as Function of [:the carrier' of C,the carrier' of C9:],
the carrier' of D;
reconsider T = (curry' S9).(id c9) as Function of the carrier' of C,the
carrier' of D;
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 d being Object of D such that
A1: S.(id [c,c9]) = id d by CAT_1:62;
take d;
thus T.(id c) = S.(id c,id c9) by FUNCT_5:70
.= id d by A1,Th25;
end;
A2: dom id c9 = c9 & cod id c9 = c9;
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) = S.(id dom f,id c9) by FUNCT_5:70
.= S.(id [dom f,c9]) by Th25
.= S.(id [dom f,dom id c9])
.= S.(id dom [f,id c9]) by Th22
.= id dom (S.(f,id c9)) by CAT_1:63
.= id dom (T.f) by FUNCT_5:70;
thus T.(id cod f) = S.(id cod f,id c9) by FUNCT_5:70
.= S.(id [cod f,c9]) by Th25
.= S.(id [cod f,cod id c9])
.= S.(id cod [f,id c9]) by Th22
.= id cod (S.(f,id c9)) by CAT_1:63
.= id cod (T.f) by FUNCT_5:70;
end;
let f,g be Morphism of C such that
A3: dom g = cod f;
Hom(c9,c9) <> {};
then
A4: (id c9)*(id c9) = (id c9)(*)(id c9) by CAT_1:def 13;
A5: dom [g,id c9] = [dom g,dom id c9] & cod [f,id c9] = [cod f,cod id c9]
by Th22;
thus T.(g(*)f) = S.(g(*)f,(id c9)*(id c9)) by FUNCT_5:70
.= S.([g,id c9](*)[f,id c9]) by A3,A2,A4,Th23
.= (S.(g,id c9))(*)(S.(f,id c9)) by A3,A5,CAT_1:64
.= (T.g)(*)(S.(f,id c9)) by FUNCT_5:70
.= (T.g)(*)(T.f) by FUNCT_5:70;
end;
hence thesis by CAT_1:61;
end;
:: Partial Functors
definition
let C,C9,D;
let S be Functor of [:C,C9:],D, c be Object of C;
func S?-c -> Functor of C9,D equals
(curry S).(id c);
coherence by Th28;
end;
theorem
for S being Functor of [:C,C9:],D, c being Object of C, f being
Morphism of C9 holds (S?-c).f = S.(id c,f) by FUNCT_5:69;
theorem
for S being Functor of [:C,C9:],D, c being Object of C, c9 being
Object of C9 holds (Obj S?-c).c9 = (Obj S).(c,c9)
proof
let S be Functor of [:C,C9:],D, c be Object of C, c9 be Object of C9;
(S?-c).(id c9) = S.(id c,id c9) by FUNCT_5:69
.= S.(id [c,c9]) by Th25
.= id ((Obj S).[c,c9]) by CAT_1:68;
hence thesis by CAT_1:67;
end;
definition
let C,C9,D;
let S be Functor of [:C,C9:],D, c9 be Object of C9;
func S-?c9 -> Functor of C,D equals
(curry' S).(id c9);
coherence by Th29;
end;
theorem
for S being Functor of [:C,C9:],D, c9 being Object of C9, f being
Morphism of C holds (S-?c9).f = S.(f,id c9) by FUNCT_5:70;
theorem
for S being Functor of [:C,C9:],D, c being Object of C, c9 being
Object of C9 holds (Obj S-?c9).c = (Obj S).(c,c9)
proof
let S be Functor of [:C,C9:],D, c be Object of C, c9 be Object of C9;
(S-?c9).(id c) = S.(id c,id c9) by FUNCT_5:70
.= S.(id [c,c9]) by Th25
.= id ((Obj S).[c,c9]) by CAT_1:68;
hence thesis by CAT_1:67;
end;
theorem
for L being Function of the carrier of C,Funct(B,D), M being Function
of the carrier of B,Funct(C,D) st ( for c being Object of C,b being Object of B
holds (M.b).(id c) = (L.c).(id b) ) & ( for f being Morphism of B for g being
Morphism of C
holds ((M.(cod f)).g)(*)((L.(dom g)).f) = ((L.(cod g)).f)(*)((M.(dom
f)).g) ) ex S being Functor of [:B,C:],D st for f being Morphism of B for g
being Morphism of C holds S.(f,g) = ((L.(cod g)).f)(*)((M.(dom f)).g)
proof
deffunc Mor(Category) = the carrier' of $1;
let L be Function of the carrier of C,Funct(B,D), M be Function of the
carrier of B,Funct(C,D) such that
A1: for c being Object of C, b being Object of B holds (M.b).(id c) = (L
.c).(id b) and
A2: for f being Morphism of B for g being Morphism of C holds ((M.(cod f
)).g)(*)((L.(dom g)).f) = ((L.(cod g)).f)(*)((M.(dom f)).g);
deffunc F(Element of Mor(B), Element of Mor(C))
= ((L.(cod $2)).$1)(*)((M.(dom
$1)).$2);
consider S being Function of [:Mor(B),Mor(C):],Mor(D) such that
A3: for f being Morphism of B for g being Morphism of C holds S.(f,g) =
F(f,g) from BINOP_1:sch 4;
reconsider T = S as Function of Mor([:B,C:]),Mor(D);
now
thus for bc being Object of [:B,C:] ex d being Object of D st T.(id bc) =
id d
proof
let bc be Object of [:B,C:];
consider b being Object of B, c being Object of C such that
A4: bc = [b,c] by DOMAIN_1:1;
consider d being Object of D such that
A5: (L.c).(id b) = id d by CAT_1:62;
take d;
Hom(d,d) <> {};
then
A6: (id d)*(id d) = (id d)(*)(id d) by CAT_1:def 13;
A7: cod id c = c & dom id b = b;
(L.c).(id b) = (M.b).(id c) by A1;
then T.(id b,id c) = id d by A3,A5,A6,A7;
hence thesis by A4,Th25;
end;
thus for fg being Morphism of [:B,C:] holds T.(id dom fg) = id dom (T.fg)
& T.(id cod fg) = id cod (T.fg)
proof
let fg be Morphism of [:B,C:];
consider f being (Morphism of B), g being Morphism of C such that
A8: fg = [f,g] by DOMAIN_1:1;
set b = dom f, c = dom g;
set g9 = id c, f9= id b;
A9: Hom(dom ((M.b).g),dom ((M.b).g)) <> {};
id dom ((L.(cod g)).f) = (L.(cod g)).(id dom f) by CAT_1:63
.= (M.(dom f)).(id cod g) by A1
.= id cod ((M.(dom f)).g) by CAT_1:63;
then
A10: dom ((L.(cod g)).f) = cod ((M.(dom f)).g) by CAT_1:59;
thus T.(id (dom fg)) = S.(id [b,c]) by A8,Th22
.= S.(id b,id c) by Th25
.= ((L.(cod g9)).f9)(*)((M.(dom f9)).g9) by A3
.= ((L.c).f9)(*)((M.(dom f9)).g9)
.= ((L.c).f9)(*)((M.b).g9)
.= ((M.b).g9)(*)((M.b).g9) by A1
.= (id dom ((M.b).g))(*)((M.b).g9) by CAT_1:63
.= (id dom ((M.b).g))(*)(id dom((M.b).g)) by CAT_1:63
.= (id dom ((M.b).g))*(id dom((M.b).g)) by A9,CAT_1:def 13
.= id dom (((L.(cod g)).f)(*)((M.(dom f)).g)) by A10,CAT_1:17
.= id dom (S.(f,g)) by A3
.= id dom(T.fg) by A8;
set b = cod f, c = cod g;
set g9 = id c, f9= id b;
A11: Hom(cod ((L.c).f),cod ((L.c).f)) <> {};
thus T.(id (cod fg)) = S.(id [b,c]) by A8,Th22
.= S.(id b,id c) by Th25
.= ((L.(cod g9)).f9)(*)((M.(dom f9)).g9) by A3
.= ((L.c).f9)(*)((M.(dom f9)).g9)
.= ((L.c).f9)(*)((M.(cod f)).g9)
.= ((L.c).f9)(*)((L.c).f9) by A1
.= (id cod (((L.c).f))(*)((L.c).f9)) by CAT_1:63
.= (id cod ((L.c).f))(*)(id cod((L.c).f)) by CAT_1:63
.= (id cod ((L.c).f))*(id cod ((L.c).f)) by A11,CAT_1:def 13
.= id cod (((L.(cod g)).f)(*)((M.(dom f)).g)) by A10,CAT_1:17
.= id cod (S.(f,g)) by A3
.= id cod (T.fg) by A8;
end;
let fg1,fg2 be Morphism of [:B,C:] such that
A12: dom fg2 = cod fg1;
consider f1 being (Morphism of B), g1 being Morphism of C such that
A13: fg1 = [f1,g1] by DOMAIN_1:1;
consider f2 being (Morphism of B), g2 being Morphism of C such that
A14: fg2 = [f2,g2] by DOMAIN_1:1;
A15: [cod f1,cod g1] = cod fg1 by A13,Th22;
set L1 = L.(cod g1), L2 = L.(cod g2), M1 = M.(dom f1), M2 = M.(dom f2);
A16: [dom f2,dom g2] = dom fg2 by A14,Th22;
then
A17: dom f2 = cod f1 by A12,A15,XTUPLE_0:1;
then
A18: dom(L2.f2) = cod (L2.f1) by CAT_1:64;
id dom (L1.f1) = L1.(id dom f1) by CAT_1:63
.= M1.(id cod g1) by A1
.= id cod (M1.g1) by CAT_1:63;
then
A19: dom (L1.f1) = cod (M1.g1) by CAT_1:59;
then
A20: cod ((L1.f1)(*)(M1.g1)) = cod (L1.f1) by CAT_1:17;
A21: dom g2 = cod g1 by A12,A16,A15,XTUPLE_0:1;
then
A22: dom(M1.g2) = cod (M1.g1) by CAT_1:64;
then
A23: cod ((M1.g2)(*)(M1.g1)) = cod(M1.g2) by CAT_1:17;
id dom (M2.g2) = M2.(id dom g2) by CAT_1:63
.= L1.(id cod f1) by A1,A17,A21
.= id cod (L1.f1) by CAT_1:63;
then
A24: dom (M2.g2) = cod(L1.f1) by CAT_1:59;
id dom (L2.f2) = L2.(id dom f2) by CAT_1:63
.= M2.(id cod g2) by A1
.= id cod (M2.g2) by CAT_1:63;
then
A25: dom (L2.f2) = cod (M2.g2) by CAT_1:59;
set f = f2(*)f1, g = g2(*)g1;
id dom (L2.f1) = L2.(id dom f1) by CAT_1:63
.= M1.(id cod g2) by A1
.= id cod (M1.g2) by CAT_1:63;
then
A26: dom (L2.f1) = cod (M1.g2) by CAT_1:59;
thus T.(fg2(*)fg1) = S.(f,g) by A12,A13,A14,Th24
.= ((L.(cod g)).f)(*)((M.(dom f)).g) by A3
.= ((L.(cod g2)).f)(*)((M.(dom f)).g) by A21,CAT_1:17
.= ((L.(cod g2)).f)(*)((M.(dom f1)).g) by A17,CAT_1:17
.= ((L2.f2)(*)(L2.f1))(*)(M1.g) by A17,CAT_1:64
.= ((L2.f2)(*)(L2.f1))(*)((M1.g2)(*)(M1.g1)) by A21,CAT_1:64
.= (L2.f2)(*)((L2.f1)(*)((M1.g2)(*)(M1.g1))) by A18,A23,A26,CAT_1:18
.= (L2.f2)(*)(((L2.f1)(*)(M1.g2))(*)(M1.g1)) by A22,A26,CAT_1:18
.= (L2.f2)(*)(((M2.g2)(*)(L1.f1))(*)(M1.g1)) by A2,A17,A21
.= (L2.f2)(*)((M2.g2)(*)((L1.f1)(*)(M1.g1))) by A19,A24,CAT_1:18
.= ((L2.f2)(*)(M2.g2))(*)((L1.f1)(*)(M1.g1)) by A24,A25,A20,CAT_1:18
.= ((L2.f2)(*)(M2.g2))(*)(S.(f1,g1)) by A3
.= (S.(f2,g2))(*)(T.fg1) by A3,A13
.= (T.fg2)(*)(T.fg1) by A14;
end;
then reconsider T as Functor of [:B,C:],D by CAT_1:61;
take T;
thus thesis by A3;
end;
theorem
for L being Function of the carrier of C,Funct(B,D),
M being Function of the carrier of B,Funct(C,D)
st ex S being Functor of [:B,C:],D st
for c being Object of C,b being Object of B
holds S-?c = L.c & S?-b = M.b
for f being Morphism of B for g being Morphism of C
holds ((M.(cod f)).g)(*)((L.(dom g)).f) =
((L.(cod g)).f)(*)((M.(dom f)).g)
proof
let L be Function of the carrier of C,Funct(B,D), M be Function of the
carrier of B,Funct(C,D);
given S be Functor of [:B,C:],D such that
A1: for c being Object of C, b being Object of B holds S-?c = L.c & S?-b = M.b;
let f be Morphism of B;
let g be Morphism of C;
dom id cod f = cod f;
then
A2: dom [id cod f,g] = [cod f,dom g] by Th22;
cod id dom g = dom g;
then
A3: cod [f,id dom g] = [cod f, dom g] by Th22;
cod id dom f = dom f;
then
A4: cod [id dom f,g] = [dom f,cod g] by Th22;
dom id cod g = cod g;
then
A5: dom [f,id cod g] = [dom f,cod g] by Th22;
thus ((M.(cod f)).g)(*)((L.(dom g)).f)
= ((S?-(cod f)).g)(*)((L.(dom g)).f) by A1
.= ((S?-(cod f)).g)(*)((S-?(dom g)).f) by A1
.= (S.(id cod f,g))(*)((S-?(dom g)).f) by FUNCT_5:69
.= (S.(id cod f,g))(*)(S.(f,id dom g)) by FUNCT_5:70
.= S.([id cod f,g](*)[f,id dom g]) by A2,A3,CAT_1:64
.= S.[(id cod f)(*)f,g(*)(id dom g)] by A2,A3,Th24
.= S.[f,g(*)(id dom g)] by CAT_1:21
.= S.[f,g] by CAT_1:22
.= S.[f(*)(id dom f),g] by CAT_1:22
.= S.[f(*)(id dom f),(id cod g)(*)g ] by CAT_1:21
.= S.([f,id cod g](*)[id dom f,g]) by A5,A4,Th24
.= (S.(f,id cod g))(*)(S.[id dom f,g]) by A5,A4,CAT_1:64
.= ((S-?(cod g)).f)(*)(S.(id dom f,g)) by FUNCT_5:70
.= ((S-?(cod g)).f)(*)((S?-(dom f)).g) by FUNCT_5:69
.= ((L.(cod g)).f)(*)((S?-(dom f)).g) by A1
.= ((L.(cod g)).f)(*)((M.(dom f)).g) by A1;
end;
definition
let C,D;
func pr1(C,D) -> Functor of [:C,D:],C equals
pr1(the carrier' of C,the carrier' of D);
coherence
proof
reconsider T = pr1(the carrier' of C,the carrier' of D) as Function of the
carrier' of [:C,D:],the carrier' of C;
now
thus for cd being Object of [:C,D:] ex c being Object of C st T.(id cd) =
id c
proof
let cd be Object of [:C,D:];
consider c being Object of C,d being Object of D such that
A1: cd = [c,d] by DOMAIN_1:1;
A2: T.(id c,id d) = id c by FUNCT_3:def 4;
id cd = [id c,id d] by A1,Th25;
hence thesis by A2;
end;
thus for fg being Morphism of [:C,D:] holds T.(id dom fg) = id dom (T.fg)
& T.(id cod fg) = id cod (T.fg)
proof
let fg be Morphism of [:C,D:];
consider f being (Morphism of C), g being Morphism of D such that
A3: fg = [f,g] by DOMAIN_1:1;
T.(f,g) = T.fg by A3;
then
A4: T.fg = f by FUNCT_3:def 4;
dom [f,g] = [dom f,dom g] by Th22;
hence T.(id dom fg) = T.(id dom f,id dom g) by A3,Th25
.= id dom(T.fg) by A4,FUNCT_3:def 4;
cod [f,g] = [cod f,cod g] by Th22;
hence T.(id cod fg) = T.(id cod f,id cod g) by A3,Th25
.= id cod(T.fg) by A4,FUNCT_3:def 4;
end;
let fg,fg9 be Morphism of [:C,D:] such that
A5: dom fg9 = cod fg;
consider f being (Morphism of C), g being Morphism of D such that
A6: fg = [f,g] by DOMAIN_1:1;
T.(f,g) = T.fg by A6;
then
A7: T.fg = f by FUNCT_3:def 4;
consider f9 being (Morphism of C), g9 being Morphism of D such that
A8: fg9 = [f9,g9] by DOMAIN_1:1;
T.(f9,g9) = T.fg9 by A8;
then
A9: T.fg9 = f9 by FUNCT_3:def 4;
dom [f9,g9] = [dom f9,dom g9] & cod [f,g] = [cod f,cod g] by Th22;
then dom f9 = cod f & dom g9 = cod g by A5,A6,A8,XTUPLE_0:1;
hence T.(fg9(*)fg) = T.(f9(*)f,g9(*)g) by A6,A8,Th23
.= (T.fg9)(*)(T.fg) by A9,A7,FUNCT_3:def 4;
end;
hence thesis by CAT_1:61;
end;
func pr2(C,D) -> Functor of [:C,D:],D equals
pr2(the carrier' of C,the carrier' of D);
coherence
proof
reconsider T = pr2(the carrier' of C,the carrier' of D)
as Function of the carrier' of [:C,D:],the carrier' of D;
now
thus for cd being Object of [:C,D:] ex d being Object of D st T.(id cd) =
id d
proof
let cd be Object of [:C,D:];
consider c being Object of C,d being Object of D such that
A10: cd = [c,d] by DOMAIN_1:1;
A11: T.(id c,id d) = id d by FUNCT_3:def 5;
id cd = [id c,id d] by A10,Th25;
hence thesis by A11;
end;
thus for fg being Morphism of [:C,D:] holds T.(id dom fg) = id dom (T.fg)
& T.(id cod fg) = id cod (T.fg)
proof
let fg be Morphism of [:C,D:];
consider f being (Morphism of C), g being Morphism of D such that
A12: fg = [f,g] by DOMAIN_1:1;
T.(f,g) = T.fg by A12;
then
A13: T.fg = g by FUNCT_3:def 5;
dom [f,g] = [dom f,dom g] by Th22;
hence T.(id dom fg) = T.(id dom f,id dom g) by A12,Th25
.= id dom(T.fg) by A13,FUNCT_3:def 5;
cod [f,g] = [cod f,cod g] by Th22;
hence T.(id cod fg) = T.(id cod f,id cod g) by A12,Th25
.= id cod(T.fg) by A13,FUNCT_3:def 5;
end;
let fg,fg9 be Morphism of [:C,D:] such that
A14: dom fg9 = cod fg;
consider f being (Morphism of C), g being Morphism of D such that
A15: fg = [f,g] by DOMAIN_1:1;
T.(f,g) = T.fg by A15;
then
A16: T.fg = g by FUNCT_3:def 5;
consider f9 being (Morphism of C), g9 being Morphism of D such that
A17: fg9 = [f9,g9] by DOMAIN_1:1;
T.(f9,g9) = T.fg9 by A17;
then
A18: T.fg9 = g9 by FUNCT_3:def 5;
dom [f9,g9] = [dom f9,dom g9] & cod [f,g] = [cod f,cod g] by Th22;
then dom f9 = cod f & dom g9 = cod g by A14,A15,A17,XTUPLE_0:1;
hence T.(fg9(*)fg) = T.(f9(*)f,g9(*)g) by A15,A17,Th23
.= (T.fg9)(*)(T.fg) by A18,A16,FUNCT_3:def 5;
end;
hence thesis by CAT_1:61;
end;
end;
::$CT 2
theorem
for c being Object of C, d being Object of D holds (Obj pr1(C,D)).(c,d ) = c
proof
let c be Object of C, d be Object of D;
id [c,d] = [id c,id d] & (pr1(C,D)).(id c,id d) = id c by Th25,FUNCT_3:def 4;
hence thesis by CAT_1:67;
end;
theorem
for c being Object of C, d being Object of D holds (Obj pr2(C,D)).(c,d ) = d
proof
let c be Object of C, d be Object of D;
id [c,d] = [id c,id d] & (pr2(C,D)).(id c,id d) = id d by Th25,FUNCT_3:def 5;
hence thesis by CAT_1:67;
end;
definition
let C,D,D9;
let T be Functor of C,D, T9 be Functor of C,D9;
redefine func <:T,T9:> -> Functor of C,[:D,D9:]; :: redefines <: (FUNCT_3, definition)
coherence
proof
reconsider S = <:T,T9:> as
Function of the carrier' of C,the carrier' of [:D,D9:];
now
thus for c being Object of C ex dd9 being Object of [:D,D9:] st S.(id c) =
id dd9
proof
let c be Object of C;
set d = (Obj T).c, d9 = (Obj T9).c;
take dd9 = [d,d9];
thus S.(id c) = [T.(id c),T9.(id c)] by FUNCT_3:59
.= [id d,T9.(id c)] by CAT_1:68
.= [id d,id d9] by CAT_1:68
.= id dd9 by Th25;
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;
T.(id dom f) = id(dom(T.f)) & T9.(id dom f) = id(dom(T9.f)) by CAT_1:63;
hence S.(id dom f) = [id(dom(T.f)),id(dom(T9.f))] by FUNCT_3:59
.= id [dom(T.f),dom(T9.f)] by Th25
.= id dom[T.f,T9.f] by Th22
.= id dom (S.f) by FUNCT_3:59;
T.(id cod f) = id(cod(T.f)) & T9.(id cod f) = id(cod(T9.f)) by CAT_1:63;
hence S.(id cod f) = [id(cod(T.f)),id(cod(T9.f))] by FUNCT_3:59
.= id [cod(T.f),cod(T9.f)] by Th25
.= id cod [T.f,T9.f] by Th22
.= id cod (S.f) by FUNCT_3:59;
end;
let f,g be Morphism of C;
assume
A1: dom g = cod f;
then
A2: dom(T.g) = cod(T.f) & dom(T9.g) = cod(T9.f) by CAT_1:64;
T.(g(*)f) = (T.g)(*)(T.f) & T9.(g(*)f) = (T9.g)(*)(T9.f) by A1,CAT_1:64;
hence S.(g(*)f) = [(T.g)(*)(T.f),(T9.g)(*)(T9.f)] by FUNCT_3:59
.= [T.g,T9.g](*)[T.f,T9.f] by A2,Th23
.= (S.g)(*)[T.f,T9.f] by FUNCT_3:59
.= (S.g)(*)(S.f) by FUNCT_3:59;
end;
hence thesis by CAT_1:61;
end;
end;
::$CT
theorem
for T being Functor of C,D, T9 being Functor of C,D9, c being Object
of C holds (Obj <:T,T9:>).c = [(Obj T).c,(Obj T9).c]
proof
let T be Functor of C,D, T9 be Functor of C,D9, c be Object of C;
A1: T.(id c) = id((Obj T).c) & T9.(id c) = id((Obj T9).c) by CAT_1:68;
<:T,T9:>.(id c) = [T.(id c),T9.(id c)] & [id((Obj T).c),id((Obj T9).c)]
= id [(Obj T).c,(Obj T9).c] by Th25,FUNCT_3:59;
hence thesis by A1,CAT_1:67;
end;
theorem Th39:
for T being Functor of C,D, T9 being Functor of C9,D9 holds [:T,
T9:] = <:T*pr1(C,C9),T9*pr2(C,C9):>
proof
let T be Functor of C,D, T9 be Functor of C9,D9;
dom T = the carrier' of C & dom T9 = the carrier' of C9 by FUNCT_2:def 1;
hence thesis by FUNCT_3:66;
end;
definition
let C,C9,D,D9;
let T be Functor of C,D, T9 be Functor of C9,D9;
redefine func [:T,T9:] -> Functor of [:C,C9:],[:D,D9:]; :: redefines [: (FUNCT_3, definition)
coherence
proof
[:T,T9:] = <:T*pr1(C,C9),T9*pr2(C,C9):> by Th39;
hence thesis;
end;
end;
::$CT
theorem
for T being Functor of C,D, T9 being Functor of C9,D9, c being Object
of C, c9 being Object of C9 holds (Obj [:T,T9:]).(c,c9) = [(Obj T).c,(Obj T9).
c9]
proof
let T be Functor of C,D, T9 be Functor of C9,D9;
let c be Object of C, c9 be Object of C9;
A1: T.(id c) = id((Obj T).c) & T9.(id c9) = id((Obj T9).c9) by CAT_1:68;
A2: [id((Obj T).c),id((Obj T9).c9)] = id [(Obj T).c,(Obj T9).c9] by Th25;
[:T,T9:].(id c,id c9) = [T.(id c),T9.(id c9)] & [id c,id c9] = id [c,c9]
by Th25,FUNCT_3:75;
hence thesis by A1,A2,CAT_1:67;
end;