CAT_3: Products and Coproducts in Categories

:: Products and Coproducts in Categories
:: by Czes{\l}aw Byli\'nski
::
:: Received May 11, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users

scheme :: CAT_3:sch 1
LambdaIdx{ F₁() -> set , F₂() -> non empty set , F₃( object ) -> Element of F₂() } :

ex F being Function of F₁(),F₂() st
for x being set st x in F₁() holds
F /. x = F₃(x)

proof end;

theorem Th1: :: CAT_3:1

for I being set
for A being non empty set
for F1, F2 being Function of I,A st ( for x being set st x in I holds
F1 /. x = F2 /. x ) holds
F1 = F2

proof end;

scheme :: CAT_3:sch 2
FuncIdxcorrectness{ F₁() -> set , F₂() -> non empty set , F₃( set ) -> Element of F₂() } :

( ex F being Function of F₁(),F₂() st
for x being set st x in F₁() holds
F /. x = F₃(x) & ( for F1, F2 being Function of F₁(),F₂() st ( for x being set st x in F₁() holds
F1 /. x = F₃(x) ) & ( for x being set st x in F₁() holds
F2 /. x = F₃(x) ) holds
F1 = F2 ) )

proof end;

definition

let A be non empty set ;
let x be set ;
let a be Element of A;
:: original: .-->
redefine func x .--> a -> Function of {x},A;
coherence by FUNCOP_1:46;

end;

theorem Th2: :: CAT_3:2

for I, x being set
for A being non empty set
for a being Element of A st x in I holds
(I --> a) /. x = a

proof end;

theorem Th3: :: CAT_3:3

for x1, x2 being set
for A being non empty set st x1 <> x2 holds
for y1, y2 being Element of A holds
( ((x1,x2) --> (y1,y2)) /. x1 = y1 & ((x1,x2) --> (y1,y2)) /. x2 = y2 )

proof end;

definition

let C be Category;
let I be set ;
let F be Function of I, the carrier' of C;

func doms F -> Function of I, the carrier of C means :Def1: :: CAT_3:def 1
for x being set st x in I holds
it /. x = dom (F /. x);

correctness

proof end;

func cods F -> Function of I, the carrier of C means :Def2: :: CAT_3:def 2
for x being set st x in I holds
it /. x = cod (F /. x);

correctness

proof end;

end;

:: deftheorem Def1 defines doms CAT_3:def 1 :

:: deftheorem Def2 defines cods CAT_3:def 2 :

theorem Th4: :: CAT_3:4

for I being set
for C being Category
for f being Morphism of C holds doms (I --> f) = I --> (dom f)

proof end;

theorem Th5: :: CAT_3:5

for I being set
for C being Category
for f being Morphism of C holds cods (I --> f) = I --> (cod f)

proof end;

theorem Th6: :: CAT_3:6

for x1, x2 being set
for C being Category
for p1, p2 being Morphism of C holds doms ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((dom p1),(dom p2))

proof end;

theorem Th7: :: CAT_3:7

for x1, x2 being set
for C being Category
for p1, p2 being Morphism of C holds cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2))

proof end;

definition

let C be Category;
let I be set ;
let F be Function of I, the carrier' of C;

func F opp -> Function of I, the carrier' of (C opp) means :Def3: :: CAT_3:def 3
for x being set st x in I holds
it /. x = (F /. x) opp ;

correctness

proof end;

end;

:: deftheorem Def3 defines opp CAT_3:def 3 :

theorem :: CAT_3:8

for I being set
for C being Category
for f being Morphism of C holds (I --> f) opp = I --> (f opp)

proof end;

theorem :: CAT_3:9

for x1, x2 being set
for C being Category
for p1, p2 being Morphism of C st x1 <> x2 holds
((x1,x2) --> (p1,p2)) opp = (x1,x2) --> ((p1 opp),(p2 opp))

proof end;

theorem :: CAT_3:10

for I being set
for C being Category
for F being Function of I, the carrier' of C holds (F opp) opp = F

proof end;

definition

let C be Category;
let I be set ;
let F be Function of I, the carrier' of (C opp);

