Commit 2024-01-09 22:39 03a46de9

View on Github →

feat(RepresentationTheory/Action): add preservation of (co)limits lemmas for functors into Action V G (#9558) Shows that a functor into Action V G preserves a given (co)limit if it does after postcomposing with the forgetful functor to V.

Estimated changes

Modified Mathlib/RepresentationTheory/Action/Limits.lean

added def Action.preservesColimitOfPreserves

added def Action.preservesColimitsOfShapeOfPreserves

added def Action.preservesColimitsOfSizeOfPreserves

added def Action.preservesLimitOfPreserves

added def Action.preservesLimitsOfShapeOfPreserves

added def Action.preservesLimitsOfSizeOfPreserves