mathlib documentation

category_theory.equivalence

Equivalence of categories #

An equivalence of categories C and D is a pair of functors F : C ā„¤ D and G : D ā„¤ C such that Ī· : šŸ­ C ā‰… F ā‹™ G and Īµ : G ā‹™ F ā‰… šŸ­ D. In many situations, equivalences are a better notion of "sameness" of categories than the stricter isomorphims of categories.

Recall that one way to express that two functors F : C ā„¤ D and G : D ā„¤ C are adjoint is using two natural transformations Ī· : šŸ­ C āŸ¶ F ā‹™ G and Īµ : G ā‹™ F āŸ¶ šŸ­ D, called the unit and the counit, such that the compositions F āŸ¶ FGF āŸ¶ F and G āŸ¶ GFG āŸ¶ G are the identity. Unfortunately, it is not the case that the natural isomorphisms Ī· and Īµ in the definition of an equivalence automatically give an adjunction. However, it is true that

For this reason, in mathlib we define an equivalence to be a "half-adjoint equivalence", which is a tuple (F, G, Ī·, Īµ) as in the first paragraph such that the composite F āŸ¶ FGF āŸ¶ F is the identity. By the remark above, this already implies that the tuple is an "adjoint equivalence", i.e., that the composite G āŸ¶ GFG āŸ¶ G is also the identity.

We also define essentially surjective functors and show that a functor is an equivalence if and only if it is full, faithful and essentially surjective.

Main definitions #

Main results #

Notations #

We write C ā‰Œ D (\backcong, not to be confused with ā‰…/\cong) for a bundled equivalence.

structure category_theory.equivalence (C : Type uā‚) [category_theory.category C] (D : Type uā‚‚) [category_theory.category D] :
Type (max uā‚ uā‚‚ vā‚ vā‚‚)

We define an equivalence as a (half)-adjoint equivalence, a pair of functors with a unit and counit which are natural isomorphisms and the triangle law FĪ· ā‰« ĪµF = 1, or in other words the composite F āŸ¶ FGF āŸ¶ F is the identity.

In unit_inverse_comp, we show that this is actually an adjoint equivalence, i.e., that the composite G āŸ¶ GFG āŸ¶ G is also the identity.

The triangle equation is written as a family of equalities between morphisms, it is more complicated if we write it as an equality of natural transformations, because then we would have to insert natural transformations like F āŸ¶ F1.

See https://stacks.math.columbia.edu/tag/001J