func opp F -> Function of I, the carrier' of C means :Def4: :: CAT_3:def 4
for x being set st x in I holds
it /. x = opp (F /. x);

correctness

proof end;

end;

:: deftheorem Def4 defines opp CAT_3:def 4 :

theorem :: CAT_3:11

for I being set
for C being Category
for f being Morphism of (C opp) holds opp (I --> f) = I --> (opp f)

proof end;

theorem :: CAT_3:12

for x1, x2 being set
for C being Category st x1 <> x2 holds
for p1, p2 being Morphism of (C opp) holds opp ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((opp p1),(opp p2))

proof end;

theorem :: CAT_3:13

for I being set
for C being Category
for F being Function of I, the carrier' of C holds opp (F opp) = F

proof end;

definition

let C be Category;
let I be set ;
let F be Function of I, the carrier' of C;
let f be Morphism of C;

func F * f -> Function of I, the carrier' of C means :Def5: :: CAT_3:def 5
for x being set st x in I holds
it /. x = (F /. x) (*) f;

correctness

proof end;

func f * F -> Function of I, the carrier' of C means :Def6: :: CAT_3:def 6
for x being set st x in I holds
it /. x = f (*) (F /. x);

correctness

proof end;

end;

:: deftheorem Def5 defines * CAT_3:def 5 :

:: deftheorem Def6 defines * CAT_3:def 6 :

theorem Th14: :: CAT_3:14

for x1, x2 being set
for C being Category
for f, p1, p2 being Morphism of C st x1 <> x2 holds
((x1,x2) --> (p1,p2)) * f = (x1,x2) --> ((p1 (*) f),(p2 (*) f))

proof end;

theorem Th15: :: CAT_3:15

for x1, x2 being set
for C being Category
for f, p1, p2 being Morphism of C st x1 <> x2 holds
f * ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((f (*) p1),(f (*) p2))

proof end;

theorem Th16: :: CAT_3:16

for I being set
for C being Category
for f being Morphism of C
for F being Function of I, the carrier' of C st doms F = I --> (cod f) holds
( doms (F * f) = I --> (dom f) & cods (F * f) = cods F )

proof end;

theorem Th17: :: CAT_3:17

for I being set
for C being Category
for f being Morphism of C
for F being Function of I, the carrier' of C st cods F = I --> (dom f) holds
( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )

proof end;

definition

let C be Category;
let I be set ;
let F, G be Function of I, the carrier' of C;

func F "*" G -> Function of I, the carrier' of C means :Def7: :: CAT_3:def 7
for x being set st x in I holds
it /. x = (F /. x) (*) (G /. x);

correctness

proof end;

end;

:: deftheorem Def7 defines "*" CAT_3:def 7 :

theorem Th18: :: CAT_3:18

for I being set
for C being Category
for F, G being Function of I, the carrier' of C st doms F = cods G holds
( doms (F "*" G) = doms G & cods (F "*" G) = cods F )

proof end;

theorem :: CAT_3:19

for x1, x2 being set
for C being Category
for p1, p2, q1, q2 being Morphism of C st x1 <> x2 holds
((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2)) = (x1,x2) --> ((p1 (*) q1),(p2 (*) q2))

proof end;

theorem :: CAT_3:20

for I being set
for C being Category
for f being Morphism of C
for F being Function of I, the carrier' of C holds F * f = F "*" (I --> f)

proof end;

theorem :: CAT_3:21

for I being set
for C being Category
for f being Morphism of C
for F being Function of I, the carrier' of C holds f * F = (I --> f) "*" F

proof end;

definition

let C be Category;
let a, b be Object of C;
let IT be Morphism of a,b;

attr IT is retraction means :: CAT_3:def 8
( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st IT * g = id b );

attr IT is coretraction means :: CAT_3:def 9
( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st g * IT = id a );

end;

:: deftheorem defines retraction CAT_3:def 8 :

:: deftheorem defines coretraction CAT_3:def 9 :

theorem Th22: :: CAT_3:22

for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is retraction holds
f is epi

proof end;

theorem :: CAT_3:23

for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is coretraction holds
f is monic

