:: CAT_3 semantic presentation

definition

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
let c₄ be set ;
assume E1: c₄ in c₁ ;
redefine func c₃ /. c₄ -> Element of a₂ equals :Def1: :: CAT_3:def 1
a₃ . a₄;
compatibility

proof end;

end;

:: deftheorem Def1 defines /. CAT_3:def 1 :

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

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

proof end;

theorem Th1: :: CAT_3:1

for b₁ being set
for b₂ being non empty set
for b₃, b₄ being Function of b₁,b₂ st ( for b₅ being set st b₅ in b₁ holds
b₃ /. b₅ = b₄ /. b₅ ) holds
b₃ = b₄

proof end;

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

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

proof end;

definition

let c₁ be non empty set ;
let c₂ be set ;
let c₃ be Element of c₁;
redefine func --> as c₂ --> c₃ -> Function of a₂,a₁;
coherence by FUNCOP_1:58;

end;

definition

let c₁ be non empty set ;
let c₂ be set ;
let c₃ be Element of c₁;
redefine func .--> as c₂ .--> c₃ -> Function of {a₂},a₁;
coherence by FUNCOP_1:58;

end;

theorem Th2: :: CAT_3:2

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being Element of b₃ st b₂ in b₁ holds
(b₁ --> b₄) /. b₂ = b₄

proof end;

theorem Th3: :: CAT_3:3

canceled;

theorem Th4: :: CAT_3:4

canceled;

theorem Th5: :: CAT_3:5

canceled;

theorem Th6: :: CAT_3:6

canceled;

theorem Th7: :: CAT_3:7

for b₁, b₂ being set
for b₃ being non empty set st b₁ <> b₂ holds
for b₄, b₅ being Element of b₃ holds
( (b₁,b₂ --> b₄,b₅) /. b₁ = b₄ & (b₁,b₂ --> b₄,b₅) /. b₂ = b₅ )

proof end;

definition

let c₁ be Category;
let c₂ be set ;
let c₃ be Function of c₂,the Morphisms of c₁;
canceled;
func doms c₃ -> Function of a₂,the Objects of a₁ means :Def3: :: CAT_3:def 3
for b₁ being set st b₁ in a₂ holds
a₄ /. b₁ = dom (a₃ /. b₁);
correctness

proof end;

func cods c₃ -> Function of a₂,the Objects of a₁ means :Def4: :: CAT_3:def 4
for b₁ being set st b₁ in a₂ holds
a₄ /. b₁ = cod (a₃ /. b₁);
correctness

proof end;

end;

:: deftheorem Def2 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 b₁ being set
for b₂ being Category
for b₃ being Morphism of b₂ holds doms (b₁ --> b₃) = b₁ --> (dom b₃)

proof end;

theorem Th9: :: CAT_3:9

for b₁ being set
for b₂ being Category
for b₃ being Morphism of b₂ holds cods (b₁ --> b₃) = b₁ --> (cod b₃)

proof end;

theorem Th10: :: CAT_3:10

for b₁, b₂ being set
for b₃ being Category
for b₄, b₅ being Morphism of b₃ holds doms (b₁,b₂ --> b₄,b₅) = b₁,b₂ --> (dom b₄),(dom b₅)

proof end;

theorem Th11: :: CAT_3:11

for b₁, b₂ being set
for b₃ being Category
for b₄, b₅ being Morphism of b₃ holds cods (b₁,b₂ --> b₄,b₅) = b₁,b₂ --> (cod b₄),(cod b₅)

proof end;

definition

let c₁ be Category;
let c₂ be set ;
let c₃ be Function of c₂,the Morphisms of c₁;
func c₃ opp -> Function of a₂,the Morphisms of (a₁ opp ) means :Def5: :: CAT_3:def 5
for b₁ being set st b₁ in a₂ holds
a₄ /. b₁ = (a₃ /. b₁) opp ;
correctness

proof end;

end;

:: deftheorem Def5 defines opp CAT_3:def 5 :

theorem Th12: :: CAT_3:12

for b₁ being set
for b₂ being Category
for b₃ being Morphism of b₂ holds (b₁ --> b₃) opp = b₁ --> (b₃ opp )

proof end;

theorem Th13: :: CAT_3:13

for b₁, b₂ being set
for b₃ being Category
for b₄, b₅ being Morphism of b₃ st b₁ <> b₂ holds
(b₁,b₂ --> b₄,b₅) opp = b₁,b₂ --> (b₄ opp ),(b₅ opp )

