:: Products in Categories without Uniqueness of { \bf cod } and { \bf dom
:: }
:: by Artur Korni{\l}owicz
::
:: Received August 19, 2012
:: Copyright (c) 2012-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,
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, NUMERALS;
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;