:: Products in Categories without Uniqueness of { \bf cod } and { \bf dom :: } :: by Artur Korni{\l}owicz :: :: Received August 19, 2012 :: Copyright (c) 2012-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, TARSKI, PARTFUN1, CARD_3, MSUALG_6; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PBOOLE, CARD_3, FUNCOP_1, NUMBERS, STRUCT_0, ALTCAT_1, ALTCAT_3; constructors ALTCAT_3, RELSET_1, CARD_3, NUMBERS; registrations XBOOLE_0, RELSET_1, FUNCOP_1, STRUCT_0, ALTCAT_1, FUNCT_2, FUNCT_1, CARD_3, RELAT_1; requirements SUBSET, BOOLE; begin reserve I for set, E for non empty set; registration cluster empty -> {}-defined for Relation; end; definition let C be AltGraph; attr C is functional means :: ALTCAT_5:def 1 for a, b being Object of C holds <^a,b^> is functional; end; registration let E; cluster EnsCat E -> functional; end; registration cluster functional strict for category; end; registration let C be functional AltCatStr; cluster the AltGraph of C -> functional; end; registration cluster functional strict for AltGraph; end; registration cluster functional strict for category; end; registration let C be functional AltGraph; let a,b be Object of C; cluster <^a,b^> -> functional; end; definition let C be non empty AltCatStr; let I be set; mode ObjectsFamily of I,C is Function of I,C; 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 o,f -> ManySortedSet of I means :: ALTCAT_5:def 2 for i being object st i in I ex o1 being Object of C st o1 = f.i & it.i is Morphism of o,o1; 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 o,f means :: ALTCAT_5:def 3 for i being Element of I holds it.i is Morphism of o,f.i; 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 o,f; let i be Element of I; redefine func M.i -> Morphism of o,f.i; 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 o,f; end; theorem :: ALTCAT_5:1 for C being non empty AltCatStr, o being Object of C for f being ObjectsFamily of {},C holds {} is MorphismsFamily of o,f; 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 B,A; attr P is feasible means :: ALTCAT_5:def 4 for i being set st i in I ex o being Object of C st o = A.i & P.i in <^B,o^>; 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 B,A; redefine attr P is feasible means :: ALTCAT_5:def 5 for i being Element of I holds P.i in <^B,A.i^>; end; definition let C be category; let I be set; let A be ObjectsFamily of I,C; let B be Object of C; :: product object let P be MorphismsFamily of B,A; :: product family attr P is projection-morphisms means :: ALTCAT_5:def 6 for X being Object of C, F being MorphismsFamily of X,A st F is feasible ex f being Morphism of X,B st f in <^X,B^> & ::existence (for i being set st i in I ex si being Object of C, Pi being Morphism of B,si st si = A.i & Pi = P.i & F.i = Pi * f) & ::uniqueness for f1 being Morphism of X,B st for i being set st i in I ex si being Object of C, Pi being Morphism of B,si st si = A.i & Pi = P.i & F.i = Pi * f1 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 B,A; redefine attr P is projection-morphisms means :: ALTCAT_5:def 7 for X being Object of C, F being MorphismsFamily of X,A st F is feasible ex f being Morphism of X,B st f in <^X,B^> & ::existence (for i being Element of I holds F.i = P.i * f) & ::uniqueness for f1 being Morphism of X,B st for i being Element of I holds F.i = P.i * f1 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 B,A; end; theorem :: ALTCAT_5:2 for C being category, A being ObjectsFamily of {},C for B being Object of C st B is terminal holds ex P being MorphismsFamily of B,A st P is empty projection-morphisms; theorem :: ALTCAT_5:3 for A being ObjectsFamily of I,EnsCat {{}}, o being Object of EnsCat {{}} holds I --> {} is MorphismsFamily of o,A; theorem :: ALTCAT_5:4 for A being ObjectsFamily of I,EnsCat {{}}, o being Object of EnsCat {{}}, P being MorphismsFamily of o,A st P = I --> {} holds P is feasible projection-morphisms; definition let C be category; attr C is with_products means :: ALTCAT_5:def 8 for I being set, A being ObjectsFamily of I,C ex B being Object of C, P being MorphismsFamily of B,A st P is feasible projection-morphisms; end; registration cluster EnsCat {{}} -> with_products; end; registration cluster with_products 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-CatProduct-like means :: ALTCAT_5:def 9 ex P being MorphismsFamily of B,A st P is feasible projection-morphisms; end; registration let C be with_products category; let I be set, A be ObjectsFamily of I,C; cluster A-CatProduct-like for Object of C; end; registration let C be category; let A be ObjectsFamily of {},C; cluster A-CatProduct-like -> terminal for Object of C; end; theorem :: ALTCAT_5:5 for C being category, A being ObjectsFamily of {},C for B being Object of C st B is terminal holds B is A-CatProduct-like; theorem :: ALTCAT_5:6 for C being category, A being ObjectsFamily of I,C, C1,C2 being Object of C st C1 is A-CatProduct-like & C2 is A-CatProduct-like holds C1,C2 are_iso; reserve A for ObjectsFamily of I,EnsCat E; definition let I,E,A; assume product A in E; func EnsCatProductObj A -> Object of EnsCat E equals :: ALTCAT_5:def 10 product A; end; definition let I,E,A; assume product A in E; func EnsCatProduct A -> MorphismsFamily of EnsCatProductObj A,A means :: ALTCAT_5:def 11 for i being set st i in I holds it.i = proj(A,i); end; theorem :: ALTCAT_5:7 product A in E & product A = {} implies EnsCatProduct A = I --> {}; theorem :: ALTCAT_5:8 product A in E implies EnsCatProduct A is feasible projection-morphisms; theorem :: ALTCAT_5:9 product A in E implies EnsCatProductObj A is A-CatProduct-like; theorem :: ALTCAT_5:10 (for I,A holds product A in E) implies EnsCat E is with_products;