proof end;

theorem Th14: :: CAT_3:14

for b₁ being set
for b₂ being Category
for b₃ being Function of b₁,the Morphisms of b₂ holds (b₃ opp ) opp = b₃

proof end;

definition

let c₁ be Category;
let c₂ be set ;
let c₃ be Function of c₂,the Morphisms of (c₁ opp );
func opp c₃ -> Function of a₂,the Morphisms of a₁ means :Def6: :: CAT_3:def 6
for b₁ being set st b₁ in a₂ holds
a₄ /. b₁ = opp (a₃ /. b₁);
correctness

proof end;

end;

:: deftheorem Def6 defines opp CAT_3:def 6 :

theorem Th15: :: CAT_3:15

for b₁ being set
for b₂ being Category
for b₃ being Morphism of (b₂ opp ) holds opp (b₁ --> b₃) = b₁ --> (opp b₃)

proof end;

theorem Th16: :: CAT_3:16

for b₁, b₂ being set
for b₃ being Category st b₁ <> b₂ holds
for b₄, b₅ being Morphism of (b₃ opp ) holds opp (b₁,b₂ --> b₄,b₅) = b₁,b₂ --> (opp b₄),(opp b₅)

proof end;

theorem Th17: :: CAT_3:17

for b₁ being set
for b₂ being Category
for b₃ being Function of b₁,the Morphisms of b₂ holds opp (b₃ opp ) = b₃

proof end;

definition

let c₁ be Category;
let c₂ be set ;
let c₃ be Function of c₂,the Morphisms of c₁;
let c₄ be Morphism of c₁;
func c₃ * c₄ -> Function of a₂,the Morphisms of a₁ means :Def7: :: CAT_3:def 7
for b₁ being set st b₁ in a₂ holds
a₅ /. b₁ = (a₃ /. b₁) * a₄;
correctness

proof end;

func c₄ * c₃ -> Function of a₂,the Morphisms of a₁ means :Def8: :: CAT_3:def 8
for b₁ being set st b₁ in a₂ holds
a₅ /. b₁ = a₄ * (a₃ /. b₁);
correctness

proof end;

end;

:: deftheorem Def7 defines * CAT_3:def 7 :

:: deftheorem Def8 defines * CAT_3:def 8 :

theorem Th18: :: CAT_3:18

for b₁, b₂ being set
for b₃ being Category
for b₄, b₅, b₆ being Morphism of b₃ st b₁ <> b₂ holds
(b₁,b₂ --> b₄,b₅) * b₆ = b₁,b₂ --> (b₄ * b₆),(b₅ * b₆)

proof end;

theorem Th19: :: CAT_3:19

for b₁, b₂ being set
for b₃ being Category
for b₄, b₅, b₆ being Morphism of b₃ st b₁ <> b₂ holds
b₄ * (b₁,b₂ --> b₅,b₆) = b₁,b₂ --> (b₄ * b₅),(b₄ * b₆)

proof end;

theorem Th20: :: CAT_3:20

for b₁ being set
for b₂ being Category
for b₃ being Morphism of b₂
for b₄ being Function of b₁,the Morphisms of b₂ st doms b₄ = b₁ --> (cod b₃) holds
( doms (b₄ * b₃) = b₁ --> (dom b₃) & cods (b₄ * b₃) = cods b₄ )

proof end;

theorem Th21: :: CAT_3:21

for b₁ being set
for b₂ being Category
for b₃ being Morphism of b₂
for b₄ being Function of b₁,the Morphisms of b₂ st cods b₄ = b₁ --> (dom b₃) holds
( doms (b₃ * b₄) = doms b₄ & cods (b₃ * b₄) = b₁ --> (cod b₃) )

proof end;

definition

let c₁ be Category;
let c₂ be set ;
let c₃, c₄ be Function of c₂,the Morphisms of c₁;
func c₃ "*" c₄ -> Function of a₂,the Morphisms of a₁ means :Def9: :: CAT_3:def 9
for b₁ being set st b₁ in a₂ holds
a₅ /. b₁ = (a₃ /. b₁) * (a₄ /. b₁);
correctness

proof end;

end;

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

theorem Th22: :: CAT_3:22

for b₁ being set
for b₂ being Category
for b₃, b₄ being Function of b₁,the Morphisms of b₂ st doms b₃ = cods b₄ holds
( doms (b₃ "*" b₄) = doms b₄ & cods (b₃ "*" b₄) = cods b₃ )

