The abstract of the Mizar article:

Cartesian Categories

by

Czeslaw Bylinski

Received October 27, 1992

MML identifier: CAT_4

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, CAT_1, WELLORD1, BOOLE, FINSET_1, CAT_3, RELAT_1,
      FUNCOP_1, FINSEQ_4, CARD_1, ARYTM_1, FUNCT_4, FUNCT_6, PARTFUN1, FUNCT_3,
      ALGSTR_1, DIRAF, EQREL_1, CAT_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, DOMAIN_1, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCT_2, ALGSTR_1, REAL_1, NAT_1, CARD_1, FUNCT_4,
      CAT_1, CAT_3;
 constructors DOMAIN_1, ALGSTR_1, REAL_1, NAT_1, CAT_3, FINSEQ_4, PARTFUN1,
      XREAL_0, XBOOLE_0;
 clusters SUBSET_1, FINSET_1, RELSET_1, RELAT_1, FUNCT_1, NAT_1, ZFMISC_1,
      XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE;


begin

reserve o,m,r for set;

definition let o,m,r;
 func (o,m) :-> r -> Function of [:{o},{m}:],{r} means
:: CAT_4:def 1
     not contradiction;
end;

definition let C be Category, a,b be Object of C;
 redefine pred a,b are_isomorphic means
:: CAT_4:def 2
    Hom(a,b)<>{} & Hom(b,a)<>{} &
   ex f being Morphism of a,b, f' being Morphism of b,a
    st f*f' = id b & f'*f = id a;
end;

begin :: Cartesian Categories

definition let C be Category;
 attr C is with_finite_product means
:: CAT_4:def 3
    for I being finite set, F being Function of I,the Objects of C
   ex a being Object of C, F' being Projections_family of a,I
    st cods F' = F & a is_a_product_wrt F';
  synonym C has_finite_product;
end;

theorem :: CAT_4:1
   for C being Category holds
    C has_finite_product iff
     (ex a being Object of C st a is terminal) &
     for a,b being Object of C
      ex c being Object of C, p1,p2 being Morphism of C
       st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b &
        c is_a_product_wrt p1,p2;

definition
  struct (CatStr)ProdCatStr
   (# Objects,Morphisms -> non empty set,
     Dom,Cod -> Function of the Morphisms, the Objects,
     Comp -> PartFunc of [:the Morphisms, the Morphisms :],the Morphisms,
     Id -> Function of the Objects, the Morphisms,
     TerminalObj -> Element of the Objects,
     CatProd -> Function of [:the Objects,the Objects:],the Objects,
     Proj1,Proj2 -> Function of [:the Objects,the Objects:],the Morphisms
    #);
end;

definition let C be ProdCatStr;
 func [1]C -> Object of C equals
:: CAT_4:def 4
  the TerminalObj of C;
  let a,b be Object of C;
  func a[x]b -> Object of C equals
:: CAT_4:def 5
  (the CatProd of C).[a,b];
 func pr1(a,b) -> Morphism of C equals
:: CAT_4:def 6
  (the Proj1 of C).[a,b];
 func pr2(a,b) -> Morphism of C equals
:: CAT_4:def 7
  (the Proj2 of C).[a,b];
end;

definition let o,m;
 func c1Cat(o,m) -> strict ProdCatStr equals
:: CAT_4:def 8
  ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
                        Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #);
end;

theorem :: CAT_4:2
     the CatStr of c1Cat(o,m) = 1Cat(o,m);

definition
 cluster strict Category-like ProdCatStr;
end;

definition let o,m be set;
 cluster c1Cat(o,m) -> Category-like;
end;

theorem :: CAT_4:3
   for a being Object of c1Cat(o,m) holds a = o;

theorem :: CAT_4:4
   for a,b being Object of c1Cat(o,m) holds a = b;

theorem :: CAT_4:5
   for f being Morphism of c1Cat(o,m) holds f = m;

theorem :: CAT_4:6
   for f,g being Morphism of c1Cat(o,m) holds f = g;

theorem :: CAT_4:7
   for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m)
     holds f in Hom(a,b);

theorem :: CAT_4:8
     for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m)
    holds f is Morphism of a,b;

