[Merged by Bors] - feat(ring_theory/localization): Localizations of integral extensions #3942

dtumad · 2020-08-25T23:59:00Z

The main definition is the algebra induced by localization at an algebra. Given an algebra R → S and a submonoid M of R, as well as localization maps f : R → Rₘ and g : S → Sₘ, there is a natural algebra Rₘ → Sₘ that makes the entire square commute, and this is defined as localization_algebra.

The two main theorems are similar but distinct statements about integral elements and localizations:

is_integral_localization_at_leading_coeff says that if an element x is algebraic over algebra R S, then if we localize to a submonoid containing the leading coefficient the image of x will be integral.
is_integral_localization says that if R → S is an integral extension, then the algebra induced by localizing at any particular submonoid will be an integral extension.

Both of the proofs of these statements are very simple to explain in words, but fiddling with the polynomial evaluations makes the proofs much larger. I pulled out a lot of lemmas to shorten them, but there is still a decent amount of the proofs that's just manipulating ring elements, and ring doesn't seem quite strong enough to figure it out.

Vierkantor

Thanks 🎉

src/data/finsupp/basic.lean

src/data/polynomial/eval.lean

src/data/polynomial/monic.lean

src/ring_theory/localization.lean

Vierkantor · 2020-08-26T11:09:38Z

src/ring_theory/integral_closure.lean

