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

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₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

Type (max u₁ u₂ v₁ v₂)

functor : C ⥤ D
inverse : D ⥤ C
unit_iso : 𝟭 C ≅ self.functor ⋙ self.inverse
counit_iso : self.inverse ⋙ self.functor ≅ 𝟭 D
functor_unit_iso_comp' : (∀ (X : C), self.functor.map (self.unit_iso.hom.app X) ≫ self.counit_iso.hom.app (self.functor.obj X) = 𝟙 (self.functor.obj X)) . "obviously"

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

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)

def category_theory.equivalence.unit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

𝟭 C ⟶ e.functor ⋙ e.inverse

The unit of an equivalence of categories.

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

e.inverse ⋙ e.functor ⟶ 𝟭 D

The counit of an equivalence of categories.

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

e.functor ⋙ e.inverse ⟶ 𝟭 C

The inverse of the unit of an equivalence of categories.

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

𝟭 D ⟶ e.inverse ⋙ e.functor

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

e.functor.map (e.unit.app X) ≫ e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X)

@[simp]

theorem category_theory.equivalence.counit_inv_functor_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X : C) :

e.counit_inv.app (e.functor.obj X) ≫ e.functor.map (e.unit_inv.app X) = 𝟙 (e.functor.obj X)

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

e.counit_inv.app (e.functor.obj X) = e.functor.map (e.unit.app X)

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

e.counit.app (e.functor.obj X) = e.functor.map (e.unit_inv.app X)

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

e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (Y : D) :

e.inverse.map (e.counit_inv.app Y) ≫ e.unit_inv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y)

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

e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counit_inv.app Y)

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

e.unit_inv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y)

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

e.functor.map (e.inverse.map f) = e.counit.app X ≫ f ≫ e.counit_inv.app 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) :

e.inverse.map (e.functor.map f) = e.unit_inv.app X ≫ f ≫ e.unit.app 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

category_theory.equivalence.adjointify_η η ε = (((((η ≪≫ category_theory.iso_whisker_left F G.left_unitor.symm) ≪≫ category_theory.iso_whisker_left F (category_theory.iso_whisker_right ε.symm G)) ≪≫ category_theory.iso_whisker_left F (G.associator F G)) ≪≫ (F.associator G (F ⋙ G)).symm) ≪≫ category_theory.iso_whisker_right η.symm (F ⋙ G)) ≪≫ (F ⋙ G).left_unitor

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