theorem :: CAT_4:9
    for a,b being Object of c1Cat(o,m) holds Hom(a,b) <> {};

theorem :: CAT_4:10
   for a being Object of c1Cat(o,m) holds a is terminal;

theorem :: CAT_4:11
   for c being Object of c1Cat(o,m), p1,p2 being Morphism of c1Cat(o,m)
    holds c is_a_product_wrt p1,p2;

definition let IT be Category-like ProdCatStr;
 attr IT is Cartesian means
:: CAT_4:def 9

  the TerminalObj of IT is terminal &
  for a,b being Object of IT holds
   cod((the Proj1 of IT).[a,b]) = a & cod((the Proj2 of IT).[a,b]) = b &
    (the CatProd of IT).[a,b]
     is_a_product_wrt (the Proj1 of IT).[a,b],(the Proj2 of IT).[a,b];
end;

theorem :: CAT_4:12
   for o,m being set holds c1Cat(o,m) is Cartesian;

definition
 cluster strict Cartesian (Category-like ProdCatStr);
end;

definition
  mode Cartesian_category is Cartesian (Category-like ProdCatStr);
end;

reserve C for Cartesian_category;
reserve a,b,c,d,e,s for Object of C;

theorem :: CAT_4:13
   [1]C is terminal;

theorem :: CAT_4:14
for f1,f2 being Morphism of a,[1]C holds f1 = f2;

theorem :: CAT_4:15
   Hom(a,[1]C) <> {};

definition let C,a;
 func term(a) -> Morphism of a,[1]C means
:: CAT_4:def 10
not contradiction;
end;

theorem :: CAT_4:16
   term a = term(a,[1]C);

theorem :: CAT_4:17
     dom(term a) = a & cod(term a) = [1]C;

theorem :: CAT_4:18
     Hom(a,[1]C) = {term a};

theorem :: CAT_4:19
   dom pr1(a,b) = a[x]b & cod pr1(a,b) = a;

theorem :: CAT_4:20
   dom pr2(a,b) = a[x]b & cod pr2(a,b) = b;

definition let C,a,b;
 redefine func pr1(a,b) -> Morphism of a[x]b,a;
 func pr2(a,b) -> Morphism of a[x]b,b;
end;

theorem :: CAT_4:21
   Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {};

theorem :: CAT_4:22
   a[x]b is_a_product_wrt pr1(a,b),pr2(a,b);

theorem :: CAT_4:23
     C has_finite_product;

theorem :: CAT_4:24
     Hom(a,b) <> {} & Hom(b,a) <> {}
    implies pr1(a,b) is retraction & pr2(a,b) is retraction;

definition let C,a,b,c;
  let f be Morphism of c,a, g be Morphism of c,b;
assume  Hom(c,a) <> {} & Hom(c,b) <> {};
 func <:f,g:> -> Morphism of c,a[x]b means
:: CAT_4:def 11
  pr1(a,b)*it = f & pr2(a,b)*it = g;
end;

theorem :: CAT_4:25
   Hom(c,a) <> {} & Hom(c,b) <> {} implies Hom(c,a[x]b) <> {};

theorem :: CAT_4:26
   <:pr1(a,b),pr2(a,b):> = id(a[x]b);

theorem :: CAT_4:27
  for f being Morphism of c,a, g being Morphism of c,b, h being Morphism of d,c
     st Hom(c,a)<>{} & Hom(c,b)<>{} & Hom(d,c)<>{}
    holds <:f*h,g*h:> = <:f,g:>*h;

theorem :: CAT_4:28
   for f,k being Morphism of c,a, g,h being Morphism of c,b
     st Hom(c,a) <> {} & Hom(c,b) <> {} & <:f,g:> = <:k,h:>
    holds f = k & g = h;

theorem :: CAT_4:29
     for f being Morphism of c,a, g being Morphism of c,b
    st Hom(c,a) <> {} & Hom(c,b) <> {} & (f is monic or g is monic)
   holds <:f,g:> is monic;

theorem :: CAT_4:30
   Hom(a,a[x][1]C) <> {} & Hom(a,[1]C[x]a) <> {};

definition let C,a;
 func lambda(a) -> Morphism of [1]C[x]a,a equals
