:: Products and Coproducts in Categories
:: by Czes{\l}aw Byli\'nski
::
:: Received May 11, 1992
:: Copyright (c) 1992 Association of Mizar Users
:: deftheorem Def1 defines /. CAT_3:def 1 :
theorem Th1: :: CAT_3:1
theorem Th2: :: CAT_3:2
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 )
:: deftheorem CAT_3:def 2 :
canceled;
:: deftheorem Def3 defines doms CAT_3:def 3 :
:: deftheorem Def4 defines cods CAT_3:def 4 :
theorem Th8: :: CAT_3:8
theorem Th9: :: CAT_3:9
theorem Th10: :: CAT_3:10
theorem Th11: :: CAT_3:11
:: deftheorem Def5 defines opp CAT_3:def 5 :
theorem :: CAT_3:12
theorem :: CAT_3:13
theorem :: CAT_3:14
:: deftheorem Def6 defines opp CAT_3:def 6 :
theorem :: CAT_3:15
theorem :: CAT_3:16
theorem :: CAT_3:17
:: deftheorem Def7 defines * CAT_3:def 7 :
:: deftheorem Def8 defines * CAT_3:def 8 :
theorem Th18: :: CAT_3:18
theorem Th19: :: CAT_3:19
theorem Th20: :: CAT_3:20
theorem Th21: :: CAT_3:21
:: deftheorem Def9 defines "*" CAT_3:def 9 :
theorem Th22: :: CAT_3:22
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)
theorem :: CAT_3:24
theorem :: CAT_3:25
:: deftheorem Def10 defines retraction CAT_3:def 10 :
:: deftheorem Def11 defines coretraction CAT_3:def 11 :
theorem Th26: :: CAT_3:26
theorem :: CAT_3:27
theorem :: CAT_3:28
theorem :: CAT_3:29
theorem :: CAT_3:30
theorem :: CAT_3:31
theorem :: CAT_3:32
theorem Th33: :: CAT_3:33
theorem :: CAT_3:34
theorem :: CAT_3:35
theorem :: CAT_3:36
theorem :: CAT_3:37
theorem :: CAT_3:38
:: deftheorem defines term CAT_3:def 12 :
theorem Th39: :: CAT_3:39
theorem Th40: :: CAT_3:40
theorem :: CAT_3:41
:: deftheorem defines init CAT_3:def 13 :
theorem Th42: :: CAT_3:42
theorem Th43: :: CAT_3:43
theorem :: CAT_3:44
:: deftheorem Def14 defines Projections_family CAT_3:def 14 :
theorem Th45: :: CAT_3:45
theorem Th46: :: CAT_3:46
theorem Th47: :: CAT_3:47
theorem Th48: :: CAT_3:48
theorem :: CAT_3:49
canceled;
theorem Th50: :: CAT_3:50
theorem :: CAT_3:51
theorem :: CAT_3:52
:: deftheorem Def15 defines is_a_product_wrt CAT_3:def 15 :
theorem Th53: :: CAT_3:53
theorem Th54: :: CAT_3:54
theorem Th55: :: CAT_3:55
theorem Th56: :: CAT_3:56
theorem :: CAT_3:57
theorem :: CAT_3:58
:: deftheorem Def16 defines is_a_product_wrt CAT_3:def 16 :
theorem Th59: :: CAT_3:59
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 ) ) ) )
theorem :: CAT_3:61
theorem :: CAT_3:62
theorem Th63: :: CAT_3:63
theorem :: CAT_3:64
theorem :: CAT_3:65
theorem :: CAT_3:66
:: deftheorem Def17 defines Injections_family CAT_3:def 17 :
theorem Th67: :: CAT_3:67
theorem :: CAT_3:68
theorem Th69: :: CAT_3:69
theorem Th70: :: CAT_3:70
theorem :: CAT_3:71
canceled;
theorem Th72: :: CAT_3:72
theorem :: CAT_3:73
theorem Th74: :: CAT_3:74
theorem Th75: :: CAT_3:75
theorem :: CAT_3:76
:: deftheorem Def18 defines is_a_coproduct_wrt CAT_3:def 18 :
theorem :: CAT_3:77
theorem Th78: :: CAT_3:78
theorem Th79: :: CAT_3:79
theorem Th80: :: CAT_3:80
theorem Th81: :: CAT_3:81
theorem :: CAT_3:82
theorem :: CAT_3:83
:: deftheorem Def19 defines is_a_coproduct_wrt CAT_3:def 19 :
theorem :: CAT_3:84
theorem Th85: :: CAT_3:85
theorem :: CAT_3:86
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 ) ) ) )
theorem :: CAT_3:88
theorem Th89: :: CAT_3:89
theorem :: CAT_3:90
theorem :: CAT_3:91
theorem :: CAT_3:92