Theorems · Definition · category theory

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.compTwoSquare

{C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        {D : Type u₅} →
          [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
            [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} D] →
                    {T : CategoryTheory.Functor C₁ C₂} →
                      {L : CategoryTheory.Functor C₁ C₃} →
                        {R : CategoryTheory.Functor C₂ C₄} →
                          {B : CategoryTheory.Functor C₃ C₄} →
                            {F : CategoryTheory.Functor C₂ D} →
                              {E : R.LeftExtension F} →
                                E.IsPointwiseLeftKanExtension →
                                  (w : CategoryTheory.TwoSquare T L R B) →
                                    [w.GuitartExact] → (E.compTwoSquare w).IsPointwiseLeftKanExtension

If w : TwoSquare T L R B is a Guitart exact square, and E is a pointwise left Kan extension of F along R, then E.compTwoSquare w is a pointwise left Kan extension of T ⋙ F along L.

Defined in

Mathlib.CategoryTheory.GuitartExact.KanExtension

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.TwoSquare.GuitartExact