Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### 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;
```