:: Cartesian Categories
:: by Czes{\l}aw Byli\'nski
::
:: Received October 27, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users

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 ) ) );

definition

let C be Category;

attr C 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 end;

definition

attr c₁ is strict ;
struct ProdCatStr -> CatStr ;
aggr ProdCatStr(# carrier, carrier', Source, Target, Comp, TerminalObj, CatProd, Proj1, Proj2 #) -> ProdCatStr ;
sel TerminalObj c₁ -> Element of the carrier of c₁;
sel CatProd c₁ -> Function of [: the carrier of c₁, the carrier of c₁:], the carrier of c₁;
sel Proj1 c₁ -> Function of [: the carrier of c₁, the carrier of c₁:], the carrier' of c₁;
sel Proj2 c₁ -> Function of [: the carrier of c₁, the carrier of c₁:], the carrier' of c₁;

end;

registration

cluster non empty non void for ProdCatStr ;

existence
ex b₁ being ProdCatStr st
( not b₁ is void & not b₁ is empty )

proof 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;

func a [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) ;

Lm1: for o, m being set holds c1Cat (o,m) is Category-like

proof end;

registration

cluster non empty non void V59() Category-like transitive associative reflexive with_identities strict for ProdCatStr ;

existence
ex b₁ being non empty non void ProdCatStr st
( b₁ is strict & b₁ is Category-like & b₁ is reflexive & b₁ is transitive & b₁ is associative & b₁ is with_identities & not b₁ is void & not b₁ is empty )

proof 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 Lm1;

end;

theorem Th3: :: CAT_4:3

for o, m being set
for a, b being Object of (c1Cat (o,m)) holds a = b

proof end;

theorem Th4: :: CAT_4:4

for o, m being set
for f, g being Morphism of (c1Cat (o,m)) holds f = g

proof 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 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 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 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 end;

definition

let IT be non empty non void Category-like transitive associative reflexive with_identities ProdCatStr ;

attr IT 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 by Th8, Th3, Th9;

registration

cluster non empty non void V59() Category-like transitive associative reflexive with_identities strict Cartesian for ProdCatStr ;

existence
ex b₁ being non empty non void Category-like transitive associative reflexive with_identities ProdCatStr st
( b₁ is strict & b₁ is Cartesian )

proof 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 end;

theorem Th13: :: CAT_4:13

for C being Cartesian_category
for a being Object of C holds Hom (a,([1] C)) <> {}

proof 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 b₁ being Morphism of a, [1] C st verum ;
uniqueness
for b₁, b₂ being Morphism of a, [1] C holds b₁ = b₂ by Th12;

end;

:: deftheorem defines term CAT_4:def 9 :
for C being Cartesian_category
for a being Object of C
for b₃ being Morphism of a, [1] C holds
( b₃ = 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 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 end;

theorem :: CAT_4:16

for C being Cartesian_category
for a being Object of C holds Hom (a,([1] C)) = {(term a)}

proof 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 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 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 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 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 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 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 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 b₁ being Morphism of c,a [x] b st
( (pr1 (a,b)) * b₁ = f & (pr2 (a,b)) * b₁ = g )

proof end;

uniqueness
for b₁, b₂ being Morphism of c,a [x] b st (pr1 (a,b)) * b₁ = f & (pr2 (a,b)) * b₁ = g & (pr1 (a,b)) * b₂ = f & (pr2 (a,b)) * b₂ = g holds
b₁ = b₂

proof 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 b₇ being Morphism of c,a [x] b holds
( b₇ = <:f,g:> iff ( (pr1 (a,b)) * b₇ = f & (pr2 (a,b)) * b₇ = g ) );

theorem Th23: :: CAT_4:23

for C being Cartesian_category
for a, b, c being Object of C st Hom (c,a) <> {} & Hom (c,b) <> {} holds
Hom (c,(a [x] b)) <> {}

proof 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 end;

theorem Th25: :: CAT_4:25

for C being Cartesian_category
for a, b, c, 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 end;

theorem Th26: :: CAT_4:26

for C being Cartesian_category
for a, b, c 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 end;

theorem :: CAT_4:27

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) <> {} & ( f is monic or g is monic ) holds
<:f,g:> is monic

proof 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 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 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 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 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 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 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 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 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 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 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 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;

func f [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, b, c, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds
Hom ((a [x] b),(c [x] d)) <> {}

proof 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 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 end;

theorem :: CAT_4:42

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
<:f,g:> = (f [x] g) * (Delta c)

proof 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 end;

definition

let C be Category;

attr C 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 end;

definition

attr c₁ is strict ;
struct CoprodCatStr -> CatStr ;
aggr CoprodCatStr(# carrier, carrier', Source, Target, Comp, Initial, Coproduct, Incl1, Incl2 #) -> CoprodCatStr ;
sel Initial c₁ -> Element of the carrier of c₁;
sel Coproduct c₁ -> Function of [: the carrier of c₁, the carrier of c₁:], the carrier of c₁;
sel Incl1 c₁ -> Function of [: the carrier of c₁, the carrier of c₁:], the carrier' of c₁;
sel Incl2 c₁ -> Function of [: the carrier of c₁, the carrier of c₁:], the carrier' of c₁;

end;

registration

cluster non empty non void for CoprodCatStr ;

existence
ex b₁ being CoprodCatStr st
( not b₁ is void & not b₁ is empty )

proof end;

end;

definition

let C be non empty non void CoprodCatStr ;

func EmptyMS 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;

func a + 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 EmptyMS CAT_4:def 21 :
for C being non empty non void CoprodCatStr holds EmptyMS 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;

::$CT

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;

Lm2: for o, m being set holds c1Cat* (o,m) is Category-like

proof end;

registration

cluster non empty non void V59() Category-like transitive associative reflexive with_identities strict for CoprodCatStr ;

existence
ex b₁ being non empty non void CoprodCatStr st
( b₁ is strict & b₁ is Category-like & b₁ is reflexive & b₁ is transitive & b₁ is associative & b₁ is with_identities )

proof 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 Lm2;

end;

theorem Th45: :: CAT_4:46

for o, m being set
for a, b being Object of (c1Cat* (o,m)) holds a = b

proof end;

theorem Th46: :: CAT_4:47

for o, m being set
for f, g being Morphism of (c1Cat* (o,m)) holds f = g

proof end;

theorem Th47: :: 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 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 end;

theorem :: CAT_4:50

for o, m being set
for a, b being Object of (c1Cat* (o,m)) holds Hom (a,b) <> {} by Th47;

theorem Th50: :: CAT_4:51

for o, m being set
for a being Object of (c1Cat* (o,m)) holds a is initial

proof end;

theorem Th51: :: 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 end;

definition

let IT be non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr ;

attr IT 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 Th52: :: CAT_4:53

for o, m being set holds c1Cat* (o,m) is Cocartesian by Th50, Th45, Th51;

registration

cluster non empty non void V59() Category-like transitive associative reflexive with_identities strict Cocartesian for CoprodCatStr ;

existence
ex b₁ being non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr st
( b₁ is strict & b₁ is Cocartesian )

proof 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 EmptyMS C is initial by Def26;

theorem Th54: :: CAT_4:55

for C being Cocartesian_category
for a being Object of C
for f1, f2 being Morphism of EmptyMS C,a holds f1 = f2

proof end;

definition

let C be Cocartesian_category;
let a be Object of C;

func init a -> Morphism of EmptyMS C,a means :: CAT_4:def 27
verum;

existence
ex b₁ being Morphism of EmptyMS C,a st verum ;
uniqueness
for b₁, b₂ being Morphism of EmptyMS C,a holds b₁ = b₂ by Th54;

end;

:: deftheorem defines init CAT_4:def 27 :
for C being Cocartesian_category
for a being Object of C
for b₃ being Morphism of EmptyMS C,a holds
( b₃ = init a iff verum );

theorem Th55: :: CAT_4:56

for C being Cocartesian_category
for a being Object of C holds Hom ((EmptyMS C),a) <> {}

proof end;

theorem Th56: :: CAT_4:57

for C being Cocartesian_category
for a being Object of C holds init a = init ((EmptyMS C),a)

proof end;

theorem :: CAT_4:58

for C being Cocartesian_category
for a being Object of C holds
( dom (init a) = EmptyMS C & cod (init a) = a )

proof end;

theorem :: CAT_4:59

for C being Cocartesian_category
for a being Object of C holds Hom ((EmptyMS C),a) = {(init a)}

proof end;

theorem Th59: :: 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 end;

theorem Th60: :: 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 end;

theorem Th61: :: 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 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 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 end;

:: original: in2
redefine func in2 (a,b) -> Morphism of b,a + b;
coherence
in2 (a,b) is Morphism of b,a + b

proof 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 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 end;

:: original: in2
redefine func in2 (a,b) -> Morphism of b,a + b;
coherence
in2 (a,b) is Morphism of b,a + b

proof 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 b₁ being Morphism of a + b,c st
( b₁ * (in1 (a,b)) = f & b₁ * (in2 (a,b)) = g )

proof end;

uniqueness
for b₁, b₂ being Morphism of a + b,c st b₁ * (in1 (a,b)) = f & b₁ * (in2 (a,b)) = g & b₂ * (in1 (a,b)) = f & b₂ * (in2 (a,b)) = g holds
b₁ = b₂

proof 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 b₇ being Morphism of a + b,c holds
( b₇ = [$f,g$] iff ( b₇ * (in1 (a,b)) = f & b₇ * (in2 (a,b)) = g ) );

theorem Th65: :: CAT_4:66

for C being Cocartesian_category
for a, b, c being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds
Hom ((a + b),c) <> {}

proof end;

theorem Th66: :: 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 end;

theorem Th67: :: CAT_4:68

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,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 end;

theorem Th68: :: CAT_4:69

for C being Cocartesian_category
for a, b, c 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 end;

theorem :: CAT_4:70

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) <> {} & ( f is epi or g is epi ) holds
[$f,g$] is epi

proof end;

theorem :: CAT_4:71

for C being Cocartesian_category
for a being Object of C holds
( a,a + (EmptyMS C) are_isomorphic & a,(EmptyMS C) + a are_isomorphic )

proof 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 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 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;

func f + 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, b, c, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds
Hom ((a + b),(c + d)) <> {}

proof 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 end;

theorem Th75: :: CAT_4:76

for C being Cocartesian_category
for a, b, c, 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 end;

theorem :: CAT_4:77

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
(nabla c) * (f + g) = [$f,g$]

proof end;

theorem :: CAT_4:78

for C being Cocartesian_category
for a, b, c, 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 end;