Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997 Association of Mizar Users

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

by
Artur Kornilowicz

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;