Commit 2025-10-29 00:04 d64be36b

View on Github →

feat(CategoryTheory): Guitart exact squares and Kan extensions (#30382) Given a Guitart exact square w : T ⋙ R ⟶ L ⋙ B, we show that pointwise left Kan extensions along R give, by composition, pointwise left Kan extensions along L.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean

Created Mathlib/CategoryTheory/GuitartExact/KanExtension.lean

added theorem CategoryTheory.Functor.LeftExtension.nonempty_isPointwiseLeftKanExtensionAt_compTwoSquare_iff

added theorem CategoryTheory.TwoSquare.hasLeftKanExtension

added theorem CategoryTheory.TwoSquare.hasPointwiseLeftKanExtension

added theorem CategoryTheory.TwoSquare.hasPointwiseLeftKanExtensionAt_iff

added theorem CategoryTheory.TwoSquare.hasPointwiseLeftKanExtension_iff

Modified Mathlib/CategoryTheory/Limits/Final.lean

added theorem CategoryTheory.Functor.Final.hasColimit_comp_iff

added theorem CategoryTheory.Functor.Initial.hasLimit_comp_iff