F.map ((category_theory.equivalence.adjointify_η η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X)

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

category_theory.equivalence.mk F G η ε = {functor := F, inverse := G, unit_iso := category_theory.equivalence.adjointify_η η ε, counit_iso := ε, functor_unit_iso_comp' := _}

@[simp]

theorem category_theory.equivalence.refl_counit_iso {C : Type u₁} [category_theory.category C] :

category_theory.equivalence.refl.counit_iso = category_theory.iso.refl (𝟭 C ⋙ 𝟭 C)

@[simp]

theorem category_theory.equivalence.refl_inverse {C : Type u₁} [category_theory.category C] :

category_theory.equivalence.refl.inverse = 𝟭 C

@[simp]

theorem category_theory.equivalence.refl_unit_iso {C : Type u₁} [category_theory.category C] :

category_theory.equivalence.refl.unit_iso = category_theory.iso.refl (𝟭 C)

def category_theory.equivalence.refl {C : Type u₁} [category_theory.category C] :

C ≌ C

Equivalence of categories is reflexive.

Equations

category_theory.equivalence.refl = {functor := 𝟭 C _inst_1, inverse := 𝟭 C _inst_1, unit_iso := category_theory.iso.refl (𝟭 C), counit_iso := category_theory.iso.refl (𝟭 C ⋙ 𝟭 C), functor_unit_iso_comp' := _}

@[simp]

theorem category_theory.equivalence.refl_functor {C : Type u₁} [category_theory.category C] :

category_theory.equivalence.refl.functor = 𝟭 C

@[protected, instance]

def category_theory.equivalence.inhabited {C : Type u₁} [category_theory.category C] :

inhabited (C ≌ C)

Equations

category_theory.equivalence.inhabited = {default := category_theory.equivalence.refl _inst_1}

@[simp]

theorem category_theory.equivalence.symm_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

e.symm.inverse = e.functor

@[simp]

theorem category_theory.equivalence.symm_functor {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

e.symm.functor = e.inverse

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

e.symm = {functor := e.inverse, inverse := e.functor, unit_iso := e.counit_iso.symm, counit_iso := e.unit_iso.symm, functor_unit_iso_comp' := _}

@[simp]

theorem category_theory.equivalence.symm_unit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

e.symm.unit_iso = e.counit_iso.symm

@[simp]

theorem category_theory.equivalence.symm_counit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

e.symm.counit_iso = e.unit_iso.symm

def category_theory.equivalence.trans {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) :

C ≌ E

Equivalence of categories is transitive.

Equations

e.trans f = {functor := e.functor ⋙ f.functor, inverse := f.inverse ⋙ e.inverse, unit_iso := e.unit_iso ≪≫ category_theory.iso_whisker_left e.functor (category_theory.iso_whisker_right f.unit_iso e.inverse), counit_iso := category_theory.iso_whisker_left f.inverse (category_theory.iso_whisker_right e.counit_iso f.functor) ≪≫ f.counit_iso, functor_unit_iso_comp' := _}

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

(e.trans f).functor = e.functor ⋙ f.functor

@[simp]

theorem category_theory.equivalence.trans_counit_iso {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) :

(e.trans f).counit_iso = category_theory.iso_whisker_left f.inverse (category_theory.iso_whisker_right e.counit_iso f.functor) ≪≫ f.counit_iso

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

(e.trans f).inverse = f.inverse ⋙ e.inverse

@[simp]

theorem category_theory.equivalence.trans_unit_iso {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) :

(e.trans f).unit_iso = e.unit_iso ≪≫ category_theory.iso_whisker_left e.functor (category_theory.iso_whisker_right f.unit_iso e.inverse)

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

e.functor ⋙ e.inverse ⋙ F ≅ F

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

Equations

e.fun_inv_id_assoc F = (e.functor.associator e.inverse F).symm ≪≫ category_theory.iso_whisker_right e.unit_iso.symm F ≪≫ F.left_unitor

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

(e.fun_inv_id_assoc F).hom.app X = F.map (e.unit_inv.app X)

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

e.inverse ⋙ e.functor ⋙ F ≅ F

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

Equations

e.inv_fun_id_assoc F = (e.inverse.associator e.functor F).symm ≪≫ category_theory.iso_whisker_right e.counit_iso F ≪≫ F.left_unitor

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

(e.inv_fun_id_assoc F).hom.app X = F.map (e.counit.app X)

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

(e.inv_fun_id_assoc F).inv.app X = F.map (e.counit_inv.app X)

@[simp]

theorem category_theory.equivalence.congr_left_counit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) :

e.congr_left.counit_iso = category_theory.nat_iso.of_components e.inv_fun_id_assoc _

@[simp]

theorem category_theory.equivalence.congr_left_unit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) :

e.congr_left.unit_iso = category_theory.equivalence.adjointify_η (category_theory.nat_iso.of_components (λ (F : C ⥤ E), (e.fun_inv_id_assoc F).symm) _) (category_theory.nat_iso.of_components e.inv_fun_id_assoc _)

@[simp]

theorem category_theory.equivalence.congr_left_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) :

e.congr_left.functor = (category_theory.whiskering_left D C E).obj e.inverse

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

C ⥤ E ≌ D ⥤ E

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

Equations

e.congr_left = category_theory.equivalence.mk ((category_theory.whiskering_left D C E).obj e.inverse) ((category_theory.whiskering_left C D E).obj e.functor) (category_theory.nat_iso.of_components (λ (F : C ⥤ E), (e.fun_inv_id_assoc F).symm) _) (category_theory.nat_iso.of_components (λ (F : D ⥤ E), e.inv_fun_id_assoc F) _)

@[simp]

theorem category_theory.equivalence.congr_left_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) :

e.congr_left.inverse = (category_theory.whiskering_left C D E).obj e.functor

@[simp]

theorem category_theory.equivalence.congr_right_counit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) :

e.congr_right.counit_iso = category_theory.nat_iso.of_components (λ (F : E ⥤ D), F.associator e.inverse e.functor ≪≫ category_theory.iso_whisker_left F e.counit_iso ≪≫ F.right_unitor) _

def category_theory.equivalence.congr_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) :

E ⥤ C ≌ E ⥤ D

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

Equations

e.congr_right = category_theory.equivalence.mk ((category_theory.whiskering_right E C D).obj e.functor) ((category_theory.whiskering_right E D C).obj e.inverse) (category_theory.nat_iso.of_components (λ (F : E ⥤ C), F.right_unitor.symm ≪≫ category_theory.iso_whisker_left F e.unit_iso ≪≫ F.associator e.functor e.inverse) _) (category_theory.nat_iso.of_components (λ (F : E ⥤ D), F.associator e.inverse e.functor ≪≫ category_theory.iso_whisker_left F e.counit_iso ≪≫ F.right_unitor) _)

