:: 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-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ALTCAT_1, CAT_1, RELAT_1, ALTCAT_3, CAT_3, FUNCT_1, PBOOLE,
ALTCAT_5, FUNCOP_1, CARD_1, FUNCT_2, XBOOLE_0, SUBSET_1, STRUCT_0,
PARTFUN1, CARD_3, MSUALG_6, MSAFREE, TARSKI, MCART_1, ALTCAT_6;
notations TARSKI, XBOOLE_0, XTUPLE_0, ORDINAL1, SUBSET_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, PBOOLE, CARD_3, FUNCOP_1, STRUCT_0,
ALTCAT_1, ALTCAT_3, ALTCAT_5, MSAFREE;
constructors ALTCAT_3, RELSET_1, ALTCAT_5, MSAFREE;
registrations XBOOLE_0, RELSET_1, FUNCOP_1, STRUCT_0, ALTCAT_1, FUNCT_2,
FUNCT_1, RELAT_1, ALTCAT_5, MSAFREE, XTUPLE_0;
requirements SUBSET, BOOLE;
begin
reserve
I for set,
E for non empty set;
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;
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
:: ALTCAT_6:def 1
for i being object st i in I
ex o1 being Object of C st o1 = f.i & it.i is Morphism of o1,o;
end;
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
:: ALTCAT_6:def 2
for i being Element of I holds it.i is Morphism of f.i,o;
end;
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;
redefine func M.i -> Morphism of f.i,o;
end;
registration
let C be functional non empty 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;
end;
theorem :: ALTCAT_6:1
for C being non empty AltCatStr, o being Object of C
for f being ObjectsFamily of {},C holds
{} is MorphismsFamily of f,o;
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 ex o being Object of C st o = A.i & P.i in <^o,B^>;
end;
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
:: ALTCAT_6:def 4
for i being Element of I holds P.i in <^A.i,B^>;
end;
definition
let C be category;
let I be set;
let A be ObjectsFamily of I,C;
let B be Object of C; :: coproduct Object
let P be MorphismsFamily of A,B; :: coproductfamily
attr P is coprojection-morphisms means
:: ALTCAT_6:def 5
for X being Object of C, F being MorphismsFamily of A,X
st F is feasible
ex f being Morphism of B,X st f in <^B,X^> &
::existence
(for i being set st i in I
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f * Pi) &
::uniqueness
for f1 being Morphism of B,X st for i being set st i in I
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f1 * Pi
holds f = f1;
end;
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, F being MorphismsFamily of A,X st F is feasible
ex f being Morphism of B,X st f in <^B,X^> &
::existence
(for i being Element of I holds F.i = f * P.i) &
::uniqueness
for f1 being Morphism of B,X st
for i being Element of I holds F.i = f1 * P.i
holds f = f1;
end;
registration
let C be category, A be ObjectsFamily of {},C;
let B be Object of C;
cluster -> feasible for MorphismsFamily of A,B;
end;
theorem :: ALTCAT_6:2
for C being category, 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 coprojection-morphisms;
theorem :: ALTCAT_6:3
for A being ObjectsFamily of I,EnsCat {{}}, o being Object of EnsCat {{}}
holds I --> {} is MorphismsFamily of A,o;
theorem :: ALTCAT_6:4
for A being ObjectsFamily of I,EnsCat {{}},
o being Object of EnsCat {{}},
P being MorphismsFamily of A,o st P = I --> {} holds
P is feasible coprojection-morphisms;
definition
let C be category;
attr C is with_coproducts means
:: ALTCAT_6:def 7
for I being set, A being ObjectsFamily of I,C
ex B being Object of C, P being MorphismsFamily of A,B st
P is feasible coprojection-morphisms;
end;
registration
cluster EnsCat {{}} -> with_coproducts;
end;
registration
cluster with_products with_coproducts strict for category;
end;
definition
let C be category;
let I be set, 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 coprojection-morphisms;
end;
registration
let C be with_coproducts category;
let I be set, A be ObjectsFamily of I,C;
cluster A-CatCoproduct-like for Object of C;
end;
registration
let C be category;
let A be ObjectsFamily of {},C;
cluster A-CatCoproduct-like -> initial for Object of C;
end;
theorem :: ALTCAT_6:5
for C being category, A being ObjectsFamily of {},C
for B being Object of C st B is initial holds
B is A-CatCoproduct-like;
theorem :: ALTCAT_6:6
for C being category, A being ObjectsFamily of I,C,
C1,C2 being Object of C
st C1 is A-CatCoproduct-like & C2 is A-CatCoproduct-like
holds C1,C2 are_iso;
reserve A for ObjectsFamily of I,EnsCat E;
definition
let I,E,A;
assume
Union coprod A in E;
func EnsCatCoproductObj A -> Object of EnsCat E equals
:: ALTCAT_6:def 9
Union coprod A;
end;
definition
let I,E,A;
func Coprod(A) -> ManySortedSet of I means
:: ALTCAT_6:def 10
for i being object st i in I
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];
end;
registration
let I,E,A;
cluster Coprod(A) -> Function-yielding;
end;
definition
let I,E,A;
assume
Union coprod A in E;
func EnsCatCoproduct A -> MorphismsFamily of A,EnsCatCoproductObj A equals
:: ALTCAT_6:def 11
Coprod A;
end;
theorem :: ALTCAT_6:7
Union coprod A = {} implies Coprod A is empty-yielding;
theorem :: ALTCAT_6:8
Union coprod A = {} implies A is empty-yielding;
theorem :: ALTCAT_6:9
Union coprod A in E & Union coprod A = {} implies
EnsCatCoproduct A = I --> {};
theorem :: ALTCAT_6:10
Union coprod A in E implies
EnsCatCoproduct A is feasible coprojection-morphisms;
theorem :: ALTCAT_6:11
Union coprod A in E implies EnsCatCoproductObj A is A-CatCoproduct-like;
theorem :: ALTCAT_6:12
(for I,A holds Union coprod A in E) implies EnsCat E is with_coproducts;