Documentation

Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Left derived functors #

In this file, given a functor F : C ⥤ H, and L : C ⥤ D that is a localization functor for W : MorphismProperty C, we define F.totalLeftDerived L W : D ⥤ H as the right Kan extension of F along L: it is defined if the type class F.HasLeftDerivedFunctor W asserting the existence of a right Kan extension is satisfied. (The name totalLeftDerived is to avoid name-collision with Functor.leftDerived which are the left derived functors in the context of abelian categories.)

Given LF : D ⥤ H and α : L ⋙ RF ⟶ F, we also introduce a type class F.IsLeftDerivedFunctor α W saying that α is a right Kan extension of F along the localization functor L.

(This file was obtained by dualizing the results in the file Mathlib.CategoryTheory.Functor.Derived.RightDerived.)

References #

source
class CategoryTheory.Functor.IsLeftDerivedFunctor {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] :
Prop

A functor LF : D ⥤ H is a left derived functor of F : C ⥤ H if it is equipped with a natural transformation α : L ⋙ LF ⟶ F which makes it a right Kan extension of F along L, where L : C ⥤ D is a localization functor for W : MorphismProperty C.

Instances
    source
    theorem CategoryTheory.Functor.isLeftDerivedFunctor_iff_isRightKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_5} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Category.{u_6, u_5} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] :
    LF.IsLeftDerivedFunctor α W ↔ LF.IsRightKanExtension α
    source
    theorem CategoryTheory.Functor.isLeftDerivedFunctor_iff_of_iso {C : Type u_1} {D : Type u_6} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_6} D] [Category.{u_2, u_3} H] (LF' LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (α' : L.comp LF' ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] (e : LF ≅ LF') (comm : CategoryStruct.comp (L.whiskerLeft e.hom) α' = α) :
    LF.IsLeftDerivedFunctor α W ↔ LF'.IsLeftDerivedFunctor α' W
    source
    noncomputable def CategoryTheory.Functor.leftDerivedLift {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (β : L.comp G ⟶ F) :
    G ⟶ LF

    Constructor for natural transformations to a left derived functor.

    Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Functor.leftDerived_fac {C : Type u_5} {D : Type u_3} {H : Type u_4} [Category.{u_6, u_5} C] [Category.{u_1, u_3} D] [Category.{u_2, u_4} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (β : L.comp G ⟶ F) :
        CategoryStruct.comp (L.whiskerLeft (LF.leftDerivedLift α W G β)) α = β
        source
        @[simp]
        theorem CategoryTheory.Functor.leftDerived_fac_assoc {C : Type u_5} {D : Type u_3} {H : Type u_4} [Category.{u_6, u_5} C] [Category.{u_1, u_3} D] [Category.{u_2, u_4} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (β : L.comp G ⟶ F) {Z : Functor C H} (h : F ⟶ Z) :
        CategoryStruct.comp (L.whiskerLeft (LF.leftDerivedLift α W G β)) (CategoryStruct.comp α h) = CategoryStruct.comp β h
        source
        @[simp]
        theorem CategoryTheory.Functor.leftDerived_fac_app {C : Type u_5} {D : Type u_3} {H : Type u_4} [Category.{u_6, u_5} C] [Category.{u_1, u_3} D] [Category.{u_2, u_4} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (β : L.comp G ⟶ F) (X : C) :
        CategoryStruct.comp ((LF.leftDerivedLift α W G β).app (L.obj X)) (α.app X) = β.app X
        source
        @[simp]
        theorem CategoryTheory.Functor.leftDerived_fac_app_assoc {C : Type u_5} {D : Type u_3} {H : Type u_4} [Category.{u_6, u_5} C] [Category.{u_1, u_3} D] [Category.{u_2, u_4} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (β : L.comp G ⟶ F) (X : C) {Z : H} (h : F.obj X ⟶ Z) :
        CategoryStruct.comp ((LF.leftDerivedLift α W G β).app (L.obj X)) (CategoryStruct.comp (α.app X) h) = CategoryStruct.comp (β.app X) h
        source
        theorem CategoryTheory.Functor.leftDerived_ext {C : Type u_5} {D : Type u_3} {H : Type u_4} [Category.{u_6, u_5} C] [Category.{u_1, u_3} D] [Category.{u_2, u_4} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (γ₁ γ₂ : G ⟶ LF) (hγ : CategoryStruct.comp (L.whiskerLeft γ₁) α = CategoryStruct.comp (L.whiskerLeft γ₂) α) :
        γ₁ = γ₂
        source
        noncomputable def CategoryTheory.Functor.leftDerivedNatTrans {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) :
        LF' ⟶ LF

        The natural transformation LF' ⟶ LF on left derived functors that is induced by a natural transformation F' ⟶ F.

        Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Functor.leftDerivedNatTrans_fac {C : Type u_1} {D : Type u_6} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_6} D] [Category.{u_2, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) :
            CategoryStruct.comp (L.whiskerLeft (LF'.leftDerivedNatTrans LF α' α W τ)) α = CategoryStruct.comp α' τ
            source
            @[simp]
            theorem CategoryTheory.Functor.leftDerivedNatTrans_fac_assoc {C : Type u_1} {D : Type u_6} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_6} D] [Category.{u_2, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) {Z : Functor C H} (h : F ⟶ Z) :
            CategoryStruct.comp (L.whiskerLeft (LF'.leftDerivedNatTrans LF α' α W τ)) (CategoryStruct.comp α h) = CategoryStruct.comp α' (CategoryStruct.comp τ h)
            source
            @[simp]
            theorem CategoryTheory.Functor.leftDerivedNatTrans_app {C : Type u_1} {D : Type u_6} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_6} D] [Category.{u_2, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) (X : C) :
            CategoryStruct.comp ((LF'.leftDerivedNatTrans LF α' α W τ).app (L.obj X)) (α.app X) = CategoryStruct.comp (α'.app X) (τ.app X)
            source
            @[simp]
            theorem CategoryTheory.Functor.leftDerivedNatTrans_app_assoc {C : Type u_1} {D : Type u_6} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_6} D] [Category.{u_2, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) (X : C) {Z : H} (h : F.obj X ⟶ Z) :
            CategoryStruct.comp ((LF'.leftDerivedNatTrans LF α' α W τ).app (L.obj X)) (CategoryStruct.comp (α.app X) h) = CategoryStruct.comp (α'.app X) (CategoryStruct.comp (τ.app X) h)
            source
            @[simp]
            theorem CategoryTheory.Functor.leftDerivedNatTrans_id {C : Type u_5} {D : Type u_1} {H : Type u_3} [Category.{u_6, u_5} C] [Category.{u_4, u_1} D] [Category.{u_2, u_3} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] :
            LF.leftDerivedNatTrans LF α α W (CategoryStruct.id F) = CategoryStruct.id LF
            source
            @[simp]
            theorem CategoryTheory.Functor.leftDerivedNatTrans_comp {C : Type u_1} {D : Type u_5} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_6, u_5} D] [Category.{u_2, u_3} H] (LF'' LF' LF : Functor D H) {F F' F'' : Functor C H} {L : Functor C D} (α'' : L.comp LF'' ⟶ F'') (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] [LF'.IsLeftDerivedFunctor α' W] (τ' : F'' ⟶ F') (τ : F' ⟶ F) :
            CategoryStruct.comp (LF''.leftDerivedNatTrans LF' α'' α' W τ') (LF'.leftDerivedNatTrans LF α' α W τ) = LF''.leftDerivedNatTrans LF α'' α W (CategoryStruct.comp τ' τ)
            source
            @[simp]
            theorem CategoryTheory.Functor.leftDerivedNatTrans_comp_assoc {C : Type u_1} {D : Type u_5} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_6, u_5} D] [Category.{u_2, u_3} H] (LF'' LF' LF : Functor D H) {F F' F'' : Functor C H} {L : Functor C D} (α'' : L.comp LF'' ⟶ F'') (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] [LF'.IsLeftDerivedFunctor α' W] (τ' : F'' ⟶ F') (τ : F' ⟶ F) {Z : Functor D H} (h : LF ⟶ Z) :
            CategoryStruct.comp (LF''.leftDerivedNatTrans LF' α'' α' W τ') (CategoryStruct.comp (LF'.leftDerivedNatTrans LF α' α W τ) h) = CategoryStruct.comp (LF''.leftDerivedNatTrans LF α'' α W (CategoryStruct.comp τ' τ)) h
            source
            noncomputable def CategoryTheory.Functor.leftDerivedNatIso {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] [LF'.IsLeftDerivedFunctor α' W] (τ : F' ≅ F) :
            LF' ≅ LF

            The natural isomorphism LF' ≅ LF on left derived functors that is induced by a natural isomorphism F' ≅ F.

            Equations
              Instances For
                source
                @[simp]
                theorem CategoryTheory.Functor.leftDerivedNatIso_inv {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] [LF'.IsLeftDerivedFunctor α' W] (τ : F' ≅ F) :
                (LF'.leftDerivedNatIso LF α' α W τ).inv = LF.leftDerivedNatTrans LF' α α' W τ.inv
                source
                @[simp]
                theorem CategoryTheory.Functor.leftDerivedNatIso_hom {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] [LF'.IsLeftDerivedFunctor α' W] (τ : F' ≅ F) :
                (LF'.leftDerivedNatIso LF α' α W τ).hom = LF'.leftDerivedNatTrans LF α' α W τ.hom
                source
                @[reducible, inline]
                noncomputable abbrev CategoryTheory.Functor.leftDerivedUnique {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF' LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (α'₂ : L.comp LF' ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] [LF'.IsLeftDerivedFunctor α'₂ W] :
                LF ≅ LF'

                Uniqueness (up to a natural isomorphism) of the left derived functor.

                Equations
                  Instances For
                    source
                    theorem CategoryTheory.Functor.isLeftDerivedFunctor_iff_isIso_leftDerivedLift {C : Type u_5} {D : Type u_3} {H : Type u_4} [Category.{u_6, u_5} C] [Category.{u_1, u_3} D] [Category.{u_2, u_4} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (β : L.comp G ⟶ F) :
                    G.IsLeftDerivedFunctor β W ↔ IsIso (LF.leftDerivedLift α W G β)
                    source
                    class CategoryTheory.Functor.HasLeftDerivedFunctor {C : Type u_1} {H : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} H] (F : Functor C H) (W : MorphismProperty C) :
                    Prop

                    A functor F : C ⥤ H has a left derived functor with respect to W : MorphismProperty C if it has a right Kan extension along W.Q : C ⥤ W.Localization (or any localization functor L : C ⥤ D for W, see hasLeftDerivedFunctor_iff).

                    Instances
                      source
                      theorem CategoryTheory.Functor.hasLeftDerivedFunctor_iff {C : Type u_1} {D : Type u_5} {H : Type u_2} [Category.{u_3, u_1} C] [Category.{u_6, u_5} D] [Category.{u_4, u_2} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] :
                      F.HasLeftDerivedFunctor W ↔ L.HasRightKanExtension F
                      source
                      theorem CategoryTheory.Functor.hasLeftDerivedFunctor_iff_of_iso {C : Type u_1} {H : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} H] {F F' : Functor C H} (e : F ≅ F') (W : MorphismProperty C) :
                      F.HasLeftDerivedFunctor W ↔ F'.HasLeftDerivedFunctor W
                      source
                      theorem CategoryTheory.Functor.HasLeftDerivedFunctor.hasRightKanExtension {C : Type u_1} {D : Type u_5} {H : Type u_2} [Category.{u_3, u_1} C] [Category.{u_6, u_5} D] [Category.{u_4, u_2} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [F.HasLeftDerivedFunctor W] :
                      L.HasRightKanExtension F
                      source
                      theorem CategoryTheory.Functor.HasLeftDerivedFunctor.mk' {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) {W : MorphismProperty C} [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] :
                      F.HasLeftDerivedFunctor W
                      source
                      noncomputable def CategoryTheory.Functor.totalLeftDerived {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [F.HasLeftDerivedFunctor W] :
                      Functor D H

                      Given a functor F : C ⥤ H, and a localization functor L : D ⥤ H for W, this is the left derived functor D ⥤ H of F, i.e. the right Kan extension of F along L.

                      Equations
                        Instances For
                          source
                          noncomputable def CategoryTheory.Functor.totalLeftDerivedCounit {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [F.HasLeftDerivedFunctor W] :
                          L.comp (F.totalLeftDerived L W) ⟶ F

                          The canonical natural transformation L ⋙ F.totalLeftDerived L W ⟶ F.

                          Equations
                            Instances For
                              source
                              instance CategoryTheory.Functor.instIsLeftDerivedFunctorTotalLeftDerivedTotalLeftDerivedCounit {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [F.HasLeftDerivedFunctor W] :
                              (F.totalLeftDerived L W).IsLeftDerivedFunctor (F.totalLeftDerivedCounit L W) W