proof end;

theorem Th23: :: CAT_3:23

for b₁, b₂ being set
for b₃ being Category
for b₄, b₅, b₆, b₇ being Morphism of b₃ st b₁ <> b₂ holds
(b₁,b₂ --> b₄,b₅) "*" (b₁,b₂ --> b₆,b₇) = b₁,b₂ --> (b₄ * b₆),(b₅ * b₇)

proof end;

theorem Th24: :: CAT_3:24

for b₁ being set
for b₂ being Category
for b₃ being Morphism of b₂
for b₄ being Function of b₁,the Morphisms of b₂ holds b₄ * b₃ = b₄ "*" (b₁ --> b₃)

proof end;

theorem Th25: :: CAT_3:25

for b₁ being set
for b₂ being Category
for b₃ being Morphism of b₂
for b₄ being Function of b₁,the Morphisms of b₂ holds b₃ * b₄ = (b₁ --> b₃) "*" b₄

proof end;

definition

let c₁ be Category;
let c₂ be Morphism of c₁;
attr a₂ is retraction means :Def10: :: CAT_3:def 10
ex b₁ being Morphism of a₁ st
( cod b₁ = dom a₂ & a₂ * b₁ = id (cod a₂) );
attr a₂ is coretraction means :Def11: :: CAT_3:def 11
ex b₁ being Morphism of a₁ st
( dom b₁ = cod a₂ & b₁ * a₂ = id (dom a₂) );

end;

:: deftheorem Def10 defines retraction CAT_3:def 10 :

:: deftheorem Def11 defines coretraction CAT_3:def 11 :

theorem Th26: :: CAT_3:26

for b₁ being Category
for b₂ being Morphism of b₁ st b₂ is retraction holds
b₂ is epi

proof end;

theorem Th27: :: CAT_3:27

for b₁ being Category
for b₂ being Morphism of b₁ st b₂ is coretraction holds
b₂ is monic

proof end;

theorem Th28: :: CAT_3:28

for b₁ being Category
for b₂, b₃ being Morphism of b₁ st b₂ is retraction & b₃ is retraction & dom b₃ = cod b₂ holds
b₃ * b₂ is retraction

proof end;

theorem Th29: :: CAT_3:29

for b₁ being Category
for b₂, b₃ being Morphism of b₁ st b₂ is coretraction & b₃ is coretraction & dom b₃ = cod b₂ holds
b₃ * b₂ is coretraction

proof end;

theorem Th30: :: CAT_3:30

for b₁ being Category
for b₂, b₃ being Morphism of b₁ st dom b₂ = cod b₃ & b₂ * b₃ is retraction holds
b₂ is retraction

proof end;

theorem Th31: :: CAT_3:31

for b₁ being Category
for b₂, b₃ being Morphism of b₁ st dom b₂ = cod b₃ & b₂ * b₃ is coretraction holds
b₃ is coretraction

proof end;

theorem Th32: :: CAT_3:32

for b₁ being Category
for b₂ being Morphism of b₁ st b₂ is retraction & b₂ is monic holds
b₂ is invertible

proof end;

theorem Th33: :: CAT_3:33

for b₁ being Category
for b₂ being Morphism of b₁ st b₂ is coretraction & b₂ is epi holds
b₂ is invertible

proof end;

theorem Th34: :: CAT_3:34

for b₁ being Category
for b₂ being Morphism of b₁ holds
( b₂ is invertible iff ( b₂ is retraction & b₂ is coretraction ) )

proof end;

theorem Th35: :: CAT_3:35

for b₁, b₂ being Category
for b₃ being Morphism of b₁
for b₄ being Functor of b₁,b₂ st b₃ is retraction holds
b₄ . b₃ is retraction

proof end;

theorem Th36: :: CAT_3:36

for b₁, b₂ being Category
for b₃ being Morphism of b₁
for b₄ being Functor of b₁,b₂ st b₃ is coretraction holds
b₄ . b₃ is coretraction

proof end;

theorem Th37: :: CAT_3:37

for b₁ being Category
for b₂ being Morphism of b₁ holds
( b₂ is retraction iff b₂ opp is coretraction )

proof end;

theorem Th38: :: CAT_3:38

for b₁ being Category
for b₂ being Morphism of b₁ holds
( b₂ is coretraction iff b₂ opp is retraction )

proof end;

definition

