Theorems · Definition · category theory

CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsoOfIsLocalization

{C : Type u₁} →
  {D : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            {F : CategoryTheory.Functor C H} →
              {L : CategoryTheory.Functor C D} →
                (W : CategoryTheory.MorphismProperty C) →
                  {G : CategoryTheory.Functor D H} →
                    (e : F ≅ L.comp G) →
                      [L.IsLocalization W] →
                        (CategoryTheory.Functor.LeftExtension.mk G e.hom).IsPointwiseLeftKanExtension

If L is a localization functor for W and e : F ≅ L ⋙ G is an isomorphism, then e.hom makes G a pointwise left Kan extension of F along L.

Defined in

Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Cited by

2 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalization