The abstract of the Mizar article:

Isomorphisms of Categories

by

Andrzej Trybulec

Received November 22, 1991

MML identifier: ISOCAT_1

[ Mizar article, MML identifier index ]

environ

 vocabulary CAT_1, FUNCT_1, RELAT_1, FUNCT_3, NATTRA_1, BOOLE, WELLORD1,
      PARTFUN1, SEQ_1, ISOCAT_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3,
      CAT_1, CAT_2, NATTRA_1;
 constructors NATTRA_1, MEMBERED, PARTFUN1, XBOOLE_0;
 clusters RELSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

:: Auxiliary theorems

 reserve A,B,C,D for Category,
         F for Functor of A,B,
         G for Functor of B,C;

theorem :: ISOCAT_1:1
 for F,G being Function st F is one-to-one & G is one-to-one
  holds [:F,G:] is one-to-one;

theorem :: ISOCAT_1:2
 rng pr1(A,B) = the Morphisms of A & rng pr2(B,A) = the Morphisms of A;

theorem :: ISOCAT_1:3
 for f being Morphism of A st f is invertible holds F.f is invertible;

theorem :: ISOCAT_1:4
 for F being Functor of A,B, G being Functor of B,A holds
 F*id A = F & id A*G = G;

canceled 2;

theorem :: ISOCAT_1:7
 for F1,F2 being Functor of A,B st F1 is_transformable_to F2
  for t being transformation of F1,F2, a being Object of A
   holds t.a in Hom(F1.a,F2.a);

theorem :: ISOCAT_1:8
 for F1,F2 being Functor of A,B, G1,G2 being Functor of B,C st
   F1 is_transformable_to F2 &
   G1 is_transformable_to G2
  holds G1*F1 is_transformable_to G2*F2;

theorem :: ISOCAT_1:9
 for F1,F2 being Functor of A,B st F1 is_transformable_to F2
 for t being transformation of F1,F2 st t is invertible
 for a being Object of A holds F1.a, F2.a are_isomorphic;

definition let C,D;
 redefine mode Functor of C,D means
:: ISOCAT_1:def 1
      (for c being Object of C ex d being Object of D st it.id c = id d) &
    (for f being Morphism of C holds
         it.id dom f = id dom(it.f) & it.id cod f = id cod(it.f)) &
    for f,g being Morphism of C st dom g = cod f
      holds it.(g*f) = it.g*it.f;
end;

definition let A;
 redefine func id A -> Functor of A,A;
 let B,C;
 let F be Functor of A,B, G be Functor of B,C;
 func G*F -> Functor of A,C;
end;

 reserve o,m for set;

theorem :: ISOCAT_1:10
 F is_an_isomorphism implies
  for g being Morphism of B ex f being Morphism of A st F.f = g;

theorem :: ISOCAT_1:11
 F is_an_isomorphism implies
  for b being Object of B ex a being Object of A st F.a = b;

theorem :: ISOCAT_1:12
 F is one-to-one implies Obj F is one-to-one;

definition let A,B,F;
 assume
  F is_an_isomorphism;
  func F" -> Functor of B,A equals
:: ISOCAT_1:def 2
 F";
end;

definition let A,B,F;
 redefine attr F is isomorphic means
:: ISOCAT_1:def 3
 F is one-to-one & rng F = the Morphisms of B;
  synonym F is_an_isomorphism;
end;

theorem :: ISOCAT_1:13
 F is_an_isomorphism implies F" is_an_isomorphism;

theorem :: ISOCAT_1:14
   F is_an_isomorphism implies (Obj F)" = Obj F";

theorem :: ISOCAT_1:15
   F is_an_isomorphism implies F"" = F;

theorem :: ISOCAT_1:16
 F is_an_isomorphism implies F*F" = id B & F"*F = id A;

theorem :: ISOCAT_1:17
 F is_an_isomorphism & G is_an_isomorphism implies
  G*F is_an_isomorphism;



:: Isomorphism of categories

definition let A,B;
 pred A,B are_isomorphic means
:: ISOCAT_1:def 4
   ex F being Functor of A,B st F is_an_isomorphism;
 reflexivity;
 symmetry;
 synonym A ~= B;
end;

canceled 2;

