Copyright (c) 1990 Association of Mizar Users
environ
vocabulary FRAENKEL, FUNCT_1, FUNCT_5, FUNCT_2, RELAT_1, BOOLE, CAT_1,
FUNCOP_1, FUNCT_3, TARSKI, PARTFUN1, FUNCT_4, MCART_1, CAT_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
FUNCT_2, PARTFUN1, FUNCT_3, FUNCT_4, FUNCT_5, FRAENKEL, CAT_1;
constructors DOMAIN_1, FUNCT_3, FUNCT_4, FUNCT_5, FRAENKEL, CAT_1, MEMBERED,
PARTFUN1, XBOOLE_0;
clusters FUNCT_1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, 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;
schemes FUNCT_2, XBOOLE_0;
begin
reserve X for set;
reserve C,D,E for non empty set;
reserve c for Element of C, d for Element of D;
:: Auxiliary theorems
definition let D,X,E; let F be FUNCTION_DOMAIN of X,E;
let f be Function of D,F; let d be Element of D;
redefine func f.d -> Element of F;
coherence proof thus f.d is Element of F; end;
end;
reserve f for Function of [:C,D:],E;
theorem Th1:
curry f is Function of C,Funcs(D,E)
proof
A1: dom f = [:C,D:] by FUNCT_2:def 1;
then A2: dom curry f = C by FUNCT_5:31;
rng curry f c= Funcs(D,E)
proof let x be set such that
A3: x in rng curry f;
rng curry f c= Funcs(D,rng f) by A1,FUNCT_5:42;
then consider g being Function such that
A4: x = g and
A5: dom g = D and
A6: rng g c= rng f by A3,FUNCT_2:def 2;
rng f c= E by RELSET_1:12;
then rng g c= E by A6,XBOOLE_1:1;
then g is Function of D,E & E<>{} by A5,FUNCT_2:def 1,RELSET_1:11;
hence thesis by A4,FUNCT_2:11;
end;
hence thesis by A2,FUNCT_2:def 1,RELSET_1:11;
end;
theorem Th2:
curry' f is Function of D,Funcs(C,E)
proof
A1: dom f = [:C,D:] by FUNCT_2:def 1;
then A2: dom curry' f = D by FUNCT_5:31;
rng curry' f c= Funcs(C,E)
proof let x be set such that
A3: x in rng curry' f;
rng curry' f c= Funcs(C,rng f) by A1,FUNCT_5:42;
then consider g being Function such that
A4: x = g and
A5: dom g = C and
A6: rng g c= rng f by A3,FUNCT_2:def 2;
rng f c= E by RELSET_1:12;
then rng g c= E by A6,XBOOLE_1:1;
then g is Function of C,E & E<>{} by A5,FUNCT_2:def 1,RELSET_1:11;
hence thesis by A4,FUNCT_2:11;
end;
hence thesis by A2,FUNCT_2:def 1,RELSET_1:11;
end;
definition let C,D,E,f;
redefine func curry f -> Function of C,Funcs(D,E);
coherence by Th1;
func curry' f -> Function of D,Funcs(C,E);
coherence by Th2;
end;
theorem Th3:
f.[c,d] = ((curry f).c).d
proof [c,d] in [:C,D:]; then [c,d] in dom f by FUNCT_2:def 1;
hence thesis by FUNCT_5:27;
end;
theorem Th4:
f.[c,d] = ((curry' f).d).c
proof [c,d] in [:C,D:]; then [c,d] in dom f by FUNCT_2:def 1;
hence thesis by FUNCT_5:29;
end;
reserve B,C,D,C',D' for Category;
:: Auxiliary theorems on Functors
definition let B,C; let c be Object of C;
func B --> c -> Functor of B,C equals
:Def1: (the Morphisms of B) --> (id c);
coherence
proof
reconsider T = (the Morphisms of B) --> id c
as Function of the Morphisms of B,the Morphisms of C by FUNCOP_1:58;
now
thus for b being Object of B ex d being Object of C st T.(id b) = id d
proof let b be Object of B; take c;
thus T.(id b) = id c by FUNCOP_1:13;
end;
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 dom f) = id c & T.(id cod f) = id c by FUNCOP_1:13;
then T.(id dom f) = id dom id c & T.(id cod f) = id cod id c &
f in the Morphisms of B by CAT_1:44;
hence thesis by FUNCOP_1:13;
end;
let f,g be Morphism of B such that dom g = cod f;
Hom(c,c) <> {} & g*f in the Morphisms of B &
g in the Morphisms of B & f in the Morphisms of B by CAT_1:56;
then T.(g*f) = id c & T.g = id c & T.f = id c &
(id c)*(id c) = (id c)*((id c) qua Morphism of C) by CAT_1:def 13,FUNCOP_1:
13;
hence T.(g*f) = (T.g)*(T.f) by CAT_1:59;
end;
hence thesis by CAT_1:96;
end;
end;
canceled;
theorem Th6:
for c being Object of C, f being Morphism of B holds (B --> c).f = id c
proof let c be Object of C, f be Morphism of B;
f in the Morphisms of B & B --> c = (the Morphisms of B) --> id c
by Def1;
hence thesis by FUNCOP_1:13;
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 Th6;
hence thesis by CAT_1:103;
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[set] means $1 is Functor of C,D;
consider F being set such that
A1: for x being set holds x in F iff
x in Funcs(the Morphisms of C,the Morphisms of D) & P[x] from Separation;
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 Morphisms of C,the Morphisms of D) by FUNCT_2:11;
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) &
(for x being set holds x in F2 iff x is Functor of C,D);
now let x be set;
(x in F1 iff x is Functor of C,D) & (x in F2 iff x is Functor of C,D) by
A3
;
hence x in F1 iff x in F2;
end;
hence thesis by TARSKI:2;
end;
end;
definition let C,D;
cluster Funct(C,D) -> non empty;
coherence
proof
consider x being 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;
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;
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;
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 Objects of it c= the Objects of C &
(for a,b being Object of it, a',b' being Object of C
st a = a' & b = b' holds Hom(a,b) c= Hom(a',b')) &
the Comp of it <= the Comp of C &
(for a being Object of it, a' being Object of C st a = a'
holds id a = id a');
existence proof take C; thus thesis; end;
end;
definition let C;
cluster strict Subcategory of C;
existence
proof consider c being Object of C;
set E = 1Cat(c,id c);
now
A1: E = CatStr(#{c},{id c},{id c}-->c,{id c}-->c,
(id c,id c).-->id c,{c}-->id c#) by CAT_1:def 9;
thus the Objects of E c= the Objects of C
proof let a be set;
assume a in the Objects of E;
then a = c by CAT_1:34;
hence thesis;
end;
thus for a,b being Object of E, a',b' being Object of C
st a = a' & b = b' holds Hom(a,b) c= Hom(a',b')
proof let a,b be Object of E, a',b' be Object of C such that
A2: a = a' & b = b';
let x be set;
assume x in Hom(a,b);
then x = id c & a' = c & b' = c by A2,CAT_1:34,35;
hence x in Hom(a',b') by CAT_1:55;
end;
thus the Comp of E <= the Comp of C
proof
A3: dom id c = c & cod id c = c by CAT_1:44;
then A4: [id c,id c] in dom the Comp of C by CAT_1:40;
A5: Hom(c,c) <> {} by CAT_1:56;
the Comp of E
= {[id c,id c]}-->id c by A1,CAT_1:def 1
.= {[id c,id c]}-->(id c)*(id c) by CAT_1:59
.= {[id c,id c]}-->(id c)*((id c) qua Morphism of C) by A5,CAT_1:def 13
.= {[id c,id c]}-->(the Comp of C).[id c,id c] by A3,CAT_1:41;
hence thesis by A4,FUNCT_4:8;
end;
let a be Object of E, a' be Object of C;
assume a = a';
then a' = c by CAT_1:34;
hence id a = id a' by CAT_1:35;
end;
then E is Subcategory of C by Def4;
hence thesis;
end;
end;
reserve E for Subcategory of C;
canceled 4;
theorem Th12:
for e being Object of E holds e is Object of C
proof let e be Object of E;
e in the Objects of E & the Objects of E c= the Objects of C
by Def4;
hence thesis;
end;
theorem Th13:
the Morphisms of E c= the Morphisms of C
proof let x be set;
assume x in the Morphisms of E;
then reconsider f = x as Morphism of E;
set a = dom f, b = cod f;
reconsider a' = a, b' = b as Object of C by Th12;
f in Hom(a,b) & Hom(a,b) c= Hom(a',b') by Def4,CAT_1:18;
then f is Morphism of a',b' by CAT_1:21;
hence thesis;
end;
theorem Th14:
for f being Morphism of E holds f is Morphism of C
proof let f be Morphism of E;
f in the Morphisms of E & the Morphisms of E c= the Morphisms of C
by Th13;
hence thesis;
end;
theorem Th15:
for f being (Morphism of E), f' being Morphism of C st f = f'
holds dom f = dom f' & cod f = cod f'
proof let f be (Morphism of E), f' be Morphism of C such that
A1: f = f';
set a = dom f, b = cod f;
reconsider a' = a, b' = b as Object of C by Th12;
f in Hom(a,b) & Hom(a,b) c= Hom(a',b') by Def4,CAT_1:18;
hence thesis by A1,CAT_1:18;
end;
theorem
for a,b being Object of E, a',b' being Object of C,f being Morphism of a,b
st a = a' & b = b' & Hom(a,b)<>{} holds f is Morphism of a',b'
proof let a,b be Object of E, a',b' be Object of C, f be Morphism of a,b;
assume a = a' & b = b' & Hom(a,b)<>{};
then f in Hom(a,b) & Hom(a,b) c= Hom(a',b') by Def4,CAT_1:def 7;
hence thesis by CAT_1:21;
end;
theorem Th17:
for f,g being (Morphism of E), f',g' being Morphism of C
st f = f' & g = g' & dom g = cod f holds g*f = g'*f'
proof let f,g be (Morphism of E), f',g' be Morphism of C such that
A1: f = f' & g = g' and
A2: dom g = cod f;
dom g = dom g' & cod f = cod f' by A1,Th15;
then g*f = (the Comp of E).[g,f] & [g,f] in dom(the Comp of E) &
g'*f' = (the Comp of C).[g',f'] & the Comp of E <= the Comp of C
by A2,Def4,CAT_1:40,41;
hence thesis by A1,GRFUNC_1:8;
end;
theorem
C is Subcategory of C
proof thus the Objects of C c= the Objects of C;
thus thesis;
end;
theorem Th19:
id E is Functor of E,C
proof id E = id the Morphisms of E by CAT_1:def 21;
then rng id E = the Morphisms of E by RELAT_1:71;
then rng id E c= the Morphisms of C & the Morphisms of E <> {}
by Th13;
then reconsider T = id E as Function of the Morphisms of E,the Morphisms of C
by FUNCT_2:8;
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 Th12;
T.(id e) = id e by CAT_1:115 .= 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;
now
thus T.(id dom f) = id dom f by CAT_1:115
.= id dom ((id E).f) by CAT_1:115;
thus T.(id cod f) = id cod f by CAT_1:115
.= id cod ((id E).f) by CAT_1:115;
thus dom (T.f) = dom((id E).f) & cod (T.f) = cod((id E).f) by Th15;
end;
hence thesis by Def4;
end;
let f,g be Morphism of E; assume
A1: dom g = cod f;
then T.f = f & T.g = g & T.(g*f) = ((id E).g)*((id E).f) by CAT_1:99,115
;
hence T.(g*f) = (T.g)*(T.f) by A1,Th17;
end;
hence thesis by CAT_1:96;
end;
definition let C,E;
func incl(E) -> Functor of E,C equals
:Def5: id E;
coherence by Th19;
end;
canceled;
theorem Th21:
for f being Morphism of E holds (incl E).f = f
proof let f be Morphism of E; incl E = id E by Def5;
hence thesis by CAT_1:115;
end;
theorem Th22:
for a being Object of E holds (Obj incl E).a = a
proof let a be Object of E;
reconsider a' = a as Object of C by Th12;
id a' = id a by Def4
.= (incl E).(id a) by Th21
.= id((Obj incl E).a) by CAT_1:104;
hence thesis by CAT_1:45;
end;
theorem Th23:
for a being Object of E holds (incl E).a = a
proof let a be Object of E; a = (Obj incl E).a by Th22;
hence thesis by CAT_1:def 20;
end;
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 = id E by Def5;
then (incl E).f1 = f1 & (incl E).f2 = f2 by CAT_1:115;
hence thesis;
end;
theorem Th25:
incl E is full iff
for a,b being Object of E, a',b' being Object of C
st a = a' & b = b' holds Hom(a,b) = Hom(a',b')
proof set T = incl E;
thus T is full implies
for a,b being Object of E, a',b' being Object of C
st a = a' & b = b' holds Hom(a,b) = Hom(a',b')
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, a',b' be Object of C such that
A2: a = a' & b = b';
now let x be set;
Hom(a,b) c= Hom(a',b') by A2,Def4;
hence x in Hom(a,b) implies x in Hom(a',b');
A3: T.a = a' & T.b = b' by A2,Th23;
assume
A4: x in Hom(a',b');
then reconsider g = x as Morphism of T.a,T.b by A3,CAT_1:def 7;
consider f being Morphism of a,b such that
A5: g = T.f by A1,A3,A4;
g = f & Hom(a,b) <> {} by A1,A3,A4,A5,Th21;
hence x in Hom(a,b) by CAT_1:def 7;
end;
hence thesis by TARSKI:2;
end;
assume
A6: for a,b being Object of E, a',b' being Object of C
st a = a' & b = b' holds Hom(a,b) = Hom(a',b');
let a,b be Object of E such that
A7: Hom(T.a,T.b) <> {};
let g be Morphism of T.a,T.b;
A8: a = T.a & b = T.b by Th23;
then A9: Hom(a,b) = Hom(T.a,T.b) by A6;
thus Hom(a,b) <> {} by A6,A7,A8;
g in Hom(T.a,T.b) by A7,CAT_1:def 7;
then reconsider f = g as Morphism of a,b by A9,CAT_1:def 7;
take f; thus thesis by Th21;
end;
definition let C be CatStr, D;
pred C is_full_subcategory_of D means
:Def6: C is Subcategory of D &
for a,b being Object of C, a',b' being Object of D
st a = a' & b = b' holds Hom(a,b) = Hom(a',b');
end;
canceled;
theorem
E is_full_subcategory_of C iff incl(E) is full
proof
thus E is_full_subcategory_of C implies incl(E) is full
proof assume E is_full_subcategory_of C;
then for a,b being Object of E, a',b' being Object of C
st a = a' & b = b' holds Hom(a,b) = Hom(a',b') by Def6;
hence thesis by Th25;
end;
assume incl(E) is full;
hence E is Subcategory of C &
for a,b being Object of E, a',b' being Object of C
st a = a' & b = b' holds Hom(a,b) = Hom(a',b') by Th25;
end;
theorem Th28:
for O being non empty Subset of the Objects 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 Morphisms of C
proof let O be non empty Subset of the Objects 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;
now
now consider a being Element of O;
reconsider a as Object of C;
id a in Hom(a,a) & Hom(a,a) in H by CAT_1:55;
then id a in M by TARSKI:def 4;
hence ex f being set st f in M;
end;
hence M is non empty set;
thus M c= the Morphisms of C
proof let x be set;
assume x in M;
then consider X being set such that
A1: x in X and
A2: X in H by TARSKI:def 4;
consider a,b being Object of C such that
A3: X = Hom(a,b) and a in O & b in O by A2;
thus thesis by A1,A3;
end;
end;
hence thesis;
end;
theorem Th29:
for O being non empty Subset of the Objects 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 Dom of C)|M is Function of M,O &
(the Cod of C)|M is Function of M,O &
(the Comp of C)|[:M,M:] is PartFunc of [:M,M:],M &
(the Id of C)|O is Function of O,M
proof let O be non empty Subset of the Objects of C;
set H = {Hom(a,b) where a is Object of C, b is Object of C: a in O & b in O};
let M be non empty set such that
A1: M = union H;
set d = (the Dom of C)|M, c = (the Cod of C)|M,
p = (the Comp of C)|[:M,M:], i = (the Id of C)|O;
A2: now let f be Morphism of C;
assume f in M;
then consider X being set such that
A3: f in X and
A4: 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 A4;
hence dom f in O & cod f in O by A3,CAT_1:18;
end;
A5: dom the Dom of C = the Morphisms of C &
dom the Cod of C = the Morphisms of C by FUNCT_2:def 1;
A6: dom d = (dom the Dom of C) /\ M & dom c = (dom the Cod of C) /\ M
by RELAT_1:90;
A7: M is non empty Subset of the Morphisms of C by A1,Th28;
now
thus dom d = M & dom c = M by A5,A7,RELAT_1:91;
thus rng d c= O
proof let y be set;
assume y in rng d;
then consider x being set such that
A8: x in dom d and
A9: y = d.x by FUNCT_1:def 5;
reconsider f = x as Morphism of C by A5,A6,A8,XBOOLE_0:def 3;
now thus d.f = (the Dom of C).f by A8,FUNCT_1:70 .= dom f by CAT_1:def
2
;
thus f in M by A6,A8,XBOOLE_0:def 3;
end;
hence thesis by A2,A9;
end;
thus rng c c= O
proof let y be set;
assume y in rng c;
then consider x being set such that
A10: x in dom c and
A11: y = c.x by FUNCT_1:def 5;
reconsider f = x as Morphism of C by A5,A6,A10,XBOOLE_0:def 3;
now thus c.f = (the Cod of C).f by A10,FUNCT_1:70 .= cod f by CAT_1:
def 3;
thus f in M by A6,A10,XBOOLE_0:def 3;
end;
hence thesis by A2,A11;
end;
end;
hence d is Function of M,O & c is Function of M,O by FUNCT_2:def 1,RELSET_1:
11;
thus p is PartFunc of [:M,M:],M
proof
A12: dom the Comp of C c= [:the Morphisms of C,the Morphisms of C:]
by RELSET_1:12;
A13: dom p = (dom the Comp of C) /\ [:M,M:] by RELAT_1:90;
then A14: dom p c= [:M,M:] by XBOOLE_1:17;
rng p c= M
proof let y be set;
assume y in rng p;
then consider x being set such that
A15: x in dom p and
A16: y = p.x by FUNCT_1:def 5;
A17: x in dom the Comp of C by A13,A15,XBOOLE_0:def 3;
then consider g,f being Morphism of C such that
A18: x = [g,f] by A12,DOMAIN_1:9;
now
thus p.x = (the Comp of C).[g,f] by A15,A18,FUNCT_1:70
.= g*f by A17,A18,CAT_1:def 4;
now [g,f] in [:M,M:] by A13,A15,A18,XBOOLE_0:def 3;
then f in M & g in M by ZFMISC_1:106;
hence dom f in O & cod g in O by A2;
dom g = cod f by A17,A18,CAT_1:40;
hence dom(g*f) = dom f & cod(g*f) = cod g by CAT_1:42;
end;
hence Hom(dom(g*f),cod(g*f)) in H & g*f in Hom(dom(g*f),cod(g*f))
by CAT_1:18;
end;
hence thesis by A1,A16,TARSKI:def 4;
end;
hence thesis by A14,RELSET_1:11;
end;
now
A19: dom the Id of C = the Objects of C by FUNCT_2:def 1;
A20: dom i = (dom the Id of C) /\ O by RELAT_1:90;
thus dom i = O by A19,RELAT_1:91;
thus rng i c= M
proof let y be set;
assume y in rng i;
then consider x being set such that
A21: x in dom i and
A22: y = i.x by FUNCT_1:def 5;
reconsider a = x as Object of C by A19,A20,A21,XBOOLE_0:def 3;
now
thus i.a = (the Id of C).a by A21,FUNCT_1:70 .= id a by CAT_1:def 5;
thus a in O by A20,A21,XBOOLE_0:def 3;
end;
then i.a in Hom(a,a) & Hom(a,a) in H by CAT_1:55;
hence thesis by A1,A22,TARSKI:def 4;
end;
end;
hence i is Function of O,M by FUNCT_2:def 1,RELSET_1:11;
end;
theorem
for O being non empty Subset of the Objects 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 Dom of C)|M & c = (the Cod of C)|M
& p = (the Comp of C)|[:M,M:] & i = (the Id of C)|O
holds CatStr(#O,M,d,c,p,i#) is_full_subcategory_of C
proof
let O be non empty Subset of the Objects 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 Dom of C)|M and
A3: c = (the Cod of C)|M and
A4: p = (the Comp of C)|[:M,M:] and
A5: i = (the Id of C)|O;
set B = CatStr(#O,M,d,c,p,i#);
A6: now let f be Morphism of B;
consider X being set such that
A7: f in X and
A8: 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 A8;
hence f is Morphism of C by A7;
end;
A9: for f,g being Element of M holds [g,f] in dom(p) iff d.g=c.f
proof let f,g be Element of M;
A10: g is Morphism of C & f is Morphism of C by A6;
A11: d.g = (the Dom of C).g & c.f = (the Cod of C).f
by A2,A3,FUNCT_1:72;
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:90;
then [g,f] in (dom the Comp of C) by XBOOLE_0:def 3;
hence thesis by A10,A11,CAT_1:def 8;
end;
assume d.g=c.f;
then [g,f] in dom the Comp of C & [g,f] in [:M,M:]
by A10,A11,CAT_1:def 8;
then [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def 3;
hence [g,f] in dom p by A4,RELAT_1:90;
end;
A12: for f,g being Element of M st d.g=c.f
holds p.[g,f] = (the Comp of C).[g,f]
proof let f,g be Element of M;
assume d.g=c.f;
then [g,f] in dom(p) by A9;
hence thesis by A4,FUNCT_1:70;
end;
A13: for f,g being Element of M st d.g=c.f holds p.[g,f] is Element of M
proof let f,g be Element of M;
assume
A14: d.g=c.f;
then [g,f] in dom p by A9;
then p.[g,f] is Element of M by PARTFUN1:27;
then reconsider h = p.[g,f] as Morphism of C by A6;
set a = dom h, b = cod h;
f is Morphism of C & g is Morphism of C &
h = (the Comp of C).[g,f] &
d.f = (the Dom of C).f & c.g = (the Cod of C).g &
d.g = (the Dom of C).g & c.f = (the Cod of C).f by A2,A3,A6,A12,A14,
FUNCT_1:72;
then (the Dom of C).h = d.f & (the Cod of C).h = c.g by A14,CAT_1:def 8;
then a = d.f & b = c.g by CAT_1:def 2,def 3;
then h in Hom(a,b) & Hom(a,b) in H by CAT_1:18;
hence thesis by A1,TARSKI:def 4;
end;
A15: for a,b being Object of B, a',b' being Object of C
st a = a' & b = b' holds Hom(a,b) = Hom(a',b')
proof let a,b be Object of B, a',b' be Object of C such that
A16: a = a' & b = b';
now let x be set;
thus x in Hom(a,b) implies x in Hom(a',b')
proof assume
A17: x in Hom(a,b);
then reconsider f = x as Morphism of B;
reconsider f' = f as Morphism of C by A6;
(the Dom of B).f = (the Dom of C).f' &
(the Cod of B).f = (the Cod of C).f' by A2,A3,FUNCT_1:72;
then (the Dom of B).f = dom f' & (the Cod of B).f = cod f'
by CAT_1:def 2,def 3;
then dom f = dom f' & cod f = cod f' by CAT_1:def 2,def 3;
then a = dom f' & b = cod f' by A17,CAT_1:18;
hence thesis by A16,CAT_1:18;
end;
assume
A18: x in Hom(a',b');
then reconsider f' = x as Morphism of C;
Hom(a',b') in H by A16;
then reconsider f = f' as Morphism of B by A1,A18,TARSKI:def 4;
(the Dom of B).f = (the Dom of C).f' &
(the Cod of B).f = (the Cod of C).f' by A2,A3,FUNCT_1:72;
then (the Dom of B).f = dom f' & (the Cod of B).f = cod f'
by CAT_1:def 2,def 3;
then dom f = dom f' & cod f = cod f' by CAT_1:def 2,def 3;
then dom f = a' & cod f = b' by A18,CAT_1:18;
hence x in Hom(a,b) by A16,CAT_1:18;
end;
hence thesis by TARSKI:2;
end;
thus B is Subcategory of C
proof
now
thus for f,g being Element of M holds [g,f] in dom(p) iff d.g=c.f by A9;
thus
A19: 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;
assume
A20: d.g=c.f;
A21: g is Morphism of C & f is Morphism of C by A6;
A22: p.[g,f] is Element of M by A13,A20;
A23: d.g = (the Dom of C).g & c.f = (the Cod of C).f by A2,A3,FUNCT_1:72;
thus d.(p.[g,f]) = (the Dom of C).(p.[g,f]) by A2,A22,FUNCT_1:72
.= (the Dom of C).((the Comp of C).[g,f]) by A12,A20
.= (the Dom of C).f by A20,A21,A23,CAT_1:def 8
.= d.f by A2,FUNCT_1:72;
thus c.(p.[g,f]) = (the Cod of C).(p.[g,f]) by A3,A22,FUNCT_1:72
.= (the Cod of C).((the Comp of C).[g,f]) by A12,A20
.= (the Cod of C).g by A20,A21,A23,CAT_1:def 8
.= c.g by A3,FUNCT_1:72;
end;
thus for f,g,h being Element of M
st d.h = c.g & d.g = c.f holds p.[h,p.[g,f]] = p.[p.[h,g],f]
proof let f,g,h be Element of M; assume
A24: d.h = c.g & d.g = c.f;
then A25: c.(p.[g,f]) = c.g by A19;
A26: h is Morphism of C & g is Morphism of C & f is Morphism of C &
d.h = (the Dom of C).h & c.g = (the Cod of C).g &
d.g = (the Dom of C).g & c.f = (the Cod of C).f by A2,A3,A6,FUNCT_1:72
;
A27: d.(p.[h,g]) = d.g & p.[h,g] is Element of M by A13,A19,A24;
p.[g,f] is Element of M by A13,A24;
hence p.[h,p.[g,f]]
= (the Comp of C).[h,p.[g,f]] by A12,A24,A25
.= (the Comp of C).[h,(the Comp of C).[g,f]] by A12,A24
.= (the Comp of C).[(the Comp of C).[h,g],f] by A24,A26,CAT_1:def 8
.= (the Comp of C).[p.[h,g],f] by A12,A24
.= p.[p.[h,g],f] by A12,A24,A27;
end;
let b be Element of O;
A28: i.b = (the Id of C).b by A5,FUNCT_1:72;
d.(i.b) = (the Dom of C).(i.b) & c.(i.b) = (the Cod of C).(i.b)
by A2,A3,FUNCT_1:72;
hence
A29: d.(i.b) = b & c.(i.b) = b by A28,CAT_1:def 8;
thus for f being Element of M st c.f=b holds p.[i.b,f] = f
proof let f be Element of M such that
A30: c.f=b;
A31: f is Morphism of C & c.f = (the Cod of C).f by A3,A6,FUNCT_1:72;
thus p.[i.b,f] = (the Comp of C).[i.b,f] by A12,A29,A30
.= f by A28,A30,A31,CAT_1:def 8;
end;
let g be Element of M;
assume
A32: d.g=b;
A33: g is Morphism of C & d.g = (the Dom of C).g by A2,A6,FUNCT_1:72;
thus p.[g,i.b] = (the Comp of C).[g,i.b] by A12,A29,A32
.= g by A28,A32,A33,CAT_1:def 8;
end;
then reconsider B as Category by CAT_1:def 8;
now
thus the Objects of B c= the Objects of C;
thus for a,b being Object of B, a',b' being Object of C
st a = a' & b = b' holds Hom(a,b) c= Hom(a',b') by A15;
thus the Comp of B <= the Comp of C by A4,RELAT_1:88;
let a be Object of B, a' be Object of C;
assume
A34: a = a';
hence id a = i.a' by CAT_1:def 5
.= (the Id of C).a' by A5,A34,FUNCT_1:72
.= id a' by CAT_1:def 5;
end;
hence thesis by Def4;
end;
thus thesis by A15;
end;
theorem
for O being non empty Subset of the Objects 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 CatStr(#O,M,d,c,p,i#) 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 Dom of C)|M & c = (the Cod of C)|M
& p = (the Comp of C)|[:M,M:] & i = (the Id of C)|O
proof
let O be non empty Subset of the Objects 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};
set B = CatStr(#O,M,d,c,p,i#);
assume that
A1: B is Subcategory of C and
A2: for a,b being Object of B, a',b' being Object of C
st a = a' & b = b' holds Hom(a,b) = Hom(a',b');
A3: for f being Morphism of B holds
d.f = (the Dom of C).f & c.f = (the Cod of C).f
proof let f be Morphism of B;
reconsider f' = f as Morphism of C by A1,Th14;
dom f = dom f' & cod f = cod f' &
dom f = (the Dom of B).f & dom f' = (the Dom of C).f' &
cod f = (the Cod of B).f & cod f' = (the Cod of C).f' by A1,Th15,CAT_1:def 2,
def 3;
hence thesis;
end;
now let x be set;
thus x in M implies x in union H
proof assume x in M;
then reconsider f = x as Morphism of B;
reconsider f' = f as Morphism of C by A1,Th14;
set a' = dom f', b' = cod f';
(the Dom of B).f = (the Dom of C).f' &
(the Cod of B).f = (the Cod of C).f' by A3;
then (the Dom of B).f = a' & (the Cod of B).f = b'
by CAT_1:def 2,def 3;
then f in Hom(a',b') & Hom(a',b') in H by CAT_1:18;
hence thesis by TARSKI:def 4;
end;
assume x in union H;
then consider X being set such that
A4: x in X and
A5: X in H by TARSKI:def 4;
consider a',b' being Object of C such that
A6: X = Hom(a',b') and
A7: a' in O & b' in O by A5;
reconsider a = a', b = b' as Object of B by A7;
Hom(a,b) = Hom(a',b') by A2;
hence x in M by A4,A6;
end;
hence
A8: M = union H by TARSKI:2;
then reconsider d' = (the Dom of C)|M, c' = (the Cod of C)|M as Function of M
,O
by Th29;
now let f be Element of M;
now thus d.f = (the Dom of C).f by A3;
thus f in M;
f is Morphism of C by A1,Th14;
then f in the Morphisms of C;
hence f in dom the Dom of C by FUNCT_2:def 1;
end;
hence d.f = d'.f by FUNCT_1:72;
end;
hence d = (the Dom of C)|M by FUNCT_2:113;
now let f be Element of M;
now thus c.f = (the Cod of C).f by A3;
thus f in M;
f is Morphism of C by A1,Th14;
then f in the Morphisms of C;
hence f in dom the Cod of C by FUNCT_2:def 1;
end;
hence c.f = c'.f by FUNCT_1:72;
end;
hence c = (the Cod of C)|M by FUNCT_2:113;
set p' = (the Comp of C)|[:M,M:];
now
A9: dom p c= [:M,M:] by RELSET_1:12;
A10: dom p' = (dom the Comp of C) /\ [:M,M:] by RELAT_1:90;
A11: dom p' c= dom p
proof let x be set;
assume
A12: x in dom p';
then x in [:M,M:] by A10,XBOOLE_0:def 3;
then consider g,f being Element of M such that
A13: x = [g,f] by DOMAIN_1:9;
reconsider f,g as Morphism of B;
reconsider f' = f ,g' = g as Morphism of C by A1,Th14;
[g,f] in dom the Comp of C by A10,A12,A13,XBOOLE_0:def 3;
then cod f = cod f' & dom g = dom g' & dom g' = cod f'
by A1,Th15,CAT_1:40;
hence x in dom p by A1,A13,CAT_1:40;
end;
the Comp of B <= the Comp of C by A1,Def4;
then dom p c= dom the Comp of C by GRFUNC_1:8;
then A14: dom p c= dom p' by A9,A10,XBOOLE_1:19;
hence
dom p = dom p' by A11,XBOOLE_0:def 10;
let x be set;
assume
A15: x in dom p;
then consider g,f being Element of M such that
A16: x = [g,f] by A9,DOMAIN_1:9;
reconsider f,g as Morphism of B;
reconsider f' = f ,g' = g as Morphism of C by A1,Th14;
A17: cod f = cod f' & dom g = dom g' & dom g = cod f
by A1,A15,A16,Th15,CAT_1:40;
hence p.x = g*f by A1,A16,CAT_1:41
.= g'*f' by A1,A17,Th17
.= (the Comp of C).[g',f'] by A17,CAT_1:41
.= p'.x by A14,A15,A16,FUNCT_1:70;
end;
hence p = (the Comp of C)|[:M,M:] by FUNCT_1:9;
reconsider i' = (the Id of C)|O as Function of O,M by A8,Th29;
now let a be Element of O;
now
reconsider a' = a as Object of C;
reconsider b = a as Object of B;
id b = id a' & id b = (the Id of B).b & id a' = (the Id of C).a'
by A1,Def4,CAT_1:def 5;
hence i.a = (the Id of C).a;
thus a in O;
a in the Objects of C;
hence a in dom the Id of C by FUNCT_2:def 1;
end;
hence i.a = i'.a by FUNCT_1:72;
end;
hence i = (the Id of C)|O by FUNCT_2:113;
end;
:: Product of Categories
definition let X1,X2,Y1,Y2 be non empty set;
let f1 be Function of X1,Y1; let f2 be Function of X2,Y2;
redefine func [:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:];
coherence
proof [:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:]; hence thesis; end;
end;
definition let A,B be non empty set;
let f be PartFunc of [:A,A:],A; let g be PartFunc of [:B,B:],B;
redefine func |:f,g:| -> PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:];
coherence by FUNCT_4:62;
end;
definition let C,D;
func [:C,D:] -> Category equals
:Def7: CatStr (# [:the Objects of C,the Objects of D:],
[:the Morphisms of C,the Morphisms of D:],
[:the Dom of C,the Dom of D:],
[:the Cod of C,the Cod of D:],
|:the Comp of C, the Comp of D:|,
[:the Id of C,the Id of D:]
#);
coherence
proof
set O = [:the Objects of C,the Objects of D:],
M = [:the Morphisms of C,the Morphisms of D:],
d = [:the Dom of C,the Dom of D:],
c = [:the Cod of C,the Cod of D:],
p = |:the Comp of C, the Comp of D:|,
i = [:the Id of C,the Id of D:];
now
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: g = [g`1,g`2] & f = [f`1,f`2] by MCART_1:23;
A3: d.[g`1,g`2] = [(the Dom of C).g`1,(the Dom of D).g`2]
& c.[f`1,f`2] = [(the Cod of C).f`1,(the Cod of D).f`2]
by FUNCT_3:96;
assume d.g = c.f;
then (the Dom of C).g`1 = (the Cod of C).f`1 &
(the Dom of D).g`2 = (the Cod of D).f`2 by A2,A3,ZFMISC_1:33;
hence [g`1,f`1] in dom(the Comp of C) & [g`2,f`2] in dom(the Comp of D)
by CAT_1:def 8;
end;
A4: for f,g being Element of M st [g,f] in dom(p) holds
(the Dom of C).g`1 = (the Cod of C).f`1 &
(the Dom of D).g`2 = (the Cod of D).f`2
proof let f,g be Element of M;
A5: g = [g`1,g`2] & f = [f`1,f`2] by MCART_1:23;
assume [g,f] in dom(p);
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:57;
hence (the Dom of C).g`1 = (the Cod of C).f`1 &
(the Dom of D).g`2 = (the Cod of D).f`2 by CAT_1:def 8;
end;
thus
A6: for f,g being Element of M holds [g,f] in dom(p) iff d.g = c.f
proof let f,g be Element of M;
A7: g = [g`1,g`2] & f = [f`1,f`2] by MCART_1:23;
thus [g,f] in dom(p) implies d.g = c.f
proof assume [g,f] in dom(p);
then (the Dom of C).g`1 = (the Cod of C).f`1 &
(the Dom of D).g`2 = (the Cod of D).f`2 &
d.[g`1,g`2] = [(the Dom of C).g`1,(the Dom of D).g`2]
& c.[f`1,f`2] = [(the Cod of C).f`1,(the Cod of D).f`2]
by A4,FUNCT_3:96;
hence thesis by A7;
end;
assume d.g = c.f;
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:57;
end;
A8: 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;
assume d.g = c.f;
then [g,f] in dom(p) & g = [g`1,g`2] & f = [f`1,f`2] by A6,MCART_1:23;
hence p.[g,f] = [(the Comp of C).[g`1,f`1],(the Comp of D).[g`2,f`2]]
by FUNCT_4:58;
end;
thus
A9: 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;
A10: g = [g`1,g`2] & f = [f`1,f`2] by MCART_1:23;
A11: d.[f`1,f`2] = [(the Dom of C).f`1,(the Dom of D).f`2]
& c.[g`1,g`2] = [(the Cod of C).g`1,(the Cod of D).g`2]
by FUNCT_3:96;
assume
A12: d.g = c.f;
then A13: [g,f] in dom(p) by A6;
[g`1,f`1] in dom(the Comp of C) & [g`2,f`2] in dom(the Comp of D)
by A1,A12;
then (the Dom of C).g`1 = (the Cod of C).f`1 &
(the Dom of D).g`2 = (the Cod of D).f`2 &
(the Comp of C).[g`1,f`1] in the Morphisms of C &
(the Comp of D).[g`2,f`2] in the Morphisms of D by A4,A13,PARTFUN1:27;
then (the Dom of C).((the Comp of C).[g`1,f`1]) = (the Dom of C).f`1 &
(the Dom of D).((the Comp of D).[g`2,f`2]) = (the Dom of D).f`2 &
(the Cod of C).((the Comp of C).[g`1,f`1]) = (the Cod of C).g`1 &
(the Cod of D).((the Comp of D).[g`2,f`2]) = (the Cod of D).g`2 &
(the Comp of C).[g`1,f`1] in dom(the Dom of C) &
(the Comp of D).[g`2,f`2] in dom(the Dom of D) &
(the Comp of C).[g`1,f`1] in dom(the Cod of C) &
(the Comp of D).[g`2,f`2] in dom(the Cod of D) &
p.[g,f] = [(the Comp of C).[g`1,f`1],(the Comp of D).[g`2,f`2]]
by A8,A12,CAT_1:def 8,FUNCT_2:def 1;
hence d.(p.[g,f]) = d.f & c.(p.[g,f]) = c.g by A10,A11,FUNCT_3:def 9;
end;
thus for f,g,h being Element of M
st d.h = c.g & d.g = c.f holds p.[h,p.[g,f]] = p.[p.[h,g],f]
proof let f,g,h be Element of M;
assume
A14: d.h = c.g & d.g = c.f;
then A15: [g`1,f`1] in dom(the Comp of C) & [g`2,f`2] in
dom(the Comp of D) &
[h`1,g`1] in dom(the Comp of C) & [h`2,g`2] in dom(the Comp of D)
by A1;
then (the Comp of C).[g`1,f`1] in the Morphisms of C &
(the Comp of D).[g`2,f`2] in the Morphisms of D &
(the Comp of C).[h`1,g`1] in the Morphisms of C &
(the Comp of D).[h`2,g`2] in the Morphisms of D by PARTFUN1:27;
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 ZFMISC_1:106;
A16: pgf`1 = (the Comp of C).[g`1,f`1] & pgf`2 = (the Comp of D).[g`2,f`2] &
phg`1 = (the Comp of C).[h`1,g`1] & phg`2 = (the Comp of D).[h`2,g`2]
by MCART_1:7;
set pgf1 = pgf`1, phg1 = phg`1;
set pgf2 = pgf`2, phg2 = phg`2;
A17: (the Dom of C).g`1 = (the Cod of C).f`1 &
(the Dom of D).g`2 = (the Cod of D).f`2 &
(the Dom of C).h`1 = (the Cod of C).g`1 &
(the Dom of D).h`2 = (the Cod of D).g`2 by A15,CAT_1:def 8;
p.[g,f] = pgf & p.[h,g] = phg & d.h = c.(p.[g,f]) & d.(p.[h,g]) = c.f
by A8,A9,A14;
then p.[h,p.[g,f]] = [(the Comp of C).[h`1,pgf1],(the Comp of D).[h`2,
pgf2]] &
p.[p.[h,g],f] = [(the Comp of C).[phg1,f`1],(the Comp of D).[phg2,f`2]] &
(the Comp of C).[h`1,pgf1] = (the Comp of C).[phg1,f`1] &
(the Comp of D).[h`2,pgf2] = (the Comp of D).[phg2,f`2]
by A8,A16,A17,CAT_1:def 8;
hence p.[h,p.[g,f]] = p.[p.[h,g],f];
end;
let b be Element of O;
A18: b = [b`1,b`2] by MCART_1:23;
then A19: (the Dom of C).((the Id of C).b`1) = b`1 &
(the Dom of D).((the Id of D).b`2) = b`2 &
(the Cod of C).((the Id of C).b`1) = b`1 &
(the Cod of D).((the Id of D).b`2) = b`2 &
i.b = [(the Id of C).b`1,(the Id of D).b`2] by CAT_1:def 8,FUNCT_3:96;
hence
A20: d.(i.b) = b & c.(i.b) = b by A18,FUNCT_3:96;
A21: (i.b)`1 = (the Id of C).b`1 & (i.b)`2 = (the Id of D).b`2
by A19,MCART_1:7;
thus for f being Element of M st c.f = b holds p.[i.b,f] = f
proof let f be Element of M;
A22: f = [f`1,f`2] by MCART_1:23;
assume
A23: c.f = b;
c.f = [(the Cod of C).f`1,(the Cod of D).f`2] by A22,FUNCT_3:96;
then (the Cod of C).f`1 = b`1 & (the Cod of D).f`2 = b`2
by A18,A23,ZFMISC_1:33;
then p.[i.b,f] =
[(the Comp of C).[(i.b)`1,f`1],(the Comp of D).[(i.b)`2,f`2]] &
(the Comp of C).[(the Id of C).b`1,f`1] = f`1 &
(the Comp of D).[(the Id of D).b`2,f`2] = f`2
by A8,A20,A23,CAT_1:def 8;
hence p.[i.b,f] = f by A21,MCART_1:23;
end;
let g be Element of M;
A24: g = [g`1,g`2] by MCART_1:23;
assume
A25: d.g = b;
d.g = [(the Dom of C).g`1,(the Dom of D).g`2] by A24,FUNCT_3:96;
then (the Dom of C).g`1 = b`1 & (the Dom of D).g`2 = b`2
by A18,A25,ZFMISC_1:33;
then p.[g,i.b] =
[(the Comp of C).[g`1,(i.b)`1],(the Comp of D).[g`2,(i.b)`2]] &
(the Comp of C).[g`1,(the Id of C).b`1] = g`1 &
(the Comp of D).[g`2,(the Id of D).b`2] = g`2
by A8,A20,A25,CAT_1:def 8;
hence p.[g,i.b] = g by A21,MCART_1:23;
end;
hence thesis by CAT_1:def 8;
end;
end;
definition let C,D;
cluster [:C,D:] -> strict;
coherence
proof
[:C,D:] = CatStr (# [:the Objects of C,the Objects of D:],
[:the Morphisms of C,the Morphisms of D:],
[:the Dom of C,the Dom of D:],
[:the Cod of C,the Cod of D:],
|:the Comp of C, the Comp of D:|,
[:the Id of C,the Id of D:]
#) by Def7;
hence [:C,D:] is strict;
end;
end;
canceled;
theorem Th33:
the Objects of [:C,D:] = [:the Objects of C,the Objects of D:] &
the Morphisms of [:C,D:] = [:the Morphisms of C,the Morphisms of D:] &
the Dom of [:C,D:] = [:the Dom of C,the Dom of D:] &
the Cod of [:C,D:] = [:the Cod of C,the Cod of D:] &
the Comp of [:C,D:] = |:the Comp of C, the Comp of D:| &
the Id of [:C,D:] = [:the Id of C,the Id of D:]
proof
[:C,D:] = CatStr (# [:the Objects of C,the Objects of D:],
[:the Morphisms of C,the Morphisms of D:],
[:the Dom of C,the Dom of D:],
[:the Cod of C,the Cod of D:],
|:the Comp of C, the Comp of D:|,
[:the Id of C,the Id of D:]
#)
by Def7;
hence thesis; end;
theorem Th34:
for c being Object of C, d being Object of D
holds [c,d] is Object of [:C,D:] by Th33;
definition let C,D; let c be Object of C; let d be Object of D;
redefine func [c,d] -> Object of [:C,D:];
coherence by Th34;
end;
theorem Th35:
for cd being Object of [:C,D:]
ex c being Object of C, d being Object of D st cd = [c,d]
proof let cd be Object of [:C,D:];
the Objects of [:C,D:] = [:the Objects of C,the Objects of D:] by Th33;
hence thesis by DOMAIN_1:9;
end;
theorem Th36:
for f being Morphism of C for g being Morphism of D
holds [f,g] is Morphism of [:C,D:] by Th33;
definition let C,D; let f be Morphism of C; let g be Morphism of D;
redefine func [f,g] -> Morphism of [:C,D:];
coherence by Th36;
end;
theorem Th37:
for fg being Morphism of [:C,D:]
ex f being (Morphism of C), g being Morphism of D st fg = [f,g]
proof let fg be Morphism of [:C,D:];
the Morphisms of [:C,D:] = [:the Morphisms of C,the Morphisms of D:] by
Th33
;
hence thesis by DOMAIN_1:9;
end;
theorem Th38:
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 Dom of [:C,D:]).[f,g] by CAT_1:def 2
.= ([:the Dom of C,the Dom of D:]).[f,g] by Th33
.= [(the Dom of C).f,(the Dom of D).g] by FUNCT_3:96
.= [dom f,(the Dom of D).g] by CAT_1:def 2
.= [dom f,dom g] by CAT_1:def 2;
thus cod [f,g] = (the Cod of [:C,D:]).[f,g] by CAT_1:def 3
.= ([:the Cod of C,the Cod of D:]).[f,g] by Th33
.= [(the Cod of C).f,(the Cod of D).g] by FUNCT_3:96
.= [cod f,(the Cod of D).g] by CAT_1:def 3
.= [cod f,cod g] by CAT_1:def 3;
end;
theorem Th39:
for f,f' being Morphism of C for g,g' being Morphism of D
st dom f' = cod f & dom g' = cod g holds [f',g']*[f,g] = [f'*f,g'*g]
proof let f,f' be Morphism of C; let g,g' be Morphism of D;
assume
A1: dom f' = cod f & dom g' = cod g;
then A2:
[f',f] in dom(the Comp of C) & [g',g] in dom(the Comp of D) by CAT_1:40;
dom [f',g'] = [dom f',dom g'] & cod [f,g] = [cod f,cod g] by Th38;
hence [f',g']*[f,g]
= (the Comp of [:C,D:]).[[f',g'],[f,g]] by A1,CAT_1:41
.= |:the Comp of C, the Comp of D:|.[[f',g'],[f,g]] by Th33
.= [(the Comp of C).[f',f],(the Comp of D).[g',g]] by A2,FUNCT_4:def 3
.= [f'*f,(the Comp of D).[g',g]] by A1,CAT_1:41
.= [f'*f,g'*g] by A1,CAT_1:41;
end;
theorem Th40:
for f,f' being Morphism of C for g,g' being Morphism of D
st dom [f',g'] = cod [f,g] holds [f',g']*[f,g] = [f'*f,g'*g]
proof let f,f' be Morphism of C; let g,g' be Morphism of D such that
A1: dom [f',g'] = cod [f,g];
[dom f',dom g'] = dom [f',g'] & cod [f,g] = [cod f,cod g] by Th38;
then dom f' = cod f & dom g' = cod g by A1,ZFMISC_1:33;
hence thesis by Th39;
end;
theorem Th41:
for c being Object of C, d being Object of D
holds id [c,d] = [id c,id d]
proof let c be Object of C, d be Object of D;
thus id [c,d] = ( the Id of [:C,D:] ).[c,d] by CAT_1:def 5
.= [:the Id of C,the Id of D:].[c,d] by Th33
.= [(the Id of C).c,(the Id of D).d] by FUNCT_3:96
.= [id c,(the Id of D).d] by CAT_1:def 5
.= [id c,id d] by CAT_1:def 5;
end;
theorem
for c,c' being Object of C, d,d' being Object of D
holds Hom([c,d],[c',d']) = [:Hom(c,c'),Hom(d,d'):]
proof let c,c' be Object of C, d,d' be Object of D;
now let x be set;
thus x in Hom([c,d],[c',d']) implies x in [:Hom(c,c'),Hom(d,d'):]
proof assume
A1: x in Hom([c,d],[c',d']);
then reconsider fg = x as Morphism of [c,d],[c',d'] by CAT_1:def 7;
A2: dom fg = [c,d] & cod fg = [c',d'] by A1,CAT_1:18;
fg in the Morphisms of [:C,D:];
then fg in [:the Morphisms of C,the Morphisms of D:] by Th33;
then consider x1,x2 being set such that
A3: x1 in the Morphisms of C & x2 in the Morphisms of D and
A4: fg = [x1,x2] by ZFMISC_1:def 2;
reconsider f = x1 as Morphism of C by A3;
reconsider g = x2 as Morphism of D by A3;
dom fg = [dom f,dom g] & cod fg = [cod f,cod g] by A4,Th38;
then dom f = c & cod f = c' & dom g = d & cod g = d' by A2,ZFMISC_1:33;
then f in Hom(c,c') & g in Hom(d,d') by CAT_1:18;
hence thesis by A4,ZFMISC_1:106;
end;
assume x in [:Hom(c,c'),Hom(d,d'):];
then consider x1,x2 being set such that
A5: x1 in Hom(c,c') & x2 in Hom(d,d') and
A6: x = [x1,x2] by ZFMISC_1:def 2;
reconsider f = x1 as Morphism of c,c' by A5,CAT_1:def 7;
reconsider g = x2 as Morphism of d,d' by A5,CAT_1:def 7;
dom f = c & cod f = c' & dom g = d & cod g = d' by A5,CAT_1:18;
then dom [f,g] = [c,d] & cod [f,g] = [c',d'] by Th38;
hence x in Hom([c,d],[c',d']) by A6,CAT_1:18;
end;
hence thesis by TARSKI:2;
end;
theorem
for c,c' being Object of C, f being Morphism of c,c',
d,d' being Object of D, g being Morphism of d,d'
st Hom(c,c') <> {} & Hom(d,d') <> {}
holds [f,g] is Morphism of [c,d],[c',d']
proof let c,c' be Object of C, f be Morphism of c,c',
d,d' be Object of D, g be Morphism of d,d';
assume Hom(c,c') <> {} & Hom(d,d') <> {};
then dom f = c & cod f = c' & dom g = d & cod g = d' by CAT_1:23;
then dom [f,g] = [c,d] & cod [f,g] = [c',d'] by Th38;
hence thesis by CAT_1:22;
end;
:: Bifunctors
theorem Th44:
for S being Functor of [:C,C':],D, c being Object of C
holds (curry S).(id c) is Functor of C',D
proof let S be Functor of [:C,C':],D, c be Object of C;
[:the Morphisms of C,the Morphisms of C':]
= the Morphisms of [:C,C':] by Th33;
then reconsider S' = S as
Function of [:the Morphisms of C,the Morphisms of C':],the Morphisms of D;
reconsider T = (curry S').(id c)
as Function of the Morphisms of C',the Morphisms 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,c']) = id d by CAT_1:97;
take d;
thus T.(id c') = S.[id c,id c'] by Th3
.= id d by A1,Th41;
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) = S.[id c,id dom f] by Th3
.= S.(id [c,dom f]) by Th41
.= S.(id [dom id c,dom f]) by CAT_1:44
.= S.(id dom [id c,f]) by Th38
.= id dom (S.[id c,f]) by CAT_1:98
.= id dom (T.f) by Th3;
thus T.(id cod f) = S.[id c,id cod f] by Th3
.= S.(id [c,cod f]) by Th41
.= S.(id [cod id c,cod f]) by CAT_1:44
.= S.(id cod [id c,f]) by Th38
.= id cod (S.[id c,f]) by CAT_1:98
.= id cod (T.f) by Th3;
end;
let f,g be Morphism of C' such that
A2: dom g = cod f;
A3: dom id c = c & cod id c = c by CAT_1:44;
A4: dom [id c,g] = [dom id c,dom g] & cod [id c,f] = [cod id c, cod f]
by Th38;
Hom(c,c) <> {} by CAT_1:56;
then A5: (id c)*(id c) = (id c)*((id c) qua Morphism of C) by CAT_1:def 13;
(id c)*(id c) = id c by CAT_1:59;
hence T.(g*f) = S.[(id c)*(id c),g*f] by Th3
.= S.([id c,g]*[id c,f]) by A2,A3,A5,Th39
.= (S.[id c,g])*(S.[id c,f]) by A2,A3,A4,CAT_1:99
.= (T.g)*(S.[id c,f]) by Th3
.= (T.g)*(T.f) by Th3;
end;
hence thesis by CAT_1:96;
end;
theorem Th45:
for S being Functor of [:C,C':],D, c' being Object of C'
holds (curry' S).(id c') is Functor of C,D
proof let S be Functor of [:C,C':],D, c' be Object of C';
[:the Morphisms of C,the Morphisms of C':]
= the Morphisms of [:C,C':] by Th33;
then reconsider S' = S as
Function of [:the Morphisms of C,the Morphisms of C':],the Morphisms of D;
reconsider T = (curry' S').(id c')
as Function of the Morphisms of C,the Morphisms 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,c']) = id d by CAT_1:97;
take d;
thus T.(id c) = S.[id c,id c'] by Th4
.= id d by A1,Th41;
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) = S.[id dom f,id c'] by Th4
.= S.(id [dom f,c']) by Th41
.= S.(id [dom f,dom id c']) by CAT_1:44
.= S.(id dom [f,id c']) by Th38
.= id dom (S.[f,id c']) by CAT_1:98
.= id dom (T.f) by Th4;
thus T.(id cod f) = S.[id cod f,id c'] by Th4
.= S.(id [cod f,c']) by Th41
.= S.(id [cod f,cod id c']) by CAT_1:44
.= S.(id cod [f,id c']) by Th38
.= id cod (S.[f,id c']) by CAT_1:98
.= id cod (T.f) by Th4;
end;
let f,g be Morphism of C such that
A2: dom g = cod f;
A3: dom id c' = c' & cod id c' = c' by CAT_1:44;
A4: dom [g,id c'] = [dom g,dom id c'] & cod [f,id c'] = [cod f,cod id c']
by Th38;
Hom(c',c') <> {} by CAT_1:56;
then A5: (id c')*(id c') = (id c')*((id c') qua Morphism of C') by CAT_1:def
13;
(id c')*(id c') = id c' by CAT_1:59;
hence T.(g*f) = S.[g*f,(id c')*(id c')] by Th4
.= S.([g,id c']*[f,id c']) by A2,A3,A5,Th39
.= (S.[g,id c'])*(S.[f,id c']) by A2,A3,A4,CAT_1:99
.= (T.g)*(S.[f,id c']) by Th4
.= (T.g)*(T.f) by Th4;
end;
hence thesis by CAT_1:96;
end;
:: Partial Functors
definition let C,C',D; let S be Functor of [:C,C':],D, c be Object of C;
func S?-c -> Functor of C',D equals
:Def8: (curry S).(id c);
coherence by Th44;
end;
canceled;
theorem Th47:
for S being Functor of [:C,C':],D, c being Object of C,
f being Morphism of C' holds (S?-c).f = S.[id c,f]
proof let S be Functor of [:C,C':],D, c be Object of C, f be Morphism of C';
[:the Morphisms of C,the Morphisms of C':]
= the Morphisms of [:C,C':] by Th33;
then reconsider S' = S as
Function of [:the Morphisms of C,the Morphisms of C':],the Morphisms of D;
thus (S?-c).f = ((curry S').(id c)).f by Def8
.= S.[id c,f] by Th3;
end;
theorem
for S being Functor of [:C,C':],D,
c being Object of C, c' being Object of C'
holds (Obj S?-c).c' = (Obj S).[c,c']
proof let S be Functor of [:C,C':],D, c be Object of C, c' be Object of C';
[:the Morphisms of C,the Morphisms of C':]
= the Morphisms of [:C,C':] by Th33;
then reconsider S' = S as
Function of [:the Morphisms of C,the Morphisms of C':],the Morphisms of D;
(S?-c).(id c') = ((curry S').(id c)).(id c') by Def8
.= S.[id c,id c'] by Th3
.= S.(id [c,c']) by Th41
.= id ((Obj S).[c,c']) by CAT_1:104;
hence thesis by CAT_1:103;
end;
definition let C,C',D; let S be Functor of [:C,C':],D, c' be Object of C';
func S-?c' -> Functor of C,D equals
:Def9: (curry' S).(id c');
coherence by Th45;
end;
canceled;
theorem Th50:
for S being Functor of [:C,C':],D, c' being Object of C',
f being Morphism of C holds (S-?c').f = S.[f,id c']
proof let S be Functor of [:C,C':],D, c' be Object of C', f be Morphism of C;
[:the Morphisms of C,the Morphisms of C':]
= the Morphisms of [:C,C':] by Th33;
then reconsider S' = S as
Function of [:the Morphisms of C,the Morphisms of C':],the Morphisms of D;
thus (S-?c').f = ((curry' S').(id c')).f by Def9
.= S.[f,id c'] by Th4;
end;
theorem
for S being Functor of [:C,C':],D,
c being Object of C, c' being Object of C'
holds (Obj S-?c').c = (Obj S).[c,c']
proof let S be Functor of [:C,C':],D, c be Object of C, c' be Object of C';
[:the Morphisms of C,the Morphisms of C':]
= the Morphisms of [:C,C':] by Th33;
then reconsider S' = S as
Function of [:the Morphisms of C,the Morphisms of C':],the Morphisms of D;
(S-?c').(id c) = ((curry' S').(id c')).(id c) by Def9
.= S.[id c,id c'] by Th4
.= S.(id [c,c']) by Th41
.= id ((Obj S).[c,c']) by CAT_1:104;
hence thesis by CAT_1:103;
end;
theorem
for L being Function of the Objects of C,Funct(B,D),
M being Function of the Objects 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 let L be Function of the Objects of C,Funct(B,D),
M be Function of the Objects 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 Mor(Category) = the Morphisms of $1;
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 Lambda2D;
[:the Morphisms of B,the Morphisms of C:]
= the Morphisms of [:B,C:] by Th33;
then 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 Th35;
consider d being Object of D such that
A5: (L.c).(id b) = id d by CAT_1:97;
take d;
Hom(d,d) <> {} by CAT_1:56;
then (id d)*(id d) = (id d)*((id d) qua Morphism of D) &
cod id c = c & dom id b = b & (L.c).(id b) = (M.b).(id c)
by A1,CAT_1:44,def 13;
then ((L.(cod id c)).(id b))*((M.(dom id b)).(id c)) = id d &
id bc = [id b,id c] by A4,A5,Th41,CAT_1:59;
hence thesis by A3;
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
A6: fg = [f,g] by Th37;
set b = dom f, c = dom g;
set g' = id c, f'= id b;
A7: Hom(dom ((M.b).g),dom ((M.b).g)) <> {} by CAT_1:56;
id dom ((L.(cod g)).f) = (L.(cod g)).(id dom f) by CAT_1:98
.= (M.(dom f)).(id cod g) by A1
.= id cod ((M.(dom f)).g) by CAT_1:98;
then A8: dom ((L.(cod g)).f) = cod ((M.(dom f)).g) by CAT_1:45;
thus T.(id (dom fg))
= S.(id [b,c]) by A6,Th38
.= S.[id b,id c] by Th41
.= ((L.(cod g')).f')*((M.(dom f')).g') by A3
.= ((L.c).f')*((M.(dom f')).g') by CAT_1:44
.= ((L.c).f')*((M.b).g') by CAT_1:44
.= ((M.b).g')*((M.b).g') by A1
.= (id dom ((M.b).g))*((M.b).g') by CAT_1:98
.= (id dom ((M.b).g))*((id dom((M.b).g)) qua Morphism of D) by CAT_1:98
.= (id dom ((M.b).g))*(id dom((M.b).g)) by A7,CAT_1:def 13
.= id dom ((M.(dom f)).g) by CAT_1:59
.= id dom (((L.(cod g)).f)*((M.(dom f)).g)) by A8,CAT_1:42
.= id dom (T.fg) by A3,A6;
set b = cod f, c = cod g;
set g' = id c, f'= id b;
A9: Hom(cod ((L.c).f),cod ((L.c).f)) <> {} by CAT_1:56;
thus T.(id (cod fg))
= S.(id [b,c]) by A6,Th38
.= S.[id b,id c] by Th41
.= ((L.(cod g')).f')*((M.(dom f')).g') by A3
.= ((L.c).f')*((M.(dom f')).g') by CAT_1:44
.= ((L.c).f')*((M.(cod f)).g') by CAT_1:44
.= ((L.c).f')*((L.c).f') by A1
.= (id cod (((L.c).f))*((L.c).f')) by CAT_1:98
.= (id cod ((L.c).f))*((id cod((L.c).f)) qua Morphism of D) by CAT_1:98
.= (id cod ((L.c).f))*(id cod ((L.c).f)) by A9,CAT_1:def 13
.= id cod ((L.(cod g)).f) by CAT_1:59
.= id cod (((L.(cod g)).f)*((M.(dom f)).g)) by A8,CAT_1:42
.= id cod (T.fg) by A3,A6;
end;
let fg1,fg2 be Morphism of [:B,C:] such that
A10: dom fg2 = cod fg1;
consider f1 being (Morphism of B), g1 being Morphism of C such that
A11: fg1 = [f1,g1] by Th37;
consider f2 being (Morphism of B), g2 being Morphism of C such that
A12: fg2 = [f2,g2] by Th37;
[dom f2,dom g2] = dom fg2 & [cod f1,cod g1] = cod fg1 by A11,A12,Th38;
then A13: dom f2 = cod f1 & dom g2 = cod g1 by A10,ZFMISC_1:33;
set f = f2*f1, g = g2*g1;
set L1 = L.(cod g1), L2 = L.(cod g2), M1 = M.(dom f1), M2 = M.(dom f2);
A14: dom(L2.f2) = cod (L2.f1) & dom(M1.g2) = cod (M1.g1) by A13,CAT_1:99;
then A15: cod ((M1.g2)*(M1.g1)) = cod(M1.g2) by CAT_1:42;
id dom (L2.f1) = L2.(id dom f1) by CAT_1:98
.= M1.(id cod g2) by A1
.= id cod (M1.g2) by CAT_1:98;
then A16: dom (L2.f1) = cod (M1.g2) by CAT_1:45;
id dom (L1.f1) = L1.(id dom f1) by CAT_1:98
.= M1.(id cod g1) by A1
.= id cod (M1.g1) by CAT_1:98;
then A17: dom (L1.f1) = cod (M1.g1) by CAT_1:45;
id dom (M2.g2) = M2.(id dom g2) by CAT_1:98
.= L1.(id cod f1) by A1,A13
.= id cod (L1.f1) by CAT_1:98;
then A18: dom (M2.g2) = cod(L1.f1) by CAT_1:45;
id dom (L2.f2) = L2.(id dom f2) by CAT_1:98
.= M2.(id cod g2) by A1
.= id cod (M2.g2) by CAT_1:98;
then A19: dom (L2.f2) = cod (M2.g2) by CAT_1:45;
A20: cod ((L1.f1)*(M1.g1)) = cod (L1.f1) by A17,CAT_1:42;
thus T.(fg2*fg1)
= S.[f,g] by A10,A11,A12,Th40
.= ((L.(cod g)).f)*((M.(dom f)).g) by A3
.= ((L.(cod g2)).f)*((M.(dom f)).g) by A13,CAT_1:42
.= ((L.(cod g2)).f)*((M.(dom f1)).g) by A13,CAT_1:42
.= ((L2.f2)*(L2.f1))*(M1.g) by A13,CAT_1:99
.= ((L2.f2)*(L2.f1))*((M1.g2)*(M1.g1)) by A13,CAT_1:99
.= (L2.f2)*((L2.f1)*((M1.g2)*(M1.g1))) by A14,A15,A16,CAT_1:43
.= (L2.f2)*(((L2.f1)*(M1.g2))*(M1.g1)) by A14,A16,CAT_1:43
.= (L2.f2)*(((M2.g2)*(L1.f1))*(M1.g1)) by A2,A13
.= (L2.f2)*((M2.g2)*((L1.f1)*(M1.g1))) by A17,A18,CAT_1:43
.= ((L2.f2)*(M2.g2))*((L1.f1)*(M1.g1)) by A18,A19,A20,CAT_1:43
.= ((L2.f2)*(M2.g2))*(T.fg1) by A3,A11
.= (T.fg2)*(T.fg1) by A3,A12;
end;
then reconsider T as Functor of [:B,C:],D by CAT_1:96;
take T; thus thesis by A3;
end;
theorem
for L being Function of the Objects of C,Funct(B,D),
M being Function of the Objects 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 Objects of C,Funct(B,D),
M be Function of the Objects 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 & cod id dom g = dom g by CAT_1:44;
then A2: dom [id cod f,g] = [cod f,dom g] & cod [f,id dom g] = [cod f, dom g]
by Th38;
dom id cod g = cod g & cod id dom f = dom f by CAT_1:44;
then A3: dom [f,id cod g] = [dom f,cod g] & cod [id dom f,g] = [dom f,cod g]
by Th38;
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 Th47
.= (S.[id cod f,g])*(S.[f,id dom g]) by Th50
.= S.([id cod f,g]*[f,id dom g]) by A2,CAT_1:99
.= S.[(id cod f)*f,g*(id dom g)] by A2,Th40
.= S.[f,g*(id dom g)] by CAT_1:46
.= S.[f,g] by CAT_1:47
.= S.[f*(id dom f),g] by CAT_1:47
.= S.[f*(id dom f),(id cod g)*g ] by CAT_1:46
.= S.([f,id cod g]*[id dom f,g]) by A3,Th40
.= (S.[f,id cod g])*(S.[id dom f,g]) by A3,CAT_1:99
.= ((S-?(cod g)).f)*(S.[id dom f,g]) by Th50
.= ((S-?(cod g)).f)*((S?-(dom f)).g) by Th47
.= ((L.(cod g)).f)*((S?-(dom f)).g) by A1
.= ((L.(cod g)).f)*((M.(dom f)).g) by A1;
end;
theorem Th54:
pr1(the Morphisms of C,the Morphisms of D) is Functor of [:C,D:],C
proof
[:the Morphisms of C,the Morphisms of D:]
= the Morphisms of [:C,D:] by Th33;
then reconsider T = pr1(the Morphisms of C,the Morphisms of D)
as Function of the Morphisms of [:C,D:],the Morphisms 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 Th35;
id cd = [id c,id d] by A1,Th41;
then T.(id cd) = id c by FUNCT_3:def 5;
hence thesis;
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
A2: fg = [f,g] by Th37;
now dom [f,g] = [dom f,dom g] & cod [f,g] = [cod f,cod g] by Th38;
hence id dom fg = [id dom f,id dom g] & id cod fg = [id cod f,id cod g]
by A2,Th41;
hence T.(id dom fg) = id dom f & T.(id cod fg) = id cod f
by FUNCT_3:def 5;
end;
hence thesis by A2,FUNCT_3:def 5;
end;
let fg,fg' be Morphism of [:C,D:] such that
A3: dom fg' = cod fg;
consider f being (Morphism of C), g being Morphism of D such that
A4: fg = [f,g] by Th37;
consider f' being (Morphism of C), g' being Morphism of D such that
A5: fg' = [f',g'] by Th37;
dom [f',g'] = [dom f',dom g'] & cod [f,g] = [cod f,cod g] by Th38;
then dom f' = cod f & dom g' = cod g by A3,A4,A5,ZFMISC_1:33;
then fg'*fg = [f'*f,g'*g] & T.fg' = f' & T.fg = f by A4,A5,Th39,FUNCT_3:def
5;
hence T.(fg'*fg) = (T.fg')*(T.fg) by FUNCT_3:def 5;
end;
hence thesis by CAT_1:96;
end;
theorem Th55:
pr2(the Morphisms of C,the Morphisms of D) is Functor of [:C,D:],D
proof
[:the Morphisms of C,the Morphisms of D:]
= the Morphisms of [:C,D:] by Th33;
then reconsider T = pr2(the Morphisms of C,the Morphisms of D)
as Function of the Morphisms of [:C,D:],the Morphisms 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
A1: cd = [c,d] by Th35;
id cd = [id c,id d] by A1,Th41;
then T.(id cd) = id d by FUNCT_3:def 6;
hence thesis;
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
A2: fg = [f,g] by Th37;
now dom [f,g] = [dom f,dom g] & cod [f,g] = [cod f,cod g] by Th38;
hence id dom fg = [id dom f,id dom g] & id cod fg = [id cod f,id cod g]
by A2,Th41;
hence T.(id dom fg) = id dom g & T.(id cod fg) = id cod g
by FUNCT_3:def 6;
end;
hence thesis by A2,FUNCT_3:def 6;
end;
let fg,fg' be Morphism of [:C,D:] such that
A3: dom fg' = cod fg;
consider f being (Morphism of C), g being Morphism of D such that
A4: fg = [f,g] by Th37;
consider f' being (Morphism of C), g' being Morphism of D such that
A5: fg' = [f',g'] by Th37;
dom [f',g'] = [dom f',dom g'] & cod [f,g] = [cod f,cod g] by Th38;
then dom f' = cod f & dom g' = cod g by A3,A4,A5,ZFMISC_1:33;
then fg'*fg = [f'*f,g'*g] & T.fg' = g' & T.fg = g by A4,A5,Th39,FUNCT_3:def
6;
hence T.(fg'*fg) = (T.fg')*(T.fg) by FUNCT_3:def 6;
end;
hence thesis by CAT_1:96;
end;
definition let C,D;
func pr1(C,D) -> Functor of [:C,D:],C equals
:Def10: pr1(the Morphisms of C,the Morphisms of D);
coherence by Th54;
func pr2(C,D) -> Functor of [:C,D:],D equals
:Def11: pr2(the Morphisms of C,the Morphisms of D);
coherence by Th55;
end;
canceled 2;
theorem Th58:
for f being (Morphism of C),g being Morphism of D
holds pr1(C,D).[f,g] = f
proof pr1(C,D) = pr1(the Morphisms of C,the Morphisms of D) by Def10;
hence thesis by FUNCT_3:def 5;
end;
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] by Th41;
then (pr1(C,D)).(id [c,d]) = id c by Th58;
hence thesis by CAT_1:103;
end;
theorem Th60:
for f being (Morphism of C),g being Morphism of D
holds pr2(C,D).[f,g] = g
proof pr2(C,D) = pr2(the Morphisms of C,the Morphisms of D) by Def11;
hence thesis by FUNCT_3:def 6;
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] by Th41;
then (pr2(C,D)).(id [c,d]) = id d by Th60;
hence thesis by CAT_1:103;
end;
theorem Th62:
for T being Functor of C,D, T' being Functor of C,D'
holds <:T,T':> is Functor of C,[:D,D':]
proof let T be Functor of C,D, T' be Functor of C,D';
[:the Morphisms of D,the Morphisms of D':]
= the Morphisms of [:D,D':] by Th33;
then reconsider S = <:T,T':>
as Function of the Morphisms of C,the Morphisms of [:D,D':];
now
thus for c being Object of C
ex dd' being Object of [:D,D':] st S.(id c) = id dd'
proof let c be Object of C;
set d = (Obj T).c, d' = (Obj T').c;
take dd' = [d,d'];
thus S.(id c) = [T.(id c),T'.(id c)] by FUNCT_3:79
.= [id d,T'.(id c)] by CAT_1:104
.= [id d,id d'] by CAT_1:104
.= id dd' by Th41;
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)) & T'.(id dom f) = id(dom(T'.f)) by CAT_1:98;
hence S.(id dom f) = [id(dom(T.f)),id(dom(T'.f))] by FUNCT_3:79
.= id [dom(T.f),dom(T'.f)] by Th41
.= id dom[T.f,T'.f] by Th38
.= id dom (S.f) by FUNCT_3:79;
T.(id cod f) = id(cod(T.f)) & T'.(id cod f) = id(cod(T'.f)) by CAT_1:98;
hence S.(id cod f) = [id(cod(T.f)),id(cod(T'.f))] by FUNCT_3:79
.= id [cod(T.f),cod(T'.f)] by Th41
.= id cod [T.f,T'.f] by Th38
.= id cod (S.f) by FUNCT_3:79;
end;
let f,g be Morphism of C;
assume
A1: dom g = cod f;
then A2: dom(T.g) = cod(T.f) & dom(T'.g) = cod(T'.f) by CAT_1:99;
T.(g*f) = (T.g)*(T.f) & T'.(g*f) = (T'.g)*(T'.f) by A1,CAT_1:99;
hence S.(g*f) = [(T.g)*(T.f),(T'.g)*(T'.f)] by FUNCT_3:79
.= [T.g,T'.g]*[T.f,T'.f] by A2,Th39
.= (S.g)*[T.f,T'.f] by FUNCT_3:79
.= (S.g)*(S.f) by FUNCT_3:79;
end;
hence thesis by CAT_1:96;
end;
definition let C,D,D';
let T be Functor of C,D, T' be Functor of C,D';
redefine func <:T,T':> -> Functor of C,[:D,D':];
coherence by Th62;
end;
theorem
for T being Functor of C,D, T' being Functor of C,D', c being Object of C
holds (Obj <:T,T':>).c = [(Obj T).c,(Obj T').c]
proof let T be Functor of C,D, T' be Functor of C,D', c be Object of C;
T.(id c) = id((Obj T).c) & T'.(id c) = id((Obj T').c) &
<:T,T':>.(id c) = [T.(id c),T'.(id c)] &
[id((Obj T).c),id((Obj T').c)] = id [(Obj T).c,(Obj T').c] by Th41,CAT_1:104,
FUNCT_3:79;
hence thesis by CAT_1:103;
end;
theorem Th64:
for T being Functor of C,D, T' being Functor of C',D'
holds [:T,T':] = <:T*pr1(C,C'),T'*pr2(C,C'):>
proof let T be Functor of C,D, T' be Functor of C',D';
pr1(C,C') = pr1(the Morphisms of C,the Morphisms of C') &
pr2(C,C') = pr2(the Morphisms of C,the Morphisms of C') &
dom T = the Morphisms of C & dom T' = the Morphisms of C'
by Def10,Def11,FUNCT_2:def 1;
hence [:T,T':] = <:T*pr1(C,C'),T'*pr2(C,C'):> by FUNCT_3:87;
end;
theorem Th65:
for T being Functor of C,D, T' being Functor of C',D'
holds [:T,T':] is Functor of [:C,C':],[:D,D':]
proof let T be Functor of C,D, T' be Functor of C',D';
T*pr1(C,C') is Functor of [:C,C':],D & T'*pr2(C,C') is Functor of [:C,C':],
D'
& [:T,T':] = <:T*pr1(C,C'),T'*pr2(C,C'):> by Th64;
hence thesis;
end;
definition let C,C',D,D';
let T be Functor of C,D, T' be Functor of C',D';
redefine func [:T,T':] -> Functor of [:C,C':],[:D,D':];
coherence by Th65;
end;
theorem
for T being Functor of C,D, T' being Functor of C',D',
c being Object of C, c' being Object of C'
holds (Obj [:T,T':]).[c,c'] = [(Obj T).c,(Obj T').c']
proof let T be Functor of C,D, T' be Functor of C',D';
let c be Object of C, c' be Object of C';
T.(id c) = id((Obj T).c) & T'.(id c') = id((Obj T').c') &
[:T,T':].[id c,id c'] = [T.(id c),T'.(id c')] & [id c,id c'] = id [c,c'] &
[id((Obj T).c),id((Obj T').c')] = id [(Obj T).c,(Obj T').c'] by Th41,CAT_1
:104,FUNCT_3:96;
hence thesis by CAT_1:103;
end;