The abstract of the Mizar article:

Products and Coproducts in Categories

by

Czeslaw Bylinski

Received May 11, 1992

MML identifier: CAT_3

[ Mizar article, MML identifier index ]

environ

 vocabulary CAT_1, FUNCT_1, FINSEQ_4, RELAT_1, FUNCOP_1, FUNCT_4, BOOLE,
      FUNCT_6, OPPCAT_1, WELLORD1, CAT_3;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FUNCT_4,
      FUNCT_2, FINSEQ_4, CAT_1, OPPCAT_1;
 constructors OPPCAT_1, FINSEQ_4, MEMBERED, XBOOLE_0;
 clusters RELSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Indexed families

reserve I for set, x,x1,x2,y,z for set, A for non empty set;
reserve C,D for Category;
reserve a,b,c,d for Object of C;
reserve f,g,h,i,j,k,p1,p2,q1,q2,i1,i2,j1,j2 for Morphism of C;

definition let I,A; let F be Function of I,A; let x be set;
 assume
  x in I;
 redefine func F/.x equals
:: CAT_3:def 1
   F.x;
end;

scheme LambdaIdx{I()->set,A()->non empty set,F(set)->Element of A()}:
  ex F being Function of I(),A() st for x st x in I() holds F/.x = F(x);

theorem :: CAT_3:1
   for F1,F2 being Function of I,A st for x st x in I holds F1/.x = F2/.x
    holds F1 = F2;

scheme FuncIdx_correctness{I()->set,A()->non empty set,F(set)->Element of A()}:
  (ex F being Function of I(),A() st for x st x in I() holds F/.x = F(x)) &
  (for F1,F2 being Function of I(),A() st
    (for x st x in I() holds F1/.x = F(x)) &
    (for x st x in I() holds F2/.x = F(x))
   holds F1 = F2);

definition let A,I; let a be Element of A;
 redefine func I --> a -> Function of I,A;
end;

theorem :: CAT_3:2
   for a being Element of A st x in I holds (I --> a)/.x = a;

canceled 4;

theorem :: CAT_3:7
   x1 <> x2 implies for y1,y2 being Element of A
    holds ((x1,x2) --> (y1,y2))/.x1 = y1 & ((x1,x2) --> (y1,y2))/.x2 = y2;

begin :: Indexed families of morphisms

definition let C,I; let F be Function of I,the Morphisms of C;
 canceled;

 func doms F -> Function of I, the Objects of C means
:: CAT_3:def 3
  for x st x in I holds it/.x = dom(F/.x);
 func cods F -> Function of I, the Objects of C means
:: CAT_3:def 4
  for x st x in I holds it/.x = cod(F/.x);
end;

theorem :: CAT_3:8
   doms(I-->f) = I-->(dom f);

theorem :: CAT_3:9
   cods(I-->f) = I-->(cod f);

theorem :: CAT_3:10
   doms((x1,x2)-->(p1,p2)) = (x1,x2)-->(dom p1,dom p2);

theorem :: CAT_3:11
   cods((x1,x2)-->(p1,p2)) = (x1,x2)-->(cod p1,cod p2);

definition let C,I; let F be Function of I,the Morphisms of C;
 func F opp -> Function of I,the Morphisms of C opp means
:: CAT_3:def 5
  for x st x in I holds it/.x = (F/.x) opp;
end;

theorem :: CAT_3:12
     (I --> f) opp = I --> f opp;

theorem :: CAT_3:13
     x1 <> x2 implies ((x1,x2)-->(p1,p2)) opp = (x1,x2)-->(p1 opp,p2 opp);

theorem :: CAT_3:14
     for F being Function of I,the Morphisms of C holds F opp opp = F;

definition let C,I; let F be Function of I,the Morphisms of C opp;
 func opp F -> Function of I,the Morphisms of C means
:: CAT_3:def 6
  for x st x in I holds it/.x = opp (F/.x);
end;

theorem :: CAT_3:15
     for f being Morphism of C opp holds opp(I --> f) = I --> (opp f);

theorem :: CAT_3:16
     x1 <> x2 implies for p1,p2 being Morphism of C opp holds
    opp ((x1,x2)-->(p1,p2)) = (x1,x2)-->(opp p1,opp p2);

theorem :: CAT_3:17
     for F being Function of I,the Morphisms of C holds opp(F opp) = F;


definition let C,I; let F be Function of I,the Morphisms of C, f;
 func F*f -> Function of I,the Morphisms of C means
:: CAT_3:def 7
 for x st x in I holds it/.x = (F/.x)*f;
 func f*F -> Function of I,the Morphisms of C means
:: CAT_3:def 8
 for x st x in I holds it/.x = f*(F/.x);
end;

