[Merged by Bors] - feat(ring_theory/fractional_ideal): helper lemmas for Dedekind domains #4994
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
An assortment of lemmas about `fractional_ideal`s, used in the Dedekind domain project. The motivation for creating this PR is that we are planning to remove the general `has_inv` instance on `fractional_ideal` (reserving it only for Dedekind domains), and we don't want to do the resulting refactoring twice. So we make sure everything is in the master branch, do the refactoring there, then merge the changes back into the work in progress branch.
Vierkantor
added
the
awaiting-review
eric-wieser
reviewed
Nov 13, 2020
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Do you mind adding some text to the PR message outlining the specific changes made in this PR? |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Nov 17, 2020
#4994) An assortment of lemmas and refactoring related to `fractional_ideal`s, used in the Dedekind domain project. The motivation for creating this PR is that we are planning to remove the general `has_inv` instance on `fractional_ideal` (reserving it only for Dedekind domains), and we don't want to do the resulting refactoring twice. So we make sure everything is in the master branch, do the refactoring there, then merge the changes back into the work in progress branch. Overview of the changes in `localization.lean`: * more `is_integer` lemmas * a localization of a noetherian ring is noetherian * generalize a few lemmas from integral domains to nontrivial `comm_ring`s * `algebra A (fraction_ring A)` instance Overview of the changes in `fractional_ideal.lean`: * generalize many lemmas from integral domains to (nontrivial) `comm_ring`s (now `R` is notation for a `comm_ring` and `R₁` for an integral domain) * `is_fractional_of_le`, `is_fractional_span_iff` and `is_fractional_of_fg` * many `simp` and `norm_cast` results involving `coe : ideal -> fractional_ideal` and `coe : fractional_ideal -> submodule`: now should be complete for `0`, `1`, `+`, `*`, `/` and `≤`. * use `1 : submodule` as `simp` normal form instead of `coe_submodule (1 : ideal)` * make the multiplication operation irreducible * port `submodule.has_mul` lemmas to `fractional_ideal.has_mul` * `simp` lemmas for `canonical_equiv`, `span_singleton` * many ways to prove `is_noetherian` Co-Authored-By: Ashvni <ashvni.n@gmail.com> Co-Authored-By: faenuccio <filippo.nuccio@univ-st-etienne.fr> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
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.
An assortment of lemmas and refactoring related to
fractional_ideals, used in the Dedekind domain project.The motivation for creating this PR is that we are planning to remove the general
has_invinstance onfractional_ideal(reserving it only for Dedekind domains), and we don't want to do the resulting refactoring twice. So we make sure everything is in the master branch, do the refactoring there, then merge the changes back into the work in progress branch.Overview of the changes in
localization.lean:is_integerlemmascomm_ringsalgebra A (fraction_ring A)instanceOverview of the changes in
fractional_ideal.lean:comm_rings (nowRis notation for acomm_ringandR₁for an integral domain)is_fractional_of_le,is_fractional_span_iffandis_fractional_of_fgsimpandnorm_castresults involvingcoe : ideal -> fractional_idealandcoe : fractional_ideal -> submodule: now should be complete for0,1,+,*,/and≤.1 : submoduleassimpnormal form instead ofcoe_submodule (1 : ideal)submodule.has_mullemmas tofractional_ideal.has_mulsimplemmas forcanonical_equiv,span_singletonis_noetherianCo-Authored-By: Ashvni ashvni.n@gmail.com
Co-Authored-By: faenuccio filippo.nuccio@univ-st-etienne.fr