proof end;

theorem :: CAT_3:24

for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is retraction & g is retraction holds
g * f is retraction

proof end;

theorem :: CAT_3:25

for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is coretraction & g is coretraction holds
g * f is coretraction

proof end;

theorem :: CAT_3:26

for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,a) <> {} & g * f is retraction holds
g is retraction

proof end;

theorem :: CAT_3:27

for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (b,c) <> {} & Hom (c,b) <> {} & g * f is coretraction holds
f is coretraction

proof end;

theorem :: CAT_3:28

for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is retraction & f is monic holds
f is invertible

proof end;

theorem Th29: :: CAT_3:29

for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is coretraction & f is epi holds
f is invertible

proof end;

theorem :: CAT_3:30

for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f is invertible iff ( f is retraction & f is coretraction ) ) by Th22, Th29;

definition

let C be Category;
let a, b be Object of C;
assume A1: Hom (a,b) <> {} ;
let D be Category;
let T be Functor of C,D;
let f be Morphism of a,b;

func T /. f -> Morphism of T . a,T . b equals :Def10: :: CAT_3:def 10
T . f;

coherence

proof end;

end;

:: deftheorem Def10 defines /. CAT_3:def 10 :

Lm1: for C, D being Category
for T being Functor of C,D
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds T /. (g * f) = (T /. g) * (T /. f)

proof end;

Lm2: for C, D being Category
for T being Functor of C,D
for c being Object of C holds T /. (id c) = id (T . c)

proof end;

theorem :: CAT_3:31

for C, D being Category
for a, b being Object of C
for f being Morphism of a,b
for T being Functor of C,D st f is retraction holds
T /. f is retraction

proof end;

theorem :: CAT_3:32

for C, D being Category
for a, b being Object of C
for f being Morphism of a,b
for T being Functor of C,D st f is coretraction holds
T /. f is coretraction

proof end;

theorem :: CAT_3:33

for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f is retraction iff f opp is coretraction )

proof end;

theorem :: CAT_3:34

for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f is coretraction iff f opp is retraction )

proof end;

definition

let C be Category;
let a, b be Object of C;
assume A1: b is terminal ;

func term (a,b) -> Morphism of a,b means :: CAT_3:def 11
verum;

existence ;
uniqueness

proof end;

end;

:: deftheorem defines term CAT_3:def 11 :

theorem Th35: :: CAT_3:35

for C being Category
for a, b being Object of C st b is terminal holds
( dom (term (a,b)) = a & cod (term (a,b)) = b )

proof end;

theorem Th36: :: CAT_3:36

for C being Category
for a, b being Object of C
for f being Morphism of C st b is terminal & dom f = a & cod f = b holds
term (a,b) = f

proof end;

theorem :: CAT_3:37

for C being Category
for a, b being Object of C
for f being Morphism of a,b st b is terminal holds
term (a,b) = f

proof end;

definition

let C be Category;
let a, b be Object of C;
assume A1: a is initial ;

func init (a,b) -> Morphism of a,b means :: CAT_3:def 12
verum;

existence ;
uniqueness

proof end;

end;

:: deftheorem defines init CAT_3:def 12 :

theorem Th38: :: CAT_3:38

for C being Category
for a, b being Object of C st a is initial holds
( dom (init (a,b)) = a & cod (init (a,b)) = b )

proof end;

theorem Th39: :: CAT_3:39

for C being Category
for a, b being Object of C
for f being Morphism of C st a is initial & dom f = a & cod f = b holds
init (a,b) = f

proof end;

theorem :: CAT_3:40

for C being Category
for a, b being Object of C
for f being Morphism of a,b st a is initial holds
init (a,b) = f

proof end;

definition

let C be Category;
let a be Object of C;
let I be set ;

mode Projections_family of a,I -> Function of I, the carrier' of C means :Def13: :: CAT_3:def 13
doms it = I --> a;

existence

proof end;

end;

:: deftheorem Def13 defines Projections_family CAT_3:def 13 :

theorem Th41: :: CAT_3:41

for I, x being set
for C being Category
for a being Object of C
for F being Projections_family of a,I st x in I holds
dom (F /. x) = a