theorem :: CAT_3:18
   x1 <> x2 implies ((x1,x2)-->(p1,p2))*f = (x1,x2)-->(p1*f,p2*f);

theorem :: CAT_3:19
   x1 <> x2 implies f*((x1,x2)-->(p1,p2)) = (x1,x2)-->(f*p1,f*p2);

theorem :: CAT_3:20
  for F being Function of I,the Morphisms of C st doms F = I-->cod f
   holds doms(F*f) = I-->dom f & cods(F*f) = cods F;

theorem :: CAT_3:21
  for F being Function of I,the Morphisms of C st cods F = I-->dom f
   holds doms(f*F) = doms F & cods(f*F) = I-->cod f;

definition let C,I; let F,G be Function of I,the Morphisms of C;
 func F"*"G -> Function of I,the Morphisms of C means
:: CAT_3:def 9
  for x st x in I holds it/.x = (F/.x)*(G/.x);
end;

theorem :: CAT_3:22
 for F,G being Function of I,the Morphisms of C st doms F = cods G
  holds doms(F"*"G) = doms G & cods(F"*"G) = cods F;

theorem :: CAT_3:23
     x1 <> x2 implies
    ((x1,x2)-->(p1,p2))"*"((x1,x2)-->(q1,q2)) = (x1,x2)-->(p1*q1,p2*q2);

theorem :: CAT_3:24
    for F being Function of I,the Morphisms of C holds F*f = F"*"(I-->f);

theorem :: CAT_3:25
    for F being Function of I,the Morphisms of C holds f*F = (I-->f)"*"F;


begin :: Retractions and Coretractions

definition let C;
  let IT be Morphism of C;
  attr IT is retraction means
:: CAT_3:def 10
 ex g st cod g = dom IT & IT*g = id(cod IT);
  attr IT is coretraction means
:: CAT_3:def 11
 ex g st dom g = cod IT & g*IT = id(dom IT);
end;

theorem :: CAT_3:26
   f is retraction implies f is epi;

theorem :: CAT_3:27
     f is coretraction implies f is monic;

theorem :: CAT_3:28
     f is retraction & g is retraction & dom g = cod f
    implies g*f is retraction;

theorem :: CAT_3:29
     f is coretraction & g is coretraction & dom g = cod f
    implies g*f is coretraction;

theorem :: CAT_3:30
     dom g = cod f & g*f is retraction implies g is retraction;

theorem :: CAT_3:31
     dom g = cod f & g*f is coretraction implies f is coretraction;

theorem :: CAT_3:32
     f is retraction & f is monic implies f is invertible;

theorem :: CAT_3:33
   f is coretraction & f is epi implies f is invertible;

theorem :: CAT_3:34
     f is invertible iff f is retraction & f is coretraction;

theorem :: CAT_3:35
     for T being Functor of C,D st f is retraction holds T.f is retraction;

theorem :: CAT_3:36
     for T being Functor of C,D st f is coretraction holds T.f is coretraction;

theorem :: CAT_3:37
     f is retraction iff f opp is coretraction;

theorem :: CAT_3:38
     f is coretraction iff f opp is retraction;

begin :: Morphisms determined by a terminal Object

definition let C,a,b;
 assume
  b is terminal;
 func term(a,b) -> Morphism of a,b means
:: CAT_3:def 12
not contradiction;
end;

theorem :: CAT_3:39
   b is terminal implies dom(term(a,b)) = a & cod(term(a,b)) = b;

theorem :: CAT_3:40
   b is terminal & dom f = a & cod f = b implies term(a,b) = f;

theorem :: CAT_3:41
     for f being Morphism of a,b st b is terminal holds term(a,b) = f;

begin :: Morphisms determined by an iniatial object

definition let C,a,b;
 assume
  a is initial;
 func init(a,b) -> Morphism of a,b means
:: CAT_3:def 13
not contradiction;
end;

theorem :: CAT_3:42
   a is initial implies dom(init(a,b)) = a & cod(init(a,b)) = b;

theorem :: CAT_3:43
   a is initial & dom f = a & cod f = b implies init(a,b) = f;

theorem :: CAT_3:44
     for f being Morphism of a,b st a is initial holds init(a,b) = f;

begin :: Products

definition let C,a,I;
  mode Projections_family of a,I -> Function of I,the Morphisms of C means
:: CAT_3:def 14
  doms it = I --> a;
end;

theorem :: CAT_3:45
  for F being Projections_family of a,I st x in I holds dom(F/.x) = a;

theorem :: CAT_3:46
   for F being Function of {},the Morphisms of C
    holds F is Projections_family of a,{};

theorem :: CAT_3:47
  dom f = a implies {y} --> f is Projections_family of a,{y};

theorem :: CAT_3:48
   dom p1 = a & dom p2 = a
    implies (x1,x2)-->(p1,p2) is Projections_family of a,{x1,x2};

