-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(ring_theory): Fractional ideals #2062
feat(ring_theory): Fractional ideals #2062
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice work! Thanks for this PR!
variables (R : Type u) [integral_domain R] (S : set R) [is_submonoid S] | ||
|
||
/-- A submodule `I` is a fractional ideal if `a I ⊆ R` for some `a ≠ 0`. -/ | ||
def is_fractional (I : submodule R (localization R S)) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
When it comes to applying this theory, this definition would benefit enormously from using a characteristic predicate for localisations. For example, it will now be hard (i.e. impossible) to talk about fractional ideals in rat
wrt to int
. Because rat
is not of the form localization int _
.
@101damnations is working on bringing this characteristic predicate to mathlib. I hope that these two PR will play well together.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I expect that changing localization ℤ (non_zero_divisors ℤ)
to, let's say a typeclass has_localization ℤ ℚ
, shouldn't have too much impact on this PR, since most of it is only concerned with is_integer
and its lemmas.
Co-Authored-By: Scott Morrison <scott@tqft.net>
(but both reduce to reflexivity anyway)
Since that is how the definition of `I / J` is traditionally done, but it is not as convenient to work with, I didn't change the definition but added a lemma stating the two are equivalent
(it got broken because I merged changes incorrectly)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
* Some WIP work on fractional ideals * Fill in the `sorry` * A lot of instances for fractional_ideal * Show that an invertible fractional ideal `I` has inverse `1 : I` * Cleanup and documentation * Move `has_div submodule` to algebra_operations * More cleanup and documentation * Explain the `non_zero_divisors R` in the `quotient` section * whitespace Co-Authored-By: Scott Morrison <scott@tqft.net> * `has_inv` instance for `fractional_ideal` * `set.univ.image` -> `set.range` * Fix: `mem_div_iff.mpr` should be `mem_div_iff.mp` (but both reduce to reflexivity anyway) * Add `mem_div_iff_smul_subset` Since that is how the definition of `I / J` is traditionally done, but it is not as convenient to work with, I didn't change the definition but added a lemma stating the two are equivalent * whitespace again (it got broken because I merged changes incorrectly) * Fix unused argument to `inv_nonzero` Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
* Some WIP work on fractional ideals * Fill in the `sorry` * A lot of instances for fractional_ideal * Show that an invertible fractional ideal `I` has inverse `1 : I` * Cleanup and documentation * Move `has_div submodule` to algebra_operations * More cleanup and documentation * Explain the `non_zero_divisors R` in the `quotient` section * whitespace Co-Authored-By: Scott Morrison <scott@tqft.net> * `has_inv` instance for `fractional_ideal` * `set.univ.image` -> `set.range` * Fix: `mem_div_iff.mpr` should be `mem_div_iff.mp` (but both reduce to reflexivity anyway) * Add `mem_div_iff_smul_subset` Since that is how the definition of `I / J` is traditionally done, but it is not as convenient to work with, I didn't change the definition but added a lemma stating the two are equivalent * whitespace again (it got broken because I merged changes incorrectly) * Fix unused argument to `inv_nonzero` Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
This PR defines fractional ideals of an integral domain and proves basic facts about them: they have a
comm_semiring
structure,lattice
structure and ideal quotient; the inverse of an ideal, if it exists, is equal to the quotient. These is the work in progress I mentioned on Zulip.The things that are called "fractional ideal of
R
" in algebraic number theory are calledfractional_ideal R (non_zero_divisors R)
in this file, a notation that probably deserves to be shorter. Do you happen to know a good abbreviation? Alternatively: Is there a good namefoo
forfractional_ideal
so that we can abbreviatefractional_ideal R := foo R (non_zero_divisors R)
?TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list