The Mizar article:

Basic Properties of Objects and Morphisms

by
Beata Madras-Kobus

Received February 14, 1997

Copyright (c) 1997 Association of Mizar Users

MML identifier: ALTCAT_3
[ 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;
 definitions TARSKI;
 theorems CQC_LANG, RELAT_1, FUNCT_2, ZFMISC_1, ALTCAT_1, PARTFUN1, TARSKI,
      FUNCT_1, REALSET1, AMI_1, RELSET_1, XBOOLE_0, XBOOLE_1;
 schemes FUNCT_1;

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 :Def1:
 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 :Def2:
 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 :Def3:
 ex B being Morphism of o2,o1 st B is_left_inverse_of A;
end;

theorem Th1:
for C being with_units (non empty AltCatStr), o being object of C holds
idm o is retraction & idm o is coretraction
 proof
  let C be with_units (non empty AltCatStr), o be object of C;
    <^o,o^> <> {} by ALTCAT_1:23;
  then (idm o) * (idm o) = idm o by ALTCAT_1:def 19;
  then idm o is_left_inverse_of idm o & idm o is_right_inverse_of idm o by Def1
;
  hence thesis by Def2,Def3;
 end;

definition
let C be category,
    o1, o2 be object of C such that
 A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
let A be Morphism of o1,o2 such that
 A2: A is retraction coretraction;
func A" -> Morphism of o2,o1 means :Def4:
 it is_left_inverse_of A & it is_right_inverse_of A;
existence
 proof
  consider B1 being Morphism of o2,o1 such that
A3: B1 is_right_inverse_of A by A2,Def2;
  consider B2 being Morphism of o2,o1 such that
A4: B2 is_left_inverse_of A by A2,Def3;
A5: B1 = idm o1 * B1 by A1,ALTCAT_1:24
      .= B2 * A * B1 by A4,Def1
      .= B2 * (A * B1) by A1,ALTCAT_1:25
      .= B2 * idm o2 by A3,Def1
      .= B2 by A1,ALTCAT_1:def 19;
  take B1;
  thus thesis by A3,A4,A5;
 end;
uniqueness
 proof
  let M1,M2 be Morphism of o2,o1 such that
A6: M1 is_left_inverse_of A & M1 is_right_inverse_of A and
A7: M2 is_left_inverse_of A & M2 is_right_inverse_of A;
  thus M1 = M1 * idm o2 by A1,ALTCAT_1:def 19
         .= M1 * (A * M2) by A7,Def1
         .= M1 * A * M2 by A1,ALTCAT_1:25
         .= idm o1 * M2 by A6,Def1
         .= M2 by A1,ALTCAT_1:24;
 end;
end;

theorem Th2:
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
 proof
  let C be category,
      o1,o2 be object of C such that
A1:   <^o1,o2^> <> {} & <^o2,o1^> <> {};
  let A be Morphism of o1,o2; assume
     A is retraction & A is coretraction;
  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;
 end;

theorem Th3:
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
 proof
  let C be category,
      o1,o2 be object of C such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
  let A be Morphism of o1,o2; assume
   A is retraction & A is coretraction;
then A2: A" is_left_inverse_of A & A" is_right_inverse_of A by A1,Def4;
 then A" is retraction & A" is coretraction by Def2,Def3;
then A3: (A")" is_right_inverse_of A" by A1,Def4;
  thus (A")" = idm o2 * ((A")") by A1,ALTCAT_1:24
            .= A * A" * (A")" by A2,Def1
            .= A * (A" * (A")") by A1,ALTCAT_1:25
            .= A * idm o1 by A3,Def1
            .= A by A1,ALTCAT_1:def 19;
 end;

theorem Th4:
for C being category, o being object of C holds
(idm o)" = idm o
 proof
  let C be category, o be object of C;
A1: <^o,o^> <> {} by ALTCAT_1:23;
    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 19
               .= idm o by A2,Def1;
 end;

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

theorem Th5:
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
 proof
let C be category,
    o1, o2 be object of C,
    A be Morphism of o1,o2;
    assume A is iso;
then A1:  A * A" = idm o2 & A" * A = idm o1 by Def5;
     then A" is_right_inverse_of A by Def1;
     hence A is retraction by Def2;
       A" is_left_inverse_of A by A1,Def1;
     hence A is coretraction by Def3;
 end;

theorem Th6:
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
 proof
let C be category,
    o1,o2 be object of C such that
A1:<^o1,o2^> <> {} & <^o2,o1^> <> {};
let A be Morphism of o1,o2;
  thus A is iso implies A is retraction & A is coretraction by Th5;
   assume that
A2:  A is retraction and
A3:  A is coretraction;
       A" is_left_inverse_of A &
     A" is_right_inverse_of A by A1,A2,A3,Def4;
     then A" * A = idm o1 & A * A" = idm o2 by Def1;
   hence A is iso by Def5;
 end;

theorem Th7:
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"
 proof
  let C be category,
      o1,o2,o3 be object of C,
      A be Morphism of o1,o2,
      B be Morphism of o2,o3; assume
A1:<^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {};
then A2: <^o2,o1^> <> {} & <^o3,o2^> <> {} & <^o1,o3^> <> {}
 by ALTCAT_1:def 4;
   assume
  A is iso & B is iso;
then A3: A is retraction & A is coretraction &
   B is retraction & B is coretraction by A1,A2,Th6;
  consider A1 be Morphism of o2,o1 such that A4: A1 = A";
  consider B1 be Morphism of o3,o2 such that A5: B1 = B";
A6:(A1*B1)*(B*A) = A1*(B1*(B*A)) by A2,ALTCAT_1:25
               .= A1*(B1*B*A) by A1,A2,ALTCAT_1:25
               .= A1*((idm o2)*A) by A1,A2,A3,A5,Th2
               .= A1*A by A1,ALTCAT_1:24
               .= idm o1 by A1,A2,A3,A4,Th2;
then A7:(A1*B1) is_left_inverse_of (B*A) by Def1;
then A8:(B*A) is coretraction by Def3;
A9:(B*A)*(A1*B1) = B*(A*(A1*B1)) by A1,ALTCAT_1:25
               .= B*(A*A1*B1) by A1,A2,ALTCAT_1:25
               .= B*((idm o2)*B1) by A1,A2,A3,A4,Th2
               .= B*B1 by A2,ALTCAT_1:24
               .= idm o3 by A1,A2,A3,A5,Th2;
then A10:(A1*B1) is_right_inverse_of (B*A) by Def1;
  then (B*A) is retraction by Def2;
  then A1*B1 = (B*A)" by A1,A2,A7,A8,A10,Def4;
  hence thesis by A4,A5,A6,A9,Def5;
 end;

definition
let C be category,
    o1, o2 be object of C;
pred o1,o2 are_iso means :Def6:
 <^o1,o2^> <> {} & <^o2,o1^> <> {} &
  ex A being Morphism of o1,o2 st A is iso;
reflexivity
 proof
  let o be object of C;
  thus A1: <^o,o^> <> {} & <^o,o^> <> {} by ALTCAT_1:23;
  take idm o;
set A = idm o;
A2:  A*A" = A * A by Th4
      .= idm o by A1,ALTCAT_1:def 19;
        A"*A = A * A by Th4
      .= idm o by A1,ALTCAT_1:def 19;
  hence thesis by A2,Def5;
 end;
symmetry
 proof
  let o1,o2 be object of C; assume that
A3:  <^o1,o2^> <> {} & <^o2,o1^> <> {} and
A4:  ex A being Morphism of o1,o2 st A is iso;
  consider A being Morphism of o1,o2 such that A5: A is iso by A4;
A6: A is retraction & A is coretraction by A5,Th5;
  thus <^o2,o1^> <> {} & <^o1,o2^> <> {} by A3;
  take A1 = A";
A7: A1*A1" = A" * A by A3,A6,Th3
          .= idm o1 by A3,A6,Th2;
     A1"*A1 = A * A" by A3,A6,Th3
          .= idm o2 by A3,A6,Th2;
  hence thesis by A7,Def5;
 end;
end;

theorem
  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
 proof
  let C be category, o1,o2,o3 be object of C such that
A1: o1,o2 are_iso and
A2: o2,o3 are_iso;
A3: <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {}
                                                    by A1,A2,Def6;
  hence A4: <^o1,o3^> <> {} & <^o3,o1^> <> {} by ALTCAT_1:def 4;
  consider A being Morphism of o1,o2 such that
A5: A is iso by A1,Def6;
  consider B being Morphism of o2,o3 such that
A6: B is iso by A2,Def6;
  take B * A;
  thus thesis by A3,A4,A5,A6,Th7;
 end;

definition
let C be non empty AltCatStr,
    o1, o2 be object of C,
    A be Morphism of o1,o2;
attr A is mono means :Def7:
 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 :Def8:
 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 Th9:
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
 proof
  let C be associative transitive (non empty AltCatStr),
      o1,o2,o3 be object of C; assume
A1:<^o1,o2^> <> {} & <^o2,o3^> <> {};
  let A be Morphism of o1,o2,
      B be Morphism of o2,o3; assume
A2: A is mono & B is mono;
   let o be object of C; assume A3: <^o,o1^> <> {};
   let M1,M2 be Morphism of o,o1; assume
A4:(B*A)*M1 = (B*A)*M2;
A5:(B*A)*M1 = B*(A*M1) by A1,A3,ALTCAT_1:25;
A6:(B*A)*M2 = B*(A*M2) by A1,A3,ALTCAT_1:25;
     <^o,o2^> <> {} by A1,A3,ALTCAT_1:def 4;
   then A*M1 = A*M2 by A2,A4,A5,A6,Def7;
    hence M1 = M2 by A2,A3,Def7;
 end;

theorem Th10:
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
 proof
  let C be associative transitive (non empty AltCatStr),
      o1,o2,o3 be object of C; assume
A1:<^o1,o2^> <> {} & <^o2,o3^> <> {};
  let A be Morphism of o1,o2,
      B be Morphism of o2,o3; assume
A2: A is epi & B is epi;
   let o be object of C; assume A3: <^o3,o^> <> {};
   let M1,M2 be Morphism of o3,o; assume
A4:M1*(B*A) = M2*(B*A);
A5:M1*(B*A) = (M1*B)*A by A1,A3,ALTCAT_1:25;
A6:M2*(B*A) = (M2*B)*A by A1,A3,ALTCAT_1:25;
     <^o2,o^> <> {} by A1,A3,ALTCAT_1:def 4;
   then M1*B = M2*B by A2,A4,A5,A6,Def8;
   hence M1 = M2 by A2,A3,Def8;
 end;

theorem
  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
 proof
  let C be associative transitive (non empty AltCatStr),
      o1,o2,o3 be object of C; assume
A1: <^o1,o2^> <> {} & <^o2,o3^> <> {};
  let A be Morphism of o1,o2,
      B be Morphism of o2,o3; assume
A2: B * A is mono;
   let o be object of C; assume A3: <^o,o1^> <> {};
   let M1,M2 be Morphism of o,o1; assume
A4:   A*M1 = A*M2;
A5:(B*A)*M1 = B*(A*M1) by A1,A3,ALTCAT_1:25;
     (B*A)*M2 = B*(A*M2) by A1,A3,ALTCAT_1:25;
   hence M1 = M2 by A2,A3,A4,A5,Def7;
 end;

theorem
  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
 proof
  let C be associative transitive (non empty AltCatStr),
      o1,o2,o3 be object of C; assume
A1: <^o1,o2^> <> {} & <^o2,o3^> <> {};
  let A be Morphism of o1,o2,
      B be Morphism of o2,o3; assume
A2: B * A is epi;
   let o be object of C; assume A3: <^o3,o^> <> {};
   let M1,M2 be Morphism of o3,o; assume
A4: M1*B = M2*B;
A5:(M1*B)*A = M1*(B*A) by A1,A3,ALTCAT_1:25;
     (M2*B)*A = M2*(B*A) by A1,A3,ALTCAT_1:25;
   hence M1 = M2 by A2,A3,A4,A5,Def8;
 end;

Lm1:
now
  let C be with_units (non empty AltCatStr),
      a be object of C;
  thus idm a is epi
  proof
    let o be object of C such that
A1:   <^a,o^> <> {};
    let B, C be Morphism of a,o such that
A2:   B * idm a = C * idm a;
    thus B = B * idm a by A1,ALTCAT_1:def 19
          .= C by A1,A2,ALTCAT_1:def 19;
  end;
  thus idm a is mono
  proof
    let o be object of C such that
A3:   <^o,a^> <> {};
    let B, C be Morphism of o,a such that
A4:   idm a * B = idm a * C;
    thus B = idm a * B by A3,ALTCAT_1:24
          .= C by A3,A4,ALTCAT_1:24;
  end;
end;

theorem
  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
 proof
  let X be non empty set,
      o1,o2 be object of EnsCat X; assume
A1: <^o1,o2^> <> {};
  let A be Morphism of o1,o2,
      F be Function of o1,o2; assume
A2: F = A;
  per cases;
  suppose o2 <> {};
then A3: dom F = o1 by FUNCT_2:def 1;
  thus A is mono implies F is one-to-one
   proof
    assume
A4:  A is mono;
    assume not F is one-to-one;
    then consider x1,x2 be set such that
A5: x1 in dom F & x2 in dom F and
A6: F.x1 = F.x2 and
A7: x1 <> x2 by FUNCT_1:def 8;
    set o = o1;
A8:  <^o,o1^> <> {} by ALTCAT_1:23;
    deffunc G(set) = x1;
    consider B be Function such that
A9: dom B = o and
A10: for x be set st x in o holds B.x = G(x) from Lambda;
    deffunc H(set) = x2;
    consider C be Function such that
A11: dom C = o and
A12: for x be set st x in o holds C.x = H(x) from Lambda;
    consider o' be Element of o;
   B.o' = x1 by A3,A5,A10;
then A13: B.o' <> C.o' by A3,A5,A7,A12;
A14: rng B c= o1
     proof
      let y be set; assume y in rng B;
      then consider x be set such that
A15:     x in dom B & B.x = y by FUNCT_1:def 5;
      thus y in o1 by A3,A5,A9,A10,A15;
     end;
    then B in Funcs(o,o1) by A9,FUNCT_2:def 2;
    then B in <^o,o1^> by ALTCAT_1:def 16;
    then reconsider B1=B as Morphism of o,o1;
A16: rng C c= o1
     proof
      let y be set; assume y in rng C;
      then consider x be set such that
A17:     x in dom C & C.x = y by FUNCT_1:def 5;
      thus y in o1 by A3,A5,A11,A12,A17;
     end;
    then C in Funcs(o,o1) by A11,FUNCT_2:def 2;
    then C in <^o,o1^> by ALTCAT_1:def 16;
    then reconsider C1=C as Morphism of o,o1;
A18: dom (F * B) = o by A3,A9,A14,RELAT_1:46;
A19: dom (F * C) = o by A3,A11,A16,RELAT_1:46;
      now let z be set; assume A20: z in o;
     hence (F * B).z = F.(B.z) by A18,FUNCT_1:22
                    .= F.x2 by A6,A10,A20
                    .= F.(C.z) by A12,A20
                    .= (F * C).z by A19,A20,FUNCT_1:22;
    end;
    then F * B = F * C by A18,A19,FUNCT_1:9;
    then A * B1 = F * C by A1,A2,A8,ALTCAT_1:18
          .= A * C1 by A1,A2,A8,ALTCAT_1:18;
    hence contradiction by A4,A8,A13,Def7;
   end;
  thus F is one-to-one implies A is mono
   proof
    assume A21: F is one-to-one;
    let o be object of EnsCat X; assume
A22: <^o,o1^> <> {};
    let B,C be Morphism of o,o1; assume
A23: A * B = A * C;
A24:  <^o,o1^> = Funcs(o,o1) by ALTCAT_1:def 16;
    then consider B1 be Function such that
A25: B1 = B & dom B1 = o & rng B1 c= o1 by A22,FUNCT_2:def 2;
    consider C1 be Function such that
A26: C1 = C & dom C1 = o & rng C1 c= o1 by A22,A24,FUNCT_2:def 2;
A27: <^o,o2^> <> {} by A1,A22,ALTCAT_1:def 4;
then A28: F * B1 = A * C by A1,A2,A22,A23,A25,ALTCAT_1:18
          .= F * C1 by A1,A2,A22,A26,A27,ALTCAT_1:18;
      now let z be set; assume A29: z in o;
then A30:  B1.z in rng B1 & C1.z in rng C1 by A25,A26,FUNCT_1:def 5;
       F.(B1.z) = (F*B1).z by A25,A29,FUNCT_1:23;
     then F.(B1.z) = F.(C1.z) by A26,A28,A29,FUNCT_1:23;
     hence B1.z = C1.z by A3,A21,A25,A26,A30,FUNCT_1:def 8;
    end;
    hence B = C by A25,A26,FUNCT_1:9;
   end;
   suppose A31: o2 = {};
A32:   now per cases;
      suppose o1 = {};
      hence F = {} by PARTFUN1:57;
     suppose o1 <> {};
      hence F = {} by A31,FUNCT_2:def 1;
     end;
   thus A is mono implies F is one-to-one
    proof
     assume A is mono;
     reconsider F1 = F as Function of {},(rng F) by A32,FUNCT_2:55,RELAT_1:60;
       F1 is one-to-one by PARTFUN1:59;
     hence thesis;
    end;
   thus F is one-to-one implies A is mono
    proof
     assume F is one-to-one;
     let o be object of EnsCat X; assume
A33:  <^o,o1^> <> {};
     let B,C be Morphism of o,o1; assume
       A * B = A * C;
A34:   <^o,o1^> = Funcs(o,o1) by ALTCAT_1:def 16;
     then consider B1 be Function such that
A35:  B1 = B & dom B1 = o & rng B1 c= o1 by A33,FUNCT_2:def 2;
     consider C1 be Function such that
A36:  C1 = C & dom C1 = o & rng C1 c= o1 by A33,A34,FUNCT_2:def 2;
A37:  <^o1,o2^> = Funcs(o1,o2) by ALTCAT_1:def 16;
     consider x be Element of Funcs(o1,o2);
     consider f be Function such that
A38:  f = x & dom f = o1 & rng f c= o2 by A1,A37,FUNCT_2:def 2;
       rng f = {} by A31,A38,XBOOLE_1:3;
     then dom f = {} by RELAT_1:65;
then A39:  rng B1 = {} by A35,A38,XBOOLE_1:3;
then A40:  dom B1 = {} by RELAT_1:65;
       B1 = {} by A39,RELAT_1:64
       .= C1 by A35,A36,A40,RELAT_1:64;
     hence thesis by A35,A36;
    end;
 end;

theorem
  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
 proof
  let X be non empty with_non-empty_elements set,
        o1,o2 be object of EnsCat X; assume
A1: <^o1,o2^> <> {};
  let A be Morphism of o1,o2,
      F be Function of o1,o2; assume
A2: F = A;
  per cases;
  suppose A3: for x be set st x in X holds x is trivial;
  thus A is epi implies F is onto
   proof
   assume A is epi;
    now per cases;
   suppose A4: o2 = {};
      now per cases;
      suppose o1 = {};
      hence F = {} by PARTFUN1:57;
      suppose o1 <> {};
      hence F = {} by A4,FUNCT_2:def 1;
     end;
   hence F is onto by A4,FUNCT_2:def 3,PARTFUN1:10;
   suppose A5: o2 <> {};
      o2 is Element of X by ALTCAT_1:def 16;
    then o2 is trivial by A3;
    then consider y be set such that
A6:  o2 = {y} by A5,REALSET1:def 12;
A7: rng F c= {y} by A6,RELSET_1:12;
A8: o1 is Element of X by ALTCAT_1:def 16;
then A9: o1 <> {} by AMI_1:def 1;
      o1 is trivial by A3,A8;
    then consider z be set such that
A10:  o1 = {z} by A9,REALSET1:def 12;
      dom F = {z} by A5,A10,FUNCT_2:def 1;
    then rng F <> {} by RELAT_1:65;
    then rng F = {y} by A7,ZFMISC_1:39;
    hence F is onto by A6,FUNCT_2:def 3;
   end;
    hence thesis;
   end;
  thus F is onto implies A is epi
   proof assume
A11: F is onto;
    let o be object of EnsCat X; assume A12: <^o2,o^> <> {};
    let B,C be Morphism of o2,o; assume A13: B * A = C * A;
A14:  <^o2,o^> = Funcs(o2,o) by ALTCAT_1:def 16;
    then consider B1 be Function such that
A15: B1 = B & dom B1 = o2 & rng B1 c= o by A12,FUNCT_2:def 2;
    consider C1 be Function such that
A16: C1 = C & dom C1 = o2 & rng C1 c= o by A12,A14,FUNCT_2:def 2;
A17: <^o1,o^> <> {} by A1,A12,ALTCAT_1:def 4;
then A18: B1 * F = C * A by A1,A2,A12,A13,A15,ALTCAT_1:18
          .= C1 * F by A1,A2,A12,A16,A17,ALTCAT_1:18;
      now assume B1 <> C1;
     then consider z be set such that
A19:  z in o2 & B1.z <> C1.z by A15,A16,FUNCT_1:9;
       z in rng F by A11,A19,FUNCT_2:def 3;
     then consider x be set such that
A20:    x in dom F & F.x = z by FUNCT_1:def 5;
       B1.(F.x) = (B1*F).x by A20,FUNCT_1:23;
     hence contradiction by A18,A19,A20,FUNCT_1:23;
    end;
  hence thesis by A15,A16;
  end;
  suppose A21: ex x be set st x in X & x is non trivial;
     now per cases;
    suppose o2 <> {};
then A22:  dom F = o1 by FUNCT_2:def 1;
    consider o be set such that
A23: o in X and
A24: o is non trivial by A21;
      o in the carrier of EnsCat X by A23,ALTCAT_1:def 16;
    then reconsider o as object of EnsCat X;
  thus A is epi implies F is onto
   proof
    assume that
A25: A is epi and
A26: not F is onto;
A27: rng F c= o2 by RELSET_1:12;
      rng F <> o2 by A26,FUNCT_2:def 3;
    then not o2 c= rng F by A27,XBOOLE_0:def 10;
    then consider y be set such that
A28: y in o2 & not y in rng F by TARSKI:def 3;
A29:  o <> {} by A23,AMI_1:def 1;
    consider k be Element of o;
    reconsider ok = (o\{k}) as non empty set by A24,A29,REALSET1:32;
    consider l be Element of ok;
A30: l in o & not l in {k} by XBOOLE_0:def 4;
    reconsider l as Element of o by XBOOLE_0:def 4;
A31: k <> l by A30,TARSKI:def 1;
A32: k in o & l in o by A29;
    deffunc G(set) = IFEQ($1,y,l,k);
    consider B be Function such that
A33: dom B = o2 and
A34: for x be set st x in o2 holds B.x = G(x) from Lambda;
    deffunc G(set) = k;
    consider C be Function such that
A35: dom C = o2 and
A36: for x be set st x in o2 holds C.x = G(x) from Lambda;
      B.y = IFEQ(y,y,l,k) by A28,A34
       .= l by CQC_LANG:def 1;
then A37:  not B = C by A28,A31,A36;
A38: rng B c= o
     proof
      let y1 be set; assume y1 in rng B;
      then consider x be set such that A39: x in dom B & B.x = y1 by FUNCT_1:
def 5;
      per cases;
      suppose A40: x = y;
         y1 = IFEQ(x,y,l,k) by A33,A34,A39
         .= l by A40,CQC_LANG:def 1;
       hence y1 in o by A29;
      suppose A41: x <> y;
         y1 = IFEQ(x,y,l,k) by A33,A34,A39
         .= k by A41,CQC_LANG:def 1;
       hence y1 in o by A29;
     end;
    then B in Funcs(o2,o) by A33,FUNCT_2:def 2;
then A42: B in <^o2,o^> by ALTCAT_1:def 16;
    then reconsider B1=B as Morphism of o2,o;
      rng C c= o
     proof
      let y be set; assume y in rng C;
      then consider x be set such that
A43:     x in dom C & C.x = y by FUNCT_1:def 5;
      thus y in o by A32,A35,A36,A43;
     end;
    then C in Funcs(o2,o) by A35,FUNCT_2:def 2;
    then C in <^o2,o^> by ALTCAT_1:def 16;
    then reconsider C1=C as Morphism of o2,o;
A44: dom (B*F) = o1 by A22,A27,A33,RELAT_1:46;
      for z be set holds z in rng(B*F) implies z in rng B by FUNCT_1:25;
    then rng (B*F) c= rng B by TARSKI:def 3;
    then rng (B*F) c= o by A38,XBOOLE_1:1;
    then (B*F) in Funcs(o1,o) by A44,FUNCT_2:def 2;
then A45:  (B*F) in <^o1,o^> by ALTCAT_1:def 16;
A46: dom (C*F) = o1 by A22,A27,A35,RELAT_1:46;
      now let z be set; assume A47: z in o1;
then A48:  F.z in rng F by A22,FUNCT_1:def 5;
then A49:  B.(F.z) = IFEQ((F.z),y,l,k) by A27,A34
            .= k by A28,A48,CQC_LANG:def 1;
     thus (B * F).z = B.(F.z) by A44,A47,FUNCT_1:22
                    .= C.(F.z) by A27,A36,A48,A49
                    .= (C * F).z by A46,A47,FUNCT_1:22;
    end;
    then B * F = C * F by A44,A46,FUNCT_1:9;
    then B1 * A = C * F by A1,A2,A42,A45,ALTCAT_1:18
          .= C1 * A by A1,A2,A42,A45,ALTCAT_1:18;
    hence contradiction by A25,A37,A42,Def8;
   end;
  thus F is onto implies A is epi
   proof
    assume A50: F is onto;
    let o be object of EnsCat X; assume A51: <^o2,o^> <> {};
    let B,C be Morphism of o2,o; assume A52: B * A = C * A;
A53:  <^o2,o^> = Funcs(o2,o) by ALTCAT_1:def 16;
    then consider B1 be Function such that
A54: B1 = B & dom B1 = o2 & rng B1 c= o by A51,FUNCT_2:def 2;
    consider C1 be Function such that
A55: C1 = C & dom C1 = o2 & rng C1 c= o by A51,A53,FUNCT_2:def 2;
A56: <^o1,o^> <> {} by A1,A51,ALTCAT_1:def 4;
then A57: B1 * F = C * A by A1,A2,A51,A52,A54,ALTCAT_1:18
          .= C1 * F by A1,A2,A51,A55,A56,ALTCAT_1:18;
      now assume B1 <> C1;
     then consider z be set such that
A58:  z in o2 & B1.z <> C1.z by A54,A55,FUNCT_1:9;
       z in rng F by A50,A58,FUNCT_2:def 3;
     then consider x be set such that
A59:    x in dom F & F.x = z by FUNCT_1:def 5;
       B1.(F.x) = (B1*F).x by A59,FUNCT_1:23;
     hence contradiction by A57,A58,A59,FUNCT_1:23;
    end;
    hence thesis by A54,A55;
   end;
    suppose A60: o2 = {};
    now per cases;
      suppose o1 = {};
      hence F = {} by PARTFUN1:57;

      suppose o1 <> {};
      hence F = {} by A60,FUNCT_2:def 1;
     end;
  hence A is epi implies F is onto by A60,FUNCT_2:def 3,PARTFUN1:10;
  thus F is onto implies A is epi
   proof
     assume F is onto;
     let o be object of EnsCat X; assume
A61:  <^o2,o^> <> {};
     let B,C be Morphism of o2,o; assume
       B * A = C * A;
A62:   <^o2,o^> = Funcs(o2,o) by ALTCAT_1:def 16;
     then consider B1 be Function such that
A63:  B1 = B & dom B1 = o2 & rng B1 c= o by A61,FUNCT_2:def 2;
     consider C1 be Function such that
A64:    C1 = C & dom C1 = o2 & rng C1 c= o by A61,A62,FUNCT_2:def 2;
       B1 = {} & C1 = {} by A60,A63,A64,RELAT_1:64;
     hence thesis by A63,A64;
    end;
  end;
  hence thesis;
 end;

theorem Th15:
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
 proof
  let C be category,
      o1,o2 be object of C; assume
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
  let A be Morphism of o1,o2; assume
    A is retraction;
  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; assume
A3: <^o2,o^> <> {};
  let B,C be Morphism of o2,o; assume
A4: B * A = C * A;
  thus B = B * idm o2 by A3,ALTCAT_1:def 19
        .= B * (A * R) by A2,Def1
        .= C * A * R by A1,A3,A4,ALTCAT_1:25
        .= C * (A * R) by A1,A3,ALTCAT_1:25
        .= C * idm o2 by A2,Def1
        .= C by A3,ALTCAT_1:def 19;
 end;

theorem Th16:
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
 proof
  let C be category,
      o1,o2 be object of C; assume
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
  let A be Morphism of o1,o2; assume
    A is coretraction;
  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; assume
A3: <^o,o1^> <> {};
  let B,C be Morphism of o,o1; assume
A4: A * B = A * C;
  thus B = idm o1 * B by A3,ALTCAT_1:24
        .= R * A * B by A2,Def1
        .= R * (A * C) by A1,A3,A4,ALTCAT_1:25
        .= R * A * C by A1,A3,ALTCAT_1:25
        .= idm o1 * C by A2,Def1
        .= C by A3,ALTCAT_1:24;
 end;

theorem
  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
proof
  let C be category;
  let o1, o2 be object of C such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
  let A be Morphism of o1, o2;
  assume
    A is iso;
then A2:  A is retraction & A is coretraction by A1,Th6;
A3:  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
  proof
    let o be object of C such that
  A4: <^o,o1^> <> {};
    let B, C be Morphism of o, o1;
    assume A * B = A * C;
    then (A" * A) * B = A" * (A * C) by A1,A4,ALTCAT_1:25;
    then idm o1 * B = A" * (A * C) by A1,A2,Th2;
    then idm o1 * B = (A" * A) * C by A1,A4,ALTCAT_1:25;
    then idm o1 * B = idm o1 * C by A1,A2,Th2;
    then B = idm o1 * C by A4,ALTCAT_1:24;
    hence B = C by A4,ALTCAT_1:24;
  end;
    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
  proof
    let o be object of C such that
  A5:  <^o2,o^> <> {};
    let B, C be Morphism of o2, o;
    assume B * A = C * A;
    then B * (A * A") = (C * A) * A" by A1,A5,ALTCAT_1:25;
    then B * idm o2 = (C * A) * A" by A1,A2,Th2;
    then B * idm o2 = C * (A * A") by A1,A5,ALTCAT_1:25;
    then B * idm o2 = C * idm o2 by A1,A2,Th2;
    then B = C * idm o2 by A5,ALTCAT_1:def 19;
    hence B = C by A5,ALTCAT_1:def 19;
  end;
  hence A is mono & A is epi by A3,Def7,Def8;
end;

theorem Th18:
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
proof
 let C be category,
     o1,o2,o3 be object of C;
     assume A1: <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {};
then A2:   <^o2,o1^> <> {} & <^o3,o2^> <> {} & <^o1,o3^> <> {} by ALTCAT_1:def
4;
  let A be Morphism of o1,o2, B be Morphism of o2,o3;
  assume A3: A is retraction & B is retraction;
   then consider A1 being Morphism of o2,o1 such that
A4:  A1 is_right_inverse_of A by Def2;
   consider B1 being Morphism of o3,o2 such that
A5:   B1 is_right_inverse_of B by A3,Def2;
   consider G being Morphism of o3,o1 such that
A6:            G = A1 * B1;
   take G;
     (B * A) * G = B * (A * (A1 * B1)) by A1,A6,ALTCAT_1:25
              .= B * ((A * A1) * B1) by A1,A2,ALTCAT_1:25
              .= B * (idm o2 * B1) by A4,Def1
              .= B * B1 by A2,ALTCAT_1:24
              .= idm o3 by A5,Def1;
  hence G is_right_inverse_of B*A by Def1;
end;

theorem Th19:
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
proof
 let C be category,
     o1,o2,o3 be object of C;
     assume A1: <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {};
then A2:   <^o2,o1^> <> {} & <^o3,o2^> <> {} & <^o1,o3^> <> {} by ALTCAT_1:def
4;
  let A be Morphism of o1,o2, B be Morphism of o2,o3;
  assume A3: A is coretraction & B is coretraction;
   then consider A1 being Morphism of o2,o1 such that
A4:  A1 is_left_inverse_of A by Def3;
   consider B1 being Morphism of o3,o2 such that
A5:  B1 is_left_inverse_of B by A3,Def3;
   consider G being Morphism of o3,o1 such that
A6:            G = A1 * B1;
   take G;
A7: <^o2,o2^> <> {} by ALTCAT_1:23;
    G * (B * A) = ((A1 * B1) * B) * A by A1,A6,ALTCAT_1:25
              .= (A1 * (B1 * B)) * A by A1,A2,ALTCAT_1:25
              .= (A1 * idm o2) * A by A5,Def1
              .= A1 * (idm o2 *A) by A1,A2,A7,ALTCAT_1:25
              .= A1 * A by A1,ALTCAT_1:24
              .= idm o1 by A4,Def1;
  hence G is_left_inverse_of B*A by Def1;
end;

theorem Th20:
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
  proof
   let C be category,
       o1, o2 be object of C,
       A be Morphism of o1,o2;
    assume that
A1: A is retraction & A is mono and
A2: <^o1,o2^> <> {} & <^o2,o1^> <> {};
A3: <^o1,o1^> <> {} by ALTCAT_1:23;
    consider B being Morphism of o2,o1 such that
A4:    B is_right_inverse_of A by A1,Def2;
       A * B * A = (idm o2) * A by A4,Def1;
     then A * (B * A) = (idm o2) * A by A2,ALTCAT_1:25;
     then A * (B * A) = A by A2,ALTCAT_1:24;
then A5:  A * (B * A) = A * idm o1 by A2,ALTCAT_1:def 19;
     then B * A = idm o1 by A1,A3,Def7;
then A6:  B is_left_inverse_of A by Def1;
then A7:  A is coretraction by Def3;
then A8:  A*A" = A * B by A1,A2,A4,A6,Def4
         .= idm o2 by A4,Def1;
       A"*A = B * A by A1,A2,A4,A6,A7,Def4
         .= idm o1 by A1,A3,A5,Def7;
    hence thesis by A8,Def5;
  end;

theorem
  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
  proof
     let C be category,
       o1, o2 be object of C,
       A be Morphism of o1,o2;
    assume that
A1: A is coretraction & A is epi and
A2: <^o1,o2^> <> {} & <^o2,o1^> <> {};
A3:  <^o2,o2^> <> {} by ALTCAT_1:23;
    consider B being Morphism of o2,o1 such that
A4:    B is_left_inverse_of A by A1,Def3;
       A * (B * A) = A * (idm o1) by A4,Def1;
     then A * (B * A) = A by A2,ALTCAT_1:def 19;
     then A * (B * A) = idm o2 * A by A2,ALTCAT_1:24;
then A5:  (A * B) * A = idm o2 * A by A2,ALTCAT_1:25;
     then A * B = idm o2 by A1,A3,Def8;
then A6:  B is_right_inverse_of A by Def1;
then A7:  A is retraction by Def2;
then A8:  A*A" = A * B by A1,A2,A4,A6,Def4
         .= idm o2 by A1,A3,A5,Def8;
       A"*A = B * A by A1,A2,A4,A6,A7,Def4
         .= idm o1 by A4,Def1;
    hence thesis by A8,Def5;
  end;

theorem
  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
  proof
  let C be category,
      o1,o2,o3 be object of C,
      A be Morphism of o1,o2,
      B be Morphism of o2,o3;
    assume A1: <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {};
    assume B * A is retraction;
    then consider G be 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:25;
    then A * G is_right_inverse_of B by Def1;
    then consider F be Morphism of o3,o2 such that A3: F = (A * G) &
       F is_right_inverse_of B;
    thus thesis by A3,Def2;
  end;

theorem
  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
  proof
   let C be category,
       o1,o2,o3 be object of C,
       A be Morphism of o1,o2,
       B be Morphism of o2,o3;
    assume A1: <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {};
    assume B * A is coretraction;
    then consider G be 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:25;
      G * (B * A) = idm o1 by A2,Def1;
    then G * B is_left_inverse_of A by A3,Def1;
    then consider F be Morphism of o2,o1 such that A4: F = (G * B) &
       F is_left_inverse_of A;
    thus thesis by A4,Def3;
  end;

theorem
  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
 proof
  let C be category;
   assume A1: for o1,o2 being object of C, A1 being Morphism of o1,o2 holds
            A1 is retraction;
   thus for a,b being object of C, A being Morphism of a,b
   st <^a,b^> <> {} & <^b,a^> <> {} holds A is iso
      proof
        let a,b be object of C;
        let A be Morphism of a,b;
        assume A2: <^a,b^> <> {} & <^b,a^> <> {};
           A3:    A is retraction by A1;
                 A is coretraction
                 proof
                   consider A1 be Morphism of b,a such that
                   A4: A1 is_right_inverse_of A by A3,Def2;
                        A1 is retraction by A1;
                   then A5:    A1 is epi by A2,Th15;
                   A6: <^a,a^> <> {} by ALTCAT_1:23;
                     A1 * (A * A1) =A1 * idm b by A4,Def1;
                   then A1 * (A * A1) =A1 by A2,ALTCAT_1:def 19;
                   then (A1 * A) * A1 =A1 by A2,ALTCAT_1:25;
                   then (A1 * A) * A1 =idm a * A1 by A2,ALTCAT_1:24;
                   then (A1 * A) =idm a by A5,A6,Def8;
                   then A1 is_left_inverse_of A by Def1;
                   hence thesis by Def3;
                 end;
        hence A is iso by A2,A3,Th6;
      end;
end;

definition
let C be with_units (non empty AltCatStr),
    o be object of C;
cluster mono epi retraction coretraction Morphism of o,o;
existence
 proof
 take idm o;
 thus thesis by Lm1,Th1;
 end;
end;

definition
let C be category,
    o be object of C;
cluster mono epi iso retraction coretraction Morphism of o,o;
existence
 proof
A1: <^o,o^> <> {} by ALTCAT_1:23;
 take I = idm o;
A2: I is retraction coretraction by Th1;
 then I is epi mono by A1,Th15,Th16;
 hence thesis by A1,A2,Th20;
 end;
end;

definition
let C be category,
    o be object of C,
    A, B be mono Morphism of o,o;
cluster A * B -> mono;
coherence
 proof
   <^o,o^> <> {} by ALTCAT_1:23;
 hence thesis by Th9;
 end;
end;

definition
let C be category,
    o be object of C,
    A, B be epi Morphism of o,o;
cluster A * B -> epi;
coherence
 proof
   <^o,o^> <> {} by ALTCAT_1:23;
 hence thesis by Th10;
 end;
end;

definition
let C be category,
    o be object of C,
    A, B be iso Morphism of o,o;
cluster A * B -> iso;
coherence
 proof
   <^o,o^> <> {} by ALTCAT_1:23;
 hence thesis by Th7;
 end;
end;

definition
let C be category,
    o be object of C,
    A, B be retraction Morphism of o,o;
cluster A * B -> retraction;
coherence
 proof
   <^o,o^> <> {} by ALTCAT_1:23;
 hence thesis by Th18;
 end;
end;

definition
let C be category,
    o be object of C,
    A, B be coretraction Morphism of o,o;
cluster A * B -> coretraction;
coherence
 proof
   <^o,o^> <> {} by ALTCAT_1:23;
 hence thesis by Th19;
 end;
end;

definition
let C be AltGraph,
    o be object of C;
attr o is initial means :Def9:
 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
  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)
 proof
  let C be AltGraph, o be object of C;
  thus o is initial implies
   (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))
  proof
   assume A1: o is initial;
   let o1 be object of C;
   consider M being Morphism of o,o1 such that
A2:  M in <^o,o1^> & <^o,o1^> is trivial by A1,Def9;
   consider i be set such that
A3: <^o,o1^> = { i } by A2,REALSET1:def 12;
   <^o,o1^> = {M} by A3,TARSKI:def 1;
   then for M1 being Morphism of o,o1 st M1 in <^o,o1^>
    holds M = M1 by TARSKI:def 1;
   hence thesis by A2;
  end;
  assume A4: (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));
   let o1 be object of C;
   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; assume A8: x in <^o,o1^>;
     then reconsider M1 = x as Morphism of o,o1;
       M1 = M by A6,A8;
     hence x in {M} by TARSKI:def 1;
    end;
    {M} c= <^o,o1^>
   proof
    let x be set; assume x in {M};
    hence x in <^o,o1^> by A5,TARSKI:def 1;
   end;
  then <^o,o1^> = {M} by A7,XBOOLE_0:def 10;
  hence thesis;
 end;

theorem Th26:
for C being category, o1,o2 being object of C st
o1 is initial & o2 is initial holds o1,o2 are_iso
 proof
  let C be category, o1,o2 be object of C
    such that
A1: o1 is initial and
A2: o2 is initial;
  consider M1 being Morphism of o1,o2 such that
A3: M1 in <^o1,o2^> & <^o1,o2^> is trivial by A1,Def9;
  consider M2 being Morphism of o2,o1 such that
A4: M2 in <^o2,o1^> & <^o2,o1^> is trivial by A2,Def9;
  thus <^o1,o2^> <> {} & <^o2,o1^> <> {} by A3,A4;
A5: (ex M being Morphism of o1,o1 st M in <^o1,o1^> & <^o1,o1^> is trivial) &
  (ex N being Morphism of o2,o2 st N in <^o2,o2^> & <^o2,o2^> is trivial)
  by A1,A2,Def9;
  then consider x being set such that A6: <^o1,o1^> = {x}
   by REALSET1:def 12;
  consider y being set such that A7: <^o2,o2^> = {y}
   by A5,REALSET1:def 12;
A8: M1 * M2 = y & M2 * M1 = x by A6,A7,TARSKI:def 1;
    idm o1 = x & idm o2 = y by A6,A7,TARSKI:def 1;
  then M2 is_left_inverse_of M1 & M2 is_right_inverse_of M1 by A8,Def1;
  then M1 is retraction & M1 is coretraction by Def2,Def3;
  then M1 is iso by A3,A4,Th6;
  hence thesis;
 end;

definition
let C be AltGraph,
    o be object of C;
attr o is terminal means :Def10:
 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
  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)
 proof
  let C be AltGraph, o be object of C;
  thus o is terminal implies
   (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))
  proof
   assume A1: o is terminal;
   let o1 be object of C;
   consider M being Morphism of o1,o such that
A2:  M in <^o1,o^> & <^o1,o^> is trivial by A1,Def10;
   consider i be set such that
A3: <^o1,o^> = { i } by A2,REALSET1:def 12;
   <^o1,o^> = {M} by A3,TARSKI:def 1;
   then for M1 being Morphism of o1,o st M1 in <^o1,o^>
    holds M = M1 by TARSKI:def 1;
   hence thesis by A2;
  end;
  assume A4: 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);
   let o1 be object of C;
   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; assume A8: x in <^o1,o^>;
     then reconsider M1 = x as Morphism of o1,o;
       M1 = M by A6,A8;
     hence x in {M} by TARSKI:def 1;
    end;
    {M} c= <^o1,o^>
   proof
    let x be set; assume x in {M};
    hence x in <^o1,o^> by A5,TARSKI:def 1;
   end;
  then <^o1,o^> = {M} by A7,XBOOLE_0:def 10;
  hence thesis;
 end;

theorem
  for C being category, o1,o2 being object of C st
o1 is terminal & o2 is terminal holds o1,o2 are_iso
 proof
  let C be category, o1,o2 be object of C; assume that
A1: o1 is terminal and
A2: o2 is terminal;
  consider M1 being Morphism of o1,o2 such that
A3: M1 in <^o1,o2^> & <^o1,o2^> is trivial by A2,Def10;
  consider M2 being Morphism of o2,o1 such that
A4: M2 in <^o2,o1^> & <^o2,o1^> is trivial by A1,Def10;
  thus <^o1,o2^> <> {} & <^o2,o1^> <> {} by A3,A4;
A5:(ex M being Morphism of o1,o1 st M in <^o1,o1^> & <^o1,o1^> is trivial) &
  (ex N being Morphism of o2,o2 st N in <^o2,o2^> & <^o2,o2^> is trivial)
  by A1,A2,Def10;
  then consider x being set such that A6: <^o1,o1^> = {x}
    by REALSET1:def 12;
  consider y being set such that A7: <^o2,o2^> = {y}
    by A5,REALSET1:def 12;
    M1 * M2 = y & M2 * M1 = x by A6,A7,TARSKI:def 1;
  then M1 * M2 = idm o2 & M2 * M1 = idm o1 by A6,A7,TARSKI:def 1;
  then M2 is_left_inverse_of M1 & M2 is_right_inverse_of M1 by Def1;
  then M1 is retraction & M1 is coretraction by Def2,Def3;
  then M1 is iso by A3,A4,Th6;
  hence thesis;
 end;

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

theorem
  for C being category, o1,o2 being object of C st
o1 is _zero & o2 is _zero holds o1,o2 are_iso
 proof
  let C be category, o1,o2 be object of C; assume
    o1 is _zero & o2 is _zero;
  then o1 is initial & o2 is initial by Def11;
  hence thesis by Th26;
 end;

definition
let C be non empty AltCatStr,
    o1, o2 be object of C,
    M be Morphism of o1,o2;
attr M is _zero means :Def12:
 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
  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
 proof
  let C be category,
      o1,o2,o3 be object of C,
      M1 be Morphism of o1,o2,
      M2 be Morphism of o2,o3; assume that
A1: M1 is _zero and
A2: M2 is _zero;
  let o be object of C; assume
A3: o is _zero;
then A4: o is initial & o is terminal by Def11;
  let A be Morphism of o1,o, B be Morphism of o,o3;
  consider B1 being Morphism of o,o2 such that
A5: B1 in <^o,o2^> & <^o,o2^> is trivial by A4,Def9;
  consider B2 being Morphism of o,o3 such that
A6: B2 in <^o,o3^> & <^o,o3^> is trivial by A4,Def9;
  consider A1 being Morphism of o1,o such that
A7: A1 in <^o1,o^> & <^o1,o^> is trivial by A4,Def10;
  consider A2 being Morphism of o2,o such that
A8: A2 in <^o2,o^> & <^o2,o^> is trivial by A4,Def10;
A9: M2 = B2 * A2 by A2,A3,Def12;
  consider x being set such that
A10: <^o1,o^> = {x} by A7,REALSET1:def 12;
A11:A = x & A1 = x by A10,TARSKI:def 1;
  consider y being set such that
A12: <^o,o3^> = {y} by A6,REALSET1:def 12;
A13: B = y & B2 = y by A12,TARSKI:def 1;
     (ex M being Morphism of o,o st M in <^o,o^> & <^o,o^> is trivial)
     by A4,Def10;
  then consider z being set such that
A14: <^o,o^> = {z} by REALSET1:def 12;
A15:idm o = z & A2 * B1 = z by A14,TARSKI:def 1;
A16: <^o,o2^> <> {} & <^o2,o^> <> {} & <^o1,o^> <> {} & <^o,o3^> <> {} &
       <^o,o^> <> {} & <^o2,o3^> <> {} by A5,A6,A7,A8,ALTCAT_1:def 4;
  thus M2 * M1 = (B2*A2) * (B1*A1) by A1,A3,A9,Def12
              .= B2*A2 * B1*A1 by A16,ALTCAT_1:25
              .= B*(idm o)*A by A5,A6,A8,A11,A13,A15,ALTCAT_1:25
              .= B*A by A6,ALTCAT_1:def 19;
 end;

Back to top