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

Instances for category_theory.equivalence
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)
@[reducible]

The unit of an equivalence of categories.

@[reducible]

The counit of an equivalence of categories.

@[reducible]

The inverse of the unit of an equivalence of categories.

@[reducible]

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]
@[simp]

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

@[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
@[symm]

Equivalence of categories is symmetric.

Equations
@[simp]
@[simp]

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)

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) :

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) :

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

Equations

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
@[class]
structure category_theory.is_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :
Type (max u₁ u₂ v₁ v₂)

A functor that is part of a (half) adjoint equivalence

Instances of this typeclass
Instances of other typeclasses for category_theory.is_equivalence
  • category_theory.is_equivalence.has_sizeof_inst
@[protected]

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
Instances for category_theory.functor.inv

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) :