proof end;

theorem Th42: :: CAT_3:42

for C being Category
for a being Object of C
for F being Function of {}, the carrier' of C holds F is Projections_family of a, {}

proof end;

theorem Th43: :: CAT_3:43

for y being set
for C being Category
for a being Object of C
for f being Morphism of C st dom f = a holds
y .--> f is Projections_family of a,{y}

proof end;

theorem Th44: :: CAT_3:44

for x1, x2 being set
for C being Category
for a being Object of C
for p1, p2 being Morphism of C st dom p1 = a & dom p2 = a holds
(x1,x2) --> (p1,p2) is Projections_family of a,{x1,x2}

proof end;

theorem Th45: :: CAT_3:45

for I being set
for C being Category
for a being Object of C
for f being Morphism of C
for F being Projections_family of a,I st cod f = a holds
F * f is Projections_family of dom f,I

proof end;

theorem :: CAT_3:46

for I being set
for C being Category
for a being Object of C
for F being Function of I, the carrier' of C
for G being Projections_family of a,I st doms F = cods G holds
F "*" G is Projections_family of a,I

proof end;

theorem :: CAT_3:47

for I being set
for C being Category
for f being Morphism of C
for F being Projections_family of cod f,I holds (f opp) * (F opp) = (F * f) opp

proof end;

definition

let C be Category;
let a be Object of C;
let I be set ;
let F be Function of I, the carrier' of C;

pred a is_a_product_wrt F means :: CAT_3:def 14
( F is Projections_family of a,I & ( for b being Object of C
for F9 being Projections_family of b,I st cods F = cods F9 holds
ex h being Morphism of C st
( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff h = k ) ) ) ) );

end;

:: deftheorem defines is_a_product_wrt CAT_3:def 14 :

theorem Th48: :: CAT_3:48

for I being set
for C being Category
for c, d being Object of C
for F being Projections_family of c,I
for F9 being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F9 & cods F = cods F9 holds
c,d are_isomorphic

proof end;

theorem Th49: :: CAT_3:49

for I being set
for C being Category
for c being Object of C
for F being Projections_family of c,I st c is_a_product_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ) holds
for x being set st x in I holds
for d being Object of C st d = cod (F /. x) & Hom (c,d) <> {} holds
for f being Morphism of c,d st f = F /. x holds
f is retraction

proof end;

theorem Th50: :: CAT_3:50

for C being Category
for a being Object of C
for F being Function of {}, the carrier' of C holds
( a is_a_product_wrt F iff a is terminal )

proof end;

theorem Th51: :: CAT_3:51

for I being set
for C being Category
for a, b being Object of C
for F being Projections_family of a,I st a is_a_product_wrt F holds
for f being Morphism of b,a st dom f = b & cod f = a & f is invertible holds
b is_a_product_wrt F * f

proof end;

theorem :: CAT_3:52

for y being set
for C being Category
for a being Object of C holds a is_a_product_wrt y .--> (id a)

proof end;

theorem :: CAT_3:53

for I being set
for C being Category
for a being Object of C
for F being Projections_family of a,I st a is_a_product_wrt F & ( for x being set st x in I holds
cod (F /. x) is terminal ) holds
a is terminal

proof end;

definition

let C be Category;
let c be Object of C;
let p1, p2 be Morphism of C;

pred c is_a_product_wrt p1,p2 means :: CAT_3:def 15
( dom p1 = c & dom p2 = c & ( for d being Object of C
for f, g being Morphism of C st f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) holds
ex h being Morphism of C st
( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) ) ) );

end;

:: deftheorem defines is_a_product_wrt CAT_3:def 15 :

theorem Th54: :: CAT_3:54

for x1, x2 being set
for C being Category
for c being Object of C
for p1, p2 being Morphism of C st x1 <> x2 holds
( c is_a_product_wrt p1,p2 iff c is_a_product_wrt (x1,x2) --> (p1,p2) )

proof end;

theorem :: CAT_3:55

