[Merged by Bors] - feat(ring_theory/localization): integral closure in field extension #3096

Vierkantor · 2020-06-17T12:38:04Z

Let A be an integral domain with field of fractions K and L a finite extension of K. This PR shows the integral closure of A in L has fraction field L. If those definitions existed, the corollary is that the ring of integers of a number field is a number ring.

For this, we need two constructions on polynomials:

If p is a nonzero polynomial, integral_normalization p is a monic polynomial with roots z * a for z a root of p and a the leading coefficient of p
If f is the localization map from A to K and p has coefficients in K, then f.integer_normalization p is a polynomial with coefficients in A (think: ∀ i, is_integer (f.integer_normalization p).coeff i) with the same roots as p.

src/ring_theory/algebraic.lean

src/data/polynomial.lean

alexjbest · 2020-06-18T15:03:31Z

Cool! I'm not sure I like the name to_monic though, I fear people might use it when they want to normalize f by dividing by the leading term (over a field say).
I can't really think of a better one though, maybe something like integral_roots_normalization? In the context of the classical rational root theorem that's exactly what it does, rescales the roots so they lie in the integers.

Vierkantor · 2020-06-18T15:17:38Z

A more descriptive name can't hurt! Perhaps to_base_ring should then be renamed to integer_coeff_normalization?

ChrisHughes24 · 2020-06-21T17:34:22Z

src/data/polynomial.lean

+begin
+  convert (show eval₂ g x (C s * p) = g s * eval₂ g x p, by rw [eval₂_mul, eval₂_C]),
+  ext,
+  rw [coeff_smul, coeff_C_mul]


Can you extract the lemma s • p = C s * p?

I found a lemma C_mul' : C s * p = s • p and used that one. Should it become a simp lemma (in either direction)?

To me it's not clear which side is simp normal form.

src/data/polynomial.lean

Vierkantor · 2020-06-22T08:44:21Z

Cool! I'm not sure I like the name to_monic though, I fear people might use it when they want to normalize f by dividing by the leading term (over a field say).
I can't really think of a better one though, maybe something like integral_roots_normalization? In the context of the classical rational root theorem that's exactly what it does, rescales the roots so they lie in the integers.

In the end, I renamed it to integral_normalization because the other name was too long. Alternative suggestions are welcome.

jcommelin

@ChrisHughes24 Shall we merge this? I'm happy with the new names.

ChrisHughes24 · 2020-06-24T08:31:13Z

bors merge

…3096) Let `A` be an integral domain with field of fractions `K` and `L` a finite extension of `K`. This PR shows the integral closure of `A` in `L` has fraction field `L`. If those definitions existed, the corollary is that the ring of integers of a number field is a number ring. For this, we need two constructions on polynomials: * If `p` is a nonzero polynomial, `integral_normalization p` is a monic polynomial with roots `z * a` for `z` a root of `p` and `a` the leading coefficient of `p` * If `f` is the localization map from `A` to `K` and `p` has coefficients in `K`, then `f.integer_normalization p` is a polynomial with coefficients in `A` (think: `∀ i, is_integer (f.integer_normalization p).coeff i`) with the same roots as `p`.

bors · 2020-06-24T08:38:00Z

Build failed:

Build mathlib

sgouezel · 2020-06-24T08:38:55Z

bors r-

…leading_coeff` times as big as the original roots

… of fractions

…denominators

Co-Authored-By: Johan Commelin <johan@commelin.net>

Co-Authored-By: Chris Hughes <chrishughes24@gmail.com>

Vierkantor · 2020-06-24T08:51:12Z

Looks like mul_ne_zero got renamed right after my last rebase on master, fixed. The files in this PR build again, let's see what CI thinks of the rest.

robertylewis · 2020-06-24T09:30:33Z

bors r+

…3096) Let `A` be an integral domain with field of fractions `K` and `L` a finite extension of `K`. This PR shows the integral closure of `A` in `L` has fraction field `L`. If those definitions existed, the corollary is that the ring of integers of a number field is a number ring. For this, we need two constructions on polynomials: * If `p` is a nonzero polynomial, `integral_normalization p` is a monic polynomial with roots `z * a` for `z` a root of `p` and `a` the leading coefficient of `p` * If `f` is the localization map from `A` to `K` and `p` has coefficients in `K`, then `f.integer_normalization p` is a polynomial with coefficients in `A` (think: `∀ i, is_integer (f.integer_normalization p).coeff i`) with the same roots as `p`.

bors · 2020-06-24T10:03:47Z

Pull request successfully merged into master.

Build succeeded:

…eanprover-community#3096) Let `A` be an integral domain with field of fractions `K` and `L` a finite extension of `K`. This PR shows the integral closure of `A` in `L` has fraction field `L`. If those definitions existed, the corollary is that the ring of integers of a number field is a number ring. For this, we need two constructions on polynomials: * If `p` is a nonzero polynomial, `integral_normalization p` is a monic polynomial with roots `z * a` for `z` a root of `p` and `a` the leading coefficient of `p` * If `f` is the localization map from `A` to `K` and `p` has coefficients in `K`, then `f.integer_normalization p` is a polynomial with coefficients in `A` (think: `∀ i, is_integer (f.integer_normalization p).coeff i`) with the same roots as `p`.

Vierkantor added the awaiting-review The author would like community review of the PR label Jun 17, 2020

Vierkantor added this to In progress in Basic arithmetic of number fields via automation Jun 17, 2020

jcommelin reviewed Jun 17, 2020

View reviewed changes

src/ring_theory/algebraic.lean Outdated Show resolved Hide resolved

jcommelin assigned ChrisHughes24 Jun 17, 2020

ChrisHughes24 reviewed Jun 17, 2020

View reviewed changes

src/data/polynomial.lean Outdated Show resolved Hide resolved

ChrisHughes24 reviewed Jun 21, 2020

View reviewed changes

Vierkantor force-pushed the integral_closure_in_field_extension branch from df93930 to c59842d Compare June 22, 2020 08:41

jcommelin reviewed Jun 24, 2020

View reviewed changes

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jun 24, 2020

Vierkantor and others added 13 commits June 24, 2020 08:46

polynomial.to_monic gives a monic polynomial with roots exactly `f.…

