[Merged by Bors] - feat(group_theory/group_action): define distrib_smul and smul_zero_class
#16123
Conversation
…_class` These are two new superclasses of `distrib_mul_action` that get rid of the `mul_action` part: * `smul_zero_class` is `has_smul` + `a • 0 = 0` * `distrib_smul` is `smul_zero_class` + `a • (x + y) = a • x + a • y`. The motivation for these classes is to instantiate `qsmul` on `splitting_field`: in general scalar multiplication with rational numbers is not a `distrib_mul_action` but it is a `distrib_smul`, and `distrib_smul` is sufficient to lift an action to the `splitting_field`. I set up both `distrib_mul_action` and `smul_with_zero` to be subclasses of the above classes, and unify `smul_zero` (depending on `distrib_mul_action`) and `smul_zero'` (depending on `smul_with_zero`) into one lemma. There are a few places where I need to help the elaborator because e.g. it's expecting `units.mk0 a ha • 0 = 0` (with `smul` coming from `distrib_mul_action`) and getting `a • 0 = 0` (with `smul` coming from `smul_zero_class`). Apparently having both the type and instance differ is too hard for the unifier. Because we don't have definitional eta for structures yet, setting up the inheritance is a bit more tricky than you might think; I added an `example` test case to ensure everything stays OK.
Vierkantor
added
awaiting-review
|
I would have expected |
I would expect the same, but that is how the |
There was a problem hiding this comment.
lgtm in general, there's some todos that feel out of scope for this PR but I think should be noted:
- replace some uses of
smul_with_zerotosmul_zero_class(e.g. unitization'scoe_smul) as the requirements are now overly strong make pi/prod instances(although I see there is some in group_theory/group_action/pi - why do we have different files for this? is it import issues? [the old ones seem to be in algebra/module/pi])
I already added instances for |
This PR builds on #16123 by adding `distrib_smul` (and `smul_zero_class`) instances for: * `finsupp` * `add_monoid_algebra` * `polynomial` * submodule quotients * scalar multiplication by `ℚ` It also generalizes some results by weakening `distrib_mul_action` to `distrib_smul`. The choice of instances and generalizations is based on which are necessary to solve instance diamonds in `splitting_field`, so I probably missed a lot of additional changes. Since I'm not so interested in generalizing everything at the moment, I'd rather leave missing instances to follow-up PRs.
|
I followed up with some generalizations and additional instances in #16132, at least the ones we needed for the splitting field diamond. |
This PR builds on #16123 by adding `distrib_smul` (and `smul_zero_class`) instances for: * `finsupp` * `add_monoid_algebra` * `polynomial` * submodule quotients * scalar multiplication by `ℚ` It also generalizes some results by weakening `distrib_mul_action` to `distrib_smul`. The choice of instances and generalizations is based on which are necessary to solve instance diamonds in `splitting_field`, so I probably missed a lot of additional changes. Since I'm not so interested in generalizing everything at the moment, I'd rather leave missing instances to follow-up PRs.
|
I'm having trouble dealing with the timeouts indicated by the slow-instances linter: it appears this PR doesn't really add to the search space much (there's definitely no recursive instances) so the only explanation is that the space is now just barely big enough to cause linter timeouts. It's not an actual timeout BTW: |
|
aren't we allowed to bump the linters' timeout in this case? |
|
I think I was the last one to bump this timeout so while I think it's fine, it's good to have someone else back me up on this :) |
|
According to binary search, looks like the correct timeout values would be about 27000 for |
|
The issue with the linter was hard to track down, right? I'll try investigate a little in a couple days if you don't know what it is, Anne |
I don't really understand this timeout beyond that the circumstances suggest slow unification within types. I can't really dedicate a lot of time to my PRs in the coming weeks, so please investigate if you have some time! |
github-actions
bot
removed
the
awaiting-CI
|
Sorry for not keeping this PR maintained and thanks for the fixes! |
|
This LGTM! I think we should merge master to see if it is still OK and then it is ready to go unless someone has an argument against it. |
|
Thanks! bors merge |
github-actions
bot
added
ready-to-merge
…_class` (#16123) These are two new superclasses of `distrib_mul_action` that get rid of the `mul_action` part: * `smul_zero_class` is `has_smul` + `a • 0 = 0` * `distrib_smul` is `smul_zero_class` + `a • (x + y) = a • x + a • y`. The motivation for these classes is to instantiate `qsmul` on `splitting_field`: in general scalar multiplication with rational numbers is not a `distrib_mul_action` but it is a `distrib_smul`, and `distrib_smul` is sufficient to lift an action to the `splitting_field`. I set up both `distrib_mul_action` and `smul_with_zero` to be subclasses of the above classes, and unify `smul_zero` (depending on `distrib_mul_action`) and `smul_zero'` (depending on `smul_with_zero`) into one lemma. There are a few places where I need to help the elaborator because e.g. it's expecting `units.mk0 a ha • 0 = 0` (with `smul` coming from `distrib_mul_action`) and getting `a • 0 = 0` (with `smul` coming from `smul_zero_class`). Apparently having both the type and instance differ is too hard for the unifier. Because we don't have definitional eta for structures yet, setting up the inheritance is a bit more tricky than you might think; I added an `example` test case to ensure everything stays OK. Co-authored-by: Mauricio Collares <mauricio@collares.org> Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
distrib_smul and smul_zero_classdistrib_smul and smul_zero_class
This PR builds on #16123 by adding `distrib_smul` (and `smul_zero_class`) instances for: * `finsupp` * `add_monoid_algebra` * `polynomial` * submodule quotients * scalar multiplication by `ℚ` It also generalizes some results by weakening `distrib_mul_action` to `distrib_smul`. The choice of instances and generalizations is based on which are necessary to solve instance diamonds in `splitting_field`, so I probably missed a lot of additional changes. Since I'm not so interested in generalizing everything at the moment, I'd rather leave missing instances to follow-up PRs.
…_class` (#16123) These are two new superclasses of `distrib_mul_action` that get rid of the `mul_action` part: * `smul_zero_class` is `has_smul` + `a • 0 = 0` * `distrib_smul` is `smul_zero_class` + `a • (x + y) = a • x + a • y`. The motivation for these classes is to instantiate `qsmul` on `splitting_field`: in general scalar multiplication with rational numbers is not a `distrib_mul_action` but it is a `distrib_smul`, and `distrib_smul` is sufficient to lift an action to the `splitting_field`. I set up both `distrib_mul_action` and `smul_with_zero` to be subclasses of the above classes, and unify `smul_zero` (depending on `distrib_mul_action`) and `smul_zero'` (depending on `smul_with_zero`) into one lemma. There are a few places where I need to help the elaborator because e.g. it's expecting `units.mk0 a ha • 0 = 0` (with `smul` coming from `distrib_mul_action`) and getting `a • 0 = 0` (with `smul` coming from `smul_zero_class`). Apparently having both the type and instance differ is too hard for the unifier. Because we don't have definitional eta for structures yet, setting up the inheritance is a bit more tricky than you might think; I added an `example` test case to ensure everything stays OK. Co-authored-by: Mauricio Collares <mauricio@collares.org> Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
This PR builds on #16123 by adding `distrib_smul` (and `smul_zero_class`) instances for: * `finsupp` * `add_monoid_algebra` * `polynomial` * submodule quotients * scalar multiplication by `ℚ` It also generalizes some results by weakening `distrib_mul_action` to `distrib_smul`. The choice of instances and generalizations is based on which are necessary to solve instance diamonds in `splitting_field`, so I probably missed a lot of additional changes. Since I'm not so interested in generalizing everything at the moment, I'd rather leave missing instances to follow-up PRs. Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
These are two new superclasses of
distrib_mul_actionthat get rid of themul_actionpart:smul_zero_classishas_smul+a • 0 = 0distrib_smulissmul_zero_class+a • (x + y) = a • x + a • y.The motivation for these classes is to instantiate
qsmulonsplitting_field: in general scalar multiplication with rational numbers is not adistrib_mul_actionbut it is adistrib_smul, anddistrib_smulis sufficient to lift an action to thesplitting_field.I set up both
distrib_mul_actionandsmul_with_zeroto be subclasses of the above classes, and unifysmul_zero(depending ondistrib_mul_action) andsmul_zero'(depending onsmul_with_zero) into one lemma.There are a few places where I need to help the elaborator because e.g. it's expecting
units.mk0 a ha • 0 = 0(withsmulcoming fromdistrib_mul_action) and gettinga • 0 = 0(withsmulcoming fromsmul_zero_class). Apparently having both the type and instance differ is too hard for the unifier. Because we don't have definitional eta for structures yet, setting up the inheritance is a bit more tricky than you might think; I added anexampletest case to ensure everything stays OK.