:: Coproducts in Categories without Uniqueness of { \bf cod } and { \bf dom}
:: by Maciej Goli\'nski and Artur Korni{\l}owicz
::
:: Received December 8, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users

set C = EnsCat {{}};

Lm1: the carrier of (EnsCat {{}}) = {0}
by ALTCAT_1:def 14;

Lm2: Funcs ({},{}) = {{}}
by FUNCT_5:57;

Lm3: now :: thesis: for o1, o being Object of (EnsCat {{}}) holds
( {} is Morphism of o1,o & {} in <^o1,o^> )

let o1, o be Object of (EnsCat {{}}); :: thesis: ( {} is Morphism of o1,o & {} in <^o1,o^> )
A1: ( o1 = {} & o = {} ) by Lm1, TARSKI:def 1;
<^o1,o^> = Funcs (o1,o) by ALTCAT_1:def 14;
hence ( {} is Morphism of o1,o & {} in <^o1,o^> ) by A1, Lm1, Lm2; :: thesis: verum

end;

Lm4: now :: thesis: for o1, o being Object of (EnsCat {{}})
for m1 being Morphism of o1,o holds m1 = {}

let o1, o be Object of (EnsCat {{}}); :: thesis: for m1 being Morphism of o1,o holds m1 = {}
let m1 be Morphism of o1,o; :: thesis: m1 = {}
A1: ( o = {} & o1 = {} ) by Lm1, TARSKI:def 1;
<^o1,o^> = Funcs (o1,o) by ALTCAT_1:def 14;
hence m1 = {} by A1, Lm2, TARSKI:def 1; :: thesis: verum

end;

Lm5: now :: thesis: for o1, o being Object of (EnsCat {{}}) holds o1 = o

let o1, o be Object of (EnsCat {{}}); :: thesis: o1 = o
( o = {} & o1 = {} ) by Lm1, TARSKI:def 1;
hence o1 = o ; :: thesis: verum

end;

Lm6: now :: thesis: for o1, o being Object of (EnsCat {{}})
for m1, m being Morphism of o1,o holds m1 = m

let o1, o be Object of (EnsCat {{}}); :: thesis: for m1, m being Morphism of o1,o holds m1 = m
let m1, m be Morphism of o1,o; :: thesis: m1 = m
thus m1 = {} by Lm4
.= m by Lm4 ; :: thesis: verum

end;

registration

let I be non empty set ;
let A be ManySortedSet of I;
let i be Element of I;

cluster coprod (i,A) -> Relation-like Function-like ;

coherence
( coprod (i,A) is Relation-like & coprod (i,A) is Function-like )

proof end;

end;

definition

let C be non empty AltCatStr ;
let o be Object of C;
let I be set ;
let f be ObjectsFamily of I,C;

mode MorphismsFamily of f,o -> ManySortedSet of I means :Def1: :: ALTCAT_6:def 1
for i being object st i in I holds
ex o1 being Object of C st
( o1 = f . i & it . i is Morphism of o1,o );

existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
ex o1 being Object of C st
( o1 = f . i & b₁ . i is Morphism of o1,o )

proof end;

end;

:: deftheorem Def1 defines MorphismsFamily ALTCAT_6:def 1 :
for C being non empty AltCatStr
for o being Object of C
for I being set
for f being ObjectsFamily of I,C
for b₅ being ManySortedSet of I holds
( b₅ is MorphismsFamily of f,o iff for i being object st i in I holds
ex o1 being Object of C st
( o1 = f . i & b₅ . i is Morphism of o1,o ) );

definition

let C be non empty AltCatStr ;
let o be Object of C;
let I be non empty set ;
let f be ObjectsFamily of I,C;

redefine mode MorphismsFamily of f,o means :Def2: :: ALTCAT_6:def 2
for i being Element of I holds it . i is Morphism of (f . i),o;

compatibility
for b₁ being ManySortedSet of I holds
( b₁ is MorphismsFamily of f,o iff for i being Element of I holds b₁ . i is Morphism of (f . i),o )

proof end;

end;