+theorem is_integral_of_is_integral_mul_unit {x y : A} {r : R} (hr : (algebra_map R A r) * y = 1)
+  (hx : is_integral R (x * y)) : (is_integral R x) :=
+begin
+  by_cases triv : (1 : R) = 0,
+  { exact ⟨0, ⟨trans leading_coeff_zero triv.symm, eval₂_zero _ _⟩⟩ },
+  haveI : nontrivial R := nontrivial_of_ne 1 0 triv,
+  obtain ⟨p, ⟨p_monic, hp⟩⟩ := hx,
+  let p' : polynomial R := ∑ (i : ℕ) in p.support, monomial i ((p.coeff i) * r ^ (p.nat_degree - i)),
+  have hp' : p'.nat_degree = p.nat_degree,
+  { refine finset_sum_monomial_degree (λ h, triv _),
+    rw [nat.sub_self, pow_zero r, mul_one] at h,
+    exact p_monic ▸ h },
+  refine ⟨p', ⟨_, _⟩⟩,
+  { rwa [monic, leading_coeff, hp', finset_sum_monomial_coeff, nat.sub_self, pow_zero, mul_one] },
+  -- TODO: A lot of this is just basic algebra, but `ring` can't solve it because only some elements are invertible
+  { have : is_unit (y ^ p.nat_degree) := is_unit_iff_exists_inv.2
+      ⟨(algebra_map R A r) ^ p.nat_degree, by rw [← mul_pow, mul_comm, hr, one_pow]⟩,
+    rw [aeval_def, eval₂, sum_over_range] at hp,
+    rw [← (is_unit.mul_right_eq_zero this), aeval_def, eval₂, sum_over_range, finset.mul_sum, ← hp],
+    refine finset.sum_congr (by rw hp') (λ n hn, _),
+    simp only [finset_sum_monomial_coeff, ring_hom.map_pow, ring_hom.map_mul],
+    rw [← mul_assoc (y ^ p.nat_degree), mul_comm (y ^ p.nat_degree), mul_comm x y, mul_pow y x n,
+        ← mul_assoc _ (y ^ n) (x ^ n), mul_assoc _ _ (y ^ p.nat_degree)],
+    congr,
+    have : is_unit ((algebra_map R A r) ^ n) := is_unit_iff_exists_inv.2
+      ⟨y ^ n, by rw [← mul_pow, hr, one_pow]⟩,
+    rw [← (is_unit.mul_left_inj this), ← mul_pow y _ n, mul_comm y, hr, mul_comm, ← mul_assoc,
+      ← pow_add, nat.add_sub_cancel' (nat.le_of_lt_succ (finset.mem_range.1 hn)),
+      ← mul_pow, hr, one_pow, one_pow],
+    all_goals {simp [add_mul]} },
+end


I think you can shorten the proof dramatically if you use scale_roots p (r⁻¹) defined in ring_theory.polynomial.rational_root.

This is very helpful as that is essentially the exact same polynomial as I tried to use here. The only issue is that if I try and import it, I end up with a cyclic dependency, rational_root → localization → integral_closure → rational_root, and I can't just move this theorem to rational_root since the additions to localization depend on it. I could maybe move these new theorems into rational_root, or create a new file like localization_integral. Not sure what's the best practice here

I think the best way would be to move the whole section scale_roots from the rational_root file to a new file ring_theory/polynomial/scale_roots.lean (or add it to ring_theory/basic, but that's getting long by itself already) (or even move it to data/polynomial/scale_roots.lean. I'm not sure what qualifies as data/polynomial and what as ring_theory/polynomial).

I've pulled out scale_roots into its own file, but to completely resolve the dependencies I also had to move non_zero_divisors into its own file, since scale_roots depends on it (I managed to remove le_non_zero_divisors from some scale_roots lemmas that didn't actually need to rely on it, but some do still actually need it`).

For now these are both in two new independent files, but perhaps non_zero_divisors could go somewhere else, maybe integral_domain or some other place that already deals with zero divisors. I also kept scale roots in ring_theory rather than data because of the reliance on non_zero_divisors for some lemmas.

Aha, I recall being annoyed before that non_zero_divisors is so far down the import hierarchy. Thank you for fixing that 🎉

As for the location of non_zero_divisors, maybe we should generalize all the way to monoid_with_zero and put it somewhere in algebra/group_with_zero.lean (I can't think of any non-ring monoid_with_zero where we would care about zero divisors, but the highest possible generality is what we really care about in mathlib :P)

I don't have any time right now for a full review, but tomorrow morning (in about 9 hours) I will check it out 👍

I changed the definition to the more generic monoid with zero, but most of the useful lemmas require more structure to prove, so as of now they still rely on either comm_ring or integral_domain. I didn't move it to location outside ring_theory either, since basically everything but the definition still relies on comm_ring

Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

…n_zero_divisors in many of the proofs

Vierkantor

It looks like we're almost finished. I found a few small points to improve and then it's good for me.

src/ring_theory/integral_closure.lean

src/ring_theory/localization.lean

src/ring_theory/non_zero_divisors.lean

Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

Vierkantor

Looks good to me.

jcommelin

Thanks for all the work you've done! I think that some parts can still be optimized a bit.

src/data/polynomial/eval.lean

src/ring_theory/localization.lean

src/ring_theory/non_zero_divisors.lean

jcommelin · 2020-09-01T03:45:07Z

src/ring_theory/non_zero_divisors.lean

+⟨λ hm hz, zero_ne_one (hm 1 $ by rw [hz, one_mul]).symm,
+λ hnx z, eq_zero_of_ne_zero_of_mul_eq_zero hnx⟩
+
+lemma map_ne_zero_of_mem_non_zero_divisors {B : Type*} [ring B] {g : A →+* B}


Does A really need to be an integral domain for this?

It looks like all it really needs is that A is nontrivial. I think whoever originally wrote these was just concerned about properties of fraction_map, and integral_domain was fine for these in that context. I'll go through and try and generalize some more of these lemmas as well.

src/ring_theory/non_zero_divisors.lean

jcommelin · 2020-09-01T03:46:43Z

src/ring_theory/non_zero_divisors.lean

+  (hg : function.injective g) {x : non_zero_divisors A} : g x ≠ 0 :=
+λ h0, mem_non_zero_divisors_iff_ne_zero.1 x.2 $ g.injective_iff.1 hg x h0
+
+lemma map_mem_non_zero_divisors {B : Type*} [integral_domain B] {g : A →+* B}


Please figure out the minimal assumptions.

I think that to drop the integral_domain assumption we'd need to instead assume that g is surjective, since I think g z * x = 0 isn't strong enough, we need to get g z * g x' = 0 to prove this is true. On the other hand I can't find any uses of this lemma anywhere in mathlib, so I'm not even sure it needs to exist in the first place.

into localization_integral

…on set doesn't contain zero divisors

jcommelin

Thanks 🎉

bors merge

…3942) The main definition is the algebra induced by localization at an algebra. Given an algebra `R → S` and a submonoid `M` of `R`, as well as localization maps `f : R → Rₘ` and `g : S → Sₘ`, there is a natural algebra `Rₘ → Sₘ` that makes the entire square commute, and this is defined as `localization_algebra`. The two main theorems are similar but distinct statements about integral elements and localizations: * `is_integral_localization_at_leading_coeff` says that if an element `x` is algebraic over `algebra R S`, then if we localize to a submonoid containing the leading coefficient the image of `x` will be integral. * `is_integral_localization` says that if `R → S` is an integral extension, then the algebra induced by localizing at any particular submonoid will be an integral extension. Co-authored-by: Devon Tuma <dtumad@gmail.com>

bors · 2020-09-02T14:54:43Z

Pull request successfully merged into master.

Build succeeded:

…3942) The main definition is the algebra induced by localization at an algebra. Given an algebra `R → S` and a submonoid `M` of `R`, as well as localization maps `f : R → Rₘ` and `g : S → Sₘ`, there is a natural algebra `Rₘ → Sₘ` that makes the entire square commute, and this is defined as `localization_algebra`. The two main theorems are similar but distinct statements about integral elements and localizations: * `is_integral_localization_at_leading_coeff` says that if an element `x` is algebraic over `algebra R S`, then if we localize to a submonoid containing the leading coefficient the image of `x` will be integral. * `is_integral_localization` says that if `R → S` is an integral extension, then the algebra induced by localizing at any particular submonoid will be an integral extension. Co-authored-by: Devon Tuma <dtumad@gmail.com>

dtumad added 7 commits August 19, 2020 12:01

First steps of a proof

e9c43a1

Mostly complete proof of one of the 2 big statements

b08755b

Merge branch 'master' into localization_integral

c3fdbe8

Filled in almost all the remaining sorry

0dde118

Closed all remaining sorry

6fc8b39

Add more comments and docstrings

802d217

fix build error

91e5546

dtumad added the awaiting-review The author would like community review of the PR label Aug 25, 2020

Vierkantor self-requested a review August 26, 2020 09:31

Vierkantor requested changes Aug 26, 2020

View reviewed changes

Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Aug 26, 2020

dtumad and others added 6 commits August 27, 2020 14:35

Apply suggestions from code review

d8ca26e

Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

Pull scale_roots into a new file, and remove the dependencey on le_no…

b9be853

…n_zero_divisors in many of the proofs

Replace old versions of mul_sum and sum_mul in finsupp

36fd84f

Fix build error from name change

7c52c3d

Remove no longer needed lemmas

1715534

Generalize non_zero_divisors to monoid with zero

eae2f77

Vierkantor requested changes Aug 28, 2020

View reviewed changes

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

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

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

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

dtumad and others added 4 commits August 28, 2020 12:56

Update src/ring_theory/integral_closure.lean

8033f90

Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

Update src/ring_theory/non_zero_divisors.lean

5cb8807

Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

Update src/ring_theory/non_zero_divisors.lean

7fc181d

Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

Update docstrings for new defs

87726ee

dtumad added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 31, 2020

Vierkantor approved these changes Aug 31, 2020

View reviewed changes

Vierkantor requested a review from jcommelin August 31, 2020 11:14

jcommelin requested changes Sep 1, 2020

View reviewed changes

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 1, 2020

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 1, 2020

dtumad added 2 commits September 1, 2020 11:04

Merge branch 'master' of https://github.com/leanprover-community/mathlib

32ce0fd

into localization_integral

Generalize lemmas about non_zero_divisors based on PR

82721da

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 1, 2020

fix build error and remove unnecessary assumption that the localizati…

1afdd55

…on set doesn't contain zero divisors

dtumad added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 2, 2020

Vierkantor mentioned this pull request Sep 2, 2020

[Merged by Bors] - feat(ring_theory/dedekind_domain): definitions #4000

Closed

jcommelin approved these changes Sep 2, 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 Sep 2, 2020

bors bot changed the title ~~feat(ring_theory/localization): Localizations of integral extensions~~ [Merged by Bors] - feat(ring_theory/localization): Localizations of integral extensions Sep 2, 2020

bors bot closed this Sep 2, 2020

bors bot deleted the localization_integral branch September 2, 2020 14:54

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(ring_theory/localization): Localizations of integral extensions #3942

[Merged by Bors] - feat(ring_theory/localization): Localizations of integral extensions #3942

dtumad commented Aug 25, 2020

Vierkantor left a comment

Vierkantor Aug 26, 2020

dtumad Aug 26, 2020

Vierkantor Aug 27, 2020

dtumad Aug 27, 2020

Vierkantor Aug 27, 2020 •

edited

dtumad Aug 28, 2020

Vierkantor left a comment

Vierkantor left a comment

jcommelin left a comment

jcommelin Sep 1, 2020

dtumad Sep 1, 2020

jcommelin Sep 1, 2020

dtumad Sep 1, 2020

jcommelin left a comment

bors bot commented Sep 2, 2020

[Merged by Bors] - feat(ring_theory/localization): Localizations of integral extensions #3942

[Merged by Bors] - feat(ring_theory/localization): Localizations of integral extensions #3942

Conversation

dtumad commented Aug 25, 2020

Vierkantor left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Vierkantor Aug 27, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Vierkantor left a comment

Choose a reason for hiding this comment

Vierkantor left a comment

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Sep 2, 2020

Vierkantor Aug 27, 2020 •

edited