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;