mathlib3 documentation

category_theory.equivalence

Equivalence of categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :
𝟭 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) :
@[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
@[refl]

Equivalence of categories is reflexive.

Equations
@[symm]

Equivalence of categories is symmetric.

Equations

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

Equations
@[simp]
@[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]
@[simp]
@[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)) :
f e.unit_inv.app Y = f' e.unit_inv.app Y f = f'
@[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) :
f e.counit_inv.app Y = f' e.counit_inv.app Y f = f'
@[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) :
f g e.counit_inv.app Y = f' g' e.counit_inv.app Y f g = f' g'
@[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) :
f g h e.unit.app Z = f' g' h' e.unit.app Z f g h = f' g' h'
@[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) :
f g h e.counit_inv.app Z = f' g' h' e.counit_inv.app Z f g h = f' g' h'

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

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) :
e.functor.map f = e.functor.map g f = g
@[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) :
e.inverse.map f = e.inverse.map g f = g