for C being Category
for a, b, c being Object of C st Hom (c,a) <> {} & Hom (c,b) <> {} holds
for p1 being Morphism of c,a
for p2 being Morphism of c,b holds
( c is_a_product_wrt p1,p2 iff for d being Object of C st Hom (d,a) <> {} & Hom (d,b) <> {} holds
( Hom (d,c) <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) )

proof end;

theorem :: CAT_3:56

for C being Category
for c, d being Object of C
for p1, p2, q1, q2 being Morphism of C st c is_a_product_wrt p1,p2 & d is_a_product_wrt q1,q2 & cod p1 = cod q1 & cod p2 = cod q2 holds
c,d are_isomorphic

proof end;

theorem :: CAT_3:57

for C being Category
for a, b, c being Object of C
for p1 being Morphism of c,a
for p2 being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & c is_a_product_wrt p1,p2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds
( p1 is retraction & p2 is retraction )

proof end;

theorem Th58: :: CAT_3:58

for C being Category
for c being Object of C
for h, p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & h in Hom (c,c) & p1 (*) h = p1 & p2 (*) h = p2 holds
h = id c

proof end;

theorem :: CAT_3:59

for C being Category
for c, d being Object of C
for p1, p2 being Morphism of C
for f being Morphism of d,c st c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible holds
d is_a_product_wrt p1 (*) f,p2 (*) f

proof end;

theorem :: CAT_3:60

for C being Category
for c being Object of C
for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p2 is terminal holds
c, cod p1 are_isomorphic

proof end;

theorem :: CAT_3:61

for C being Category
for c being Object of C
for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p1 is terminal holds
c, cod p2 are_isomorphic

proof end;

definition

let C be Category;
let c be Object of C;
let I be set ;

mode Injections_family of c,I -> Function of I, the carrier' of C means :Def16: :: CAT_3:def 16
cods it = I --> c;

existence

proof end;

end;

:: deftheorem Def16 defines Injections_family CAT_3:def 16 :

theorem Th62: :: CAT_3:62

for I, x being set
for C being Category
for c being Object of C
for F being Injections_family of c,I st x in I holds
cod (F /. x) = c

proof end;

theorem :: CAT_3:63

for C being Category
for a being Object of C
for F being Function of {}, the carrier' of C holds F is Injections_family of a, {}

proof end;

theorem Th64: :: CAT_3:64

for y being set
for C being Category
for a being Object of C
for f being Morphism of C st cod f = a holds
y .--> f is Injections_family of a,{y}

proof end;

theorem Th65: :: CAT_3:65

for x1, x2 being set
for C being Category
for c being Object of C
for p1, p2 being Morphism of C st cod p1 = c & cod p2 = c holds
(x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}

proof end;

theorem Th66: :: CAT_3:66

for I being set
for C being Category
for b being Object of C
for f being Morphism of C
for F being Injections_family of b,I st dom f = b holds
f * F is Injections_family of cod f,I

proof end;

theorem :: CAT_3:67

for I being set
for C being Category
for b being Object of C
for F being Injections_family of b,I
for G being Function of I, the carrier' of C st doms F = cods G holds
F "*" G is Injections_family of b,I

proof end;

theorem Th68: :: CAT_3:68

for I being set
for C being Category
for c being Object of C
for F being Function of I, the carrier' of C holds
( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )

proof end;

theorem Th69: :: CAT_3:69

for I being set
for C being Category
for F being Function of I, the carrier' of (C opp)
for c being Object of (C opp) holds
( F is Injections_family of c,I iff opp F is Projections_family of opp c,I )

proof end;

theorem :: CAT_3:70

for I being set
for C being Category
for f being Morphism of C
for F being Injections_family of dom f,I holds (F opp) * (f opp) = (f * F) opp

proof end;

definition

let C be Category;
let c be Object of C;
let I be set ;
let F be Function of I, the carrier' of C;

pred c is_a_coproduct_wrt F means :: CAT_3:def 17
( F is Injections_family of c,I & ( for d being Object of C
for F9 being Injections_family of d,I st doms F = doms F9 holds
ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( for x being set st x in I holds
k (*) (F /. x) = F9 /. x ) iff h = k ) ) ) ) );

