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