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 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 (whiskerLeft L 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 (whiskerLeft L (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 (whiskerLeft L (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 (whiskerLeft L γ₁) α = CategoryStruct.comp (whiskerLeft L γ₂) α) :
      γ₁ = γ₂
      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 (whiskerLeft L (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 (whiskerLeft L (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