:: deftheorem Def2 defines MorphismsFamily ALTCAT_6:def 2 :
for C being non empty AltCatStr
for o being Object of C
for I being non empty set
for f being ObjectsFamily of I,C
for b₅ being ManySortedSet of I holds
( b₅ is MorphismsFamily of f,o iff for i being Element of I holds b₅ . i is Morphism of (f . i),o );

definition

let C be non empty AltCatStr ;
let o be Object of C;
let I be non empty set ;
let f be ObjectsFamily of I,C;
let M be MorphismsFamily of f,o;
let i be Element of I;
:: original: .
redefine func M . i -> Morphism of (f . i),o;
coherence
M . i is Morphism of (f . i),o by Def2;

end;

registration

let C be non empty functional AltCatStr ;
let o be Object of C;
let I be set ;
let f be ObjectsFamily of I,C;

cluster -> Function-yielding for MorphismsFamily of f,o;

coherence
for b₁ being MorphismsFamily of f,o holds b₁ is Function-yielding

proof end;

end;

theorem Th1: :: ALTCAT_6:1

for C being non empty AltCatStr
for o being Object of C
for f being ObjectsFamily of {},C holds {} is MorphismsFamily of f,o

proof end;

definition

let C be non empty AltCatStr ;
let I be set ;
let A be ObjectsFamily of I,C;
let B be Object of C;
let P be MorphismsFamily of A,B;

attr P is feasible means :: ALTCAT_6:def 3
for i being set st i in I holds
ex o being Object of C st
( o = A . i & P . i in <^o,B^> );

end;

:: deftheorem defines feasible ALTCAT_6:def 3 :
for C being non empty AltCatStr
for I being set
for A being ObjectsFamily of I,C
for B being Object of C
for P being MorphismsFamily of A,B holds
( P is feasible iff for i being set st i in I holds
ex o being Object of C st
( o = A . i & P . i in <^o,B^> ) );

definition

let C be non empty AltCatStr ;
let I be non empty set ;
let A be ObjectsFamily of I,C;
let B be Object of C;
let P be MorphismsFamily of A,B;

redefine attr P is feasible means :Def4: :: ALTCAT_6:def 4
for i being Element of I holds P . i in <^(A . i),B^>;

compatibility
( P is feasible iff for i being Element of I holds P . i in <^(A . i),B^> )

proof end;

end;

:: deftheorem Def4 defines feasible ALTCAT_6:def 4 :
for C being non empty AltCatStr
for I being non empty set
for A being ObjectsFamily of I,C
for B being Object of C
for P being MorphismsFamily of A,B holds
( P is feasible iff for i being Element of I holds P . i in <^(A . i),B^> );

definition

let C be category;
let I be set ;
let A be ObjectsFamily of I,C;
let B be Object of C;
let P be MorphismsFamily of A,B;

attr P is coprojection-morphisms means :: ALTCAT_6:def 5
for X being Object of C
for F being MorphismsFamily of A,X st F is feasible holds
ex f being Morphism of B,X st
( f in <^B,X^> & ( for i being set st i in I holds
ex si being Object of C ex Pi being Morphism of si,B st
( si = A . i & Pi = P . i & F . i = f * Pi ) ) & ( for f1 being Morphism of B,X st ( for i being set st i in I holds
ex si being Object of C ex Pi being Morphism of si,B st
( si = A . i & Pi = P . i & F . i = f1 * Pi ) ) holds
f = f1 ) );

end;

:: deftheorem defines coprojection-morphisms ALTCAT_6:def 5 :
for C being category
for I being set
for A being ObjectsFamily of I,C
for B being Object of C
for P being MorphismsFamily of A,B holds
( P is coprojection-morphisms iff for X being Object of C
for F being MorphismsFamily of A,X st F is feasible holds
ex f being Morphism of B,X st
( f in <^B,X^> & ( for i being set st i in I holds
ex si being Object of C ex Pi being Morphism of si,B st
( si = A . i & Pi = P . i & F . i = f * Pi ) ) & ( for f1 being Morphism of B,X st ( for i being set st i in I holds
ex si being Object of C ex Pi being Morphism of si,B st
( si = A . i & Pi = P . i & F . i = f1 * Pi ) ) holds
f = f1 ) ) );

definition