let c₁ be Category;
let c₂, c₃ be Object of c₁;
assume E25: c₃ is terminal ;
func term c₂,c₃ -> Morphism of a₂,a₃ means :: CAT_3:def 12
verum;
existence ;
uniqueness

proof end;

end;

:: deftheorem Def12 defines term CAT_3:def 12 :

theorem Th39: :: CAT_3:39

for b₁ being Category
for b₂, b₃ being Object of b₁ st b₂ is terminal holds
( dom (term b₃,b₂) = b₃ & cod (term b₃,b₂) = b₂ )

proof end;

theorem Th40: :: CAT_3:40

for b₁ being Category
for b₂, b₃ being Object of b₁
for b₄ being Morphism of b₁ st b₂ is terminal & dom b₄ = b₃ & cod b₄ = b₂ holds
term b₃,b₂ = b₄

proof end;

theorem Th41: :: CAT_3:41

for b₁ being Category
for b₂, b₃ being Object of b₁
for b₄ being Morphism of b₂,b₃ st b₃ is terminal holds
term b₂,b₃ = b₄

proof end;

definition

let c₁ be Category;
let c₂, c₃ be Object of c₁;
assume E27: c₂ is initial ;
func init c₂,c₃ -> Morphism of a₂,a₃ means :: CAT_3:def 13
verum;
existence ;
uniqueness

proof end;

end;

:: deftheorem Def13 defines init CAT_3:def 13 :

theorem Th42: :: CAT_3:42

for b₁ being Category
for b₂, b₃ being Object of b₁ st b₂ is initial holds
( dom (init b₂,b₃) = b₂ & cod (init b₂,b₃) = b₃ )

proof end;

theorem Th43: :: CAT_3:43

for b₁ being Category
for b₂, b₃ being Object of b₁
for b₄ being Morphism of b₁ st b₂ is initial & dom b₄ = b₂ & cod b₄ = b₃ holds
init b₂,b₃ = b₄

proof end;

theorem Th44: :: CAT_3:44

for b₁ being Category
for b₂, b₃ being Object of b₁
for b₄ being Morphism of b₂,b₃ st b₂ is initial holds
init b₂,b₃ = b₄

proof end;

definition

let c₁ be Category;
let c₂ be Object of c₁;
let c₃ be set ;
mode Projections_family of c₂,c₃ -> Function of a₃,the Morphisms of a₁ means :Def14: :: CAT_3:def 14
doms a₄ = a₃ --> a₂;
existence

proof end;

end;

:: deftheorem Def14 defines Projections_family CAT_3:def 14 :

theorem Th45: :: CAT_3:45

for b₁, b₂ being set
for b₃ being Category
for b₄ being Object of b₃
for b₅ being Projections_family of b₄,b₁ st b₂ in b₁ holds
dom (b₅ /. b₂) = b₄

proof end;

theorem Th46: :: CAT_3:46

for b₁ being Category
for b₂ being Object of b₁
for b₃ being Function of {} ,the Morphisms of b₁ holds b₃ is Projections_family of b₂, {}

proof end;

theorem Th47: :: CAT_3:47

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Morphism of b₂ st dom b₄ = b₃ holds
b₁ .--> b₄ is Projections_family of b₃,{b₁}

proof end;

theorem Th48: :: CAT_3:48

for b₁, b₂ being set
for b₃ being Category
for b₄ being Object of b₃
for b₅, b₆ being Morphism of b₃ st dom b₅ = b₄ & dom b₆ = b₄ holds
b₁,b₂ --> b₅,b₆ is Projections_family of b₄,{b₁,b₂}

proof end;

theorem Th49: :: CAT_3:49

canceled;

theorem Th50: :: CAT_3:50

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Morphism of b₂
for b₅ being Projections_family of b₃,b₁ st cod b₄ = b₃ holds
b₅ * b₄ is Projections_family of dom b₄,b₁

proof end;

theorem Th51: :: CAT_3:51

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Function of b₁,the Morphisms of b₂
for b₅ being Projections_family of b₃,b₁ st doms b₄ = cods b₅ holds
b₄ "*" b₅ is Projections_family of b₃,b₁

proof end;

theorem Th52: :: CAT_3:52

for b₁ being set
for b₂ being Category
for b₃ being Morphism of b₂
for b₄ being Projections_family of cod b₃,b₁ holds (b₃ opp ) * (b₄ opp ) = (b₄ * b₃) opp

proof end;

definition

