The abstract of the Mizar article:

Basic Properties of Objects and Morphisms

by

Beata Madras-Kobus

Received February 14, 1997

MML identifier: ALTCAT_3

[ Mizar article, MML identifier index ]

environ

 vocabulary ALTCAT_1, CAT_1, CAT_3, BOOLE, RELAT_1, BINOP_1, RELAT_2, FUNCT_1,
      FUNCT_2, AMI_1, SGRAPH1, REALSET1, CQC_LANG, ALTCAT_3;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, REALSET1, FUNCT_1, FUNCT_2,
      STRUCT_0, CQC_LANG, ALTCAT_1, AMI_1;
 constructors ALTCAT_1, AMI_1;
 clusters FUNCT_1, AMI_1, TEX_2, ALTCAT_1, RELSET_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

definition
let C be with_units (non empty AltCatStr),
    o1, o2 be object of C,
    A be Morphism of o1,o2,
    B be Morphism of o2,o1;
pred A is_left_inverse_of B means
:: ALTCAT_3:def 1
 A * B = idm o2;
 synonym B is_right_inverse_of A;
end;

definition
let C be with_units (non empty AltCatStr),
    o1, o2 be object of C,
    A be Morphism of o1,o2;
attr A is retraction means
:: ALTCAT_3:def 2
 ex B being Morphism of o2,o1 st B is_right_inverse_of A;
end;

definition
let C be with_units (non empty AltCatStr),
    o1, o2 be object of C,
    A be Morphism of o1,o2;
attr A is coretraction means
:: ALTCAT_3:def 3
 ex B being Morphism of o2,o1 st B is_left_inverse_of A;
end;

theorem :: ALTCAT_3:1
for C being with_units (non empty AltCatStr), o being object of C holds
idm o is retraction & idm o is coretraction;

definition
let C be category,
    o1, o2 be object of C such that
  <^o1,o2^> <> {} & <^o2,o1^> <> {};
let A be Morphism of o1,o2 such that
  A is retraction coretraction;
func A" -> Morphism of o2,o1 means
:: ALTCAT_3:def 4
 it is_left_inverse_of A & it is_right_inverse_of A;
end;

theorem :: ALTCAT_3:2
for C being category, o1,o2 being object of C st
  <^o1,o2^> <> {} & <^o2,o1^> <> {}
for A being Morphism of o1,o2 st
  A is retraction & A is coretraction holds
A" * A = idm o1 & A * A" = idm o2;

theorem :: ALTCAT_3:3
for C being category, o1,o2 being object of C st
 <^o1,o2^> <> {} & <^o2,o1^> <> {}
for A being Morphism of o1,o2 st A is retraction & A is coretraction
holds (A")" = A;

theorem :: ALTCAT_3:4
for C being category, o being object of C holds
(idm o)" = idm o;

definition
let C be category,
    o1, o2 be object of C,
    A be Morphism of o1,o2;
attr A is iso means
:: ALTCAT_3:def 5
 A*A" = idm o2 & A"*A = idm o1;
end;

theorem :: ALTCAT_3:5
for C being category, o1, o2 being object of C, A being Morphism of o1,o2 st
 A is iso holds A is retraction coretraction;

theorem :: ALTCAT_3:6
for C being category, o1,o2 being object of C st
 <^o1,o2^> <> {} & <^o2,o1^> <> {}
for A being Morphism of o1,o2 holds
 A is iso iff A is retraction & A is coretraction;

theorem :: ALTCAT_3:7
for C being category, o1,o2,o3 being object of C,
A being Morphism of o1,o2, B being Morphism of o2,o3 st
 <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {}
 & A is iso & B is iso holds
B * A is iso & (B * A)" = A" * B";

definition
let C be category,
    o1, o2 be object of C;
pred o1,o2 are_iso means
:: ALTCAT_3:def 6
 <^o1,o2^> <> {} & <^o2,o1^> <> {} &
  ex A being Morphism of o1,o2 st A is iso;
reflexivity;
symmetry;
end;

theorem :: ALTCAT_3:8
  for C being category, o1,o2,o3 being object of C st
 o1,o2 are_iso & o2,o3 are_iso holds o1,o3 are_iso;

definition
let C be non empty AltCatStr,
    o1, o2 be object of C,
    A be Morphism of o1,o2;
attr A is mono means
:: ALTCAT_3:def 7
 for o being object of C st <^o,o1^> <> {}
  for B,C being Morphism of o,o1 st A * B = A * C holds B = C;
end;

definition
let C be non empty AltCatStr,
    o1, o2 be object of C,
    A be Morphism of o1,o2;
attr A is epi means
:: ALTCAT_3:def 8
 for o being object of C st <^o2,o^> <> {}
  for B,C being Morphism of o2,o st B * A = C * A holds B = C;
end;

theorem :: ALTCAT_3:9
for C being associative transitive (non empty AltCatStr),
    o1,o2,o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for A being Morphism of o1,o2, B being Morphism of o2,o3 st
 A is mono & B is mono holds
B * A is mono;

theorem :: ALTCAT_3:10
for C being associative transitive (non empty AltCatStr),
    o1,o2,o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for A being Morphism of o1,o2, B being Morphism of o2,o3 st A is epi & B is epi
 holds B * A is epi;

theorem :: ALTCAT_3:11
  for C being associative transitive (non empty AltCatStr),
    o1,o2,o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for A being Morphism of o1,o2, B being Morphism of o2,o3 st B * A is mono
 holds A is mono;

theorem :: ALTCAT_3:12
  for C being associative transitive (non empty AltCatStr),
    o1,o2,o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for A being Morphism of o1,o2, B being Morphism of o2,o3 st B * A is epi
 holds B is epi;

theorem :: ALTCAT_3:13
  for X being non empty set
for o1,o2 being object of EnsCat X st <^o1,o2^> <> {}
for A being Morphism of o1,o2,
    F being Function of o1,o2 st F = A holds
A is mono iff F is one-to-one;

theorem :: ALTCAT_3:14
  for X being non empty with_non-empty_elements set
for o1,o2 being object of EnsCat X st <^o1,o2^> <> {}
for A being Morphism of o1,o2,
    F being Function of o1,o2 st F = A holds
A is epi iff F is onto;

theorem :: ALTCAT_3:15
for C being category, o1,o2 being object of C st
 <^o1,o2^> <> {} & <^o2,o1^> <> {}
for A being Morphism of o1,o2 st A is retraction holds A is epi;

theorem :: ALTCAT_3:16
for C being category, o1,o2 being object of C st
 <^o1,o2^> <> {} & <^o2,o1^> <> {}
for A being Morphism of o1,o2 st A is coretraction holds A is mono;

theorem :: ALTCAT_3:17
  for C being category, o1,o2 being object of C st
 <^o1,o2^> <> {} & <^o2,o1^> <> {}
for A being Morphism of o1,o2 st A is iso holds A is mono epi;

theorem :: ALTCAT_3:18
for C being category, o1,o2,o3 being object of C st
 <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {}
for A being Morphism of o1,o2, B being Morphism of o2,o3 st
 A is retraction & B is retraction holds
B*A is retraction;

theorem :: ALTCAT_3:19
for C being category, o1,o2,o3 being object of C st
 <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {}
for A being Morphism of o1,o2, B being Morphism of o2,o3 st
 A is coretraction & B is coretraction holds
B*A is coretraction;

theorem :: ALTCAT_3:20
for C being category, o1, o2 being object of C, A being Morphism of o1,o2 st
 A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {}
  holds A is iso;

theorem :: ALTCAT_3:21
  for C being category, o1, o2 being object of C, A being Morphism of o1, o2 st
 A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {}
  holds A is iso;

theorem :: ALTCAT_3:22
  for C being category, o1,o2,o3 being object of C, A being Morphism of o1,o2,
B being Morphism of o2,o3 st
<^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction
holds B is retraction;

theorem :: ALTCAT_3:23
  for C being category, o1,o2,o3 being object of C, A being Morphism of o1,o2,
B being Morphism of o2,o3 st
<^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction
holds A is coretraction;

theorem :: ALTCAT_3:24
  for C being category st
for o1,o2 being object of C, A1 being Morphism of o1,o2 holds A1 is retraction
holds
 for a,b being object of C,A being Morphism of a,b
  st <^a,b^> <> {} & <^b,a^> <> {} holds A is iso;

definition
let C be with_units (non empty AltCatStr),
    o be object of C;
cluster mono epi retraction coretraction Morphism of o,o;
end;

definition
let C be category,
    o be object of C;
cluster mono epi iso retraction coretraction Morphism of o,o;
end;

definition
let C be category,
    o be object of C,
    A, B be mono Morphism of o,o;
cluster A * B -> mono;
end;

definition
let C be category,
    o be object of C,
    A, B be epi Morphism of o,o;
cluster A * B -> epi;
end;

definition
let C be category,
    o be object of C,
    A, B be iso Morphism of o,o;
cluster A * B -> iso;
end;

definition
let C be category,
    o be object of C,
    A, B be retraction Morphism of o,o;
cluster A * B -> retraction;
end;

definition
let C be category,
    o be object of C,
    A, B be coretraction Morphism of o,o;
cluster A * B -> coretraction;
end;

definition
let C be AltGraph,
    o be object of C;
attr o is initial means
:: ALTCAT_3:def 9
 for o1 being object of C holds
 ex M being Morphism of o,o1 st M in <^o,o1^> & <^o,o1^> is trivial;
end;

theorem :: ALTCAT_3:25
  for C being AltGraph, o being object of C holds
o is initial iff
for o1 being object of C holds
 ex M being Morphism of o,o1 st M in <^o,o1^> &
 (for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds M = M1);

theorem :: ALTCAT_3:26
for C being category, o1,o2 being object of C st
o1 is initial & o2 is initial holds o1,o2 are_iso;

definition
let C be AltGraph,
    o be object of C;
attr o is terminal means
:: ALTCAT_3:def 10
 for o1 being object of C holds
  ex M being Morphism of o1,o st M in <^o1,o^> & <^o1,o^> is trivial;
end;

theorem :: ALTCAT_3:27
  for C being AltGraph, o being object of C holds
o is terminal iff
for o1 being object of C holds
 ex M being Morphism of o1,o st M in <^o1,o^> &
 (for M1 being Morphism of o1,o st M1 in <^o1,o^> holds M = M1);

theorem :: ALTCAT_3:28
  for C being category, o1,o2 being object of C st
o1 is terminal & o2 is terminal holds o1,o2 are_iso;

definition
let C be AltGraph,
    o be object of C;
attr o is _zero means
:: ALTCAT_3:def 11
 o is initial terminal;
end;

theorem :: ALTCAT_3:29
  for C being category, o1,o2 being object of C st
o1 is _zero & o2 is _zero holds o1,o2 are_iso;

definition
let C be non empty AltCatStr,
    o1, o2 be object of C,
    M be Morphism of o1,o2;
attr M is _zero means
:: ALTCAT_3:def 12
 for o being object of C st o is _zero
  for A being Morphism of o1,o, B being Morphism of o,o2 holds M = B*A;
end;

theorem :: ALTCAT_3:30
  for C being category, o1,o2,o3 being object of C
for M1 being Morphism of o1,o2, M2 being Morphism of o2,o3
st M1 is _zero & M2 is _zero holds M2 * M1 is _zero;