canceled;

theorem :: CAT_3:50
   for F being Projections_family of a,I st cod f = a
    holds F*f is Projections_family of dom f,I;

theorem :: CAT_3:51
     for F being Function of I,the Morphisms of C,
       G being Projections_family of a,I st doms F = cods G
    holds F"*"G is Projections_family of a,I;

theorem :: CAT_3:52
     for F being Projections_family of cod f,I holds (f opp)*(F opp) = (F*f)
opp;

definition let C,a,I; let F be Function of I,the Morphisms of C;
  pred a is_a_product_wrt F means
:: CAT_3:def 15
  F is Projections_family of a,I &
  for b for F' being Projections_family of b,I st cods F = cods F'
   ex h st h in Hom(b,a) &
    for k st k in Hom(b,a) holds
      (for x st x in I holds (F/.x)*k = F'/.x) iff h = k;
end;

theorem :: CAT_3:53
   for F being Projections_family of c,I, F' being Projections_family of d,I
    st c is_a_product_wrt F & d is_a_product_wrt F' & cods F = cods F'
     holds c,d are_isomorphic;

theorem :: CAT_3:54
   for F being Projections_family of c,I
     st c is_a_product_wrt F &
      for x1,x2 st x1 in I & x2 in I holds Hom(cod(F/.x1),cod(F/.x2)) <> {}
    for x st x in I holds F/.x is retraction;

theorem :: CAT_3:55
  for F being Function of {},the Morphisms of C holds
   a is_a_product_wrt F iff a is terminal;

theorem :: CAT_3:56
   for F being Projections_family of a,I
    st a is_a_product_wrt F & dom f = b & cod f = a & f is invertible
     holds b is_a_product_wrt F*f;

theorem :: CAT_3:57
     a is_a_product_wrt {y} --> id a;

theorem :: CAT_3:58
     for F being Projections_family of a,I
    st a is_a_product_wrt F &
      for x st x in I holds cod(F/.x) is terminal
     holds a is terminal;

definition let C,c,p1,p2;
   pred c is_a_product_wrt p1,p2 means
:: CAT_3:def 16
 dom p1 = c & dom p2 = c &
  for d,f,g st f in Hom(d,cod p1) & g in Hom(d,cod p2)
   ex h st h in Hom(d,c) &
    for k st k in Hom(d,c) holds p1*k = f & p2*k = g iff h = k;
end;

theorem :: CAT_3:59
  x1 <> x2 implies
   (c is_a_product_wrt p1,p2 iff c is_a_product_wrt (x1,x2)-->(p1,p2));

theorem :: CAT_3:60
    Hom(c,a) <> {} & Hom(c,b) <> {} implies
   for p1 being Morphism of c,a, p2 being Morphism of c,b
    holds c is_a_product_wrt p1,p2 iff
     for d st Hom(d,a)<>{} & Hom(d,b)<>{} holds
      Hom(d,c) <> {} &
      for f being Morphism of d,a, g being Morphism of d,b
       ex h being Morphism of d,c st
        for k being Morphism of d,c holds p1*k = f & p2*k = g iff h = k;

theorem :: CAT_3:61
     c is_a_product_wrt p1,p2 & d is_a_product_wrt q1,q2 &
    cod p1 = cod q1 & cod p2 = cod q2 implies c,d are_isomorphic;

theorem :: CAT_3:62
     c is_a_product_wrt p1,p2 & Hom(cod p1,cod p2) <> {} & Hom(cod p2,cod p1)
<>
{}
    implies p1 is retraction & p2 is retraction;

theorem :: CAT_3:63
   c is_a_product_wrt p1,p2 & h in Hom(c,c) & p1*h = p1 & p2*h = p2
    implies h = id c;

theorem :: CAT_3:64
     c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible
    implies d is_a_product_wrt p1*f,p2*f;

theorem :: CAT_3:65
     c is_a_product_wrt p1,p2 & cod p2 is terminal
    implies c,cod p1 are_isomorphic;

theorem :: CAT_3:66
     c is_a_product_wrt p1,p2 & cod p1 is terminal
    implies c,cod p2 are_isomorphic;

begin :: Coproducts

definition let C,c,I;
  mode Injections_family of c,I -> Function of I,the Morphisms of C means
:: CAT_3:def 17
  cods it = I --> c;
end;

theorem :: CAT_3:67
   for F being Injections_family of c,I st x in I holds cod(F/.x) = c;

theorem :: CAT_3:68
     for F being Function of {},the Morphisms of C
    holds F is Injections_family of a,{};

theorem :: CAT_3:69
   cod f = a implies {y} --> f is Injections_family of a,{y};

theorem :: CAT_3:70
   cod p1 = c & cod p2 = c
    implies (x1,x2)-->(p1,p2) is Injections_family of c,{x1,x2};

canceled;

theorem :: CAT_3:72
   for F being Injections_family of b,I st dom f = b
    holds f*F is Injections_family of cod f,I;

theorem :: CAT_3:73
     for F being Injections_family of b,I,
       G being Function of I,the Morphisms of C st doms F = cods G
    holds F"*"G is Injections_family of b,I;

theorem :: CAT_3:74
   for F be Function of I,the Morphisms of C holds
     F is Projections_family of c,I iff F opp is Injections_family of c opp,I;

theorem :: CAT_3:75
 for F be Function of I,the Morphisms of C opp, c being Object of C opp holds
   F is Injections_family of c,I iff opp F is Projections_family of opp c,I;

theorem :: CAT_3:76
     for F being Injections_family of dom f,I holds (F opp)*(f opp) = (f*F) opp
;

definition let C,c,I; let F be Function of I,the Morphisms of C;
  pred c is_a_coproduct_wrt F means
:: CAT_3:def 18
  F is Injections_family of c,I &
  for d for F' being Injections_family of d,I st doms F = doms F'
   ex h st h in Hom(c,d) &
    for k st k in Hom(c,d) holds
     (for x st x in I holds k*(F/.x) = F'/.x) iff h = k;
end;

theorem :: CAT_3:77
    for F being Function of I,the Morphisms of C holds
   c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp;

theorem :: CAT_3:78
   for F being Injections_family of c,I, F' being Injections_family of d,I
    st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F' & doms F = doms F'
     holds c,d are_isomorphic;

theorem :: CAT_3:79
   for F being Injections_family of c,I
     st c is_a_coproduct_wrt F &
      for x1,x2 st x1 in I & x2 in I holds Hom(dom(F/.x1),dom(F/.x2)) <> {}
    for x st x in I holds F/.x is coretraction;

theorem :: CAT_3:80
   for F being Injections_family of a,I
    st a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible
     holds b is_a_coproduct_wrt f*F;

theorem :: CAT_3:81
  for F being Injections_family of a,{} holds
   a is_a_coproduct_wrt F iff a is initial;

theorem :: CAT_3:82
     a is_a_coproduct_wrt {y} --> id a;

theorem :: CAT_3:83
     for F being Injections_family of a,I
    st a is_a_coproduct_wrt F &
      for x st x in I holds dom(F/.x) is initial
     holds a is initial;

definition let C,c,i1,i2;
   pred c is_a_coproduct_wrt i1,i2 means
:: CAT_3:def 19

 cod i1 = c & cod i2 = c &
 for d,f,g st f in Hom(dom i1,d) & g in Hom(dom i2,d)
  ex h st h in Hom(c,d) &
   for k st k in Hom(c,d) holds k*i1 = f & k*i2 = g iff h = k;
end;

theorem :: CAT_3:84
     c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp, p2 opp;

theorem :: CAT_3:85
  x1 <> x2 implies
   (c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2)-->(i1,i2));

theorem :: CAT_3:86
     c is_a_coproduct_wrt i1,i2 & d is_a_coproduct_wrt j1,j2 &
    dom i1 = dom j1 & dom i2 = dom j2 implies c,d are_isomorphic;

theorem :: CAT_3:87
     Hom(a,c) <> {} & Hom(b,c) <> {} implies
    for i1 being Morphism of a,c, i2 being Morphism of b,c
     holds c is_a_coproduct_wrt i1,i2 iff
      for d st Hom(a,d)<>{} & Hom(b,d)<>{} holds
       Hom(c,d) <> {} &
        for f being Morphism of a,d, g being Morphism of b,d
         ex h being Morphism of c,d st
          for k being Morphism of c,d holds k*i1 = f & k*i2 = g iff h = k;

theorem :: CAT_3:88
     c is_a_coproduct_wrt i1,i2 &
      Hom(dom i1,dom i2) <> {} & Hom(dom i2,dom i1) <> {}
    implies i1 is coretraction & i2 is coretraction;

theorem :: CAT_3:89
   c is_a_coproduct_wrt i1,i2 & h in Hom(c,c) & h*i1 = i1 & h*i2 = i2
    implies h = id c;

theorem :: CAT_3:90
     c is_a_coproduct_wrt i1,i2 & dom f = c & cod f = d & f is invertible
    implies d is_a_coproduct_wrt f*i1,f*i2;

theorem :: CAT_3:91
     c is_a_coproduct_wrt i1,i2 & dom i2 is initial
    implies dom i1,c are_isomorphic;

theorem :: CAT_3:92
     c is_a_coproduct_wrt i1,i2 & dom i1 is initial
    implies dom i2,c are_isomorphic;