@[simp]

theorem category_theory.equivalence.congr_right_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) :

e.congr_right.functor = (category_theory.whiskering_right E C D).obj e.functor

@[simp]

theorem category_theory.equivalence.congr_right_unit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) :

e.congr_right.unit_iso = category_theory.equivalence.adjointify_η (category_theory.nat_iso.of_components (λ (F : E ⥤ C), F.right_unitor.symm ≪≫ category_theory.iso_whisker_left F e.unit_iso ≪≫ F.associator e.functor e.inverse) _) (category_theory.nat_iso.of_components (λ (F : E ⥤ D), F.associator e.inverse e.functor ≪≫ category_theory.iso_whisker_left F e.counit_iso ≪≫ F.right_unitor) _)

@[simp]

theorem category_theory.equivalence.congr_right_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) :

e.congr_right.inverse = (category_theory.whiskering_right E D C).obj e.inverse

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

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

e.pow_nat (n + 2) = e.trans (e.pow_nat n.succ)
e.pow_nat 1 = e
e.pow_nat 0 = category_theory.equivalence.refl

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

e.pow -[1+ n] = e.symm.pow_nat (n + 1)
e.pow (int.of_nat n) = e.pow_nat n

@[protected, instance]

def category_theory.equivalence.int.has_pow {C : Type u₁} [category_theory.category C] :

has_pow (C ≌ C) ℤ

Equations

category_theory.equivalence.int.has_pow = {pow := category_theory.equivalence.pow _inst_1}

@[simp]

theorem category_theory.equivalence.pow_zero {C : Type u₁} [category_theory.category C] (e : C ≌ C) :

e ^ 0 = category_theory.equivalence.refl

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

inverse : D ⥤ C
unit_iso : 𝟭 C ≅ F ⋙ category_theory.is_equivalence.inverse F
counit_iso : category_theory.is_equivalence.inverse F ⋙ F ≅ 𝟭 D
functor_unit_iso_comp' : (∀ (X : C), F.map (category_theory.is_equivalence.unit_iso.hom.app X) ≫ category_theory.is_equivalence.counit_iso.hom.app (F.obj X) = 𝟙 (F.obj X)) . "obviously"

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

Instances

@[simp]

theorem category_theory.is_equivalence.functor_unit_iso_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} [self : category_theory.is_equivalence F] (X : C) :

F.map (category_theory.is_equivalence.unit_iso.hom.app X) ≫ category_theory.is_equivalence.counit_iso.hom.app (F.obj X) = 𝟙 (F.obj X)

@[simp]

theorem category_theory.is_equivalence.functor_unit_iso_comp_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} [self : category_theory.is_equivalence F] (X : C) {X' : D} (f' : F.obj X ⟶ X') :

F.map (category_theory.is_equivalence.unit_iso.hom.app X) ≫ category_theory.is_equivalence.counit_iso.hom.app (F.obj X) ≫ f' = f'

@[protected, instance]

def category_theory.is_equivalence.of_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ≌ D) :

category_theory.is_equivalence F.functor

Equations

category_theory.is_equivalence.of_equivalence F = {inverse := F.inverse, unit_iso := F.unit_iso, counit_iso := F.counit_iso, functor_unit_iso_comp' := _}

@[protected, instance]

def category_theory.is_equivalence.of_equivalence_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ≌ D) :

category_theory.is_equivalence F.inverse

Equations

category_theory.is_equivalence.of_equivalence_inverse F = category_theory.is_equivalence.of_equivalence F.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) :

category_theory.is_equivalence F

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

