Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### On the Categories Without Uniqueness of \bf cod and \bf dom . Some Properties of the Morphisms and the Functors

**by****Artur Kornilowicz**- Received October 3, 1997
- MML identifier: ALTCAT_4

- [ Mizar article, MML identifier index ]

environ vocabulary ALTCAT_1, CAT_1, RELAT_1, BOOLE, ALTCAT_3, CAT_3, RELAT_2, FUNCTOR0, FUNCT_1, SGRAPH1, PRALG_1, MSUALG_3, PBOOLE, MSUALG_6, ALTCAT_2, ALTCAT_4; notation TARSKI, XBOOLE_0, ZFMISC_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, MULTOP_1, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_3, ALTCAT_1, ALTCAT_2, ALTCAT_3, FUNCTOR0; constructors ALTCAT_3, FUNCTOR0, MCART_1; clusters FUNCTOR0, ALTCAT_2, MSUALG_1, PRALG_1, FUNCTOR2, RELSET_1, SUBSET_1, ALTCAT_1, STRUCT_0, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Preliminaries reserve C for category, o1, o2, o3 for object of C; definition let C be with_units (non empty AltCatStr), o be object of C; cluster <^o,o^> -> non empty; end; theorem :: ALTCAT_4:1 for v being Morphism of o1, o2, u being Morphism of o1, o3 for f being Morphism of o2, o3 st u = f * v & f" * f = idm o2 & <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {} holds v = f" * u; theorem :: ALTCAT_4:2 for v being Morphism of o2, o3, u being Morphism of o1, o3 for f being Morphism of o1, o2 st u = v * f & f * f" = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} holds v = u * f"; theorem :: ALTCAT_4:3 for m being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso holds m" is iso; theorem :: ALTCAT_4:4 for C being with_units (non empty AltCatStr), o being object of C holds idm o is epi mono; definition let C be with_units (non empty AltCatStr), o be object of C; cluster idm o -> epi mono retraction coretraction; end; definition let C be category, o be object of C; cluster idm o -> iso; end; theorem :: ALTCAT_4:5 for f being Morphism of o1, o2, g, h being Morphism of o2, o1 st h * f = idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds g = h; theorem :: ALTCAT_4:6 (for o1, o2 being object of C, f being Morphism of o1, o2 holds f is coretraction) implies for a, b being object of C, g being Morphism of a, b st <^a,b^> <> {} & <^b,a^> <> {} holds g is iso; begin :: Some properties of the initial and terminal objects theorem :: ALTCAT_4:7 for m, m' being Morphism of o1, o2 st m is _zero & m' is _zero & ex O being object of C st O is _zero holds m = m'; theorem :: ALTCAT_4:8 for C being non empty AltCatStr, O, A being object of C for M being Morphism of O, A st O is terminal holds M is mono; theorem :: ALTCAT_4:9 for C being non empty AltCatStr, O, A being object of C for M being Morphism of A, O st O is initial holds M is epi; theorem :: ALTCAT_4:10 o2 is terminal & o1, o2 are_iso implies o1 is terminal; theorem :: ALTCAT_4:11 o1 is initial & o1, o2 are_iso implies o2 is initial; theorem :: ALTCAT_4:12 o1 is initial & o2 is terminal & <^o2,o1^> <> {} implies o2 is initial & o1 is terminal; begin :: The properties of the functors theorem :: ALTCAT_4:13 for A, B being transitive with_units (non empty AltCatStr) for F being contravariant Functor of A, B for a being object of A holds F.idm a = idm (F.a); theorem :: ALTCAT_4:14 for C1, C2 being non empty AltCatStr for F being Contravariant FunctorStr over C1, C2 holds F is full iff for o1, o2 being object of C1 holds Morph-Map(F,o2,o1) is onto; theorem :: ALTCAT_4:15 for C1, C2 being non empty AltCatStr for F being Contravariant FunctorStr over C1, C2 holds F is faithful iff for o1, o2 being object of C1 holds Morph-Map(F,o2,o1) is one-to-one; theorem :: ALTCAT_4:16 for C1, C2 being non empty AltCatStr for F being Covariant FunctorStr over C1, C2 for o1, o2 being object of C1, Fm being Morphism of F.o1, F.o2 st <^o1,o2^> <> {} & F is full feasible ex m being Morphism of o1, o2 st Fm = F.m; theorem :: ALTCAT_4:17 for C1, C2 being non empty AltCatStr for F being Contravariant FunctorStr over C1, C2 for o1, o2 being object of C1, Fm being Morphism of F.o2, F.o1 st <^o1,o2^> <> {} & F is full feasible ex m being Morphism of o1, o2 st Fm = F.m; theorem :: ALTCAT_4:18 for A, B being transitive with_units (non empty AltCatStr) for F being covariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is retraction holds F.a is retraction; theorem :: ALTCAT_4:19 for A, B being transitive with_units (non empty AltCatStr) for F being covariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction holds F.a is coretraction; theorem :: ALTCAT_4:20 for A, B being category, F being covariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is iso holds F.a is iso; theorem :: ALTCAT_4:21 for A, B being category, F being covariant Functor of A, B for o1, o2 being object of A st o1, o2 are_iso holds F.o1, F.o2 are_iso; theorem :: ALTCAT_4:22 for A, B being transitive with_units (non empty AltCatStr) for F being contravariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is retraction holds F.a is coretraction; theorem :: ALTCAT_4:23 for A, B being transitive with_units (non empty AltCatStr) for F being contravariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction holds F.a is retraction; theorem :: ALTCAT_4:24 for A, B being category, F being contravariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is iso holds F.a is iso; theorem :: ALTCAT_4:25 for A, B being category, F being contravariant Functor of A, B for o1, o2 being object of A st o1, o2 are_iso holds F.o2, F.o1 are_iso; theorem :: ALTCAT_4:26 for A, B being transitive with_units (non empty AltCatStr) for F being covariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is retraction holds a is retraction; theorem :: ALTCAT_4:27 for A, B being transitive with_units (non empty AltCatStr) for F being covariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is coretraction holds a is coretraction; theorem :: ALTCAT_4:28 for A, B being category, F being covariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is iso holds a is iso; theorem :: ALTCAT_4:29 for A, B being category, F being covariant Functor of A, B for o1, o2 being object of A st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.o1, F.o2 are_iso holds o1, o2 are_iso; theorem :: ALTCAT_4:30 for A, B being transitive with_units (non empty AltCatStr) for F being contravariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is retraction holds a is coretraction; theorem :: ALTCAT_4:31 for A, B being transitive with_units (non empty AltCatStr) for F being contravariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is coretraction holds a is retraction; theorem :: ALTCAT_4:32 for A, B being category, F being contravariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is iso holds a is iso; theorem :: ALTCAT_4:33 for A, B being category, F being contravariant Functor of A, B for o1, o2 being object of A st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.o2, F.o1 are_iso holds o1, o2 are_iso; begin :: The subcategories of the morphisms theorem :: ALTCAT_4:34 for C being AltCatStr, D being SubCatStr of C st the carrier of C = the carrier of D & the Arrows of C = the Arrows of D holds D is full; theorem :: ALTCAT_4:35 for C being with_units (non empty AltCatStr), D being SubCatStr of C st the carrier of C = the carrier of D & the Arrows of C = the Arrows of D holds D is full id-inheriting; definition let C be category; cluster full non empty strict subcategory of C; end; theorem :: ALTCAT_4:36 for B being non empty subcategory of C for A being non empty subcategory of B holds A is non empty subcategory of C; theorem :: ALTCAT_4:37 for C being non empty transitive AltCatStr for D being non empty transitive SubCatStr of C for o1, o2 being object of C, p1, p2 being object of D for m being Morphism of o1, o2, n being Morphism of p1, p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds (m is mono implies n is mono) & (m is epi implies n is epi); theorem :: ALTCAT_4:38 for D being non empty subcategory of C for o1, o2 being object of C, p1, p2 being object of D for m being Morphism of o1, o2, m1 being Morphism of o2, o1 for n being Morphism of p1, p2, n1 being Morphism of p2, p1 st p1 = o1 & p2 = o2 & m = n & m1 = n1 & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds (m is_left_inverse_of m1 iff n is_left_inverse_of n1) & (m is_right_inverse_of m1 iff n is_right_inverse_of n1); theorem :: ALTCAT_4:39 for D being full non empty subcategory of C for o1, o2 being object of C, p1, p2 being object of D for m being Morphism of o1, o2, n being Morphism of p1, p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds (m is retraction implies n is retraction) & (m is coretraction implies n is coretraction) & (m is iso implies n is iso); theorem :: ALTCAT_4:40 for D being non empty subcategory of C for o1, o2 being object of C, p1, p2 being object of D for m being Morphism of o1, o2, n being Morphism of p1, p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds (n is retraction implies m is retraction) & (n is coretraction implies m is coretraction) & (n is iso implies m is iso); definition let C be category; func AllMono C -> strict non empty transitive SubCatStr of C means :: ALTCAT_4:def 1 the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of it).(o1,o2) iff <^o1,o2^> <> {} & m is mono; end; definition let C be category; cluster AllMono C -> id-inheriting; end; definition let C be category; func AllEpi C -> strict non empty transitive SubCatStr of C means :: ALTCAT_4:def 2 the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of it).(o1,o2) iff <^o1,o2^> <> {} & m is epi; end; definition let C be category; cluster AllEpi C -> id-inheriting; end; definition let C be category; func AllRetr C -> strict non empty transitive SubCatStr of C means :: ALTCAT_4:def 3 the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of it).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction; end; definition let C be category; cluster AllRetr C -> id-inheriting; end; definition let C be category; func AllCoretr C -> strict non empty transitive SubCatStr of C means :: ALTCAT_4:def 4 the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of it).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction; end; definition let C be category; cluster AllCoretr C -> id-inheriting; end; definition let C be category; func AllIso C -> strict non empty transitive SubCatStr of C means :: ALTCAT_4:def 5 the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of it).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso; end; definition let C be category; cluster AllIso C -> id-inheriting; end; theorem :: ALTCAT_4:41 AllIso C is non empty subcategory of AllRetr C; theorem :: ALTCAT_4:42 AllIso C is non empty subcategory of AllCoretr C; theorem :: ALTCAT_4:43 AllCoretr C is non empty subcategory of AllMono C; theorem :: ALTCAT_4:44 AllRetr C is non empty subcategory of AllEpi C; theorem :: ALTCAT_4:45 (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is mono) implies the AltCatStr of C = AllMono C; theorem :: ALTCAT_4:46 (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is epi) implies the AltCatStr of C = AllEpi C; theorem :: ALTCAT_4:47 (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is retraction & <^o2,o1^> <> {}) implies the AltCatStr of C = AllRetr C; theorem :: ALTCAT_4:48 (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is coretraction & <^o2,o1^> <> {}) implies the AltCatStr of C = AllCoretr C; theorem :: ALTCAT_4:49 (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is iso & <^o2,o1^> <> {}) implies the AltCatStr of C = AllIso C; theorem :: ALTCAT_4:50 for o1, o2 being object of AllMono C for m being Morphism of o1, o2 st <^o1,o2^> <> {} holds m is mono; theorem :: ALTCAT_4:51 for o1, o2 being object of AllEpi C for m being Morphism of o1, o2 st <^o1,o2^> <> {} holds m is epi; theorem :: ALTCAT_4:52 for o1, o2 being object of AllIso C for m being Morphism of o1, o2 st <^o1,o2^> <> {} holds m is iso & m" in <^o2,o1^>; theorem :: ALTCAT_4:53 AllMono AllMono C = AllMono C; theorem :: ALTCAT_4:54 AllEpi AllEpi C = AllEpi C; theorem :: ALTCAT_4:55 AllIso AllIso C = AllIso C; theorem :: ALTCAT_4:56 AllIso AllMono C = AllIso C; theorem :: ALTCAT_4:57 AllIso AllEpi C = AllIso C; theorem :: ALTCAT_4:58 AllIso AllRetr C = AllIso C; theorem :: ALTCAT_4:59 AllIso AllCoretr C = AllIso C;

Back to top