let C be category;
let I be non empty set ;
let A be ObjectsFamily of I,C;
let B be Object of C;
let P be MorphismsFamily of A,B;

redefine attr P is coprojection-morphisms means :: ALTCAT_6:def 6
for X being Object of C
for F being MorphismsFamily of A,X st F is feasible holds
ex f being Morphism of B,X st
( f in <^B,X^> & ( for i being Element of I holds F . i = f * (P . i) ) & ( for f1 being Morphism of B,X st ( for i being Element of I holds F . i = f1 * (P . i) ) holds
f = f1 ) );

correctness
compatibility
( P is coprojection-morphisms iff for X being Object of C
for F being MorphismsFamily of A,X st F is feasible holds
ex f being Morphism of B,X st
( f in <^B,X^> & ( for i being Element of I holds F . i = f * (P . i) ) & ( for f1 being Morphism of B,X st ( for i being Element of I holds F . i = f1 * (P . i) ) holds
f = f1 ) ) );

proof end;

end;

:: deftheorem defines coprojection-morphisms ALTCAT_6:def 6 :
for C being category
for I being non empty set
for A being ObjectsFamily of I,C
for B being Object of C
for P being MorphismsFamily of A,B holds
( P is coprojection-morphisms iff for X being Object of C
for F being MorphismsFamily of A,X st F is feasible holds
ex f being Morphism of B,X st
( f in <^B,X^> & ( for i being Element of I holds F . i = f * (P . i) ) & ( for f1 being Morphism of B,X st ( for i being Element of I holds F . i = f1 * (P . i) ) holds
f = f1 ) ) );

registration

let C be category;
let A be ObjectsFamily of {},C;
let B be Object of C;

cluster -> feasible for MorphismsFamily of A,B;

coherence
for b₁ being MorphismsFamily of A,B holds b₁ is feasible ;

end;

theorem Th2: :: ALTCAT_6:2

for C being category
for A being ObjectsFamily of {},C
for B being Object of C st B is initial holds
ex P being MorphismsFamily of A,B st
( P is empty & P is coprojection-morphisms )

proof end;

theorem Th3: :: ALTCAT_6:3

for I being set
for A being ObjectsFamily of I,(EnsCat {{}})
for o being Object of (EnsCat {{}}) holds I --> {} is MorphismsFamily of A,o

proof end;

theorem Th4: :: ALTCAT_6:4

for I being set
for A being ObjectsFamily of I,(EnsCat {{}})
for o being Object of (EnsCat {{}})
for P being MorphismsFamily of A,o st P = I --> {} holds
( P is feasible & P is coprojection-morphisms )

proof end;

definition

let C be category;

attr C is with_coproducts means :Def7: :: ALTCAT_6:def 7
for I being set
for A being ObjectsFamily of I,C ex B being Object of C ex P being MorphismsFamily of A,B st
( P is feasible & P is coprojection-morphisms );

end;

:: deftheorem Def7 defines with_coproducts ALTCAT_6:def 7 :
for C being category holds
( C is with_coproducts iff for I being set
for A being ObjectsFamily of I,C ex B being Object of C ex P being MorphismsFamily of A,B st
( P is feasible & P is coprojection-morphisms ) );

registration

cluster EnsCat {{}} -> with_coproducts ;

coherence
EnsCat {{}} is with_coproducts

proof end;

end;

registration

cluster non empty V62() strict V71() with_units with_products with_coproducts for AltCatStr ;

existence
ex b₁ being category st
( b₁ is with_products & b₁ is with_coproducts & b₁ is strict )

proof end;

end;

definition

let C be category;
let I be set ;
let A be ObjectsFamily of I,C;
let B be Object of C;

attr B is A -CatCoproduct-like means :: ALTCAT_6:def 8
ex P being MorphismsFamily of A,B st
( P is feasible & P is coprojection-morphisms );

end;

:: deftheorem defines -CatCoproduct-like ALTCAT_6:def 8 :
for C being category
for I being set
for A being ObjectsFamily of I,C
for B being Object of C holds
( B is A -CatCoproduct-like iff ex P being MorphismsFamily of A,B st
( P is feasible & P is coprojection-morphisms ) );

