-
Notifications
You must be signed in to change notification settings - Fork 297
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
[Merged by Bors] - feat(number_theory): define number fields, function fields and their rings of integers #8701
Conversation
Let `L` be a finite separable extension of `K = Frac(A)`, where `A` is a Dedekind domain. Then `integral_closure A L` is also a Dedekind domain. In combination with the definitions of #8701, we can conclude that rings of integers are Dedekind domains.
Let `L` be a finite separable extension of `K = Frac(A)`, where `A` is a Dedekind domain. Then `integral_closure A L` is also a Dedekind domain. In combination with the definitions of #8701, we can conclude that rings of integers are Dedekind domains.
Let `L` be a finite separable extension of `K = Frac(A)`, where `A` is a Dedekind domain. Then `integral_closure A L` is also a Dedekind domain. In combination with the definitions of #8701, we can conclude that rings of integers are Dedekind domains.
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
6b13304
to
bb57364
Compare
The typeclass `is_integral_closure A R B` states `A` is the integral closure of `R` in `B`, i.e. that an element of `B` is integral over `R` iff it is an element of (the image of) `A`. We also show that any integral extension of `R` contained in `B` is contained in `A`, and the integral closure is unique up to isomorphism. This was suggested in the review of #8701, in order to define a characteristic predicate for rings of integers.
The typeclass `is_integral_closure A R B` states `A` is the integral closure of `R` in `B`, i.e. that an element of `B` is integral over `R` iff it is an element of (the image of) `A`. We also show that any integral extension of `R` contained in `B` is contained in `A`, and the integral closure is unique up to isomorphism. This was suggested in the review of #8701, in order to define a characteristic predicate for rings of integers. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Let `L` be a finite separable extension of `K = Frac(A)`, where `A` is a Dedekind domain. Then `integral_closure A L` is also a Dedekind domain. In combination with the definitions of #8701, we can conclude that rings of integers are Dedekind domains.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-Authored-By: Eric Wieser <wieser.eric@gmail.com>
bb57364
to
129a9b6
Compare
Let `L` be a finite separable extension of `K = Frac(A)`, where `A` is a Dedekind domain. Then `integral_closure A L` is also a Dedekind domain. In combination with the definitions of #8701, we can conclude that rings of integers are Dedekind domains.
Thanks 🎉 bors d+ |
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
src/number_theory/number_field.lean
Outdated
-- The `is_number_field K` hypothesis is not used but is required for | ||
-- this definition to make sense. | ||
@[nolint unused_arguments] |
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.
Shouldn't we leave it out anyway? It would be sufficient to assume it for lemmas, right?
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'm just a bit wary of someone having open function_field number_field
somewhere, trying to get the ring of integers of a function field, and receiving the integral closure of ℤ
instead. Complaining about a missing instance would prevent that issue. But I guess they will notice the issue as soon as they try to prove anything with it.
…DD (#8847) Let `L` be a finite separable extension of `K = Frac(A)`, where `A` is a Dedekind domain. Then any `is_integral_closure C A L` is also a Dedekind domain, in particular for `C := integral_closure A L`. In combination with the definitions of #8701, we can conclude that rings of integers are Dedekind domains.
bors merge |
…rings of integers (#8701) Co-Authored-By: Ashvni <ashvni.n@gmail.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Co-Authored-By: Ashvni ashvni.n@gmail.com
R ≃ R'
, map a basis forR
-moduleM
toR'
-moduleM
#8699