category_theory.is_equivalence.mk G η ε = {inverse := G, unit_iso := category_theory.equivalence.adjointify_η η ε, counit_iso := ε, functor_unit_iso_comp' := _}

def category_theory.functor.as_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

C ≌ D

Interpret a functor that is an equivalence as an equivalence.

Equations

F.as_equivalence = {functor := F, inverse := category_theory.is_equivalence.inverse F _inst_3, unit_iso := category_theory.is_equivalence.unit_iso _inst_3, counit_iso := category_theory.is_equivalence.counit_iso _inst_3, functor_unit_iso_comp' := _}

@[protected, instance]

def category_theory.functor.is_equivalence_refl {C : Type u₁} [category_theory.category C] :

category_theory.is_equivalence (𝟭 C)

Equations

category_theory.functor.is_equivalence_refl = category_theory.is_equivalence.of_equivalence category_theory.equivalence.refl

def category_theory.functor.inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

D ⥤ C

The inverse functor of a functor that is an equivalence.

Equations

F.inv = category_theory.is_equivalence.inverse F

@[protected, instance]

def category_theory.functor.is_equivalence_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

category_theory.is_equivalence F.inv

Equations

F.is_equivalence_inv = category_theory.is_equivalence.of_equivalence F.as_equivalence.symm

@[simp]

theorem category_theory.functor.as_equivalence_functor {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

F.as_equivalence.functor = F

@[simp]

theorem category_theory.functor.as_equivalence_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

F.as_equivalence.inverse = F.inv

@[simp]

theorem category_theory.functor.as_equivalence_unit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} [h : category_theory.is_equivalence F] :

F.as_equivalence.unit_iso = category_theory.is_equivalence.unit_iso

@[simp]

theorem category_theory.functor.as_equivalence_counit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} [category_theory.is_equivalence F] :

F.as_equivalence.counit_iso = category_theory.is_equivalence.counit_iso

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

@[protected, instance]

def category_theory.functor.is_equivalence_trans {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.is_equivalence F] [category_theory.is_equivalence G] :

category_theory.is_equivalence (F ⋙ G)

Equations

F.is_equivalence_trans G = category_theory.is_equivalence.of_equivalence (F.as_equivalence.trans G.as_equivalence)

@[simp]

theorem category_theory.equivalence.functor_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (E : C ≌ D) :

E.functor.inv = E.inverse

@[simp]

theorem category_theory.equivalence.inverse_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (E : C ≌ D) :

E.inverse.inv = E.functor

@[simp]

theorem category_theory.equivalence.functor_as_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (E : C ≌ D) :

E.functor.as_equivalence = E

@[simp]

theorem category_theory.equivalence.inverse_as_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (E : C ≌ D) :

E.inverse.as_equivalence = E.symm

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

F.map (F.inv.map f) = F.as_equivalence.counit.app X ≫ f ≫ F.as_equivalence.counit_inv.app 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) :

F.inv.map (F.map f) = F.as_equivalence.unit_inv.app X ≫ f ≫ F.as_equivalence.unit.app Y

def category_theory.is_equivalence.of_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (e : F ≅ G) (hF : category_theory.is_equivalence F) :

category_theory.is_equivalence 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