:: CAT_4:def 12
  pr2([1]C,a);
 func lambda'(a) -> Morphism of a,[1]C[x]a equals
:: CAT_4:def 13
  <:term a,id a:>;
 func rho(a) -> Morphism of a[x][1]C,a equals
:: CAT_4:def 14
  pr1(a,[1]C);
 func rho'(a) -> Morphism of a,a[x][1]C equals
:: CAT_4:def 15
  <:id a,term a:>;
end;

theorem :: CAT_4:31
   lambda(a)*lambda'(a) = id a & lambda'(a)*lambda(a) = id([1]C[x]a) &
   rho(a)*rho'(a) = id a & rho'(a)*rho(a) = id(a[x][1]C);

theorem :: CAT_4:32
     a, a[x][1]C are_isomorphic & a,[1]C[x]a are_isomorphic;

definition let C,a,b;
 func Switch(a,b) -> Morphism of a[x]b,b[x]a equals
:: CAT_4:def 16
  <:pr2(a,b),pr1(a,b):>;
end;

theorem :: CAT_4:33
  Hom(a[x]b,b[x]a)<>{};


theorem :: CAT_4:34
   Switch(a,b)*Switch(b,a) = id(b[x]a);

theorem :: CAT_4:35
     a[x]b,b[x]a are_isomorphic;

definition let C,a;
 func Delta a -> Morphism of a,a[x]a equals
:: CAT_4:def 17
  <:id a,id a:>;
end;

theorem :: CAT_4:36
     Hom(a,a[x]a) <> {};

theorem :: CAT_4:37
     for f being Morphism of a,b st Hom(a,b) <> {}
    holds <:f,f:> = Delta(b)*f;

definition let C,a,b,c;
 func Alpha(a,b,c) -> Morphism of (a[x]b)[x]c,a[x](b[x]c) equals
:: CAT_4:def 18
  <:pr1(a,b)*pr1(a[x]b,c),<:pr2(a,b)*pr1(a[x]b,c),pr2(a[x]b,c):>:>;
 func Alpha'(a,b,c) -> Morphism of a[x](b[x]c),(a[x]b)[x]c equals
:: CAT_4:def 19
  <:<:pr1(a,b[x]c),pr1(b,c)*pr2(a,b[x]c):>,pr2(b,c)*pr2(a,b[x]c):>;
end;

theorem :: CAT_4:38
   Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} & Hom(a[x](b[x]c),(a[x]b)[x]c) <> {};

theorem :: CAT_4:39
   Alpha(a,b,c)*Alpha'(a,b,c) = id(a[x](b[x]c)) &
   Alpha'(a,b,c)*Alpha(a,b,c) = id((a[x]b)[x]c);

theorem :: CAT_4:40
     (a[x]b)[x]c,a[x](b[x]c) are_isomorphic;

definition let C,a,b,c,d;
  let f be Morphism of a,b, g be Morphism of c,d;
 func f[x]g -> Morphism of a[x]c,b[x]d equals
:: CAT_4:def 20
  <:f*pr1(a,c),g*pr2(a,c):>;
end;

theorem :: CAT_4:41
     Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a[x]b,c[x]d) <> {};

theorem :: CAT_4:42
     (id a)[x](id b) = id(a[x]b);

theorem :: CAT_4:43
   for f being Morphism of a,b, h being Morphism of c,d,
       g being Morphism of e,a, k being Morphism of e,c
     st Hom(a,b) <> {} & Hom(c,d) <> {} & Hom(e,a) <> {} & Hom(e,c) <> {}
    holds (f[x]h)*<:g,k:> = <:f*g,h*k:>;

theorem :: CAT_4:44
     for f being Morphism of c,a, g being Morphism of c,b
    st Hom(c,a) <> {} & Hom(c,b) <> {} holds <:f,g:> = (f[x]g)*Delta(c);

theorem :: CAT_4:45
     for f being Morphism of a,b, h being Morphism of c,d,
       g being Morphism of e,a, k being Morphism of s,c
      st Hom(a,b) <> {} & Hom(c,d) <> {} & Hom(e,a) <> {} & Hom(s,c) <> {}
     holds (f[x]h)*(g[x]k) = (f*g)[x](h*k);

begin :: Categories with Finite Coproducts

