:: 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-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, 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;