:: On the Categories Without Uniqueness of { \bf cod } and { \bf
:: dom } . Some Properties of the Morphisms and the Functors
:: by Artur Korni{\l}owicz
::
:: Received October 3, 1997
:: Copyright (c) 1997-2019 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, XBOOLE_0, CAT_1, RELAT_1, ALTCAT_3, CAT_3, RELAT_2,
FUNCTOR0, FUNCT_1, FUNCT_2, ZFMISC_1, STRUCT_0, PBOOLE, MSUALG_3,
MSUALG_6, ALTCAT_2, TARSKI, ALTCAT_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, RELAT_1, FUNCT_1,
FUNCT_2, BINOP_1, MULTOP_1, PBOOLE, STRUCT_0, MSUALG_3, ALTCAT_1,
ALTCAT_2, ALTCAT_3, FUNCTOR0;
constructors REALSET1, MSUALG_3, FUNCTOR0, ALTCAT_3, RELSET_1, XTUPLE_0;
registrations SUBSET_1, RELSET_1, FUNCOP_1, STRUCT_0, FUNCT_1, RELAT_1,
ALTCAT_1, ALTCAT_2, FUNCTOR0, FUNCTOR2, PBOOLE;
requirements SUBSET, BOOLE;
begin :: Preliminaries
reserve C for category,
o1, o2, o3 for Object of C;
registration
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;
registration
let C be with_units non empty AltCatStr, o be Object of C;
cluster idm o -> epi mono retraction coretraction;
end;
registration
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, m9 being Morphism of o1, o2 st m is _zero & m9 is _zero & ex O
being Object of C st O is _zero holds m = m9;
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 id-inheriting;
registration
let C be category;
cluster full non empty strict for 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;
registration
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;
registration
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;
registration
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;
registration
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;
registration
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;