:: ALTCAT_3 semantic presentation begin definition let C be non empty with_units AltCatStr ; let o1, o2 be object of C; let A be Morphism of o1,o2; let B be Morphism of o2,o1; predA is_left_inverse_of B means :Def1: :: ALTCAT_3:def 1 A * B = idm o2; end; :: deftheorem Def1 defines is_left_inverse_of ALTCAT_3:def_1_:_ for C being non empty with_units AltCatStr for o1, o2 being object of C for A being Morphism of o1,o2 for B being Morphism of o2,o1 holds ( A is_left_inverse_of B iff A * B = idm o2 ); notation let C be non empty with_units AltCatStr ; let o1, o2 be object of C; let A be Morphism of o1,o2; let 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 non empty with_units AltCatStr ; let o1, o2 be object of C; let A be Morphism of o1,o2; attrA is retraction means :Def2: :: ALTCAT_3:def 2 ex B being Morphism of o2,o1 st B is_right_inverse_of A; end; :: deftheorem Def2 defines retraction ALTCAT_3:def_2_:_ for C being non empty with_units AltCatStr for o1, o2 being object of C for A being Morphism of o1,o2 holds ( A is retraction iff ex B being Morphism of o2,o1 st B is_right_inverse_of A ); definition let C be non empty with_units AltCatStr ; let o1, o2 be object of C; let A be Morphism of o1,o2; attrA is coretraction means :Def3: :: ALTCAT_3:def 3 ex B being Morphism of o2,o1 st B is_left_inverse_of A; end; :: deftheorem Def3 defines coretraction ALTCAT_3:def_3_:_ for C being non empty with_units AltCatStr for o1, o2 being object of C for A being Morphism of o1,o2 holds ( A is coretraction iff ex B being Morphism of o2,o1 st B is_left_inverse_of A ); theorem Th1: :: ALTCAT_3:1 for C being non empty with_units AltCatStr for o being object of C holds ( idm o is retraction & idm o is coretraction ) proof let C be non empty with_units AltCatStr ; ::_thesis: for o being object of C holds ( idm o is retraction & idm o is coretraction ) let o be object of C; ::_thesis: ( idm o is retraction & idm o is coretraction ) <^o,o^> <> {} by ALTCAT_1:19; then (idm o) * (idm o) = idm o by ALTCAT_1:def_17; then idm o is_left_inverse_of idm o by Def1; hence ( idm o is retraction & idm o is coretraction ) by Def2, Def3; ::_thesis: verum end; definition let C be category; let o1, o2 be object of C; assume that B1: <^o1,o2^> <> {} and B2: <^o2,o1^> <> {} ; let A be Morphism of o1,o2; assume B3: ( A is retraction & A is coretraction ) ; funcA " -> Morphism of o2,o1 means :Def4: :: ALTCAT_3:def 4 ( it is_left_inverse_of A & it is_right_inverse_of A ); existence ex b1 being Morphism of o2,o1 st ( b1 is_left_inverse_of A & b1 is_right_inverse_of A ) proof consider B1 being Morphism of o2,o1 such that A1: B1 is_right_inverse_of A by B3, Def2; take B1 ; ::_thesis: ( B1 is_left_inverse_of A & B1 is_right_inverse_of A ) consider B2 being Morphism of o2,o1 such that A2: B2 is_left_inverse_of A by B3, Def3; B1 = (idm o1) * B1 by B2, ALTCAT_1:20 .= (B2 * A) * B1 by A2, Def1 .= B2 * (A * B1) by B1, B2, ALTCAT_1:21 .= B2 * (idm o2) by A1, Def1 .= B2 by B2, ALTCAT_1:def_17 ; hence ( B1 is_left_inverse_of A & B1 is_right_inverse_of A ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being Morphism of o2,o1 st b1 is_left_inverse_of A & b1 is_right_inverse_of A & b2 is_left_inverse_of A & b2 is_right_inverse_of A holds b1 = b2 proof let M1, M2 be Morphism of o2,o1; ::_thesis: ( M1 is_left_inverse_of A & M1 is_right_inverse_of A & M2 is_left_inverse_of A & M2 is_right_inverse_of A implies M1 = M2 ) assume that A3: M1 is_left_inverse_of A and M1 is_right_inverse_of A and M2 is_left_inverse_of A and A4: M2 is_right_inverse_of A ; ::_thesis: M1 = M2 thus M1 = M1 * (idm o2) by B2, ALTCAT_1:def_17 .= M1 * (A * M2) by A4, Def1 .= (M1 * A) * M2 by B1, B2, ALTCAT_1:21 .= (idm o1) * M2 by A3, Def1 .= M2 by B2, ALTCAT_1:20 ; ::_thesis: verum end; end; :: deftheorem Def4 defines " ALTCAT_3:def_4_:_ for C being category for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 st A is retraction & A is coretraction holds for b5 being Morphism of o2,o1 holds ( b5 = A " iff ( b5 is_left_inverse_of A & b5 is_right_inverse_of A ) ); theorem Th2: :: ALTCAT_3:2 for C being category for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 st A is retraction & A is coretraction holds ( (A ") * A = idm o1 & A * (A ") = idm o2 ) proof let C be category; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 st A is retraction & A is coretraction holds ( (A ") * A = idm o1 & A * (A ") = idm o2 ) let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is retraction & A is coretraction holds ( (A ") * A = idm o1 & A * (A ") = idm o2 ) ) assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2 st A is retraction & A is coretraction holds ( (A ") * A = idm o1 & A * (A ") = idm o2 ) let A be Morphism of o1,o2; ::_thesis: ( A is retraction & A is coretraction implies ( (A ") * A = idm o1 & A * (A ") = idm o2 ) ) assume ( A is retraction & A is coretraction ) ; ::_thesis: ( (A ") * A = idm o1 & A * (A ") = idm o2 ) then ( A " is_left_inverse_of A & A " is_right_inverse_of A ) by A1, Def4; hence ( (A ") * A = idm o1 & A * (A ") = idm o2 ) by Def1; ::_thesis: verum end; theorem Th3: :: ALTCAT_3:3 for C being category for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 st A is retraction & A is coretraction holds (A ") " = A proof let C be category; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 st A is retraction & A is coretraction holds (A ") " = A let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is retraction & A is coretraction holds (A ") " = A ) assume that A1: <^o1,o2^> <> {} and A2: <^o2,o1^> <> {} ; ::_thesis: for A being Morphism of o1,o2 st A is retraction & A is coretraction holds (A ") " = A let A be Morphism of o1,o2; ::_thesis: ( A is retraction & A is coretraction implies (A ") " = A ) assume A3: ( A is retraction & A is coretraction ) ; ::_thesis: (A ") " = A then A " is_left_inverse_of A by A1, A2, Def4; then A4: A " is retraction by Def2; A5: A " is_right_inverse_of A by A1, A2, A3, Def4; then A " is coretraction by Def3; then A6: (A ") " is_right_inverse_of A " by A1, A2, A4, Def4; thus (A ") " = (idm o2) * ((A ") ") by A1, ALTCAT_1:20 .= (A * (A ")) * ((A ") ") by A5, Def1 .= A * ((A ") * ((A ") ")) by A1, A2, ALTCAT_1:21 .= A * (idm o1) by A6, Def1 .= A by A1, ALTCAT_1:def_17 ; ::_thesis: verum end; theorem Th4: :: ALTCAT_3:4 for C being category for o being object of C holds (idm o) " = idm o proof let C be category; ::_thesis: for o being object of C holds (idm o) " = idm o let o be object of C; ::_thesis: (idm o) " = idm o A1: <^o,o^> <> {} by ALTCAT_1:19; ( idm o is retraction & idm o is coretraction ) by Th1; then A2: (idm o) " is_left_inverse_of idm o by A1, Def4; thus (idm o) " = ((idm o) ") * (idm o) by A1, ALTCAT_1:def_17 .= idm o by A2, Def1 ; ::_thesis: verum end; definition let C be category; let o1, o2 be object of C; let A be Morphism of o1,o2; attrA is iso means :Def5: :: ALTCAT_3:def 5 ( A * (A ") = idm o2 & (A ") * A = idm o1 ); end; :: deftheorem Def5 defines iso ALTCAT_3:def_5_:_ for C being category for o1, o2 being object of C for A being Morphism of o1,o2 holds ( A is iso iff ( A * (A ") = idm o2 & (A ") * A = idm o1 ) ); theorem Th5: :: ALTCAT_3:5 for C being category for o1, o2 being object of C for A being Morphism of o1,o2 st A is iso holds ( A is retraction & A is coretraction ) proof let C be category; ::_thesis: for o1, o2 being object of C for A being Morphism of o1,o2 st A is iso holds ( A is retraction & A is coretraction ) let o1, o2 be object of C; ::_thesis: for A being Morphism of o1,o2 st A is iso holds ( A is retraction & A is coretraction ) let A be Morphism of o1,o2; ::_thesis: ( A is iso implies ( A is retraction & A is coretraction ) ) assume A1: A is iso ; ::_thesis: ( A is retraction & A is coretraction ) then A * (A ") = idm o2 by Def5; then A " is_right_inverse_of A by Def1; hence A is retraction by Def2; ::_thesis: A is coretraction (A ") * A = idm o1 by A1, Def5; then A " is_left_inverse_of A by Def1; hence A is coretraction by Def3; ::_thesis: verum end; theorem Th6: :: ALTCAT_3:6 for C being category for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 holds ( A is iso iff ( A is retraction & A is coretraction ) ) proof let C be category; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 holds ( A is iso iff ( A is retraction & A is coretraction ) ) let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 holds ( A is iso iff ( A is retraction & A is coretraction ) ) ) assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2 holds ( A is iso iff ( A is retraction & A is coretraction ) ) let A be Morphism of o1,o2; ::_thesis: ( A is iso iff ( A is retraction & A is coretraction ) ) thus ( A is iso implies ( A is retraction & A is coretraction ) ) by Th5; ::_thesis: ( A is retraction & A is coretraction implies A is iso ) assume A2: ( A is retraction & A is coretraction ) ; ::_thesis: A is iso then A " is_right_inverse_of A by A1, Def4; then A3: A * (A ") = idm o2 by Def1; A " is_left_inverse_of A by A1, A2, Def4; then (A ") * A = idm o1 by Def1; hence A is iso by A3, Def5; ::_thesis: verum end; theorem Th7: :: ALTCAT_3:7 for C being category for o1, o2, o3 being object of C for A being Morphism of o1,o2 for 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 ") ) proof let C be category; ::_thesis: for o1, o2, o3 being object of C for A being Morphism of o1,o2 for 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 ") ) let o1, o2, o3 be object of C; ::_thesis: for A being Morphism of o1,o2 for 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 ") ) let A be Morphism of o1,o2; ::_thesis: for 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 ") ) let B be Morphism of o2,o3; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso implies ( B * A is iso & (B * A) " = (A ") * (B ") ) ) assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} and A3: <^o3,o1^> <> {} ; ::_thesis: ( not A is iso or not B is iso or ( B * A is iso & (B * A) " = (A ") * (B ") ) ) assume that A4: A is iso and A5: B is iso ; ::_thesis: ( B * A is iso & (B * A) " = (A ") * (B ") ) consider A1 being Morphism of o2,o1 such that A6: A1 = A " ; A7: <^o2,o1^> <> {} by A2, A3, ALTCAT_1:def_2; then A8: ( A is retraction & A is coretraction ) by A1, A4, Th6; consider B1 being Morphism of o3,o2 such that A9: B1 = B " ; A10: <^o3,o2^> <> {} by A1, A3, ALTCAT_1:def_2; then A11: ( B is retraction & B is coretraction ) by A2, A5, Th6; A12: (B * A) * (A1 * B1) = B * (A * (A1 * B1)) by A1, A2, A3, ALTCAT_1:21 .= B * ((A * A1) * B1) by A1, A7, A10, ALTCAT_1:21 .= B * ((idm o2) * B1) by A1, A7, A8, A6, Th2 .= B * B1 by A10, ALTCAT_1:20 .= idm o3 by A2, A10, A11, A9, Th2 ; then A13: A1 * B1 is_right_inverse_of B * A by Def1; then A14: B * A is retraction by Def2; A15: <^o1,o3^> <> {} by A1, A2, ALTCAT_1:def_2; then A16: (A1 * B1) * (B * A) = A1 * (B1 * (B * A)) by A7, A10, ALTCAT_1:21 .= A1 * ((B1 * B) * A) by A1, A2, A10, ALTCAT_1:21 .= A1 * ((idm o2) * A) by A2, A10, A11, A9, Th2 .= A1 * A by A1, ALTCAT_1:20 .= idm o1 by A1, A7, A8, A6, Th2 ; then A17: A1 * B1 is_left_inverse_of B * A by Def1; then B * A is coretraction by Def3; then A1 * B1 = (B * A) " by A3, A15, A17, A13, A14, Def4; hence ( B * A is iso & (B * A) " = (A ") * (B ") ) by A6, A9, A16, A12, Def5; ::_thesis: verum end; definition let C be category; let o1, o2 be object of C; predo1,o2 are_iso means :Def6: :: ALTCAT_3:def 6 ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso ); reflexivity for o1 being object of C holds ( <^o1,o1^> <> {} & <^o1,o1^> <> {} & ex A being Morphism of o1,o1 st A is iso ) proof let o be object of C; ::_thesis: ( <^o,o^> <> {} & <^o,o^> <> {} & ex A being Morphism of o,o st A is iso ) thus A1: ( <^o,o^> <> {} & <^o,o^> <> {} ) by ALTCAT_1:19; ::_thesis: ex A being Morphism of o,o st A is iso take idm o ; ::_thesis: idm o is iso set A = idm o; A2: ((idm o) ") * (idm o) = (idm o) * (idm o) by Th4 .= idm o by A1, ALTCAT_1:def_17 ; (idm o) * ((idm o) ") = (idm o) * (idm o) by Th4 .= idm o by A1, ALTCAT_1:def_17 ; hence idm o is iso by A2, Def5; ::_thesis: verum end; symmetry for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso holds ( <^o2,o1^> <> {} & <^o1,o2^> <> {} & ex A being Morphism of o2,o1 st A is iso ) proof let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso implies ( <^o2,o1^> <> {} & <^o1,o2^> <> {} & ex A being Morphism of o2,o1 st A is iso ) ) assume that A3: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) and A4: ex A being Morphism of o1,o2 st A is iso ; ::_thesis: ( <^o2,o1^> <> {} & <^o1,o2^> <> {} & ex A being Morphism of o2,o1 st A is iso ) thus ( <^o2,o1^> <> {} & <^o1,o2^> <> {} ) by A3; ::_thesis: ex A being Morphism of o2,o1 st A is iso consider A being Morphism of o1,o2 such that A5: A is iso by A4; take A1 = A " ; ::_thesis: A1 is iso A6: ( A is retraction & A is coretraction ) by A5, Th5; then A7: (A1 ") * A1 = A * (A ") by A3, Th3 .= idm o2 by A3, A6, Th2 ; A1 * (A1 ") = (A ") * A by A3, A6, Th3 .= idm o1 by A3, A6, Th2 ; hence A1 is iso by A7, Def5; ::_thesis: verum end; end; :: deftheorem Def6 defines are_iso ALTCAT_3:def_6_:_ for C being category for o1, o2 being object of C holds ( o1,o2 are_iso iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso ) ); theorem :: ALTCAT_3:8 for C being category for o1, o2, o3 being object of C st o1,o2 are_iso & o2,o3 are_iso holds o1,o3 are_iso proof let C be category; ::_thesis: for o1, o2, o3 being object of C st o1,o2 are_iso & o2,o3 are_iso holds o1,o3 are_iso let o1, o2, o3 be object of C; ::_thesis: ( o1,o2 are_iso & o2,o3 are_iso implies o1,o3 are_iso ) assume that A1: o1,o2 are_iso and A2: o2,o3 are_iso ; ::_thesis: o1,o3 are_iso A3: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) by A1, A2, Def6; consider B being Morphism of o2,o3 such that A4: B is iso by A2, Def6; consider A being Morphism of o1,o2 such that A5: A is iso by A1, Def6; ( <^o2,o1^> <> {} & <^o3,o2^> <> {} ) by A1, A2, Def6; hence A6: ( <^o1,o3^> <> {} & <^o3,o1^> <> {} ) by A3, ALTCAT_1:def_2; :: according to ALTCAT_3:def_6 ::_thesis: ex A being Morphism of o1,o3 st A is iso take B * A ; ::_thesis: B * A is iso thus B * A is iso by A3, A6, A5, A4, Th7; ::_thesis: verum end; definition let C be non empty AltCatStr ; let o1, o2 be object of C; let A be Morphism of o1,o2; attrA is mono means :Def7: :: ALTCAT_3:def 7 for o being object of C st <^o,o1^> <> {} holds for B, C being Morphism of o,o1 st A * B = A * C holds B = C; end; :: deftheorem Def7 defines mono ALTCAT_3:def_7_:_ for C being non empty AltCatStr for o1, o2 being object of C for A being Morphism of o1,o2 holds ( A is mono iff for o being object of C st <^o,o1^> <> {} holds for B, C being Morphism of o,o1 st A * B = A * C holds B = C ); definition let C be non empty AltCatStr ; let o1, o2 be object of C; let A be Morphism of o1,o2; attrA is epi means :Def8: :: ALTCAT_3:def 8 for o being object of C st <^o2,o^> <> {} holds for B, C being Morphism of o2,o st B * A = C * A holds B = C; end; :: deftheorem Def8 defines epi ALTCAT_3:def_8_:_ for C being non empty AltCatStr for o1, o2 being object of C for A being Morphism of o1,o2 holds ( A is epi iff for o being object of C st <^o2,o^> <> {} holds for B, C being Morphism of o2,o st B * A = C * A holds B = C ); theorem Th9: :: ALTCAT_3:9 for C being non empty transitive associative AltCatStr for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is mono & B is mono holds B * A is mono proof let C be non empty transitive associative AltCatStr ; ::_thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is mono & B is mono holds B * A is mono let o1, o2, o3 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is mono & B is mono holds B * A is mono ) assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} ; ::_thesis: for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is mono & B is mono holds B * A is mono let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st A is mono & B is mono holds B * A is mono let B be Morphism of o2,o3; ::_thesis: ( A is mono & B is mono implies B * A is mono ) assume that A3: A is mono and A4: B is mono ; ::_thesis: B * A is mono let o be object of C; :: according to ALTCAT_3:def_7 ::_thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st (B * A) * B = (B * A) * C holds B = C ) assume A5: <^o,o1^> <> {} ; ::_thesis: for B, C being Morphism of o,o1 st (B * A) * B = (B * A) * C holds B = C then A6: <^o,o2^> <> {} by A1, ALTCAT_1:def_2; let M1, M2 be Morphism of o,o1; ::_thesis: ( (B * A) * M1 = (B * A) * M2 implies M1 = M2 ) assume A7: (B * A) * M1 = (B * A) * M2 ; ::_thesis: M1 = M2 ( (B * A) * M1 = B * (A * M1) & (B * A) * M2 = B * (A * M2) ) by A1, A2, A5, ALTCAT_1:21; then A * M1 = A * M2 by A4, A7, A6, Def7; hence M1 = M2 by A3, A5, Def7; ::_thesis: verum end; theorem Th10: :: ALTCAT_3:10 for C being non empty transitive associative AltCatStr for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is epi & B is epi holds B * A is epi proof let C be non empty transitive associative AltCatStr ; ::_thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is epi & B is epi holds B * A is epi let o1, o2, o3 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is epi & B is epi holds B * A is epi ) assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} ; ::_thesis: for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is epi & B is epi holds B * A is epi let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st A is epi & B is epi holds B * A is epi let B be Morphism of o2,o3; ::_thesis: ( A is epi & B is epi implies B * A is epi ) assume that A3: A is epi and A4: B is epi ; ::_thesis: B * A is epi let o be object of C; :: according to ALTCAT_3:def_8 ::_thesis: ( <^o3,o^> <> {} implies for B, C being Morphism of o3,o st B * (B * A) = C * (B * A) holds B = C ) assume A5: <^o3,o^> <> {} ; ::_thesis: for B, C being Morphism of o3,o st B * (B * A) = C * (B * A) holds B = C then A6: <^o2,o^> <> {} by A2, ALTCAT_1:def_2; let M1, M2 be Morphism of o3,o; ::_thesis: ( M1 * (B * A) = M2 * (B * A) implies M1 = M2 ) assume A7: M1 * (B * A) = M2 * (B * A) ; ::_thesis: M1 = M2 ( M1 * (B * A) = (M1 * B) * A & M2 * (B * A) = (M2 * B) * A ) by A1, A2, A5, ALTCAT_1:21; then M1 * B = M2 * B by A3, A7, A6, Def8; hence M1 = M2 by A4, A5, Def8; ::_thesis: verum end; theorem :: ALTCAT_3:11 for C being non empty transitive associative AltCatStr for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for A being Morphism of o1,o2 for B being Morphism of o2,o3 st B * A is mono holds A is mono proof let C be non empty transitive associative AltCatStr ; ::_thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for A being Morphism of o1,o2 for B being Morphism of o2,o3 st B * A is mono holds A is mono let o1, o2, o3 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for A being Morphism of o1,o2 for B being Morphism of o2,o3 st B * A is mono holds A is mono ) assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2 for B being Morphism of o2,o3 st B * A is mono holds A is mono let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st B * A is mono holds A is mono let B be Morphism of o2,o3; ::_thesis: ( B * A is mono implies A is mono ) assume A2: B * A is mono ; ::_thesis: A is mono let o be object of C; :: according to ALTCAT_3:def_7 ::_thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds B = C ) assume A3: <^o,o1^> <> {} ; ::_thesis: for B, C being Morphism of o,o1 st A * B = A * C holds B = C let M1, M2 be Morphism of o,o1; ::_thesis: ( A * M1 = A * M2 implies M1 = M2 ) assume A4: A * M1 = A * M2 ; ::_thesis: M1 = M2 ( (B * A) * M1 = B * (A * M1) & (B * A) * M2 = B * (A * M2) ) by A1, A3, ALTCAT_1:21; hence M1 = M2 by A2, A3, A4, Def7; ::_thesis: verum end; theorem :: ALTCAT_3:12 for C being non empty transitive associative AltCatStr for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for A being Morphism of o1,o2 for B being Morphism of o2,o3 st B * A is epi holds B is epi proof let C be non empty transitive associative AltCatStr ; ::_thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for A being Morphism of o1,o2 for B being Morphism of o2,o3 st B * A is epi holds B is epi let o1, o2, o3 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for A being Morphism of o1,o2 for B being Morphism of o2,o3 st B * A is epi holds B is epi ) assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2 for B being Morphism of o2,o3 st B * A is epi holds B is epi let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st B * A is epi holds B is epi let B be Morphism of o2,o3; ::_thesis: ( B * A is epi implies B is epi ) assume A2: B * A is epi ; ::_thesis: B is epi let o be object of C; :: according to ALTCAT_3:def_8 ::_thesis: ( <^o3,o^> <> {} implies for B, C being Morphism of o3,o st B * B = C * B holds B = C ) assume A3: <^o3,o^> <> {} ; ::_thesis: for B, C being Morphism of o3,o st B * B = C * B holds B = C let M1, M2 be Morphism of o3,o; ::_thesis: ( M1 * B = M2 * B implies M1 = M2 ) assume A4: M1 * B = M2 * B ; ::_thesis: M1 = M2 ( (M1 * B) * A = M1 * (B * A) & (M2 * B) * A = M2 * (B * A) ) by A1, A3, ALTCAT_1:21; hence M1 = M2 by A2, A3, A4, Def8; ::_thesis: verum end; Lm1: now__::_thesis:_for_C_being_non_empty_with_units_AltCatStr_ for_a_being_object_of_C_holds_ (_idm_a_is_epi_&_idm_a_is_mono_) let C be non empty with_units AltCatStr ; ::_thesis: for a being object of C holds ( idm a is epi & idm a is mono ) let a be object of C; ::_thesis: ( idm a is epi & idm a is mono ) thus idm a is epi ::_thesis: idm a is mono proof let o be object of C; :: according to ALTCAT_3:def_8 ::_thesis: ( <^a,o^> <> {} implies for B, C being Morphism of a,o st B * (idm a) = C * (idm a) holds B = C ) assume A1: <^a,o^> <> {} ; ::_thesis: for B, C being Morphism of a,o st B * (idm a) = C * (idm a) holds B = C let B, C be Morphism of a,o; ::_thesis: ( B * (idm a) = C * (idm a) implies B = C ) assume A2: B * (idm a) = C * (idm a) ; ::_thesis: B = C thus B = B * (idm a) by A1, ALTCAT_1:def_17 .= C by A1, A2, ALTCAT_1:def_17 ; ::_thesis: verum end; thus idm a is mono ::_thesis: verum proof let o be object of C; :: according to ALTCAT_3:def_7 ::_thesis: ( <^o,a^> <> {} implies for B, C being Morphism of o,a st (idm a) * B = (idm a) * C holds B = C ) assume A3: <^o,a^> <> {} ; ::_thesis: for B, C being Morphism of o,a st (idm a) * B = (idm a) * C holds B = C let B, C be Morphism of o,a; ::_thesis: ( (idm a) * B = (idm a) * C implies B = C ) assume A4: (idm a) * B = (idm a) * C ; ::_thesis: B = C thus B = (idm a) * B by A3, ALTCAT_1:20 .= C by A3, A4, ALTCAT_1:20 ; ::_thesis: verum end; end; theorem :: ALTCAT_3:13 for X being non empty set for o1, o2 being object of (EnsCat X) st <^o1,o2^> <> {} holds for A being Morphism of o1,o2 for F being Function of o1,o2 st F = A holds ( A is mono iff F is one-to-one ) proof let X be non empty set ; ::_thesis: for o1, o2 being object of (EnsCat X) st <^o1,o2^> <> {} holds for A being Morphism of o1,o2 for F being Function of o1,o2 st F = A holds ( A is mono iff F is one-to-one ) let o1, o2 be object of (EnsCat X); ::_thesis: ( <^o1,o2^> <> {} implies for A being Morphism of o1,o2 for F being Function of o1,o2 st F = A holds ( A is mono iff F is one-to-one ) ) assume A1: <^o1,o2^> <> {} ; ::_thesis: for A being Morphism of o1,o2 for F being Function of o1,o2 st F = A holds ( A is mono iff F is one-to-one ) let A be Morphism of o1,o2; ::_thesis: for F being Function of o1,o2 st F = A holds ( A is mono iff F is one-to-one ) let F be Function of o1,o2; ::_thesis: ( F = A implies ( A is mono iff F is one-to-one ) ) assume A2: F = A ; ::_thesis: ( A is mono iff F is one-to-one ) percases ( o2 <> {} or o2 = {} ) ; suppose o2 <> {} ; ::_thesis: ( A is mono iff F is one-to-one ) then A3: dom F = o1 by FUNCT_2:def_1; thus ( A is mono implies F is one-to-one ) ::_thesis: ( F is one-to-one implies A is mono ) proof set o = o1; assume A4: A is mono ; ::_thesis: F is one-to-one assume not F is one-to-one ; ::_thesis: contradiction then consider x1, x2 being set such that A5: x1 in dom F and A6: x2 in dom F and A7: F . x1 = F . x2 and A8: x1 <> x2 by FUNCT_1:def_4; set C = o1 --> x2; set B = o1 --> x1; A9: dom (o1 --> x2) = o1 by FUNCOP_1:13; A10: rng (o1 --> x2) c= o1 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (o1 --> x2) or y in o1 ) assume y in rng (o1 --> x2) ; ::_thesis: y in o1 then ex x being set st ( x in dom (o1 --> x2) & (o1 --> x2) . x = y ) by FUNCT_1:def_3; hence y in o1 by A3, A6, A9, FUNCOP_1:7; ::_thesis: verum end; then A11: dom (F * (o1 --> x2)) = o1 by A3, A9, RELAT_1:27; o1 --> x2 in Funcs (o1,o1) by A9, A10, FUNCT_2:def_2; then reconsider C1 = o1 --> x2 as Morphism of o1,o1 by ALTCAT_1:def_14; set o9 = the Element of o1; A12: <^o1,o1^> <> {} by ALTCAT_1:19; (o1 --> x1) . the Element of o1 = x1 by A3, A5, FUNCOP_1:7; then A13: (o1 --> x1) . the Element of o1 <> (o1 --> x2) . the Element of o1 by A3, A5, A8, FUNCOP_1:7; A14: dom (o1 --> x1) = o1 by FUNCOP_1:13; A15: rng (o1 --> x1) c= o1 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (o1 --> x1) or y in o1 ) assume y in rng (o1 --> x1) ; ::_thesis: y in o1 then ex x being set st ( x in dom (o1 --> x1) & (o1 --> x1) . x = y ) by FUNCT_1:def_3; hence y in o1 by A3, A5, A14, FUNCOP_1:7; ::_thesis: verum end; then o1 --> x1 in Funcs (o1,o1) by A14, FUNCT_2:def_2; then reconsider B1 = o1 --> x1 as Morphism of o1,o1 by ALTCAT_1:def_14; A16: dom (F * (o1 --> x1)) = o1 by A3, A14, A15, RELAT_1:27; now__::_thesis:_for_z_being_set_st_z_in_o1_holds_ (F_*_(o1_-->_x1))_._z_=_(F_*_(o1_-->_x2))_._z let z be set ; ::_thesis: ( z in o1 implies (F * (o1 --> x1)) . z = (F * (o1 --> x2)) . z ) assume A17: z in o1 ; ::_thesis: (F * (o1 --> x1)) . z = (F * (o1 --> x2)) . z hence (F * (o1 --> x1)) . z = F . ((o1 --> x1) . z) by A16, FUNCT_1:12 .= F . x2 by A7, A17, FUNCOP_1:7 .= F . ((o1 --> x2) . z) by A17, FUNCOP_1:7 .= (F * (o1 --> x2)) . z by A11, A17, FUNCT_1:12 ; ::_thesis: verum end; then F * (o1 --> x1) = F * (o1 --> x2) by A16, A11, FUNCT_1:2; then A * B1 = F * (o1 --> x2) by A1, A2, A12, ALTCAT_1:16 .= A * C1 by A1, A2, A12, ALTCAT_1:16 ; hence contradiction by A4, A12, A13, Def7; ::_thesis: verum end; thus ( F is one-to-one implies A is mono ) ::_thesis: verum proof assume A18: F is one-to-one ; ::_thesis: A is mono let o be object of (EnsCat X); :: according to ALTCAT_3:def_7 ::_thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds B = C ) assume A19: <^o,o1^> <> {} ; ::_thesis: for B, C being Morphism of o,o1 st A * B = A * C holds B = C then A20: <^o,o2^> <> {} by A1, ALTCAT_1:def_2; let B, C be Morphism of o,o1; ::_thesis: ( A * B = A * C implies B = C ) A21: <^o,o1^> = Funcs (o,o1) by ALTCAT_1:def_14; then consider B1 being Function such that A22: B1 = B and A23: dom B1 = o and A24: rng B1 c= o1 by A19, FUNCT_2:def_2; consider C1 being Function such that A25: C1 = C and A26: dom C1 = o and A27: rng C1 c= o1 by A19, A21, FUNCT_2:def_2; assume A * B = A * C ; ::_thesis: B = C then A28: F * B1 = A * C by A1, A2, A19, A22, A20, ALTCAT_1:16 .= F * C1 by A1, A2, A19, A25, A20, ALTCAT_1:16 ; now__::_thesis:_for_z_being_set_st_z_in_o_holds_ B1_._z_=_C1_._z let z be set ; ::_thesis: ( z in o implies B1 . z = C1 . z ) assume A29: z in o ; ::_thesis: B1 . z = C1 . z then F . (B1 . z) = (F * B1) . z by A23, FUNCT_1:13; then A30: F . (B1 . z) = F . (C1 . z) by A26, A28, A29, FUNCT_1:13; ( B1 . z in rng B1 & C1 . z in rng C1 ) by A23, A26, A29, FUNCT_1:def_3; hence B1 . z = C1 . z by A3, A18, A24, A27, A30, FUNCT_1:def_4; ::_thesis: verum end; hence B = C by A22, A23, A25, A26, FUNCT_1:2; ::_thesis: verum end; end; supposeA31: o2 = {} ; ::_thesis: ( A is mono iff F is one-to-one ) then F = {} ; hence ( A is mono implies F is one-to-one ) ; ::_thesis: ( F is one-to-one implies A is mono ) thus ( F is one-to-one implies A is mono ) ::_thesis: verum proof set x = the Element of Funcs (o1,o2); assume F is one-to-one ; ::_thesis: A is mono let o be object of (EnsCat X); :: according to ALTCAT_3:def_7 ::_thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds B = C ) assume A32: <^o,o1^> <> {} ; ::_thesis: for B, C being Morphism of o,o1 st A * B = A * C holds B = C <^o1,o2^> = Funcs (o1,o2) by ALTCAT_1:def_14; then consider f being Function such that f = the Element of Funcs (o1,o2) and A33: dom f = o1 and A34: rng f c= o2 by A1, FUNCT_2:def_2; let B, C be Morphism of o,o1; ::_thesis: ( A * B = A * C implies B = C ) A35: <^o,o1^> = Funcs (o,o1) by ALTCAT_1:def_14; then consider B1 being Function such that A36: B1 = B and A37: dom B1 = o and A38: rng B1 c= o1 by A32, FUNCT_2:def_2; rng f = {} by A31, A34, XBOOLE_1:3; then dom f = {} by RELAT_1:42; then A39: rng B1 = {} by A38, A33, XBOOLE_1:3; then A40: dom B1 = {} by RELAT_1:42; assume A * B = A * C ; ::_thesis: B = C consider C1 being Function such that A41: C1 = C and A42: dom C1 = o and rng C1 c= o1 by A32, A35, FUNCT_2:def_2; B1 = {} by A39, RELAT_1:41 .= C1 by A37, A42, A40, RELAT_1:41 ; hence B = C by A36, A41; ::_thesis: verum end; end; end; end; 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^> <> {} holds for A being Morphism of o1,o2 for F being Function of o1,o2 st F = A holds ( A is epi iff F is onto ) proof let X be non empty with_non-empty_elements set ; ::_thesis: for o1, o2 being object of (EnsCat X) st <^o1,o2^> <> {} holds for A being Morphism of o1,o2 for F being Function of o1,o2 st F = A holds ( A is epi iff F is onto ) let o1, o2 be object of (EnsCat X); ::_thesis: ( <^o1,o2^> <> {} implies for A being Morphism of o1,o2 for F being Function of o1,o2 st F = A holds ( A is epi iff F is onto ) ) assume A1: <^o1,o2^> <> {} ; ::_thesis: for A being Morphism of o1,o2 for F being Function of o1,o2 st F = A holds ( A is epi iff F is onto ) let A be Morphism of o1,o2; ::_thesis: for F being Function of o1,o2 st F = A holds ( A is epi iff F is onto ) let F be Function of o1,o2; ::_thesis: ( F = A implies ( A is epi iff F is onto ) ) assume A2: F = A ; ::_thesis: ( A is epi iff F is onto ) percases ( for x being set st x in X holds x is trivial or ex x being set st ( x in X & not x is trivial ) ) ; supposeA3: for x being set st x in X holds x is trivial ; ::_thesis: ( A is epi iff F is onto ) thus ( A is epi implies F is onto ) ::_thesis: ( F is onto implies A is epi ) proof assume A is epi ; ::_thesis: F is onto now__::_thesis:_F_is_onto percases ( o2 = {} or o2 <> {} ) ; supposeA4: o2 = {} ; ::_thesis: F is onto then F = {} ; hence F is onto by A4, FUNCT_2:def_3, RELAT_1:38; ::_thesis: verum end; supposeA5: o2 <> {} ; ::_thesis: F is onto A6: o1 is Element of X by ALTCAT_1:def_14; then o1 is trivial by A3; then consider z being set such that A7: o1 = {z} by A6, ZFMISC_1:131; dom F = {z} by A5, A7, FUNCT_2:def_1; then A8: rng F <> {} by RELAT_1:42; o2 is Element of X by ALTCAT_1:def_14; then o2 is trivial by A3; then consider y being set such that A9: o2 = {y} by A5, ZFMISC_1:131; rng F c= {y} by A9, RELAT_1:def_19; then rng F = {y} by A8, ZFMISC_1:33; hence F is onto by A9, FUNCT_2:def_3; ::_thesis: verum end; end; end; hence F is onto ; ::_thesis: verum end; thus ( F is onto implies A is epi ) ::_thesis: verum proof assume A10: F is onto ; ::_thesis: A is epi let o be object of (EnsCat X); :: according to ALTCAT_3:def_8 ::_thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds B = C ) assume A11: <^o2,o^> <> {} ; ::_thesis: for B, C being Morphism of o2,o st B * A = C * A holds B = C then A12: <^o1,o^> <> {} by A1, ALTCAT_1:def_2; let B, C be Morphism of o2,o; ::_thesis: ( B * A = C * A implies B = C ) A13: <^o2,o^> = Funcs (o2,o) by ALTCAT_1:def_14; then consider B1 being Function such that A14: B1 = B and A15: dom B1 = o2 and rng B1 c= o by A11, FUNCT_2:def_2; consider C1 being Function such that A16: C1 = C and A17: dom C1 = o2 and rng C1 c= o by A11, A13, FUNCT_2:def_2; assume B * A = C * A ; ::_thesis: B = C then A18: B1 * F = C * A by A1, A2, A11, A14, A12, ALTCAT_1:16 .= C1 * F by A1, A2, A11, A16, A12, ALTCAT_1:16 ; now__::_thesis:_not_B1_<>_C1 assume B1 <> C1 ; ::_thesis: contradiction then consider z being set such that A19: z in o2 and A20: B1 . z <> C1 . z by A15, A17, FUNCT_1:2; z in rng F by A10, A19, FUNCT_2:def_3; then consider x being set such that A21: x in dom F and A22: F . x = z by FUNCT_1:def_3; B1 . (F . x) = (B1 * F) . x by A21, FUNCT_1:13; hence contradiction by A18, A20, A21, A22, FUNCT_1:13; ::_thesis: verum end; hence B = C by A14, A16; ::_thesis: verum end; end; supposeA23: ex x being set st ( x in X & not x is trivial ) ; ::_thesis: ( A is epi iff F is onto ) now__::_thesis:_(_(_A_is_epi_implies_F_is_onto_)_&_(_F_is_onto_implies_A_is_epi_)_) percases ( o2 <> {} or o2 = {} ) ; supposeA24: o2 <> {} ; ::_thesis: ( ( A is epi implies F is onto ) & ( F is onto implies A is epi ) ) consider o being set such that A25: o in X and A26: not o is trivial by A23; reconsider o = o as object of (EnsCat X) by A25, ALTCAT_1:def_14; A27: dom F = o1 by A24, FUNCT_2:def_1; thus ( A is epi implies F is onto ) ::_thesis: ( F is onto implies A is epi ) proof set k = the Element of o; A28: rng F c= o2 by RELAT_1:def_19; reconsider ok = o \ { the Element of o} as non empty set by A26, REALSET1:3; assume that A29: A is epi and A30: not F is onto ; ::_thesis: contradiction rng F <> o2 by A30, FUNCT_2:def_3; then not o2 c= rng F by A28, XBOOLE_0:def_10; then consider y being set such that A31: y in o2 and A32: not y in rng F by TARSKI:def_3; set C = o2 --> the Element of o; A33: dom (o2 --> the Element of o) = o2 by FUNCOP_1:13; A34: o <> {} by A25; then A35: the Element of o in o ; rng (o2 --> the Element of o) c= o proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (o2 --> the Element of o) or y in o ) assume y in rng (o2 --> the Element of o) ; ::_thesis: y in o then ex x being set st ( x in dom (o2 --> the Element of o) & (o2 --> the Element of o) . x = y ) by FUNCT_1:def_3; hence y in o by A35, A33, FUNCOP_1:7; ::_thesis: verum end; then o2 --> the Element of o in Funcs (o2,o) by A33, FUNCT_2:def_2; then reconsider C1 = o2 --> the Element of o as Morphism of o2,o by ALTCAT_1:def_14; set l = the Element of ok; A36: not the Element of ok in { the Element of o} by XBOOLE_0:def_5; reconsider l = the Element of ok as Element of o by XBOOLE_0:def_5; A37: the Element of o <> l by A36, TARSKI:def_1; deffunc H1( set ) -> Element of o = IFEQ (\$1,y,l, the Element of o); consider B being Function such that A38: dom B = o2 and A39: for x being set st x in o2 holds B . x = H1(x) from FUNCT_1:sch_3(); A40: dom (B * F) = o1 by A27, A28, A38, RELAT_1:27; A41: rng B c= o proof let y1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not y1 in rng B or y1 in o ) assume y1 in rng B ; ::_thesis: y1 in o then consider x being set such that A42: ( x in dom B & B . x = y1 ) by FUNCT_1:def_3; percases ( x = y or x <> y ) ; supposeA43: x = y ; ::_thesis: y1 in o y1 = IFEQ (x,y,l, the Element of o) by A38, A39, A42 .= l by A43, FUNCOP_1:def_8 ; hence y1 in o by A34; ::_thesis: verum end; supposeA44: x <> y ; ::_thesis: y1 in o y1 = IFEQ (x,y,l, the Element of o) by A38, A39, A42 .= the Element of o by A44, FUNCOP_1:def_8 ; hence y1 in o by A34; ::_thesis: verum end; end; end; then A45: B in Funcs (o2,o) by A38, FUNCT_2:def_2; then A46: B in <^o2,o^> by ALTCAT_1:def_14; reconsider B1 = B as Morphism of o2,o by A45, ALTCAT_1:def_14; for z being set st z in rng (B * F) holds z in rng B by FUNCT_1:14; then rng (B * F) c= rng B by TARSKI:def_3; then rng (B * F) c= o by A41, XBOOLE_1:1; then B * F in Funcs (o1,o) by A40, FUNCT_2:def_2; then A47: B * F in <^o1,o^> by ALTCAT_1:def_14; B . y = IFEQ (y,y,l, the Element of o) by A31, A39 .= l by FUNCOP_1:def_8 ; then A48: not B = o2 --> the Element of o by A31, A37, FUNCOP_1:7; A49: dom ((o2 --> the Element of o) * F) = o1 by A27, A28, A33, RELAT_1:27; now__::_thesis:_for_z_being_set_st_z_in_o1_holds_ (B_*_F)_._z_=_((o2_-->_the_Element_of_o)_*_F)_._z let z be set ; ::_thesis: ( z in o1 implies (B * F) . z = ((o2 --> the Element of o) * F) . z ) assume A50: z in o1 ; ::_thesis: (B * F) . z = ((o2 --> the Element of o) * F) . z then A51: F . z in rng F by A27, FUNCT_1:def_3; then A52: B . (F . z) = IFEQ ((F . z),y,l, the Element of o) by A28, A39 .= the Element of o by A32, A51, FUNCOP_1:def_8 ; thus (B * F) . z = B . (F . z) by A40, A50, FUNCT_1:12 .= (o2 --> the Element of o) . (F . z) by A28, A51, A52, FUNCOP_1:7 .= ((o2 --> the Element of o) * F) . z by A49, A50, FUNCT_1:12 ; ::_thesis: verum end; then B * F = (o2 --> the Element of o) * F by A40, A49, FUNCT_1:2; then B1 * A = (o2 --> the Element of o) * F by A1, A2, A46, A47, ALTCAT_1:16 .= C1 * A by A1, A2, A46, A47, ALTCAT_1:16 ; hence contradiction by A29, A48, A46, Def8; ::_thesis: verum end; thus ( F is onto implies A is epi ) ::_thesis: verum proof assume A53: F is onto ; ::_thesis: A is epi let o be object of (EnsCat X); :: according to ALTCAT_3:def_8 ::_thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds B = C ) assume A54: <^o2,o^> <> {} ; ::_thesis: for B, C being Morphism of o2,o st B * A = C * A holds B = C then A55: <^o1,o^> <> {} by A1, ALTCAT_1:def_2; let B, C be Morphism of o2,o; ::_thesis: ( B * A = C * A implies B = C ) A56: <^o2,o^> = Funcs (o2,o) by ALTCAT_1:def_14; then consider B1 being Function such that A57: B1 = B and A58: dom B1 = o2 and rng B1 c= o by A54, FUNCT_2:def_2; consider C1 being Function such that A59: C1 = C and A60: dom C1 = o2 and rng C1 c= o by A54, A56, FUNCT_2:def_2; assume B * A = C * A ; ::_thesis: B = C then A61: B1 * F = C * A by A1, A2, A54, A57, A55, ALTCAT_1:16 .= C1 * F by A1, A2, A54, A59, A55, ALTCAT_1:16 ; now__::_thesis:_not_B1_<>_C1 assume B1 <> C1 ; ::_thesis: contradiction then consider z being set such that A62: z in o2 and A63: B1 . z <> C1 . z by A58, A60, FUNCT_1:2; z in rng F by A53, A62, FUNCT_2:def_3; then consider x being set such that A64: x in dom F and A65: F . x = z by FUNCT_1:def_3; B1 . (F . x) = (B1 * F) . x by A64, FUNCT_1:13; hence contradiction by A61, A63, A64, A65, FUNCT_1:13; ::_thesis: verum end; hence B = C by A57, A59; ::_thesis: verum end; end; supposeA66: o2 = {} ; ::_thesis: ( ( A is epi implies F is onto ) & ( F is onto implies A is epi ) ) then F = {} ; hence ( A is epi implies F is onto ) by A66, FUNCT_2:def_3, RELAT_1:38; ::_thesis: ( F is onto implies A is epi ) thus ( F is onto implies A is epi ) ::_thesis: verum proof assume F is onto ; ::_thesis: A is epi let o be object of (EnsCat X); :: according to ALTCAT_3:def_8 ::_thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds B = C ) assume A67: <^o2,o^> <> {} ; ::_thesis: for B, C being Morphism of o2,o st B * A = C * A holds B = C let B, C be Morphism of o2,o; ::_thesis: ( B * A = C * A implies B = C ) A68: <^o2,o^> = Funcs (o2,o) by ALTCAT_1:def_14; then consider B1 being Function such that A69: B1 = B and A70: dom B1 = o2 and rng B1 c= o by A67, FUNCT_2:def_2; A71: ex C1 being Function st ( C1 = C & dom C1 = o2 & rng C1 c= o ) by A67, A68, FUNCT_2:def_2; assume B * A = C * A ; ::_thesis: B = C B1 = {} by A66, A70, RELAT_1:41; hence B = C by A66, A69, A71, RELAT_1:41; ::_thesis: verum end; end; end; end; hence ( A is epi iff F is onto ) ; ::_thesis: verum end; end; end; theorem Th15: :: ALTCAT_3:15 for C being category for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 st A is retraction holds A is epi proof let C be category; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 st A is retraction holds A is epi let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is retraction holds A is epi ) assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2 st A is retraction holds A is epi let A be Morphism of o1,o2; ::_thesis: ( A is retraction implies A is epi ) assume A is retraction ; ::_thesis: A is epi then consider R being Morphism of o2,o1 such that A2: R is_right_inverse_of A by Def2; let o be object of C; :: according to ALTCAT_3:def_8 ::_thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds B = C ) assume A3: <^o2,o^> <> {} ; ::_thesis: for B, C being Morphism of o2,o st B * A = C * A holds B = C let B, C be Morphism of o2,o; ::_thesis: ( B * A = C * A implies B = C ) assume A4: B * A = C * A ; ::_thesis: B = C thus B = B * (idm o2) by A3, ALTCAT_1:def_17 .= B * (A * R) by A2, Def1 .= (C * A) * R by A1, A3, A4, ALTCAT_1:21 .= C * (A * R) by A1, A3, ALTCAT_1:21 .= C * (idm o2) by A2, Def1 .= C by A3, ALTCAT_1:def_17 ; ::_thesis: verum end; theorem Th16: :: ALTCAT_3:16 for C being category for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 st A is coretraction holds A is mono proof let C be category; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 st A is coretraction holds A is mono let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is coretraction holds A is mono ) assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2 st A is coretraction holds A is mono let A be Morphism of o1,o2; ::_thesis: ( A is coretraction implies A is mono ) assume A is coretraction ; ::_thesis: A is mono then consider R being Morphism of o2,o1 such that A2: R is_left_inverse_of A by Def3; let o be object of C; :: according to ALTCAT_3:def_7 ::_thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds B = C ) assume A3: <^o,o1^> <> {} ; ::_thesis: for B, C being Morphism of o,o1 st A * B = A * C holds B = C let B, C be Morphism of o,o1; ::_thesis: ( A * B = A * C implies B = C ) assume A4: A * B = A * C ; ::_thesis: B = C thus B = (idm o1) * B by A3, ALTCAT_1:20 .= (R * A) * B by A2, Def1 .= R * (A * C) by A1, A3, A4, ALTCAT_1:21 .= (R * A) * C by A1, A3, ALTCAT_1:21 .= (idm o1) * C by A2, Def1 .= C by A3, ALTCAT_1:20 ; ::_thesis: verum end; theorem :: ALTCAT_3:17 for C being category for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 st A is iso holds ( A is mono & A is epi ) proof let C be category; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds for A being Morphism of o1,o2 st A is iso holds ( A is mono & A is epi ) let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is iso holds ( A is mono & A is epi ) ) assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2 st A is iso holds ( A is mono & A is epi ) let A be Morphism of o1,o2; ::_thesis: ( A is iso implies ( A is mono & A is epi ) ) assume A is iso ; ::_thesis: ( A is mono & A is epi ) then A2: ( A is retraction & A is coretraction ) by A1, Th6; A3: for o being object of C st <^o2,o^> <> {} holds for B, C being Morphism of o2,o st B * A = C * A holds B = C proof let o be object of C; ::_thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds B = C ) assume A4: <^o2,o^> <> {} ; ::_thesis: for B, C being Morphism of o2,o st B * A = C * A holds B = C let B, C be Morphism of o2,o; ::_thesis: ( B * A = C * A implies B = C ) assume B * A = C * A ; ::_thesis: B = C then B * (A * (A ")) = (C * A) * (A ") by A1, A4, ALTCAT_1:21; then B * (idm o2) = (C * A) * (A ") by A1, A2, Th2; then B * (idm o2) = C * (A * (A ")) by A1, A4, ALTCAT_1:21; then B * (idm o2) = C * (idm o2) by A1, A2, Th2; then B = C * (idm o2) by A4, ALTCAT_1:def_17; hence B = C by A4, ALTCAT_1:def_17; ::_thesis: verum end; for o being object of C st <^o,o1^> <> {} holds for B, C being Morphism of o,o1 st A * B = A * C holds B = C proof let o be object of C; ::_thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds B = C ) assume A5: <^o,o1^> <> {} ; ::_thesis: for B, C being Morphism of o,o1 st A * B = A * C holds B = C let B, C be Morphism of o,o1; ::_thesis: ( A * B = A * C implies B = C ) assume A * B = A * C ; ::_thesis: B = C then ((A ") * A) * B = (A ") * (A * C) by A1, A5, ALTCAT_1:21; then (idm o1) * B = (A ") * (A * C) by A1, A2, Th2; then (idm o1) * B = ((A ") * A) * C by A1, A5, ALTCAT_1:21; then (idm o1) * B = (idm o1) * C by A1, A2, Th2; then B = (idm o1) * C by A5, ALTCAT_1:20; hence B = C by A5, ALTCAT_1:20; ::_thesis: verum end; hence ( A is mono & A is epi ) by A3, Def7, Def8; ::_thesis: verum end; theorem Th18: :: ALTCAT_3:18 for C being category for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} holds for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is retraction & B is retraction holds B * A is retraction proof let C be category; ::_thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} holds for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is retraction & B is retraction holds B * A is retraction let o1, o2, o3 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} implies for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is retraction & B is retraction holds B * A is retraction ) assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} and A3: <^o3,o1^> <> {} ; ::_thesis: for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is retraction & B is retraction holds B * A is retraction A4: <^o2,o1^> <> {} by A2, A3, ALTCAT_1:def_2; A5: <^o3,o2^> <> {} by A1, A3, ALTCAT_1:def_2; let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st A is retraction & B is retraction holds B * A is retraction let B be Morphism of o2,o3; ::_thesis: ( A is retraction & B is retraction implies B * A is retraction ) assume that A6: A is retraction and A7: B is retraction ; ::_thesis: B * A is retraction consider A1 being Morphism of o2,o1 such that A8: A1 is_right_inverse_of A by A6, Def2; consider B1 being Morphism of o3,o2 such that A9: B1 is_right_inverse_of B by A7, Def2; consider G being Morphism of o3,o1 such that A10: G = A1 * B1 ; take G ; :: according to ALTCAT_3:def_2 ::_thesis: G is_right_inverse_of B * A (B * A) * G = B * (A * (A1 * B1)) by A1, A2, A3, A10, ALTCAT_1:21 .= B * ((A * A1) * B1) by A1, A4, A5, ALTCAT_1:21 .= B * ((idm o2) * B1) by A8, Def1 .= B * B1 by A5, ALTCAT_1:20 .= idm o3 by A9, Def1 ; hence G is_right_inverse_of B * A by Def1; ::_thesis: verum end; theorem Th19: :: ALTCAT_3:19 for C being category for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} holds for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds B * A is coretraction proof let C be category; ::_thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} holds for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds B * A is coretraction let o1, o2, o3 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} implies for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds B * A is coretraction ) assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} and A3: <^o3,o1^> <> {} ; ::_thesis: for A being Morphism of o1,o2 for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds B * A is coretraction A4: <^o2,o1^> <> {} by A2, A3, ALTCAT_1:def_2; A5: <^o3,o2^> <> {} by A1, A3, ALTCAT_1:def_2; let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds B * A is coretraction let B be Morphism of o2,o3; ::_thesis: ( A is coretraction & B is coretraction implies B * A is coretraction ) assume that A6: A is coretraction and A7: B is coretraction ; ::_thesis: B * A is coretraction consider A1 being Morphism of o2,o1 such that A8: A1 is_left_inverse_of A by A6, Def3; consider B1 being Morphism of o3,o2 such that A9: B1 is_left_inverse_of B by A7, Def3; consider G being Morphism of o3,o1 such that A10: G = A1 * B1 ; take G ; :: according to ALTCAT_3:def_3 ::_thesis: G is_left_inverse_of B * A A11: <^o2,o2^> <> {} by ALTCAT_1:19; G * (B * A) = ((A1 * B1) * B) * A by A1, A2, A3, A10, ALTCAT_1:21 .= (A1 * (B1 * B)) * A by A2, A4, A5, ALTCAT_1:21 .= (A1 * (idm o2)) * A by A9, Def1 .= A1 * ((idm o2) * A) by A1, A4, A11, ALTCAT_1:21 .= A1 * A by A1, ALTCAT_1:20 .= idm o1 by A8, Def1 ; hence G is_left_inverse_of B * A by Def1; ::_thesis: verum end; theorem Th20: :: ALTCAT_3:20 for C being category for o1, o2 being object of C for A being Morphism of o1,o2 st A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds A is iso proof let C be category; ::_thesis: for o1, o2 being object of C for A being Morphism of o1,o2 st A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds A is iso let o1, o2 be object of C; ::_thesis: for A being Morphism of o1,o2 st A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds A is iso let A be Morphism of o1,o2; ::_thesis: ( A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} implies A is iso ) assume that A1: A is retraction and A2: A is mono and A3: <^o1,o2^> <> {} and A4: <^o2,o1^> <> {} ; ::_thesis: A is iso consider B being Morphism of o2,o1 such that A5: B is_right_inverse_of A by A1, Def2; (A * B) * A = (idm o2) * A by A5, Def1; then A * (B * A) = (idm o2) * A by A3, A4, ALTCAT_1:21; then A * (B * A) = A by A3, ALTCAT_1:20; then A6: ( <^o1,o1^> <> {} & A * (B * A) = A * (idm o1) ) by A3, ALTCAT_1:19, ALTCAT_1:def_17; then B * A = idm o1 by A2, Def7; then A7: B is_left_inverse_of A by Def1; then A8: A is coretraction by Def3; then A9: A * (A ") = A * B by A1, A3, A4, A5, A7, Def4 .= idm o2 by A5, Def1 ; (A ") * A = B * A by A1, A3, A4, A5, A7, A8, Def4 .= idm o1 by A2, A6, Def7 ; hence A is iso by A9, Def5; ::_thesis: verum end; theorem :: ALTCAT_3:21 for C being category for o1, o2 being object of C for A being Morphism of o1,o2 st A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds A is iso proof let C be category; ::_thesis: for o1, o2 being object of C for A being Morphism of o1,o2 st A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds A is iso let o1, o2 be object of C; ::_thesis: for A being Morphism of o1,o2 st A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds A is iso let A be Morphism of o1,o2; ::_thesis: ( A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} implies A is iso ) assume that A1: A is coretraction and A2: A is epi and A3: <^o1,o2^> <> {} and A4: <^o2,o1^> <> {} ; ::_thesis: A is iso consider B being Morphism of o2,o1 such that A5: B is_left_inverse_of A by A1, Def3; A * (B * A) = A * (idm o1) by A5, Def1; then A * (B * A) = A by A3, ALTCAT_1:def_17; then A * (B * A) = (idm o2) * A by A3, ALTCAT_1:20; then A6: ( <^o2,o2^> <> {} & (A * B) * A = (idm o2) * A ) by A3, A4, ALTCAT_1:19, ALTCAT_1:21; then A * B = idm o2 by A2, Def8; then A7: B is_right_inverse_of A by Def1; then A8: A is retraction by Def2; then A9: (A ") * A = B * A by A1, A3, A4, A5, A7, Def4 .= idm o1 by A5, Def1 ; A * (A ") = A * B by A1, A3, A4, A5, A7, A8, Def4 .= idm o2 by A2, A6, Def8 ; hence A is iso by A9, Def5; ::_thesis: verum end; theorem :: ALTCAT_3:22 for C being category for o1, o2, o3 being object of C for A being Morphism of o1,o2 for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds B is retraction proof let C be category; ::_thesis: for o1, o2, o3 being object of C for A being Morphism of o1,o2 for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds B is retraction let o1, o2, o3 be object of C; ::_thesis: for A being Morphism of o1,o2 for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds B is retraction let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds B is retraction let B be Morphism of o2,o3; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction implies B is retraction ) assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} ) ; ::_thesis: ( not B * A is retraction or B is retraction ) assume B * A is retraction ; ::_thesis: B is retraction then consider G being Morphism of o3,o1 such that A2: G is_right_inverse_of B * A by Def2; (B * A) * G = idm o3 by A2, Def1; then B * (A * G) = idm o3 by A1, ALTCAT_1:21; then A * G is_right_inverse_of B by Def1; hence B is retraction by Def2; ::_thesis: verum end; theorem :: ALTCAT_3:23 for C being category for o1, o2, o3 being object of C for A being Morphism of o1,o2 for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction holds A is coretraction proof let C be category; ::_thesis: for o1, o2, o3 being object of C for A being Morphism of o1,o2 for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction holds A is coretraction let o1, o2, o3 be object of C; ::_thesis: for A being Morphism of o1,o2 for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction holds A is coretraction let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction holds A is coretraction let B be Morphism of o2,o3; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction implies A is coretraction ) assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} ) ; ::_thesis: ( not B * A is coretraction or A is coretraction ) assume B * A is coretraction ; ::_thesis: A is coretraction then consider G being Morphism of o3,o1 such that A2: G is_left_inverse_of B * A by Def3; A3: (G * B) * A = G * (B * A) by A1, ALTCAT_1:21; G * (B * A) = idm o1 by A2, Def1; then G * B is_left_inverse_of A by A3, Def1; hence A is coretraction by Def3; ::_thesis: verum end; theorem :: ALTCAT_3:24 for C being category st ( for o1, o2 being object of C for A1 being Morphism of o1,o2 holds A1 is retraction ) holds for a, b being object of C for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds A is iso proof let C be category; ::_thesis: ( ( for o1, o2 being object of C for A1 being Morphism of o1,o2 holds A1 is retraction ) implies for a, b being object of C for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds A is iso ) assume A1: for o1, o2 being object of C for A1 being Morphism of o1,o2 holds A1 is retraction ; ::_thesis: for a, b being object of C for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds A is iso thus for a, b being object of C for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds A is iso ::_thesis: verum proof let a, b be object of C; ::_thesis: for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds A is iso let A be Morphism of a,b; ::_thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies A is iso ) assume that A2: <^a,b^> <> {} and A3: <^b,a^> <> {} ; ::_thesis: A is iso A4: A is retraction by A1; A is coretraction proof consider A1 being Morphism of b,a such that A5: A1 is_right_inverse_of A by A4, Def2; A1 * (A * A1) = A1 * (idm b) by A5, Def1; then A1 * (A * A1) = A1 by A3, ALTCAT_1:def_17; then (A1 * A) * A1 = A1 by A2, A3, ALTCAT_1:21; then A6: (A1 * A) * A1 = (idm a) * A1 by A3, ALTCAT_1:20; ( A1 is epi & <^a,a^> <> {} ) by A1, A2, A3, Th15, ALTCAT_1:19; then A1 * A = idm a by A6, Def8; then A1 is_left_inverse_of A by Def1; hence A is coretraction by Def3; ::_thesis: verum end; hence A is iso by A2, A3, A4, Th6; ::_thesis: verum end; end; registration let C be non empty with_units AltCatStr ; let o be object of C; cluster retraction coretraction mono epi for Element of <^o,o^>; existence ex b1 being Morphism of o,o st ( b1 is mono & b1 is epi & b1 is retraction & b1 is coretraction ) proof take idm o ; ::_thesis: ( idm o is mono & idm o is epi & idm o is retraction & idm o is coretraction ) thus ( idm o is mono & idm o is epi & idm o is retraction & idm o is coretraction ) by Lm1, Th1; ::_thesis: verum end; end; registration let C be category; let o be object of C; cluster retraction coretraction iso mono epi for Element of <^o,o^>; existence ex b1 being Morphism of o,o st ( b1 is mono & b1 is epi & b1 is iso & b1 is retraction & b1 is coretraction ) proof take I = idm o; ::_thesis: ( I is mono & I is epi & I is iso & I is retraction & I is coretraction ) ( <^o,o^> <> {} & I is retraction & I is coretraction ) by Th1, ALTCAT_1:19; hence ( I is mono & I is epi & I is iso & I is retraction & I is coretraction ) by Th15, Th16, Th20; ::_thesis: verum end; end; registration let C be category; let o be object of C; let A, B be mono Morphism of o,o; clusterA * B -> mono ; coherence A * B is mono proof <^o,o^> <> {} by ALTCAT_1:19; hence A * B is mono by Th9; ::_thesis: verum end; end; registration let C be category; let o be object of C; let A, B be epi Morphism of o,o; clusterA * B -> epi ; coherence A * B is epi proof <^o,o^> <> {} by ALTCAT_1:19; hence A * B is epi by Th10; ::_thesis: verum end; end; registration let C be category; let o be object of C; let A, B be iso Morphism of o,o; clusterA * B -> iso ; coherence A * B is iso proof <^o,o^> <> {} by ALTCAT_1:19; hence A * B is iso by Th7; ::_thesis: verum end; end; registration let C be category; let o be object of C; let A, B be retraction Morphism of o,o; clusterA * B -> retraction ; coherence A * B is retraction proof <^o,o^> <> {} by ALTCAT_1:19; hence A * B is retraction by Th18; ::_thesis: verum end; end; registration let C be category; let o be object of C; let A, B be coretraction Morphism of o,o; clusterA * B -> coretraction ; coherence A * B is coretraction proof <^o,o^> <> {} by ALTCAT_1:19; hence A * B is coretraction by Th19; ::_thesis: verum end; end; definition let C be AltGraph ; let o be object of C; attro is initial means :Def9: :: ALTCAT_3:def 9 for o1 being object of C ex M being Morphism of o,o1 st ( M in <^o,o1^> & <^o,o1^> is trivial ); end; :: deftheorem Def9 defines initial ALTCAT_3:def_9_:_ for C being AltGraph for o being object of C holds ( o is initial iff for o1 being object of C ex M being Morphism of o,o1 st ( M in <^o,o1^> & <^o,o1^> is trivial ) ); theorem :: ALTCAT_3:25 for C being AltGraph for o being object of C holds ( o is initial iff for o1 being object of C 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 ) ) ) proof let C be AltGraph ; ::_thesis: for o being object of C holds ( o is initial iff for o1 being object of C 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 ) ) ) let o be object of C; ::_thesis: ( o is initial iff for o1 being object of C 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 ) ) ) thus ( o is initial implies for o1 being object of C 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 ) ) ) ::_thesis: ( ( for o1 being object of C 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 ) ) ) implies o is initial ) proof assume A1: o is initial ; ::_thesis: for o1 being object of C 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 ) ) let o1 be object of C; ::_thesis: 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 ) ) consider M being Morphism of o,o1 such that A2: M in <^o,o1^> and A3: <^o,o1^> is trivial by A1, Def9; ex i being set st <^o,o1^> = {i} by A2, A3, ZFMISC_1:131; then <^o,o1^> = {M} by TARSKI:def_1; then for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds M = M1 by TARSKI:def_1; hence 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 ) ) by A2; ::_thesis: verum end; assume A4: for o1 being object of C 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 ) ) ; ::_thesis: o is initial let o1 be object of C; :: according to ALTCAT_3:def_9 ::_thesis: ex M being Morphism of o,o1 st ( M in <^o,o1^> & <^o,o1^> is trivial ) consider M being Morphism of o,o1 such that A5: M in <^o,o1^> and A6: for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds M = M1 by A4; A7: <^o,o1^> c= {M} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in <^o,o1^> or x in {M} ) assume A8: x in <^o,o1^> ; ::_thesis: x in {M} then reconsider M1 = x as Morphism of o,o1 ; M1 = M by A6, A8; hence x in {M} by TARSKI:def_1; ::_thesis: verum end; {M} c= <^o,o1^> proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {M} or x in <^o,o1^> ) assume x in {M} ; ::_thesis: x in <^o,o1^> hence x in <^o,o1^> by A5, TARSKI:def_1; ::_thesis: verum end; then <^o,o1^> = {M} by A7, XBOOLE_0:def_10; hence ex M being Morphism of o,o1 st ( M in <^o,o1^> & <^o,o1^> is trivial ) ; ::_thesis: verum end; theorem Th26: :: ALTCAT_3:26 for C being category for o1, o2 being object of C st o1 is initial & o2 is initial holds o1,o2 are_iso proof let C be category; ::_thesis: for o1, o2 being object of C st o1 is initial & o2 is initial holds o1,o2 are_iso let o1, o2 be object of C; ::_thesis: ( o1 is initial & o2 is initial implies o1,o2 are_iso ) assume that A1: o1 is initial and A2: o2 is initial ; ::_thesis: o1,o2 are_iso ex N being Morphism of o2,o2 st ( N in <^o2,o2^> & <^o2,o2^> is trivial ) by A2, Def9; then consider y being set such that A3: <^o2,o2^> = {y} by ZFMISC_1:131; consider M2 being Morphism of o2,o1 such that A4: M2 in <^o2,o1^> and <^o2,o1^> is trivial by A2, Def9; consider M1 being Morphism of o1,o2 such that A5: M1 in <^o1,o2^> and <^o1,o2^> is trivial by A1, Def9; thus ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A5, A4; :: according to ALTCAT_3:def_6 ::_thesis: ex A being Morphism of o1,o2 st A is iso ( M1 * M2 = y & idm o2 = y ) by A3, TARSKI:def_1; then M2 is_right_inverse_of M1 by Def1; then A6: M1 is retraction by Def2; ex M being Morphism of o1,o1 st ( M in <^o1,o1^> & <^o1,o1^> is trivial ) by A1, Def9; then consider x being set such that A7: <^o1,o1^> = {x} by ZFMISC_1:131; ( M2 * M1 = x & idm o1 = x ) by A7, TARSKI:def_1; then M2 is_left_inverse_of M1 by Def1; then M1 is coretraction by Def3; then M1 is iso by A5, A4, A6, Th6; hence ex A being Morphism of o1,o2 st A is iso ; ::_thesis: verum end; definition let C be AltGraph ; let o be object of C; attro is terminal means :Def10: :: ALTCAT_3:def 10 for o1 being object of C ex M being Morphism of o1,o st ( M in <^o1,o^> & <^o1,o^> is trivial ); end; :: deftheorem Def10 defines terminal ALTCAT_3:def_10_:_ for C being AltGraph for o being object of C holds ( o is terminal iff for o1 being object of C ex M being Morphism of o1,o st ( M in <^o1,o^> & <^o1,o^> is trivial ) ); theorem :: ALTCAT_3:27 for C being AltGraph for o being object of C holds ( o is terminal iff for o1 being object of C 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 ) ) ) proof let C be AltGraph ; ::_thesis: for o being object of C holds ( o is terminal iff for o1 being object of C 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 ) ) ) let o be object of C; ::_thesis: ( o is terminal iff for o1 being object of C 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 ) ) ) thus ( o is terminal implies for o1 being object of C 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 ) ) ) ::_thesis: ( ( for o1 being object of C 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 ) ) ) implies o is terminal ) proof assume A1: o is terminal ; ::_thesis: for o1 being object of C 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 ) ) let o1 be object of C; ::_thesis: 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 ) ) consider M being Morphism of o1,o such that A2: M in <^o1,o^> and A3: <^o1,o^> is trivial by A1, Def10; ex i being set st <^o1,o^> = {i} by A2, A3, ZFMISC_1:131; then <^o1,o^> = {M} by TARSKI:def_1; then for M1 being Morphism of o1,o st M1 in <^o1,o^> holds M = M1 by TARSKI:def_1; hence 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 ) ) by A2; ::_thesis: verum end; assume A4: for o1 being object of C 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 ) ) ; ::_thesis: o is terminal let o1 be object of C; :: according to ALTCAT_3:def_10 ::_thesis: ex M being Morphism of o1,o st ( M in <^o1,o^> & <^o1,o^> is trivial ) consider M being Morphism of o1,o such that A5: M in <^o1,o^> and A6: for M1 being Morphism of o1,o st M1 in <^o1,o^> holds M = M1 by A4; A7: <^o1,o^> c= {M} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in <^o1,o^> or x in {M} ) assume A8: x in <^o1,o^> ; ::_thesis: x in {M} then reconsider M1 = x as Morphism of o1,o ; M1 = M by A6, A8; hence x in {M} by TARSKI:def_1; ::_thesis: verum end; {M} c= <^o1,o^> proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {M} or x in <^o1,o^> ) assume x in {M} ; ::_thesis: x in <^o1,o^> hence x in <^o1,o^> by A5, TARSKI:def_1; ::_thesis: verum end; then <^o1,o^> = {M} by A7, XBOOLE_0:def_10; hence ex M being Morphism of o1,o st ( M in <^o1,o^> & <^o1,o^> is trivial ) ; ::_thesis: verum end; theorem :: ALTCAT_3:28 for C being category for o1, o2 being object of C st o1 is terminal & o2 is terminal holds o1,o2 are_iso proof let C be category; ::_thesis: for o1, o2 being object of C st o1 is terminal & o2 is terminal holds o1,o2 are_iso let o1, o2 be object of C; ::_thesis: ( o1 is terminal & o2 is terminal implies o1,o2 are_iso ) assume that A1: o1 is terminal and A2: o2 is terminal ; ::_thesis: o1,o2 are_iso ex M being Morphism of o1,o1 st ( M in <^o1,o1^> & <^o1,o1^> is trivial ) by A1, Def10; then consider x being set such that A3: <^o1,o1^> = {x} by ZFMISC_1:131; consider M2 being Morphism of o2,o1 such that A4: M2 in <^o2,o1^> and <^o2,o1^> is trivial by A1, Def10; consider M1 being Morphism of o1,o2 such that A5: M1 in <^o1,o2^> and <^o1,o2^> is trivial by A2, Def10; thus ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A5, A4; :: according to ALTCAT_3:def_6 ::_thesis: ex A being Morphism of o1,o2 st A is iso M2 * M1 = x by A3, TARSKI:def_1; then M2 * M1 = idm o1 by A3, TARSKI:def_1; then M2 is_left_inverse_of M1 by Def1; then A6: M1 is coretraction by Def3; ex N being Morphism of o2,o2 st ( N in <^o2,o2^> & <^o2,o2^> is trivial ) by A2, Def10; then consider y being set such that A7: <^o2,o2^> = {y} by ZFMISC_1:131; M1 * M2 = y by A7, TARSKI:def_1; then M1 * M2 = idm o2 by A7, TARSKI:def_1; then M2 is_right_inverse_of M1 by Def1; then M1 is retraction by Def2; then M1 is iso by A5, A4, A6, Th6; hence ex A being Morphism of o1,o2 st A is iso ; ::_thesis: verum end; definition let C be AltGraph ; let o be object of C; attro is _zero means :Def11: :: ALTCAT_3:def 11 ( o is initial & o is terminal ); end; :: deftheorem Def11 defines _zero ALTCAT_3:def_11_:_ for C being AltGraph for o being object of C holds ( o is _zero iff ( o is initial & o is terminal ) ); theorem :: ALTCAT_3:29 for C being category for o1, o2 being object of C st o1 is _zero & o2 is _zero holds o1,o2 are_iso proof let C be category; ::_thesis: for o1, o2 being object of C st o1 is _zero & o2 is _zero holds o1,o2 are_iso let o1, o2 be object of C; ::_thesis: ( o1 is _zero & o2 is _zero implies o1,o2 are_iso ) assume ( o1 is _zero & o2 is _zero ) ; ::_thesis: o1,o2 are_iso then ( o1 is initial & o2 is initial ) by Def11; hence o1,o2 are_iso by Th26; ::_thesis: verum end; definition let C be non empty AltCatStr ; let o1, o2 be object of C; let M be Morphism of o1,o2; attrM is _zero means :Def12: :: ALTCAT_3:def 12 for o being object of C st o is _zero holds for A being Morphism of o1,o for B being Morphism of o,o2 holds M = B * A; end; :: deftheorem Def12 defines _zero ALTCAT_3:def_12_:_ for C being non empty AltCatStr for o1, o2 being object of C for M being Morphism of o1,o2 holds ( M is _zero iff for o being object of C st o is _zero holds for A being Morphism of o1,o for B being Morphism of o,o2 holds M = B * A ); theorem :: ALTCAT_3:30 for C being category for o1, o2, o3 being object of C for M1 being Morphism of o1,o2 for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds M2 * M1 is _zero proof let C be category; ::_thesis: for o1, o2, o3 being object of C for M1 being Morphism of o1,o2 for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds M2 * M1 is _zero let o1, o2, o3 be object of C; ::_thesis: for M1 being Morphism of o1,o2 for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds M2 * M1 is _zero let M1 be Morphism of o1,o2; ::_thesis: for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds M2 * M1 is _zero let M2 be Morphism of o2,o3; ::_thesis: ( M1 is _zero & M2 is _zero implies M2 * M1 is _zero ) assume that A1: M1 is _zero and A2: M2 is _zero ; ::_thesis: M2 * M1 is _zero let o be object of C; :: according to ALTCAT_3:def_12 ::_thesis: ( o is _zero implies for A being Morphism of o1,o for B being Morphism of o,o3 holds M2 * M1 = B * A ) assume A3: o is _zero ; ::_thesis: for A being Morphism of o1,o for B being Morphism of o,o3 holds M2 * M1 = B * A then A4: o is initial by Def11; then consider B1 being Morphism of o,o2 such that A5: B1 in <^o,o2^> and <^o,o2^> is trivial by Def9; let A be Morphism of o1,o; ::_thesis: for B being Morphism of o,o3 holds M2 * M1 = B * A let B be Morphism of o,o3; ::_thesis: M2 * M1 = B * A consider B2 being Morphism of o,o3 such that A6: B2 in <^o,o3^> and A7: <^o,o3^> is trivial by A4, Def9; consider y being set such that A8: <^o,o3^> = {y} by A6, A7, ZFMISC_1:131; A9: o is terminal by A3, Def11; then consider A1 being Morphism of o1,o such that A10: A1 in <^o1,o^> and A11: <^o1,o^> is trivial by Def10; consider x being set such that A12: <^o1,o^> = {x} by A10, A11, ZFMISC_1:131; ex M being Morphism of o,o st ( M in <^o,o^> & <^o,o^> is trivial ) by A9, Def10; then consider z being set such that A13: <^o,o^> = {z} by ZFMISC_1:131; consider A2 being Morphism of o2,o such that A14: A2 in <^o2,o^> and <^o2,o^> is trivial by A9, Def10; A15: ( idm o = z & A2 * B1 = z ) by A13, TARSKI:def_1; A16: ( B = y & B2 = y ) by A8, TARSKI:def_1; A17: ( A = x & A1 = x ) by A12, TARSKI:def_1; A18: <^o2,o3^> <> {} by A6, A14, ALTCAT_1:def_2; M2 = B2 * A2 by A2, A3, Def12; hence M2 * M1 = (B2 * A2) * (B1 * A1) by A1, A3, Def12 .= ((B2 * A2) * B1) * A1 by A5, A10, A18, ALTCAT_1:21 .= (B * (idm o)) * A by A5, A6, A14, A17, A16, A15, ALTCAT_1:21 .= B * A by A6, ALTCAT_1:def_17 ; ::_thesis: verum end;