Documentation

TauCeti.CategoryTheory.Equivalence.EssImage

Equivalences onto the essential image with a prescribed inverse #

A fully faithful functor L : C ⥤ D is an equivalence onto its essential image (CategoryTheory.Functor.fullyFaithfulToEssImage), but the inverse of L.toEssImage.asEquivalence is chosen. When L is full and admits a retraction R : D ⥤ C, in the sense of a natural isomorphism e : L ⋙ R ≅ 𝟭 C (which makes L faithful), this file constructs the equivalence C ≌ L.EssImageSubcategory whose inverse is R restricted to the essential image and whose unit is e.symm. Its counit is determined by the triangle identities; on objects L.obj X it is L.map (e.hom.app X), by CategoryTheory.Equivalence.counit_app_functor.

This is the shape of the equivalence between a category of coefficients and the free objects on them, whose coefficients are recovered by a retraction: for instance, quasicoherent sheaves and their graded symmetric algebras, with the degree-one component as retraction.

Main declarations #

source
noncomputable def CategoryTheory.Functor.equivEssImageOfCompIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [L.Full] {R : Functor D C} (e : L.comp R ≅ Functor.id C) :
C ≌ L.EssImageSubcategory

A full functor L with a retraction e : L ⋙ R ≅ 𝟭 C, which is then fully faithful, is an equivalence onto its essential image whose inverse is R restricted to the essential image and whose unit is e.symm.

Instances For
    source
    @[simp]
    theorem CategoryTheory.Functor.equivEssImageOfCompIso_functor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [L.Full] {R : Functor D C} (e : L.comp R ≅ Functor.id C) :
    (L.equivEssImageOfCompIso e).functor = L.toEssImage

    The forward functor of equivEssImageOfCompIso is the corestriction of L to its essential image.

    source
    @[simp]
    theorem CategoryTheory.Functor.equivEssImageOfCompIso_inverse {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [L.Full] {R : Functor D C} (e : L.comp R ≅ Functor.id C) :
    (L.equivEssImageOfCompIso e).inverse = L.essImage.ι.comp R

    The inverse functor of equivEssImageOfCompIso is the retraction R restricted to the essential image.

    source
    @[simp]
    theorem CategoryTheory.Functor.equivEssImageOfCompIso_unitIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [L.Full] {R : Functor D C} (e : L.comp R ≅ Functor.id C) :
    (L.equivEssImageOfCompIso e).unitIso = e.symm

    The unit of equivEssImageOfCompIso is the inverse of the retraction isomorphism.

    source
    theorem CategoryTheory.Functor.essImage_iff_nonempty_iso_of_compIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) {R : Functor D C} (e : L.comp R ≅ Functor.id C) (A : D) :
    L.essImage A ↔ Nonempty (L.obj (R.obj A) ≅ A)

    An object lies in the essential image of a functor L with a retraction e : L ⋙ R ≅ 𝟭 C exactly when it is isomorphic to L applied to its image under R.