ALTCAT_6: Coproducts in Categories without Uniqueness of { \bf cod } and { \bf dom}

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

let o1, o be Object of (EnsCat {{}}); :: thesis:
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:

end;

Lm4: now :: thesis:

let o1, o be Object of (EnsCat {{}}); :: thesis:
let m1 be Morphism of o1,o; :: thesis:
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:

end;

Lm5: now :: thesis:

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

end;

Lm6: now :: thesis:

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

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

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

proof end;

end;

:: deftheorem Def1 defines MorphismsFamily ALTCAT_6:def 1 :

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

proof end;

end;

:: deftheorem Def2 defines MorphismsFamily ALTCAT_6:def 2 :

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

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 :

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

proof end;

end;

:: deftheorem Def4 defines feasible ALTCAT_6:def 4 :

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 :

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

proof end;

end;

:: deftheorem defines coprojection-morphisms ALTCAT_6:def 6 :

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 ;

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 :

registration

cluster EnsCat {{}} -> with_coproducts ;

coherence

proof end;

end;

registration

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

existence

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 :

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

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

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 by A1, ALTCAT_1:def 14;

end;

:: deftheorem Def9 defines EnsCatCoproductObj ALTCAT_6:def 9 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines Coprod ALTCAT_6:def 10 :

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

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

proof end;

end;

:: deftheorem Def11 defines EnsCatCoproduct ALTCAT_6:def 11 :

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;