Commit 2024-11-15 12:41 0b70c322

View on Github →

feat: colim preserves limits in functor categories (#18521) Together with #18511 this will enable us to commute finite limits with filtered colimits in functor categories.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean

added def CategoryTheory.colimitCompWhiskeringRightIsoColimitComp

added def CategoryTheory.limitCompWhiskeringRightIsoLimitComp

added theorem CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π

added theorem CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_π

added theorem CategoryTheory.whiskerRight_ι_colimitCompWhiskeringRightIsoColimitComp_inv

added theorem CategoryTheory.ι_colimitCompWhiskeringRightIsoColimitComp_hom