let c₁ be Category;
let c₂ be Object of c₁;
let c₃ be set ;
let c₄ be Function of c₃,the Morphisms of c₁;
pred c₂ is_a_product_wrt c₄ means :Def15: :: CAT_3:def 15
( a₄ is Projections_family of a₂,a₃ & ( for b₁ being Object of a₁
for b₂ being Projections_family of b₁,a₃ st cods a₄ = cods b₂ holds
ex b₃ being Morphism of a₁ st
( b₃ in Hom b₁,a₂ & ( for b₄ being Morphism of a₁ st b₄ in Hom b₁,a₂ holds
( ( for b₅ being set st b₅ in a₃ holds
(a₄ /. b₅) * b₄ = b₂ /. b₅ ) iff b₃ = b₄ ) ) ) ) );

end;

:: deftheorem Def15 defines is_a_product_wrt CAT_3:def 15 :

theorem Th53: :: CAT_3:53

for b₁ being set
for b₂ being Category
for b₃, b₄ being Object of b₂
for b₅ being Projections_family of b₃,b₁
for b₆ being Projections_family of b₄,b₁ st b₃ is_a_product_wrt b₅ & b₄ is_a_product_wrt b₆ & cods b₅ = cods b₆ holds
b₃,b₄ are_isomorphic

proof end;

theorem Th54: :: CAT_3:54

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Projections_family of b₃,b₁ st b₃ is_a_product_wrt b₄ & ( for b₅, b₆ being set st b₅ in b₁ & b₆ in b₁ holds
Hom (cod (b₄ /. b₅)),(cod (b₄ /. b₆)) <> {} ) holds
for b₅ being set st b₅ in b₁ holds
b₄ /. b₅ is retraction

proof end;

theorem Th55: :: CAT_3:55

for b₁ being Category
for b₂ being Object of b₁
for b₃ being Function of {} ,the Morphisms of b₁ holds
( b₂ is_a_product_wrt b₃ iff b₂ is terminal )

proof end;

theorem Th56: :: CAT_3:56

for b₁ being set
for b₂ being Category
for b₃, b₄ being Object of b₂
for b₅ being Morphism of b₂
for b₆ being Projections_family of b₃,b₁ st b₃ is_a_product_wrt b₆ & dom b₅ = b₄ & cod b₅ = b₃ & b₅ is invertible holds
b₄ is_a_product_wrt b₆ * b₅

proof end;

theorem Th57: :: CAT_3:57

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂ holds b₃ is_a_product_wrt b₁ .--> (id b₃)

proof end;

theorem Th58: :: CAT_3:58

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Projections_family of b₃,b₁ st b₃ is_a_product_wrt b₄ & ( for b₅ being set st b₅ in b₁ holds
cod (b₄ /. b₅) is terminal ) holds
b₃ is terminal

proof end;

definition

let c₁ be Category;
let c₂ be Object of c₁;
let c₃, c₄ be Morphism of c₁;
pred c₂ is_a_product_wrt c₃,c₄ means :Def16: :: CAT_3:def 16
( dom a₃ = a₂ & dom a₄ = a₂ & ( for b₁ being Object of a₁
for b₂, b₃ being Morphism of a₁ st b₂ in Hom b₁,(cod a₃) & b₃ in Hom b₁,(cod a₄) holds
ex b₄ being Morphism of a₁ st
( b₄ in Hom b₁,a₂ & ( for b₅ being Morphism of a₁ st b₅ in Hom b₁,a₂ holds
( ( a₃ * b₅ = b₂ & a₄ * b₅ = b₃ ) iff b₄ = b₅ ) ) ) ) );

end;

:: deftheorem Def16 defines is_a_product_wrt CAT_3:def 16 :

theorem Th59: :: CAT_3:59

for b₁, b₂ being set
for b₃ being Category
for b₄ being Object of b₃
for b₅, b₆ being Morphism of b₃ st b₁ <> b₂ holds
( b₄ is_a_product_wrt b₅,b₆ iff b₄ is_a_product_wrt b₁,b₂ --> b₅,b₆ )

proof end;

theorem Th60: :: CAT_3:60