category_theory.is_equivalence.of_iso e hF = {inverse := category_theory.is_equivalence.inverse F hF, unit_iso := category_theory.is_equivalence.unit_iso ≪≫ category_theory.nat_iso.hcomp e (category_theory.iso.refl (category_theory.is_equivalence.inverse F)), counit_iso := category_theory.nat_iso.hcomp (category_theory.iso.refl (category_theory.is_equivalence.inverse F)) e.symm ≪≫ category_theory.is_equivalence.counit_iso, functor_unit_iso_comp' := _}

@[simp]

theorem category_theory.is_equivalence.of_iso_counit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (e : F ≅ G) (hF : category_theory.is_equivalence F) :

category_theory.is_equivalence.counit_iso = category_theory.nat_iso.hcomp (category_theory.iso.refl (category_theory.is_equivalence.inverse F)) e.symm ≪≫ category_theory.is_equivalence.counit_iso

@[simp]

theorem category_theory.is_equivalence.of_iso_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (e : F ≅ G) (hF : category_theory.is_equivalence F) :

category_theory.is_equivalence.inverse G = category_theory.is_equivalence.inverse F

@[simp]

theorem category_theory.is_equivalence.of_iso_unit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (e : F ≅ G) (hF : category_theory.is_equivalence F) :

category_theory.is_equivalence.unit_iso = category_theory.is_equivalence.unit_iso ≪≫ category_theory.nat_iso.hcomp e (category_theory.iso.refl (category_theory.is_equivalence.inverse F))

theorem category_theory.is_equivalence.of_iso_trans {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G H : C ⥤ D} (e : F ≅ G) (e' : G ≅ H) (hF : category_theory.is_equivalence F) :

category_theory.is_equivalence.of_iso e' (category_theory.is_equivalence.of_iso e hF) = category_theory.is_equivalence.of_iso (e ≪≫ e') hF

Compatibility of of_iso with the composition of isomorphisms of functors

theorem category_theory.is_equivalence.of_iso_refl {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (hF : category_theory.is_equivalence F) :

category_theory.is_equivalence.of_iso (category_theory.iso.refl F) hF = hF

Compatibility of of_iso with identity isomorphisms of functors

def category_theory.is_equivalence.equiv_of_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (e : F ≅ G) :

category_theory.is_equivalence F ≃ category_theory.is_equivalence G

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

Equations

category_theory.is_equivalence.equiv_of_iso e = {to_fun := category_theory.is_equivalence.of_iso e, inv_fun := category_theory.is_equivalence.of_iso e.symm, left_inv := _, right_inv := _}

@[simp]

theorem category_theory.is_equivalence.equiv_of_iso_symm_apply {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (e : F ≅ G) (hF : category_theory.is_equivalence G) :

⇑((category_theory.is_equivalence.equiv_of_iso e).symm) hF = category_theory.is_equivalence.of_iso e.symm hF

@[simp]

theorem category_theory.is_equivalence.equiv_of_iso_apply {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (e : F ≅ G) (hF : category_theory.is_equivalence F) :

⇑(category_theory.is_equivalence.equiv_of_iso e) hF = category_theory.is_equivalence.of_iso e hF

@[simp]

def category_theory.is_equivalence.cancel_comp_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) (hG : category_theory.is_equivalence G) (hGF : category_theory.is_equivalence (F ⋙ G)) :

category_theory.is_equivalence F

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

Equations

category_theory.is_equivalence.cancel_comp_right F G hG hGF = category_theory.is_equivalence.of_iso (F.associator G G.inv ≪≫ category_theory.nat_iso.hcomp (category_theory.iso.refl F) category_theory.is_equivalence.unit_iso.symm ≪≫ F.right_unitor) ((F ⋙ G).is_equivalence_trans G.inv)

@[simp]

def category_theory.is_equivalence.cancel_comp_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) (hF : category_theory.is_equivalence F) (hGF : category_theory.is_equivalence (F ⋙ G)) :

category_theory.is_equivalence G

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

Equations

category_theory.is_equivalence.cancel_comp_left F G hF hGF = category_theory.is_equivalence.of_iso ((F.inv.associator F G).symm ≪≫ category_theory.nat_iso.hcomp category_theory.is_equivalence.counit_iso (category_theory.iso.refl G) ≪≫ G.left_unitor) (F.inv.is_equivalence_trans (F ⋙ G))

theorem category_theory.equivalence.ess_surj_of_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

category_theory.ess_surj F

An equivalence is essentially surjective.

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

@[protected, instance]

def category_theory.equivalence.faithful_of_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

category_theory.faithful F

An equivalence is faithful.

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

@[protected, instance]

def category_theory.equivalence.full_of_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

category_theory.full F

An equivalence is full.

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

Equations

category_theory.equivalence.full_of_equivalence F = {preimage := λ (X Y : C) (f : F.obj X ⟶ F.obj Y), F.as_equivalence.unit.app X ≫ F.inv.map f ≫ F.as_equivalence.unit_inv.app Y, witness' := _}

noncomputable def category_theory.equivalence.of_fully_faithfully_ess_surj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.full F] [category_theory.faithful F] [category_theory.ess_surj F] :

category_theory.is_equivalence F

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

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

Equations

category_theory.equivalence.of_fully_faithfully_ess_surj F = category_theory.is_equivalence.mk (equivalence_inverse F) (category_theory.nat_iso.of_components (λ (X : C), (category_theory.preimage_iso (F.obj_obj_preimage_iso (F.obj X))).symm) _) (category_theory.nat_iso.of_components F.obj_obj_preimage_iso _)

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

@[protected, instance]

def category_theory.equivalence.ess_surj_induced_functor {D : Type u₂} [category_theory.category D] {C' : Type u_1} (e : C' ≃ D) :

category_theory.ess_surj (category_theory.induced_functor ⇑e)

@[protected, instance]

noncomputable def category_theory.equivalence.induced_functor_of_equiv {D : Type u₂} [category_theory.category D] {C' : Type u_1} (e : C' ≃ D) :

category_theory.is_equivalence (category_theory.induced_functor ⇑e)

Equations

category_theory.equivalence.induced_functor_of_equiv e = category_theory.equivalence.of_fully_faithfully_ess_surj (category_theory.induced_functor ⇑e)

@[protected, instance]

noncomputable def category_theory.equivalence.fully_faithful_to_ess_image {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.full F] [category_theory.faithful F] :

category_theory.is_equivalence F.to_ess_image

Equations

category_theory.equivalence.fully_faithful_to_ess_image F = category_theory.equivalence.of_fully_faithfully_ess_surj F.to_ess_image