[Merged by Bors] - feat(RepresentationTheory/Action): add more limit properties of Action V G and Action.forget V G
#9603
Conversation
chrisflav
added
awaiting-review
| @@ -40,6 +40,11 @@ instance [HasFiniteLimits V] : HasFiniteLimits (Action V G) where | |||
| instance [HasLimits V] : HasLimits (Action V G) := | |||
| Adjunction.has_limits_of_equivalence (Action.functorCategoryEquivalence _ _).functor | |||
|
|
|||
| /-- If `V` has limits of shape `J`, so does `Action V G`.-/ | |||
| lemma hasLimitsOfShapeOfHasLimitsOfShape {J : Type w₁} [Category.{w₂} J] [HasLimitsOfShape J V] : | |||
There was a problem hiding this comment.
I think this can be made an instance (with a slightly simpler name), and similarly for colimits:
| lemma hasLimitsOfShapeOfHasLimitsOfShape {J : Type w₁} [Category.{w₂} J] [HasLimitsOfShape J V] : | |
| instance hasLimitsOfShape {J : Type w₁} [Category.{w₂} J] [HasLimitsOfShape J V] : |
There was a problem hiding this comment.
This was an instance originally (see the first commit in this PR), but it caused a instance synthesization timeout in Mathlib.RepresentationTheory.FdRep at HasKernels (FdRep k G) (see: https://github.com/leanprover-community/mathlib4/actions/runs/7468254528/job/20323323137). Bumping the maximum number of heartbeats there to 50000 fixed it, but I was not sure whether this is desirable. Maybe this can be circumvented by adding some more auxiliary instances in the FdRep file to make the instance search faster?
There was a problem hiding this comment.
I have tried to investigate this. I have just pushed this 8c5c763 which seems to fix the problem.
joelriou
added
awaiting-author
chrisflav
added
awaiting-review
|
Thanks! bors merge |
github-actions
bot
added
ready-to-merge
…on V G` and `Action.forget V G` (#9603) Adds instances on limit properties of `Action V G` and `Action.forget V G`. Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Action V G and Action.forget V GAction V G and Action.forget V G
…on V G` and `Action.forget V G` (#9603) Adds instances on limit properties of `Action V G` and `Action.forget V G`. Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Adds instances on limit properties of
Action V GandAction.forget V G.