for b₁ being Category
for b₂, b₃, b₄ being Object of b₁ st Hom b₂,b₃ <> {} & Hom b₂,b₄ <> {} holds
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₂,b₄ holds
( b₂ is_a_product_wrt b₅,b₆ iff for b₇ being Object of b₁ st Hom b₇,b₃ <> {} & Hom b₇,b₄ <> {} holds
( Hom b₇,b₂ <> {} & ( for b₈ being Morphism of b₇,b₃
for b₉ being Morphism of b₇,b₄ ex b₁₀ being Morphism of b₇,b₂ st
for b₁₁ being Morphism of b₇,b₂ holds
( ( b₅ * b₁₁ = b₈ & b₆ * b₁₁ = b₉ ) iff b₁₀ = b₁₁ ) ) ) )

proof end;

theorem Th61: :: CAT_3:61

for b₁ being Category
for b₂, b₃ being Object of b₁
for b₄, b₅, b₆, b₇ being Morphism of b₁ st b₂ is_a_product_wrt b₄,b₅ & b₃ is_a_product_wrt b₆,b₇ & cod b₄ = cod b₆ & cod b₅ = cod b₇ holds
b₂,b₃ are_isomorphic

proof end;

theorem Th62: :: CAT_3:62

for b₁ being Category
for b₂ being Object of b₁
for b₃, b₄ being Morphism of b₁ st b₂ is_a_product_wrt b₃,b₄ & Hom (cod b₃),(cod b₄) <> {} & Hom (cod b₄),(cod b₃) <> {} holds
( b₃ is retraction & b₄ is retraction )

proof end;

theorem Th63: :: CAT_3:63

for b₁ being Category
for b₂ being Object of b₁
for b₃, b₄, b₅ being Morphism of b₁ st b₂ is_a_product_wrt b₃,b₄ & b₅ in Hom b₂,b₂ & b₃ * b₅ = b₃ & b₄ * b₅ = b₄ holds
b₅ = id b₂

proof end;

theorem Th64: :: CAT_3:64

for b₁ being Category
for b₂, b₃ being Object of b₁
for b₄, b₅, b₆ being Morphism of b₁ st b₂ is_a_product_wrt b₄,b₅ & dom b₆ = b₃ & cod b₆ = b₂ & b₆ is invertible holds
b₃ is_a_product_wrt b₄ * b₆,b₅ * b₆

proof end;

theorem Th65: :: CAT_3:65

for b₁ being Category
for b₂ being Object of b₁
for b₃, b₄ being Morphism of b₁ st b₂ is_a_product_wrt b₃,b₄ & cod b₄ is terminal holds
b₂, cod b₃ are_isomorphic

proof end;

theorem Th66: :: CAT_3:66

for b₁ being Category
for b₂ being Object of b₁
for b₃, b₄ being Morphism of b₁ st b₂ is_a_product_wrt b₃,b₄ & cod b₃ is terminal holds
b₂, cod b₄ are_isomorphic

proof end;

definition

let c₁ be Category;
let c₂ be Object of c₁;
let c₃ be set ;
mode Injections_family of c₂,c₃ -> Function of a₃,the Morphisms of a₁ means :Def17: :: CAT_3:def 17
cods a₄ = a₃ --> a₂;
existence

proof end;

end;

:: deftheorem Def17 defines Injections_family CAT_3:def 17 :

theorem Th67: :: CAT_3:67

for b₁, b₂ being set
for b₃ being Category
for b₄ being Object of b₃
for b₅ being Injections_family of b₄,b₁ st b₂ in b₁ holds
cod (b₅ /. b₂) = b₄

proof end;

theorem Th68: :: CAT_3:68

for b₁ being Category
for b₂ being Object of b₁
for b₃ being Function of {} ,the Morphisms of b₁ holds b₃ is Injections_family of b₂, {}

proof end;

theorem Th69: :: CAT_3:69

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Morphism of b₂ st cod b₄ = b₃ holds
b₁ .--> b₄ is Injections_family of b₃,{b₁}

proof end;

theorem Th70: :: CAT_3:70

for b₁, b₂ being set
for b₃ being Category
for b₄ being Object of b₃
for b₅, b₆ being Morphism of b₃ st cod b₅ = b₄ & cod b₆ = b₄ holds
b₁,b₂ --> b₅,b₆ is Injections_family of b₄,{b₁,b₂}

proof end;

theorem Th71: :: CAT_3:71

canceled;

theorem Th72: :: CAT_3:72

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Morphism of b₂
for b₅ being Injections_family of b₃,b₁ st dom b₄ = b₃ holds
b₄ * b₅ is Injections_family of cod b₄,b₁

proof end;