6bbcb47

…leading_coeff` times as big as the original roots

Show that an algebraic element has a multiple which is integral

55970d4

The field in which we take an integral closure is the closure's field…

f81b76f

… of fractions

A field extension is algebraic if it is finite

00b0f9b

localization_map.to_base_ring p is the polynomial p with cleared …

e12fd9c

…denominators

The fraction field of the integral closure in a finite field extension

f5208ba

Make finite_dimensional K L a typeclass argument

36d1be4

Co-Authored-By: Johan Commelin <johan@commelin.net>

Fix linting errors

684645e

Use eval₂_mul to prove eval₂_smul

2fe6d48

Use ne_zero instead of nonzero to express ≠ 0

b72dd2c

Co-Authored-By: Chris Hughes <chrishughes24@gmail.com>

Use C_mul' to show s • p = C s * p

3e973d2

Rename to_monic to integral_normalization

98650bf

Rename to_base_ring to integer_normalization

0a161a5

Update mul_ne_zero' -> mul_ne_zero

509cb0e

Vierkantor force-pushed the integral_closure_in_field_extension branch from c59842d to 509cb0e Compare June 24, 2020 08:50

bors bot changed the title ~~feat(ring_theory/localization): integral closure in field extension~~ [Merged by Bors] - feat(ring_theory/localization): integral closure in field extension Jun 24, 2020

bors bot closed this Jun 24, 2020

Basic arithmetic of number fields automation moved this from In progress to Done Jun 24, 2020

bryangingechen deleted the integral_closure_in_field_extension branch June 24, 2020 14:20

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(ring_theory/localization): integral closure in field extension #3096

[Merged by Bors] - feat(ring_theory/localization): integral closure in field extension #3096

Vierkantor commented Jun 17, 2020 •

edited

Loading

alexjbest commented Jun 18, 2020

Vierkantor commented Jun 18, 2020

ChrisHughes24 Jun 21, 2020

Vierkantor Jun 22, 2020

jcommelin Jun 22, 2020

Vierkantor commented Jun 22, 2020

jcommelin left a comment

ChrisHughes24 commented Jun 24, 2020

bors bot commented Jun 24, 2020

sgouezel commented Jun 24, 2020

Vierkantor commented Jun 24, 2020

robertylewis commented Jun 24, 2020

bors bot commented Jun 24, 2020

[Merged by Bors] - feat(ring_theory/localization): integral closure in field extension #3096

[Merged by Bors] - feat(ring_theory/localization): integral closure in field extension #3096

Conversation

Vierkantor commented Jun 17, 2020 • edited Loading

alexjbest commented Jun 18, 2020

Vierkantor commented Jun 18, 2020

ChrisHughes24 Jun 21, 2020

Choose a reason for hiding this comment

Vierkantor Jun 22, 2020

Choose a reason for hiding this comment

jcommelin Jun 22, 2020

Choose a reason for hiding this comment

Vierkantor commented Jun 22, 2020

jcommelin left a comment

Choose a reason for hiding this comment

ChrisHughes24 commented Jun 24, 2020

bors bot commented Jun 24, 2020

sgouezel commented Jun 24, 2020

Vierkantor commented Jun 24, 2020

robertylewis commented Jun 24, 2020

bors bot commented Jun 24, 2020

Vierkantor commented Jun 17, 2020 •

edited

Loading