[Merged by Bors] - feat: additivize equivariance of morphisms of actions#19171
[Merged by Bors] - feat: additivize equivariance of morphisms of actions#19171AntoineChambert-Loir wants to merge 11 commits intomasterfrom
Conversation
PR summary 41ce244be7Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks! This is really necessary work
|
bot fix style |
|
|
||
| /-- `φ`-equivariant functions `X → Y`, | ||
| where `φ : M → N`, where `M` and `N` act additively on `X` and `Y` respectively -/ | ||
| notation:25 (name := «AddActionHomLocal≺») X " →ₑ[" φ:25 "] " Y:0 => AddActionHom φ X Y |
There was a problem hiding this comment.
This notation is the same as the multiplicative one, right? Surely that's not desirable!
There was a problem hiding this comment.
(and if it is, it should come with a comment explaining why this isn't an issue)
I think you run into trouble when φ = id (PUnit), for instance; but maybe these cases are rare enough that you can make people use the AddActionHom spelling in that case.
There was a problem hiding this comment.
The issue is:
- finding a new notation (and I don't know which one to choose, that would be remembered and make sense at first sight, and is not too heavy), I had proposed
_evwhich Yaël didn't like so much. - having a duplicate notation which will rarely lead into confusion.
There was a problem hiding this comment.
Can you add a comment explaining that the notation is actually the same? Personally I think it is OK, and we can at least give a try.
There was a problem hiding this comment.
it is said so in the header of the file, but I will add something here.
|
bot fix style |
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
|
LGTM, @eric-wieser what do you think? |
YaelDillies
left a comment
There was a problem hiding this comment.
Looks good to me, thanks! @Eric Wieser ?
maintainer merge?
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
Let's merge this, we can always change the notation if we realize it is a bad idea. bors merge |
Additivize the definition of equivariant morphisms with respect to multiplicative actions. The notation introduced is `X →ₑᵥ[φ] Y` for equivariant morphisms, and `X →ᵥ[M] Y` when the underlying map is identity. The goal is to be able to fully additivize the properties of blocks for actions and the definition of primitive actions in #12052 Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
Additivize the definition of equivariant morphisms with respect to multiplicative actions.
The notation introduced is
X →ₑᵥ[φ] Yfor equivariant morphisms, andX →ᵥ[M] Ywhen theunderlying map is identity.
The goal is to be able to fully additivize the properties of blocks for actions and the definition
of primitive actions in #12052