Theorems · Theorem · category theory

CategoryTheory.Presheaf.preservesColimitsOfSize_of_isLeftKanExtension

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ} [CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (α : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) [L.IsLeftKanExtension α],
  CategoryTheory.Limits.PreservesColimitsOfSize.{v₃, u₃, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L

Any left Kan extension along the Yoneda embedding preserves colimits.

Defined in

Mathlib.CategoryTheory.Limits.Presheaf

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.HasPointwiseLeftKanExtensionCategoryTheory.Functor.IsLeftKanExtension