Commit 2024-11-13 20:45 b24a0708

View on Github →

feat(CategoryTheory): Every colimit is a colimit on the Grothendieck construction on costructured arrows (#18532) Expresses L.lan as a fiberwise colimit and uses this result to transform every colimit into a colimit on the Grothendieck construction on costructured arrows.

Estimated changes

Modified Mathlib/CategoryTheory/Comma/StructuredArrow/Functor.lean

added def CategoryTheory.CostructuredArrow.grothendieckProj

added def CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj

added def CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst

added def CategoryTheory.CostructuredArrow.ιCompGrothendieckProj

Modified Mathlib/CategoryTheory/Functor/Flat.lean

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

added theorem CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grotendieckProj

added theorem CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom

added theorem CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv

deleted theorem CategoryTheory.Functor.ι_lanObjObjIsoColimit_hom

deleted theorem CategoryTheory.Functor.ι_lanObjObjIsoColimit_inv

added theorem CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_hom

added theorem CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_inv

Modified Mathlib/Topology/Sheaves/Presheaf.lean

Modified Mathlib/Topology/Sheaves/Stalks.lean