definition let C be Category;
 attr C is with_finite_coproduct means
:: CAT_4:def 21
     for I being finite set, F being Function of I,the Objects of C
   ex a being Object of C, F' being Injections_family of a,I
    st doms F' = F & a is_a_coproduct_wrt F';
  synonym C has_finite_coproduct;
end;

theorem :: CAT_4:46
   for C being Category holds
    C has_finite_coproduct iff
     (ex a being Object of C st a is initial) &
     for a,b being Object of C
      ex c being Object of C, i1,i2 being Morphism of C
       st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c &
        c is_a_coproduct_wrt i1,i2;

definition
  struct (CatStr)CoprodCatStr
   (# Objects,Morphisms -> non empty set,
     Dom,Cod -> Function of the Morphisms, the Objects,
     Comp -> PartFunc of [:the Morphisms, the Morphisms :],the Morphisms,
     Id -> Function of the Objects, the Morphisms,
     Initial -> Element of the Objects,
     Coproduct -> Function of [:the Objects,the Objects:],the Objects,
     Incl1,Incl2 -> Function of [:the Objects,the Objects:],the Morphisms
   #);
end;

definition let C be CoprodCatStr;
 func [0]C -> Object of C equals
:: CAT_4:def 22
  the Initial of C;
  let a,b be Object of C;
 func a+b -> Object of C equals
:: CAT_4:def 23
  (the Coproduct of C).[a,b];
 func in1(a,b) -> Morphism of C equals
:: CAT_4:def 24
  (the Incl1 of C).[a,b];
 func in2(a,b) -> Morphism of C equals
:: CAT_4:def 25
  (the Incl2 of C).[a,b];
end;

definition let o,m;
 func c1Cat*(o,m) -> strict CoprodCatStr equals
:: CAT_4:def 26
  CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
                 Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #);
end;

theorem :: CAT_4:47
     the CatStr of c1Cat*(o,m) = 1Cat(o,m);

definition
 cluster strict Category-like CoprodCatStr;
end;

definition let o,m be set;
 cluster c1Cat*(o,m) -> Category-like;
end;

theorem :: CAT_4:48
   for a being Object of c1Cat*(o,m) holds a = o;

theorem :: CAT_4:49
   for a,b being Object of c1Cat*(o,m) holds a = b;

theorem :: CAT_4:50
   for f being Morphism of c1Cat*(o,m) holds f = m;

theorem :: CAT_4:51
   for f,g being Morphism of c1Cat*(o,m) holds f = g;

theorem :: CAT_4:52
   for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(o,m)
     holds f in Hom(a,b);

theorem :: CAT_4:53
     for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(o,m)
    holds f is Morphism of a,b;

theorem :: CAT_4:54
    for a,b being Object of c1Cat*(o,m) holds Hom(a,b) <> {};

theorem :: CAT_4:55
   for a being Object of c1Cat*(o,m) holds a is initial;

theorem :: CAT_4:56
   for c being Object of c1Cat*(o,m),
    i1,i2 being Morphism of c1Cat*(o,m) holds c is_a_coproduct_wrt i1,i2;

definition let IT be Category-like CoprodCatStr;
 attr IT is Cocartesian means
:: CAT_4:def 27

  the Initial of IT is initial &
  for a,b being Object of IT holds
     dom((the Incl1 of IT).[a,b]) = a & dom((the Incl2 of IT).[a,b]) = b &
     (the Coproduct of IT).[a,b]
       is_a_coproduct_wrt (the Incl1 of IT).[a,b],(the Incl2 of IT).[a,b];
end;

theorem :: CAT_4:57
   for o,m being set holds c1Cat*(o,m) is Cocartesian;

definition
 cluster strict Cocartesian (Category-like CoprodCatStr);
end;

definition
  mode Cocartesian_category is Cocartesian (Category-like CoprodCatStr);
end;

reserve C for Cocartesian_category;
reserve a,b,c,d,e,s for Object of C;

theorem :: CAT_4:58
   [0]C is initial;

theorem :: CAT_4:59
   for f1,f2 being Morphism of [0]C,a holds f1 = f2;

definition let C,a;
 func init a -> Morphism of [0]C, a means
:: CAT_4:def 28
not contradiction;
end;

theorem :: CAT_4:60
   Hom([0]C,a) <> {};

theorem :: CAT_4:61
   init a = init([0]C,a);

theorem :: CAT_4:62
     dom(init a) = [0]C & cod(init a) = a;

theorem :: CAT_4:63
     Hom([0]C,a) = {init a};

theorem :: CAT_4:64
   dom in1(a,b) = a & cod in1(a,b) = a+b;

theorem :: CAT_4:65
   dom in2(a,b) = b & cod in2(a,b) = a+b;

theorem :: CAT_4:66
   Hom(a,a+b) <> {} & Hom(b,a+b) <> {};

theorem :: CAT_4:67
   a+b is_a_coproduct_wrt in1(a,b),in2(a,b);

theorem :: CAT_4:68
     C has_finite_coproduct;

theorem :: CAT_4:69
     Hom(a,b) <> {} & Hom(b,a) <> {}
    implies in1(a,b) is coretraction & in2(a,b) is coretraction;

definition let C,a,b; redefine
 func in1(a,b) -> Morphism of a,a+b;
 func in2(a,b) -> Morphism of b,a+b;
end;

definition let C,a,b,c;
  let f be Morphism of a,c, g be Morphism of b,c;
assume  Hom(a,c) <> {} & Hom(b,c) <> {};
 func [$f,g$] -> Morphism of a+b,c means
:: CAT_4:def 29
  it*in1(a,b) = f & it*in2(a,b) = g;
end;

theorem :: CAT_4:70
   Hom(a,c) <> {} & Hom(b,c) <> {} implies Hom(a+b,c) <> {};

theorem :: CAT_4:71
   [$in1(a,b),in2(a,b)$] = id(a+b);

theorem :: CAT_4:72
  for f being Morphism of a,c, g being Morphism of b,c, h being Morphism of c,d
     st Hom(a,c)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{}
    holds [$h*f,h*g$] = h*[$f,g$];

theorem :: CAT_4:73
   for f,k being Morphism of a,c, g,h being Morphism of b,c
     st Hom(a,c) <> {} & Hom(b,c) <> {} & [$f,g$] = [$k,h$]
    holds f = k & g = h;

theorem :: CAT_4:74
     for f being Morphism of a,c, g being Morphism of b,c
    st Hom(a,c) <> {} & Hom(b,c) <> {} & (f is epi or g is epi)
   holds [$f,g$] is epi;

theorem :: CAT_4:75
     a, a+[0]C are_isomorphic & a,[0]C+a are_isomorphic;

theorem :: CAT_4:76
     a+b,b+a are_isomorphic;

theorem :: CAT_4:77
     (a+b)+c,a+(b+c) are_isomorphic;

definition let C,a;
 func nabla a -> Morphism of a+a,a equals
:: CAT_4:def 30
  [$id a,id a$];
end;

definition let C,a,b,c,d;
  let f be Morphism of a,c, g be Morphism of b,d;
 func f+g -> Morphism of a+b,c+d equals
:: CAT_4:def 31
  [$in1(c,d)*f,in2(c,d)*g$];
end;

theorem :: CAT_4:78
     Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a+b,c+d) <> {};

theorem :: CAT_4:79
     (id a)+(id b) = id(a+b);

theorem :: CAT_4:80
   for f being Morphism of a,c, h being Morphism of b,d,
       g being Morphism of c,e, k being Morphism of d,e
     st Hom(a,c) <> {} & Hom(b,d) <> {} & Hom(c,e) <> {} & Hom(d,e) <> {}
    holds [$g,k$]*(f+h) = [$g*f,k*h$];

theorem :: CAT_4:81
     for f being Morphism of a,c, g being Morphism of b,c
    st Hom(a,c) <> {} & Hom(b,c) <> {} holds nabla(c)*(f+g) = [$f,g$];

theorem :: CAT_4:82
     for f being Morphism of a,c, h being Morphism of b,d,
       g being Morphism of c,e, k being Morphism of d,s
      st Hom(a,c) <> {} & Hom(b,d) <> {} & Hom(c,e) <> {} & Hom(d,s) <> {}
     holds (g+k)*(f+h) = (g*f)+(k*h);