theorem category_theory.equivalence.functor_unit_iso_comp {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (self : C ā‰Œ D) (X : C) :
self.functor.map (self.unit_iso.hom.app X) ā‰« self.counit_iso.hom.app (self.functor.obj X) = šŸ™ (self.functor.obj X)

The unit of an equivalence of categories.

The counit of an equivalence of categories.

The inverse of the unit of an equivalence of categories.

The inverse of the counit of an equivalence of categories.

@[simp]
theorem category_theory.equivalence.equivalence_mk'_unit {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (functor : C ā„¤ D) (inverse : D ā„¤ C) (unit_iso : šŸ­ C ā‰… functor ā‹™ inverse) (counit_iso : inverse ā‹™ functor ā‰… šŸ­ D) (f : (āˆ€ (X : C), functor.map (unit_iso.hom.app X) ā‰« counit_iso.hom.app (functor.obj X) = šŸ™ (functor.obj X)) . "obviously") :
{functor := functor, inverse := inverse, unit_iso := unit_iso, counit_iso := counit_iso, functor_unit_iso_comp' := f}.unit = unit_iso.hom
@[simp]
theorem category_theory.equivalence.equivalence_mk'_counit {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (functor : C ā„¤ D) (inverse : D ā„¤ C) (unit_iso : šŸ­ C ā‰… functor ā‹™ inverse) (counit_iso : inverse ā‹™ functor ā‰… šŸ­ D) (f : (āˆ€ (X : C), functor.map (unit_iso.hom.app X) ā‰« counit_iso.hom.app (functor.obj X) = šŸ™ (functor.obj X)) . "obviously") :
{functor := functor, inverse := inverse, unit_iso := unit_iso, counit_iso := counit_iso, functor_unit_iso_comp' := f}.counit = counit_iso.hom
@[simp]
theorem category_theory.equivalence.equivalence_mk'_unit_inv {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (functor : C ā„¤ D) (inverse : D ā„¤ C) (unit_iso : šŸ­ C ā‰… functor ā‹™ inverse) (counit_iso : inverse ā‹™ functor ā‰… šŸ­ D) (f : (āˆ€ (X : C), functor.map (unit_iso.hom.app X) ā‰« counit_iso.hom.app (functor.obj X) = šŸ™ (functor.obj X)) . "obviously") :
{functor := functor, inverse := inverse, unit_iso := unit_iso, counit_iso := counit_iso, functor_unit_iso_comp' := f}.unit_inv = unit_iso.inv
@[simp]
theorem category_theory.equivalence.equivalence_mk'_counit_inv {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (functor : C ā„¤ D) (inverse : D ā„¤ C) (unit_iso : šŸ­ C ā‰… functor ā‹™ inverse) (counit_iso : inverse ā‹™ functor ā‰… šŸ­ D) (f : (āˆ€ (X : C), functor.map (unit_iso.hom.app X) ā‰« counit_iso.hom.app (functor.obj X) = šŸ™ (functor.obj X)) . "obviously") :
{functor := functor, inverse := inverse, unit_iso := unit_iso, counit_iso := counit_iso, functor_unit_iso_comp' := f}.counit_inv = counit_iso.inv
@[simp]
theorem category_theory.equivalence.functor_unit_comp {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) (X : C) :
@[simp]
theorem category_theory.equivalence.counit_inv_app_functor {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) (X : C) :
theorem category_theory.equivalence.counit_app_functor {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) (X : C) :
@[simp]
theorem category_theory.equivalence.unit_inverse_comp {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) (Y : D) :

The other triangle equality. The proof follows the following proof in Globular: http://globular.science/1905.001

@[simp]
theorem category_theory.equivalence.unit_app_inverse {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) (Y : D) :
theorem category_theory.equivalence.unit_inv_app_inverse {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) (Y : D) :
@[simp]
theorem category_theory.equivalence.fun_inv_map {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) (X Y : D) (f : X āŸ¶ Y) :
@[simp]
theorem category_theory.equivalence.inv_fun_map {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) (X Y : C) (f : X āŸ¶ Y) :
def category_theory.equivalence.adjointify_Ī· {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] {F : C ā„¤ D} {G : D ā„¤ C} (Ī· : šŸ­ C ā‰… F ā‹™ G) (Īµ : G ā‹™ F ā‰… šŸ­ D) :

If Ī· : šŸ­ C ā‰… F ā‹™ G is part of a (not necessarily half-adjoint) equivalence, we can upgrade it to a refined natural isomorphism adjointify_Ī· Ī· : šŸ­ C ā‰… F ā‹™ G which exhibits the properties required for a half-adjoint equivalence. See equivalence.mk.

Equations
theorem category_theory.equivalence.adjointify_Ī·_Īµ {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] {F : C ā„¤ D} {G : D ā„¤ C} (Ī· : šŸ­ C ā‰… F ā‹™ G) (Īµ : G ā‹™ F ā‰… šŸ­ D) (X : C) :
@[protected]
def category_theory.equivalence.mk {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (F : C ā„¤ D) (G : D ā„¤ C) (Ī· : šŸ­ C ā‰… F ā‹™ G) (Īµ : G ā‹™ F ā‰… šŸ­ D) :
C ā‰Œ D

Every equivalence of categories consisting of functors F and G such that F ā‹™ G and G ā‹™ F are naturally isomorphic to identity functors can be transformed into a half-adjoint equivalence without changing F or G.

Equations
@[simp]
theorem category_theory.equivalence.symm_inverse {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) :
@[simp]
theorem category_theory.equivalence.symm_functor {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) :
def category_theory.equivalence.symm {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) :
D ā‰Œ C

Equivalence of categories is symmetric.

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.equivalence.trans_functor {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] {E : Type uā‚ƒ} [category_theory.category E] (e : C ā‰Œ D) (f : D ā‰Œ E) :
@[simp]
theorem category_theory.equivalence.trans_inverse {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] {E : Type uā‚ƒ} [category_theory.category E] (e : C ā‰Œ D) (f : D ā‰Œ E) :
def category_theory.equivalence.fun_inv_id_assoc {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] {E : Type uā‚ƒ} [category_theory.category E] (e : C ā‰Œ D) (F : C ā„¤ E) :

Composing a functor with both functors of an equivalence yields a naturally isomorphic functor.

Equations
@[simp]
theorem category_theory.equivalence.fun_inv_id_assoc_hom_app {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] {E : Type uā‚ƒ} [category_theory.category E] (e : C ā‰Œ D) (F : C ā„¤ E) (X : C) :
@[simp]
theorem category_theory.equivalence.fun_inv_id_assoc_inv_app {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] {E : Type uā‚ƒ} [category_theory.category E] (e : C ā‰Œ D) (F : C ā„¤ E) (X : C) :
(e.fun_inv_id_assoc F).inv.app X = F.map (e.unit.app X)
def category_theory.equivalence.inv_fun_id_assoc {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] {E : Type uā‚ƒ} [category_theory.category E] (e : C ā‰Œ D) (F : D ā„¤ E) :

Composing a functor with both functors of an equivalence yields a naturally isomorphic functor.

Equations
@[simp]
theorem category_theory.equivalence.inv_fun_id_assoc_hom_app {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] {E : Type uā‚ƒ} [category_theory.category E] (e : C ā‰Œ D) (F : D ā„¤ E) (X : D) :
@[simp]
theorem category_theory.equivalence.inv_fun_id_assoc_inv_app {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] {E : Type uā‚ƒ} [category_theory.category E] (e : C ā‰Œ D) (F : D ā„¤ E) (X : D) :
def category_theory.equivalence.congr_left {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] {E : Type uā‚ƒ} [category_theory.category E] (e : C ā‰Œ D) :

If C is equivalent to D, then C ā„¤ E is equivalent to D ā„¤ E.

Equations
@[simp]
theorem category_theory.equivalence.cancel_unit_right {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) {X Y : C} (f f' : X āŸ¶ Y) :
f ā‰« e.unit.app Y = f' ā‰« e.unit.app Y ā†” f = f'
@[simp]
theorem category_theory.equivalence.cancel_unit_inv_right {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) {X Y : C} (f f' : X āŸ¶ e.inverse.obj (e.functor.obj Y)) :
@[simp]
theorem category_theory.equivalence.cancel_counit_right {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) {X Y : D} (f f' : X āŸ¶ e.functor.obj (e.inverse.obj Y)) :
f ā‰« e.counit.app Y = f' ā‰« e.counit.app Y ā†” f = f'
@[simp]
theorem category_theory.equivalence.cancel_counit_inv_right {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) {X Y : D} (f f' : X āŸ¶ Y) :
@[simp]
theorem category_theory.equivalence.cancel_unit_right_assoc {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) {W X X' Y : C} (f : W āŸ¶ X) (g : X āŸ¶ Y) (f' : W āŸ¶ X') (g' : X' āŸ¶ Y) :
f ā‰« g ā‰« e.unit.app Y = f' ā‰« g' ā‰« e.unit.app Y ā†” f ā‰« g = f' ā‰« g'
@[simp]
theorem category_theory.equivalence.cancel_counit_inv_right_assoc {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) {W X X' Y : D} (f : W āŸ¶ X) (g : X āŸ¶ Y) (f' : W āŸ¶ X') (g' : X' āŸ¶ Y) :
@[simp]
theorem category_theory.equivalence.cancel_unit_right_assoc' {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) {W X X' Y Y' Z : C} (f : W āŸ¶ X) (g : X āŸ¶ Y) (h : Y āŸ¶ Z) (f' : W āŸ¶ X') (g' : X' āŸ¶ Y') (h' : Y' āŸ¶ Z) :
@[simp]
theorem category_theory.equivalence.cancel_counit_inv_right_assoc' {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) {W X X' Y Y' Z : D} (f : W āŸ¶ X) (g : X āŸ¶ Y) (h : Y āŸ¶ Z) (f' : W āŸ¶ X') (g' : X' āŸ¶ Y') (h' : Y' āŸ¶ Z) :
def category_theory.equivalence.pow_nat {C : Type uā‚} [category_theory.category C] (e : C ā‰Œ C) :
ā„• ā†’ (C ā‰Œ C)

Natural number powers of an auto-equivalence. Use (^) instead.

Equations
def category_theory.equivalence.pow {C : Type uā‚} [category_theory.category C] (e : C ā‰Œ C) :
ā„¤ ā†’ (C ā‰Œ C)

Powers of an auto-equivalence. Use (^) instead.

Equations
@[simp]
theorem category_theory.equivalence.pow_one {C : Type uā‚} [category_theory.category C] (e : C ā‰Œ C) :
e ^ 1 = e
@[simp]
theorem category_theory.equivalence.pow_neg_one {C : Type uā‚} [category_theory.category C] (e : C ā‰Œ C) :
e ^ -1 = e.symm
@[protected]
def category_theory.is_equivalence.mk {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] {F : C ā„¤ D} (G : D ā„¤ C) (Ī· : šŸ­ C ā‰… F ā‹™ G) (Īµ : G ā‹™ F ā‰… šŸ­ D) :

To see that a functor is an equivalence, it suffices to provide an inverse functor G such that F ā‹™ G and G ā‹™ F are naturally isomorphic to identity functors.

Equations

The inverse functor of a functor that is an equivalence.

Equations
@[simp]
theorem category_theory.functor.inv_inv {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (F : C ā„¤ D) [category_theory.is_equivalence F] :
F.inv.inv = F
@[simp]
theorem category_theory.equivalence.functor_inv {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (E : C ā‰Œ D) :
@[simp]
theorem category_theory.equivalence.inverse_inv {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (E : C ā‰Œ D) :
@[simp]

Compatibility of of_iso with the composition of isomorphisms of functors

Compatibility of of_iso with identity isomorphisms of functors

@[simp]
theorem category_theory.equivalence.functor_map_inj_iff {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) {X Y : C} (f g : X āŸ¶ Y) :
@[simp]
theorem category_theory.equivalence.inverse_map_inj_iff {C : Type uā‚} [category_theory.category C] {D : Type uā‚‚} [category_theory.category D] (e : C ā‰Œ D) {X Y : D} (f g : X āŸ¶ Y) :