theorem :: ISOCAT_1:20
   A ~= B & B ~= C implies A ~= C;

theorem :: ISOCAT_1:21
   [:1Cat(o,m),A:] ~= A;

theorem :: ISOCAT_1:22
   [:A,B:] ~= [:B,A:];

theorem :: ISOCAT_1:23
   [:[:A,B:],C:] ~= [:A,[:B,C:]:];

theorem :: ISOCAT_1:24
   A ~= B & C ~= D implies [:A,C:] ~= [:B,D:];

definition let A,B,C; let F1,F2 be Functor of A,B such that
 F1 is_transformable_to F2;
 let t be transformation of F1,F2;
 let G be Functor of B,C;
  func G*t -> transformation of G*F1,G*F2 equals
:: ISOCAT_1:def 5
  G*t;
end;

definition let A,B,C; let G1,G2 be Functor of B,C such that
 G1 is_transformable_to G2;
 let F be Functor of A,B;
 let t be transformation of G1,G2;
  func t*F -> transformation of G1*F,G2*F equals
:: ISOCAT_1:def 6
  t*Obj F;
end;

theorem :: ISOCAT_1:25
 for G1,G2 be Functor of B,C st G1 is_transformable_to G2
 for F be Functor of A,B, t be transformation of G1,G2, a be Object of A
  holds (t*F).a = t.(F.a);

theorem :: ISOCAT_1:26
 for F1,F2 be Functor of A,B st F1 is_transformable_to F2
 for t be transformation of F1,F2, G be Functor of B,C, a being Object of A
  holds (G*t).a = G.(t.a);

theorem :: ISOCAT_1:27
 for F1,F2 being Functor of A,B, G1,G2 being Functor of B,C st
   F1 is_naturally_transformable_to F2 &
   G1 is_naturally_transformable_to G2
  holds G1*F1 is_naturally_transformable_to G2*F2;

definition let A,B,C; let F1,F2 be Functor of A,B such that
 F1 is_naturally_transformable_to F2;
 let t be natural_transformation of F1,F2;
 let G be Functor of B,C;
  func G*t -> natural_transformation of G*F1,G*F2 equals
:: ISOCAT_1:def 7
  G*t;
end;

theorem :: ISOCAT_1:28
 for F1,F2 be Functor of A,B st F1 is_naturally_transformable_to F2
 for t be natural_transformation of F1,F2, G be Functor of B,C,
     a being Object of A
  holds (G*t).a = G.(t.a);

definition let A,B,C; let G1,G2 be Functor of B,C such that
 G1 is_naturally_transformable_to G2;
 let F be Functor of A,B;
 let t be natural_transformation of G1,G2;
  func t*F -> natural_transformation of G1*F,G2*F equals
:: ISOCAT_1:def 8
  t*F;
end;

theorem :: ISOCAT_1:29
 for G1,G2 be Functor of B,C st G1 is_naturally_transformable_to G2
 for F be Functor of A,B, t be natural_transformation of G1,G2,
     a be Object of A
  holds (t*F).a = t.(F.a);

reserve F,F1,F2,F3 for Functor of A,B,
        G,G1,G2,G3 for Functor of B,C,
        H,H1,H2 for Functor of C,D,
        s for natural_transformation of F1,F2,
        s' for natural_transformation of F2,F3,
        t for natural_transformation of G1,G2,
        t' for natural_transformation of G2,G3,
        u for natural_transformation of H1,H2;

theorem :: ISOCAT_1:30
 F1 is_naturally_transformable_to F2 implies
 for a being Object of A holds Hom(F1.a,F2.a) <> {};

theorem :: ISOCAT_1:31
 F1 is_naturally_transformable_to F2 implies
 for t1,t2 being natural_transformation of F1,F2 st
   for a being Object of A holds t1.a = t2.a
  holds t1 = t2;

theorem :: ISOCAT_1:32
 F1 is_naturally_transformable_to F2 &
 F2 is_naturally_transformable_to F3
  implies G*(s'`*`s) = (G*s')`*`(G*s);

theorem :: ISOCAT_1:33
  G1 is_naturally_transformable_to G2 &
  G2 is_naturally_transformable_to G3
   implies (t'`*`t)*F = (t'*F)`*`(t*F);

