Commit 2025-05-02 13:41 fe901a50

View on Github →

chore(CategoryTheory/Action): generalize universes (#24547) Since #21652 the universe restrictions are no longer necessary. This also allows to remove some universe restrictions in the Galois category API.

Estimated changes

Modified Mathlib/CategoryTheory/Action/Basic.lean

modified def Action.res

modified def Action.resComp

modified def Action.resId

modified def Action.ρAut

modified theorem Action.ρ_one

modified structure Action

modified def CategoryTheory.Functor.mapAction

Modified Mathlib/CategoryTheory/Action/Concrete.lean

modified def Action.FintypeCat.ofMulAction

modified theorem Action.FintypeCat.ofMulAction_apply

modified def Action.diagonalOneIsoLeftRegular

modified def Action.ofMulAction

modified theorem Action.ofMulAction_apply

Modified Mathlib/CategoryTheory/Action/Continuous.lean

Modified Mathlib/CategoryTheory/Action/Limits.lean

modified def Action.abelianAux

modified theorem Action.preservesColimit_of_preserves

modified theorem Action.preservesColimitsOfShape_of_preserves

modified theorem Action.preservesLimit_of_preserves

modified theorem Action.preservesLimitsOfShape_of_preserves

Modified Mathlib/CategoryTheory/Action/Monoidal.lean

Modified Mathlib/CategoryTheory/Galois/Action.lean

Modified Mathlib/CategoryTheory/Galois/Full.lean

Modified Mathlib/RepresentationTheory/Rep.lean