:: CAT_4 semantic presentation
begin
definition
let C be Category;
let a, b be Object of C;
redefine pred a,b are_isomorphic means :: CAT_4:def 1
( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) );
compatibility
( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) ) by CAT_1:48;
end;
:: deftheorem defines are_isomorphic CAT_4:def_1_:_
for C being Category
for a, b being Object of C holds
( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) );
begin
definition
let C be Category;
attrC is with_finite_product means :: CAT_4:def 2
for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 );
end;
:: deftheorem defines with_finite_product CAT_4:def_2_:_
for C being Category holds
( C is with_finite_product iff for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 ) );
theorem Th1: :: CAT_4:1
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 ex 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; ::_thesis: ( 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 ex 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 ) ) ) )
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 ex 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 ) ) ) ) ::_thesis: ( ex a being Object of C st a is terminal & ( for a, b being Object of C ex c being Object of C ex 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 ) ) implies C is with_finite_product )
proof
reconsider F = {} as Function of {}, the carrier of C by RELSET_1:12;
assume A1: for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 ) ; :: according to CAT_4:def_2 ::_thesis: ( ex a being Object of C st a is terminal & ( for a, b being Object of C ex c being Object of C ex 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 ) ) )
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; ::_thesis: for a, b being Object of C ex c being Object of C ex 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 )
let a, b be Object of C; ::_thesis: ex c being Object of C ex 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 )
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 = (0,1) --> (a,b) and
A4: c is_a_product_wrt F9 by A1;
take c ; ::_thesis: ex 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 )
take p1 = F9 /. 0; ::_thesis: ex 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 )
take p2 = F9 /. 1; ::_thesis: ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 )
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; ::_thesis: ( cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 )
( ((0,1) --> (a,b)) /. 0 = a & ((0,1) --> (a,b)) /. 1 = b ) by CAT_3:3;
hence ( cod p1 = a & cod p2 = b ) by A3, A7, A5, CAT_3:def_2; ::_thesis: c is_a_product_wrt p1,p2
( dom F9 = {0,1} & p1 = F9 . 0 ) by A7, FUNCT_2:def_1, FUNCT_2:def_13;
then F9 = (0,1) --> (p1,p2) by A6, FUNCT_4:66;
hence c is_a_product_wrt p1,p2 by A4, CAT_3:54; ::_thesis: verum
end;
given a being Object of C such that A8: a is terminal ; ::_thesis: ( ex a, b being Object of C st
for c being Object of C
for p1, p2 being Morphism of C holds
( not dom p1 = c or not dom p2 = c or not cod p1 = a or not cod p2 = b or not c is_a_product_wrt p1,p2 ) or C is with_finite_product )
defpred S1[ Nat] means for I being finite set
for F being Function of I, the carrier of C st card I = $1 holds
ex a being Object of C ex 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 ex 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 ) ; ::_thesis: C is with_finite_product
A10: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A11: S1[n] ; ::_thesis: S1[n + 1]
let I be finite set ; ::_thesis: for F being Function of I, the carrier of C st card I = n + 1 holds
ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 )
let F be Function of I, the carrier of C; ::_thesis: ( card I = n + 1 implies ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 ) )
assume A12: card I = n + 1 ; ::_thesis: ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 )
set x = the Element of I;
reconsider Ix = I \ { the Element of I} as finite set ;
reconsider sx = { the Element of I} as finite set ;
reconsider G = F | (I \ { the Element of I}) as Function of (I \ { the Element of I}), the carrier of C by FUNCT_2:32;
card Ix = (card I) - (card sx) by CARD_2:44, A12, CARD_1:27, 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 \ { the Element of I} 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 /. the Element of I and
A19: c is_a_product_wrt p1,p2 by A9;
set F9 = (G9 * p1) +* ( the Element of I .--> p2);
A20: dom ({ the Element of I} --> p2) = { the Element of I} by FUNCT_2:def_1;
rng ((G9 * p1) +* ( the Element of I .--> p2)) c= (rng (G9 * p1)) \/ (rng ( the Element of I .--> p2)) by FUNCT_4:17;
then A21: rng ((G9 * p1) +* ( the Element of I .--> p2)) c= the carrier' of C by XBOOLE_1:1;
dom (G9 * p1) = I \ { the Element of I} by FUNCT_2:def_1;
then A22: (dom (G9 * p1)) \/ (dom ( the Element of I .--> p2)) = I \/ { the Element of I} by A20, XBOOLE_1:39
.= I by A12, CARD_1:27, ZFMISC_1:40 ;
then dom ((G9 * p1) +* ( the Element of I .--> p2)) = I by FUNCT_4:def_1;
then reconsider F9 = (G9 * p1) +* ( the Element of I .--> p2) as Function of I, the carrier' of C by A21, FUNCT_2:def_1, RELSET_1:4;
A23: doms G9 = (I \ { the Element of I}) --> a by CAT_3:def_13;
now__::_thesis:_for_y_being_set_st_y_in_I_holds_
(doms_F9)_._y_=_(I_-->_c)_._y
let y be set ; ::_thesis: ( y in I implies (doms F9) . y = (I --> c) . y )
assume A24: y in I ; ::_thesis: (doms F9) . y = (I --> c) . y
now__::_thesis:_(I_-->_c)_._y_=_(doms_F9)_/._y
percases ( y = the Element of I or y <> the Element of I ) ;
suppose y = the Element of I ; ::_thesis: (I --> c) . y = (doms F9) /. y
then A25: y in { the Element of I} by TARSKI:def_1;
F9 /. y = F9 . y by A24, FUNCT_2:def_13
.= ( the Element of I .--> 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 ;
::_thesis: verum
end;
supposeA26: y <> the Element of I ; ::_thesis: (doms F9) /. y = (I --> c) . y
then A27: not y in { the Element of I} by TARSKI:def_1;
A28: y in I \ { the Element of I} 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 \ { the Element of I}) --> c) /. y by A15, A17, A23, CAT_3:16
.= c by A24, A26, ZFMISC_1:56, CAT_3:2
.= (I --> c) . y by A24, FUNCOP_1:7 ;
::_thesis: verum
end;
end;
end;
hence (doms F9) . y = (I --> c) . y by A24, FUNCT_2:def_13; ::_thesis: verum
end;
then reconsider F9 = F9 as Projections_family of c,I by CAT_3:def_13, FUNCT_2:12;
take c ; ::_thesis: ex F9 being Projections_family of c,I st
( cods F9 = F & c is_a_product_wrt F9 )
take F9 ; ::_thesis: ( cods F9 = F & c is_a_product_wrt F9 )
B35: now__::_thesis:_for_y_being_set_st_y_in_I_holds_
(cods_F9)_/._y_=_F_/._y
let y be set ; ::_thesis: ( y in I implies (cods F9) /. y = F /. y )
assume A29: y in I ; ::_thesis: (cods F9) /. y = F /. y
now__::_thesis:_(cods_F9)_/._y_=_F_/._y
percases ( y = the Element of I or y <> the Element of I ) ;
supposeA30: y = the Element of I ; ::_thesis: (cods F9) /. y = F /. y
then A31: y in { the Element of I} by TARSKI:def_1;
F9 /. y = F9 . y by A29, FUNCT_2:def_13
.= ( the Element of I .--> p2) . y by A20, A31, FUNCT_4:13
.= p2 by A31, FUNCOP_1:7 ;
hence (cods F9) /. y = F /. y by A18, A29, A30, CAT_3:def_2; ::_thesis: verum
end;
supposeA32: y <> the Element of I ; ::_thesis: (cods F9) /. y = F /. y
then A33: not y in { the Element of I} by TARSKI:def_1;
A34: y in I \ { the Element of I} by A29, A32, ZFMISC_1:56;
F9 /. y = F9 . y by A29, FUNCT_2:def_13
.= (G9 * p1) . y by A20, A22, A29, A33, FUNCT_4:def_1
.= (G9 * p1) /. y by A34, FUNCT_2:def_13 ;
hence (cods F9) /. y = cod ((G9 * p1) /. y) by A29, CAT_3:def_2
.= (cods (G9 * p1)) /. y by A34, CAT_3:def_2
.= G /. y by A13, A17, A23, CAT_3:16
.= G . y by A34, FUNCT_2:def_13
.= F . y by A29, A32, ZFMISC_1:56, FUNCT_1:49
.= F /. y by A29, FUNCT_2:def_13 ;
::_thesis: verum
end;
end;
end;
hence (cods F9) /. y = F /. y ; ::_thesis: verum
end;
hence cods F9 = F by CAT_3:1; ::_thesis: c is_a_product_wrt F9
thus F9 is Projections_family of c,I ; :: according to CAT_3:def_14 ::_thesis: for b1 being Element of the carrier of C
for b2 being Projections_family of b1,I holds
( not cods F9 = cods b2 or ex b3 being Element of the carrier' of C st
( b3 in Hom (b1,c) & ( for b4 being Element of the carrier' of C holds
( not b4 in Hom (b1,c) or ( ( ex b5 being set st
( b5 in I & not (F9 /. b5) (*) b4 = b2 /. b5 ) or b3 = b4 ) & ( not b3 = b4 or for b5 being set holds
( not b5 in I or (F9 /. b5) (*) b4 = b2 /. b5 ) ) ) ) ) ) )
let d be Object of C; ::_thesis: for b1 being Projections_family of d,I holds
( not cods F9 = cods b1 or ex b2 being Element of the carrier' of C st
( b2 in Hom (d,c) & ( for b3 being Element of the carrier' of C holds
( not b3 in Hom (d,c) or ( ( ex b4 being set st
( b4 in I & not (F9 /. b4) (*) b3 = b1 /. b4 ) or b2 = b3 ) & ( not b2 = b3 or for b4 being set holds
( not b4 in I or (F9 /. b4) (*) b3 = b1 /. b4 ) ) ) ) ) ) )
let F99 be Projections_family of d,I; ::_thesis: ( not cods F9 = cods F99 or ex b1 being Element of the carrier' of C st
( b1 in Hom (d,c) & ( for b2 being Element of the carrier' of C holds
( not b2 in Hom (d,c) or ( ( ex b3 being set st
( b3 in I & not (F9 /. b3) (*) b2 = F99 /. b3 ) or b1 = b2 ) & ( not b1 = b2 or for b3 being set holds
( not b3 in I or (F9 /. b3) (*) b2 = F99 /. b3 ) ) ) ) ) ) )
assume A36: cods F9 = cods F99 ; ::_thesis: ex b1 being Element of the carrier' of C st
( b1 in Hom (d,c) & ( for b2 being Element of the carrier' of C holds
( not b2 in Hom (d,c) or ( ( ex b3 being set st
( b3 in I & not (F9 /. b3) (*) b2 = F99 /. b3 ) or b1 = b2 ) & ( not b1 = b2 or for b3 being set holds
( not b3 in I or (F9 /. b3) (*) b2 = F99 /. b3 ) ) ) ) ) )
reconsider G99 = F99 | (I \ { the Element of I}) as Function of (I \ { the Element of I}), the carrier' of C by FUNCT_2:32;
now__::_thesis:_for_y_being_set_st_y_in_I_\_{_the_Element_of_I}_holds_
(doms_G99)_/._y_=_((I_\_{_the_Element_of_I})_-->_d)_/._y
let y be set ; ::_thesis: ( y in I \ { the Element of I} implies (doms G99) /. y = ((I \ { the Element of I}) --> d) /. y )
assume A37: y in I \ { the Element of I} ; ::_thesis: (doms G99) /. y = ((I \ { the Element of I}) --> d) /. y
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 \ { the Element of I}) --> d) /. y by A37, CAT_3:2 ;
::_thesis: verum
end;
then reconsider G99 = G99 as Projections_family of d,I \ { the Element of I} by CAT_3:def_13, CAT_3:1;
now__::_thesis:_for_y_being_set_st_y_in_I_\_{_the_Element_of_I}_holds_
(cods_G9)_/._y_=_(cods_G99)_/._y
let y be set ; ::_thesis: ( y in I \ { the Element of I} implies (cods G9) /. y = (cods G99) /. y )
assume A38: y in I \ { the Element of I} ; ::_thesis: (cods G9) /. y = (cods G99) /. y
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, CAT_3:def_2, CAT_3:1, B35
.= (cods G99) /. y by A38, CAT_3:def_2 ;
::_thesis: verum
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 \ { the Element of I} holds
(G9 /. y) (*) k = G99 /. y ) iff h9 = k ) by A14, CAT_3:def_14, CAT_3:1;
A42: the Element of I in { the Element of I} by TARSKI:def_1;
set g = F99 /. the Element of I;
A43: dom (F99 /. the Element of I) = d by A12, CARD_1:27, CAT_3:41;
A44: F9 /. the Element of I = F9 . the Element of I by A12, CARD_1:27, FUNCT_2:def_13
.= ( the Element of I .--> p2) . the Element of I by A20, A42, FUNCT_4:13
.= p2 by A42, FUNCOP_1:7 ;
then cod p2 = (cods F9) /. the Element of I by A12, CARD_1:27, CAT_3:def_2
.= cod (F99 /. the Element of I) by A12, A36, CARD_1:27, CAT_3:def_2 ;
then F99 /. the Element of I 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 = F99 /. the Element of I ) iff h = k ) by A17, A19, A40, CAT_3:def_15;
take h ; ::_thesis: ( h in Hom (d,c) & ( for b1 being Element of the carrier' of C holds
( not b1 in Hom (d,c) or ( ( ex b2 being set st
( b2 in I & not (F9 /. b2) (*) b1 = F99 /. b2 ) or h = b1 ) & ( not h = b1 or for b2 being set holds
( not b2 in I or (F9 /. b2) (*) b1 = F99 /. b2 ) ) ) ) ) )
thus h in Hom (d,c) by A45; ::_thesis: for b1 being Element of the carrier' of C holds
( not b1 in Hom (d,c) or ( ( ex b2 being set st
( b2 in I & not (F9 /. b2) (*) b1 = F99 /. b2 ) or h = b1 ) & ( not h = b1 or for b2 being set holds
( not b2 in I or (F9 /. b2) (*) b1 = F99 /. b2 ) ) ) )
let k be Morphism of C; ::_thesis: ( not k in Hom (d,c) or ( ( ex b1 being set st
( b1 in I & not (F9 /. b1) (*) k = F99 /. b1 ) or h = k ) & ( not h = k or for b1 being set holds
( not b1 in I or (F9 /. b1) (*) k = F99 /. b1 ) ) ) )
assume A47: k in Hom (d,c) ; ::_thesis: ( ( ex b1 being set st
( b1 in I & not (F9 /. b1) (*) k = F99 /. b1 ) or h = k ) & ( not h = k or for b1 being set holds
( not b1 in I or (F9 /. b1) (*) k = F99 /. b1 ) ) )
thus ( ( for y being set st y in I holds
(F9 /. y) (*) k = F99 /. y ) implies h = k ) ::_thesis: ( not h = k or for b1 being set holds
( not b1 in I or (F9 /. b1) (*) k = F99 /. b1 ) )
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 ; ::_thesis: h = k
A51: for y being set st y in I \ { the Element of I} holds
(G9 /. y) (*) (p1 (*) k) = G99 /. y
proof
let y be set ; ::_thesis: ( y in I \ { the Element of I} implies (G9 /. y) (*) (p1 (*) k) = G99 /. y )
assume A52: y in I \ { the Element of I} ; ::_thesis: (G9 /. y) (*) (p1 (*) k) = G99 /. y
then A53: not y in { the Element of I} 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 ;
::_thesis: verum
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 = F99 /. the Element of I by A12, A44, A50, CARD_1:27;
hence h = k by A46, A47, A55; ::_thesis: verum
end;
assume A56: h = k ; ::_thesis: for b1 being set holds
( not b1 in I or (F9 /. b1) (*) k = F99 /. b1 )
let y be set ; ::_thesis: ( not y in I or (F9 /. y) (*) k = F99 /. y )
assume A57: y in I ; ::_thesis: (F9 /. y) (*) k = F99 /. y
now__::_thesis:_(F9_/._y)_(*)_k_=_F99_/._y
percases ( y = the Element of I or y <> the Element of I ) ;
supposeA58: y = the Element of I ; ::_thesis: (F9 /. y) (*) k = F99 /. y
then A59: y in { the Element of I} by TARSKI:def_1;
F9 /. y = F9 . y by A57, FUNCT_2:def_13
.= ( the Element of I .--> p2) . y by A20, A59, FUNCT_4:13
.= p2 by A59, FUNCOP_1:7 ;
hence (F9 /. y) (*) k = F99 /. y by A46, A47, A56, A58; ::_thesis: verum
end;
supposeA60: y <> the Element of I ; ::_thesis: (F9 /. y) (*) k = F99 /. y
then A61: not y in { the Element of I} by TARSKI:def_1;
A62: cod k = c by A47, CAT_1:1;
A63: y in I \ { the Element of I} by A57, A60, ZFMISC_1:56;
A64: dom (G9 /. y) = a by CAT_3:41, A57, A60, 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, ZFMISC_1:56, FUNCT_1:49
.= F99 /. y by A57, FUNCT_2:def_13 ;
::_thesis: verum
end;
end;
end;
hence (F9 /. y) (*) k = F99 /. y ; ::_thesis: verum
end;
let I be finite set ; :: according to CAT_4:def_2 ::_thesis: for F being Function of I, the carrier of C ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 )
let F be Function of I, the carrier of C; ::_thesis: ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 )
A65: card I = card I ;
A66: S1[ 0 ]
proof
let I be finite set ; ::_thesis: for F being Function of I, the carrier of C st card I = 0 holds
ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 )
let F be Function of I, the carrier of C; ::_thesis: ( card I = 0 implies ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 ) )
assume card I = 0 ; ::_thesis: ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 )
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 ; ::_thesis: ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 )
take F9 ; ::_thesis: ( cods F9 = F & a is_a_product_wrt F9 )
for x being set st x in I holds
(cods F9) /. x = F /. x ;
hence cods F9 = F by CAT_3:1; ::_thesis: a is_a_product_wrt F9
thus a is_a_product_wrt F9 by A8, A67, CAT_3:50; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A66, A10);
hence ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 ) by A65; ::_thesis: verum
end;
definition
attrc1 is strict ;
struct ProdCatStr -> CatStr ;
aggrProdCatStr(# carrier, carrier', Source, Target, Comp, TerminalObj, CatProd, Proj1, Proj2 #) -> ProdCatStr ;
sel TerminalObj c1 -> Element of the carrier of c1;
sel CatProd c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier of c1;
sel Proj1 c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier' of c1;
sel Proj2 c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier' of c1;
end;
registration
cluster non empty non void for ProdCatStr ;
existence
ex b1 being ProdCatStr st
( not b1 is void & not b1 is empty )
proof
set o = the set ;
take ProdCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) ; ::_thesis: ( not ProdCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is void & not ProdCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is empty )
thus ( not ProdCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is void & not ProdCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is empty ) ; ::_thesis: verum
end;
end;
definition
let C be non empty non void ProdCatStr ;
func [1] C -> Object of C equals :: CAT_4:def 3
the TerminalObj of C;
correctness
coherence
the TerminalObj of C is Object of C;
;
let a, b be Object of C;
funca [x] b -> Object of C equals :: CAT_4:def 4
the CatProd of C . (a,b);
correctness
coherence
the CatProd of C . (a,b) is Object of C;
;
func pr1 (a,b) -> Morphism of C equals :: CAT_4:def 5
the Proj1 of C . (a,b);
correctness
coherence
the Proj1 of C . (a,b) is Morphism of C;
;
func pr2 (a,b) -> Morphism of C equals :: CAT_4:def 6
the Proj2 of C . (a,b);
correctness
coherence
the Proj2 of C . (a,b) is Morphism of C;
;
end;
:: deftheorem defines [1] CAT_4:def_3_:_
for C being non empty non void ProdCatStr holds [1] C = the TerminalObj of C;
:: deftheorem defines [x] CAT_4:def_4_:_
for C being non empty non void ProdCatStr
for a, b being Object of C holds a [x] b = the CatProd of C . (a,b);
:: deftheorem defines pr1 CAT_4:def_5_:_
for C being non empty non void ProdCatStr
for a, b being Object of C holds pr1 (a,b) = the Proj1 of C . (a,b);
:: deftheorem defines pr2 CAT_4:def_6_:_
for C being non empty non void ProdCatStr
for a, b being Object of C holds pr2 (a,b) = the Proj2 of C . (a,b);
definition
let o, m be set ;
func c1Cat (o,m) -> strict ProdCatStr equals :: CAT_4:def 7
ProdCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #);
correctness
coherence
ProdCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) is strict ProdCatStr ;
;
end;
:: deftheorem defines c1Cat CAT_4:def_7_:_
for o, m being set holds c1Cat (o,m) = ProdCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #);
registration
let o, m be set ;
cluster c1Cat (o,m) -> non empty trivial non void trivial' strict ;
coherence
( not c1Cat (o,m) is empty & c1Cat (o,m) is trivial & not c1Cat (o,m) is void & c1Cat (o,m) is trivial' ) ;
end;
theorem :: CAT_4:2
for o, m being set holds CatStr(# the carrier of (c1Cat (o,m)), the carrier' of (c1Cat (o,m)), the Source of (c1Cat (o,m)), the Target of (c1Cat (o,m)), the Comp of (c1Cat (o,m)) #) = 1Cat (o,m) ;
Lm1a: for o, m being set holds c1Cat (o,m) is Category-like
proof
let o, m be set ; ::_thesis: c1Cat (o,m) is Category-like
set C = c1Cat (o,m);
set CP = the Comp of (c1Cat (o,m));
set CD = the Source of (c1Cat (o,m));
set CC = the Target of (c1Cat (o,m));
thus for f, g being Morphism of (c1Cat (o,m)) holds
( [g,f] in dom the Comp of (c1Cat (o,m)) iff dom g = cod f ) :: according to CAT_1:def_6 ::_thesis: verum
proof
let f, g be Morphism of (c1Cat (o,m)); ::_thesis: ( [g,f] in dom the Comp of (c1Cat (o,m)) iff dom g = cod f )
A1: dom the Comp of (c1Cat (o,m)) = {[m,m]} by FUNCOP_1:13;
( f = m & g = m ) by TARSKI:def_1;
hence ( [g,f] in dom the Comp of (c1Cat (o,m)) iff dom g = cod f ) by A1, TARSKI:def_1; ::_thesis: verum
end;
end;
registration
cluster non empty non void V57() Category-like transitive associative reflexive with_identities strict for ProdCatStr ;
existence
ex b1 being non empty non void ProdCatStr st
( b1 is strict & b1 is Category-like & b1 is reflexive & b1 is transitive & b1 is associative & b1 is with_identities & not b1 is void & not b1 is empty )
proof
( c1Cat (0,1) is Category-like & c1Cat (0,1) is transitive & c1Cat (0,1) is reflexive & c1Cat (0,1) is associative & c1Cat (0,1) is with_identities ) by Lm1a;
hence ex b1 being non empty non void ProdCatStr st
( b1 is strict & b1 is Category-like & b1 is reflexive & b1 is transitive & b1 is associative & b1 is with_identities & not b1 is void & not b1 is empty ) ; ::_thesis: verum
end;
end;
registration
let o, m be set ;
cluster c1Cat (o,m) -> non empty non void Category-like transitive associative reflexive with_identities strict ;
coherence
( c1Cat (o,m) is Category-like & c1Cat (o,m) is reflexive & c1Cat (o,m) is transitive & c1Cat (o,m) is associative & c1Cat (o,m) is with_identities & not c1Cat (o,m) is empty & not c1Cat (o,m) is void ) by Lm1a;
end;
theorem Th3: :: CAT_4:3
for o, m being set
for a, b being Object of (c1Cat (o,m)) holds a = b
proof
let o, m be set ; ::_thesis: for a, b being Object of (c1Cat (o,m)) holds a = b
let a, b be Object of (c1Cat (o,m)); ::_thesis: a = b
a = o by TARSKI:def_1;
hence a = b by TARSKI:def_1; ::_thesis: verum
end;
theorem Th4: :: CAT_4:4
for o, m being set
for f, g being Morphism of (c1Cat (o,m)) holds f = g
proof
let o, m be set ; ::_thesis: for f, g being Morphism of (c1Cat (o,m)) holds f = g
let f, g be Morphism of (c1Cat (o,m)); ::_thesis: f = g
f = m by TARSKI:def_1;
hence f = g by TARSKI:def_1; ::_thesis: verum
end;
theorem Th5: :: CAT_4:5
for o, m being set
for a, b being Object of (c1Cat (o,m))
for f being Morphism of (c1Cat (o,m)) holds f in Hom (a,b)
proof
let o, m be set ; ::_thesis: for a, b being Object of (c1Cat (o,m))
for f being Morphism of (c1Cat (o,m)) holds f in Hom (a,b)
let a, b be Object of (c1Cat (o,m)); ::_thesis: for f being Morphism of (c1Cat (o,m)) holds f in Hom (a,b)
let f be Morphism of (c1Cat (o,m)); ::_thesis: f in Hom (a,b)
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 f in Hom (a,b) by A1; ::_thesis: verum
end;
theorem :: CAT_4:6
for o, m being set
for a, b being Object of (c1Cat (o,m))
for f being Morphism of (c1Cat (o,m)) holds f is Morphism of a,b
proof
let o, m be set ; ::_thesis: for a, b being Object of (c1Cat (o,m))
for f being Morphism of (c1Cat (o,m)) holds f is Morphism of a,b
let a, b be Object of (c1Cat (o,m)); ::_thesis: for f being Morphism of (c1Cat (o,m)) holds f is Morphism of a,b
let f be Morphism of (c1Cat (o,m)); ::_thesis: f is Morphism of a,b
f in Hom (a,b) by Th5;
hence f is Morphism of a,b by CAT_1:def_5; ::_thesis: verum
end;
theorem :: CAT_4:7
for o, m being set
for a, b being Object of (c1Cat (o,m)) holds Hom (a,b) <> {} by Th5;
theorem Th8: :: CAT_4:8
for o, m being set
for a being Object of (c1Cat (o,m)) holds a is terminal
proof
let o, m be set ; ::_thesis: for a being Object of (c1Cat (o,m)) holds a is terminal
let a be Object of (c1Cat (o,m)); ::_thesis: a is terminal
let b be Object of (c1Cat (o,m)); :: according to CAT_1:def_18 ::_thesis: ( not Hom (b,a) = {} & ex b1 being Morphism of b,a st
for b2 being Morphism of b,a holds b1 = b2 )
set f = the Morphism of b,a;
thus Hom (b,a) <> {} by Th5; ::_thesis: ex b1 being Morphism of b,a st
for b2 being Morphism of b,a holds b1 = b2
take the Morphism of b,a ; ::_thesis: for b1 being Morphism of b,a holds the Morphism of b,a = b1
thus for b1 being Morphism of b,a holds the Morphism of b,a = b1 by Th4; ::_thesis: verum
end;
theorem Th9: :: CAT_4:9
for o, m being set
for c being Object of (c1Cat (o,m))
for p1, p2 being Morphism of (c1Cat (o,m)) holds c is_a_product_wrt p1,p2
proof
let o, m be set ; ::_thesis: for c being Object of (c1Cat (o,m))
for p1, p2 being Morphism of (c1Cat (o,m)) holds c is_a_product_wrt p1,p2
let c be Object of (c1Cat (o,m)); ::_thesis: for p1, p2 being Morphism of (c1Cat (o,m)) holds c is_a_product_wrt p1,p2
let p1, p2 be Morphism of (c1Cat (o,m)); ::_thesis: c is_a_product_wrt p1,p2
thus ( dom p1 = c & dom p2 = c ) by Th3; :: according to CAT_3:def_15 ::_thesis: for b1 being Element of the carrier of (c1Cat (o,m))
for b2, b3 being Element of the carrier' of (c1Cat (o,m)) holds
( not b2 in Hom (b1,(cod p1)) or not b3 in Hom (b1,(cod p2)) or ex b4 being Element of the carrier' of (c1Cat (o,m)) st
( b4 in Hom (b1,c) & ( for b5 being Element of the carrier' of (c1Cat (o,m)) holds
( not b5 in Hom (b1,c) or ( ( not p1 (*) b5 = b2 or not p2 (*) b5 = b3 or b4 = b5 ) & ( not b4 = b5 or ( p1 (*) b5 = b2 & p2 (*) b5 = b3 ) ) ) ) ) ) )
let d be Object of (c1Cat (o,m)); ::_thesis: for b1, b2 being Element of the carrier' of (c1Cat (o,m)) holds
( not b1 in Hom (d,(cod p1)) or not b2 in Hom (d,(cod p2)) or ex b3 being Element of the carrier' of (c1Cat (o,m)) st
( b3 in Hom (d,c) & ( for b4 being Element of the carrier' of (c1Cat (o,m)) holds
( not b4 in Hom (d,c) or ( ( not p1 (*) b4 = b1 or not p2 (*) b4 = b2 or b3 = b4 ) & ( not b3 = b4 or ( p1 (*) b4 = b1 & p2 (*) b4 = b2 ) ) ) ) ) ) )
let f, g be Morphism of (c1Cat (o,m)); ::_thesis: ( not f in Hom (d,(cod p1)) or not g in Hom (d,(cod p2)) or ex b1 being Element of the carrier' of (c1Cat (o,m)) st
( b1 in Hom (d,c) & ( for b2 being Element of the carrier' of (c1Cat (o,m)) holds
( not b2 in Hom (d,c) or ( ( not p1 (*) b2 = f or not p2 (*) b2 = g or b1 = b2 ) & ( not b1 = b2 or ( p1 (*) b2 = f & p2 (*) b2 = g ) ) ) ) ) ) )
assume that
f in Hom (d,(cod p1)) and
g in Hom (d,(cod p2)) ; ::_thesis: ex b1 being Element of the carrier' of (c1Cat (o,m)) st
( b1 in Hom (d,c) & ( for b2 being Element of the carrier' of (c1Cat (o,m)) holds
( not b2 in Hom (d,c) or ( ( not p1 (*) b2 = f or not p2 (*) b2 = g or b1 = b2 ) & ( not b1 = b2 or ( p1 (*) b2 = f & p2 (*) b2 = g ) ) ) ) ) )
take h = p1; ::_thesis: ( h in Hom (d,c) & ( for b1 being Element of the carrier' of (c1Cat (o,m)) holds
( not b1 in Hom (d,c) or ( ( not p1 (*) b1 = f or not p2 (*) b1 = g or h = b1 ) & ( not h = b1 or ( p1 (*) b1 = f & p2 (*) b1 = g ) ) ) ) ) )
thus h in Hom (d,c) by Th5; ::_thesis: for b1 being Element of the carrier' of (c1Cat (o,m)) holds
( not b1 in Hom (d,c) or ( ( not p1 (*) b1 = f or not p2 (*) b1 = g or h = b1 ) & ( not h = b1 or ( p1 (*) b1 = f & p2 (*) b1 = g ) ) ) )
thus for b1 being Element of the carrier' of (c1Cat (o,m)) holds
( not b1 in Hom (d,c) or ( ( not p1 (*) b1 = f or not p2 (*) b1 = g or h = b1 ) & ( not h = b1 or ( p1 (*) b1 = f & p2 (*) b1 = g ) ) ) ) by Th4; ::_thesis: verum
end;
definition
let IT be non empty non void Category-like transitive associative reflexive with_identities ProdCatStr ;
attrIT is Cartesian means :Def8: :: CAT_4:def 8
( 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;
:: deftheorem Def8 defines Cartesian CAT_4:def_8_:_
for IT being non empty non void Category-like transitive associative reflexive with_identities ProdCatStr holds
( IT is Cartesian iff ( 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) ) ) ) );
theorem Th10: :: CAT_4:10
for o, m being set holds c1Cat (o,m) is Cartesian
proof
let o, m be set ; ::_thesis: c1Cat (o,m) is Cartesian
set 1PCat = c1Cat (o,m);
thus the TerminalObj of (c1Cat (o,m)) is terminal by Th8; :: according to CAT_4:def_8 ::_thesis: for a, b being Object of (c1Cat (o,m)) holds
( cod ( the Proj1 of (c1Cat (o,m)) . (a,b)) = a & cod ( the Proj2 of (c1Cat (o,m)) . (a,b)) = b & the CatProd of (c1Cat (o,m)) . (a,b) is_a_product_wrt the Proj1 of (c1Cat (o,m)) . (a,b), the Proj2 of (c1Cat (o,m)) . (a,b) )
let a, b be Object of (c1Cat (o,m)); ::_thesis: ( cod ( the Proj1 of (c1Cat (o,m)) . (a,b)) = a & cod ( the Proj2 of (c1Cat (o,m)) . (a,b)) = b & the CatProd of (c1Cat (o,m)) . (a,b) is_a_product_wrt the Proj1 of (c1Cat (o,m)) . (a,b), the Proj2 of (c1Cat (o,m)) . (a,b) )
thus cod ( the Proj1 of (c1Cat (o,m)) . (a,b)) = a by Th3; ::_thesis: ( cod ( the Proj2 of (c1Cat (o,m)) . (a,b)) = b & the CatProd of (c1Cat (o,m)) . (a,b) is_a_product_wrt the Proj1 of (c1Cat (o,m)) . (a,b), the Proj2 of (c1Cat (o,m)) . (a,b) )
thus cod ( the Proj2 of (c1Cat (o,m)) . (a,b)) = b by Th3; ::_thesis: the CatProd of (c1Cat (o,m)) . (a,b) is_a_product_wrt the Proj1 of (c1Cat (o,m)) . (a,b), the Proj2 of (c1Cat (o,m)) . (a,b)
thus the CatProd of (c1Cat (o,m)) . (a,b) is_a_product_wrt the Proj1 of (c1Cat (o,m)) . (a,b), the Proj2 of (c1Cat (o,m)) . (a,b) by Th9; ::_thesis: verum
end;
registration
cluster non empty non void V57() Category-like transitive associative reflexive with_identities strict Cartesian for ProdCatStr ;
existence
ex b1 being non empty non void Category-like transitive associative reflexive with_identities ProdCatStr st
( b1 is strict & b1 is Cartesian )
proof
c1Cat (0,1) is Cartesian by Th10;
hence ex b1 being non empty non void Category-like transitive associative reflexive with_identities ProdCatStr st
( b1 is strict & b1 is Cartesian ) ; ::_thesis: verum
end;
end;
definition
mode Cartesian_category is non empty non void Category-like transitive associative reflexive with_identities Cartesian ProdCatStr ;
end;
theorem :: CAT_4:11
for C being Cartesian_category holds [1] C is terminal by Def8;
theorem Th12: :: CAT_4:12
for C being Cartesian_category
for a being Object of C
for f1, f2 being Morphism of a, [1] C holds f1 = f2
proof
let C be Cartesian_category; ::_thesis: for a being Object of C
for f1, f2 being Morphism of a, [1] C holds f1 = f2
let a be Object of C; ::_thesis: for f1, f2 being Morphism of a, [1] C holds f1 = f2
let f1, f2 be Morphism of a, [1] C; ::_thesis: f1 = f2
[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 by CAT_1:def_18;
thus f1 = f by A1
.= f2 by A1 ; ::_thesis: verum
end;
theorem Th13: :: CAT_4:13
for C being Cartesian_category
for a being Object of C holds Hom (a,([1] C)) <> {}
proof
let C be Cartesian_category; ::_thesis: for a being Object of C holds Hom (a,([1] C)) <> {}
let a be Object of C; ::_thesis: Hom (a,([1] C)) <> {}
[1] C is terminal by Def8;
hence Hom (a,([1] C)) <> {} by CAT_1:def_18; ::_thesis: verum
end;
definition
let C be Cartesian_category;
let a be Object of C;
func term a -> Morphism of a, [1] C means :: CAT_4:def 9
verum;
existence
ex b1 being Morphism of a, [1] C st verum ;
uniqueness
for b1, b2 being Morphism of a, [1] C holds b1 = b2 by Th12;
end;
:: deftheorem defines term CAT_4:def_9_:_
for C being Cartesian_category
for a being Object of C
for b3 being Morphism of a, [1] C holds
( b3 = term a iff verum );
theorem Th14: :: CAT_4:14
for C being Cartesian_category
for a being Object of C holds term a = term (a,([1] C))
proof
let C be Cartesian_category; ::_thesis: for a being Object of C holds term a = term (a,([1] C))
let a be Object of C; ::_thesis: term a = term (a,([1] C))
[1] C is terminal by Def8;
hence term a = term (a,([1] C)) by CAT_3:37; ::_thesis: verum
end;
theorem :: CAT_4:15
for C being Cartesian_category
for a being Object of C holds
( dom (term a) = a & cod (term a) = [1] C )
proof
let C be Cartesian_category; ::_thesis: for a being Object of C holds
( dom (term a) = a & cod (term a) = [1] C )
let a be Object of C; ::_thesis: ( dom (term a) = a & cod (term a) = [1] C )
( [1] C is terminal & term a = term (a,([1] C)) ) by Def8, Th14;
hence ( dom (term a) = a & cod (term a) = [1] C ) by CAT_3:35; ::_thesis: verum
end;
theorem :: CAT_4:16
for C being Cartesian_category
for a being Object of C holds Hom (a,([1] C)) = {(term a)}
proof
let C be Cartesian_category; ::_thesis: for a being Object of C holds Hom (a,([1] C)) = {(term a)}
let a be Object of C; ::_thesis: Hom (a,([1] C)) = {(term a)}
for f2 being Morphism of a, [1] C holds term a = f2 by Th12;
hence Hom (a,([1] C)) = {(term a)} by Th13, CAT_1:8; ::_thesis: verum
end;
theorem Th17: :: CAT_4:17
for C being Cartesian_category
for a, b being Object of C holds
( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a )
proof
let C be Cartesian_category; ::_thesis: for a, b being Object of C holds
( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a )
let a, b be Object of C; ::_thesis: ( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a )
set p1 = the Proj1 of C . (a,b);
set p2 = the Proj2 of C . (a,b);
a [x] b is_a_product_wrt the Proj1 of C . (a,b), the Proj2 of C . (a,b) by Def8;
hence ( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a ) by Def8, CAT_3:def_15; ::_thesis: verum
end;
theorem Th18: :: CAT_4:18
for C being Cartesian_category
for a, b being Object of C holds
( dom (pr2 (a,b)) = a [x] b & cod (pr2 (a,b)) = b )
proof
let C be Cartesian_category; ::_thesis: for a, b being Object of C holds
( dom (pr2 (a,b)) = a [x] b & cod (pr2 (a,b)) = b )
let a, b be Object of C; ::_thesis: ( dom (pr2 (a,b)) = a [x] b & cod (pr2 (a,b)) = b )
set p1 = the Proj1 of C . (a,b);
set p2 = the Proj2 of C . (a,b);
a [x] b is_a_product_wrt the Proj1 of C . (a,b), the Proj2 of C . (a,b) by Def8;
hence ( dom (pr2 (a,b)) = a [x] b & cod (pr2 (a,b)) = b ) by Def8, CAT_3:def_15; ::_thesis: verum
end;
definition
let C be Cartesian_category;
let a, b be Object of C;
:: original: pr1
redefine func pr1 (a,b) -> Morphism of a [x] b,a;
coherence
pr1 (a,b) is Morphism of a [x] b,a
proof
( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a ) by Th17;
hence pr1 (a,b) is Morphism of a [x] b,a by CAT_1:4; ::_thesis: verum
end;
:: original: pr2
redefine func pr2 (a,b) -> Morphism of a [x] b,b;
coherence
pr2 (a,b) is Morphism of a [x] b,b
proof
( dom (pr2 (a,b)) = a [x] b & cod (pr2 (a,b)) = b ) by Th18;
hence pr2 (a,b) is Morphism of a [x] b,b by CAT_1:4; ::_thesis: verum
end;
end;
theorem Th19: :: CAT_4:19
for C being Cartesian_category
for a, b being Object of C holds
( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} )
proof
let C be Cartesian_category; ::_thesis: for a, b being Object of C holds
( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} )
let a, b be Object of C; ::_thesis: ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} )
set c = the CatProd of C . (a,b);
set p1 = the Proj1 of C . (a,b);
set p2 = the Proj2 of C . (a,b);
the CatProd of C . (a,b) is_a_product_wrt the Proj1 of C . (a,b), the Proj2 of C . (a,b) by Def8;
then A1: ( dom ( the Proj1 of C . (a,b)) = the CatProd of C . (a,b) & dom ( the Proj2 of C . (a,b)) = the CatProd of C . (a,b) ) by CAT_3:def_15;
( cod ( the Proj1 of C . (a,b)) = a & cod ( the Proj2 of C . (a,b)) = b ) by Def8;
hence ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by A1, CAT_1:1; ::_thesis: verum
end;
theorem :: CAT_4:20
for C being Cartesian_category
for a, b being Object of C holds a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) by Def8;
theorem :: CAT_4:21
for C being Cartesian_category holds C is with_finite_product
proof
let C be Cartesian_category; ::_thesis: C is with_finite_product
A1: for a, b being Object of C ex c being Object of C ex 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 be Object of C; ::_thesis: ex c being Object of C ex 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 )
take a [x] b ; ::_thesis: ex p1, p2 being Morphism of C st
( dom p1 = a [x] b & dom p2 = a [x] b & cod p1 = a & cod p2 = b & a [x] b is_a_product_wrt p1,p2 )
take pr1 (a,b) ; ::_thesis: ex p2 being Morphism of C st
( dom (pr1 (a,b)) = a [x] b & dom p2 = a [x] b & cod (pr1 (a,b)) = a & cod p2 = b & a [x] b is_a_product_wrt pr1 (a,b),p2 )
take pr2 (a,b) ; ::_thesis: ( dom (pr1 (a,b)) = a [x] b & dom (pr2 (a,b)) = a [x] b & cod (pr1 (a,b)) = a & cod (pr2 (a,b)) = b & a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) )
thus ( dom (pr1 (a,b)) = a [x] b & dom (pr2 (a,b)) = a [x] b & cod (pr1 (a,b)) = a & cod (pr2 (a,b)) = b & a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) ) by Def8, Th17, Th18; ::_thesis: verum
end;
[1] C is terminal by Def8;
hence C is with_finite_product by A1, Th1; ::_thesis: verum
end;
theorem :: CAT_4:22
for C being Cartesian_category
for a, b being Object of C st Hom (a,b) <> {} & Hom (b,a) <> {} holds
( pr1 (a,b) is retraction & pr2 (a,b) is retraction )
proof
let C be Cartesian_category; ::_thesis: for a, b being Object of C st Hom (a,b) <> {} & Hom (b,a) <> {} holds
( pr1 (a,b) is retraction & pr2 (a,b) is retraction )
let a, b be Object of C; ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} implies ( pr1 (a,b) is retraction & pr2 (a,b) is retraction ) )
X: ( 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 ( Hom (a,b) <> {} & Hom (b,a) <> {} implies ( pr1 (a,b) is retraction & pr2 (a,b) is retraction ) ) by X, CAT_3:57; ::_thesis: verum
end;
definition
let C be Cartesian_category;
let a, b, c be Object of C;
let f be Morphism of c,a;
let 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: :: CAT_4:def 10
( (pr1 (a,b)) * it = f & (pr2 (a,b)) * it = g );
existence
ex b1 being Morphism of c,a [x] b st
( (pr1 (a,b)) * b1 = f & (pr2 (a,b)) * b1 = g )
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 ; ::_thesis: ( (pr1 (a,b)) * h = f & (pr2 (a,b)) * h = g )
thus ( (pr1 (a,b)) * h = f & (pr2 (a,b)) * h = g ) by A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Morphism of c,a [x] b st (pr1 (a,b)) * b1 = f & (pr2 (a,b)) * b1 = g & (pr1 (a,b)) * b2 = f & (pr2 (a,b)) * b2 = g holds
b1 = b2
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; ::_thesis: ( (pr1 (a,b)) * h1 = f & (pr2 (a,b)) * h1 = g & (pr1 (a,b)) * h2 = f & (pr2 (a,b)) * h2 = g implies h1 = h2 )
assume that
A6: ( (pr1 (a,b)) * h1 = f & (pr2 (a,b)) * h1 = g ) and
A7: ( (pr1 (a,b)) * h2 = f & (pr2 (a,b)) * h2 = g ) ; ::_thesis: h1 = h2
h1 = h by A6, A5;
hence h1 = h2 by A7, A5; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines <: CAT_4:def_10_:_
for C being Cartesian_category
for a, b, c being Object of C
for f being Morphism of c,a
for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
for b7 being Morphism of c,a [x] b holds
( b7 = <:f,g:> iff ( (pr1 (a,b)) * b7 = f & (pr2 (a,b)) * b7 = g ) );
theorem Th23: :: CAT_4:23
for C being Cartesian_category
for c, a, b being Object of C st Hom (c,a) <> {} & Hom (c,b) <> {} holds
Hom (c,(a [x] b)) <> {}
proof
let C be Cartesian_category; ::_thesis: for c, a, b being Object of C st Hom (c,a) <> {} & Hom (c,b) <> {} holds
Hom (c,(a [x] b)) <> {}
let c, a, b be Object of C; ::_thesis: ( Hom (c,a) <> {} & Hom (c,b) <> {} implies Hom (c,(a [x] b)) <> {} )
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 ( Hom (c,a) <> {} & Hom (c,b) <> {} implies Hom (c,(a [x] b)) <> {} ) by A1, CAT_3:55; ::_thesis: verum
end;
theorem Th24: :: CAT_4:24
for C being Cartesian_category
for a, b being Object of C holds <:(pr1 (a,b)),(pr2 (a,b)):> = id (a [x] b)
proof
let C be Cartesian_category; ::_thesis: for a, b being Object of C holds <:(pr1 (a,b)),(pr2 (a,b)):> = id (a [x] b)
let a, b be Object of C; ::_thesis: <:(pr1 (a,b)),(pr2 (a,b)):> = id (a [x] b)
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 <:(pr1 (a,b)),(pr2 (a,b)):> = id (a [x] b) by A3, A1, A2, Def10; ::_thesis: verum
end;
theorem Th25: :: CAT_4:25
for C being Cartesian_category
for c, a, b, d being Object of C
for f being Morphism of c,a
for g being Morphism of c,b
for 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 C be Cartesian_category; ::_thesis: for c, a, b, d being Object of C
for f being Morphism of c,a
for g being Morphism of c,b
for h being Morphism of d,c st Hom (c,a) <> {} & Hom (c,b) <> {} & Hom (d,c) <> {} holds
<:(f * h),(g * h):> = <:f,g:> * h
let c, a, b, d be Object of C; ::_thesis: for f being Morphism of c,a
for g being Morphism of c,b
for h being Morphism of d,c st Hom (c,a) <> {} & Hom (c,b) <> {} & Hom (d,c) <> {} holds
<:(f * h),(g * h):> = <:f,g:> * h
let f be Morphism of c,a; ::_thesis: for g being Morphism of c,b
for h being Morphism of d,c st Hom (c,a) <> {} & Hom (c,b) <> {} & Hom (d,c) <> {} holds
<:(f * h),(g * h):> = <:f,g:> * h
let g be Morphism of c,b; ::_thesis: for h being Morphism of d,c st Hom (c,a) <> {} & Hom (c,b) <> {} & Hom (d,c) <> {} holds
<:(f * h),(g * h):> = <:f,g:> * h
let h be Morphism of d,c; ::_thesis: ( Hom (c,a) <> {} & Hom (c,b) <> {} & Hom (d,c) <> {} implies <:(f * h),(g * h):> = <:f,g:> * h )
assume that
A1: ( Hom (c,a) <> {} & Hom (c,b) <> {} ) and
A2: Hom (d,c) <> {} ; ::_thesis: <:(f * h),(g * h):> = <:f,g:> * h
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 <:(f * h),(g * h):> = <:f,g:> * h by A5, A7, Def10; ::_thesis: verum
end;
theorem Th26: :: CAT_4:26
for C being Cartesian_category
for c, a, b being Object of C
for f, k being Morphism of c,a
for 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 C be Cartesian_category; ::_thesis: for c, a, b being Object of C
for f, k being Morphism of c,a
for g, h being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & <:f,g:> = <:k,h:> holds
( f = k & g = h )
let c, a, b be Object of C; ::_thesis: for f, k being Morphism of c,a
for g, h being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & <:f,g:> = <:k,h:> holds
( f = k & g = h )
let f, k be Morphism of c,a; ::_thesis: for g, h being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & <:f,g:> = <:k,h:> holds
( f = k & g = h )
let g, h be Morphism of c,b; ::_thesis: ( Hom (c,a) <> {} & Hom (c,b) <> {} & <:f,g:> = <:k,h:> implies ( f = k & g = h ) )
assume A1: ( Hom (c,a) <> {} & Hom (c,b) <> {} ) ; ::_thesis: ( not <:f,g:> = <:k,h:> or ( f = k & g = h ) )
then ( (pr1 (a,b)) * <:f,g:> = f & (pr2 (a,b)) * <:f,g:> = g ) by Def10;
hence ( not <:f,g:> = <:k,h:> or ( f = k & g = h ) ) by A1, Def10; ::_thesis: verum
end;
theorem :: CAT_4:27
for C being Cartesian_category
for c, a, b being Object of C
for f being Morphism of c,a
for 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 C be Cartesian_category; ::_thesis: for c, a, b being Object of C
for f being Morphism of c,a
for 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
let c, a, b be Object of C; ::_thesis: for f being Morphism of c,a
for 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
let f be Morphism of c,a; ::_thesis: for 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
let g be Morphism of c,b; ::_thesis: ( Hom (c,a) <> {} & Hom (c,b) <> {} & ( f is monic or g is monic ) implies <:f,g:> is monic )
assume that
A1: Hom (c,a) <> {} and
A2: Hom (c,b) <> {} and
A3: ( f is monic or g is monic ) ; ::_thesis: <:f,g:> is monic
A4: now__::_thesis:_(_g_is_monic_implies_for_d_being_Object_of_C
for_f1,_f2_being_Morphism_of_d,c_st_Hom_(d,c)_<>_{}_&_<:f,g:>_*_f1_=_<:f,g:>_*_f2_holds_
f1_=_f2_)
assume A5: g is monic ; ::_thesis: for d being Object of C
for f1, f2 being Morphism of d,c st Hom (d,c) <> {} & <:f,g:> * f1 = <:f,g:> * f2 holds
f1 = f2
let d be Object of C; ::_thesis: for f1, f2 being Morphism of d,c st Hom (d,c) <> {} & <:f,g:> * f1 = <:f,g:> * f2 holds
f1 = f2
let f1, f2 be Morphism of d,c; ::_thesis: ( Hom (d,c) <> {} & <:f,g:> * f1 = <:f,g:> * f2 implies f1 = f2 )
assume that
A6: Hom (d,c) <> {} and
A7: <:f,g:> * f1 = <:f,g:> * f2 ; ::_thesis: f1 = 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 A2, A5, A6, CAT_1:31; ::_thesis: verum
end;
A9: now__::_thesis:_(_f_is_monic_implies_for_d_being_Object_of_C
for_f1,_f2_being_Morphism_of_d,c_st_Hom_(d,c)_<>_{}_&_<:f,g:>_*_f1_=_<:f,g:>_*_f2_holds_
f1_=_f2_)
assume A10: f is monic ; ::_thesis: for d being Object of C
for f1, f2 being Morphism of d,c st Hom (d,c) <> {} & <:f,g:> * f1 = <:f,g:> * f2 holds
f1 = f2
let d be Object of C; ::_thesis: for f1, f2 being Morphism of d,c st Hom (d,c) <> {} & <:f,g:> * f1 = <:f,g:> * f2 holds
f1 = f2
let f1, f2 be Morphism of d,c; ::_thesis: ( Hom (d,c) <> {} & <:f,g:> * f1 = <:f,g:> * f2 implies f1 = f2 )
assume that
A11: Hom (d,c) <> {} and
A12: <:f,g:> * f1 = <:f,g:> * f2 ; ::_thesis: f1 = 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 A1, A10, A11, CAT_1:31; ::_thesis: verum
end;
Hom (c,(a [x] b)) <> {} by A1, A2, Th23;
hence <:f,g:> is monic by A3, A9, A4, CAT_1:31; ::_thesis: verum
end;
theorem Th28: :: CAT_4:28
for C being Cartesian_category
for a being Object of C holds
( Hom (a,(a [x] ([1] C))) <> {} & Hom (a,(([1] C) [x] a)) <> {} )
proof
let C be Cartesian_category; ::_thesis: for a being Object of C holds
( Hom (a,(a [x] ([1] C))) <> {} & Hom (a,(([1] C) [x] a)) <> {} )
let a be Object of C; ::_thesis: ( Hom (a,(a [x] ([1] C))) <> {} & Hom (a,(([1] C) [x] a)) <> {} )
( Hom (a,([1] C)) <> {} & Hom (a,a) <> {} ) by Th13;
hence ( Hom (a,(a [x] ([1] C))) <> {} & Hom (a,(([1] C) [x] a)) <> {} ) by Th23; ::_thesis: verum
end;
definition
let C be Cartesian_category;
let a be Object of C;
func lambda a -> Morphism of ([1] C) [x] a,a equals :: CAT_4:def 11
pr2 (([1] C),a);
correctness
coherence
pr2 (([1] C),a) is Morphism of ([1] C) [x] a,a;
;
func lambda' a -> Morphism of a,([1] C) [x] a equals :: CAT_4:def 12
<:(term a),(id a):>;
correctness
coherence
<:(term a),(id a):> is Morphism of a,([1] C) [x] a;
;
func rho a -> Morphism of a [x] ([1] C),a equals :: CAT_4:def 13
pr1 (a,([1] C));
correctness
coherence
pr1 (a,([1] C)) is Morphism of a [x] ([1] C),a;
;
func rho' a -> Morphism of a,a [x] ([1] C) equals :: CAT_4:def 14
<:(id a),(term a):>;
correctness
coherence
<:(id a),(term a):> is Morphism of a,a [x] ([1] C);
;
end;
:: deftheorem defines lambda CAT_4:def_11_:_
for C being Cartesian_category
for a being Object of C holds lambda a = pr2 (([1] C),a);
:: deftheorem defines lambda' CAT_4:def_12_:_
for C being Cartesian_category
for a being Object of C holds lambda' a = <:(term a),(id a):>;
:: deftheorem defines rho CAT_4:def_13_:_
for C being Cartesian_category
for a being Object of C holds rho a = pr1 (a,([1] C));
:: deftheorem defines rho' CAT_4:def_14_:_
for C being Cartesian_category
for a being Object of C holds rho' a = <:(id a),(term a):>;
theorem Th29: :: CAT_4:29
for C being Cartesian_category
for a being Object of C holds
( (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
let C be Cartesian_category; ::_thesis: for a being Object of C holds
( (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)) )
let a be Object of C; ::_thesis: ( (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)) )
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; ::_thesis: ( (lambda' a) * (lambda a) = id (([1] C) [x] a) & (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) )
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; ::_thesis: ( (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) )
thus id a = (rho a) * (rho' a) by A2, Def10; ::_thesis: (rho' a) * (rho a) = id (a [x] ([1] C))
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 (rho' a) * (rho a) = id (a [x] ([1] C)) by Th24; ::_thesis: verum
end;
theorem :: CAT_4:30
for C being Cartesian_category
for a being Object of C holds
( a,a [x] ([1] C) are_isomorphic & a,([1] C) [x] a are_isomorphic )
proof
let C be Cartesian_category; ::_thesis: for a being Object of C holds
( a,a [x] ([1] C) are_isomorphic & a,([1] C) [x] a are_isomorphic )
let a be Object of C; ::_thesis: ( a,a [x] ([1] C) are_isomorphic & a,([1] C) [x] a are_isomorphic )
thus a,a [x] ([1] C) are_isomorphic ::_thesis: a,([1] C) [x] a are_isomorphic
proof
thus ( Hom (a,(a [x] ([1] C))) <> {} & Hom ((a [x] ([1] C)),a) <> {} ) by Th19, Th28; :: according to CAT_4:def_1 ::_thesis: ex f being Morphism of a,a [x] ([1] C) ex f9 being Morphism of a [x] ([1] C),a st
( f * f9 = id (a [x] ([1] C)) & f9 * f = id a )
take rho' a ; ::_thesis: ex f9 being Morphism of a [x] ([1] C),a st
( (rho' a) * f9 = id (a [x] ([1] C)) & f9 * (rho' a) = id a )
take rho a ; ::_thesis: ( (rho' a) * (rho a) = id (a [x] ([1] C)) & (rho a) * (rho' a) = id a )
thus ( (rho' a) * (rho a) = id (a [x] ([1] C)) & (rho a) * (rho' a) = id a ) by Th29; ::_thesis: verum
end;
thus ( Hom (a,(([1] C) [x] a)) <> {} & Hom ((([1] C) [x] a),a) <> {} ) by Th19, Th28; :: according to CAT_4:def_1 ::_thesis: ex f being Morphism of a,([1] C) [x] a ex f9 being Morphism of ([1] C) [x] a,a st
( f * f9 = id (([1] C) [x] a) & f9 * f = id a )
take lambda' a ; ::_thesis: ex f9 being Morphism of ([1] C) [x] a,a st
( (lambda' a) * f9 = id (([1] C) [x] a) & f9 * (lambda' a) = id a )
take lambda a ; ::_thesis: ( (lambda' a) * (lambda a) = id (([1] C) [x] a) & (lambda a) * (lambda' a) = id a )
thus ( (lambda' a) * (lambda a) = id (([1] C) [x] a) & (lambda a) * (lambda' a) = id a ) by Th29; ::_thesis: verum
end;
definition
let C be Cartesian_category;
let a, b be Object of C;
func Switch (a,b) -> Morphism of a [x] b,b [x] a equals :: CAT_4:def 15
<:(pr2 (a,b)),(pr1 (a,b)):>;
correctness
coherence
<:(pr2 (a,b)),(pr1 (a,b)):> is Morphism of a [x] b,b [x] a;
;
end;
:: deftheorem defines Switch CAT_4:def_15_:_
for C being Cartesian_category
for a, b being Object of C holds Switch (a,b) = <:(pr2 (a,b)),(pr1 (a,b)):>;
theorem Th31: :: CAT_4:31
for C being Cartesian_category
for a, b being Object of C holds Hom ((a [x] b),(b [x] a)) <> {}
proof
let C be Cartesian_category; ::_thesis: for a, b being Object of C holds Hom ((a [x] b),(b [x] a)) <> {}
let a, b be Object of C; ::_thesis: Hom ((a [x] b),(b [x] a)) <> {}
( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by Th19;
hence Hom ((a [x] b),(b [x] a)) <> {} by Th23; ::_thesis: verum
end;
theorem Th32: :: CAT_4:32
for C being Cartesian_category
for a, b being Object of C holds (Switch (a,b)) * (Switch (b,a)) = id (b [x] a)
proof
let C be Cartesian_category; ::_thesis: for a, b being Object of C holds (Switch (a,b)) * (Switch (b,a)) = id (b [x] a)
let a, b be Object of C; ::_thesis: (Switch (a,b)) * (Switch (b,a)) = id (b [x] a)
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 ;
::_thesis: verum
end;
theorem :: CAT_4:33
for C being Cartesian_category
for a, b being Object of C holds a [x] b,b [x] a are_isomorphic
proof
let C be Cartesian_category; ::_thesis: for a, b being Object of C holds a [x] b,b [x] a are_isomorphic
let a, b be Object of C; ::_thesis: a [x] b,b [x] a are_isomorphic
thus ( Hom ((a [x] b),(b [x] a)) <> {} & Hom ((b [x] a),(a [x] b)) <> {} ) by Th31; :: according to CAT_4:def_1 ::_thesis: ex f being Morphism of a [x] b,b [x] a ex f9 being Morphism of b [x] a,a [x] b st
( f * f9 = id (b [x] a) & f9 * f = id (a [x] b) )
take Switch (a,b) ; ::_thesis: ex f9 being Morphism of b [x] a,a [x] b st
( (Switch (a,b)) * f9 = id (b [x] a) & f9 * (Switch (a,b)) = id (a [x] b) )
take Switch (b,a) ; ::_thesis: ( (Switch (a,b)) * (Switch (b,a)) = id (b [x] a) & (Switch (b,a)) * (Switch (a,b)) = id (a [x] b) )
thus ( (Switch (a,b)) * (Switch (b,a)) = id (b [x] a) & (Switch (b,a)) * (Switch (a,b)) = id (a [x] b) ) by Th32; ::_thesis: verum
end;
definition
let C be Cartesian_category;
let a be Object of C;
func Delta a -> Morphism of a,a [x] a equals :: CAT_4:def 16
<:(id a),(id a):>;
correctness
coherence
<:(id a),(id a):> is Morphism of a,a [x] a;
;
end;
:: deftheorem defines Delta CAT_4:def_16_:_
for C being Cartesian_category
for a being Object of C holds Delta a = <:(id a),(id a):>;
theorem :: CAT_4:34
for C being Cartesian_category
for a being Object of C holds Hom (a,(a [x] a)) <> {}
proof
let C be Cartesian_category; ::_thesis: for a being Object of C holds Hom (a,(a [x] a)) <> {}
let a be Object of C; ::_thesis: Hom (a,(a [x] a)) <> {}
Hom (a,a) <> {} ;
hence Hom (a,(a [x] a)) <> {} by Th23; ::_thesis: verum
end;
theorem :: CAT_4:35
for C being Cartesian_category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
<:f,f:> = (Delta b) * f
proof
let C be Cartesian_category; ::_thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
<:f,f:> = (Delta b) * f
let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds
<:f,f:> = (Delta b) * f
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies <:f,f:> = (Delta b) * f )
assume A1: Hom (a,b) <> {} ; ::_thesis: <:f,f:> = (Delta b) * f
( Hom (b,b) <> {} & (id b) * f = f ) by A1, CAT_1:28;
hence <:f,f:> = (Delta b) * f by A1, Th25; ::_thesis: verum
end;
definition
let C be Cartesian_category;
let a, b, c be Object of C;
func Alpha (a,b,c) -> Morphism of (a [x] b) [x] c,a [x] (b [x] c) equals :: CAT_4:def 17
<:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>;
correctness
coherence
<:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:> is Morphism of (a [x] b) [x] c,a [x] (b [x] c);
;
func Alpha' (a,b,c) -> Morphism of a [x] (b [x] c),(a [x] b) [x] c equals :: CAT_4:def 18
<:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>;
correctness
coherence
<:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):> is Morphism of a [x] (b [x] c),(a [x] b) [x] c;
;
end;
:: deftheorem defines Alpha CAT_4:def_17_:_
for C being Cartesian_category
for a, b, c being Object of C holds Alpha (a,b,c) = <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>;
:: deftheorem defines Alpha' CAT_4:def_18_:_
for C being Cartesian_category
for a, b, c being Object of C holds Alpha' (a,b,c) = <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>;
theorem Th36: :: CAT_4:36
for C being Cartesian_category
for a, b, c being Object of C holds
( Hom (((a [x] b) [x] c),(a [x] (b [x] c))) <> {} & Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {} )
proof
let C be Cartesian_category; ::_thesis: for a, b, c being Object of C holds
( Hom (((a [x] b) [x] c),(a [x] (b [x] c))) <> {} & Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {} )
let a, b, c be Object of C; ::_thesis: ( Hom (((a [x] b) [x] c),(a [x] (b [x] c))) <> {} & Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {} )
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; ::_thesis: Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {}
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 Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {} by A5, Th23; ::_thesis: verum
end;
theorem Th37: :: CAT_4:37
for C being Cartesian_category
for a, b, c being Object of C holds
( (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
let C be Cartesian_category; ::_thesis: for a, b, c being Object of C holds
( (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) )
let a, b, c be Object of C; ::_thesis: ( (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) )
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))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>;
set g = <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((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))) * <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):> = (pr2 (a,b)) * ((pr1 ((a [x] b),c)) * <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>) by A1, A2, CAT_1:25
.= (pr2 (a,b)) * <:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):> by A10, A14, Def10
.= (pr1 (b,c)) * (pr2 (a,(b [x] c))) by A12, A13, Def10 ;
then A16: <:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):> * <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):> = <:((pr1 (b,c)) * (pr2 (a,(b [x] c)))),((pr2 ((a [x] b),c)) * <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>):> 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)))) * <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:> = (pr1 (b,c)) * ((pr2 (a,(b [x] c))) * <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>) by A11, A8, CAT_1:25
.= (pr1 (b,c)) * <:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):> by A7, A5, Def10
.= (pr2 (a,b)) * (pr1 ((a [x] b),c)) by A3, A4, Def10 ;
then A18: <:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):> * <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:> = <:((pr1 (a,(b [x] c))) * <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>),((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))) * <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):> = (pr1 (a,b)) * ((pr1 ((a [x] b),c)) * <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>) by A6, A1, A15, CAT_1:25
.= (pr1 (a,b)) * <:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):> 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 ;
::_thesis: (Alpha' (a,b,c)) * (Alpha (a,b,c)) = id ((a [x] b) [x] c)
((pr2 (b,c)) * (pr2 (a,(b [x] c)))) * <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:> = (pr2 (b,c)) * ((pr2 (a,(b [x] c))) * <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>) by A17, A8, A9, CAT_1:25
.= (pr2 (b,c)) * <:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):> 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 ;
::_thesis: verum
end;
theorem :: CAT_4:38
for C being Cartesian_category
for a, b, c being Object of C holds (a [x] b) [x] c,a [x] (b [x] c) are_isomorphic
proof
let C be Cartesian_category; ::_thesis: for a, b, c being Object of C holds (a [x] b) [x] c,a [x] (b [x] c) are_isomorphic
let a, b, c be Object of C; ::_thesis: (a [x] b) [x] c,a [x] (b [x] c) are_isomorphic
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; :: according to CAT_4:def_1 ::_thesis: ex f being Morphism of (a [x] b) [x] c,a [x] (b [x] c) ex f9 being Morphism of a [x] (b [x] c),(a [x] b) [x] c st
( f * f9 = id (a [x] (b [x] c)) & f9 * f = id ((a [x] b) [x] c) )
take Alpha (a,b,c) ; ::_thesis: ex f9 being Morphism of a [x] (b [x] c),(a [x] b) [x] c st
( (Alpha (a,b,c)) * f9 = id (a [x] (b [x] c)) & f9 * (Alpha (a,b,c)) = id ((a [x] b) [x] c) )
take Alpha' (a,b,c) ; ::_thesis: ( (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) )
thus ( (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) ) by Th37; ::_thesis: verum
end;
definition
let C be Cartesian_category;
let a, b, c, d be Object of C;
let f be Morphism of a,b;
let g be Morphism of c,d;
funcf [x] g -> Morphism of a [x] c,b [x] d equals :: CAT_4:def 19
<:(f * (pr1 (a,c))),(g * (pr2 (a,c))):>;
correctness
coherence
<:(f * (pr1 (a,c))),(g * (pr2 (a,c))):> is Morphism of a [x] c,b [x] d;
;
end;
:: deftheorem defines [x] CAT_4:def_19_:_
for C being Cartesian_category
for a, b, c, d being Object of C
for f being Morphism of a,b
for g being Morphism of c,d holds f [x] g = <:(f * (pr1 (a,c))),(g * (pr2 (a,c))):>;
theorem :: CAT_4:39
for C being Cartesian_category
for a, c, b, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds
Hom ((a [x] b),(c [x] d)) <> {}
proof
let C be Cartesian_category; ::_thesis: for a, c, b, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds
Hom ((a [x] b),(c [x] d)) <> {}
let a, c, b, d be Object of C; ::_thesis: ( Hom (a,c) <> {} & Hom (b,d) <> {} implies Hom ((a [x] b),(c [x] d)) <> {} )
assume that
A1: Hom (a,c) <> {} and
A2: Hom (b,d) <> {} ; ::_thesis: Hom ((a [x] b),(c [x] 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 Hom ((a [x] b),(c [x] d)) <> {} by A3, Th23; ::_thesis: verum
end;
theorem :: CAT_4:40
for C being Cartesian_category
for a, b being Object of C holds (id a) [x] (id b) = id (a [x] b)
proof
let C be Cartesian_category; ::_thesis: for a, b being Object of C holds (id a) [x] (id b) = id (a [x] b)
let a, b be Object of C; ::_thesis: (id a) [x] (id b) = id (a [x] b)
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 (id a) [x] (id b) = id (a [x] b) by A1, Th24; ::_thesis: verum
end;
theorem Th41: :: CAT_4:41
for C being Cartesian_category
for a, b, c, d, e being Object of C
for f being Morphism of a,b
for h being Morphism of c,d
for g being Morphism of e,a
for 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 C be Cartesian_category; ::_thesis: for a, b, c, d, e being Object of C
for f being Morphism of a,b
for h being Morphism of c,d
for g being Morphism of e,a
for 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):>
let a, b, c, d, e be Object of C; ::_thesis: for f being Morphism of a,b
for h being Morphism of c,d
for g being Morphism of e,a
for 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):>
let f be Morphism of a,b; ::_thesis: for h being Morphism of c,d
for g being Morphism of e,a
for 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):>
let h be Morphism of c,d; ::_thesis: for g being Morphism of e,a
for 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):>
let g be Morphism of e,a; ::_thesis: for 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):>
let k be Morphism of e,c; ::_thesis: ( Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (e,c) <> {} implies (f [x] h) * <:g,k:> = <:(f * g),(h * k):> )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (c,d) <> {} and
A3: ( Hom (e,a) <> {} & Hom (e,c) <> {} ) ; ::_thesis: (f [x] h) * <:g,k:> = <:(f * g),(h * k):>
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 (f [x] h) * <:g,k:> = <:(f * g),(h * k):> by A4, A8, A6, A9, Th25; ::_thesis: verum
end;
theorem :: CAT_4:42
for C being Cartesian_category
for c, a, b being Object of C
for f being Morphism of c,a
for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
<:f,g:> = (f [x] g) * (Delta c)
proof
let C be Cartesian_category; ::_thesis: for c, a, b being Object of C
for f being Morphism of c,a
for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
<:f,g:> = (f [x] g) * (Delta c)
let c, a, b be Object of C; ::_thesis: for f being Morphism of c,a
for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
<:f,g:> = (f [x] g) * (Delta c)
let f be Morphism of c,a; ::_thesis: for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
<:f,g:> = (f [x] g) * (Delta c)
let g be Morphism of c,b; ::_thesis: ( Hom (c,a) <> {} & Hom (c,b) <> {} implies <:f,g:> = (f [x] g) * (Delta c) )
assume that
A1: Hom (c,a) <> {} and
A2: Hom (c,b) <> {} ; ::_thesis: <:f,g:> = (f [x] g) * (Delta c)
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 ;
::_thesis: verum
end;
theorem :: CAT_4:43
for C being Cartesian_category
for a, b, c, d, e, s being Object of C
for f being Morphism of a,b
for h being Morphism of c,d
for g being Morphism of e,a
for 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 C be Cartesian_category; ::_thesis: for a, b, c, d, e, s being Object of C
for f being Morphism of a,b
for h being Morphism of c,d
for g being Morphism of e,a
for 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)
let a, b, c, d, e, s be Object of C; ::_thesis: for f being Morphism of a,b
for h being Morphism of c,d
for g being Morphism of e,a
for 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)
let f be Morphism of a,b; ::_thesis: for h being Morphism of c,d
for g being Morphism of e,a
for 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)
let h be Morphism of c,d; ::_thesis: for g being Morphism of e,a
for 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)
let g be Morphism of e,a; ::_thesis: for 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)
let k be Morphism of s,c; ::_thesis: ( Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} implies (f [x] h) * (g [x] k) = (f * g) [x] (h * k) )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (c,d) <> {} and
A3: Hom (e,a) <> {} and
A4: Hom (s,c) <> {} ; ::_thesis: (f [x] h) * (g [x] k) = (f * g) [x] (h * k)
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 (f [x] h) * (g [x] k) = (f * g) [x] (h * k) by A1, A2, A6, A8, Th41; ::_thesis: verum
end;
begin
definition
let C be Category;
attrC is with_finite_coproduct means :: CAT_4:def 20
for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 );
end;
:: deftheorem defines with_finite_coproduct CAT_4:def_20_:_
for C being Category holds
( C is with_finite_coproduct iff for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 ) );
theorem Th44: :: CAT_4:44
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 ex 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; ::_thesis: ( 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 ex 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 ) ) ) )
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 ex 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 ) ) ) ) ::_thesis: ( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex 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 ) ) implies C is with_finite_coproduct )
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
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 ) ; :: according to CAT_4:def_20 ::_thesis: ( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex 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 ) ) )
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 CAT_3:75, A3; ::_thesis: for a, b being Object of C ex c being Object of C ex 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 )
let a, b be Object of C; ::_thesis: ex c being Object of C ex 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 )
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 = (0,1) --> (a,b) and
A5: c is_a_coproduct_wrt F9 by A2;
take c ; ::_thesis: ex 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 )
take i1 = F9 /. 0; ::_thesis: ex 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 )
take i2 = F9 /. 1; ::_thesis: ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 )
A6: 1 in {0,1} by TARSKI:def_2;
then A7: i2 = F9 . 1 by FUNCT_2:def_13;
( ((0,1) --> (a,b)) /. 0 = a & ((0,1) --> (a,b)) /. 1 = b ) by CAT_3:3;
hence ( dom i1 = a & dom i2 = b ) by A4, A1, A6, CAT_3:def_1; ::_thesis: ( cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 )
thus ( cod i1 = c & cod i2 = c ) by A1, A6, CAT_3:62; ::_thesis: c is_a_coproduct_wrt i1,i2
( dom F9 = {0,1} & i1 = F9 . 0 ) by A1, FUNCT_2:def_1, FUNCT_2:def_13;
then F9 = (0,1) --> (i1,i2) by A7, FUNCT_4:66;
hence c is_a_coproduct_wrt i1,i2 by A5, CAT_3:79; ::_thesis: verum
end;
given a being Object of C such that A8: a is initial ; ::_thesis: ( ex a, b being Object of C st
for c being Object of C
for i1, i2 being Morphism of C holds
( not dom i1 = a or not dom i2 = b or not cod i1 = c or not cod i2 = c or not c is_a_coproduct_wrt i1,i2 ) or C is with_finite_coproduct )
defpred S1[ Nat] means for I being finite set
for F being Function of I, the carrier of C st card I = $1 holds
ex a being Object of C ex 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 ex 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 ) ; ::_thesis: C is with_finite_coproduct
A10: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A11: S1[n] ; ::_thesis: S1[n + 1]
let I be finite set ; ::_thesis: for F being Function of I, the carrier of C st card I = n + 1 holds
ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
let F be Function of I, the carrier of C; ::_thesis: ( card I = n + 1 implies ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 ) )
assume A12: card I = n + 1 ; ::_thesis: ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
set x = the Element of I;
reconsider Ix = I \ { the Element of I} as finite set ;
reconsider sx = { the Element of I} as finite set ;
reconsider G = F | (I \ { the Element of I}) as Function of (I \ { the Element of I}), the carrier of C by FUNCT_2:32;
card Ix = (card I) - (card sx) by CARD_2:44, A12, CARD_1:27, 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 \ { the Element of I} such that
A13: doms G9 = G and
A14: a is_a_coproduct_wrt G9 by A11;
set b = F /. the Element of I;
consider c being Object of C, i1, i2 being Morphism of C such that
A15: dom i1 = a and
A16: dom i2 = F /. the Element of I 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) +* ( the Element of I .--> i2);
A20: dom ({ the Element of I} --> i2) = { the Element of I} by FUNCT_2:def_1;
rng ((i1 * G9) +* ( the Element of I .--> i2)) c= (rng (i1 * G9)) \/ (rng ( the Element of I .--> i2)) by FUNCT_4:17;
then A21: rng ((i1 * G9) +* ( the Element of I .--> i2)) c= the carrier' of C by XBOOLE_1:1;
dom (i1 * G9) = I \ { the Element of I} by FUNCT_2:def_1;
then A22: (dom (i1 * G9)) \/ (dom ( the Element of I .--> i2)) = I \/ { the Element of I} by A20, XBOOLE_1:39
.= I by A12, CARD_1:27, ZFMISC_1:40 ;
then dom ((i1 * G9) +* ( the Element of I .--> i2)) = I by FUNCT_4:def_1;
then reconsider F9 = (i1 * G9) +* ( the Element of I .--> i2) as Function of I, the carrier' of C by A21, FUNCT_2:def_1, RELSET_1:4;
A23: cods G9 = (I \ { the Element of I}) --> a by CAT_3:def_16;
now__::_thesis:_for_y_being_set_st_y_in_I_holds_
(cods_F9)_._y_=_(I_-->_c)_._y
let y be set ; ::_thesis: ( y in I implies (cods F9) . y = (I --> c) . y )
assume A24: y in I ; ::_thesis: (cods F9) . y = (I --> c) . y
now__::_thesis:_(I_-->_c)_._y_=_(cods_F9)_/._y
percases ( y = the Element of I or y <> the Element of I ) ;
suppose y = the Element of I ; ::_thesis: (I --> c) . y = (cods F9) /. y
then A25: y in { the Element of I} by TARSKI:def_1;
F9 /. y = F9 . y by A24, FUNCT_2:def_13
.= ( the Element of I .--> 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 ;
::_thesis: verum
end;
supposeA26: y <> the Element of I ; ::_thesis: (cods F9) /. y = (I --> c) . y
then A27: not y in { the Element of I} by TARSKI:def_1;
A28: y in I \ { the Element of I} 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 \ { the Element of I}) --> c) /. y by A15, A17, A23, CAT_3:17
.= c by A24, A26, ZFMISC_1:56, CAT_3:2
.= (I --> c) . y by A24, FUNCOP_1:7 ;
::_thesis: verum
end;
end;
end;
hence (cods F9) . y = (I --> c) . y by A24, FUNCT_2:def_13; ::_thesis: verum
end;
then reconsider F9 = F9 as Injections_family of c,I by CAT_3:def_16, FUNCT_2:12;
take c ; ::_thesis: ex F9 being Injections_family of c,I st
( doms F9 = F & c is_a_coproduct_wrt F9 )
take F9 ; ::_thesis: ( doms F9 = F & c is_a_coproduct_wrt F9 )
B35: now__::_thesis:_for_y_being_set_st_y_in_I_holds_
(doms_F9)_/._y_=_F_/._y
let y be set ; ::_thesis: ( y in I implies (doms F9) /. y = F /. y )
assume A29: y in I ; ::_thesis: (doms F9) /. y = F /. y
now__::_thesis:_(doms_F9)_/._y_=_F_/._y
percases ( y = the Element of I or y <> the Element of I ) ;
supposeA30: y = the Element of I ; ::_thesis: (doms F9) /. y = F /. y
then A31: y in { the Element of I} by TARSKI:def_1;
F9 /. y = F9 . y by A29, FUNCT_2:def_13
.= ( the Element of I .--> i2) . y by A20, A31, FUNCT_4:13
.= i2 by A31, FUNCOP_1:7 ;
hence (doms F9) /. y = F /. y by A16, A29, A30, CAT_3:def_1; ::_thesis: verum
end;
supposeA32: y <> the Element of I ; ::_thesis: (doms F9) /. y = F /. y
then A33: not y in { the Element of I} by TARSKI:def_1;
A34: y in I \ { the Element of I} by A29, A32, ZFMISC_1:56;
F9 /. y = F9 . y by A29, FUNCT_2:def_13
.= (i1 * G9) . y by A20, A22, A29, A33, FUNCT_4:def_1
.= (i1 * G9) /. y by A34, FUNCT_2:def_13 ;
hence (doms F9) /. y = dom ((i1 * G9) /. y) by A29, CAT_3:def_1
.= (doms (i1 * G9)) /. y by A34, CAT_3:def_1
.= G /. y by A13, A15, A23, CAT_3:17
.= G . y by A34, FUNCT_2:def_13
.= F . y by A29, A32, ZFMISC_1:56, FUNCT_1:49
.= F /. y by A29, FUNCT_2:def_13 ;
::_thesis: verum
end;
end;
end;
hence (doms F9) /. y = F /. y ; ::_thesis: verum
end;
hence doms F9 = F by CAT_3:1; ::_thesis: c is_a_coproduct_wrt F9
thus F9 is Injections_family of c,I ; :: according to CAT_3:def_17 ::_thesis: for b1 being Element of the carrier of C
for b2 being Injections_family of b1,I holds
( not doms F9 = doms b2 or ex b3 being Element of the carrier' of C st
( b3 in Hom (c,b1) & ( for b4 being Element of the carrier' of C holds
( not b4 in Hom (c,b1) or ( ( ex b5 being set st
( b5 in I & not b4 (*) (F9 /. b5) = b2 /. b5 ) or b3 = b4 ) & ( not b3 = b4 or for b5 being set holds
( not b5 in I or b4 (*) (F9 /. b5) = b2 /. b5 ) ) ) ) ) ) )
let d be Object of C; ::_thesis: for b1 being Injections_family of d,I holds
( not doms F9 = doms b1 or ex b2 being Element of the carrier' of C st
( b2 in Hom (c,d) & ( for b3 being Element of the carrier' of C holds
( not b3 in Hom (c,d) or ( ( ex b4 being set st
( b4 in I & not b3 (*) (F9 /. b4) = b1 /. b4 ) or b2 = b3 ) & ( not b2 = b3 or for b4 being set holds
( not b4 in I or b3 (*) (F9 /. b4) = b1 /. b4 ) ) ) ) ) ) )
let F99 be Injections_family of d,I; ::_thesis: ( not doms F9 = doms F99 or ex b1 being Element of the carrier' of C st
( b1 in Hom (c,d) & ( for b2 being Element of the carrier' of C holds
( not b2 in Hom (c,d) or ( ( ex b3 being set st
( b3 in I & not b2 (*) (F9 /. b3) = F99 /. b3 ) or b1 = b2 ) & ( not b1 = b2 or for b3 being set holds
( not b3 in I or b2 (*) (F9 /. b3) = F99 /. b3 ) ) ) ) ) ) )
assume A36: doms F9 = doms F99 ; ::_thesis: ex b1 being Element of the carrier' of C st
( b1 in Hom (c,d) & ( for b2 being Element of the carrier' of C holds
( not b2 in Hom (c,d) or ( ( ex b3 being set st
( b3 in I & not b2 (*) (F9 /. b3) = F99 /. b3 ) or b1 = b2 ) & ( not b1 = b2 or for b3 being set holds
( not b3 in I or b2 (*) (F9 /. b3) = F99 /. b3 ) ) ) ) ) )
reconsider G99 = F99 | (I \ { the Element of I}) as Function of (I \ { the Element of I}), the carrier' of C by FUNCT_2:32;
now__::_thesis:_for_y_being_set_st_y_in_I_\_{_the_Element_of_I}_holds_
(cods_G99)_/._y_=_((I_\_{_the_Element_of_I})_-->_d)_/._y
let y be set ; ::_thesis: ( y in I \ { the Element of I} implies (cods G99) /. y = ((I \ { the Element of I}) --> d) /. y )
assume A37: y in I \ { the Element of I} ; ::_thesis: (cods G99) /. y = ((I \ { the Element of I}) --> d) /. y
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 \ { the Element of I}) --> d) /. y by A37, CAT_3:2 ;
::_thesis: verum
end;
then reconsider G99 = G99 as Injections_family of d,I \ { the Element of I} by CAT_3:def_16, CAT_3:1;
now__::_thesis:_for_y_being_set_st_y_in_I_\_{_the_Element_of_I}_holds_
(doms_G9)_/._y_=_(doms_G99)_/._y
let y be set ; ::_thesis: ( y in I \ { the Element of I} implies (doms G9) /. y = (doms G99) /. y )
assume A38: y in I \ { the Element of I} ; ::_thesis: (doms G9) /. y = (doms G99) /. y
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, B35, A36, A38, A39, CAT_3:def_1, CAT_3:1
.= (doms G99) /. y by A38, CAT_3:def_1 ;
::_thesis: verum
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 \ { the Element of I} holds
k (*) (G9 /. y) = G99 /. y ) iff h9 = k ) by A14, CAT_3:def_17, CAT_3:1;
A42: the Element of I in { the Element of I} by TARSKI:def_1;
set g = F99 /. the Element of I;
A43: cod (F99 /. the Element of I) = d by A12, CARD_1:27, CAT_3:62;
A44: F9 /. the Element of I = F9 . the Element of I by A12, CARD_1:27, FUNCT_2:def_13
.= ( the Element of I .--> i2) . the Element of I by A20, A42, FUNCT_4:13
.= i2 by A42, FUNCOP_1:7 ;
then dom i2 = (doms F9) /. the Element of I by A12, CARD_1:27, CAT_3:def_1
.= dom (F99 /. the Element of I) by A12, A36, CARD_1:27, CAT_3:def_1 ;
then F99 /. the Element of I 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 = F99 /. the Element of I ) iff h = k ) by A15, A19, A40, CAT_3:def_18;
take h ; ::_thesis: ( h in Hom (c,d) & ( for b1 being Element of the carrier' of C holds
( not b1 in Hom (c,d) or ( ( ex b2 being set st
( b2 in I & not b1 (*) (F9 /. b2) = F99 /. b2 ) or h = b1 ) & ( not h = b1 or for b2 being set holds
( not b2 in I or b1 (*) (F9 /. b2) = F99 /. b2 ) ) ) ) ) )
thus h in Hom (c,d) by A45; ::_thesis: for b1 being Element of the carrier' of C holds
( not b1 in Hom (c,d) or ( ( ex b2 being set st
( b2 in I & not b1 (*) (F9 /. b2) = F99 /. b2 ) or h = b1 ) & ( not h = b1 or for b2 being set holds
( not b2 in I or b1 (*) (F9 /. b2) = F99 /. b2 ) ) ) )
let k be Morphism of C; ::_thesis: ( not k in Hom (c,d) or ( ( ex b1 being set st
( b1 in I & not k (*) (F9 /. b1) = F99 /. b1 ) or h = k ) & ( not h = k or for b1 being set holds
( not b1 in I or k (*) (F9 /. b1) = F99 /. b1 ) ) ) )
assume A47: k in Hom (c,d) ; ::_thesis: ( ( ex b1 being set st
( b1 in I & not k (*) (F9 /. b1) = F99 /. b1 ) or h = k ) & ( not h = k or for b1 being set holds
( not b1 in I or k (*) (F9 /. b1) = F99 /. b1 ) ) )
thus ( ( for y being set st y in I holds
k (*) (F9 /. y) = F99 /. y ) implies h = k ) ::_thesis: ( not h = k or for b1 being set holds
( not b1 in I or k (*) (F9 /. b1) = F99 /. b1 ) )
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 ; ::_thesis: h = k
A51: for y being set st y in I \ { the Element of I} holds
(k (*) i1) (*) (G9 /. y) = G99 /. y
proof
let y be set ; ::_thesis: ( y in I \ { the Element of I} implies (k (*) i1) (*) (G9 /. y) = G99 /. y )
assume A52: y in I \ { the Element of I} ; ::_thesis: (k (*) i1) (*) (G9 /. y) = G99 /. y
then A53: not y in { the Element of I} 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 ;
::_thesis: verum
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 = F99 /. the Element of I by A12, A44, A50, CARD_1:27;
hence h = k by A46, A47, A55; ::_thesis: verum
end;
assume A56: h = k ; ::_thesis: for b1 being set holds
( not b1 in I or k (*) (F9 /. b1) = F99 /. b1 )
let y be set ; ::_thesis: ( not y in I or k (*) (F9 /. y) = F99 /. y )
assume A57: y in I ; ::_thesis: k (*) (F9 /. y) = F99 /. y
now__::_thesis:_k_(*)_(F9_/._y)_=_F99_/._y
percases ( y = the Element of I or y <> the Element of I ) ;
supposeA58: y = the Element of I ; ::_thesis: k (*) (F9 /. y) = F99 /. y
then A59: y in { the Element of I} by TARSKI:def_1;
F9 /. y = F9 . y by A57, FUNCT_2:def_13
.= ( the Element of I .--> i2) . y by A20, A59, FUNCT_4:13
.= i2 by A59, FUNCOP_1:7 ;
hence k (*) (F9 /. y) = F99 /. y by A46, A47, A56, A58; ::_thesis: verum
end;
supposeA60: y <> the Element of I ; ::_thesis: k (*) (F9 /. y) = F99 /. y
then A61: not y in { the Element of I} by TARSKI:def_1;
A62: dom k = c by A47, CAT_1:1;
A63: y in I \ { the Element of I} by A57, A60, ZFMISC_1:56;
A64: cod (G9 /. y) = a by CAT_3:62, A57, A60, 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, ZFMISC_1:56, FUNCT_1:49
.= F99 /. y by A57, FUNCT_2:def_13 ;
::_thesis: verum
end;
end;
end;
hence k (*) (F9 /. y) = F99 /. y ; ::_thesis: verum
end;
let I be finite set ; :: according to CAT_4:def_20 ::_thesis: for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
let F be Function of I, the carrier of C; ::_thesis: ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
A65: card I = card I ;
A66: S1[ 0 ]
proof
let I be finite set ; ::_thesis: for F being Function of I, the carrier of C st card I = 0 holds
ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
let F be Function of I, the carrier of C; ::_thesis: ( card I = 0 implies ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 ) )
assume card I = 0 ; ::_thesis: ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
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 ; ::_thesis: ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
take F9 ; ::_thesis: ( doms F9 = F & a is_a_coproduct_wrt F9 )
for x being set st x in I holds
(doms F9) /. x = F /. x ;
hence doms F9 = F by CAT_3:1; ::_thesis: a is_a_coproduct_wrt F9
thus a is_a_coproduct_wrt F9 by A8, A67, CAT_3:75; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A66, A10);
hence ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 ) by A65; ::_thesis: verum
end;
definition
attrc1 is strict ;
struct CoprodCatStr -> CatStr ;
aggrCoprodCatStr(# carrier, carrier', Source, Target, Comp, Initial, Coproduct, Incl1, Incl2 #) -> CoprodCatStr ;
sel Initial c1 -> Element of the carrier of c1;
sel Coproduct c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier of c1;
sel Incl1 c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier' of c1;
sel Incl2 c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier' of c1;
end;
registration
cluster non empty non void for CoprodCatStr ;
existence
ex b1 being CoprodCatStr st
( not b1 is void & not b1 is empty )
proof
set o = the set ;
take CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) ; ::_thesis: ( not CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is void & not CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is empty )
thus ( not CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is void & not CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is empty ) ; ::_thesis: verum
end;
end;
definition
let C be non empty non void CoprodCatStr ;
func [[0]] C -> Object of C equals :: CAT_4:def 21
the Initial of C;
correctness
coherence
the Initial of C is Object of C;
;
let a, b be Object of C;
funca + b -> Object of C equals :: CAT_4:def 22
the Coproduct of C . (a,b);
correctness
coherence
the Coproduct of C . (a,b) is Object of C;
;
func in1 (a,b) -> Morphism of C equals :: CAT_4:def 23
the Incl1 of C . (a,b);
correctness
coherence
the Incl1 of C . (a,b) is Morphism of C;
;
func in2 (a,b) -> Morphism of C equals :: CAT_4:def 24
the Incl2 of C . (a,b);
correctness
coherence
the Incl2 of C . (a,b) is Morphism of C;
;
end;
:: deftheorem defines [[0]] CAT_4:def_21_:_
for C being non empty non void CoprodCatStr holds [[0]] C = the Initial of C;
:: deftheorem defines + CAT_4:def_22_:_
for C being non empty non void CoprodCatStr
for a, b being Object of C holds a + b = the Coproduct of C . (a,b);
:: deftheorem defines in1 CAT_4:def_23_:_
for C being non empty non void CoprodCatStr
for a, b being Object of C holds in1 (a,b) = the Incl1 of C . (a,b);
:: deftheorem defines in2 CAT_4:def_24_:_
for C being non empty non void CoprodCatStr
for a, b being Object of C holds in2 (a,b) = the Incl2 of C . (a,b);
definition
let o, m be set ;
func c1Cat* (o,m) -> strict CoprodCatStr equals :: CAT_4:def 25
CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #);
correctness
coherence
CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) is strict CoprodCatStr ;
;
end;
:: deftheorem defines c1Cat* CAT_4:def_25_:_
for o, m being set holds c1Cat* (o,m) = CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #);
theorem :: CAT_4:45
canceled;
registration
let o, m be set ;
cluster c1Cat* (o,m) -> non empty trivial non void trivial' strict ;
coherence
( not c1Cat* (o,m) is void & not c1Cat* (o,m) is empty & c1Cat* (o,m) is trivial & c1Cat* (o,m) is trivial' ) ;
end;
Lm2a: for o, m being set holds c1Cat* (o,m) is Category-like
proof
let o, m be set ; ::_thesis: c1Cat* (o,m) is Category-like
set C = c1Cat* (o,m);
set CP = the Comp of (c1Cat* (o,m));
set CD = the Source of (c1Cat* (o,m));
set CC = the Target of (c1Cat* (o,m));
thus for f, g being Morphism of (c1Cat* (o,m)) holds
( [g,f] in dom the Comp of (c1Cat* (o,m)) iff dom g = cod f ) :: according to CAT_1:def_6 ::_thesis: verum
proof
let f, g be Morphism of (c1Cat* (o,m)); ::_thesis: ( [g,f] in dom the Comp of (c1Cat* (o,m)) iff dom g = cod f )
A1: dom the Comp of (c1Cat* (o,m)) = {[m,m]} by FUNCOP_1:13;
Y: ( f = m & g = m ) by TARSKI:def_1;
thus ( [g,f] in dom the Comp of (c1Cat* (o,m)) implies dom g = cod f ) by ZFMISC_1:def_10; ::_thesis: ( dom g = cod f implies [g,f] in dom the Comp of (c1Cat* (o,m)) )
thus ( dom g = cod f implies [g,f] in dom the Comp of (c1Cat* (o,m)) ) by A1, Y, TARSKI:def_1; ::_thesis: verum
end;
end;
registration
cluster non empty non void V57() Category-like transitive associative reflexive with_identities strict for CoprodCatStr ;
existence
ex b1 being non empty non void CoprodCatStr st
( b1 is strict & b1 is Category-like & b1 is reflexive & b1 is transitive & b1 is associative & b1 is with_identities )
proof
( c1Cat* (0,1) is reflexive & c1Cat* (0,1) is transitive & c1Cat* (0,1) is associative & c1Cat* (0,1) is with_identities & c1Cat* (0,1) is Category-like ) by Lm2a;
hence ex b1 being non empty non void CoprodCatStr st
( b1 is strict & b1 is Category-like & b1 is reflexive & b1 is transitive & b1 is associative & b1 is with_identities ) ; ::_thesis: verum
end;
end;
registration
let o, m be set ;
cluster c1Cat* (o,m) -> non empty non void Category-like transitive associative reflexive with_identities strict ;
coherence
( c1Cat* (o,m) is Category-like & c1Cat* (o,m) is reflexive & c1Cat* (o,m) is transitive & c1Cat* (o,m) is associative & c1Cat* (o,m) is with_identities & not c1Cat* (o,m) is void & not c1Cat* (o,m) is empty ) by Lm2a;
end;
theorem Th46: :: CAT_4:46
for o, m being set
for a, b being Object of (c1Cat* (o,m)) holds a = b
proof
let o, m be set ; ::_thesis: for a, b being Object of (c1Cat* (o,m)) holds a = b
let a, b be Object of (c1Cat* (o,m)); ::_thesis: a = b
a = o by TARSKI:def_1;
hence a = b by TARSKI:def_1; ::_thesis: verum
end;
theorem Th47: :: CAT_4:47
for o, m being set
for f, g being Morphism of (c1Cat* (o,m)) holds f = g
proof
let o, m be set ; ::_thesis: for f, g being Morphism of (c1Cat* (o,m)) holds f = g
let f, g be Morphism of (c1Cat* (o,m)); ::_thesis: f = g
f = m by TARSKI:def_1;
hence f = g by TARSKI:def_1; ::_thesis: verum
end;
theorem Th48: :: CAT_4:48
for o, m being set
for a, b being Object of (c1Cat* (o,m))
for f being Morphism of (c1Cat* (o,m)) holds f in Hom (a,b)
proof
let o, m be set ; ::_thesis: for a, b being Object of (c1Cat* (o,m))
for f being Morphism of (c1Cat* (o,m)) holds f in Hom (a,b)
let a, b be Object of (c1Cat* (o,m)); ::_thesis: for f being Morphism of (c1Cat* (o,m)) holds f in Hom (a,b)
let f be Morphism of (c1Cat* (o,m)); ::_thesis: f in Hom (a,b)
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 f in Hom (a,b) by A1; ::_thesis: verum
end;
theorem :: CAT_4:49
for o, m being set
for a, b being Object of (c1Cat* (o,m))
for f being Morphism of (c1Cat* (o,m)) holds f is Morphism of a,b
proof
let o, m be set ; ::_thesis: for a, b being Object of (c1Cat* (o,m))
for f being Morphism of (c1Cat* (o,m)) holds f is Morphism of a,b
let a, b be Object of (c1Cat* (o,m)); ::_thesis: for f being Morphism of (c1Cat* (o,m)) holds f is Morphism of a,b
let f be Morphism of (c1Cat* (o,m)); ::_thesis: f is Morphism of a,b
f in Hom (a,b) by Th48;
hence f is Morphism of a,b by CAT_1:def_5; ::_thesis: verum
end;
theorem :: CAT_4:50
for o, m being set
for a, b being Object of (c1Cat* (o,m)) holds Hom (a,b) <> {} by Th48;
theorem Th51: :: CAT_4:51
for o, m being set
for a being Object of (c1Cat* (o,m)) holds a is initial
proof
let o, m be set ; ::_thesis: for a being Object of (c1Cat* (o,m)) holds a is initial
let a be Object of (c1Cat* (o,m)); ::_thesis: a is initial
let b be Object of (c1Cat* (o,m)); :: according to CAT_1:def_19 ::_thesis: ( not Hom (a,b) = {} & ex b1 being Morphism of a,b st
for b2 being Morphism of a,b holds b1 = b2 )
set f = the Morphism of a,b;
thus Hom (a,b) <> {} by Th48; ::_thesis: ex b1 being Morphism of a,b st
for b2 being Morphism of a,b holds b1 = b2
take the Morphism of a,b ; ::_thesis: for b1 being Morphism of a,b holds the Morphism of a,b = b1
thus for b1 being Morphism of a,b holds the Morphism of a,b = b1 by Th47; ::_thesis: verum
end;
theorem Th52: :: CAT_4:52
for o, m being set
for c being Object of (c1Cat* (o,m))
for i1, i2 being Morphism of (c1Cat* (o,m)) holds c is_a_coproduct_wrt i1,i2
proof
let o, m be set ; ::_thesis: for c being Object of (c1Cat* (o,m))
for i1, i2 being Morphism of (c1Cat* (o,m)) holds c is_a_coproduct_wrt i1,i2
let c be Object of (c1Cat* (o,m)); ::_thesis: for i1, i2 being Morphism of (c1Cat* (o,m)) holds c is_a_coproduct_wrt i1,i2
let i1, i2 be Morphism of (c1Cat* (o,m)); ::_thesis: c is_a_coproduct_wrt i1,i2
thus ( cod i1 = c & cod i2 = c ) by Th46; :: according to CAT_3:def_18 ::_thesis: for b1 being Element of the carrier of (c1Cat* (o,m))
for b2, b3 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b2 in Hom ((dom i1),b1) or not b3 in Hom ((dom i2),b1) or ex b4 being Element of the carrier' of (c1Cat* (o,m)) st
( b4 in Hom (c,b1) & ( for b5 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b5 in Hom (c,b1) or ( ( not b5 (*) i1 = b2 or not b5 (*) i2 = b3 or b4 = b5 ) & ( not b4 = b5 or ( b5 (*) i1 = b2 & b5 (*) i2 = b3 ) ) ) ) ) ) )
let d be Object of (c1Cat* (o,m)); ::_thesis: for b1, b2 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b1 in Hom ((dom i1),d) or not b2 in Hom ((dom i2),d) or ex b3 being Element of the carrier' of (c1Cat* (o,m)) st
( b3 in Hom (c,d) & ( for b4 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b4 in Hom (c,d) or ( ( not b4 (*) i1 = b1 or not b4 (*) i2 = b2 or b3 = b4 ) & ( not b3 = b4 or ( b4 (*) i1 = b1 & b4 (*) i2 = b2 ) ) ) ) ) ) )
let f, g be Morphism of (c1Cat* (o,m)); ::_thesis: ( not f in Hom ((dom i1),d) or not g in Hom ((dom i2),d) or ex b1 being Element of the carrier' of (c1Cat* (o,m)) st
( b1 in Hom (c,d) & ( for b2 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b2 in Hom (c,d) or ( ( not b2 (*) i1 = f or not b2 (*) i2 = g or b1 = b2 ) & ( not b1 = b2 or ( b2 (*) i1 = f & b2 (*) i2 = g ) ) ) ) ) ) )
assume that
f in Hom ((dom i1),d) and
g in Hom ((dom i2),d) ; ::_thesis: ex b1 being Element of the carrier' of (c1Cat* (o,m)) st
( b1 in Hom (c,d) & ( for b2 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b2 in Hom (c,d) or ( ( not b2 (*) i1 = f or not b2 (*) i2 = g or b1 = b2 ) & ( not b1 = b2 or ( b2 (*) i1 = f & b2 (*) i2 = g ) ) ) ) ) )
take h = i1; ::_thesis: ( h in Hom (c,d) & ( for b1 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b1 in Hom (c,d) or ( ( not b1 (*) i1 = f or not b1 (*) i2 = g or h = b1 ) & ( not h = b1 or ( b1 (*) i1 = f & b1 (*) i2 = g ) ) ) ) ) )
thus h in Hom (c,d) by Th48; ::_thesis: for b1 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b1 in Hom (c,d) or ( ( not b1 (*) i1 = f or not b1 (*) i2 = g or h = b1 ) & ( not h = b1 or ( b1 (*) i1 = f & b1 (*) i2 = g ) ) ) )
thus for b1 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b1 in Hom (c,d) or ( ( not b1 (*) i1 = f or not b1 (*) i2 = g or h = b1 ) & ( not h = b1 or ( b1 (*) i1 = f & b1 (*) i2 = g ) ) ) ) by Th47; ::_thesis: verum
end;
definition
let IT be non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr ;
attrIT is Cocartesian means :Def26: :: CAT_4:def 26
( 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;
:: deftheorem Def26 defines Cocartesian CAT_4:def_26_:_
for IT being non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr holds
( IT is Cocartesian iff ( 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) ) ) ) );
theorem Th53: :: CAT_4:53
for o, m being set holds c1Cat* (o,m) is Cocartesian
proof
let o, m be set ; ::_thesis: c1Cat* (o,m) is Cocartesian
set 1PCat = c1Cat* (o,m);
thus the Initial of (c1Cat* (o,m)) is initial by Th51; :: according to CAT_4:def_26 ::_thesis: for a, b being Object of (c1Cat* (o,m)) holds
( dom ( the Incl1 of (c1Cat* (o,m)) . (a,b)) = a & dom ( the Incl2 of (c1Cat* (o,m)) . (a,b)) = b & the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) )
let a, b be Object of (c1Cat* (o,m)); ::_thesis: ( dom ( the Incl1 of (c1Cat* (o,m)) . (a,b)) = a & dom ( the Incl2 of (c1Cat* (o,m)) . (a,b)) = b & the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) )
thus dom ( the Incl1 of (c1Cat* (o,m)) . (a,b)) = a by Th46; ::_thesis: ( dom ( the Incl2 of (c1Cat* (o,m)) . (a,b)) = b & the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) )
thus dom ( the Incl2 of (c1Cat* (o,m)) . (a,b)) = b by Th46; ::_thesis: the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b)
thus the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) by Th52; ::_thesis: verum
end;
registration
cluster non empty non void V57() Category-like transitive associative reflexive with_identities strict Cocartesian for CoprodCatStr ;
existence
ex b1 being non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr st
( b1 is strict & b1 is Cocartesian )
proof
c1Cat* (0,1) is Cocartesian by Th53;
hence ex b1 being non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr st
( b1 is strict & b1 is Cocartesian ) ; ::_thesis: verum
end;
end;
definition
mode Cocartesian_category is non empty non void Category-like transitive associative reflexive with_identities Cocartesian CoprodCatStr ;
end;
theorem :: CAT_4:54
for C being Cocartesian_category holds [[0]] C is initial by Def26;
theorem Th55: :: CAT_4:55
for C being Cocartesian_category
for a being Object of C
for f1, f2 being Morphism of [[0]] C,a holds f1 = f2
proof
let C be Cocartesian_category; ::_thesis: for a being Object of C
for f1, f2 being Morphism of [[0]] C,a holds f1 = f2
let a be Object of C; ::_thesis: for f1, f2 being Morphism of [[0]] C,a holds f1 = f2
let f1, f2 be Morphism of [[0]] C,a; ::_thesis: f1 = f2
[[0]] C is initial by Def26;
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_19;
thus f1 = f by A1
.= f2 by A1 ; ::_thesis: verum
end;
definition
let C be Cocartesian_category;
let a be Object of C;
func init a -> Morphism of [[0]] C,a means :: CAT_4:def 27
verum;
existence
ex b1 being Morphism of [[0]] C,a st verum ;
uniqueness
for b1, b2 being Morphism of [[0]] C,a holds b1 = b2 by Th55;
end;
:: deftheorem defines init CAT_4:def_27_:_
for C being Cocartesian_category
for a being Object of C
for b3 being Morphism of [[0]] C,a holds
( b3 = init a iff verum );
theorem Th56: :: CAT_4:56
for C being Cocartesian_category
for a being Object of C holds Hom (([[0]] C),a) <> {}
proof
let C be Cocartesian_category; ::_thesis: for a being Object of C holds Hom (([[0]] C),a) <> {}
let a be Object of C; ::_thesis: Hom (([[0]] C),a) <> {}
[[0]] C is initial by Def26;
hence Hom (([[0]] C),a) <> {} by CAT_1:def_19; ::_thesis: verum
end;
theorem Th57: :: CAT_4:57
for C being Cocartesian_category
for a being Object of C holds init a = init (([[0]] C),a)
proof
let C be Cocartesian_category; ::_thesis: for a being Object of C holds init a = init (([[0]] C),a)
let a be Object of C; ::_thesis: init a = init (([[0]] C),a)
[[0]] C is initial by Def26;
hence init a = init (([[0]] C),a) by CAT_3:40; ::_thesis: verum
end;
theorem :: CAT_4:58
for C being Cocartesian_category
for a being Object of C holds
( dom (init a) = [[0]] C & cod (init a) = a )
proof
let C be Cocartesian_category; ::_thesis: for a being Object of C holds
( dom (init a) = [[0]] C & cod (init a) = a )
let a be Object of C; ::_thesis: ( dom (init a) = [[0]] C & cod (init a) = a )
( [[0]] C is initial & init a = init (([[0]] C),a) ) by Def26, Th57;
hence ( dom (init a) = [[0]] C & cod (init a) = a ) by CAT_3:38; ::_thesis: verum
end;
theorem :: CAT_4:59
for C being Cocartesian_category
for a being Object of C holds Hom (([[0]] C),a) = {(init a)}
proof
let C be Cocartesian_category; ::_thesis: for a being Object of C holds Hom (([[0]] C),a) = {(init a)}
let a be Object of C; ::_thesis: Hom (([[0]] C),a) = {(init a)}
for f2 being Morphism of [[0]] C,a holds init a = f2 by Th55;
hence Hom (([[0]] C),a) = {(init a)} by Th56, CAT_1:8; ::_thesis: verum
end;
theorem Th60: :: CAT_4:60
for C being Cocartesian_category
for a, b being Object of C holds
( dom (in1 (a,b)) = a & cod (in1 (a,b)) = a + b )
proof
let C be Cocartesian_category; ::_thesis: for a, b being Object of C holds
( dom (in1 (a,b)) = a & cod (in1 (a,b)) = a + b )
let a, b be Object of C; ::_thesis: ( dom (in1 (a,b)) = a & cod (in1 (a,b)) = a + b )
set i1 = the Incl1 of C . (a,b);
set i2 = the Incl2 of C . (a,b);
a + b is_a_coproduct_wrt the Incl1 of C . (a,b), the Incl2 of C . (a,b) by Def26;
hence ( dom (in1 (a,b)) = a & cod (in1 (a,b)) = a + b ) by Def26, CAT_3:def_18; ::_thesis: verum
end;
theorem Th61: :: CAT_4:61
for C being Cocartesian_category
for a, b being Object of C holds
( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b )
proof
let C be Cocartesian_category; ::_thesis: for a, b being Object of C holds
( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b )
let a, b be Object of C; ::_thesis: ( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b )
set i1 = the Incl1 of C . (a,b);
set i2 = the Incl2 of C . (a,b);
a + b is_a_coproduct_wrt the Incl1 of C . (a,b), the Incl2 of C . (a,b) by Def26;
hence ( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b ) by Def26, CAT_3:def_18; ::_thesis: verum
end;
theorem Th62: :: CAT_4:62
for C being Cocartesian_category
for a, b being Object of C holds
( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} )
proof
let C be Cocartesian_category; ::_thesis: for a, b being Object of C holds
( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} )
let a, b be Object of C; ::_thesis: ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} )
set c = the Coproduct of C . (a,b);
set i1 = the Incl1 of C . (a,b);
set i2 = the Incl2 of C . (a,b);
the Coproduct of C . (a,b) is_a_coproduct_wrt the Incl1 of C . (a,b), the Incl2 of C . (a,b) by Def26;
then A1: ( cod ( the Incl1 of C . (a,b)) = the Coproduct of C . (a,b) & cod ( the Incl2 of C . (a,b)) = the Coproduct of C . (a,b) ) by CAT_3:def_18;
( dom ( the Incl1 of C . (a,b)) = a & dom ( the Incl2 of C . (a,b)) = b ) by Def26;
hence ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by A1, CAT_1:1; ::_thesis: verum
end;
theorem :: CAT_4:63
for C being Cocartesian_category
for a, b being Object of C holds a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) by Def26;
theorem :: CAT_4:64
for C being Cocartesian_category holds C is with_finite_coproduct
proof
let C be Cocartesian_category; ::_thesis: C is with_finite_coproduct
A1: for a, b being Object of C ex c being Object of C ex 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 be Object of C; ::_thesis: ex c being Object of C ex 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 )
take a + b ; ::_thesis: ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = a + b & cod i2 = a + b & a + b is_a_coproduct_wrt i1,i2 )
take in1 (a,b) ; ::_thesis: ex i2 being Morphism of C st
( dom (in1 (a,b)) = a & dom i2 = b & cod (in1 (a,b)) = a + b & cod i2 = a + b & a + b is_a_coproduct_wrt in1 (a,b),i2 )
take in2 (a,b) ; ::_thesis: ( dom (in1 (a,b)) = a & dom (in2 (a,b)) = b & cod (in1 (a,b)) = a + b & cod (in2 (a,b)) = a + b & a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) )
thus ( dom (in1 (a,b)) = a & dom (in2 (a,b)) = b & cod (in1 (a,b)) = a + b & cod (in2 (a,b)) = a + b & a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) ) by Def26, Th60, Th61; ::_thesis: verum
end;
[[0]] C is initial by Def26;
hence C is with_finite_coproduct by A1, Th44; ::_thesis: verum
end;
definition
let C be Cocartesian_category;
let a, b be Object of C;
:: original: in1
redefine func in1 (a,b) -> Morphism of a,a + b;
coherence
in1 (a,b) is Morphism of a,a + b
proof
( dom (in1 (a,b)) = a & cod (in1 (a,b)) = a + b ) by Th60;
hence in1 (a,b) is Morphism of a,a + b by CAT_1:4; ::_thesis: verum
end;
:: original: in2
redefine func in2 (a,b) -> Morphism of b,a + b;
coherence
in2 (a,b) is Morphism of b,a + b
proof
( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b ) by Th61;
hence in2 (a,b) is Morphism of b,a + b by CAT_1:4; ::_thesis: verum
end;
end;
theorem :: CAT_4:65
for C being Cocartesian_category
for a, b being Object of C st Hom (a,b) <> {} & Hom (b,a) <> {} holds
( in1 (a,b) is coretraction & in2 (a,b) is coretraction )
proof
let C be Cocartesian_category; ::_thesis: for a, b being Object of C st Hom (a,b) <> {} & Hom (b,a) <> {} holds
( in1 (a,b) is coretraction & in2 (a,b) is coretraction )
let a, b be Object of C; ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} implies ( in1 (a,b) is coretraction & in2 (a,b) is coretraction ) )
X: ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by Th62;
( a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) & dom (in1 (a,b)) = a ) by Def26;
hence ( Hom (a,b) <> {} & Hom (b,a) <> {} implies ( in1 (a,b) is coretraction & in2 (a,b) is coretraction ) ) by X, CAT_3:82; ::_thesis: verum
end;
definition
let C be Cocartesian_category;
let a, b be Object of C;
:: original: in1
redefine func in1 (a,b) -> Morphism of a,a + b;
coherence
in1 (a,b) is Morphism of a,a + b
proof
( cod (in1 (a,b)) = a + b & dom (in1 (a,b)) = a ) by Th60;
hence in1 (a,b) is Morphism of a,a + b ; ::_thesis: verum
end;
:: original: in2
redefine func in2 (a,b) -> Morphism of b,a + b;
coherence
in2 (a,b) is Morphism of b,a + b
proof
( cod (in2 (a,b)) = a + b & dom (in2 (a,b)) = b ) by Th61;
hence in2 (a,b) is Morphism of b,a + b ; ::_thesis: verum
end;
end;
definition
let C be Cocartesian_category;
let a, b, c be Object of C;
let f be Morphism of a,c;
let g be Morphism of b,c;
assume A1: ( Hom (a,c) <> {} & Hom (b,c) <> {} ) ;
func[$f,g$] -> Morphism of a + b,c means :Def28: :: CAT_4:def 28
( it * (in1 (a,b)) = f & it * (in2 (a,b)) = g );
existence
ex b1 being Morphism of a + b,c st
( b1 * (in1 (a,b)) = f & b1 * (in2 (a,b)) = g )
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 Th62;
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 ; ::_thesis: ( h * (in1 (a,b)) = f & h * (in2 (a,b)) = g )
thus ( h * (in1 (a,b)) = f & h * (in2 (a,b)) = g ) by A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Morphism of a + b,c st b1 * (in1 (a,b)) = f & b1 * (in2 (a,b)) = g & b2 * (in1 (a,b)) = f & b2 * (in2 (a,b)) = g holds
b1 = b2
proof
A4: Hom (b,(a + b)) <> {} by Th62;
( a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) & Hom (a,(a + b)) <> {} ) by Def26, Th62;
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; ::_thesis: ( h1 * (in1 (a,b)) = f & h1 * (in2 (a,b)) = g & h2 * (in1 (a,b)) = f & h2 * (in2 (a,b)) = g implies h1 = h2 )
assume that
A6: ( h1 * (in1 (a,b)) = f & h1 * (in2 (a,b)) = g ) and
A7: ( h2 * (in1 (a,b)) = f & h2 * (in2 (a,b)) = g ) ; ::_thesis: h1 = h2
h1 = h by A6, A5;
hence h1 = h2 by A7, A5; ::_thesis: verum
end;
end;
:: deftheorem Def28 defines [$ CAT_4:def_28_:_
for C being Cocartesian_category
for a, b, c being Object of C
for f being Morphism of a,c
for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds
for b7 being Morphism of a + b,c holds
( b7 = [$f,g$] iff ( b7 * (in1 (a,b)) = f & b7 * (in2 (a,b)) = g ) );
theorem Th66: :: CAT_4:66
for C being Cocartesian_category
for a, c, b being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds
Hom ((a + b),c) <> {}
proof
let C be Cocartesian_category; ::_thesis: for a, c, b being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds
Hom ((a + b),c) <> {}
let a, c, b be Object of C; ::_thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} implies Hom ((a + b),c) <> {} )
A1: a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) by Def26;
( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by Th62;
hence ( Hom (a,c) <> {} & Hom (b,c) <> {} implies Hom ((a + b),c) <> {} ) by A1, CAT_3:81; ::_thesis: verum
end;
theorem Th67: :: CAT_4:67
for C being Cocartesian_category
for a, b being Object of C holds [$(in1 (a,b)),(in2 (a,b))$] = id (a + b)
proof
let C be Cocartesian_category; ::_thesis: for a, b being Object of C holds [$(in1 (a,b)),(in2 (a,b))$] = id (a + b)
let a, b be Object of C; ::_thesis: [$(in1 (a,b)),(in2 (a,b))$] = id (a + b)
A1: Hom (b,(a + b)) <> {} by Th62;
then A2: (id (a + b)) * (in2 (a,b)) = in2 (a,b) by CAT_1:28;
A3: Hom (a,(a + b)) <> {} by Th62;
then (id (a + b)) * (in1 (a,b)) = in1 (a,b) by CAT_1:28;
hence [$(in1 (a,b)),(in2 (a,b))$] = id (a + b) by A3, A1, A2, Def28; ::_thesis: verum
end;
theorem Th68: :: CAT_4:68
for C being Cocartesian_category
for a, c, b, d being Object of C
for f being Morphism of a,c
for g being Morphism of b,c
for 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 C be Cocartesian_category; ::_thesis: for a, c, b, d being Object of C
for f being Morphism of a,c
for g being Morphism of b,c
for h being Morphism of c,d st Hom (a,c) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
[$(h * f),(h * g)$] = h * [$f,g$]
let a, c, b, d be Object of C; ::_thesis: for f being Morphism of a,c
for g being Morphism of b,c
for h being Morphism of c,d st Hom (a,c) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
[$(h * f),(h * g)$] = h * [$f,g$]
let f be Morphism of a,c; ::_thesis: for g being Morphism of b,c
for h being Morphism of c,d st Hom (a,c) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
[$(h * f),(h * g)$] = h * [$f,g$]
let g be Morphism of b,c; ::_thesis: for h being Morphism of c,d st Hom (a,c) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
[$(h * f),(h * g)$] = h * [$f,g$]
let h be Morphism of c,d; ::_thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} implies [$(h * f),(h * g)$] = h * [$f,g$] )
assume that
A1: ( Hom (a,c) <> {} & Hom (b,c) <> {} ) and
A2: Hom (c,d) <> {} ; ::_thesis: [$(h * f),(h * g)$] = h * [$f,g$]
A3: Hom ((a + b),c) <> {} by A1, Th66;
A4: Hom (b,(a + b)) <> {} by Th62;
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 Th62;
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 [$(h * f),(h * g)$] = h * [$f,g$] by A5, A7, Def28; ::_thesis: verum
end;
theorem Th69: :: CAT_4:69
for C being Cocartesian_category
for a, c, b being Object of C
for f, k being Morphism of a,c
for 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 C be Cocartesian_category; ::_thesis: for a, c, b being Object of C
for f, k being Morphism of a,c
for g, h being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & [$f,g$] = [$k,h$] holds
( f = k & g = h )
let a, c, b be Object of C; ::_thesis: for f, k being Morphism of a,c
for g, h being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & [$f,g$] = [$k,h$] holds
( f = k & g = h )
let f, k be Morphism of a,c; ::_thesis: for g, h being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & [$f,g$] = [$k,h$] holds
( f = k & g = h )
let g, h be Morphism of b,c; ::_thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} & [$f,g$] = [$k,h$] implies ( f = k & g = h ) )
assume A1: ( Hom (a,c) <> {} & Hom (b,c) <> {} ) ; ::_thesis: ( not [$f,g$] = [$k,h$] or ( f = k & g = h ) )
then ( [$f,g$] * (in1 (a,b)) = f & [$f,g$] * (in2 (a,b)) = g ) by Def28;
hence ( not [$f,g$] = [$k,h$] or ( f = k & g = h ) ) by A1, Def28; ::_thesis: verum
end;
theorem :: CAT_4:70
for C being Cocartesian_category
for a, c, b being Object of C
for f being Morphism of a,c
for 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 C be Cocartesian_category; ::_thesis: for a, c, b being Object of C
for f being Morphism of a,c
for 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
let a, c, b be Object of C; ::_thesis: for f being Morphism of a,c
for 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
let f be Morphism of a,c; ::_thesis: for 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
let g be Morphism of b,c; ::_thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} & ( f is epi or g is epi ) implies [$f,g$] is epi )
assume that
A1: Hom (a,c) <> {} and
A2: Hom (b,c) <> {} and
A3: ( f is epi or g is epi ) ; ::_thesis: [$f,g$] is epi
A4: now__::_thesis:_(_g_is_epi_implies_for_d_being_Object_of_C
for_f1,_f2_being_Morphism_of_c,d_st_Hom_(c,d)_<>_{}_&_f1_*_[$f,g$]_=_f2_*_[$f,g$]_holds_
f1_=_f2_)
assume A5: g is epi ; ::_thesis: for d being Object of C
for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] holds
f1 = f2
let d be Object of C; ::_thesis: for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] holds
f1 = f2
let f1, f2 be Morphism of c,d; ::_thesis: ( Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] implies f1 = f2 )
assume that
A6: Hom (c,d) <> {} and
A7: f1 * [$f,g$] = f2 * [$f,g$] ; ::_thesis: f1 = f2
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, Th68;
then f1 * g = f2 * g by A7, A8, Th69;
hence f1 = f2 by A2, A5, A6, CAT_1:36; ::_thesis: verum
end;
A9: now__::_thesis:_(_f_is_epi_implies_for_d_being_Object_of_C
for_f1,_f2_being_Morphism_of_c,d_st_Hom_(c,d)_<>_{}_&_f1_*_[$f,g$]_=_f2_*_[$f,g$]_holds_
f1_=_f2_)
assume A10: f is epi ; ::_thesis: for d being Object of C
for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] holds
f1 = f2
let d be Object of C; ::_thesis: for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] holds
f1 = f2
let f1, f2 be Morphism of c,d; ::_thesis: ( Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] implies f1 = f2 )
assume that
A11: Hom (c,d) <> {} and
A12: f1 * [$f,g$] = f2 * [$f,g$] ; ::_thesis: f1 = f2
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, Th68;
then f1 * f = f2 * f by A12, A13, Th69;
hence f1 = f2 by A1, A10, A11, CAT_1:36; ::_thesis: verum
end;
Hom ((a + b),c) <> {} by A1, A2, Th66;
hence [$f,g$] is epi by A3, A9, A4, CAT_1:36; ::_thesis: verum
end;
theorem :: CAT_4:71
for C being Cocartesian_category
for a being Object of C holds
( a,a + ([[0]] C) are_isomorphic & a,([[0]] C) + a are_isomorphic )
proof
let C be Cocartesian_category; ::_thesis: for a being Object of C holds
( a,a + ([[0]] C) are_isomorphic & a,([[0]] C) + a are_isomorphic )
let a be Object of C; ::_thesis: ( a,a + ([[0]] C) are_isomorphic & a,([[0]] C) + a are_isomorphic )
A1: (in2 (([[0]] C),a)) * (init a) = in1 (([[0]] C),a) by Th55;
A2: ( Hom (([[0]] C),a) <> {} & Hom (a,a) <> {} ) by Th56;
thus a,a + ([[0]] C) are_isomorphic ::_thesis: a,([[0]] C) + a are_isomorphic
proof
thus A3: Hom (a,(a + ([[0]] C))) <> {} by Th62; :: according to CAT_4:def_1 ::_thesis: ( Hom ((a + ([[0]] C)),a) <> {} & ex f being Morphism of a,a + ([[0]] C) ex f9 being Morphism of a + ([[0]] C),a st
( f * f9 = id (a + ([[0]] C)) & f9 * f = id a ) )
thus Hom ((a + ([[0]] C)),a) <> {} by A2, Th66; ::_thesis: ex f being Morphism of a,a + ([[0]] C) ex f9 being Morphism of a + ([[0]] C),a st
( f * f9 = id (a + ([[0]] C)) & f9 * f = id a )
take g = in1 (a,([[0]] C)); ::_thesis: ex f9 being Morphism of a + ([[0]] C),a st
( g * f9 = id (a + ([[0]] C)) & f9 * g = id a )
take f = [$(id a),(init a)$]; ::_thesis: ( g * f = id (a + ([[0]] C)) & f * g = id a )
A4: (in1 (a,([[0]] C))) * (init a) = in2 (a,([[0]] C)) by Th55;
(in1 (a,([[0]] C))) * (id a) = in1 (a,([[0]] C)) by A3, CAT_1:29;
then g * f = [$(in1 (a,([[0]] C))),(in2 (a,([[0]] C)))$] by A2, A3, A4, Th68;
hence ( g * f = id (a + ([[0]] C)) & f * g = id a ) by A2, Def28, Th67; ::_thesis: verum
end;
thus A5: Hom (a,(([[0]] C) + a)) <> {} by Th62; :: according to CAT_4:def_1 ::_thesis: ( Hom ((([[0]] C) + a),a) <> {} & ex f being Morphism of a,([[0]] C) + a ex f9 being Morphism of ([[0]] C) + a,a st
( f * f9 = id (([[0]] C) + a) & f9 * f = id a ) )
thus Hom ((([[0]] C) + a),a) <> {} by A2, Th66; ::_thesis: ex f being Morphism of a,([[0]] C) + a ex f9 being Morphism of ([[0]] C) + a,a st
( f * f9 = id (([[0]] C) + a) & f9 * f = id a )
take g = in2 (([[0]] C),a); ::_thesis: ex f9 being Morphism of ([[0]] C) + a,a st
( g * f9 = id (([[0]] C) + a) & f9 * g = id a )
take f = [$(init a),(id a)$]; ::_thesis: ( g * f = id (([[0]] C) + a) & f * g = id a )
(in2 (([[0]] C),a)) * (id a) = in2 (([[0]] C),a) by A5, CAT_1:29;
then g * f = [$(in1 (([[0]] C),a)),(in2 (([[0]] C),a))$] by A2, A5, A1, Th68;
hence ( g * f = id (([[0]] C) + a) & f * g = id a ) by A2, Def28, Th67; ::_thesis: verum
end;
theorem :: CAT_4:72
for C being Cocartesian_category
for a, b being Object of C holds a + b,b + a are_isomorphic
proof
let C be Cocartesian_category; ::_thesis: for a, b being Object of C holds a + b,b + a are_isomorphic
let a, b be Object of C; ::_thesis: a + b,b + a are_isomorphic
A1: ( Hom (a,(b + a)) <> {} & Hom (b,(b + a)) <> {} ) by Th62;
hence A2: Hom ((a + b),(b + a)) <> {} by Th66; :: according to CAT_4:def_1 ::_thesis: ( Hom ((b + a),(a + b)) <> {} & ex f being Morphism of a + b,b + a ex f9 being Morphism of b + a,a + b st
( f * f9 = id (b + a) & f9 * f = id (a + b) ) )
A3: ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by Th62;
hence A4: Hom ((b + a),(a + b)) <> {} by Th66; ::_thesis: ex f being Morphism of a + b,b + a ex f9 being Morphism of b + a,a + b st
( f * f9 = id (b + a) & f9 * f = id (a + b) )
take f9 = [$(in2 (b,a)),(in1 (b,a))$]; ::_thesis: ex f9 being Morphism of b + a,a + b st
( f9 * f9 = id (b + a) & f9 * f9 = id (a + b) )
take f = [$(in2 (a,b)),(in1 (a,b))$]; ::_thesis: ( f9 * f = id (b + a) & f * f9 = id (a + b) )
thus f9 * f = [$(f9 * (in2 (a,b))),(f9 * (in1 (a,b)))$] by A2, A3, Th68
.= [$(in1 (b,a)),(f9 * (in1 (a,b)))$] by A1, Def28
.= [$(in1 (b,a)),(in2 (b,a))$] by A1, Def28
.= id (b + a) by Th67 ; ::_thesis: f * f9 = id (a + b)
thus f * f9 = [$(f * (in2 (b,a))),(f * (in1 (b,a)))$] by A1, A4, Th68
.= [$(in1 (a,b)),(f * (in1 (b,a)))$] by A3, Def28
.= [$(in1 (a,b)),(in2 (a,b))$] by A3, Def28
.= id (a + b) by Th67 ; ::_thesis: verum
end;
theorem :: CAT_4:73
for C being Cocartesian_category
for a, b, c being Object of C holds (a + b) + c,a + (b + c) are_isomorphic
proof
let C be Cocartesian_category; ::_thesis: for a, b, c being Object of C holds (a + b) + c,a + (b + c) are_isomorphic
let a, b, c be Object of C; ::_thesis: (a + b) + c,a + (b + c) are_isomorphic
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 Th62;
A2: Hom (b,(b + c)) <> {} by Th62;
then A3: Hom (b,(a + (b + c))) <> {} by A1, CAT_1:24;
A4: Hom (a,(a + (b + c))) <> {} by Th62;
then A5: Hom ((a + b),(a + (b + c))) <> {} by A3, Th66;
A6: Hom (c,(b + c)) <> {} by Th62;
then A7: Hom (c,(a + (b + c))) <> {} by A1, CAT_1:24;
hence A8: Hom (((a + b) + c),(a + (b + c))) <> {} by A5, Th66; :: according to CAT_4:def_1 ::_thesis: ( Hom ((a + (b + c)),((a + b) + c)) <> {} & ex f being Morphism of (a + b) + c,a + (b + c) ex f9 being Morphism of a + (b + c),(a + b) + c st
( f * f9 = id (a + (b + c)) & f9 * f = id ((a + b) + c) ) )
A9: Hom ((a + b),((a + b) + c)) <> {} by Th62;
A10: Hom (b,(a + b)) <> {} by Th62;
then A11: Hom (b,((a + b) + c)) <> {} by A9, CAT_1:24;
A12: Hom (c,((a + b) + c)) <> {} by Th62;
then A13: Hom ((b + c),((a + b) + c)) <> {} by A11, Th66;
A14: Hom (a,(a + b)) <> {} by Th62;
then A15: Hom (a,((a + b) + c)) <> {} by A9, CAT_1:24;
hence A16: Hom ((a + (b + c)),((a + b) + c)) <> {} by A13, Th66; ::_thesis: ex f being Morphism of (a + b) + c,a + (b + c) ex f9 being Morphism of a + (b + c),(a + b) + c st
( f * f9 = id (a + (b + c)) & f9 * f = id ((a + b) + c) )
take g = [$[$(in1 (a,(b + c))),((in2 (a,(b + c))) * (in1 (b,c)))$],((in2 (a,(b + c))) * (in2 (b,c)))$]; ::_thesis: ex f9 being Morphism of a + (b + c),(a + b) + c st
( g * f9 = id (a + (b + c)) & f9 * g = id ((a + 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
.= [$(in1 (a,(b + c))),((in2 (a,(b + c))) * (in1 (b,c)))$] * (in2 (a,b)) by A7, A5, Def28
.= (in2 (a,(b + c))) * (in1 (b,c)) by A3, A4, Def28 ;
then A17: g * [$((in1 ((a + b),c)) * (in2 (a,b))),(in2 ((a + b),c))$] = [$((in2 (a,(b + c))) * (in1 (b,c))),(g * (in2 ((a + b),c)))$] by A8, A11, A12, Th68
.= [$((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, Th68
.= (in2 (a,(b + c))) * (id (b + c)) by Th67
.= in2 (a,(b + c)) by A1, CAT_1:29 ;
take f = [$((in1 ((a + b),c)) * (in1 (a,b))),[$((in1 ((a + b),c)) * (in2 (a,b))),(in2 ((a + b),c))$]$]; ::_thesis: ( g * f = id (a + (b + c)) & f * g = id ((a + b) + c) )
f * ((in2 (a,(b + c))) * (in1 (b,c))) = (f * (in2 (a,(b + c)))) * (in1 (b,c)) by A2, A1, A16, CAT_1:25
.= [$((in1 ((a + b),c)) * (in2 (a,b))),(in2 ((a + b),c))$] * (in1 (b,c)) by A15, A13, Def28
.= (in1 ((a + b),c)) * (in2 (a,b)) by A11, A12, Def28 ;
then A18: f * [$(in1 (a,(b + c))),((in2 (a,(b + c))) * (in1 (b,c)))$] = [$(f * (in1 (a,(b + c)))),((in1 ((a + b),c)) * (in2 (a,b)))$] by A3, A4, A16, Th68
.= [$((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, Th68
.= (in1 ((a + b),c)) * (id (a + b)) by Th67
.= 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
.= [$(in1 (a,(b + c))),((in2 (a,(b + c))) * (in1 (b,c)))$] * (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, Th68
.= id (a + (b + c)) by Th67 ;
::_thesis: f * g = id ((a + b) + c)
f * ((in2 (a,(b + c))) * (in2 (b,c))) = (f * (in2 (a,(b + c)))) * (in2 (b,c)) by A1, A6, A16, CAT_1:25
.= [$((in1 ((a + b),c)) * (in2 (a,b))),(in2 ((a + b),c))$] * (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, Th68
.= id ((a + b) + c) by Th67 ;
::_thesis: verum
end;
definition
let C be Cocartesian_category;
let a be Object of C;
func nabla a -> Morphism of a + a,a equals :: CAT_4:def 29
[$(id a),(id a)$];
correctness
coherence
[$(id a),(id a)$] is Morphism of a + a,a;
;
end;
:: deftheorem defines nabla CAT_4:def_29_:_
for C being Cocartesian_category
for a being Object of C holds nabla a = [$(id a),(id a)$];
definition
let C be Cocartesian_category;
let a, b, c, d be Object of C;
let f be Morphism of a,c;
let g be Morphism of b,d;
funcf + g -> Morphism of a + b,c + d equals :: CAT_4:def 30
[$((in1 (c,d)) * f),((in2 (c,d)) * g)$];
correctness
coherence
[$((in1 (c,d)) * f),((in2 (c,d)) * g)$] is Morphism of a + b,c + d;
;
end;
:: deftheorem defines + CAT_4:def_30_:_
for C being Cocartesian_category
for a, b, c, d being Object of C
for f being Morphism of a,c
for g being Morphism of b,d holds f + g = [$((in1 (c,d)) * f),((in2 (c,d)) * g)$];
theorem :: CAT_4:74
for C being Cocartesian_category
for a, c, b, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds
Hom ((a + b),(c + d)) <> {}
proof
let C be Cocartesian_category; ::_thesis: for a, c, b, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds
Hom ((a + b),(c + d)) <> {}
let a, c, b, d be Object of C; ::_thesis: ( Hom (a,c) <> {} & Hom (b,d) <> {} implies Hom ((a + b),(c + d)) <> {} )
assume that
A1: Hom (a,c) <> {} and
A2: Hom (b,d) <> {} ; ::_thesis: Hom ((a + b),(c + d)) <> {}
Hom (d,(c + d)) <> {} by Th62;
then A3: Hom (b,(c + d)) <> {} by A2, CAT_1:24;
Hom (c,(c + d)) <> {} by Th62;
then Hom (a,(c + d)) <> {} by A1, CAT_1:24;
hence Hom ((a + b),(c + d)) <> {} by A3, Th66; ::_thesis: verum
end;
theorem :: CAT_4:75
for C being Cocartesian_category
for a, b being Object of C holds (id a) + (id b) = id (a + b)
proof
let C be Cocartesian_category; ::_thesis: for a, b being Object of C holds (id a) + (id b) = id (a + b)
let a, b be Object of C; ::_thesis: (id a) + (id b) = id (a + b)
Hom (b,(a + b)) <> {} by Th62;
then A1: (in2 (a,b)) * (id b) = in2 (a,b) by CAT_1:29;
Hom (a,(a + b)) <> {} by Th62;
then (in1 (a,b)) * (id a) = in1 (a,b) by CAT_1:29;
hence (id a) + (id b) = id (a + b) by A1, Th67; ::_thesis: verum
end;
theorem Th76: :: CAT_4:76
for C being Cocartesian_category
for a, c, b, d, e being Object of C
for f being Morphism of a,c
for h being Morphism of b,d
for g being Morphism of c,e
for 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 C be Cocartesian_category; ::_thesis: for a, c, b, d, e being Object of C
for f being Morphism of a,c
for h being Morphism of b,d
for g being Morphism of c,e
for 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)$]
let a, c, b, d, e be Object of C; ::_thesis: for f being Morphism of a,c
for h being Morphism of b,d
for g being Morphism of c,e
for 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)$]
let f be Morphism of a,c; ::_thesis: for h being Morphism of b,d
for g being Morphism of c,e
for 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)$]
let h be Morphism of b,d; ::_thesis: for g being Morphism of c,e
for 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)$]
let g be Morphism of c,e; ::_thesis: for 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)$]
let k be Morphism of d,e; ::_thesis: ( Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} implies [$g,k$] * (f + h) = [$(g * f),(k * h)$] )
assume that
A1: Hom (a,c) <> {} and
A2: Hom (b,d) <> {} and
A3: ( Hom (c,e) <> {} & Hom (d,e) <> {} ) ; ::_thesis: [$g,k$] * (f + h) = [$(g * f),(k * h)$]
A4: Hom ((c + d),e) <> {} by A3, Th66;
A5: Hom (d,(c + d)) <> {} by Th62;
then A6: Hom (b,(c + d)) <> {} by A2, CAT_1:24;
A7: Hom (c,(c + d)) <> {} by Th62;
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 [$g,k$] * (f + h) = [$(g * f),(k * h)$] by A4, A8, A6, A9, Th68; ::_thesis: verum
end;
theorem :: CAT_4:77
for C being Cocartesian_category
for a, c, b being Object of C
for f being Morphism of a,c
for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds
(nabla c) * (f + g) = [$f,g$]
proof
let C be Cocartesian_category; ::_thesis: for a, c, b being Object of C
for f being Morphism of a,c
for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds
(nabla c) * (f + g) = [$f,g$]
let a, c, b be Object of C; ::_thesis: for f being Morphism of a,c
for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds
(nabla c) * (f + g) = [$f,g$]
let f be Morphism of a,c; ::_thesis: for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds
(nabla c) * (f + g) = [$f,g$]
let g be Morphism of b,c; ::_thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} implies (nabla c) * (f + g) = [$f,g$] )
assume that
A1: Hom (a,c) <> {} and
A2: Hom (b,c) <> {} ; ::_thesis: (nabla c) * (f + g) = [$f,g$]
Hom (c,c) <> {} ;
hence (nabla c) * (f + g) = [$((id c) * f),((id c) * g)$] by A1, A2, Th76
.= [$f,((id c) * g)$] by A1, CAT_1:28
.= [$f,g$] by A2, CAT_1:28 ;
::_thesis: verum
end;
theorem :: CAT_4:78
for C being Cocartesian_category
for a, c, b, d, e, s being Object of C
for f being Morphism of a,c
for h being Morphism of b,d
for g being Morphism of c,e
for 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 C be Cocartesian_category; ::_thesis: for a, c, b, d, e, s being Object of C
for f being Morphism of a,c
for h being Morphism of b,d
for g being Morphism of c,e
for 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)
let a, c, b, d, e, s be Object of C; ::_thesis: for f being Morphism of a,c
for h being Morphism of b,d
for g being Morphism of c,e
for 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)
let f be Morphism of a,c; ::_thesis: for h being Morphism of b,d
for g being Morphism of c,e
for 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)
let h be Morphism of b,d; ::_thesis: for g being Morphism of c,e
for 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)
let g be Morphism of c,e; ::_thesis: for 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)
let k be Morphism of d,s; ::_thesis: ( Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,s) <> {} implies (g + k) * (f + h) = (g * f) + (k * h) )
assume that
A1: Hom (a,c) <> {} and
A2: Hom (b,d) <> {} and
A3: Hom (c,e) <> {} and
A4: Hom (d,s) <> {} ; ::_thesis: (g + k) * (f + h) = (g * f) + (k * h)
A5: Hom (s,(e + s)) <> {} by Th62;
then A6: Hom (d,(e + s)) <> {} by A4, CAT_1:24;
A7: Hom (e,(e + s)) <> {} by Th62;
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 (g + k) * (f + h) = (g * f) + (k * h) by A1, A2, A6, A8, Th76; ::_thesis: verum
end;