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

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) β†’ (𝟭 C β‰… F β‹™ G)

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

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

@[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 {C : Type u₁} [category_theory.category C] :
(C β‰Œ C) β†’ β„€ β†’ (C β‰Œ C)

Powers of an auto-equivalence.

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_minus_one {C : Type u₁} [category_theory.category C] (e : C β‰Œ C) :
e ^ -1 = e.symm

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

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

The composition of functor that is an equivalence with its inverse is naturally isomorphic to the identity functor.

Equations

The composition of functor that is an equivalence with its inverse is naturally isomorphic to the identity functor.

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

@[simp]
theorem category_theory.is_equivalence.fun_inv_map {C : Type u₁} [category_theory.category C] {D : Type uβ‚‚} [category_theory.category D] (F : C β₯€ D) [category_theory.is_equivalence F] (X Y : D) (f : X ⟢ Y) :

@[simp]
theorem category_theory.is_equivalence.inv_fun_map {C : Type u₁} [category_theory.category C] {D : Type uβ‚‚} [category_theory.category D] (F : C β₯€ D) [category_theory.is_equivalence F] (X Y : C) (f : X ⟢ Y) :

@[class]
structure category_theory.ess_surj {C : Type u₁} [category_theory.category C] {D : Type uβ‚‚} [category_theory.category D] :
C β₯€ D β†’ Type (max u₁ uβ‚‚ vβ‚‚)

A functor F : C β₯€ D is essentially surjective if for every d : D, there is some c : C so F.obj c β‰… D.

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

Instances
def category_theory.functor.obj_preimage {C : Type u₁} [category_theory.category C] {D : Type uβ‚‚} [category_theory.category D] (F : C β₯€ D) [category_theory.ess_surj F] :
D β†’ C

Given an essentially surjective functor, we can find a preimage for every object d in the codomain. Applying the functor to this preimage will yield an object isomorphic to d, see fun_obj_preimage_iso.

Equations

Applying an essentially surjective functor to a preimage of d yields an object that is isomorphic to d.

Equations

An equivalence is essentially surjective.

See https://stacks.math.columbia.edu/tag/02C3.

Equations
@[instance]

An equivalence is faithful.

See https://stacks.math.columbia.edu/tag/02C3.

@[instance]

An equivalence is full.

See https://stacks.math.columbia.edu/tag/02C3.

Equations
@[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) :