[Merged by Bors] - feat(group_theory/group_action): generalize is_algebra_tower
#3717
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This PR introduces a new typeclass `is_scalar_tower R M N` stating that scalar multiplications between the three types are compatible: `smul_assoc : ((x : R) • (y : M)) • (z : N) = x • (y • z)`. This typeclass is the general form of `is_algebra_tower`. It also generalizes some of the existing instances of `is_algebra_tower`. I didn't try very hard though, so I might have missed some. Related Zulip discussions: * https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Effect.20of.20changing.20the.20base.20field.20on.20span * https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/pull.20back.20an.20R.20module.20along.20.60S.20-.3E.2B*.20R.60
Vierkantor
added
the
awaiting-review
kckennylau
requested changes
Aug 7, 2020
|
Thanks! |
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
|
Should we merge this before derivations? |
sgouezel
reviewed
Aug 9, 2020
| class is_algebra_tower [comm_semiring R] [comm_semiring S] [semiring A] | ||
| [algebra R S] [algebra S A] [algebra R A] : Prop := | ||
| (smul_assoc : ∀ (x : R) (y : S) (z : A), (x • y) • z = x • (y • z)) | ||
| abbreviation is_algebra_tower [comm_semiring R] [comm_semiring S] [semiring A] |
There was a problem hiding this comment.
Do you really want to keep this abbreviation? It seems simpler to just use is_scalar_tower everywhere.
There was a problem hiding this comment.
I completely agree with this. Working with both names for derivations I already see that having to remember which name is used where is confusing and I do not see the point of having this abbreviation.
|
bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Aug 10, 2020
This PR introduces a new typeclass `is_scalar_tower R M N` stating that scalar multiplications between the three types are compatible: `smul_assoc : ((x : R) • (y : M)) • (z : N) = x • (y • z)`. This typeclass is the general form of `is_algebra_tower`. It also generalizes some of the existing instances of `is_algebra_tower`. I didn't try very hard though, so I might have missed some instances. Related Zulip discussions: * https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Effect.20of.20changing.20the.20base.20field.20on.20span * https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/pull.20back.20an.20R.20module.20along.20.60S.20-.3E.2B*.20R.60
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
is_algebra_toweris_algebra_tower
Vierkantor
added a commit
that referenced
this pull request
Aug 15, 2020
Delete the abbreviation `is_algebra_tower` for `is_scalar_tower`, and replace all references (including the usages of the `is_algebra_tower` namespace) with `is_scalar_tower`. Documentation should also have been updated accordingly. This change was requested in a comment on #3717.
Vierkantor
added a commit
that referenced
this pull request
Aug 15, 2020
Delete the abbreviation `is_algebra_tower` for `is_scalar_tower`, and replace all references (including the usages of the `is_algebra_tower` namespace) with `is_scalar_tower`. Documentation should also have been updated accordingly. This change was requested in a comment on #3717.
bors bot
pushed a commit
that referenced
this pull request
Aug 15, 2020
Delete the abbreviation `is_algebra_tower` for `is_scalar_tower`, and replace all references (including the usages of the `is_algebra_tower` namespace) with `is_scalar_tower`. Documentation should also have been updated accordingly. This change was requested in a comment on #3717. Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR introduces a new typeclass
is_scalar_tower R M Nstating that scalar multiplications between the three types are compatible:smul_assoc : ((x : R) • (y : M)) • (z : N) = x • (y • z).This typeclass is the general form of
is_algebra_tower. It also generalizes some of the existing instances ofis_algebra_tower. I didn't try very hard though, so I might have missed some instances.Related Zulip discussions: