:: Basic properties of objects and morphisms. In categories without
:: uniqueness of { \bf cod } and { \bf dom }
:: by Beata Madras
::
:: Received February 14, 1997
:: Copyright (c) 1997-2018 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, CAT_3, BINOP_1, RELAT_2,
FUNCT_1, FUNCOP_1, TARSKI, FUNCT_2, SUBSET_1, SETFAM_1, ZFMISC_1,
ALTCAT_3;
notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
FUNCT_2, FUNCOP_1, STRUCT_0, ALTCAT_1;
constructors SETFAM_1, ALTCAT_1, RELSET_1;
registrations XBOOLE_0, SETFAM_1, FUNCT_1, RELSET_1, ALTCAT_1, ZFMISC_1;
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;
end;
notation
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;
synonym B is_right_inverse_of A for A is_left_inverse_of B;
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^> <> {} and
<^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;
registration
let C be with_units non empty AltCatStr, o be Object of C;
cluster mono epi retraction coretraction for Morphism of o,o;
end;
registration
let C be category, o be Object of C;
cluster mono epi iso retraction coretraction for Morphism of o,o;
end;
registration
let C be category, o be Object of C, A, B be mono Morphism of o,o;
cluster A * B -> mono;
end;
registration
let C be category, o be Object of C, A, B be epi Morphism of o,o;
cluster A * B -> epi;
end;
registration
let C be category, o be Object of C, A, B be iso Morphism of o,o;
cluster A * B -> iso;
end;
registration
let C be category, o be Object of C, A, B be retraction Morphism of o,o;
cluster A * B -> retraction;
end;
registration
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;