# mathlib3documentation

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

• if one of the two compositions is the identity, then so is the other, and
• given an equivalence of categories, it is always possible to refine `η` in such a way that the identities are satisfied.

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 #

• `equivalence`: bundled (half-)adjoint equivalences of categories
• `is_equivalence`: type class on a functor `F` containing the data of the inverse `G` as well as the natural isomorphisms `η` and `ε`.
• `ess_surj`: type class on a functor `F` containing the data of the preimages and the isomorphisms `F.obj (preimage d) ≅ d`.

## Main results #

• `equivalence.mk`: upgrade an equivalence to a (half-)adjoint equivalence
• `is_equivalence.equiv_of_iso`: when `F` and `G` are isomorphic functors, `F` is an equivalence iff `G` is.
• `equivalence.of_fully_faithfully_ess_surj`: a fully faithful essentially surjective functor is an equivalence.

## Notations #

We write `C ≌ D` (`\backcong`, not to be confused with `≅`/`\cong`) for a bundled equivalence.

structure category_theory.equivalence (C : Type u₁) (D : Type u₂)  :
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`.

Instances for `category_theory.equivalence`
theorem category_theory.equivalence.functor_unit_iso_comp {C : Type u₁} {D : Type u₂} (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]
def category_theory.equivalence.unit {C : Type u₁} {D : Type u₂} (e : C D) :

The unit of an equivalence of categories.

@[reducible]
def category_theory.equivalence.counit {C : Type u₁} {D : Type u₂} (e : C D) :

The counit of an equivalence of categories.

@[reducible]
def category_theory.equivalence.unit_inv {C : Type u₁} {D : Type u₂} (e : C D) :

The inverse of the unit of an equivalence of categories.

@[reducible]
def category_theory.equivalence.counit_inv {C : Type u₁} {D : Type u₂} (e : C D) :

The inverse of the counit of an equivalence of categories.

@[simp]
theorem category_theory.equivalence.equivalence_mk'_unit {C : Type u₁} {D : Type u₂} (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₁} {D : Type u₂} (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₁} {D : Type u₂} (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₁} {D : Type u₂} (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₁} {D : Type u₂} (e : C D) (X : C) :
@[simp]
theorem category_theory.equivalence.counit_inv_functor_comp {C : Type u₁} {D : Type u₂} (e : C D) (X : C) :
theorem category_theory.equivalence.counit_inv_app_functor {C : Type u₁} {D : Type u₂} (e : C D) (X : C) :
theorem category_theory.equivalence.counit_app_functor {C : Type u₁} {D : Type u₂} (e : C D) (X : C) :
@[simp]
theorem category_theory.equivalence.unit_inverse_comp {C : Type u₁} {D : Type u₂} (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.inverse_counit_inv_comp {C : Type u₁} {D : Type u₂} (e : C D) (Y : D) :
theorem category_theory.equivalence.unit_app_inverse {C : Type u₁} {D : Type u₂} (e : C D) (Y : D) :
theorem category_theory.equivalence.unit_inv_app_inverse {C : Type u₁} {D : Type u₂} (e : C D) (Y : D) :
@[simp]
theorem category_theory.equivalence.fun_inv_map {C : Type u₁} {D : Type u₂} (e : C D) (X Y : D) (f : X Y) :
@[simp]
theorem category_theory.equivalence.inv_fun_map {C : Type u₁} {D : Type u₂} (e : C D) (X Y : C) (f : X Y) :
def category_theory.equivalence.adjointify_η {C : Type u₁} {D : Type u₂} {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₁} {D : Type u₂} {F : C D} {G : D C} (η : 𝟭 C F G) (ε : G F 𝟭 D) (X : C) :
F.map ε.hom.app (F.obj X) = 𝟙 (F.obj X)
@[protected]
def category_theory.equivalence.mk {C : Type u₁} {D : Type u₂} (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]
@[simp]
@[simp]
@[refl]
def category_theory.equivalence.refl {C : Type u₁}  :
C C

Equivalence of categories is reflexive.

Equations
@[simp]
@[protected, instance]
Equations
@[simp]
theorem category_theory.equivalence.symm_inverse {C : Type u₁} {D : Type u₂} (e : C D) :
@[simp]
theorem category_theory.equivalence.symm_functor {C : Type u₁} {D : Type u₂} (e : C D) :
@[symm]
def category_theory.equivalence.symm {C : Type u₁} {D : Type u₂} (e : C D) :
D C

Equivalence of categories is symmetric.

Equations
@[simp]
theorem category_theory.equivalence.symm_unit_iso {C : Type u₁} {D : Type u₂} (e : C D) :
@[simp]
theorem category_theory.equivalence.symm_counit_iso {C : Type u₁} {D : Type u₂} (e : C D) :
@[trans]
def category_theory.equivalence.trans {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) (f : D E) :
C E

Equivalence of categories is transitive.

Equations
@[simp]
theorem category_theory.equivalence.trans_functor {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) (f : D E) :
@[simp]
theorem category_theory.equivalence.trans_counit_iso {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) (f : D E) :
@[simp]
theorem category_theory.equivalence.trans_inverse {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) (f : D E) :
@[simp]
theorem category_theory.equivalence.trans_unit_iso {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) (f : D E) :
def category_theory.equivalence.fun_inv_id_assoc {C : Type u₁} {D : Type u₂} {E : Type u₃} (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₁} {D : Type u₂} {E : Type u₃} (e : C D) (F : C E) (X : C) :
@[simp]
theorem category_theory.equivalence.fun_inv_id_assoc_inv_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (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₁} {D : Type u₂} {E : Type u₃} (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₁} {D : Type u₂} {E : Type u₃} (e : C D) (F : D E) (X : D) :
@[simp]
theorem category_theory.equivalence.inv_fun_id_assoc_inv_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) (F : D E) (X : D) :
@[simp]
theorem category_theory.equivalence.congr_left_counit_iso {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) :
@[simp]
theorem category_theory.equivalence.congr_left_unit_iso {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) :
@[simp]
theorem category_theory.equivalence.congr_left_functor {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) :
def category_theory.equivalence.congr_left {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) :
C E D E

If `C` is equivalent to `D`, then `C ⥤ E` is equivalent to `D ⥤ E`.

Equations
@[simp]
theorem category_theory.equivalence.congr_left_inverse {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) :
@[simp]
def category_theory.equivalence.congr_right {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) :
E C E D

If `C` is equivalent to `D`, then `E ⥤ C` is equivalent to `E ⥤ D`.

Equations
@[simp]
theorem category_theory.equivalence.congr_right_functor {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) :
@[simp]
theorem category_theory.equivalence.congr_right_inverse {C : Type u₁} {D : Type u₂} {E : Type u₃} (e : C D) :
@[simp]
theorem category_theory.equivalence.cancel_unit_right {C : Type u₁} {D : Type u₂} (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₁} {D : Type u₂} (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₁} {D : Type u₂} (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₁} {D : Type u₂} (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₁} {D : Type u₂} (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₁} {D : Type u₂} (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₁} {D : Type u₂} (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₁} {D : Type u₂} (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'
def category_theory.equivalence.pow_nat {C : Type u₁} (e : C C) :
(C C)

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

Equations
def category_theory.equivalence.pow {C : Type u₁} (e : C C) :
(C C)

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

Equations
@[protected, instance]
Equations
@[simp]
theorem category_theory.equivalence.pow_zero {C : Type u₁} (e : C C) :
@[simp]
theorem category_theory.equivalence.pow_one {C : Type u₁} (e : C C) :
e ^ 1 = e
@[simp]
theorem category_theory.equivalence.pow_neg_one {C : Type u₁} (e : C C) :
e ^ -1 = e.symm
@[class]
structure category_theory.is_equivalence {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ v₂)
• inverse : D C
• unit_iso :
• counit_iso :
• functor_unit_iso_comp' : ( (X : C), = 𝟙 (F.obj X)) . "obviously"

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
@[simp]
theorem category_theory.is_equivalence.functor_unit_iso_comp {C : Type u₁} {D : Type u₂} {F : C D} [self : category_theory.is_equivalence F] (X : C) :
= 𝟙 (F.obj X)
@[simp]
theorem category_theory.is_equivalence.functor_unit_iso_comp_assoc {C : Type u₁} {D : Type u₂} {F : C D} [self : category_theory.is_equivalence F] (X : C) {X' : D} (f' : F.obj X X') :
= f'
@[protected, instance]
def category_theory.is_equivalence.of_equivalence {C : Type u₁} {D : Type u₂} (F : C D) :
Equations
@[protected, instance]
def category_theory.is_equivalence.of_equivalence_inverse {C : Type u₁} {D : Type u₂} (F : C D) :
Equations
@[protected]
def category_theory.is_equivalence.mk {C : Type u₁} {D : Type u₂} {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
def category_theory.functor.as_equivalence {C : Type u₁} {D : Type u₂} (F : C D)  :
C D

Interpret a functor that is an equivalence as an equivalence.

Equations
@[protected, instance]
Equations
def category_theory.functor.inv {C : Type u₁} {D : Type u₂} (F : C D)  :
D C

The inverse functor of a functor that is an equivalence.

Equations
Instances for `category_theory.functor.inv`
@[protected, instance]
def category_theory.functor.is_equivalence_inv {C : Type u₁} {D : Type u₂} (F : C D)  :
Equations
@[simp]
theorem category_theory.functor.as_equivalence_functor {C : Type u₁} {D : Type u₂} (F : C D)  :
@[simp]
theorem category_theory.functor.as_equivalence_inverse {C : Type u₁} {D : Type u₂} (F : C D)  :
@[simp]
theorem category_theory.functor.as_equivalence_unit {C : Type u₁} {D : Type u₂} {F : C D}  :
@[simp]
theorem category_theory.functor.as_equivalence_counit {C : Type u₁} {D : Type u₂} {F : C D}  :
@[simp]
theorem category_theory.functor.inv_inv {C : Type u₁} {D : Type u₂} (F : C D)  :
F.inv.inv = F
@[protected, instance]
def category_theory.functor.is_equivalence_trans {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D) (G : D E)  :
Equations
@[simp]
theorem category_theory.equivalence.functor_inv {C : Type u₁} {D : Type u₂} (E : C D) :
@[simp]
theorem category_theory.equivalence.inverse_inv {C : Type u₁} {D : Type u₂} (E : C D) :
@[simp]
theorem category_theory.equivalence.functor_as_equivalence {C : Type u₁} {D : Type u₂} (E : C D) :
@[simp]
theorem category_theory.equivalence.inverse_as_equivalence {C : Type u₁} {D : Type u₂} (E : C D) :
@[simp]
theorem category_theory.is_equivalence.fun_inv_map {C : Type u₁} {D : Type u₂} (F : C D) (X Y : D) (f : X Y) :
F.map (F.inv.map f) = f
@[simp]
theorem category_theory.is_equivalence.inv_fun_map {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) (f : X Y) :
F.inv.map (F.map f) = f
def category_theory.is_equivalence.of_iso {C : Type u₁} {D : Type u₂} {F G : C D} (e : F G)  :

When a functor `F` is an equivalence of categories, and `G` is isomorphic to `F`, then `G` is also an equivalence of categories.

Equations
@[simp]
theorem category_theory.is_equivalence.of_iso_counit_iso {C : Type u₁} {D : Type u₂} {F G : C D} (e : F G)  :
@[simp]
theorem category_theory.is_equivalence.of_iso_inverse {C : Type u₁} {D : Type u₂} {F G : C D} (e : F G)  :
@[simp]
theorem category_theory.is_equivalence.of_iso_unit_iso {C : Type u₁} {D : Type u₂} {F G : C D} (e : F G)  :
theorem category_theory.is_equivalence.of_iso_trans {C : Type u₁} {D : Type u₂} {F G H : C D} (e : F G) (e' : G H)  :

Compatibility of `of_iso` with the composition of isomorphisms of functors

theorem category_theory.is_equivalence.of_iso_refl {C : Type u₁} {D : Type u₂} (F : C D)  :

Compatibility of `of_iso` with identity isomorphisms of functors

def category_theory.is_equivalence.equiv_of_iso {C : Type u₁} {D : Type u₂} {F G : C D} (e : F G) :

When `F` and `G` are two isomorphic functors, then `F` is an equivalence iff `G` is.

Equations
@[simp]
theorem category_theory.is_equivalence.equiv_of_iso_symm_apply {C : Type u₁} {D : Type u₂} {F G : C D} (e : F G)  :
@[simp]
theorem category_theory.is_equivalence.equiv_of_iso_apply {C : Type u₁} {D : Type u₂} {F G : C D} (e : F G)  :
@[simp]
def category_theory.is_equivalence.cancel_comp_right {C : Type u₁} {D : Type u₂} {E : Type u_1} (F : C D) (G : D E) (hGF : category_theory.is_equivalence (F G)) :

If `G` and `F ⋙ G` are equivalence of categories, then `F` is also an equivalence.

Equations
@[simp]
def category_theory.is_equivalence.cancel_comp_left {C : Type u₁} {D : Type u₂} {E : Type u_1} (F : C D) (G : D E) (hGF : category_theory.is_equivalence (F G)) :

If `F` and `F ⋙ G` are equivalence of categories, then `G` is also an equivalence.

Equations
theorem category_theory.equivalence.ess_surj_of_equivalence {C : Type u₁} {D : Type u₂} (F : C D)  :

An equivalence is essentially surjective.

@[protected, instance]
def category_theory.equivalence.faithful_of_equivalence {C : Type u₁} {D : Type u₂} (F : C D)  :

An equivalence is faithful.

@[protected, instance]
def category_theory.equivalence.full_of_equivalence {C : Type u₁} {D : Type u₂} (F : C D)  :

An equivalence is full.

Equations
noncomputable def category_theory.equivalence.of_fully_faithfully_ess_surj {C : Type u₁} {D : Type u₂} (F : C D)  :

A functor which is full, faithful, and essentially surjective is an equivalence.

Equations
@[simp]
theorem category_theory.equivalence.functor_map_inj_iff {C : Type u₁} {D : Type u₂} (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₁} {D : Type u₂} (e : C D) {X Y : D} (f g : X Y) :
e.inverse.map f = e.inverse.map g f = g
@[protected, instance]
def category_theory.equivalence.ess_surj_induced_functor {D : Type u₂} {C' : Type u_1} (e : C' D) :
@[protected, instance]
noncomputable def category_theory.equivalence.induced_functor_of_equiv {D : Type u₂} {C' : Type u_1} (e : C' D) :
Equations
@[protected, instance]
noncomputable def category_theory.equivalence.fully_faithful_to_ess_image {C : Type u₁} {D : Type u₂} (F : C D)  :
Equations