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]
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) :
@[symm]
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
@[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]
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
Instances for category_theory.functor.inv
@[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) :