[Merged by Bors] - refactor(ring_theory/ideal/*, ring_theory/jacobson): use comm_semiring instead of comm_ring for ideals
#5954
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
eric-wieser
reviewed
Jan 29, 2021
eric-wieser
reviewed
Jan 29, 2021
bryangingechen
added
the
awaiting-review
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Eric, thank you very much for your suggested improvements! |
eric-wieser
reviewed
Jan 29, 2021
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
jcommelin
changed the title
comm_semiring instead of comm_ring for idealscomm_semiring instead of comm_ring for ideals
Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>
Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>
|
Xavier, thank you for your improvements! |
bryangingechen
approved these changes
Jan 31, 2021
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
bryangingechen
added
awaiting-author
eric-wieser
reviewed
Jan 31, 2021
| @@ -84,16 +78,6 @@ theorem eq_top_iff_one : I = ⊤ ↔ (1:α) ∈ I := | |||
| theorem ne_top_iff_one : I ≠ ⊤ ↔ (1:α) ∉ I := | |||
| not_congr I.eq_top_iff_one | |||
|
|
|||
| lemma exists_mem_ne_zero_iff_ne_bot : (∃ p ∈ I, p ≠ (0 : α)) ↔ I ≠ ⊥ := | |||
There was a problem hiding this comment.
At a glance, I'm surprised this isn't true for semirings
There was a problem hiding this comment.
Eric, you are right: below is a proof (the first one that I found) of the "same" result for a submodule of R, when R is a semiring.
However, at the moment, ideal is only defined for a comm_semiring. In fact, I think that what you suggest should be a separate PR, in case it is not already there.
More generally, we should have a "theory" of cyclic modules, i.e. modules generated by a single element, where this result would fit nicely, replacing 1 : R by a generating element of the module.
lemma submodule.ne_top_iff_one {R : Type*} [semiring R]
(J : submodule R R): J ≠ ⊤ ↔ (1:R) ∉ J :=
not_congr ⟨λ a, submodule.eq_top_iff'.mp a 1, λ hx, submodule.ext
(λ x, ⟨λ _, submodule.mem_top, λ xj, by { rw [← mul_one x], exact submodule.smul_mem J x hx }⟩)⟩
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
|
bors r+ |
|
Thanks Bryan, I just told Bors to merge! Eric, you have a point with the |
bors bot
pushed a commit
that referenced
this pull request
Feb 1, 2021
…ng` instead of `comm_ring` for ideals (#5954) This is the second pass at refactoring the definition of `ideal`. I have changed a `comm_ring` assumption to a `comm_semiring` assumption on many of the lemmas in `ring_theory/ideal/basic`. Most implied changes were very simple, with the usual exception of `jacobson`. I also moved out of `jacobson` the lemmas that were left-over from the previous refactor in this sequence. Besides changing such assumptions on other files, many of the lemmas in `ring_theory/ideal/basic` still using `comm_ring` and without explicit subtractions, deal with quotients.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
comm_semiring instead of comm_ring for idealscomm_semiring instead of comm_ring for ideals
b-mehta
pushed a commit
that referenced
this pull request
Apr 2, 2021
…ng` instead of `comm_ring` for ideals (#5954) This is the second pass at refactoring the definition of `ideal`. I have changed a `comm_ring` assumption to a `comm_semiring` assumption on many of the lemmas in `ring_theory/ideal/basic`. Most implied changes were very simple, with the usual exception of `jacobson`. I also moved out of `jacobson` the lemmas that were left-over from the previous refactor in this sequence. Besides changing such assumptions on other files, many of the lemmas in `ring_theory/ideal/basic` still using `comm_ring` and without explicit subtractions, deal with quotients.
adomani
removed
the
awaiting-author
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 is the second pass at refactoring the definition of
ideal. I have changed acomm_ringassumption to acomm_semiringassumption on many of the lemmas inring_theory/ideal/basic. Most implied changes were very simple, with the usual exception ofjacobson.I also moved out of
jacobsonthe lemmas that were left-over from the previous refactor in this sequence.Besides changing such assumptions on other files, many of the lemmas in
ring_theory/ideal/basicstill usingcomm_ringand without explicit subtractions, deal with quotients.