end;

:: deftheorem defines is_a_coproduct_wrt CAT_3:def 17 :

theorem :: CAT_3:71

for I being set
for C being Category
for c being Object of C
for F being Function of I, the carrier' of C holds
( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )

proof end;

theorem Th72: :: CAT_3:72

for I being set
for C being Category
for c, d being Object of C
for F being Injections_family of c,I
for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds
c,d are_isomorphic

proof end;

theorem Th73: :: CAT_3:73

for I being set
for C being Category
for c being Object of C
for F being Injections_family of c,I st c is_a_coproduct_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} ) holds
for x being set st x in I holds
for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds
for f being Morphism of d,c st f = F /. x holds
f is coretraction

proof end;

theorem Th74: :: CAT_3:74

for I being set
for C being Category
for a, b being Object of C
for f being Morphism of a,b
for F being Injections_family of a,I st a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible holds
b is_a_coproduct_wrt f * F

proof end;

theorem Th75: :: CAT_3:75

for C being Category
for a being Object of C
for F being Injections_family of a, {} holds
( a is_a_coproduct_wrt F iff a is initial )

proof end;

theorem :: CAT_3:76

for y being set
for C being Category
for a being Object of C holds a is_a_coproduct_wrt y .--> (id a)

proof end;

theorem :: CAT_3:77

for I being set
for C being Category
for a being Object of C
for F being Injections_family of a,I st a is_a_coproduct_wrt F & ( for x being set st x in I holds
dom (F /. x) is initial ) holds
a is initial

proof end;

definition

let C be Category;
let c be Object of C;
let i1, i2 be Morphism of C;

pred c is_a_coproduct_wrt i1,i2 means :: CAT_3:def 18
( cod i1 = c & cod i2 = c & ( for d being Object of C
for f, g being Morphism of C st f in Hom ((dom i1),d) & g in Hom ((dom i2),d) holds
ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) ) ) );

end;

:: deftheorem defines is_a_coproduct_wrt CAT_3:def 18 :

theorem :: CAT_3:78

for C being Category
for c being Object of C
for p1, p2 being Morphism of C holds
( c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp ,p2 opp )

proof end;

theorem Th79: :: CAT_3:79

for x1, x2 being set
for C being Category
for c being Object of C
for i1, i2 being Morphism of C st x1 <> x2 holds
( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )

proof end;

theorem :: CAT_3:80

for C being Category
for c, d being Object of C
for i1, i2, j1, j2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & d is_a_coproduct_wrt j1,j2 & dom i1 = dom j1 & dom i2 = dom j2 holds
c,d are_isomorphic

proof end;

theorem :: CAT_3:81

for C being Category
for a, b, c being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds
for i1 being Morphism of a,c
for i2 being Morphism of b,c holds
( c is_a_coproduct_wrt i1,i2 iff for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds
( Hom (c,d) <> {} & ( for f being Morphism of a,d
for g being Morphism of b,d ex h being Morphism of c,d st
for k being Morphism of c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k ) ) ) )

proof end;

theorem :: CAT_3:82

for C being Category
for a, b, c being Object of C
for i1 being Morphism of a,c
for i2 being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & c is_a_coproduct_wrt i1,i2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds
( i1 is coretraction & i2 is coretraction )

proof end;

theorem Th83: :: CAT_3:83

for C being Category
for c being Object of C
for h, i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & h in Hom (c,c) & h (*) i1 = i1 & h (*) i2 = i2 holds
h = id c

proof end;

theorem :: CAT_3:84

for C being Category
for c, d being Object of C
for i1, i2 being Morphism of C
for f being Morphism of c,d st c is_a_coproduct_wrt i1,i2 & dom f = c & cod f = d & f is invertible holds
d is_a_coproduct_wrt f (*) i1,f (*) i2

proof end;

theorem :: CAT_3:85

for C being Category
for c being Object of C
for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom i2 is initial holds
dom i1,c are_isomorphic

proof end;

theorem :: CAT_3:86

for C being Category
for c being Object of C
for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom i1 is initial holds
dom i2,c are_isomorphic

proof end;