[Merged by Bors] - feat(algebra/smul_regular): add M-regular elements
#6659
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 proves a few injectivity results for (scalar) multiplication in the setting of modules and algebras over a ring.
I am really bad at choosing between `left` and `right` in lemma names :)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…ity/mathlib into adomani_module_regular
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…ity/mathlib into adomani_module_regular
simplify proof of units.is_smul_regular
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This is the second part of PR #6590. It contains the actual API Zulip: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews
github-actions
bot
added
the
blocked-by-other-PR
adomani
added
the
awaiting-review
bors bot
pushed a commit
that referenced
this pull request
Mar 15, 2021
…ce `mul_action_with_zero` and `M`-regular elements (#6590) This PR has been split and there are now two separate PRs. * #6590, this one, introducing `smul_with_zero` and `mul_action_with_zero`: two typeclasses to deal with multiplicative actions of `monoid_with_zero`, without the need to assume the presence of an addition! * #6659, introducing `M`-regular elements, called `smul_regular`: the analogue of `is_left_regular`, but defined for an action of `monoid_with_zero` on a module `M`. This PR is a preparation for introducing `M`-regular elements. From the doc-string: ### Introduce `smul_with_zero` In analogy with the usual monoid action on a Type `M`, we introduce an action of a `monoid_with_zero` on a Type with `0`. In particular, for Types `R` and `M`, both containing `0`, we define `smul_with_zero R M` to be the typeclass where the products `r • 0` and `0 • m` vanish for all `r ∈ R` and all `m ∈ M`. Moreover, in the case in which `R` is a `monoid_with_zero`, we introduce the typeclass `mul_action_with_zero R M`, mimicking group actions and having an absorbing `0` in `R`. Thus, the action is required to be compatible with * the unit of the monoid, acting as the identity; * the zero of the monoid_with_zero, acting as zero; * associativity of the monoid. Next, in a separate file, I introduce `M`-regular elements for a `monoid_with_zero R` with a `mul_action_with_zero` on a module `M`. The definition is simply to require that an element `a : R` is `M`-regular if the smultiplication `M → M`, given by `m ↦ a • m` is injective. We also prove some basic facts about `M`-regular elements. The PR further changes three further the files * `data/polynomial/coeffs`; * `topology/algebra/module.lean`; * `analysis/normed_space/bounded_linear_maps`. The changes are prompted by a failure in CI. In each case, the change was tiny, mostly having to do with an exchange of a multiplication by a smultiplication or vice-versa. Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
github-actions
bot
removed
the
blocked-by-other-PR
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Mar 22, 2021
This PR extends PR #6590, that is now merged. The current PR contains the actual API to work with `M`-regular elements `r : R`, called `is_smul_regular M r`. Zulip: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews From the doc-string: ### Action of regular elements on a module We introduce `M`-regular elements, in the context of an `R`-module `M`. The corresponding predicate is called `is_smul_regular`. There are very limited typeclass assumptions on `R` and `M`, but the "mathematical" case of interest is a commutative ring `R` acting an a module `M`. Since the properties are "multiplicative", there is no actual requirement of having an addition, but there is a zero in both `R` and `M`. Smultiplications involving `0` are, of course, all trivial. The defining property is that an element `a ∈ R` is `M`-regular if the smultiplication map `M → M`, defined by `m ↦ a • m`, is injective. This property is the direct generalization to modules of the property `is_left_regular` defined in `algebra/regular`. Lemma `is_smul_regular.is_left_regular_iff` shows that indeed the two notions coincide. Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
M-regular elementsM-regular elements
b-mehta
pushed a commit
that referenced
this pull request
Apr 2, 2021
…ce `mul_action_with_zero` and `M`-regular elements (#6590) This PR has been split and there are now two separate PRs. * #6590, this one, introducing `smul_with_zero` and `mul_action_with_zero`: two typeclasses to deal with multiplicative actions of `monoid_with_zero`, without the need to assume the presence of an addition! * #6659, introducing `M`-regular elements, called `smul_regular`: the analogue of `is_left_regular`, but defined for an action of `monoid_with_zero` on a module `M`. This PR is a preparation for introducing `M`-regular elements. From the doc-string: ### Introduce `smul_with_zero` In analogy with the usual monoid action on a Type `M`, we introduce an action of a `monoid_with_zero` on a Type with `0`. In particular, for Types `R` and `M`, both containing `0`, we define `smul_with_zero R M` to be the typeclass where the products `r • 0` and `0 • m` vanish for all `r ∈ R` and all `m ∈ M`. Moreover, in the case in which `R` is a `monoid_with_zero`, we introduce the typeclass `mul_action_with_zero R M`, mimicking group actions and having an absorbing `0` in `R`. Thus, the action is required to be compatible with * the unit of the monoid, acting as the identity; * the zero of the monoid_with_zero, acting as zero; * associativity of the monoid. Next, in a separate file, I introduce `M`-regular elements for a `monoid_with_zero R` with a `mul_action_with_zero` on a module `M`. The definition is simply to require that an element `a : R` is `M`-regular if the smultiplication `M → M`, given by `m ↦ a • m` is injective. We also prove some basic facts about `M`-regular elements. The PR further changes three further the files * `data/polynomial/coeffs`; * `topology/algebra/module.lean`; * `analysis/normed_space/bounded_linear_maps`. The changes are prompted by a failure in CI. In each case, the change was tiny, mostly having to do with an exchange of a multiplication by a smultiplication or vice-versa. Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
b-mehta
pushed a commit
that referenced
this pull request
Apr 2, 2021
This PR extends PR #6590, that is now merged. The current PR contains the actual API to work with `M`-regular elements `r : R`, called `is_smul_regular M r`. Zulip: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews From the doc-string: ### Action of regular elements on a module We introduce `M`-regular elements, in the context of an `R`-module `M`. The corresponding predicate is called `is_smul_regular`. There are very limited typeclass assumptions on `R` and `M`, but the "mathematical" case of interest is a commutative ring `R` acting an a module `M`. Since the properties are "multiplicative", there is no actual requirement of having an addition, but there is a zero in both `R` and `M`. Smultiplications involving `0` are, of course, all trivial. The defining property is that an element `a ∈ R` is `M`-regular if the smultiplication map `M → M`, defined by `m ↦ a • m`, is injective. This property is the direct generalization to modules of the property `is_left_regular` defined in `algebra/regular`. Lemma `is_smul_regular.is_left_regular_iff` shows that indeed the two notions coincide. Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <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 extends PR #6590, that is now merged. The current PR contains the actual API to work with
M-regular elementsr : R, calledis_smul_regular M r.Zulip:
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews
From the doc-string:
Action of regular elements on a module
We introduce
M-regular elements, in the context of anR-moduleM. The correspondingpredicate is called
is_smul_regular.There are very limited typeclass assumptions on
RandM, but the "mathematical" case of interestis a commutative ring
Racting an a moduleM. Since the properties are "multiplicative", thereis no actual requirement of having an addition, but there is a zero in both
RandM.Smultiplications involving
0are, of course, all trivial.The defining property is that an element
a ∈ RisM-regular if the smultiplication mapM → M, defined bym ↦ a • m, is injective.This property is the direct generalization to modules of the property
is_left_regulardefined inalgebra/regular. Lemmais_smul_regular.is_left_regular_iffshows that indeed the two notionscoincide.
[*] depended on: #6590 [The earlier PR introduces
smul_with_zeroandmul_action_with_zero.]