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-2011 Association of Mizar Users

begin

scheme :: CAT_3:sch 1
LambdaIdx{ 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)

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:58;

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 :: CAT_3:3

canceled;

theorem :: CAT_3:4

canceled;

theorem :: CAT_3:5

canceled;

theorem :: CAT_3:6

canceled;

theorem Th7: :: CAT_3:7

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;

begin

definition

let C be Category;
let I be set ;
let F be Function of I, the carrier' of C;
canceled;
canceled;
func doms F -> Function of I, the carrier of C means :Def3: :: CAT_3:def 3
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 :Def4: :: CAT_3:def 4
for x being set st x in I holds
it /. x = cod (F /. x);
correctness

proof end;

end;

:: deftheorem CAT_3:def 1 :

:: deftheorem CAT_3:def 2 :

:: deftheorem Def3 defines doms CAT_3:def 3 :

:: deftheorem Def4 defines cods CAT_3:def 4 :

theorem Th8: :: CAT_3:8

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

proof end;

theorem Th9: :: CAT_3:9

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

proof end;

theorem Th10: :: CAT_3:10

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 Th11: :: CAT_3:11

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 :Def5: :: CAT_3:def 5
for x being set st x in I holds
it /. x = (F /. x) opp ;
correctness

proof end;

end;

:: deftheorem Def5 defines opp CAT_3:def 5 :

theorem :: CAT_3:12

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:13

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:14

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 :Def6: :: CAT_3:def 6
for x being set st x in I holds
it /. x = opp (F /. x);
correctness

proof end;

end;

:: deftheorem Def6 defines opp CAT_3:def 6 :

theorem :: CAT_3:15

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:16

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:17

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 :Def7: :: CAT_3:def 7
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 :Def8: :: CAT_3:def 8
for x being set st x in I holds
it /. x = f * (F /. x);
correctness

proof end;

end;

:: deftheorem Def7 defines * CAT_3:def 7 :

:: deftheorem Def8 defines * CAT_3:def 8 :

theorem Th18: :: CAT_3:18

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

proof end;

theorem Th19: :: CAT_3:19

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 Th20: :: 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 st doms F = I --> (cod f) holds
( doms (F * f) = I --> (dom f) & cods (F * f) = cods F )

proof end;

theorem Th21: :: 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 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 :Def9: :: CAT_3:def 9
for x being set st x in I holds
it /. x = (F /. x) * (G /. x);
correctness

proof end;

end;

:: deftheorem Def9 defines "*" CAT_3:def 9 :

theorem Th22: :: CAT_3:22

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:23

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:24

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:25

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;

begin

definition

let C be Category;
let IT be Morphism of C;
attr IT is retraction means :Def10: :: CAT_3:def 10
ex g being Morphism of C st
( cod g = dom IT & IT * g = id (cod IT) );
attr IT is coretraction means :Def11: :: CAT_3:def 11
ex g being Morphism of C st
( dom g = cod IT & g * IT = id (dom IT) );

end;

:: deftheorem Def10 defines retraction CAT_3:def 10 :

:: deftheorem Def11 defines coretraction CAT_3:def 11 :

theorem Th26: :: CAT_3:26

for C being Category
for f being Morphism of C st f is retraction holds
f is epi

proof end;

theorem :: CAT_3:27

for C being Category
for f being Morphism of C st f is coretraction holds
f is monic

proof end;

theorem :: CAT_3:28

for C being Category
for f, g being Morphism of C st f is retraction & g is retraction & dom g = cod f holds
g * f is retraction

proof end;

theorem :: CAT_3:29

for C being Category
for f, g being Morphism of C st f is coretraction & g is coretraction & dom g = cod f holds
g * f is coretraction

proof end;

theorem :: CAT_3:30

for C being Category
for g, f being Morphism of C st dom g = cod f & g * f is retraction holds
g is retraction

proof end;

theorem :: CAT_3:31

for C being Category
for g, f being Morphism of C st dom g = cod f & g * f is coretraction holds
f is coretraction

proof end;

theorem :: CAT_3:32

for C being Category
for f being Morphism of C st f is retraction & f is monic holds
f is invertible

proof end;

theorem Th33: :: CAT_3:33

