Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### 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;

Back to top