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