for C being Category
for f being Morphism of C st f is coretraction & f is epi holds
f is invertible

proof end;

theorem :: CAT_3:34

for C being Category
for f being Morphism of C holds
( f is invertible iff ( f is retraction & f is coretraction ) )

proof end;

theorem :: CAT_3:35

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

proof end;

theorem :: CAT_3:36

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

proof end;

theorem :: CAT_3:37

for C being Category
for f being Morphism of C holds
( f is retraction iff f opp is coretraction )

proof end;

theorem :: CAT_3:38

for C being Category
for f being Morphism of C holds
( f is coretraction iff f opp is retraction )

proof end;

begin

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 12
verum;
existence ;
uniqueness

proof end;

end;

:: deftheorem defines term CAT_3:def 12 :

theorem Th39: :: CAT_3:39

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

proof end;

theorem Th40: :: CAT_3:40

for C being Category
for b, a 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:41

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;

begin

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 13
verum;
existence ;
uniqueness

proof end;

end;

:: deftheorem defines init CAT_3:def 13 :

theorem Th42: :: CAT_3:42

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 Th43: :: CAT_3:43

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:44

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;

begin

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 :Def14: :: CAT_3:def 14
doms it = I --> a;
existence

proof end;

end;

:: deftheorem Def14 defines Projections_family CAT_3:def 14 :

theorem Th45: :: CAT_3:45

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 Th46: :: CAT_3:46

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 Th47: :: CAT_3:47

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 Th48: :: CAT_3:48

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 :: CAT_3:49

canceled;

theorem Th50: :: CAT_3:50

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:51

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:52

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 :Def15: :: CAT_3:def 15
( 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 Def15 defines is_a_product_wrt CAT_3:def 15 :

theorem Th53: :: CAT_3:53

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 Th54: :: CAT_3:54

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
F /. x is retraction

proof end;

theorem Th55: :: CAT_3:55

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 Th56: :: CAT_3:56

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

proof end;

theorem :: CAT_3:57

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:58

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 :Def16: :: CAT_3:def 16
( 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 Def16 defines is_a_product_wrt CAT_3:def 16 :

theorem Th59: :: CAT_3:59

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:60

for C being Category
for c, a, b 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:61

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:62

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 & Hom ((cod p1),(cod p2)) <> {} & Hom ((cod p2),(cod p1)) <> {} holds
( p1 is retraction & p2 is retraction )

proof end;

theorem Th63: :: CAT_3:63

for C being Category
for c being Object of C
for p1, p2, h 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:64

for C being Category
for c, d being Object of C
for p1, p2, f being Morphism of 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:65

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:66

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;

begin

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 :Def17: :: CAT_3:def 17
cods it = I --> c;
existence

proof end;

end;

:: deftheorem Def17 defines Injections_family CAT_3:def 17 :

theorem Th67: :: CAT_3:67

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:68

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 Th69: :: CAT_3:69

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 Th70: :: CAT_3:70

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 :: CAT_3:71

canceled;

theorem Th72: :: CAT_3:72

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:73

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 Th74: :: CAT_3:74

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 Th75: :: CAT_3:75

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:76

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 :Def18: :: CAT_3:def 18
( 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 Def18 defines is_a_coproduct_wrt CAT_3:def 18 :

theorem :: CAT_3:77

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 Th78: :: CAT_3:78

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 Th79: :: CAT_3:79

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
F /. x is coretraction

proof end;

theorem Th80: :: CAT_3:80

for I being set
for C being Category
for a, b being Object of C
for f being Morphism of C
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 Th81: :: CAT_3:81

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:82

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:83

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 :Def19: :: CAT_3:def 19
( 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 Def19 defines is_a_coproduct_wrt CAT_3:def 19 :

theorem :: CAT_3:84

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 Th85: :: CAT_3:85

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:86

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:87

for C being Category
for a, c, b 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:88

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 & Hom ((dom i1),(dom i2)) <> {} & Hom ((dom i2),(dom i1)) <> {} holds
( i1 is coretraction & i2 is coretraction )

proof end;

theorem Th89: :: CAT_3:89

for C being Category
for c being Object of C
for i1, i2, h 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:90

for C being Category
for c, d being Object of C
for i1, i2, f being Morphism of C 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:91

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:92

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;