theorem Th73: :: CAT_3:73

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Injections_family of b₃,b₁
for b₅ being Function of b₁,the Morphisms of b₂ st doms b₄ = cods b₅ holds
b₄ "*" b₅ is Injections_family of b₃,b₁

proof end;

theorem Th74: :: CAT_3:74

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Function of b₁,the Morphisms of b₂ holds
( b₄ is Projections_family of b₃,b₁ iff b₄ opp is Injections_family of b₃ opp ,b₁ )

proof end;

theorem Th75: :: CAT_3:75

for b₁ being set
for b₂ being Category
for b₃ being Function of b₁,the Morphisms of (b₂ opp )
for b₄ being Object of (b₂ opp ) holds
( b₃ is Injections_family of b₄,b₁ iff opp b₃ is Projections_family of opp b₄,b₁ )

proof end;

theorem Th76: :: CAT_3:76

for b₁ being set
for b₂ being Category
for b₃ being Morphism of b₂
for b₄ being Injections_family of dom b₃,b₁ holds (b₄ opp ) * (b₃ opp ) = (b₃ * b₄) opp

proof end;

definition

let c₁ be Category;
let c₂ be Object of c₁;
let c₃ be set ;
let c₄ be Function of c₃,the Morphisms of c₁;
pred c₂ is_a_coproduct_wrt c₄ means :Def18: :: CAT_3:def 18
( a₄ is Injections_family of a₂,a₃ & ( for b₁ being Object of a₁
for b₂ being Injections_family of b₁,a₃ st doms a₄ = doms b₂ holds
ex b₃ being Morphism of a₁ st
( b₃ in Hom a₂,b₁ & ( for b₄ being Morphism of a₁ st b₄ in Hom a₂,b₁ holds
( ( for b₅ being set st b₅ in a₃ holds
b₄ * (a₄ /. b₅) = b₂ /. b₅ ) iff b₃ = b₄ ) ) ) ) );

end;

:: deftheorem Def18 defines is_a_coproduct_wrt CAT_3:def 18 :

theorem Th77: :: CAT_3:77

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Function of b₁,the Morphisms of b₂ holds
( b₃ is_a_product_wrt b₄ iff b₃ opp is_a_coproduct_wrt b₄ opp )

proof end;

theorem Th78: :: CAT_3:78

for b₁ being set
for b₂ being Category
for b₃, b₄ being Object of b₂
for b₅ being Injections_family of b₃,b₁
for b₆ being Injections_family of b₄,b₁ st b₃ is_a_coproduct_wrt b₅ & b₄ is_a_coproduct_wrt b₆ & doms b₅ = doms b₆ holds
b₃,b₄ are_isomorphic

proof end;

theorem Th79: :: CAT_3:79

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Injections_family of b₃,b₁ st b₃ is_a_coproduct_wrt b₄ & ( for b₅, b₆ being set st b₅ in b₁ & b₆ in b₁ holds
Hom (dom (b₄ /. b₅)),(dom (b₄ /. b₆)) <> {} ) holds
for b₅ being set st b₅ in b₁ holds
b₄ /. b₅ is coretraction

proof end;

theorem Th80: :: CAT_3:80

for b₁ being set
for b₂ being Category
for b₃, b₄ being Object of b₂
for b₅ being Morphism of b₂
for b₆ being Injections_family of b₃,b₁ st b₃ is_a_coproduct_wrt b₆ & dom b₅ = b₃ & cod b₅ = b₄ & b₅ is invertible holds
b₄ is_a_coproduct_wrt b₅ * b₆

proof end;

theorem Th81: :: CAT_3:81

for b₁ being Category
for b₂ being Object of b₁
for b₃ being Injections_family of b₂, {} holds
( b₂ is_a_coproduct_wrt b₃ iff b₂ is initial )

proof end;

theorem Th82: :: CAT_3:82

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂ holds b₃ is_a_coproduct_wrt b₁ .--> (id b₃)

proof end;

theorem Th83: :: CAT_3:83

for b₁ being set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Injections_family of b₃,b₁ st b₃ is_a_coproduct_wrt b₄ & ( for b₅ being set st b₅ in b₁ holds
dom (b₄ /. b₅) is initial ) holds
b₃ is initial

proof end;

definition