theorem :: ISOCAT_1:34
 H1 is_naturally_transformable_to H2 implies u*G*F = u*(G*F);

theorem :: ISOCAT_1:35
 G1 is_naturally_transformable_to G2 implies H*t*F = H*(t*F);

theorem :: ISOCAT_1:36
 F1 is_naturally_transformable_to F2 implies H*G*s = H*(G*s);

theorem :: ISOCAT_1:37
 (id G)*F = id(G*F);

theorem :: ISOCAT_1:38
 G*id F = id(G*F);

theorem :: ISOCAT_1:39
 G1 is_naturally_transformable_to G2 implies t*id B = t;

theorem :: ISOCAT_1:40
 F1 is_naturally_transformable_to F2 implies (id B)*s = s;

definition let A,B,C,F1,F2,G1,G2;
 let s,t;
 func t(#)s -> natural_transformation of G1*F1,G2*F2 equals
:: ISOCAT_1:def 9
  (t*F2)`*`(G1*s);
end;

theorem :: ISOCAT_1:41
 F1 is_naturally_transformable_to F2 &
 G1 is_naturally_transformable_to G2 implies
 t(#)s = (G2*s)`*`(t*F1);

theorem :: ISOCAT_1:42
   F1 is_naturally_transformable_to F2 implies (id id B)(#)s = s;

theorem :: ISOCAT_1:43
   G1 is_naturally_transformable_to G2 implies t(#)(id id B) = t;

theorem :: ISOCAT_1:44
   F1 is_naturally_transformable_to F2 &
 G1 is_naturally_transformable_to G2 &
 H1 is_naturally_transformable_to H2 implies
  u(#)(t(#)s) = (u(#)t)(#)s;

theorem :: ISOCAT_1:45
   G1 is_naturally_transformable_to G2 implies t*F = t(#)id F;

theorem :: ISOCAT_1:46
   F1 is_naturally_transformable_to F2 implies G*s = (id G)(#)s;

theorem :: ISOCAT_1:47
   F1 is_naturally_transformable_to F2 &
 F2 is_naturally_transformable_to F3 &
 G1 is_naturally_transformable_to G2 &
 G2 is_naturally_transformable_to G3 implies
 (t'`*`t)(#)(s'`*`s) = (t'(#)s')`*`(t(#)s);

theorem :: ISOCAT_1:48
 for F being Functor of A,B, G being Functor of C,D
 for I,J being Functor of B,C st I ~= J holds G*I ~= G*J & I*F ~= J*F;

theorem :: ISOCAT_1:49
 for F being Functor of A,B, G being Functor of B,A
 for I being Functor of A,A st I ~= id A holds F*I ~= F & I*G ~= G;

definition
 let A,B be Category;
 pred A is_equivalent_with B means
:: ISOCAT_1:def 10
 ex F being Functor of A,B, G being Functor of B,A st
   G*F ~= id A & F*G ~= id B;
 reflexivity;
 symmetry;
 synonym A,B are_equivalent;
end;

theorem :: ISOCAT_1:50
   A ~= B implies A is_equivalent_with B;

canceled 2;

theorem :: ISOCAT_1:53
 A,B are_equivalent & B,C are_equivalent implies A,C are_equivalent;

definition let A,B;
 assume
 A,B are_equivalent;
 mode Equivalence of A,B -> Functor of A,B means
:: ISOCAT_1:def 11
 ex G being Functor of B,A st G*it ~= id A & it*G ~= id B;
end;

theorem :: ISOCAT_1:54
   id A is Equivalence of A,A;

theorem :: ISOCAT_1:55
   A,B are_equivalent & B,C are_equivalent implies
  for F being Equivalence of A,B, G being Equivalence of B,C holds
    G*F is Equivalence of A,C;

theorem :: ISOCAT_1:56
 A,B are_equivalent implies
  for F being Equivalence of A,B ex G being Equivalence of B,A
   st G*F ~= id A & F*G ~= id B;

theorem :: ISOCAT_1:57
 for F being Functor of A,B, G being Functor of B,A st G*F ~= id A
  holds F is faithful;

theorem :: ISOCAT_1:58
   A,B are_equivalent implies
 for F being Equivalence of A,B
  holds F is full & F is faithful &
   for b being Object of B ex a being Object of A st b, F.a are_isomorphic;