registration

let C be with_coproducts category;
let I be set ;
let A be ObjectsFamily of I,C;

cluster A -CatCoproduct-like for Element of the carrier of C;

existence
ex b₁ being Object of C st b₁ is A -CatCoproduct-like

proof end;

end;

registration

let C be category;
let A be ObjectsFamily of {},C;

cluster A -CatCoproduct-like -> initial for Element of the carrier of C;

coherence
for b₁ being Object of C st b₁ is A -CatCoproduct-like holds
b₁ is initial

proof end;

end;

theorem :: ALTCAT_6:5

for C being category
for A being ObjectsFamily of {},C
for B being Object of C st B is initial holds
B is A -CatCoproduct-like

proof end;

theorem :: ALTCAT_6:6

for I being set
for C being category
for A being ObjectsFamily of I,C
for C1, C2 being Object of C st C1 is A -CatCoproduct-like & C2 is A -CatCoproduct-like holds
C1,C2 are_iso

proof end;

definition

let I be set ;
let E be non empty set ;
let A be ObjectsFamily of I,(EnsCat E);
assume A1: Union (coprod A) in E ;

func EnsCatCoproductObj A -> Object of (EnsCat E) equals :Def9: :: ALTCAT_6:def 9
Union (coprod A);

coherence
Union (coprod A) is Object of (EnsCat E) by A1, ALTCAT_1:def 14;

end;

:: deftheorem Def9 defines EnsCatCoproductObj ALTCAT_6:def 9 :
for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds
EnsCatCoproductObj A = Union (coprod A);

definition

let I be set ;
let E be non empty set ;
let A be ObjectsFamily of I,(EnsCat E);

func Coprod A -> ManySortedSet of I means :Def10: :: ALTCAT_6:def 10
for i being object st i in I holds
ex F being Function of (A . i),(Union (coprod A)) st
( it . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) );

existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
ex F being Function of (A . i),(Union (coprod A)) st
( b₁ . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being object st i in I holds
ex F being Function of (A . i),(Union (coprod A)) st
( b₁ . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) ) ) & ( for i being object st i in I holds
ex F being Function of (A . i),(Union (coprod A)) st
( b₂ . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines Coprod ALTCAT_6:def 10 :
for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E)
for b₄ being ManySortedSet of I holds
( b₄ = Coprod A iff for i being object st i in I holds
ex F being Function of (A . i),(Union (coprod A)) st
( b₄ . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) ) );

registration

let I be set ;
let E be non empty set ;
let A be ObjectsFamily of I,(EnsCat E);

cluster Coprod A -> Function-yielding ;

coherence
Coprod A is Function-yielding

proof end;

end;

definition

let I be set ;
let E be non empty set ;
let A be ObjectsFamily of I,(EnsCat E);
assume A1: Union (coprod A) in E ;

func EnsCatCoproduct A -> MorphismsFamily of A, EnsCatCoproductObj A equals :Def11: :: ALTCAT_6:def 11
Coprod A;

coherence
Coprod A is MorphismsFamily of A, EnsCatCoproductObj A

proof end;

end;

:: deftheorem Def11 defines EnsCatCoproduct ALTCAT_6:def 11 :
for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds
EnsCatCoproduct A = Coprod A;

theorem Th7: :: ALTCAT_6:7

for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) = {} holds
Coprod A is V6()

proof end;

theorem Th8: :: ALTCAT_6:8

for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) = {} holds
A is V6()

proof end;

theorem :: ALTCAT_6:9

for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E & Union (coprod A) = {} holds
EnsCatCoproduct A = I --> {}

proof end;

theorem Th10: :: ALTCAT_6:10

for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds
( EnsCatCoproduct A is feasible & EnsCatCoproduct A is coprojection-morphisms )

proof end;

theorem :: ALTCAT_6:11

for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds
EnsCatCoproductObj A is A -CatCoproduct-like

proof end;

theorem :: ALTCAT_6:12

for E being non empty set st ( for I being set
for A being ObjectsFamily of I,(EnsCat E) holds Union (coprod A) in E ) holds
EnsCat E is with_coproducts

proof end;