Copyright (c) 1992 Association of Mizar Users
environ
vocabulary FUNCT_1, CAT_1, WELLORD1, BOOLE, FINSET_1, CAT_3, RELAT_1,
FUNCOP_1, FINSEQ_4, CARD_1, ARYTM_1, FUNCT_4, FUNCT_6, PARTFUN1, FUNCT_3,
ALGSTR_1, DIRAF, EQREL_1, CAT_4;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, DOMAIN_1, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, ALGSTR_1, REAL_1, NAT_1, CARD_1, FUNCT_4,
CAT_1, CAT_3;
constructors DOMAIN_1, ALGSTR_1, REAL_1, NAT_1, CAT_3, FINSEQ_4, PARTFUN1,
XREAL_0, XBOOLE_0;
clusters SUBSET_1, FINSET_1, RELSET_1, RELAT_1, FUNCT_1, NAT_1, ZFMISC_1,
XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE;
definitions CAT_1, CAT_3;
theorems TARSKI, ZFMISC_1, FUNCT_2, FUNCOP_1, FUNCT_4, CARD_1, CARD_2, CAT_1,
CAT_3, FUNCT_1, RELSET_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes NAT_1;
begin
reserve o,m,r for set;
definition let o,m,r;
func (o,m) :-> r -> Function of [:{o},{m}:],{r} means
not contradiction;
existence;
uniqueness by FUNCT_2:66;
end;
definition let C be Category, a,b be Object of C;
redefine pred a,b are_isomorphic means
Hom(a,b)<>{} & Hom(b,a)<>{} &
ex f being Morphism of a,b, f' being Morphism of b,a
st f*f' = id b & f'*f = id a;
compatibility by CAT_1:81;
end;
begin :: Cartesian Categories
definition let C be Category;
attr C is with_finite_product means
for I being finite set, F being Function of I,the Objects of C
ex a being Object of C, F' being Projections_family of a,I
st cods F' = F & a is_a_product_wrt F';
synonym C has_finite_product;
end;
theorem Th1:
for C being Category holds
C has_finite_product iff
(ex a being Object of C st a is terminal) &
for a,b being Object of C
ex c being Object of C, p1,p2 being Morphism of C
st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b &
c is_a_product_wrt p1,p2
proof let C be Category;
thus C has_finite_product implies
(ex a being Object of C st a is terminal) &
for a,b being Object of C
ex c being Object of C, p1,p2 being Morphism of C
st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b &
c is_a_product_wrt p1,p2
proof assume
A1: for I being finite set, F being Function of I,the Objects of C
ex a being Object of C, F' being Projections_family of a,I
st cods F' = F & a is_a_product_wrt F';
reconsider F = {} as Function of {},the Objects of C by FUNCT_2:55,RELAT_1:
60;
consider a being Object of C, F' being Projections_family of a,{}
such that cods F' = F and
A2: a is_a_product_wrt F' by A1;
a is terminal by A2,CAT_3:55;
hence ex a being Object of C st a is terminal;
let a,b be Object of C;
set F = (0,1)-->(a,b);
consider c being Object of C, F' being Projections_family of c,{0,1}
such that
A3: cods F' = F and
A4: c is_a_product_wrt F' by A1;
take c, p1 = F'/.0, p2 = F'/.1;
A5: 0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
hence dom p1 = c & dom p2 = c by CAT_3:45;
F/.0 = a & F/.1 = b by CAT_3:7;
hence cod p1 = a & cod p2 = b by A3,A5,CAT_3:def 4;
A6: dom F' = {0,1} by FUNCT_2:def 1;
p1 = F'.0 & p2 = F'.1 by A5,CAT_3:def 1;
then 0 <> 1 & F' = (0,1)-->(p1,p2) by A6,FUNCT_4:69;
hence c is_a_product_wrt p1,p2 by A4,CAT_3:59;
end;
given a being Object of C such that
A7: a is terminal;
assume
A8:for a,b being Object of C
ex c being Object of C, p1,p2 being Morphism of C
st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b &
c is_a_product_wrt p1,p2;
defpred Q[Nat] means
for I being finite set, F being Function of I,the Objects of C
st card I = $1
ex a being Object of C, F' being Projections_family of a,I
st cods F' = F & a is_a_product_wrt F';
A9: Q[ 0 ]
proof let I be finite set, F be Function of I,the Objects of C;
assume A10: card I = 0;
then A11: I = {} by CARD_2:59;
{} is Function of {}, the Morphisms of C by FUNCT_2:55,RELAT_1:60;
then reconsider F' = {} as Projections_family of a,I by A11,CAT_3:46;
take a,F';
for x being set st x in I holds (cods F')/.x = F/.x by A10,CARD_2:59;
hence cods F' = F by CAT_3:1;
thus thesis by A7,A11,CAT_3:55;
end;
A12: for n being Nat st Q[n] holds Q[n+1]
proof let n be Nat such that
A13: Q[n];
let I be finite set, F be Function of I,the Objects of C such that
A14: card I = n+1;
consider x being Element of I;
reconsider Ix = I \ {x} as finite set;
A15: {x} c= I by A14,CARD_1:47,ZFMISC_1:37;
reconsider sx = {x} as finite set;
A16: card(Ix) = card(I) - card(sx) by A15,CARD_2:63
.= card(I) - 1 by CARD_1:79
.= n by A14,XCMPLX_1:26;
A17: I\{x} c= I & the Objects of C <> {} by XBOOLE_1:36;
then reconsider G = F|(I\{x}) as Function of I\{x},the Objects of C
by FUNCT_2:38;
consider a being Object of C, G' being Projections_family of a,I\{x}
such that
A18: cods G' = G and
A19: a is_a_product_wrt G' by A13,A16;
consider c being Object of C, p1,p2 being Morphism of C
such that
A20: dom p1 = c & dom p2 = c and
A21: cod p1 = a & cod p2 = F/.x and
A22: c is_a_product_wrt p1,p2 by A8;
set F' = (G'*p1) +* ({x} -->p2);
A23: dom(G'*p1) = I\{x} & dom({x} -->p2) = {x} by FUNCT_2:def 1;
then A24: dom(G'*p1) \/ dom({x} -->p2) = I \/ {x} by XBOOLE_1:39
.= I by A14,CARD_1:47,ZFMISC_1:46;
then A25: dom F' = I by FUNCT_4:def 1;
A26: rng F' c= rng(G'*p1) \/ rng({x} -->p2) by FUNCT_4:18;
rng(G'*p1) c= the Morphisms of C & rng({x} -->p2) c= the Morphisms of C
by RELSET_1:12;
then rng(G'*p1) \/ rng({x} -->p2) c= the Morphisms of C by XBOOLE_1:8;
then rng F' c= the Morphisms of C by A26,XBOOLE_1:1;
then reconsider F' as Function of I, the Morphisms of C
by A25,FUNCT_2:def 1,RELSET_1:11;
A27: doms G' = (I\{x})-->a by CAT_3:def 14;
now let y be set;
assume
A28: y in I;
now per cases;
suppose y = x;
then A29: y in {x} by TARSKI:def 1;
F'/.y = F'.y by A28,CAT_3:def 1
.= ({x} -->p2).y by A23,A29,FUNCT_4:14
.= p2 by A29,FUNCOP_1:13;
hence (I --> c).y = dom(F'/.y) by A20,A28,FUNCOP_1:13
.= (doms F')/.y by A28,CAT_3:def 3;
suppose
A30: y <> x;
then A31: not y in {x} by TARSKI:def 1;
A32: y in I\{x} by A28,A30,ZFMISC_1:64;
F'/.y = F'.y by A28,CAT_3:def 1
.= (G'*p1).y by A23,A24,A28,A31,FUNCT_4:def 1
.= (G'*p1)/.y by A32,CAT_3:def 1;
hence (doms F')/.y = dom((G'*p1)/.y) by A28,CAT_3:def 3
.= (doms(G'*p1))/.y by A32,CAT_3:def 3
.= ((I\{x})-->c)/.y by A20,A21,A27,CAT_3:20
.= c by A32,CAT_3:2
.= (I --> c).y by A28,FUNCOP_1:13;
end;
hence (doms F').y = (I --> c).y by A28,CAT_3:def 1;
end;
then doms F' = I --> c by FUNCT_2:18;
then reconsider F' as Projections_family of c,I by CAT_3:def 14;
take c,F';
now let y be set;
assume
A33: y in I;
now per cases;
suppose
A34: y = x;
then A35: y in {x} by TARSKI:def 1;
F'/.y = F'.y by A33,CAT_3:def 1
.= ({x} -->p2).y by A23,A35,FUNCT_4:14
.= p2 by A35,FUNCOP_1:13;
hence (cods F')/.y = F/.y by A21,A33,A34,CAT_3:def 4;
suppose
A36: y <> x;
then A37: not y in {x} by TARSKI:def 1;
A38: y in I\{x} by A33,A36,ZFMISC_1:64;
F'/.y = F'.y by A33,CAT_3:def 1
.= (G'*p1).y by A23,A24,A33,A37,FUNCT_4:def 1
.= (G'*p1)/.y by A38,CAT_3:def 1;
hence (cods F')/.y = cod((G'*p1)/.y) by A33,CAT_3:def 4
.= (cods(G'*p1))/.y by A38,CAT_3:def 4
.= G/.y by A18,A21,A27,CAT_3:20
.= G.y by A38,CAT_3:def 1
.= F.y by A38,FUNCT_1:72
.= F/.y by A33,CAT_3:def 1;
end;
hence (cods F')/.y = F/.y;
end;
hence
A39: cods F' = F by CAT_3:1;
thus F' is Projections_family of c,I;
let d be Object of C;
let F'' be Projections_family of d,I such that
A40: cods F' = cods F'';
reconsider G'' = F''|(I\{x}) as Function of I\{x},the Morphisms of C
by A17,FUNCT_2:38;
now let y be set;
assume
A41: y in I\{x};
then A42: y in I by XBOOLE_0:def 4;
G''/.y = G''.y by A41,CAT_3:def 1
.= F''.y by A41,FUNCT_1:72
.= F''/.y by A42,CAT_3:def 1;
hence doms(G'')/.y = dom(F''/.y) by A41,CAT_3:def 3
.= d by A42,CAT_3:45
.= ((I\{x})-->d)/.y by A41,CAT_3:2;
end;
then doms G'' = I\{x} --> d by CAT_3:1;
then reconsider G'' as Projections_family of d,I\{x} by CAT_3:def 14;
now let y be set;
assume
A43: y in I\{x};
then A44: y in I by XBOOLE_0:def 4;
then A45: F''/.y = F''.y by CAT_3:def 1
.= G''.y by A43,FUNCT_1:72
.= G''/.y by A43,CAT_3:def 1;
G/.y = G.y by A43,CAT_3:def 1
.= F.y by A43,FUNCT_1:72
.= F/.y by A44,CAT_3:def 1;
hence (cods G')/.y = cod(G''/.y) by A18,A39,A40,A44,A45,CAT_3:def 4
.= (cods G'')/.y by A43,CAT_3:def 4;
end;
then cods G' = cods G'' by CAT_3:1;
then consider h' being Morphism of C such that
A46: h' in Hom(d,a) and
A47: for k being Morphism of C st k in Hom(d,a) holds
(for y being set st y in I\{x} holds (G'/.y)*k = G''/.y) iff h' = k
by A19,CAT_3:def 15;
set g = F''/.x;
A48: dom g = d by A14,CARD_1:47,CAT_3:45;
A49: x in {x} by TARSKI:def 1;
A50: F'/.x = F'.x by A14,CARD_1:47,CAT_3:def 1
.= ({x} -->p2).x by A23,A49,FUNCT_4:14
.= p2 by A49,FUNCOP_1:13;
then cod p2 = (cods F')/.x by A14,CARD_1:47,CAT_3:def 4
.= cod g by A14,A40,CARD_1:47,CAT_3:def 4;
then g in Hom(d,cod p2) by A48,CAT_1:18;
then consider h being Morphism of C such that
A51: h in Hom(d,c) and
A52: for k being Morphism of C st k in Hom(d,c)
holds p1*k = h' & p2*k = g iff h = k by A21,A22,A46,CAT_3:def 16;
take h;
thus h in Hom(d,c) by A51;
let k be Morphism of C such that
A53: k in Hom(d,c);
thus (for y being set st y in I holds (F'/.y)*k = F''/.y) implies h = k
proof assume
A54: for y being set st y in I holds (F'/.y)*k = F''/.y;
then A55: p2*k = g by A14,A50,CARD_1:47;
A56: dom k = d & cod k = c by A53,CAT_1:18;
then dom(p1*k) = d & cod(p1*k) = a by A20,A21,CAT_1:42;
then A57: p1*k in Hom(d,a) by CAT_1:18;
for y being set st y in I\{x} holds (G'/.y)*(p1*k) = G''/.y
proof let y be set;
assume
A58: y in I\{x};
then A59: y in I & not y in {x} by XBOOLE_0:def 4;
then A60: F'/.y = F'.y by CAT_3:def 1
.= (G'*p1).y by A23,A24,A59,FUNCT_4:def 1
.= (G'*p1)/.y by A58,CAT_3:def 1;
dom(G'/.y) = a by A58,CAT_3:45;
hence (G'/.y)*(p1*k) = ((G'/.y)*p1)*k by A20,A21,A56,CAT_1:43
.= ((G'*p1)/.y)*k by A58,CAT_3:def 7
.= F''/.y by A54,A59,A60
.= F''.y by A59,CAT_3:def 1
.= G''.y by A58,FUNCT_1:72
.= G''/.y by A58,CAT_3:def 1;
end;
then p1*k = h' by A47,A57;
hence h = k by A52,A53,A55;
end;
assume
A61: h = k;
let y be set such that
A62: y in I;
now per cases;
suppose
A63: y = x;
then A64: y in {x} by TARSKI:def 1;
F'/.y = F'.y by A62,CAT_3:def 1
.= ({x} -->p2).y by A23,A64,FUNCT_4:14
.= p2 by A64,FUNCOP_1:13;
hence thesis by A52,A53,A61,A63;
suppose
A65: y <> x;
then A66: not y in {x} by TARSKI:def 1;
A67: y in I\{x} by A62,A65,ZFMISC_1:64;
then A68: cod k = c & dom(G'/.y) = a by A53,CAT_1:18,CAT_3:45;
F'/.y = F'.y by A62,CAT_3:def 1
.= (G'*p1).y by A23,A24,A62,A66,FUNCT_4:def 1
.= (G'*p1)/.y by A67,CAT_3:def 1
.= (G'/.y)*p1 by A67,CAT_3:def 7;
hence (F'/.y)*k = (G'/.y)*(p1*k) by A20,A21,A68,CAT_1:43
.= (G'/.y)*h' by A52,A53,A61
.= G''/.y by A46,A47,A67
.= G''.y by A67,CAT_3:def 1
.= F''.y by A67,FUNCT_1:72
.= F''/.y by A62,CAT_3:def 1;
end;
hence thesis;
end;
A69: for n being Nat holds Q[n] from Ind(A9,A12);
let I be finite set, F be Function of I,the Objects of C;
card I = card I;
hence thesis by A69;
end;
definition
struct (CatStr)ProdCatStr
(# Objects,Morphisms -> non empty set,
Dom,Cod -> Function of the Morphisms, the Objects,
Comp -> PartFunc of [:the Morphisms, the Morphisms :],the Morphisms,
Id -> Function of the Objects, the Morphisms,
TerminalObj -> Element of the Objects,
CatProd -> Function of [:the Objects,the Objects:],the Objects,
Proj1,Proj2 -> Function of [:the Objects,the Objects:],the Morphisms
#);
end;
definition let C be ProdCatStr;
func [1]C -> Object of C equals
:Def4: the TerminalObj of C;
correctness;
let a,b be Object of C;
func a[x]b -> Object of C equals
:Def5: (the CatProd of C).[a,b];
correctness;
func pr1(a,b) -> Morphism of C equals
:Def6: (the Proj1 of C).[a,b];
correctness;
func pr2(a,b) -> Morphism of C equals
:Def7: (the Proj2 of C).[a,b];
correctness;
end;
definition let o,m;
func c1Cat(o,m) -> strict ProdCatStr equals
:Def8: ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #);
correctness;
end;
theorem
the CatStr of c1Cat(o,m) = 1Cat(o,m)
proof
c1Cat(o,m) = ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def8;
hence thesis by CAT_1:def 9;
end;
Lm1: c1Cat(o,m) is Category-like
proof
set C = c1Cat(o,m);
A1: C = ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def8;
set CP = the Comp of C, CD = the Dom of C, CC = the Cod of C,
CI = the Id of C;
thus for f,g being Morphism of C holds
[g,f] in dom CP iff CD.g=CC.f
proof let f,g be Morphism of C;
f = m & g = m & dom CP = {[m,m]} by A1,CAT_1:7,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
thus for f,g being Morphism of C
st CD.g=CC.f holds CD.(CP.[g,f]) = CD.f & CC.(CP.[g,f]) = CC.g
proof let f,g be Morphism of C;
CP.[g,f] = m by A1,CAT_1:9;
then reconsider gf = CP.[g,f] as Morphism of C by A1,TARSKI:def 1;
CD.f = o & CC.g = o & CD.gf = o & CC.gf = o by A1,FUNCT_2:65;
hence thesis;
end;
thus for f,g,h being Morphism of C
st CD.h = CC.g & CD.g = CC.f
holds CP.[h,CP.[g,f]] = CP.[CP.[h,g],f]
proof let f,g,h be Morphism of C;
CP.[g,f] = m & CP.[h,g] = m by A1,CAT_1:9;
then reconsider gf = CP.[g,f],hg = CP.[h,g] as Morphism of C
by A1,TARSKI:def 1; CP.[h,gf] = m & CP.[hg,f] = m by A1,CAT_1:9;
hence thesis;
end;
let b be Object of C;
b = o by A1,TARSKI:def 1;
hence CD.(CI.b) = b & CC.(CI.b) = b by A1,FUNCT_2:65;
thus for f being Morphism of C st CC.f = b holds CP.[CI.b,f] = f
proof let f be Morphism of C; f = m by A1,TARSKI:def 1;
hence thesis by A1,CAT_1:9;
end;
let g be Morphism of C;
assume CD.g = b;
g = m by A1,TARSKI:def 1;
hence CP.[g,CI.b] = g by A1,CAT_1:9;
end;
definition
cluster strict Category-like ProdCatStr;
existence
proof c1Cat(0,1) is Category-like by Lm1; hence thesis; end;
end;
definition let o,m be set;
cluster c1Cat(o,m) -> Category-like;
coherence by Lm1;
end;
theorem Th3:
for a being Object of c1Cat(o,m) holds a = o
proof let a be Object of c1Cat(o,m);
c1Cat(o,m) = ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def8;
hence thesis by TARSKI:def 1;
end;
theorem Th4:
for a,b being Object of c1Cat(o,m) holds a = b
proof let a,b be Object of c1Cat(o,m);
a = o & b = o by Th3; hence thesis;
end;
theorem Th5:
for f being Morphism of c1Cat(o,m) holds f = m
proof let f be Morphism of c1Cat(o,m);
c1Cat(o,m) = ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def8;
hence thesis by TARSKI:def 1;
end;
theorem Th6:
for f,g being Morphism of c1Cat(o,m) holds f = g
proof let f,g be Morphism of c1Cat(o,m);
f = m & g = m by Th5; hence thesis;
end;
theorem Th7:
for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m)
holds f in Hom(a,b)
proof let a,b be Object of c1Cat(o,m), f be Morphism of c1Cat(o,m);
dom f = o & cod f = o by Th3; then dom f = a & cod f = b by Th3;
hence f in Hom(a,b) by CAT_1:18;
end;
theorem
for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m)
holds f is Morphism of a,b
proof let a,b be Object of c1Cat(o,m), f be Morphism of c1Cat(o,m);
f in Hom(a,b) by Th7; hence thesis by CAT_1:def 7;
end;
theorem
for a,b being Object of c1Cat(o,m) holds Hom(a,b) <> {} by Th7;
theorem Th10:
for a being Object of c1Cat(o,m) holds a is terminal
proof let a be Object of c1Cat(o,m);
let b be Object of c1Cat(o,m);
thus Hom(b,a)<>{} by Th7;
consider f being Morphism of b,a;
take f; thus thesis by Th6;
end;
theorem Th11:
for c being Object of c1Cat(o,m), p1,p2 being Morphism of c1Cat(o,m)
holds c is_a_product_wrt p1,p2
proof let c be Object of c1Cat(o,m), p1,p2 be Morphism of c1Cat(o,m);
thus dom p1 = c & dom p2 = c by Th4;
let d be Object of c1Cat(o,m),f,g be Morphism of c1Cat(o,m) such that
f in Hom(d,cod p1) & g in Hom(d,cod p2);
take h = p1;
thus h in Hom(d,c) by Th7;
thus thesis by Th6;
end;
definition let IT be Category-like ProdCatStr;
attr IT is Cartesian means
:Def9:
the TerminalObj of IT is terminal &
for a,b being Object of IT holds
cod((the Proj1 of IT).[a,b]) = a & cod((the Proj2 of IT).[a,b]) = b &
(the CatProd of IT).[a,b]
is_a_product_wrt (the Proj1 of IT).[a,b],(the Proj2 of IT).[a,b];
end;
theorem Th12:
for o,m being set holds c1Cat(o,m) is Cartesian
proof let o,m be set;
set 1PCat = c1Cat(o,m);
thus the TerminalObj of 1PCat is terminal by Th10;
let a,b be Object of 1PCat;
thus cod((the Proj1 of 1PCat).[a,b]) = a by Th4;
thus cod((the Proj2 of 1PCat).[a,b]) = b by Th4;
thus (the CatProd of 1PCat).[a,b]
is_a_product_wrt (the Proj1 of 1PCat).[a,b],(the Proj2 of 1PCat).[a,b]
by Th11;
end;
definition
cluster strict Cartesian (Category-like ProdCatStr);
existence
proof c1Cat(0,1) is Cartesian by Th12;
hence thesis;
end;
end;
definition
mode Cartesian_category is Cartesian (Category-like ProdCatStr);
end;
reserve C for Cartesian_category;
reserve a,b,c,d,e,s for Object of C;
theorem Th13:
[1]C is terminal
proof [1]C = the TerminalObj of C by Def4; hence thesis by Def9; end;
theorem Th14: for f1,f2 being Morphism of a,[1]C holds f1 = f2
proof let f1,f2 be Morphism of a,[1]C;
[1]C is terminal by Th13;
then consider f being Morphism of a,[1]C such that
A1: for g being Morphism of a,[1]C holds f = g by CAT_1:def 15;
thus f1 = f by A1 .= f2 by A1;
end;
theorem Th15:
Hom(a,[1]C) <> {}
proof [1]C is terminal by Th13; hence thesis by CAT_1:def 15; end;
definition let C,a;
func term(a) -> Morphism of a,[1]C means not contradiction;
existence;
uniqueness by Th14;
end;
theorem Th16:
term a = term(a,[1]C)
proof [1]C is terminal by Th13; hence thesis by CAT_3:41; end;
theorem
dom(term a) = a & cod(term a) = [1]C
proof [1]C is terminal & term a = term(a,[1]C) by Th13,Th16;
hence thesis by CAT_3:39;
end;
theorem
Hom(a,[1]C) = {term a}
proof
A1: Hom(a,[1]C) <> {} by Th15;
for f2 being Morphism of a,[1]C holds term a = f2 by Th14;
hence thesis by A1,CAT_1:26;
end;
theorem Th19:
dom pr1(a,b) = a[x]b & cod pr1(a,b) = a
proof
set p1 = (the Proj1 of C).[a,b], p2 = (the Proj2 of C).[a,b];
(the CatProd of C).[a,b] is_a_product_wrt p1,p2 by Def9;
then a[x]b is_a_product_wrt p1,p2 by Def5;
then dom p1 = a[x]b & cod p1 = a by Def9,CAT_3:def 16;
hence thesis by Def6;
end;
theorem Th20:
dom pr2(a,b) = a[x]b & cod pr2(a,b) = b
proof
set p1 = (the Proj1 of C).[a,b], p2 = (the Proj2 of C).[a,b];
(the CatProd of C).[a,b] is_a_product_wrt p1,p2 by Def9;
then a[x]b is_a_product_wrt p1,p2 by Def5;
then dom p2 = a[x]b & cod p2 = b by Def9,CAT_3:def 16;
hence thesis by Def7;
end;
definition let C,a,b;
redefine func pr1(a,b) -> Morphism of a[x]b,a;
coherence
proof dom pr1(a,b) = a[x]b & cod pr1(a,b) = a by Th19;
hence thesis by CAT_1:22;
end;
func pr2(a,b) -> Morphism of a[x]b,b;
coherence
proof dom pr2(a,b) = a[x]b & cod pr2(a,b) = b by Th20;
hence thesis by CAT_1:22;
end;
end;
theorem Th21:
Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {}
proof
set c = (the CatProd of C).[a,b],
p1 = (the Proj1 of C).[a,b], p2 = (the Proj2 of C).[a,b];
c is_a_product_wrt p1,p2 by Def9;
then dom p1 = c & dom p2 = c & cod(p1) = a & cod(p2) = b by Def9,CAT_3:def 16
;
then Hom(c,a) <> {} & Hom(c,b) <> {} by CAT_1:18;
hence thesis by Def5;
end;
theorem Th22:
a[x]b is_a_product_wrt pr1(a,b),pr2(a,b)
proof
(the CatProd of C).[a,b] = a[x]b & (the Proj1 of C).[a,b] = pr1(a,b) &
(the Proj2 of C).[a,b] = pr2(a,b) by Def5,Def6,Def7;
hence thesis by Def9;
end;
theorem
C has_finite_product
proof
A1: [1]C is terminal by Th13;
for a,b
ex c being Object of C, p1,p2 being Morphism of C
st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b &
c is_a_product_wrt p1,p2
proof let a,b;
take a[x]b, pr1(a,b), pr2(a,b);
thus thesis by Th19,Th20,Th22;
end;
hence thesis by A1,Th1;
end;
theorem
Hom(a,b) <> {} & Hom(b,a) <> {}
implies pr1(a,b) is retraction & pr2(a,b) is retraction
proof
a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) &
cod pr1(a,b) = a & cod pr2(a,b) = b by Th19,Th20,Th22;
hence thesis by CAT_3:62;
end;
definition let C,a,b,c;
let f be Morphism of c,a, g be Morphism of c,b;
assume A1: Hom(c,a) <> {} & Hom(c,b) <> {};
func <:f,g:> -> Morphism of c,a[x]b means
:Def11: pr1(a,b)*it = f & pr2(a,b)*it = g;
existence
proof Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} &
a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Th21,Th22;
then consider h being Morphism of c,a[x]b such that
A2: for h1 being Morphism of c,a[x]b
holds pr1(a,b)*h1 = f & pr2(a,b)*h1 = g iff h = h1 by A1,CAT_3:60;
take h; thus thesis by A2;
end;
uniqueness
proof let h1,h2 be Morphism of c,a[x]b such that
A3: pr1(a,b)*h1 = f & pr2(a,b)*h1 = g and
A4: pr1(a,b)*h2 = f & pr2(a,b)*h2 = g;
Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} &
a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Th21,Th22;
then consider h being Morphism of c,a[x]b such that
A5: for h1 being Morphism of c,a[x]b
holds pr1(a,b)*h1 = f & pr2(a,b)*h1 = g iff h = h1 by A1,CAT_3:60;
h1 = h & h2 = h by A3,A4,A5;
hence thesis;
end;
end;
theorem Th25:
Hom(c,a) <> {} & Hom(c,b) <> {} implies Hom(c,a[x]b) <> {}
proof Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} &
a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Th21,Th22;
hence thesis by CAT_3:60;
end;
theorem Th26:
<:pr1(a,b),pr2(a,b):> = id(a[x]b)
proof
A1: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21;
then pr1(a,b)*(id(a[x]b)) = pr1(a,b) & pr2(a,b)*(id(a[x]b)) = pr2(a,b)
by CAT_1:58;
hence thesis by A1,Def11;
end;
theorem Th27:
for f being Morphism of c,a, g being Morphism of c,b, h being Morphism of d,c
st Hom(c,a)<>{} & Hom(c,b)<>{} & Hom(d,c)<>{}
holds <:f*h,g*h:> = <:f,g:>*h
proof let f be Morphism of c,a, g be Morphism of c,b, h be Morphism of d,c;
assume that
A1: Hom(c,a)<>{} and
A2: Hom(c,b)<>{} and
A3: Hom(d,c)<>{};
Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} & Hom(c,a[x]b) <> {} &
(pr1(a,b)*<:f,g:>)*h = f*h & (pr2(a,b)*<:f,g:>)*h = g*h
by A1,A2,Def11,Th21,Th25;
then pr1(a,b)*(<:f,g:>*h) = f*h & pr2(a,b)*(<:f,g:>*h) = g*h &
Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A3,CAT_1:52,54;
hence thesis by Def11;
end;
theorem Th28:
for f,k being Morphism of c,a, g,h being Morphism of c,b
st Hom(c,a) <> {} & Hom(c,b) <> {} & <:f,g:> = <:k,h:>
holds f = k & g = h
proof let f,k be Morphism of c,a, g,h be Morphism of c,b;
assume Hom(c,a) <> {} & Hom(c,b) <> {};
then pr1(a,b)*<:f,g:> = f & pr1(a,b)*<:k,h:> = k &
pr2(a,b)*<:f,g:> = g & pr2(a,b)*<:k,h:> = h by Def11;
hence thesis;
end;
theorem
for f being Morphism of c,a, g being Morphism of c,b
st Hom(c,a) <> {} & Hom(c,b) <> {} & (f is monic or g is monic)
holds <:f,g:> is monic
proof let f be Morphism of c,a, g be Morphism of c,b;
assume that
A1: Hom(c,a) <> {} and
A2: Hom(c,b) <> {} and
A3: f is monic or g is monic;
A4: now assume
A5: f is monic;
let d;
let f1,f2 be Morphism of d,c such that
A6: Hom(d,c)<>{} and
A7: <:f,g:>*f1 = <:f,g:>*f2;
<:f*f1,g*f1:> = <:f,g:>*f1 & <:f*f2,g*f2:> = <:f,g:>*f2 &
Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A6,Th27,CAT_1:52;
then f*f1 = f*f2 by A7,Th28;
hence f1 = f2 by A1,A5,A6,CAT_1:60;
end;
A8: Hom(c,a[x]b) <> {} by A1,A2,Th25;
now assume
A9: g is monic;
let d be Object of C, f1,f2 be Morphism of d,c such that
A10: Hom(d,c)<>{} and
A11: <:f,g:>*f1 = <:f,g:>*f2;
<:f*f1,g*f1:> = <:f,g:>*f1 & <:f*f2,g*f2:> = <:f,g:>*f2 &
Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A10,Th27,CAT_1:52;
then g*f1 = g*f2 by A11,Th28;
hence f1 = f2 by A2,A9,A10,CAT_1:60;
end;
hence thesis by A3,A4,A8,CAT_1:60;
end;
theorem Th30:
Hom(a,a[x][1]C) <> {} & Hom(a,[1]C[x]a) <> {}
proof
Hom(a,[1]C) <> {} & Hom(a,a) <> {} by Th15,CAT_1:56;
hence thesis by Th25;
end;
definition let C,a;
func lambda(a) -> Morphism of [1]C[x]a,a equals
:Def12: pr2([1]C,a);
correctness;
func lambda'(a) -> Morphism of a,[1]C[x]a equals
:Def13: <:term a,id a:>;
correctness;
func rho(a) -> Morphism of a[x][1]C,a equals
:Def14: pr1(a,[1]C);
correctness;
func rho'(a) -> Morphism of a,a[x][1]C equals
:Def15: <:id a,term a:>;
correctness;
end;
theorem Th31:
lambda(a)*lambda'(a) = id a & lambda'(a)*lambda(a) = id([1]C[x]a) &
rho(a)*rho'(a) = id a & rho'(a)*rho(a) = id(a[x][1]C)
proof
A1: Hom(a,[1]C) <> {} & Hom(a,a) <> {} by Th15,CAT_1:56;
A2: Hom([1]C[x]a,a) <> {} by Th21;
then (id a)*pr2([1]C,a) = pr2([1]C,a) & (term a)*pr2([1]C,a) = pr1([1]C,a)
& Hom([1]C[x]a,[1]C)<>{} by Th14,Th21,CAT_1:57;
then A3:<:term a,id a:>*pr2([1]C,a) = <:pr1([1]C,a),pr2([1]C,a):> by A1,A2,
Th27;
pr2([1]C,a)*<:term a,id a:> = id a by A1,Def11;
hence id a = lambda(a)*<:term a,id a:> by Def12
.= lambda(a)*lambda'(a) by Def13;
<:term a,id a:>*pr2([1]C,a) = id([1]C[x]a) by A3,Th26;
hence id([1]C[x]a) = <:term a,id a:>*lambda(a) by Def12
.= lambda'(a)*lambda(a) by Def13;
A4: Hom(a[x][1]C,a) <> {} by Th21;
then (id a)*pr1(a,[1]C) = pr1(a,[1]C) & (term a)*pr1(a,[1]C) = pr2(a,[1]C)
& Hom(a[x][1]C,[1]C)<>{} by Th14,Th21,CAT_1:57;
then A5: <:id a,term a:>*pr1(a,[1]C) = <:pr1(a,[1]C),pr2(a,[1]C):> by A1,A4,
Th27;
pr1(a,[1]C)*<:id a,term a:> = id a by A1,Def11;
hence id a = rho(a)*<:id a,term a:> by Def14
.= rho(a)*rho'(a) by Def15;
<:id a,term a:>*pr1(a,[1]C) = id(a[x][1]C) by A5,Th26;
hence id(a[x][1]C) = <:id a,term a:>*rho(a) by Def14
.= rho'(a)*rho(a) by Def15;
end;
theorem
a, a[x][1]C are_isomorphic & a,[1]C[x]a are_isomorphic
proof
thus a,a[x][1]C are_isomorphic
proof thus Hom(a,a[x][1]C) <> {} & Hom(a[x][1]C,a) <> {} by Th21,Th30;
take rho'(a), rho(a);
thus thesis by Th31;
end;
thus Hom(a,[1]C[x]a) <> {} & Hom([1]C[x]a,a) <> {} by Th21,Th30;
take lambda'(a), lambda(a);
thus thesis by Th31;
end;
definition let C,a,b;
func Switch(a,b) -> Morphism of a[x]b,b[x]a equals
:Def16: <:pr2(a,b),pr1(a,b):>;
correctness;
end;
theorem Th33:
Hom(a[x]b,b[x]a)<>{}
proof
Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21;
hence thesis by Th25;
end;
theorem Th34:
Switch(a,b)*Switch(b,a) = id(b[x]a)
proof
A1: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21;
A2: Hom(b[x]a,b) <> {} & Hom(b[x]a,a) <> {} by Th21;
then A3: Hom(b[x]a,a[x]b)<>{} by Th25;
thus Switch(a,b)*Switch(b,a)
= <:pr2(a,b),pr1(a,b):>*Switch(b,a) by Def16
.= <:pr2(a,b),pr1(a,b):>*<:pr2(b,a),pr1(b,a):> by Def16
.= <:pr2(a,b)*<:pr2(b,a),pr1(b,a):>,pr1(a,b)*<:pr2(b,a),pr1(b,a):>:>
by A1,A3,Th27
.= <:pr1(b,a),pr1(a,b)*<:pr2(b,a),pr1(b,a):>:> by A2,Def11
.= <:pr1(b,a),pr2(b,a):> by A2,Def11
.= id(b[x]a) by Th26;
end;
theorem
a[x]b,b[x]a are_isomorphic
proof
thus Hom(a[x]b,b[x]a)<>{} & Hom(b[x]a,a[x]b)<>{} by Th33;
take Switch(a,b), Switch(b,a);
thus thesis by Th34;
end;
definition let C,a;
func Delta a -> Morphism of a,a[x]a equals
:Def17: <:id a,id a:>;
correctness;
end;
theorem
Hom(a,a[x]a) <> {}
proof Hom(a,a) <> {} by CAT_1:56; hence thesis by Th25; end;
theorem
for f being Morphism of a,b st Hom(a,b) <> {}
holds <:f,f:> = Delta(b)*f
proof let f be Morphism of a,b such that
A1: Hom(a,b) <> {};
A2: Hom(b,b) <> {} by CAT_1:56;
(id b)*f = f by A1,CAT_1:57;
hence <:f,f:> = <:id b, id b:>*f by A1,A2,Th27
.= Delta(b)*f by Def17;
end;
definition let C,a,b,c;
func Alpha(a,b,c) -> Morphism of (a[x]b)[x]c,a[x](b[x]c) equals
:Def18: <:pr1(a,b)*pr1(a[x]b,c),<:pr2(a,b)*pr1(a[x]b,c),pr2(a[x]b,c):>:>;
correctness;
func Alpha'(a,b,c) -> Morphism of a[x](b[x]c),(a[x]b)[x]c equals
:Def19: <:<:pr1(a,b[x]c),pr1(b,c)*pr2(a,b[x]c):>,pr2(b,c)*pr2(a,b[x]c):>;
correctness;
end;
theorem Th38:
Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} & Hom(a[x](b[x]c),(a[x]b)[x]c) <> {}
proof
A1: Hom(a[x]b,a) <> {} by Th21;
A2: Hom((a[x]b)[x]c,a[x]b) <> {} by Th21;
then A3: Hom((a[x]b)[x]c,a) <> {} by A1,CAT_1:52;
Hom(a[x]b,b) <> {} by Th21;
then A4: Hom((a[x]b)[x]c,b) <> {} by A2,CAT_1:52;
Hom((a[x]b)[x]c,c) <> {} by Th21;
then Hom((a[x]b)[x]c,b[x]c) <> {} by A4,Th25;
hence Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} by A3,Th25;
A5: Hom(b[x]c,b) <> {} by Th21;
A6: Hom(a[x](b[x]c),b[x]c) <> {} by Th21;
then A7: Hom(a[x](b[x]c),b) <> {} by A5,CAT_1:52;
Hom(b[x]c,c) <> {} by Th21;
then A8: Hom(a[x](b[x]c),c) <> {} by A6,CAT_1:52;
Hom(a[x](b[x]c),a) <> {} by Th21;
then Hom(a[x](b[x]c),a[x]b) <> {} by A7,Th25;
hence Hom(a[x](b[x]c),(a[x]b)[x]c) <> {} by A8,Th25;
end;
theorem Th39:
Alpha(a,b,c)*Alpha'(a,b,c) = id(a[x](b[x]c)) &
Alpha'(a,b,c)*Alpha(a,b,c) = id((a[x]b)[x]c)
proof
A1: Hom(a[x]b,a) <> {} by Th21;
A2: Hom((a[x]b)[x]c,a[x]b) <> {} by Th21;
then A3: Hom((a[x]b)[x]c,a) <> {} by A1,CAT_1:52;
A4: Hom(a[x]b,b) <> {} by Th21;
then A5: Hom((a[x]b)[x]c,b) <> {} by A2,CAT_1:52;
A6: Hom((a[x]b)[x]c,c) <> {} by Th21;
then A7: Hom((a[x]b)[x]c,b[x]c) <> {} by A5,Th25;
A8: Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} by Th38;
A9: Hom(b[x]c,b) <> {} by Th21;
A10: Hom(a[x](b[x]c),b[x]c) <> {} by Th21;
then A11: Hom(a[x](b[x]c),b) <> {} by A9,CAT_1:52;
A12: Hom(b[x]c,c) <> {} by Th21;
then A13: Hom(a[x](b[x]c),c) <> {} by A10,CAT_1:52;
A14: Hom(a[x](b[x]c),a) <> {} by Th21;
then A15: Hom(a[x](b[x]c),a[x]b) <> {} by A11,Th25;
A16: Hom(a[x](b[x]c),(a[x]b)[x]c) <> {} by Th38;
set k = <:pr2(a,b)*pr1(a[x]b,c),pr2(a[x]b,c):>;
set l = <:pr1(a,b[x]c),pr1(b,c)*pr2(a,b[x]c):>;
set f = <:pr1(a,b)*pr1(a[x]b,c),k:>;
set g = <:l,pr2(b,c)*pr2(a,b[x]c):>;
A17: pr1(a,b)*pr1(a[x]b,c)*g
= pr1(a,b)*(pr1(a[x]b,c)*g) by A1,A2,A16,CAT_1:54
.= pr1(a,b)*l by A13,A15,Def11
.= pr1(a,b[x]c) by A11,A14,Def11;
pr2(a,b)*pr1(a[x]b,c)*g = pr2(a,b)*(pr1(a[x]b,c)*g) by A2,A4,A16,CAT_1:54
.= pr2(a,b)*l by A13,A15,Def11
.= pr1(b,c)*pr2(a,b[x]c) by A11,A14,Def11;
then A18: k*g = <:pr1(b,c)*pr2(a,b[x]c),pr2(a[x]b,c)*g:> by A5,A6,A16,Th27
.= <:pr1(b,c)*pr2(a,b[x]c),pr2(b,c)*pr2(a,b[x]c):> by A13,A15,Def11
.= <:pr1(b,c),pr2(b,c):>*pr2(a,b[x]c) by A9,A10,A12,Th27
.= id(b[x]c)*pr2(a,b[x]c) by Th26
.= pr2(a,b[x]c) by A10,CAT_1:57;
thus Alpha(a,b,c)*Alpha'(a,b,c)
= Alpha(a,b,c)*g by Def19
.= f*g by Def18
.= <:pr1(a,b[x]c),pr2(a,b[x]c):> by A3,A7,A16,A17,A18,Th27
.= id(a[x](b[x]c)) by Th26;
pr1(b,c)*pr2(a,b[x]c)*f = pr1(b,c)*(pr2(a,b[x]c)*f) by A8,A9,A10,CAT_1:54
.= pr1(b,c)*k by A3,A7,Def11
.= pr2(a,b)*pr1(a[x]b,c) by A5,A6,Def11;
then A19: l*f = <:pr1(a,b[x]c)*f,pr2(a,b)*pr1(a[x]b,c):> by A8,A11,A14,Th27
.= <:pr1(a,b)*pr1(a[x]b,c),pr2(a,b)*pr1(a[x]b,c):> by A3,A7,Def11
.= <:pr1(a,b),pr2(a,b):>*pr1(a[x]b,c) by A1,A2,A4,Th27
.= id(a[x]b)*pr1(a[x]b,c) by Th26
.= pr1(a[x]b,c) by A2,CAT_1:57;
A20: pr2(b,c)*pr2(a,b[x]c)*f
= pr2(b,c)*(pr2(a,b[x]c)*f) by A8,A10,A12,CAT_1:54
.= pr2(b,c)*k by A3,A7,Def11
.= pr2(a[x]b,c) by A5,A6,Def11;
thus Alpha'(a,b,c)*Alpha(a,b,c)
= Alpha'(a,b,c)*f by Def18
.= g*f by Def19
.= <:pr1(a[x]b,c),pr2(a[x]b,c):> by A8,A13,A15,A19,A20,Th27
.= id((a[x]b)[x]c) by Th26;
end;
theorem
(a[x]b)[x]c,a[x](b[x]c) are_isomorphic
proof
thus Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} & Hom(a[x](b[x]c),(a[x]b)[x]c) <> {}
by Th38;
take Alpha(a,b,c), Alpha'(a,b,c);
thus thesis by Th39;
end;
definition let C,a,b,c,d;
let f be Morphism of a,b, g be Morphism of c,d;
func f[x]g -> Morphism of a[x]c,b[x]d equals
:Def20: <:f*pr1(a,c),g*pr2(a,c):>;
correctness;
end;
theorem
Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a[x]b,c[x]d) <> {}
proof assume
A1: Hom(a,c) <> {} & Hom(b,d) <> {};
Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21;
then Hom(a[x]b,c) <> {} & Hom(a[x]b,d) <> {} by A1,CAT_1:52;
hence thesis by Th25;
end;
theorem
(id a)[x](id b) = id(a[x]b)
proof Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21;
then (id a)*pr1(a,b) = pr1(a,b) & (id b)*pr2(a,b) = pr2(a,b) by CAT_1:57;
then (id a)[x](id b) = <:pr1(a,b),pr2(a,b):> by Def20;
hence thesis by Th26;
end;
theorem Th43:
for f being Morphism of a,b, h being Morphism of c,d,
g being Morphism of e,a, k being Morphism of e,c
st Hom(a,b) <> {} & Hom(c,d) <> {} & Hom(e,a) <> {} & Hom(e,c) <> {}
holds (f[x]h)*<:g,k:> = <:f*g,h*k:>
proof let f be Morphism of a,b, h be Morphism of c,d;
let g be Morphism of e,a, k be Morphism of e,c;
assume that
A1: Hom(a,b) <> {} and
A2: Hom(c,d) <> {} and
A3: Hom(e,a) <> {} and
A4: Hom(e,c) <> {};
A5: Hom(e,a[x]c) <> {} by A3,A4,Th25;
Hom(a[x]c,a) <> {} & Hom(a[x]c,c) <> {} &
pr1(a,c)*<:g,k:> = g & pr2(a,c)*<:g,k:> = k by A3,A4,Def11,Th21;
then Hom(a[x]c,b) <> {} & Hom(a[x]c,d) <> {} &
f*g = (f*pr1(a,c))*<:g,k:> & h*k = (h*pr2(a,c))*<:g,k:>
by A1,A2,A5,CAT_1:52,54;
then <:f*g,h*k:> = <:f*pr1(a,c),h*pr2(a,c):>*<:g,k:> by A5,Th27;
hence thesis by Def20;
end;
theorem
for f being Morphism of c,a, g being Morphism of c,b
st Hom(c,a) <> {} & Hom(c,b) <> {} holds <:f,g:> = (f[x]g)*Delta(c)
proof let f be Morphism of c,a, g be Morphism of c,b such that
A1: Hom(c,a) <> {} and
A2: Hom(c,b) <> {};
A3: Hom(c,c) <> {} by CAT_1:56;
thus (f[x]g)*Delta(c) = (f[x]g)*<:id c,id c:> by Def17
.= <:f*(id c),g*(id c):> by A1,A2,A3,Th43
.= <:f,g*(id c):> by A1,CAT_1:58
.= <:f,g:> by A2,CAT_1:58;
end;
theorem
for f being Morphism of a,b, h being Morphism of c,d,
g being Morphism of e,a, k being Morphism of s,c
st Hom(a,b) <> {} & Hom(c,d) <> {} & Hom(e,a) <> {} & Hom(s,c) <> {}
holds (f[x]h)*(g[x]k) = (f*g)[x](h*k)
proof let f be Morphism of a,b, h be Morphism of c,d;
let g be Morphism of e,a, k be Morphism of s,c;
assume that
A1: Hom(a,b) <> {} and
A2: Hom(c,d) <> {} and
A3: Hom(e,a) <> {} and
A4: Hom(s,c) <> {};
A5: Hom(e[x]s,e) <> {} & Hom(e[x]s,s) <> {} by Th21;
then f*(g*pr1(e,s)) = (f*g)*pr1(e,s) & h*(k*pr2(e,s)) = (h*k)*pr2(e,s)
by A1,A2,A3,A4,CAT_1:54;
then Hom(e[x]s,a) <> {} & Hom(e[x]s,c) <> {} &
(f*g)[x](h*k) = <:f*(g*pr1(e,s)),h*(k*pr2(e,s)):> &
g[x]k = <:g*pr1(e,s),k*pr2(e,s):>
by A3,A4,A5,Def20,CAT_1:52;
hence thesis by A1,A2,Th43;
end;
begin :: Categories with Finite Coproducts
definition let C be Category;
attr C is with_finite_coproduct means
for I being finite set, F being Function of I,the Objects of C
ex a being Object of C, F' being Injections_family of a,I
st doms F' = F & a is_a_coproduct_wrt F';
synonym C has_finite_coproduct;
end;
theorem Th46:
for C being Category holds
C has_finite_coproduct iff
(ex a being Object of C st a is initial) &
for a,b being Object of C
ex c being Object of C, i1,i2 being Morphism of C
st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c &
c is_a_coproduct_wrt i1,i2
proof let C be Category;
thus C has_finite_coproduct implies
(ex a being Object of C st a is initial) &
for a,b being Object of C
ex c being Object of C, i1,i2 being Morphism of C
st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c &
c is_a_coproduct_wrt i1,i2
proof assume
A1: for I being finite set, F being Function of I,the Objects of C
ex a being Object of C, F' being Injections_family of a,I
st doms F' = F & a is_a_coproduct_wrt F';
reconsider F = {} as Function of {},the Objects of C by FUNCT_2:55,RELAT_1:
60;
consider a being Object of C, F' being Injections_family of a,{}
such that doms F' = F and
A2: a is_a_coproduct_wrt F' by A1;
a is initial by A2,CAT_3:81;
hence ex a being Object of C st a is initial;
let a,b be Object of C;
set F = (0,1)-->(a,b);
consider c being Object of C, F' being Injections_family of c,{0,1}
such that
A3: doms F' = F and
A4: c is_a_coproduct_wrt F' by A1;
take c, i1 = F'/.0, i2 = F'/.1;
A5: 0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
F/.0 = a & F/.1 = b by CAT_3:7;
hence dom i1 = a & dom i2 = b by A3,A5,CAT_3:def 3;
thus cod i1 = c & cod i2 = c by A5,CAT_3:67;
A6: dom F' = {0,1} by FUNCT_2:def 1;
i1 = F'.0 & i2 = F'.1 by A5,CAT_3:def 1;
then 0 <> 1 & F' = (0,1)-->(i1,i2) by A6,FUNCT_4:69;
hence c is_a_coproduct_wrt i1,i2 by A4,CAT_3:85;
end;
given a being Object of C such that
A7: a is initial;
assume
A8: for a,b being Object of C
ex c being Object of C, i1,i2 being Morphism of C
st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c &
c is_a_coproduct_wrt i1,i2;
defpred Q[Nat] means
for I being finite set, F being Function of I,the Objects of C
st card I = $1
ex a being Object of C, F' being Injections_family of a,I
st doms F' = F & a is_a_coproduct_wrt F';
A9: Q[ 0 ]
proof let I be finite set, F be Function of I,the Objects of C;
assume A10: card I = 0;
then A11: I = {} by CARD_2:59;
{} is Function of {}, the Morphisms of C by FUNCT_2:55,RELAT_1:60;
then reconsider F' = {} as Injections_family of a,I by A11,CAT_3:68;
take a,F';
for x being set st x in I holds (doms F')/.x = F/.x by A10,CARD_2:59;
hence doms F' = F by CAT_3:1;
thus thesis by A7,A11,CAT_3:81;
end;
A12: for n being Nat st Q[n] holds Q[n+1]
proof let n be Nat such that
A13: Q[n];
let I be finite set, F be Function of I,the Objects of C such that
A14: card I = n+1;
consider x being Element of I;
reconsider Ix = I \ {x} as finite set;
A15: {x} c= I by A14,CARD_1:47,ZFMISC_1:37;
reconsider sx = {x} as finite set;
A16: card(Ix) = card(I) - card(sx) by A15,CARD_2:63
.= card(I) - 1 by CARD_1:79
.= n by A14,XCMPLX_1:26;
A17: I\{x} c= I & the Objects of C <> {} by XBOOLE_1:36;
then reconsider G = F|(I\{x}) as Function of I\{x},the Objects of C
by FUNCT_2:38;
consider a being Object of C, G' being Injections_family of a,I\{x}
such that
A18: doms G' = G and
A19: a is_a_coproduct_wrt G' by A13,A16;
set b = F/.x;
consider c being Object of C, i1,i2 being Morphism of C
such that
A20: dom i1 = a & dom i2 = b and
A21: cod i1 = c & cod i2 = c and
A22: c is_a_coproduct_wrt i1,i2 by A8;
set F' = (i1*G') +* ({x} -->i2);
A23: dom(i1*G') = I\{x} & dom({x} -->i2) = {x} by FUNCT_2:def 1;
then A24: dom(i1*G') \/ dom({x} -->i2) = I \/ {x} by XBOOLE_1:39
.= I by A14,CARD_1:47,ZFMISC_1:46;
then A25: dom F' = I by FUNCT_4:def 1;
A26: rng F' c= rng(i1*G') \/ rng({x} -->i2) by FUNCT_4:18;
rng(i1*G') c= the Morphisms of C & rng({x} -->i2) c= the Morphisms of C
by RELSET_1:12;
then rng(i1*G') \/ rng({x} -->i2) c= the Morphisms of C by XBOOLE_1:8;
then rng F' c= the Morphisms of C by A26,XBOOLE_1:1;
then reconsider F' as Function of I, the Morphisms of C
by A25,FUNCT_2:def 1,RELSET_1:11;
A27: cods G' = (I\{x})-->a by CAT_3:def 17;
now let y be set;
assume
A28: y in I;
now per cases;
suppose y = x;
then A29: y in {x} by TARSKI:def 1;
F'/.y = F'.y by A28,CAT_3:def 1
.= ({x} -->i2).y by A23,A29,FUNCT_4:14
.= i2 by A29,FUNCOP_1:13;
hence (I --> c).y = cod(F'/.y) by A21,A28,FUNCOP_1:13
.= (cods F')/.y by A28,CAT_3:def 4;
suppose
A30: y <> x;
then A31: not y in {x} by TARSKI:def 1;
A32: y in I\{x} by A28,A30,ZFMISC_1:64;
F'/.y = F'.y by A28,CAT_3:def 1
.= (i1*G').y by A23,A24,A28,A31,FUNCT_4:def 1
.= (i1*G')/.y by A32,CAT_3:def 1;
hence (cods F')/.y = cod((i1*G')/.y) by A28,CAT_3:def 4
.= (cods(i1*G'))/.y by A32,CAT_3:def 4
.= ((I\{x})-->c)/.y by A20,A21,A27,CAT_3:21
.= c by A32,CAT_3:2
.= (I --> c).y by A28,FUNCOP_1:13;
end;
hence (cods F').y = (I --> c).y by A28,CAT_3:def 1;
end;
then cods F' = I --> c by FUNCT_2:18;
then reconsider F' as Injections_family of c,I by CAT_3:def 17;
take c,F';
now let y be set;
assume
A33: y in I;
now per cases;
suppose
A34: y = x;
then A35: y in {x} by TARSKI:def 1;
F'/.y = F'.y by A33,CAT_3:def 1
.= ({x} -->i2).y by A23,A35,FUNCT_4:14
.= i2 by A35,FUNCOP_1:13;
hence (doms F')/.y = F/.y by A20,A33,A34,CAT_3:def 3;
suppose
A36: y <> x;
then A37: not y in {x} by TARSKI:def 1;
A38: y in I\{x} by A33,A36,ZFMISC_1:64;
F'/.y = F'.y by A33,CAT_3:def 1
.= (i1*G').y by A23,A24,A33,A37,FUNCT_4:def 1
.= (i1*G')/.y by A38,CAT_3:def 1;
hence (doms F')/.y = dom((i1*G')/.y) by A33,CAT_3:def 3
.= (doms(i1*G'))/.y by A38,CAT_3:def 3
.= G/.y by A18,A20,A27,CAT_3:21
.= G.y by A38,CAT_3:def 1
.= F.y by A38,FUNCT_1:72
.= F/.y by A33,CAT_3:def 1;
end;
hence (doms F')/.y = F/.y;
end;
hence
A39: doms F' = F by CAT_3:1;
thus F' is Injections_family of c,I;
let d be Object of C;
let F'' be Injections_family of d,I such that
A40: doms F' = doms F'';
reconsider G'' = F''|(I\{x}) as Function of I\{x},the Morphisms of C
by A17,FUNCT_2:38;
now let y be set;
assume
A41: y in I\{x};
then A42: y in I by XBOOLE_0:def 4;
G''/.y = G''.y by A41,CAT_3:def 1
.= F''.y by A41,FUNCT_1:72
.= F''/.y by A42,CAT_3:def 1;
hence cods(G'')/.y = cod(F''/.y) by A41,CAT_3:def 4
.= d by A42,CAT_3:67
.= ((I\{x})-->d)/.y by A41,CAT_3:2;
end;
then cods G'' = I\{x} --> d by CAT_3:1;
then reconsider G'' as Injections_family of d,I\{x} by CAT_3:def 17;
now let y be set;
assume
A43: y in I\{x};
then A44: y in I by XBOOLE_0:def 4;
then A45: F''/.y = F''.y by CAT_3:def 1
.= G''.y by A43,FUNCT_1:72
.= G''/.y by A43,CAT_3:def 1;
G/.y = G.y by A43,CAT_3:def 1
.= F.y by A43,FUNCT_1:72
.= F/.y by A44,CAT_3:def 1;
hence (doms G')/.y = dom(G''/.y) by A18,A39,A40,A44,A45,CAT_3:def 3
.= (doms G'')/.y by A43,CAT_3:def 3;
end;
then doms G' = doms G'' by CAT_3:1;
then consider h' being Morphism of C such that
A46: h' in Hom(a,d) and
A47: for k being Morphism of C st k in Hom(a,d) holds
(for y being set st y in I\{x} holds k*(G'/.y) = G''/.y) iff h' = k
by A19,CAT_3:def 18;
set g = F''/.x;
A48: cod g = d by A14,CARD_1:47,CAT_3:67;
A49: x in {x} by TARSKI:def 1;
A50: F'/.x = F'.x by A14,CARD_1:47,CAT_3:def 1
.= ({x} -->i2).x by A23,A49,FUNCT_4:14
.= i2 by A49,FUNCOP_1:13;
then dom i2 = (doms F')/.x by A14,CARD_1:47,CAT_3:def 3
.= dom g by A14,A40,CARD_1:47,CAT_3:def 3;
then g in Hom(dom i2,d) by A48,CAT_1:18;
then consider h being Morphism of C such that
A51: h in Hom(c,d) and
A52: for k being Morphism of C st k in Hom(c,d)
holds k*i1 = h' & k*i2 = g iff h = k by A20,A22,A46,CAT_3:def 19;
take h;
thus h in Hom(c,d) by A51;
let k be Morphism of C such that
A53: k in Hom(c,d);
thus (for y being set st y in I holds k*(F'/.y) = F''/.y) implies h = k
proof assume
A54: for y being set st y in I holds k*(F'/.y) = F''/.y;
then A55: k*i2 = g by A14,A50,CARD_1:47;
A56: cod k = d & dom k = c by A53,CAT_1:18;
then cod(k*i1) = d & dom(k*i1) = a by A20,A21,CAT_1:42;
then A57: k*i1 in Hom(a,d) by CAT_1:18;
for y being set st y in I\{x} holds k*i1*(G'/.y) = G''/.y
proof let y be set;
assume
A58: y in I\{x};
then A59: y in I & not y in {x} by XBOOLE_0:def 4;
then A60: F'/.y = F'.y by CAT_3:def 1
.= (i1*G').y by A23,A24,A59,FUNCT_4:def 1
.= (i1*G')/.y by A58,CAT_3:def 1;
cod(G'/.y) = a by A58,CAT_3:67;
hence k*i1*(G'/.y) = k*(i1*(G'/.y)) by A20,A21,A56,CAT_1:43
.= k*((i1*G')/.y) by A58,CAT_3:def 8
.= F''/.y by A54,A59,A60
.= F''.y by A59,CAT_3:def 1
.= G''.y by A58,FUNCT_1:72
.= G''/.y by A58,CAT_3:def 1;
end;
then k*i1 = h' by A47,A57;
hence h = k by A52,A53,A55;
end;
assume
A61: h = k;
let y be set such that
A62: y in I;
now per cases;
suppose
A63: y = x;
then A64: y in {x} by TARSKI:def 1;
F'/.y = F'.y by A62,CAT_3:def 1
.= ({x} -->i2).y by A23,A64,FUNCT_4:14
.= i2 by A64,FUNCOP_1:13;
hence thesis by A52,A53,A61,A63;
suppose
A65: y <> x;
then A66: not y in {x} by TARSKI:def 1;
A67: y in I\{x} by A62,A65,ZFMISC_1:64;
then A68: dom k = c & cod(G'/.y) = a by A53,CAT_1:18,CAT_3:67;
F'/.y = F'.y by A62,CAT_3:def 1
.= (i1*G').y by A23,A24,A62,A66,FUNCT_4:def 1
.= (i1*G')/.y by A67,CAT_3:def 1
.= i1*(G'/.y) by A67,CAT_3:def 8;
hence k*(F'/.y) = k*i1*(G'/.y) by A20,A21,A68,CAT_1:43
.= h'*(G'/.y) by A52,A53,A61
.= G''/.y by A46,A47,A67
.= G''.y by A67,CAT_3:def 1
.= F''.y by A67,FUNCT_1:72
.= F''/.y by A62,CAT_3:def 1;
end;
hence thesis;
end;
A69: for n being Nat holds Q[n] from Ind(A9,A12);
let I be finite set, F be Function of I,the Objects of C;
card I = card I;
hence thesis by A69;
end;
definition
struct (CatStr)CoprodCatStr
(# Objects,Morphisms -> non empty set,
Dom,Cod -> Function of the Morphisms, the Objects,
Comp -> PartFunc of [:the Morphisms, the Morphisms :],the Morphisms,
Id -> Function of the Objects, the Morphisms,
Initial -> Element of the Objects,
Coproduct -> Function of [:the Objects,the Objects:],the Objects,
Incl1,Incl2 -> Function of [:the Objects,the Objects:],the Morphisms
#);
end;
definition let C be CoprodCatStr;
func [0]C -> Object of C equals
:Def22: the Initial of C;
correctness;
let a,b be Object of C;
func a+b -> Object of C equals
:Def23: (the Coproduct of C).[a,b];
correctness;
func in1(a,b) -> Morphism of C equals
:Def24: (the Incl1 of C).[a,b];
correctness;
func in2(a,b) -> Morphism of C equals
:Def25: (the Incl2 of C).[a,b];
correctness;
end;
definition let o,m;
func c1Cat*(o,m) -> strict CoprodCatStr equals
:Def26: CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #);
correctness;
end;
theorem
the CatStr of c1Cat*(o,m) = 1Cat(o,m)
proof
c1Cat*(o,m) = CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def26;
hence thesis by CAT_1:def 9;
end;
Lm2: c1Cat*(o,m) is Category-like
proof
set C = c1Cat*(o,m);
A1: C = CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def26;
set CP = the Comp of C, CD = the Dom of C, CC = the Cod of C,
CI = the Id of C;
thus for f,g being Morphism of C holds
[g,f] in dom CP iff CD.g=CC.f
proof let f,g be Morphism of C;
f = m & g = m & dom CP = {[m,m]} by A1,CAT_1:7,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
thus for f,g being Morphism of C
st CD.g=CC.f holds CD.(CP.[g,f]) = CD.f & CC.(CP.[g,f]) = CC.g
proof let f,g be Morphism of C;
CP.[g,f] = m by A1,CAT_1:9;
then reconsider gf = CP.[g,f] as Morphism of C by A1,TARSKI:def 1;
CD.f = o & CC.g = o & CD.gf = o & CC.gf = o by A1,FUNCT_2:65;
hence thesis;
end;
thus for f,g,h being Morphism of C
st CD.h = CC.g & CD.g = CC.f
holds CP.[h,CP.[g,f]] = CP.[CP.[h,g],f]
proof let f,g,h be Morphism of C;
CP.[g,f] = m & CP.[h,g] = m by A1,CAT_1:9;
then reconsider gf = CP.[g,f],hg = CP.[h,g] as Morphism of C
by A1,TARSKI:def 1; CP.[h,gf] = m & CP.[hg,f] = m by A1,CAT_1:9;
hence thesis;
end;
let b be Object of C;
b = o by A1,TARSKI:def 1;
hence CD.(CI.b) = b & CC.(CI.b) = b by A1,FUNCT_2:65;
thus for f being Morphism of C st CC.f = b holds CP.[CI.b,f] = f
proof let f be Morphism of C; f = m by A1,TARSKI:def 1;
hence thesis by A1,CAT_1:9;
end;
let g be Morphism of C;
assume CD.g = b;
g = m by A1,TARSKI:def 1; hence CP.[g,CI.b] = g by A1,CAT_1:9;
end;
definition
cluster strict Category-like CoprodCatStr;
existence
proof c1Cat*(0,1) is Category-like by Lm2; hence thesis; end;
end;
definition let o,m be set;
cluster c1Cat*(o,m) -> Category-like;
coherence by Lm2;
end;
theorem Th48:
for a being Object of c1Cat*(o,m) holds a = o
proof let a be Object of c1Cat*(o,m);
c1Cat*(o,m) = CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def26;
hence thesis by TARSKI:def 1;
end;
theorem Th49:
for a,b being Object of c1Cat*(o,m) holds a = b
proof let a,b be Object of c1Cat*(o,m);
a = o & b = o by Th48; hence thesis;
end;
theorem Th50:
for f being Morphism of c1Cat*(o,m) holds f = m
proof let f be Morphism of c1Cat*(o,m);
c1Cat*(o,m) = CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def26;
hence thesis by TARSKI:def 1;
end;
theorem Th51:
for f,g being Morphism of c1Cat*(o,m) holds f = g
proof let f,g be Morphism of c1Cat*(o,m);
f = m & g = m by Th50; hence thesis;
end;
theorem Th52:
for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(o,m)
holds f in Hom(a,b)
proof let a,b be Object of c1Cat*(o,m), f be Morphism of c1Cat*(o,m);
dom f = o & cod f = o by Th48; then dom f = a & cod f = b by Th48;
hence f in Hom(a,b) by CAT_1:18;
end;
theorem
for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(o,m)
holds f is Morphism of a,b
proof let a,b be Object of c1Cat*(o,m), f be Morphism of c1Cat*(o,m);
f in Hom(a,b) by Th52; hence thesis by CAT_1:def 7;
end;
theorem
for a,b being Object of c1Cat*(o,m) holds Hom(a,b) <> {} by Th52;
theorem Th55:
for a being Object of c1Cat*(o,m) holds a is initial
proof let a be Object of c1Cat*(o,m);
let b be Object of c1Cat*(o,m);
thus Hom(a,b)<>{} by Th52;
consider f being Morphism of a,b;
take f; thus thesis by Th51;
end;
theorem Th56:
for c being Object of c1Cat*(o,m),
i1,i2 being Morphism of c1Cat*(o,m) holds c is_a_coproduct_wrt i1,i2
proof
let c be Object of c1Cat*(o,m), i1,i2 be Morphism of c1Cat*(o,m);
thus cod i1 = c & cod i2 = c by Th49;
let d be Object of c1Cat*(o,m), f,g be Morphism of c1Cat*(o,m) such that
f in Hom(dom i1,d) & g in Hom(dom i2,d);
take h = i1;
thus h in Hom(c,d) by Th52;
thus thesis by Th51;
end;
definition let IT be Category-like CoprodCatStr;
attr IT is Cocartesian means
:Def27:
the Initial of IT is initial &
for a,b being Object of IT holds
dom((the Incl1 of IT).[a,b]) = a & dom((the Incl2 of IT).[a,b]) = b &
(the Coproduct of IT).[a,b]
is_a_coproduct_wrt (the Incl1 of IT).[a,b],(the Incl2 of IT).[a,b];
end;
theorem Th57:
for o,m being set holds c1Cat*(o,m) is Cocartesian
proof let o,m be set;
set 1PCat = c1Cat*(o,m);
thus the Initial of 1PCat is initial by Th55;
let a,b be Object of 1PCat;
thus dom((the Incl1 of 1PCat).[a,b]) = a by Th49;
thus dom((the Incl2 of 1PCat).[a,b]) = b by Th49;
thus (the Coproduct of 1PCat).[a,b]
is_a_coproduct_wrt (the Incl1 of 1PCat).[a,b],(the Incl2 of 1PCat).[a,b]
by Th56;
end;
definition
cluster strict Cocartesian (Category-like CoprodCatStr);
existence
proof c1Cat*(0,1) is Cocartesian by Th57;
hence thesis;
end;
end;
definition
mode Cocartesian_category is Cocartesian (Category-like CoprodCatStr);
end;
reserve C for Cocartesian_category;
reserve a,b,c,d,e,s for Object of C;
theorem Th58:
[0]C is initial
proof [0]C = the Initial of C by Def22; hence thesis by Def27; end;
theorem Th59:
for f1,f2 being Morphism of [0]C,a holds f1 = f2
proof let f1,f2 be Morphism of [0]C,a;
[0]C is initial by Th58;
then consider f being Morphism of [0]C,a such that
A1: for g being Morphism of [0]C, a holds f = g by CAT_1:def 16;
thus f1 = f by A1 .= f2 by A1;
end;
definition let C,a;
func init a -> Morphism of [0]C, a means not contradiction;
existence;
uniqueness by Th59;
end;
theorem Th60:
Hom([0]C,a) <> {}
proof [0]C is initial by Th58; hence thesis by CAT_1:def 16; end;
theorem Th61:
init a = init([0]C,a)
proof [0]C is initial by Th58; hence thesis by CAT_3:44; end;
theorem
dom(init a) = [0]C & cod(init a) = a
proof [0]C is initial & init a = init([0]C,a) by Th58,Th61;
hence thesis by CAT_3:42;
end;
theorem
Hom([0]C,a) = {init a}
proof
A1: Hom([0]C,a) <> {} by Th60;
for f2 being Morphism of [0]C,a holds init a = f2 by Th59;
hence thesis by A1,CAT_1:26;
end;
theorem Th64:
dom in1(a,b) = a & cod in1(a,b) = a+b
proof
set i1 = (the Incl1 of C).[a,b], i2 = (the Incl2 of C).[a,b];
(the Coproduct of C).[a,b] is_a_coproduct_wrt i1,i2 by Def27;
then a+b is_a_coproduct_wrt i1,i2 by Def23;
then cod i1 = a+b & dom i1 = a by Def27,CAT_3:def 19;
hence thesis by Def24;
end;
theorem Th65:
dom in2(a,b) = b & cod in2(a,b) = a+b
proof
set i1 = (the Incl1 of C).[a,b], i2 = (the Incl2 of C).[a,b];
(the Coproduct of C).[a,b] is_a_coproduct_wrt i1,i2 by Def27;
then a+b is_a_coproduct_wrt i1,i2 by Def23;
then cod i2 = a+b & dom i2 = b by Def27,CAT_3:def 19;
hence thesis by Def25;
end;
theorem Th66:
Hom(a,a+b) <> {} & Hom(b,a+b) <> {}
proof
set c = (the Coproduct of C).[a,b];
set i1 = (the Incl1 of C).[a,b], i2 = (the Incl2 of C).[a,b];
c is_a_coproduct_wrt i1,i2 by Def27;
then cod i1 = c & cod i2 = c & dom(i1) = a & dom(i2) = b
by Def27,CAT_3:def 19;
then Hom(a,c) <> {} & Hom(b,c) <> {} by CAT_1:18;
hence thesis by Def23;
end;
theorem Th67:
a+b is_a_coproduct_wrt in1(a,b),in2(a,b)
proof
set i1 = (the Incl1 of C).[a,b], i2 = (the Incl2 of C).[a,b];
(the Coproduct of C).[a,b] = a+b & i1 = in1(a,b) & i2 = in2(a,b)
by Def23,Def24,Def25;
hence thesis by Def27;
end;
theorem
C has_finite_coproduct
proof
A1: [0]C is initial by Th58;
for a,b
ex c being Object of C, i1,i2 being Morphism of C
st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c &
c is_a_coproduct_wrt i1,i2
proof let a,b;
take a+b, in1(a,b), in2(a,b);
thus thesis by Th64,Th65,Th67;
end;
hence thesis by A1,Th46;
end;
theorem
Hom(a,b) <> {} & Hom(b,a) <> {}
implies in1(a,b) is coretraction & in2(a,b) is coretraction
proof
a+b is_a_coproduct_wrt in1(a,b),in2(a,b) &
dom in1(a,b) = a & dom in2(a,b) = b by Th64,Th65,Th67;
hence thesis by CAT_3:88;
end;
definition let C,a,b; redefine
func in1(a,b) -> Morphism of a,a+b;
coherence
proof cod in1(a,b) = a+b & dom in1(a,b) = a by Th64;
hence thesis by CAT_1:22;
end;
func in2(a,b) -> Morphism of b,a+b;
coherence
proof cod in2(a,b) = a+b & dom in2(a,b) = b by Th65;
hence thesis by CAT_1:22;
end;
end;
definition let C,a,b,c;
let f be Morphism of a,c, g be Morphism of b,c;
assume A1: Hom(a,c) <> {} & Hom(b,c) <> {};
func [$f,g$] -> Morphism of a+b,c means
:Def29: it*in1(a,b) = f & it*in2(a,b) = g;
existence
proof Hom(a,a+b) <> {} & Hom(b,a+b) <> {} &
a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Th66,Th67;
then consider h being Morphism of a+b,c such that
A2: for k being Morphism of a+b,c
holds k*in1(a,b) = f & k*in2(a,b) = g iff h = k by A1,CAT_3:87;
take h; thus thesis by A2;
end;
uniqueness
proof let h1,h2 be Morphism of a+b,c such that
A3: h1*in1(a,b) = f & h1*in2(a,b) = g and
A4: h2*in1(a,b) = f & h2*in2(a,b) = g;
a+b is_a_coproduct_wrt in1(a,b),in2(a,b) &
Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th66,Th67;
then consider h being Morphism of a+b,c such that
A5: for k being Morphism of a+b,c
holds k*in1(a,b) = f & k*in2(a,b) = g iff h = k by A1,CAT_3:87;
h1 = h & h2 = h by A3,A4,A5;
hence thesis;
end;
end;
theorem Th70:
Hom(a,c) <> {} & Hom(b,c) <> {} implies Hom(a+b,c) <> {}
proof Hom(a,a+b) <> {} & Hom(b,a+b) <> {} &
a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Th66,Th67;
hence thesis by CAT_3:87;
end;
theorem Th71:
[$in1(a,b),in2(a,b)$] = id(a+b)
proof
A1: Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th66;
then (id(a+b))*in1(a,b) = in1(a,b) & (id(a+b))*in2(a,b) = in2(a,b)
by CAT_1:57;
hence thesis by A1,Def29;
end;
theorem Th72:
for f being Morphism of a,c, g being Morphism of b,c, h being Morphism of c,d
st Hom(a,c)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{}
holds [$h*f,h*g$] = h*[$f,g$]
proof let f be Morphism of a,c, g be Morphism of b,c, h be Morphism of c,d;
assume that
A1: Hom(a,c)<>{} and
A2: Hom(b,c)<>{} and
A3: Hom(c,d)<>{};
Hom(a,a+b) <> {} & Hom(b,a+b) <> {} & Hom(a+b,c) <> {} &
h*([$f,g$]*in1(a,b)) = h*f & h*([$f,g$]*in2(a,b)) = h*g
by A1,A2,Def29,Th66,Th70;
then h*[$f,g$]*in1(a,b) = h*f & h*[$f,g$]*in2(a,b) = h*g &
Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A3,CAT_1:52,54;
hence thesis by Def29;
end;
theorem Th73:
for f,k being Morphism of a,c, g,h being Morphism of b,c
st Hom(a,c) <> {} & Hom(b,c) <> {} & [$f,g$] = [$k,h$]
holds f = k & g = h
proof let f,k be Morphism of a,c, g,h be Morphism of b,c;
assume Hom(a,c) <> {} & Hom(b,c) <> {};
then [$f,g$]*in1(a,b) = f & [$k,h$]*in1(a,b) = k &
[$f,g$]*in2(a,b) = g & [$k,h$]*in2(a,b) = h by Def29;
hence thesis;
end;
theorem
for f being Morphism of a,c, g being Morphism of b,c
st Hom(a,c) <> {} & Hom(b,c) <> {} & (f is epi or g is epi)
holds [$f,g$] is epi
proof
let f be Morphism of a,c, g be Morphism of b,c;
assume that
A1: Hom(a,c) <> {} and
A2: Hom(b,c) <> {} and
A3: f is epi or g is epi;
A4: now assume
A5: f is epi;
let d;
let f1,f2 be Morphism of c,d such that
A6: Hom(c,d)<>{} and
A7: f1*[$f,g$] = f2*[$f,g$];
[$f1*f,f1*g$] = f1*[$f,g$] & [$f2*f,f2*g$] = f2*[$f,g$] &
Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A6,Th72,CAT_1:52;
then f1*f = f2*f by A7,Th73;
hence f1 = f2 by A1,A5,A6,CAT_1:65;
end;
A8: Hom(a+b,c) <> {} by A1,A2,Th70;
now assume
A9: g is epi;
let d be Object of C, f1,f2 be Morphism of c,d such that
A10: Hom(c,d)<>{} and
A11: f1*[$f,g$] = f2*[$f,g$];
[$f1*f,f1*g$] = f1*[$f,g$] & [$f2*f,f2*g$] = f2*[$f,g$] &
Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A10,Th72,CAT_1:52;
then f1*g = f2*g by A11,Th73;
hence f1 = f2 by A2,A9,A10,CAT_1:65;
end;
hence thesis by A3,A4,A8,CAT_1:65;
end;
theorem
a, a+[0]C are_isomorphic & a,[0]C+a are_isomorphic
proof
A1: Hom([0]C,a) <> {} & Hom(a,a) <> {} by Th60,CAT_1:56;
thus a,a+[0]C are_isomorphic
proof thus
A2: Hom(a,a+[0]C) <> {} by Th66;
thus Hom(a+[0]C,a) <> {} by A1,Th70;
take g = in1(a,[0]C), f = [$id a,init a$];
in1(a,[0]C)*id(a) = in1(a,[0]C) & in1(a,[0]C)*init a = in2(a,[0]C)
& Hom([0]C,a+[0]C)<>{} by A2,Th59,Th66,CAT_1:58;
then g*f = [$in1(a,[0]C),in2(a,[0]C)$] by A1,A2,Th72;
hence thesis by A1,Def29,Th71;
end;
thus
A3: Hom(a,[0]C+a) <> {} by Th66;
thus Hom([0]C+a,a) <> {} by A1,Th70;
take g = in2([0]C,a), f = [$init a,id a$];
in2([0]C,a)*id(a) = in2([0]C,a) & in2([0]C,a)*init a = in1([0]C,a)
& Hom([0]C,[0]C+a)<>{} by A3,Th59,Th66,CAT_1:58;
then g*f = [$in1([0]C,a),in2([0]C,a)$] by A1,A3,Th72;
hence thesis by A1,Def29,Th71;
end;
theorem
a+b,b+a are_isomorphic
proof
A1: Hom(a,b+a) <> {} & Hom(b,b+a) <> {} by Th66;
hence
A2: Hom(a+b,b+a)<>{} by Th70;
A3: Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th66;
hence
A4: Hom(b+a,a+b)<>{} by Th70;
take f' = [$in2(b,a),in1(b,a)$], f = [$in2(a,b),in1(a,b)$];
thus f'*f
= [$f'*in2(a,b),f'*in1(a,b)$] by A2,A3,Th72
.= [$in1(b,a),f'*in1(a,b)$] by A1,Def29
.= [$in1(b,a),in2(b,a)$] by A1,Def29
.= id(b+a) by Th71;
thus f*f'
= [$f*in2(b,a),f*in1(b,a)$] by A1,A4,Th72
.= [$in1(a,b),f*in1(b,a)$] by A3,Def29
.= [$in1(a,b),in2(a,b)$] by A3,Def29
.= id(a+b) by Th71;
end;
theorem
(a+b)+c,a+(b+c) are_isomorphic
proof
A1: Hom(b,b+c) <> {} by Th66;
A2: Hom(b+c,a+(b+c)) <> {} by Th66;
then A3: Hom(b,a+(b+c)) <> {} by A1,CAT_1:52;
A4: Hom(c,b+c) <> {} by Th66;
then A5: Hom(c,a+(b+c)) <> {} by A2,CAT_1:52;
A6: Hom(a,a+(b+c)) <> {} by Th66;
then A7: Hom(a+b,a+(b+c)) <> {} by A3,Th70;
hence
A8: Hom((a+b)+c,a+(b+c)) <> {} by A5,Th70;
A9: Hom(a,a+b) <> {} by Th66;
A10: Hom(a+b,(a+b)+c) <> {} by Th66;
then A11: Hom(a,(a+b)+c) <> {} by A9,CAT_1:52;
A12: Hom(b,a+b) <> {} by Th66;
then A13: Hom(b,(a+b)+c) <> {} by A10,CAT_1:52;
A14: Hom(c,(a+b)+c) <> {} by Th66;
then A15: Hom(b+c,(a+b)+c) <> {} by A13,Th70;
hence
A16: Hom(a+(b+c),(a+b)+c) <> {} by A11,Th70;
set k = [$in1(a+b,c)*in2(a,b),in2(a+b,c)$];
set l = [$in1(a,b+c),in2(a,b+c)*in1(b,c)$];
take g = [$l,in2(a,b+c)*in2(b,c)$];
take f = [$in1(a+b,c)*in1(a,b),k$];
now
thus g*(in1(a+b,c)*in1(a,b))
= g*in1(a+b,c)*in1(a,b) by A8,A9,A10,CAT_1:54
.= l*in1(a,b) by A5,A7,Def29
.= in1(a,b+c) by A3,A6,Def29;
g*(in1(a+b,c)*in2(a,b)) = (g*in1(a+b,c))*in2(a,b) by A8,A10,A12,CAT_1:54
.= l*in2(a,b) by A5,A7,Def29
.= in2(a,b+c)*in1(b,c) by A3,A6,Def29;
hence g*k
= [$in2(a,b+c)*in1(b,c),g*in2(a+b,c)$] by A8,A13,A14,Th72
.= [$in2(a,b+c)*in1(b,c),in2(a,b+c)*in2(b,c)$] by A5,A7,Def29
.= in2(a,b+c)*[$in1(b,c),in2(b,c)$] by A1,A2,A4,Th72
.= in2(a,b+c)*id(b+c) by Th71
.= in2(a,b+c) by A2,CAT_1:58;
end;
hence g*f = [$in1(a,b+c),in2(a,b+c)$] by A8,A11,A15,Th72
.= id(a+(b+c)) by Th71;
now
f*(in2(a,b+c)*in1(b,c)) = (f*in2(a,b+c))*in1(b,c) by A1,A2,A16,CAT_1:54
.= k*in1(b,c) by A11,A15,Def29
.= in1(a+b,c)*in2(a,b) by A13,A14,Def29;
hence f*l
= [$f*in1(a,b+c),in1(a+b,c)*in2(a,b)$] by A3,A6,A16,Th72
.= [$in1(a+b,c)*in1(a,b),in1(a+b,c)*in2(a,b)$] by A11,A15,Def29
.= in1(a+b,c)*[$in1(a,b),in2(a,b)$] by A9,A10,A12,Th72
.= in1(a+b,c)*id(a+b) by Th71
.= in1(a+b,c) by A10,CAT_1:58;
thus f*(in2(a,b+c)*in2(b,c))
= (f*in2(a,b+c))*in2(b,c) by A2,A4,A16,CAT_1:54
.= k*in2(b,c) by A11,A15,Def29
.= in2(a+b,c) by A13,A14,Def29;
end;
hence f*g = [$in1(a+b,c),in2(a+b,c)$] by A5,A7,A16,Th72
.= id((a+b)+c) by Th71;
end;
definition let C,a;
func nabla a -> Morphism of a+a,a equals
:Def30: [$id a,id a$];
correctness;
end;
definition let C,a,b,c,d;
let f be Morphism of a,c, g be Morphism of b,d;
func f+g -> Morphism of a+b,c+d equals
:Def31: [$in1(c,d)*f,in2(c,d)*g$];
correctness;
end;
theorem
Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a+b,c+d) <> {}
proof assume
A1: Hom(a,c) <> {} & Hom(b,d) <> {};
Hom(c,c+d) <> {} & Hom(d,c+d) <> {} by Th66;
then Hom(a,c+d) <> {} & Hom(b,c+d) <> {} by A1,CAT_1:52;
hence thesis by Th70;
end;
theorem
(id a)+(id b) = id(a+b)
proof Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th66;
then in1(a,b)*(id a) = in1(a,b) & in2(a,b)*(id b) = in2(a,b) by CAT_1:58;
then (id a)+(id b) = [$in1(a,b),in2(a,b)$] by Def31;
hence thesis by Th71;
end;
theorem Th80:
for f being Morphism of a,c, h being Morphism of b,d,
g being Morphism of c,e, k being Morphism of d,e
st Hom(a,c) <> {} & Hom(b,d) <> {} & Hom(c,e) <> {} & Hom(d,e) <> {}
holds [$g,k$]*(f+h) = [$g*f,k*h$]
proof let f be Morphism of a,c, h be Morphism of b,d;
let g be Morphism of c,e, k be Morphism of d,e;
assume that
A1: Hom(a,c) <> {} and
A2: Hom(b,d) <> {} and
A3: Hom(c,e) <> {} and
A4: Hom(d,e) <> {};
A5: Hom(c+d,e) <> {} by A3,A4,Th70;
Hom(c,c+d) <> {} & Hom(d,c+d) <> {} &
[$g,k$]*in1(c,d) = g & [$g,k$]*in2(c,d) = k by A3,A4,Def29,Th66;
then Hom(a,c+d) <> {} & Hom(b,c+d) <> {} &
g*f = [$g,k$]*(in1(c,d)*f) & k*h = [$g,k$]*(in2(c,d)*h)
by A1,A2,A5,CAT_1:52,54;
then [$g*f,k*h$] = [$g,k$]*[$in1(c,d)*f,in2(c,d)*h$] by A5,Th72;
hence thesis by Def31;
end;
theorem
for f being Morphism of a,c, g being Morphism of b,c
st Hom(a,c) <> {} & Hom(b,c) <> {} holds nabla(c)*(f+g) = [$f,g$]
proof let f be Morphism of a,c, g be Morphism of b,c such that
A1: Hom(a,c) <> {} and
A2: Hom(b,c) <> {};
A3: Hom(c,c) <> {} by CAT_1:56;
thus nabla(c)*(f+g) = [$id c,id c$]*(f+g) by Def30
.= [$(id c)*f,(id c)*g$] by A1,A2,A3,Th80
.= [$f,(id c)*g$] by A1,CAT_1:57
.= [$f,g$] by A2,CAT_1:57;
end;
theorem
for f being Morphism of a,c, h being Morphism of b,d,
g being Morphism of c,e, k being Morphism of d,s
st Hom(a,c) <> {} & Hom(b,d) <> {} & Hom(c,e) <> {} & Hom(d,s) <> {}
holds (g+k)*(f+h) = (g*f)+(k*h)
proof let f be Morphism of a,c, h be Morphism of b,d;
let g be Morphism of c,e, k be Morphism of d,s;
assume that
A1: Hom(a,c) <> {} and
A2: Hom(b,d) <> {} and
A3: Hom(c,e) <> {} and
A4: Hom(d,s) <> {};
A5: Hom(e,e+s) <> {} & Hom(s,e+s) <> {} by Th66;
then in1(e,s)*g*f = in1(e,s)*(g*f) & in2(e,s)*k*h = in2(e,s)*(k*h)
by A1,A2,A3,A4,CAT_1:54;
then Hom(c,e+s) <> {} & Hom(d,e+s) <> {} &
(g*f)+(k*h) = [$in1(e,s)*g*f,in2(e,s)*k*h$] &
g+k = [$in1(e,s)*g,in2(e,s)*k$] by A3,A4,A5,Def31,CAT_1:52;
hence thesis by A1,A2,Th80;
end;