:: Cartesian Categories
:: by Czes{\l}aw Byli\'nski
::
:: Received October 27, 1992
:: Copyright (c) 1992-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies CAT_1, WELLORD1, XBOOLE_0, RELAT_1, FINSET_1, FUNCT_1, STRUCT_0,
CAT_3, GRAPH_1, CARD_1, FUNCOP_1, PARTFUN1, NAT_1, ARYTM_3, SUBSET_1,
TARSKI, ARYTM_1, FUNCT_4, FUNCT_6, ZFMISC_1, ALGSTR_1, MCART_1, DIRAF,
PBOOLE, EQREL_1, CAT_4, MONOID_0, RELAT_2, BINOP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, ALGSTR_1, XCMPLX_0,
ORDINAL1, CARD_1, FUNCT_4, STRUCT_0, GRAPH_1, CAT_1, CAT_3;
constructors BINOP_1, REAL_1, NAT_1, ALGSTR_1, CAT_3, RELSET_1, XREAL_0,
FUNCT_4;
registrations XBOOLE_0, FUNCT_1, FINSET_1, XREAL_0, NAT_1, ORDINAL1, CARD_1,
STRUCT_0, PARTFUN1, FUNCT_2, RELSET_1, CAT_1;
requirements NUMERALS, SUBSET, BOOLE;
definitions CAT_1, CAT_3;
equalities CAT_1, FUNCOP_1, GRAPH_1;
expansions 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, XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes NAT_1;
begin
reserve o,m for set;
definition
let C be Category, a,b be Object of C;
redefine pred a,b are_isomorphic means :: redefines are_isomorphic (CAT_1, definition)
Hom(a,b)<>{} & Hom(b,a)<>{} & ex f
being Morphism of a,b, f9 being Morphism of b,a st f*f9 = id b & f9*f = id a;
compatibility by CAT_1:48;
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 carrier of C ex a being Object of C, F9 being Projections_family of a,
I st cods F9 = F & a is_a_product_wrt F9;
end;
theorem Th1:
for C being Category holds C is with_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 is with_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
reconsider F = {} as Function of {},the carrier of C by RELSET_1:12;
assume
A1: for I being finite set, F being Function of I,the carrier of C ex
a being Object of C, F9 being Projections_family of a,I st cods F9 = F & a
is_a_product_wrt F9;
then consider
a being Object of C, F9 being Projections_family of a,{} such
that
cods F9 = F and
A2: a is_a_product_wrt F9;
thus ex a being Object of C st a is terminal by A2,CAT_3:50;
let a,b be Object of C;
set F = (0,1)-->(a,b);
consider c being Object of C, F9 being Projections_family of c,{0,1} such
that
A3: cods F9 = F and
A4: c is_a_product_wrt F9 by A1;
take c, p1 = F9/.0, p2 = F9/.1;
A5: 1 in {0,1} by TARSKI:def 2;
then
A6: p2 = F9.1 by FUNCT_2:def 13;
A7: 0 in {0,1} by TARSKI:def 2;
hence dom p1 = c & dom p2 = c by A5,CAT_3:41;
F/.0 = a & F/.1 = b by CAT_3:3;
hence cod p1 = a & cod p2 = b by A3,A7,A5,CAT_3:def 2;
dom F9 = {0,1} & p1 = F9.0 by A7,FUNCT_2:def 1,def 13;
then F9 = (0,1)-->(p1,p2) by A6,FUNCT_4:66;
hence thesis by A4,CAT_3:54;
end;
given a being Object of C such that
A8: a is terminal;
defpred Q[Nat] means for I being finite set, F being Function of I,the
carrier of C st card I = $1 ex a being Object of C, F9 being Projections_family
of a,I st cods F9 = F & a is_a_product_wrt F9;
assume
A9: 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;
A10: for n being Nat st Q[n] holds Q[n+1]
proof
let n be Nat such that
A11: Q[n];
let I be finite set, F be Function of I,the carrier of C such that
A12: card I = n+1;
set x = the Element of I;
reconsider Ix = I \ {x} as finite set;
reconsider sx = {x} as finite set;
reconsider G = F|(I\{x}) as Function of I\{x},the carrier of C by
FUNCT_2:32;
card(Ix) = card(I) - card(sx) by A12,CARD_1:27,CARD_2:44,ZFMISC_1:31
.= card(I) - 1 by CARD_1:30
.= n by A12,XCMPLX_1:26;
then consider
a being Object of C, G9 being Projections_family of a,I\{x} such
that
A13: cods G9 = G and
A14: a is_a_product_wrt G9 by A11;
consider c being Object of C, p1,p2 being Morphism of C such that
A15: dom p1 = c and
A16: dom p2 = c and
A17: cod p1 = a and
A18: cod p2 = F/.x and
A19: c is_a_product_wrt p1,p2 by A9;
set F9 = (G9*p1) +* (x .-->p2);
A20: dom({x} -->p2) = {x} by FUNCT_2:def 1;
rng F9 c= rng(G9*p1) \/ rng(x .-->p2) by FUNCT_4:17;
then
A21: rng F9 c= the carrier' of C by XBOOLE_1:1;
dom(G9*p1) = I\{x} by FUNCT_2:def 1;
then
A22: dom(G9*p1) \/ dom(x .-->p2) = I \/ {x} by A20,XBOOLE_1:39
.= I by A12,CARD_1:27,ZFMISC_1:40;
then dom F9 = I by FUNCT_4:def 1;
then reconsider F9 as Function of I, the carrier' of C by A21,FUNCT_2:def 1
,RELSET_1:4;
A23: doms G9 = (I\{x})-->a by CAT_3:def 13;
now
let y be object;
assume
A24: y in I;
now
per cases;
suppose
y = x;
then
A25: y in {x} by TARSKI:def 1;
F9/.y = F9.y by A24,FUNCT_2:def 13
.= (x .-->p2).y by A20,A25,FUNCT_4:13
.= p2 by A25,FUNCOP_1:7;
hence (I --> c).y = dom(F9/.y) by A16,A24,FUNCOP_1:7
.= (doms F9)/.y by A24,CAT_3:def 1;
end;
suppose
A26: y <> x;
then
A27: not y in {x} by TARSKI:def 1;
A28: y in I\{x} by A24,A26,ZFMISC_1:56;
F9/.y = F9.y by A24,FUNCT_2:def 13
.= (G9*p1).y by A20,A22,A24,A27,FUNCT_4:def 1
.= (G9*p1)/.y by A28,FUNCT_2:def 13;
hence (doms F9)/.y = dom((G9*p1)/.y) by A24,CAT_3:def 1
.= (doms(G9*p1))/.y by A28,CAT_3:def 1
.= ((I\{x})-->c)/.y by A15,A17,A23,CAT_3:16
.= c by A24,A26,CAT_3:2,ZFMISC_1:56
.= (I --> c).y by A24,FUNCOP_1:7;
end;
end;
hence (doms F9).y = (I --> c).y by A24,FUNCT_2:def 13;
end;
then reconsider F9 as Projections_family of c,I
by CAT_3:def 13,FUNCT_2:12;
take c,F9;
A29: now
let y be set;
assume
A30: y in I;
now
per cases;
suppose
A31: y = x;
then
A32: y in {x} by TARSKI:def 1;
F9/.y = F9.y by A30,FUNCT_2:def 13
.= (x .-->p2).y by A20,A32,FUNCT_4:13
.= p2 by A32,FUNCOP_1:7;
hence (cods F9)/.y = F/.y by A18,A30,A31,CAT_3:def 2;
end;
suppose
A33: y <> x;
then
A34: not y in {x} by TARSKI:def 1;
A35: y in I\{x} by A30,A33,ZFMISC_1:56;
F9/.y = F9.y by A30,FUNCT_2:def 13
.= (G9*p1).y by A20,A22,A30,A34,FUNCT_4:def 1
.= (G9*p1)/.y by A35,FUNCT_2:def 13;
hence (cods F9)/.y = cod((G9*p1)/.y) by A30,CAT_3:def 2
.= (cods(G9*p1))/.y by A35,CAT_3:def 2
.= G/.y by A13,A17,A23,CAT_3:16
.= G.y by A35,FUNCT_2:def 13
.= F.y by A30,A33,FUNCT_1:49,ZFMISC_1:56
.= F/.y by A30,FUNCT_2:def 13;
end;
end;
hence (cods F9)/.y = F/.y;
end;
hence
cods F9 = F by CAT_3:1;
thus F9 is Projections_family of c,I;
let d be Object of C;
let F99 be Projections_family of d,I such that
A36: cods F9 = cods F99;
reconsider G99 = F99|(I\{x}) as Function of I\{x},the carrier' of C by
FUNCT_2:32;
now
let y be set;
assume
A37: y in I\{x};
then G99/.y = G99.y by FUNCT_2:def 13
.= F99.y by A37,FUNCT_1:49
.= F99/.y by A37,FUNCT_2:def 13;
hence doms(G99)/.y = dom(F99/.y) by A37,CAT_3:def 1
.= d by A37,CAT_3:41
.= ((I\{x})-->d)/.y by A37,CAT_3:2;
end;
then reconsider G99 as Projections_family of d,I\{x}
by CAT_3:1,def 13;
now
let y be set;
assume
A38: y in I\{x};
then
A39: G/.y = G.y by FUNCT_2:def 13
.= F.y by A38,FUNCT_1:49
.= F/.y by A38,FUNCT_2:def 13;
F99/.y = F99.y by A38,FUNCT_2:def 13
.= G99.y by A38,FUNCT_1:49
.= G99/.y by A38,FUNCT_2:def 13;
hence (cods G9)/.y = cod(G99/.y)
by A13,A36,A38,A39,A29,CAT_3:1,def 2
.= (cods G99)/.y by A38,CAT_3:def 2;
end;
then consider h9 being Morphism of C such that
A40: h9 in Hom(d,a) and
A41: for k being Morphism of C st k in Hom(d,a) holds (for y being set
st y in I\{x} holds (G9/.y)(*)k = G99/.y) iff h9 = k by A14,CAT_3:1;
A42: x in {x} by TARSKI:def 1;
set g = F99/.x;
A43: dom g = d by A12,CARD_1:27,CAT_3:41;
A44: F9/.x = F9.x by A12,CARD_1:27,FUNCT_2:def 13
.= (x .-->p2).x by A20,A42,FUNCT_4:13
.= p2 by A42,FUNCOP_1:7;
then cod p2 = (cods F9)/.x by A12,CARD_1:27,CAT_3:def 2
.= cod g by A12,A36,CARD_1:27,CAT_3:def 2;
then g in Hom(d,cod p2) by A43;
then consider h being Morphism of C such that
A45: h in Hom(d,c) and
A46: for k being Morphism of C st k in Hom(d,c) holds p1(*)k = h9 & p2(*)k
= g iff h = k by A17,A19,A40;
take h;
thus h in Hom(d,c) by A45;
let k be Morphism of C such that
A47: k in Hom(d,c);
thus (for y being set st y in I holds (F9/.y)(*)k = F99/.y) implies h = k
proof
A48: cod k = c by A47,CAT_1:1;
then
A49: cod(p1(*)k) = a by A15,A17,CAT_1:17;
assume
A50: for y being set st y in I holds (F9/.y)(*)k = F99/.y;
A51: for y being set st y in I\{x} holds (G9/.y)(*)(p1(*)k) = G99/.y
proof
let y be set;
assume
A52: y in I\{x};
then
A53: not y in {x} by XBOOLE_0:def 5;
A54: F9/.y = F9.y by A52,FUNCT_2:def 13
.= (G9*p1).y by A20,A22,A52,A53,FUNCT_4:def 1
.= (G9*p1)/.y by A52,FUNCT_2:def 13;
dom(G9/.y) = a by A52,CAT_3:41;
hence (G9/.y)(*)(p1(*)k) = ((G9/.y)(*)p1)(*)k by A15,A17,A48,CAT_1:18
.= ((G9*p1)/.y)(*)k by A52,CAT_3:def 5
.= F99/.y by A50,A52,A54
.= F99.y by A52,FUNCT_2:def 13
.= G99.y by A52,FUNCT_1:49
.= G99/.y by A52,FUNCT_2:def 13;
end;
dom k = d by A47,CAT_1:1;
then dom(p1(*)k) = d by A15,A48,CAT_1:17;
then p1(*)k in Hom(d,a) by A49;
then
A55: p1(*)k = h9 by A41,A51;
p2(*)k = g by A12,A44,A50,CARD_1:27;
hence thesis by A46,A47,A55;
end;
assume
A56: h = k;
let y be set such that
A57: y in I;
now
per cases;
suppose
A58: y = x;
then
A59: y in {x} by TARSKI:def 1;
F9/.y = F9.y by A57,FUNCT_2:def 13
.= (x .-->p2).y by A20,A59,FUNCT_4:13
.= p2 by A59,FUNCOP_1:7;
hence thesis by A46,A47,A56,A58;
end;
suppose
A60: y <> x;
then
A61: not y in {x} by TARSKI:def 1;
A62: cod k = c by A47,CAT_1:1;
A63: y in I\{x} by A57,A60,ZFMISC_1:56;
A64: dom(G9/.y) = a by A57,A60,CAT_3:41,ZFMISC_1:56;
F9/.y = F9.y by A57,FUNCT_2:def 13
.= (G9*p1).y by A20,A22,A57,A61,FUNCT_4:def 1
.= (G9*p1)/.y by A63,FUNCT_2:def 13
.= (G9/.y)(*)p1 by A63,CAT_3:def 5;
hence (F9/.y)(*)k = (G9/.y)(*)(p1(*)k) by A15,A17,A62,A64,CAT_1:18
.= (G9/.y)(*)h9 by A46,A47,A56
.= G99/.y by A40,A41,A63
.= G99.y by A63,FUNCT_2:def 13
.= F99.y by A57,A60,FUNCT_1:49,ZFMISC_1:56
.= F99/.y by A57,FUNCT_2:def 13;
end;
end;
hence thesis;
end;
let I be finite set, F be Function of I,the carrier of C;
A65: card I = card I;
A66: Q[ 0 ]
proof
let I be finite set, F be Function of I,the carrier of C;
assume card I = 0;
then
A67: I = {};
{} is Function of {}, the carrier' of C by RELSET_1:12;
then reconsider F9 = {} as Projections_family of a,I by A67,CAT_3:42;
take a,F9;
for x being set st x in I holds (cods F9)/.x = F/.x;
hence cods F9 = F by CAT_3:1;
thus thesis by A8,A67,CAT_3:50;
end;
for n being Nat holds Q[n] from NAT_1:sch 2(A66,A10);
hence thesis by A65;
end;
definition
struct (CatStr)ProdCatStr (# carrier,carrier' -> set, Source,Target ->
Function of the carrier', the carrier, Comp -> PartFunc of [:the carrier', the
carrier' :],the carrier',
TerminalObj -> Element of the carrier, CatProd -> Function of [:the carrier,the
carrier:],the carrier, Proj1,Proj2 -> Function of [:the carrier,the carrier:],
the carrier' #);
end;
registration
cluster non void non empty for ProdCatStr;
existence
proof
set o = the set;
take ProdCatStr(# {o},{o},o:->o,o:->o,(o,o):->o,Extract(o),(o,o):->
o,(o,o):->o,(o,o):->o #);
thus thesis;
end;
end;
definition
let C be non void non empty ProdCatStr;
func [1]C -> Object of C equals
the TerminalObj of C;
correctness;
let a,b be Object of C;
func a[x]b -> Object of C equals
(the CatProd of C).(a,b);
correctness;
func pr1(a,b) -> Morphism of C equals
(the Proj1 of C).(a,b);
correctness;
func pr2(a,b) -> Morphism of C equals
(the Proj2 of C).(a,b);
correctness;
end;
definition
let o,m;
func c1Cat(o,m) -> strict ProdCatStr equals
ProdCatStr(# {o},{m},m:->o,m:->o,(m,m):->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #);
correctness;
end;
registration let o,m be set;
cluster c1Cat(o,m) -> non empty trivial non void trivial';
coherence;
end;
theorem
the CatStr of c1Cat(o,m) = 1Cat(o,m);
Lm1: c1Cat(o,m) is Category-like
proof
set C = c1Cat(o,m);
set CP = the Comp of C, CD = the Source of C, CC = the Target of C;
thus
for f,g being Morphism of C holds [g,f] in dom CP iff dom g = cod f
proof
let f,g be Morphism of C;
A1: dom CP = {[m,m]} by FUNCOP_1:13;
f = m & g = m by TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
end;
registration
cluster strict Category-like reflexive transitive
associative with_identities
non void non empty for non void non empty ProdCatStr;
existence
proof
c1Cat(0,1) is Category-like transitive reflexive associative
with_identities by Lm1;
hence thesis;
end;
end;
registration
let o,m be set;
cluster c1Cat(o,m) -> Category-like reflexive transitive
associative with_identities non empty non void;
coherence by Lm1;
end;
theorem Th3:
for a,b being Object of c1Cat(o,m) holds a = b
proof
let a,b be Object of c1Cat(o,m);
a = o by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
theorem Th4:
for f,g being Morphism of c1Cat(o,m) holds f = g
proof
let f,g be Morphism of c1Cat(o,m);
f = m by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
theorem Th5:
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);
cod f = o by TARSKI:def 1;
then
A1: cod f = b by TARSKI:def 1;
dom f = o by TARSKI:def 1;
then dom f = a by TARSKI:def 1;
hence thesis by A1;
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 Th5;
hence thesis by CAT_1:def 5;
end;
theorem
for a,b being Object of c1Cat(o,m) holds Hom(a,b) <> {} by Th5;
theorem Th8:
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);
set f = the Morphism of b,a;
thus Hom(b,a)<>{} by Th5;
take f;
thus thesis by Th4;
end;
theorem Th9:
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 Th3;
let d be Object of c1Cat(o,m),f,g be Morphism of c1Cat(o,m) such that
f in Hom(d,cod p1) and
g in Hom(d,cod p2);
take h = p1;
thus h in Hom(d,c) by Th5;
thus thesis by Th4;
end;
definition
let IT be Category-like reflexive transitive
associative with_identities
non void non empty ProdCatStr;
attr IT is Cartesian means
:Def8:
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 Th10:
for o,m being set holds c1Cat(o,m) is Cartesian
by Th8,Th3,Th9;
registration
cluster strict Cartesian
for Category-like reflexive transitive associative with_identities
non void non empty ProdCatStr;
existence
proof
c1Cat(0,1) is Cartesian by Th10;
hence thesis;
end;
end;
definition
mode Cartesian_category is Cartesian
Category-like non void non empty
reflexive transitive associative with_identities
non void non empty
ProdCatStr;
end;
reserve C for Cartesian_category;
reserve a,b,c,d,e,s for Object of C;
theorem
[1]C is terminal by Def8;
theorem Th12:
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 Def8;
then consider f being Morphism of a,[1]C such that
A1: for g being Morphism of a,[1]C holds f = g;
thus f1 = f by A1
.= f2 by A1;
end;
theorem Th13:
Hom(a,[1]C) <> {}
proof
[1]C is terminal by Def8;
hence thesis;
end;
definition
let C,a;
func term(a) -> Morphism of a,[1]C means
not contradiction;
existence;
uniqueness by Th12;
end;
theorem Th14:
term a = term(a,[1]C)
proof
[1]C is terminal by Def8;
hence thesis by CAT_3:37;
end;
theorem
dom(term a) = a & cod(term a) = [1]C
proof
[1]C is terminal & term a = term(a,[1]C) by Def8,Th14;
hence thesis by CAT_3:35;
end;
theorem
Hom(a,[1]C) = {term a}
proof
for f2 being Morphism of a,[1]C holds term a = f2 by Th12;
hence thesis by Th13,CAT_1:8;
end;
theorem Th17:
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);
a[x]b is_a_product_wrt p1,p2 by Def8;
hence thesis by Def8;
end;
theorem Th18:
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);
a[x]b is_a_product_wrt p1,p2 by Def8;
hence thesis by Def8;
end;
definition
let C,a,b;
redefine func pr1(a,b) -> Morphism of a[x]b,a; :: redefines pr1 (CAT_4, definition)
coherence
proof
dom pr1(a,b) = a[x]b & cod pr1(a,b) = a by Th17;
hence thesis by CAT_1:4;
end;
redefine func pr2(a,b) -> Morphism of a[x]b,b; :: redefines pr2 (CAT_4, definition)
coherence
proof
dom pr2(a,b) = a[x]b & cod pr2(a,b) = b by Th18;
hence thesis by CAT_1:4;
end;
end;
theorem Th19:
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 Def8;
then
A1: dom p1 = c & dom p2 = c;
cod(p1) = a & cod(p2) = b by Def8;
hence thesis by A1,CAT_1:1;
end;
theorem
a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Def8;
theorem
C is with_finite_product
proof
A1: 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 Def8,Th17,Th18;
end;
[1]C is terminal by Def8;
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
A1: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19;
a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) & cod pr1(a,b) = a by Def8;
hence thesis by A1,CAT_3:57;
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
:Def10:
pr1(a,b)*it = f & pr2(a,b) *it = g;
existence
proof
A2: a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Def8;
Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19;
then consider h being Morphism of c,a[x]b such that
A3: 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,A2,CAT_3:55;
take h;
thus thesis by A3;
end;
uniqueness
proof
A4: a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Def8;
Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19;
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,A4,CAT_3:55;
let h1,h2 be Morphism of c,a[x]b such that
A6: pr1(a,b)*h1 = f & pr2(a,b)*h1 = g and
A7: pr1(a,b)*h2 = f & pr2(a,b)*h2 = g;
h1 = h by A6,A5;
hence thesis by A7,A5;
end;
end;
theorem Th23:
Hom(c,a) <> {} & Hom(c,b) <> {} implies Hom(c,a[x]b) <> {}
proof
A1: a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Def8;
Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19;
hence thesis by A1,CAT_3:55;
end;
theorem Th24:
<:pr1(a,b),pr2(a,b):> = id(a[x]b)
proof
A1: Hom(a[x]b,b) <> {} by Th19;
then
A2: pr2(a,b)*(id(a[x]b)) = pr2(a,b) by CAT_1:29;
A3: Hom(a[x]b,a) <> {} by Th19;
then pr1(a,b)*(id(a[x]b)) = pr1(a,b) by CAT_1:29;
hence thesis by A3,A1,A2,Def10;
end;
theorem Th25:
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)<>{} & Hom(c,b)<>{} and
A2: Hom(d,c)<>{};
A3: Hom(c,a[x]b) <> {} by A1,Th23;
A4: Hom(a[x]b,b) <> {} by Th19;
(pr2(a,b)*<:f,g:>)*h = g*h by A1,Def10;
then
A5: pr2(a,b)*(<:f,g:>*h) = g*h by A2,A4,A3,CAT_1:25;
A6: Hom(a[x]b,a) <> {} by Th19;
A7: Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,CAT_1:24;
(pr1(a,b)*<:f,g:>)*h = f*h by A1,Def10;
then pr1(a,b)*(<:f,g:>*h) = f*h by A2,A6,A3,CAT_1:25;
hence thesis by A5,A7,Def10;
end;
theorem Th26:
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
A1: Hom(c,a) <> {} & Hom(c,b) <> {};
then pr1(a,b)*<:f,g:> = f & pr2(a,b)*<:f,g:> = g by Def10;
hence thesis by A1,Def10;
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: g is monic;
let d be Object of C, f1,f2 be Morphism of d,c such that
A6: Hom(d,c)<>{} and
A7: <:f,g:>*f1 = <:f,g:>*f2;
A8: Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A6,CAT_1:24;
<:f*f1,g*f1:> = <:f,g:>*f1 & <:f*f2,g*f2:> = <:f,g:>*f2 by A1,A2,A6,Th25;
then g*f1 = g*f2 by A7,A8,Th26;
hence f1 = f2 by A5,A6;
end;
A9: now
assume
A10: f is monic;
let d;
let f1,f2 be Morphism of d,c such that
A11: Hom(d,c)<>{} and
A12: <:f,g:>*f1 = <:f,g:>*f2;
A13: Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A11,CAT_1:24;
<:f*f1,g*f1:> = <:f,g:>*f1 & <:f*f2,g*f2:> = <:f,g:>*f2 by A1,A2,A11,Th25;
then f*f1 = f*f2 by A12,A13,Th26;
hence f1 = f2 by A10,A11;
end;
Hom(c,a[x]b) <> {} by A1,A2,Th23;
hence thesis by A3,A9,A4;
end;
theorem Th28:
Hom(a,a[x][1]C) <> {} & Hom(a,[1]C[x]a) <> {}
proof
Hom(a,[1]C) <> {} & Hom(a,a) <> {} by Th13;
hence thesis by Th23;
end;
definition
let C,a;
func lambda(a) -> Morphism of [1]C[x]a,a equals
pr2([1]C,a);
correctness;
func lambda'(a) -> Morphism of a,[1]C[x]a equals
<:term a,id a:>;
correctness;
func rho(a) -> Morphism of a[x][1]C,a equals
pr1(a,[1]C);
correctness;
func rho'(a) -> Morphism of a,a[x][1]C equals
<:id a,term a:>;
correctness;
end;
theorem Th29:
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: (term a)*pr2([1]C,a) = pr1([1]C,a) by Th12;
A2: Hom(a,[1]C) <> {} & Hom(a,a) <> {} by Th13;
hence id a = lambda(a)*lambda'(a) by Def10;
A3: Hom([1]C[x]a,a) <> {} by Th19;
then (id a)*pr2([1]C,a) = pr2([1]C,a) by CAT_1:28;
then <:term a,id a:>*pr2([1]C,a) = <:pr1([1]C,a),pr2([1]C,a):> by A2,A3,A1
,Th25;
hence id([1]C[x]a) = lambda'(a)*lambda(a) by Th24;
thus id a = rho(a)*rho'(a) by A2,Def10;
A4: (term a)*pr1(a,[1]C) = pr2(a,[1]C) by Th12;
A5: Hom(a[x][1]C,a) <> {} by Th19;
then (id a)*pr1(a,[1]C) = pr1(a,[1]C) by CAT_1:28;
then <:id a,term a:>*pr1(a,[1]C) = <:pr1(a,[1]C),pr2(a,[1]C):> by A2,A5,A4
,Th25;
hence thesis by Th24;
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 Th19,Th28;
take rho'(a), rho(a);
thus thesis by Th29;
end;
thus Hom(a,[1]C[x]a) <> {} & Hom([1]C[x]a,a) <> {} by Th19,Th28;
take lambda'(a), lambda(a);
thus thesis by Th29;
end;
definition
let C,a,b;
func Switch(a,b) -> Morphism of a[x]b,b[x]a equals
<:pr2(a,b),pr1(a,b):>;
correctness;
end;
theorem Th31:
Hom(a[x]b,b[x]a)<>{}
proof
Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19;
hence thesis by Th23;
end;
theorem Th32:
Switch(a,b)*Switch(b,a) = id(b[x]a)
proof
A1: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19;
A2: Hom(b[x]a,b) <> {} & Hom(b[x]a,a) <> {} by Th19;
then Hom(b[x]a,a[x]b)<>{} by Th23;
hence Switch(a,b)*Switch(b,a) = <:pr2(a,b)*<:pr2(b,a),pr1(b,a):>,pr1(a,b)*<:
pr2(b,a),pr1(b,a):>:> by A1,Th25
.= <:pr1(b,a),pr1(a,b)*<:pr2(b,a),pr1(b,a):>:> by A2,Def10
.= <:pr1(b,a),pr2(b,a):> by A2,Def10
.= id(b[x]a) by Th24;
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 Th31;
take Switch(a,b), Switch(b,a);
thus thesis by Th32;
end;
definition
let C,a;
func Delta a -> Morphism of a,a[x]a equals
<:id a,id a:>;
correctness;
end;
theorem
Hom(a,a[x]a) <> {}
proof
Hom(a,a) <> {};
hence thesis by Th23;
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) <> {};
Hom(b,b) <> {} & (id b)*f = f by A1,CAT_1:28;
hence thesis by A1,Th25;
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
<: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
<:<:pr1(a,b
[x]c),pr1(b,c)*pr2(a,b[x]c):>,pr2(b,c)*pr2(a,b[x]c):>;
correctness;
end;
theorem Th36:
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)[x]c,a[x]b) <> {} by Th19;
Hom(a[x]b,b) <> {} by Th19;
then
A2: Hom((a[x]b)[x]c,b) <> {} by A1,CAT_1:24;
Hom(a[x]b,a) <> {} by Th19;
then
A3: Hom((a[x]b)[x]c,a) <> {} by A1,CAT_1:24;
Hom((a[x]b)[x]c,c) <> {} by Th19;
then Hom((a[x]b)[x]c,b[x]c) <> {} by A2,Th23;
hence Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} by A3,Th23;
A4: Hom(a[x](b[x]c),b[x]c) <> {} by Th19;
Hom(b[x]c,c) <> {} by Th19;
then
A5: Hom(a[x](b[x]c),c) <> {} by A4,CAT_1:24;
Hom(b[x]c,b) <> {} by Th19;
then
A6: Hom(a[x](b[x]c),b) <> {} by A4,CAT_1:24;
Hom(a[x](b[x]c),a) <> {} by Th19;
then Hom(a[x](b[x]c),a[x]b) <> {} by A6,Th23;
hence thesis by A5,Th23;
end;
theorem Th37:
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
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):>;
A1: Hom((a[x]b)[x]c,a[x]b) <> {} by Th19;
A2: Hom(a[x]b,b) <> {} by Th19;
then
A3: Hom((a[x]b)[x]c,b) <> {} by A1,CAT_1:24;
A4: Hom((a[x]b)[x]c,c) <> {} by Th19;
then
A5: Hom((a[x]b)[x]c,b[x]c) <> {} by A3,Th23;
A6: Hom(a[x]b,a) <> {} by Th19;
then
A7: Hom((a[x]b)[x]c,a) <> {} by A1,CAT_1:24;
A8: Hom(a[x](b[x]c),b[x]c) <> {} by Th19;
A9: Hom(b[x]c,c) <> {} by Th19;
then
A10: Hom(a[x](b[x]c),c) <> {} by A8,CAT_1:24;
A11: Hom(b[x]c,b) <> {} by Th19;
then
A12: Hom(a[x](b[x]c),b) <> {} by A8,CAT_1:24;
A13: Hom(a[x](b[x]c),a) <> {} by Th19;
then
A14: Hom(a[x](b[x]c),a[x]b) <> {} by A12,Th23;
A15: Hom(a[x](b[x]c),(a[x]b)[x]c) <> {} by Th36;
then pr2(a,b)*pr1(a[x]b,c)*g = pr2(a,b)*(pr1(a[x]b,c)*g) by A1,A2,CAT_1:25
.= pr2(a,b)*l by A10,A14,Def10
.= pr1(b,c)*pr2(a,b[x]c) by A12,A13,Def10;
then
A16: k*g = <:pr1(b,c)*pr2(a,b[x]c),pr2(a[x]b,c)*g:> by A3,A4,A15,Th25
.= <:pr1(b,c)*pr2(a,b[x]c),pr2(b,c)*pr2(a,b[x]c):> by A10,A14,Def10
.= <:pr1(b,c),pr2(b,c):>*pr2(a,b[x]c) by A11,A8,A9,Th25
.= id(b[x]c)*pr2(a,b[x]c) by Th24
.= pr2(a,b[x]c) by A8,CAT_1:28;
A17: Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} by Th36;
then pr1(b,c)*pr2(a,b[x]c)*f = pr1(b,c)*(pr2(a,b[x]c)*f) by A11,A8,CAT_1:25
.= pr1(b,c)*k by A7,A5,Def10
.= pr2(a,b)*pr1(a[x]b,c) by A3,A4,Def10;
then
A18: l*f = <:pr1(a,b[x]c)*f,pr2(a,b)*pr1(a[x]b,c):> by A17,A12,A13,Th25
.= <:pr1(a,b)*pr1(a[x]b,c),pr2(a,b)*pr1(a[x]b,c):> by A7,A5,Def10
.= <:pr1(a,b),pr2(a,b):>*pr1(a[x]b,c) by A6,A1,A2,Th25
.= id(a[x]b)*pr1(a[x]b,c) by Th24
.= pr1(a[x]b,c) by A1,CAT_1:28;
pr1(a,b)*pr1(a[x]b,c)*g = pr1(a,b)*(pr1(a[x]b,c)*g) by A6,A1,A15,CAT_1:25
.= pr1(a,b)*l by A10,A14,Def10
.= pr1(a,b[x]c) by A12,A13,Def10;
hence
Alpha(a,b,c)*Alpha'(a,b,c) = <:pr1(a,b[x]c),pr2(a,b[x]c):> by A7,A5,A15,A16
,Th25
.= id(a[x](b[x]c)) by Th24;
pr2(b,c)*pr2(a,b[x]c)*f = pr2(b,c)*(pr2(a,b[x]c)*f) by A17,A8,A9,CAT_1:25
.= pr2(b,c)*k by A7,A5,Def10
.= pr2(a[x]b,c) by A3,A4,Def10;
hence Alpha'(a,b,c)*Alpha(a,b,c) = <:pr1(a[x]b,c),pr2(a[x]b,c):> by A17,A10
,A14,A18,Th25
.= id((a[x]b)[x]c) by Th24;
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 Th36;
take Alpha(a,b,c), Alpha'(a,b,c);
thus thesis by Th37;
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
<: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 that
A1: Hom(a,c) <> {} and
A2: Hom(b,d) <> {};
Hom(a[x]b,b) <> {} by Th19;
then
A3: Hom(a[x]b,d) <> {} by A2,CAT_1:24;
Hom(a[x]b,a) <> {} by Th19;
then Hom(a[x]b,c) <> {} by A1,CAT_1:24;
hence thesis by A3,Th23;
end;
theorem
(id a)[x](id b) = id(a[x]b)
proof
Hom(a[x]b,b) <> {} by Th19;
then
A1: (id b)*pr2(a,b) = pr2(a,b) by CAT_1:28;
Hom(a[x]b,a) <> {} by Th19;
then (id a)*pr1(a,b) = pr1(a,b) by CAT_1:28;
hence thesis by A1,Th24;
end;
theorem Th41:
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) <> {} & Hom(e,c) <> {};
A4: Hom(e,a[x]c) <> {} by A3,Th23;
A5: Hom(a[x]c,c) <> {} by Th19;
then
A6: Hom(a[x]c,d) <> {} by A2,CAT_1:24;
A7: Hom(a[x]c,a) <> {} by Th19;
then
A8: Hom(a[x]c,b) <> {} by A1,CAT_1:24;
pr2(a,c)*<:g,k:> = k by A3,Def10;
then
A9: h*k = (h*pr2(a,c))*<:g,k:> by A2,A4,A5,CAT_1:25;
pr1(a,c)*<:g,k:> = g by A3,Def10;
then f*g = (f*pr1(a,c))*<:g,k:> by A1,A4,A7,CAT_1:25;
hence thesis by A4,A8,A6,A9,Th25;
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) <> {};
Hom(c,c) <> {};
hence (f[x]g)*Delta(c) = <:f*(id c),g*(id c):> by A1,A2,Th41
.= <:f,g*(id c):> by A1,CAT_1:29
.= <:f,g:> by A2,CAT_1:29;
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,s) <> {} by Th19;
then
A6: Hom(e[x]s,c) <> {} by A4,CAT_1:24;
A7: Hom(e[x]s,e) <> {} by Th19;
then f*(g*pr1(e,s)) = (f*g)*pr1(e,s) by A1,A3,CAT_1:25;
then
A8: (f*g)[x](h*k) = <:f*(g*pr1(e,s)),h*(k*pr2(e,s)):> by A2,A4,A5,CAT_1:25;
Hom(e[x]s,a) <> {} by A3,A7,CAT_1:24;
hence thesis by A1,A2,A6,A8,Th41;
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 carrier of C ex a being Object of C, F9 being
Injections_family of a,I st doms F9 = F & a is_a_coproduct_wrt F9;
end;
theorem Th44:
for C being Category holds C is with_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 is with_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
reconsider F = {} as Function of {},the carrier of C by RELSET_1:12;
A1: 0 in {0,1} by TARSKI:def 2;
assume
A2: for I being finite set, F being Function of I,the carrier of C ex
a being Object of C, F9 being Injections_family of a,I st doms F9 = F & a
is_a_coproduct_wrt F9;
then consider
a being Object of C, F9 being Injections_family of a,{} such that
doms F9 = F and
A3: a is_a_coproduct_wrt F9;
thus ex a being Object of C st a is initial by A3,CAT_3:75;
let a,b be Object of C;
set F = (0,1)-->(a,b);
consider c being Object of C, F9 being Injections_family of c,{0,1} such
that
A4: doms F9 = F and
A5: c is_a_coproduct_wrt F9 by A2;
take c, i1 = F9/.0, i2 = F9/.1;
A6: 1 in {0,1} by TARSKI:def 2;
then
A7: i2 = F9.1 by FUNCT_2:def 13;
F/.0 = a & F/.1 = b by CAT_3:3;
hence dom i1 = a & dom i2 = b by A4,A1,A6,CAT_3:def 1;
thus cod i1 = c & cod i2 = c by A1,A6,CAT_3:62;
dom F9 = {0,1} & i1 = F9.0 by A1,FUNCT_2:def 1,def 13;
then F9 = (0,1)-->(i1,i2) by A7,FUNCT_4:66;
hence thesis by A5,CAT_3:79;
end;
given a being Object of C such that
A8: a is initial;
defpred Q[Nat] means for I being finite set, F being Function of I,the
carrier of C st card I = $1 ex a being Object of C, F9 being Injections_family
of a,I st doms F9 = F & a is_a_coproduct_wrt F9;
assume
A9: 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;
A10: for n being Nat st Q[n] holds Q[n+1]
proof
let n be Nat such that
A11: Q[n];
let I be finite set, F be Function of I,the carrier of C such that
A12: card I = n+1;
set x = the Element of I;
reconsider Ix = I \ {x} as finite set;
reconsider sx = {x} as finite set;
reconsider G = F|(I\{x}) as Function of I\{x},the carrier of C by
FUNCT_2:32;
card(Ix) = card(I) - card(sx) by A12,CARD_1:27,CARD_2:44,ZFMISC_1:31
.= card(I) - 1 by CARD_1:30
.= n by A12,XCMPLX_1:26;
then consider
a being Object of C, G9 being Injections_family of a,I\{x} such
that
A13: doms G9 = G and
A14: a is_a_coproduct_wrt G9 by A11;
set b = F/.x;
consider c being Object of C, i1,i2 being Morphism of C such that
A15: dom i1 = a and
A16: dom i2 = b and
A17: cod i1 = c and
A18: cod i2 = c and
A19: c is_a_coproduct_wrt i1,i2 by A9;
set F9 = (i1*G9) +* (x .-->i2);
A20: dom({x} -->i2) = {x} by FUNCT_2:def 1;
rng F9 c= rng(i1*G9) \/ rng(x .-->i2) by FUNCT_4:17;
then
A21: rng F9 c= the carrier' of C by XBOOLE_1:1;
dom(i1*G9) = I\{x} by FUNCT_2:def 1;
then
A22: dom(i1*G9) \/ dom(x .-->i2) = I \/ {x} by A20,XBOOLE_1:39
.= I by A12,CARD_1:27,ZFMISC_1:40;
then dom F9 = I by FUNCT_4:def 1;
then reconsider F9 as Function of I, the carrier' of C by A21,FUNCT_2:def 1
,RELSET_1:4;
A23: cods G9 = (I\{x})-->a by CAT_3:def 16;
now
let y be object;
assume
A24: y in I;
now
per cases;
suppose
y = x;
then
A25: y in {x} by TARSKI:def 1;
F9/.y = F9.y by A24,FUNCT_2:def 13
.= (x .-->i2).y by A20,A25,FUNCT_4:13
.= i2 by A25,FUNCOP_1:7;
hence (I --> c).y = cod(F9/.y) by A18,A24,FUNCOP_1:7
.= (cods F9)/.y by A24,CAT_3:def 2;
end;
suppose
A26: y <> x;
then
A27: not y in {x} by TARSKI:def 1;
A28: y in I\{x} by A24,A26,ZFMISC_1:56;
F9/.y = F9.y by A24,FUNCT_2:def 13
.= (i1*G9).y by A20,A22,A24,A27,FUNCT_4:def 1
.= (i1*G9)/.y by A28,FUNCT_2:def 13;
hence (cods F9)/.y = cod((i1*G9)/.y) by A24,CAT_3:def 2
.= (cods(i1*G9))/.y by A28,CAT_3:def 2
.= ((I\{x})-->c)/.y by A15,A17,A23,CAT_3:17
.= c by A24,A26,CAT_3:2,ZFMISC_1:56
.= (I --> c).y by A24,FUNCOP_1:7;
end;
end;
hence (cods F9).y = (I --> c).y by A24,FUNCT_2:def 13;
end;
then reconsider F9 as Injections_family of c,I
by CAT_3:def 16,FUNCT_2:12;
take c,F9;
A29: now
let y be set;
assume
A30: y in I;
now
per cases;
suppose
A31: y = x;
then
A32: y in {x} by TARSKI:def 1;
F9/.y = F9.y by A30,FUNCT_2:def 13
.= (x .-->i2).y by A20,A32,FUNCT_4:13
.= i2 by A32,FUNCOP_1:7;
hence (doms F9)/.y = F/.y by A16,A30,A31,CAT_3:def 1;
end;
suppose
A33: y <> x;
then
A34: not y in {x} by TARSKI:def 1;
A35: y in I\{x} by A30,A33,ZFMISC_1:56;
F9/.y = F9.y by A30,FUNCT_2:def 13
.= (i1*G9).y by A20,A22,A30,A34,FUNCT_4:def 1
.= (i1*G9)/.y by A35,FUNCT_2:def 13;
hence (doms F9)/.y = dom((i1*G9)/.y) by A30,CAT_3:def 1
.= (doms(i1*G9))/.y by A35,CAT_3:def 1
.= G/.y by A13,A15,A23,CAT_3:17
.= G.y by A35,FUNCT_2:def 13
.= F.y by A30,A33,FUNCT_1:49,ZFMISC_1:56
.= F/.y by A30,FUNCT_2:def 13;
end;
end;
hence (doms F9)/.y = F/.y;
end;
hence
doms F9 = F by CAT_3:1;
thus F9 is Injections_family of c,I;
let d be Object of C;
let F99 be Injections_family of d,I such that
A36: doms F9 = doms F99;
reconsider G99 = F99|(I\{x}) as Function of I\{x},the carrier' of C by
FUNCT_2:32;
now
let y be set;
assume
A37: y in I\{x};
then G99/.y = G99.y by FUNCT_2:def 13
.= F99.y by A37,FUNCT_1:49
.= F99/.y by A37,FUNCT_2:def 13;
hence cods(G99)/.y = cod(F99/.y) by A37,CAT_3:def 2
.= d by A37,CAT_3:62
.= ((I\{x})-->d)/.y by A37,CAT_3:2;
end;
then reconsider G99 as Injections_family of d,I\{x}
by CAT_3:1,def 16;
now
let y be set;
assume
A38: y in I\{x};
then
A39: G/.y = G.y by FUNCT_2:def 13
.= F.y by A38,FUNCT_1:49
.= F/.y by A38,FUNCT_2:def 13;
F99/.y = F99.y by A38,FUNCT_2:def 13
.= G99.y by A38,FUNCT_1:49
.= G99/.y by A38,FUNCT_2:def 13;
hence (doms G9)/.y = dom(G99/.y) by A13,A29,A36,A38,A39,CAT_3:1,def 1
.= (doms G99)/.y by A38,CAT_3:def 1;
end;
then consider h9 being Morphism of C such that
A40: h9 in Hom(a,d) and
A41: for k being Morphism of C st k in Hom(a,d) holds (for y being set
st y in I\{x} holds k(*)(G9/.y) = G99/.y) iff h9 = k by A14,CAT_3:1;
A42: x in {x} by TARSKI:def 1;
set g = F99/.x;
A43: cod g = d by A12,CARD_1:27,CAT_3:62;
A44: F9/.x = F9.x by A12,CARD_1:27,FUNCT_2:def 13
.= (x .-->i2).x by A20,A42,FUNCT_4:13
.= i2 by A42,FUNCOP_1:7;
then dom i2 = (doms F9)/.x by A12,CARD_1:27,CAT_3:def 1
.= dom g by A12,A36,CARD_1:27,CAT_3:def 1;
then g in Hom(dom i2,d) by A43;
then consider h being Morphism of C such that
A45: h in Hom(c,d) and
A46: for k being Morphism of C st k in Hom(c,d) holds k(*)i1 = h9 & k(*)i2
= g iff h = k by A15,A19,A40;
take h;
thus h in Hom(c,d) by A45;
let k be Morphism of C such that
A47: k in Hom(c,d);
thus (for y being set st y in I holds k(*)(F9/.y) = F99/.y) implies h = k
proof
A48: dom k = c by A47,CAT_1:1;
then
A49: dom(k(*)i1) = a by A15,A17,CAT_1:17;
assume
A50: for y being set st y in I holds k(*)(F9/.y) = F99/.y;
A51: for y being set st y in I\{x} holds k(*)i1(*)(G9/.y) = G99/.y
proof
let y be set;
assume
A52: y in I\{x};
then
A53: not y in {x} by XBOOLE_0:def 5;
A54: F9/.y = F9.y by A52,FUNCT_2:def 13
.= (i1*G9).y by A20,A22,A52,A53,FUNCT_4:def 1
.= (i1*G9)/.y by A52,FUNCT_2:def 13;
cod(G9/.y) = a by A52,CAT_3:62;
hence k(*)i1(*)(G9/.y) = k(*)(i1(*)(G9/.y)) by A15,A17,A48,CAT_1:18
.= k(*)((i1*G9)/.y) by A52,CAT_3:def 6
.= F99/.y by A50,A52,A54
.= F99.y by A52,FUNCT_2:def 13
.= G99.y by A52,FUNCT_1:49
.= G99/.y by A52,FUNCT_2:def 13;
end;
cod k = d by A47,CAT_1:1;
then cod(k(*)i1) = d by A17,A48,CAT_1:17;
then k(*)i1 in Hom(a,d) by A49;
then
A55: k(*)i1 = h9 by A41,A51;
k(*)i2 = g by A12,A44,A50,CARD_1:27;
hence thesis by A46,A47,A55;
end;
assume
A56: h = k;
let y be set such that
A57: y in I;
now
per cases;
suppose
A58: y = x;
then
A59: y in {x} by TARSKI:def 1;
F9/.y = F9.y by A57,FUNCT_2:def 13
.= (x .-->i2).y by A20,A59,FUNCT_4:13
.= i2 by A59,FUNCOP_1:7;
hence thesis by A46,A47,A56,A58;
end;
suppose
A60: y <> x;
then
A61: not y in {x} by TARSKI:def 1;
A62: dom k = c by A47,CAT_1:1;
A63: y in I\{x} by A57,A60,ZFMISC_1:56;
A64: cod(G9/.y) = a by A57,A60,CAT_3:62,ZFMISC_1:56;
F9/.y = F9.y by A57,FUNCT_2:def 13
.= (i1*G9).y by A20,A22,A57,A61,FUNCT_4:def 1
.= (i1*G9)/.y by A63,FUNCT_2:def 13
.= i1(*)(G9/.y) by A63,CAT_3:def 6;
hence k(*)(F9/.y) = k(*)i1(*)(G9/.y) by A15,A17,A62,A64,CAT_1:18
.= h9(*)(G9/.y) by A46,A47,A56
.= G99/.y by A40,A41,A63
.= G99.y by A63,FUNCT_2:def 13
.= F99.y by A57,A60,FUNCT_1:49,ZFMISC_1:56
.= F99/.y by A57,FUNCT_2:def 13;
end;
end;
hence thesis;
end;
let I be finite set, F be Function of I,the carrier of C;
A65: card I = card I;
A66: Q[ 0 ]
proof
let I be finite set, F be Function of I,the carrier of C;
assume card I = 0;
then
A67: I = {};
{} is Function of {}, the carrier' of C by RELSET_1:12;
then reconsider F9 = {} as Injections_family of a,I by A67,CAT_3:63;
take a,F9;
for x being set st x in I holds (doms F9)/.x = F/.x;
hence doms F9 = F by CAT_3:1;
thus thesis by A8,A67,CAT_3:75;
end;
for n being Nat holds Q[n] from NAT_1:sch 2(A66,A10);
hence thesis by A65;
end;
definition
struct (CatStr)CoprodCatStr (# carrier,carrier' -> set, Source,Target ->
Function of the carrier', the carrier, Comp -> PartFunc of [:the carrier', the
carrier' :],the carrier',
Initial
-> Element of the carrier, Coproduct -> Function of [:the carrier,the carrier:]
,the carrier, Incl1,Incl2 -> Function of [:the carrier,the carrier:],the
carrier' #);
end;
registration
cluster non void non empty for CoprodCatStr;
existence
proof
set o = the set;
take CoprodCatStr(# {o},{o},o:->o,o:->o,(o,o):->o,Extract(o),(o,o)
:->o,(o,o):->o,(o,o):->o #);
thus thesis;
end;
end;
definition
let C be non void non empty CoprodCatStr;
func EmptyMS C -> Object of C equals
the Initial of C;
correctness;
let a,b be Object of C;
func a+b -> Object of C equals
(the Coproduct of C).(a,b);
correctness;
func in1(a,b) -> Morphism of C equals
(the Incl1 of C).(a,b);
correctness;
func in2(a,b) -> Morphism of C equals
(the Incl2 of C).(a,b);
correctness;
end;
definition
let o,m;
func c1Cat*(o,m) -> strict CoprodCatStr equals
CoprodCatStr(# {o},{m},m:->o,m:->o,(m,m):->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #);
correctness;
end;
::$CT
registration
let o,m;
cluster c1Cat*(o,m) -> non void non empty trivial trivial';
coherence;
end;
Lm2: c1Cat*(o,m) is Category-like
proof
set C = c1Cat*(o,m);
set CP = the Comp of C, CD = the Source of C, CC = the Target of C;
thus
for f,g being Morphism of C holds [g,f] in dom CP iff dom g=cod f
proof
let f,g be Morphism of C;
A1: dom CP = {[m,m]} by FUNCOP_1:13;
A2: f = m & g = m by TARSKI:def 1;
thus [g,f] in dom CP implies dom g=cod f
by ZFMISC_1:def 10;
thus thesis by A1,A2,TARSKI:def 1;
end;
end;
registration
cluster strict Category-like
reflexive transitive associative with_identities
for non void non empty CoprodCatStr;
existence
proof
c1Cat*(0,1) is
reflexive transitive associative with_identities
Category-like by Lm2;
hence thesis;
end;
end;
registration
let o,m be set;
cluster c1Cat*(o,m) -> Category-like
reflexive transitive associative with_identities
non void non empty;
coherence by Lm2;
end;
theorem Th45:
for a,b being Object of c1Cat*(o,m) holds a = b
proof
let a,b be Object of c1Cat*(o,m);
a = o by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
theorem Th46:
for f,g being Morphism of c1Cat*(o,m) holds f = g
proof
let f,g be Morphism of c1Cat*(o,m);
f = m by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
theorem Th47:
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);
cod f = o by TARSKI:def 1;
then
A1: cod f = b by TARSKI:def 1;
dom f = o by TARSKI:def 1;
then dom f = a by TARSKI:def 1;
hence thesis by A1;
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 Th47;
hence thesis by CAT_1:def 5;
end;
theorem
for a,b being Object of c1Cat*(o,m) holds Hom(a,b) <> {} by Th47;
theorem Th50:
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);
set f = the Morphism of a,b;
thus Hom(a,b)<>{} by Th47;
take f;
thus thesis by Th46;
end;
theorem Th51:
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 Th45;
let d be Object of c1Cat*(o,m), f,g be Morphism of c1Cat*(o,m) such that
f in Hom(dom i1,d) and
g in Hom(dom i2,d);
take h = i1;
thus h in Hom(c,d) by Th47;
thus thesis by Th46;
end;
definition
let IT be Category-like
reflexive transitive associative with_identities
non void non empty CoprodCatStr;
attr IT is Cocartesian means
:Def26:
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 Th52:
for o,m being set holds c1Cat*(o,m) is Cocartesian
by Th50,Th45,Th51;
registration
cluster strict Cocartesian for
reflexive transitive associative with_identities
Category-like non void non empty CoprodCatStr;
existence
proof
c1Cat*(0,1) is Cocartesian by Th52;
hence thesis;
end;
end;
definition
mode Cocartesian_category is Cocartesian
reflexive transitive associative with_identities
Category-like non void non empty
CoprodCatStr;
end;
reserve C for Cocartesian_category;
reserve a,b,c,d,e,s for Object of C;
theorem
EmptyMS C is initial by Def26;
theorem Th54:
for f1,f2 being Morphism of EmptyMS C,a holds f1 = f2
proof
let f1,f2 be Morphism of EmptyMS C,a;
EmptyMS C is initial by Def26;
then consider f being Morphism of EmptyMS C,a such that
A1: for g being Morphism of EmptyMS C, a holds f = g;
thus f1 = f by A1
.= f2 by A1;
end;
definition
let C,a;
func init a -> Morphism of EmptyMS C, a means
not contradiction;
existence;
uniqueness by Th54;
end;
theorem Th55:
Hom(EmptyMS C,a) <> {}
proof
EmptyMS C is initial by Def26;
hence thesis;
end;
theorem Th56:
init a = init(EmptyMS C,a)
proof
EmptyMS C is initial by Def26;
hence thesis by CAT_3:40;
end;
theorem
dom(init a) = EmptyMS C & cod(init a) = a
proof
EmptyMS C is initial & init a = init(EmptyMS C,a) by Def26,Th56;
hence thesis by CAT_3:38;
end;
theorem
Hom(EmptyMS C,a) = {init a}
proof
for f2 being Morphism of EmptyMS C,a holds init a = f2 by Th54;
hence thesis by Th55,CAT_1:8;
end;
theorem Th59:
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);
a+b is_a_coproduct_wrt i1,i2 by Def26;
hence thesis by Def26;
end;
theorem Th60:
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);
a+b is_a_coproduct_wrt i1,i2 by Def26;
hence thesis by Def26;
end;
theorem Th61:
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 Def26;
then
A1: cod i1 = c & cod i2 = c;
dom(i1) = a & dom(i2) = b by Def26;
hence thesis by A1,CAT_1:1;
end;
theorem
a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Def26;
theorem
C is with_finite_coproduct
proof
A1: 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 Def26,Th59,Th60;
end;
EmptyMS C is initial by Def26;
hence thesis by A1,Th44;
end;
definition
let C,a,b;
redefine func in1(a,b) -> Morphism of a,a+b; :: redefines in1 (CAT_4, definition)
coherence
proof
dom in1(a,b) = a & cod in1(a,b) = a+b by Th59;
hence thesis by CAT_1:4;
end;
redefine func in2(a,b) -> Morphism of b,a+b; :: redefines in2 (CAT_4, definition)
coherence
proof
dom in2(a,b) = b & cod in2(a,b) = a+b by Th60;
hence thesis by CAT_1:4;
end;
end;
theorem
Hom(a,b) <> {} & Hom(b,a) <> {} implies in1(a,b) is coretraction & in2
(a,b) is coretraction
proof
A1: Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th61;
a+b is_a_coproduct_wrt in1(a,b),in2(a,b) & dom in1(a,b) = a by Def26;
hence thesis by A1,CAT_3:82;
end;
definition
let C,a,b;
redefine func in1(a,b) -> Morphism of a,a+b; :: redefines in1 (CAT_4, definition)
coherence
proof
cod in1(a,b) = a+b & dom in1(a,b) = a by Th59;
hence thesis;
end;
redefine func in2(a,b) -> Morphism of b,a+b; :: redefines in2 (CAT_4, definition)
coherence
proof
cod in2(a,b) = a+b & dom in2(a,b) = b by Th60;
hence thesis;
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
:Def28:
it*in1(a,b) = f & it*in2(a,b ) = g;
existence
proof
A2: a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Def26;
Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th61;
then consider h being Morphism of a+b,c such that
A3: for k being Morphism of a+b,c holds k*in1(a,b) = f & k*in2(a,b) =
g iff h = k by A1,A2,CAT_3:81;
take h;
thus thesis by A3;
end;
uniqueness
proof
A4: Hom(b,a+b) <> {} by Th61;
a+b is_a_coproduct_wrt in1(a,b),in2(a,b) & Hom(a,a+b) <> {} by Def26,Th61;
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,A4,CAT_3:81;
let h1,h2 be Morphism of a+b,c such that
A6: h1*in1(a,b) = f & h1*in2(a,b) = g and
A7: h2*in1(a,b) = f & h2*in2(a,b) = g;
h1 = h by A6,A5;
hence thesis by A7,A5;
end;
end;
theorem Th65:
Hom(a,c) <> {} & Hom(b,c) <> {} implies Hom(a+b,c) <> {}
proof
A1: a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Def26;
Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th61;
hence thesis by A1,CAT_3:81;
end;
theorem Th66:
[$in1(a,b),in2(a,b)$] = id(a+b)
proof
A1: Hom(b,a+b) <> {} by Th61;
then
A2: (id(a+b))*in2(a,b) = in2(a,b) by CAT_1:28;
A3: Hom(a,a+b) <> {} by Th61;
then (id(a+b))*in1(a,b) = in1(a,b) by CAT_1:28;
hence thesis by A3,A1,A2,Def28;
end;
theorem Th67:
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)<>{} & Hom(b,c)<>{} and
A2: Hom(c,d)<>{};
A3: Hom(a+b,c) <> {} by A1,Th65;
A4: Hom(b,a+b) <> {} by Th61;
h*([$f,g$]*in2(a,b)) = h*g by A1,Def28;
then
A5: h*[$f,g$]*in2(a,b) = h*g by A2,A4,A3,CAT_1:25;
A6: Hom(a,a+b) <> {} by Th61;
A7: Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,CAT_1:24;
h*([$f,g$]*in1(a,b)) = h*f by A1,Def28;
then h*[$f,g$]*in1(a,b) = h*f by A2,A6,A3,CAT_1:25;
hence thesis by A5,A7,Def28;
end;
theorem Th68:
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
A1: Hom(a,c) <> {} & Hom(b,c) <> {};
then [$f,g$]*in1(a,b) = f & [$f,g$]*in2(a,b) = g by Def28;
hence thesis by A1,Def28;
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: g is epi;
let d be Object of C, f1,f2 be Morphism of c,d such that
A6: Hom(c,d)<>{} and
A7: f1*[$f,g$] = f2*[$f,g$];
A8: Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A6,CAT_1:24;
[$f1*f,f1*g$] = f1*[$f,g$] & [$f2*f,f2*g$] = f2*[$f,g$] by A1,A2,A6,Th67;
then f1*g = f2*g by A7,A8,Th68;
hence f1 = f2 by A5,A6;
end;
A9: now
assume
A10: f is epi;
let d;
let f1,f2 be Morphism of c,d such that
A11: Hom(c,d)<>{} and
A12: f1*[$f,g$] = f2*[$f,g$];
A13: Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A11,CAT_1:24;
[$f1*f,f1*g$] = f1*[$f,g$] & [$f2*f,f2*g$] = f2*[$f,g$] by A1,A2,A11,Th67;
then f1*f = f2*f by A12,A13,Th68;
hence f1 = f2 by A10,A11;
end;
Hom(a+b,c) <> {} by A1,A2,Th65;
hence thesis by A3,A9,A4;
end;
theorem
a, a+EmptyMS C are_isomorphic & a,EmptyMS C+a are_isomorphic
proof
A1: in2(EmptyMS C,a)*init a = in1(EmptyMS C,a) by Th54;
A2: Hom(EmptyMS C,a) <> {} & Hom(a,a) <> {} by Th55;
thus a,a+EmptyMS C are_isomorphic
proof
thus
A3: Hom(a,a+EmptyMS C) <> {} by Th61;
thus Hom(a+EmptyMS C,a) <> {} by A2,Th65;
take g = in1(a,EmptyMS C), f = [$id a,init a$];
A4: in1(a,EmptyMS C)*init a = in2(a,EmptyMS C) by Th54;
in1(a,EmptyMS C)*id(a) = in1(a,EmptyMS C) by A3,CAT_1:29;
then g*f = [$in1(a,EmptyMS C),in2(a,EmptyMS C)$] by A2,A3,A4,Th67;
hence thesis by A2,Def28,Th66;
end;
thus
A5: Hom(a,EmptyMS C+a) <> {} by Th61;
thus Hom(EmptyMS C+a,a) <> {} by A2,Th65;
take g = in2(EmptyMS C,a), f = [$init a,id a$];
in2(EmptyMS C,a)*id(a) = in2(EmptyMS C,a) by A5,CAT_1:29;
then g*f = [$in1(EmptyMS C,a),in2(EmptyMS C,a)$] by A2,A5,A1,Th67;
hence thesis by A2,Def28,Th66;
end;
theorem
a+b,b+a are_isomorphic
proof
A1: Hom(a,b+a) <> {} & Hom(b,b+a) <> {} by Th61;
hence
A2: Hom(a+b,b+a)<>{} by Th65;
A3: Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th61;
hence
A4: Hom(b+a,a+b)<>{} by Th65;
take f9 = [$in2(b,a),in1(b,a)$], f = [$in2(a,b),in1(a,b)$];
thus f9*f = [$f9*in2(a,b),f9*in1(a,b)$] by A2,A3,Th67
.= [$in1(b,a),f9*in1(a,b)$] by A1,Def28
.= [$in1(b,a),in2(b,a)$] by A1,Def28
.= id(b+a) by Th66;
thus f*f9 = [$f*in2(b,a),f*in1(b,a)$] by A1,A4,Th67
.= [$in1(a,b),f*in1(b,a)$] by A3,Def28
.= [$in1(a,b),in2(a,b)$] by A3,Def28
.= id(a+b) by Th66;
end;
theorem
(a+b)+c,a+(b+c) are_isomorphic
proof
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)$];
A1: Hom(b+c,a+(b+c)) <> {} by Th61;
A2: Hom(b,b+c) <> {} by Th61;
then
A3: Hom(b,a+(b+c)) <> {} by A1,CAT_1:24;
A4: Hom(a,a+(b+c)) <> {} by Th61;
then
A5: Hom(a+b,a+(b+c)) <> {} by A3,Th65;
A6: Hom(c,b+c) <> {} by Th61;
then
A7: Hom(c,a+(b+c)) <> {} by A1,CAT_1:24;
hence
A8: Hom((a+b)+c,a+(b+c)) <> {} by A5,Th65;
A9: Hom(a+b,(a+b)+c) <> {} by Th61;
A10: Hom(b,a+b) <> {} by Th61;
then
A11: Hom(b,(a+b)+c) <> {} by A9,CAT_1:24;
A12: Hom(c,(a+b)+c) <> {} by Th61;
then
A13: Hom(b+c,(a+b)+c) <> {} by A11,Th65;
A14: Hom(a,a+b) <> {} by Th61;
then
A15: Hom(a,(a+b)+c) <> {} by A9,CAT_1:24;
hence
A16: Hom(a+(b+c),(a+b)+c) <> {} by A13,Th65;
take g = [$l,in2(a,b+c)*in2(b,c)$];
g*(in1(a+b,c)*in2(a,b)) = (g*in1(a+b,c))*in2(a,b) by A8,A9,A10,CAT_1:25
.= l*in2(a,b) by A7,A5,Def28
.= in2(a,b+c)*in1(b,c) by A3,A4,Def28;
then
A17: g*k = [$in2(a,b+c)*in1(b,c),g*in2(a+b,c)$] by A8,A11,A12,Th67
.= [$in2(a,b+c)*in1(b,c),in2(a,b+c)*in2(b,c)$] by A7,A5,Def28
.= in2(a,b+c)*[$in1(b,c),in2(b,c)$] by A2,A1,A6,Th67
.= in2(a,b+c)*id(b+c) by Th66
.= in2(a,b+c) by A1,CAT_1:29;
take f = [$in1(a+b,c)*in1(a,b),k$];
f*(in2(a,b+c)*in1(b,c)) = (f*in2(a,b+c))*in1(b,c) by A2,A1,A16,CAT_1:25
.= k*in1(b,c) by A15,A13,Def28
.= in1(a+b,c)*in2(a,b) by A11,A12,Def28;
then
A18: f*l = [$f*in1(a,b+c),in1(a+b,c)*in2(a,b)$] by A3,A4,A16,Th67
.= [$in1(a+b,c)*in1(a,b),in1(a+b,c)*in2(a,b)$] by A15,A13,Def28
.= in1(a+b,c)*[$in1(a,b),in2(a,b)$] by A14,A9,A10,Th67
.= in1(a+b,c)*id(a+b) by Th66
.= in1(a+b,c) by A9,CAT_1:29;
g*(in1(a+b,c)*in1(a,b)) = g*in1(a+b,c)*in1(a,b) by A8,A14,A9,CAT_1:25
.= l*in1(a,b) by A7,A5,Def28
.= in1(a,b+c) by A3,A4,Def28;
hence g*f = [$in1(a,b+c),in2(a,b+c)$] by A8,A15,A13,A17,Th67
.= id(a+(b+c)) by Th66;
f*(in2(a,b+c)*in2(b,c)) = (f*in2(a,b+c))*in2(b,c) by A1,A6,A16,CAT_1:25
.= k*in2(b,c) by A15,A13,Def28
.= in2(a+b,c) by A11,A12,Def28;
hence f*g = [$in1(a+b,c),in2(a+b,c)$] by A7,A5,A16,A18,Th67
.= id((a+b)+c) by Th66;
end;
definition
let C,a;
func nabla a -> Morphism of a+a,a equals
[$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
[$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 that
A1: Hom(a,c) <> {} and
A2: Hom(b,d) <> {};
Hom(d,c+d) <> {} by Th61;
then
A3: Hom(b,c+d) <> {} by A2,CAT_1:24;
Hom(c,c+d) <> {} by Th61;
then Hom(a,c+d) <> {} by A1,CAT_1:24;
hence thesis by A3,Th65;
end;
theorem
(id a)+(id b) = id(a+b)
proof
Hom(b,a+b) <> {} by Th61;
then
A1: in2(a,b)*(id b) = in2(a,b) by CAT_1:29;
Hom(a,a+b) <> {} by Th61;
then in1(a,b)*(id a) = in1(a,b) by CAT_1:29;
hence thesis by A1,Th66;
end;
theorem Th75:
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) <> {} & Hom(d,e) <> {};
A4: Hom(c+d,e) <> {} by A3,Th65;
A5: Hom(d,c+d) <> {} by Th61;
then
A6: Hom(b,c+d) <> {} by A2,CAT_1:24;
A7: Hom(c,c+d) <> {} by Th61;
then
A8: Hom(a,c+d) <> {} by A1,CAT_1:24;
[$g,k$]*in2(c,d) = k by A3,Def28;
then
A9: k*h = [$g,k$]*(in2(c,d)*h) by A2,A4,A5,CAT_1:25;
[$g,k$]*in1(c,d) = g by A3,Def28;
then g*f = [$g,k$]*(in1(c,d)*f) by A1,A4,A7,CAT_1:25;
hence thesis by A4,A8,A6,A9,Th67;
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) <> {};
Hom(c,c) <> {};
hence nabla(c)*(f+g) = [$(id c)*f,(id c)*g$] by A1,A2,Th75
.= [$f,(id c)*g$] by A1,CAT_1:28
.= [$f,g$] by A2,CAT_1:28;
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(s,e+s) <> {} by Th61;
then
A6: Hom(d,e+s) <> {} by A4,CAT_1:24;
A7: Hom(e,e+s) <> {} by Th61;
then in1(e,s)*g*f = in1(e,s)*(g*f) by A1,A3,CAT_1:25;
then
A8: (g*f)+(k*h) = [$in1(e,s)*g*f,in2(e,s)*k*h$] by A2,A4,A5,CAT_1:25;
Hom(c,e+s) <> {} by A3,A7,CAT_1:24;
hence thesis by A1,A2,A6,A8,Th75;
end;