let c₁ be Category;
let c₂ be Object of c₁;
let c₃, c₄ be Morphism of c₁;
pred c₂ is_a_coproduct_wrt c₃,c₄ means :Def19: :: CAT_3:def 19
( cod a₃ = a₂ & cod a₄ = a₂ & ( for b₁ being Object of a₁
for b₂, b₃ being Morphism of a₁ st b₂ in Hom (dom a₃),b₁ & b₃ in Hom (dom a₄),b₁ holds
ex b₄ being Morphism of a₁ st
( b₄ in Hom a₂,b₁ & ( for b₅ being Morphism of a₁ st b₅ in Hom a₂,b₁ holds
( ( b₅ * a₃ = b₂ & b₅ * a₄ = b₃ ) iff b₄ = b₅ ) ) ) ) );

end;

:: deftheorem Def19 defines is_a_coproduct_wrt CAT_3:def 19 :

theorem Th84: :: CAT_3:84

for b₁ being Category
for b₂ being Object of b₁
for b₃, b₄ being Morphism of b₁ holds
( b₂ is_a_product_wrt b₃,b₄ iff b₂ opp is_a_coproduct_wrt b₃ opp ,b₄ opp )

proof end;

theorem Th85: :: CAT_3:85

for b₁, b₂ being set
for b₃ being Category
for b₄ being Object of b₃
for b₅, b₆ being Morphism of b₃ st b₁ <> b₂ holds
( b₄ is_a_coproduct_wrt b₅,b₆ iff b₄ is_a_coproduct_wrt b₁,b₂ --> b₅,b₆ )

proof end;

theorem Th86: :: CAT_3:86

for b₁ being Category
for b₂, b₃ being Object of b₁
for b₄, b₅, b₆, b₇ being Morphism of b₁ st b₂ is_a_coproduct_wrt b₄,b₅ & b₃ is_a_coproduct_wrt b₆,b₇ & dom b₄ = dom b₆ & dom b₅ = dom b₇ holds
b₂,b₃ are_isomorphic

proof end;

theorem Th87: :: CAT_3:87

for b₁ being Category
for b₂, b₃, b₄ being Object of b₁ st Hom b₂,b₃ <> {} & Hom b₄,b₃ <> {} holds
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₄,b₃ holds
( b₃ is_a_coproduct_wrt b₅,b₆ iff for b₇ being Object of b₁ st Hom b₂,b₇ <> {} & Hom b₄,b₇ <> {} holds
( Hom b₃,b₇ <> {} & ( for b₈ being Morphism of b₂,b₇
for b₉ being Morphism of b₄,b₇ ex b₁₀ being Morphism of b₃,b₇ st
for b₁₁ being Morphism of b₃,b₇ holds
( ( b₁₁ * b₅ = b₈ & b₁₁ * b₆ = b₉ ) iff b₁₀ = b₁₁ ) ) ) )

proof end;

theorem Th88: :: CAT_3:88

for b₁ being Category
for b₂ being Object of b₁
for b₃, b₄ being Morphism of b₁ st b₂ is_a_coproduct_wrt b₃,b₄ & Hom (dom b₃),(dom b₄) <> {} & Hom (dom b₄),(dom b₃) <> {} holds
( b₃ is coretraction & b₄ is coretraction )

proof end;

theorem Th89: :: CAT_3:89

for b₁ being Category
for b₂ being Object of b₁
for b₃, b₄, b₅ being Morphism of b₁ st b₂ is_a_coproduct_wrt b₃,b₄ & b₅ in Hom b₂,b₂ & b₅ * b₃ = b₃ & b₅ * b₄ = b₄ holds
b₅ = id b₂

proof end;

theorem Th90: :: CAT_3:90

for b₁ being Category
for b₂, b₃ being Object of b₁
for b₄, b₅, b₆ being Morphism of b₁ st b₂ is_a_coproduct_wrt b₄,b₅ & dom b₆ = b₂ & cod b₆ = b₃ & b₆ is invertible holds
b₃ is_a_coproduct_wrt b₆ * b₄,b₆ * b₅

proof end;

theorem Th91: :: CAT_3:91

for b₁ being Category
for b₂ being Object of b₁
for b₃, b₄ being Morphism of b₁ st b₂ is_a_coproduct_wrt b₃,b₄ & dom b₄ is initial holds
dom b₃,b₂ are_isomorphic

proof end;

theorem Th92: :: CAT_3:92

for b₁ being Category
for b₂ being Object of b₁
for b₃, b₄ being Morphism of b₁ st b₂ is_a_coproduct_wrt b₃,b₄ & dom b₃ is initial holds
dom b₄,b₂ are_isomorphic

proof end;