From 7a7076463c779967e3d49b39e18b8e2ab78d20d2 Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Tue, 17 Nov 2020 12:21:30 +0000 Subject: [PATCH] feat(ring_theory/fractional_ideal): helper lemmas for Dedekind domains (#4994) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Co-Authored-By: faenuccio Co-authored-by: Anne Baanen --- src/ring_theory/fractional_ideal.lean | 537 ++++++++++++++++++++++---- src/ring_theory/localization.lean | 26 +- 2 files changed, 473 insertions(+), 90 deletions(-) diff --git a/src/ring_theory/fractional_ideal.lean b/src/ring_theory/fractional_ideal.lean index 39c9d28ae10a2..dad99f4751e9d 100644 --- a/src/ring_theory/fractional_ideal.lean +++ b/src/ring_theory/fractional_ideal.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Anne Baanen -/ import ring_theory.localization +import ring_theory.noetherian import ring_theory.principal_ideal_domain /-! @@ -67,7 +68,7 @@ namespace ring section defs -variables {R : Type*} [integral_domain R] {S : submonoid R} {P : Type*} [comm_ring P] +variables {R : Type*} [comm_ring R] {S : submonoid R} {P : Type*} [comm_ring P] (f : localization_map S P) /-- A submodule `I` is a fractional ideal if `a I ⊆ R` for some `a ≠ 0`. -/ @@ -90,14 +91,14 @@ namespace fractional_ideal open set open submodule -variables {R : Type*} [integral_domain R] {S : submonoid R} {P : Type*} [comm_ring P] +variables {R : Type*} [comm_ring R] {S : submonoid R} {P : Type*} [comm_ring P] {f : localization_map S P} instance : has_coe (fractional_ideal f) (submodule R f.codomain) := ⟨λ I, I.val⟩ @[simp] lemma val_eq_coe (I : fractional_ideal f) : I.val = I := rfl -@[simp] lemma coe_mk (I : submodule R f.codomain) (hI : is_fractional f I) : +@[simp, norm_cast] lemma coe_mk (I : submodule R f.codomain) (hI : is_fractional f I) : (subtype.mk I hI : submodule R f.codomain) = I := rfl instance : has_mem P (fractional_ideal f) := ⟨λ x I, x ∈ (I : submodule R f.codomain)⟩ @@ -111,6 +112,9 @@ instance : has_mem P (fractional_ideal f) := ⟨λ x I, x ∈ (I : submodule R f lemma ext {I J : fractional_ideal f} : (I : submodule R f.codomain) = J → I = J := subtype.ext_iff_val.mpr +lemma ext_iff {I J : fractional_ideal f} : (∀ x, (x ∈ I ↔ x ∈ J)) ↔ I = J := +⟨ λ h, ext (submodule.ext h), λ h x, h ▸ iff.rfl ⟩ + lemma fractional_of_subset_one (I : submodule R f.codomain) (h : I ≤ (submodule.span R {1})) : is_fractional f I := @@ -124,14 +128,23 @@ begin exact set.mem_range_self b', end +lemma is_fractional_of_le {I : submodule R f.codomain} {J : fractional_ideal f} + (hIJ : I ≤ J) : is_fractional f I := +begin + obtain ⟨a, a_mem, ha⟩ := J.2, + use [a, a_mem], + intros b b_mem, + exact ha b (hIJ b_mem) +end + instance coe_to_fractional_ideal : has_coe (ideal R) (fractional_ideal f) := ⟨ λ I, ⟨f.coe_submodule I, fractional_of_subset_one _ $ λ x ⟨y, hy, h⟩, submodule.mem_span_singleton.2 ⟨y, by rw ←h; exact mul_one _⟩⟩ ⟩ -@[simp] lemma coe_coe_ideal (I : ideal R) : +@[simp, norm_cast] lemma coe_coe_ideal (I : ideal R) : ((I : fractional_ideal f) : submodule R f.codomain) = f.coe_submodule I := rfl -@[simp] lemma mem_coe {x : f.codomain} {I : ideal R} : +@[simp] lemma mem_coe_ideal {x : f.codomain} {I : ideal R} : x ∈ (I : fractional_ideal f) ↔ ∃ (x' ∈ I), f.to_map x' = x := ⟨ λ ⟨x', hx', hx⟩, ⟨x', hx', hx⟩, λ ⟨x', hx', hx⟩, ⟨x', hx', hx⟩ ⟩ @@ -144,13 +157,40 @@ instance : has_zero (fractional_ideal f) := ⟨(0 : ideal R)⟩ by simp [x'_eq_x.symm, x'_eq_zero]), (λ hx, ⟨0, rfl, by simp [hx]⟩) ⟩ -@[simp] lemma coe_zero : ↑(0 : fractional_ideal f) = (⊥ : submodule R f.codomain) := +@[simp, norm_cast] lemma coe_zero : ↑(0 : fractional_ideal f) = (⊥ : submodule R f.codomain) := submodule.ext $ λ _, mem_zero_iff -lemma coe_ne_bot_iff_nonzero {I : fractional_ideal f} : +@[simp, norm_cast] lemma coe_to_fractional_ideal_bot : ((⊥ : ideal R) : fractional_ideal f) = 0 := +rfl + +@[simp] lemma exists_mem_to_map_eq {x : R} {I : ideal R} (h : S ≤ non_zero_divisors R) : + (∃ x', x' ∈ I ∧ f.to_map x' = f.to_map x) ↔ x ∈ I := +⟨λ ⟨x', hx', eq⟩, f.injective h eq ▸ hx', λ h, ⟨x, h, rfl⟩⟩ + +lemma coe_to_fractional_ideal_injective (h : S ≤ non_zero_divisors R) : + function.injective (coe : ideal R → fractional_ideal f) := +λ I J heq, have + ∀ (x : R), f.to_map x ∈ (I : fractional_ideal f) ↔ f.to_map x ∈ (J : fractional_ideal f) := +λ x, heq ▸ iff.rfl, +ideal.ext (by { simpa only [mem_coe_ideal, exists_prop, exists_mem_to_map_eq h] using this }) + +lemma coe_to_fractional_ideal_eq_zero {I : ideal R} (hS : S ≤ non_zero_divisors R) : + (I : fractional_ideal f) = 0 ↔ I = (⊥ : ideal R) := +⟨λ h, coe_to_fractional_ideal_injective hS h, + λ h, by rw [h, coe_to_fractional_ideal_bot]⟩ + +lemma coe_to_fractional_ideal_ne_zero {I : ideal R} (hS : S ≤ non_zero_divisors R) : + (I : fractional_ideal f) ≠ 0 ↔ I ≠ (⊥ : ideal R) := +not_iff_not.mpr (coe_to_fractional_ideal_eq_zero hS) + +lemma coe_to_submodule_eq_bot {I : fractional_ideal f} : + (I : submodule R f.codomain) = ⊥ ↔ I = 0 := +⟨λ h, ext (by simp [h]), + λ h, by simp [h] ⟩ + +lemma coe_to_submodule_ne_bot {I : fractional_ideal f} : ↑I ≠ (⊥ : submodule R f.codomain) ↔ I ≠ 0 := -⟨ λ h h', h (by simp [h']), - λ h h', h (ext (by simp [h'])) ⟩ +not_iff_not.mpr coe_to_submodule_eq_bot instance : inhabited (fractional_ideal f) := ⟨0⟩ @@ -166,7 +206,20 @@ mem_one_iff.mpr ⟨x, rfl⟩ lemma one_mem_one : (1 : P) ∈ (1 : fractional_ideal f) := mem_one_iff.mpr ⟨1, f.to_map.map_one⟩ -@[simp] lemma coe_one : ↑(1 : fractional_ideal f) = f.coe_submodule 1 := rfl +/-- `(1 : fractional_ideal f)` is defined as the R-submodule `f(R) ≤ K`. + +However, this is not definitionally equal to `1 : submodule R K`, +which is proved in the actual `simp` lemma `coe_one`. -/ +lemma coe_one_eq_coe_submodule_one : + ↑(1 : fractional_ideal f) = f.coe_submodule (1 : ideal R) := +rfl + +@[simp, norm_cast] lemma coe_one : + (↑(1 : fractional_ideal f) : submodule R f.codomain) = 1 := +begin + simp only [coe_one_eq_coe_submodule_one, ideal.one_eq_top], + convert (submodule.one_eq_map_top).symm, +end section lattice @@ -183,7 +236,12 @@ instance : partial_order (fractional_ideal f) := le_antisymm := λ ⟨I, hI⟩ ⟨J, hJ⟩ hIJ hJI, by { congr, exact le_antisymm hIJ hJI }, le_trans := λ _ _ _ hIJ hJK, le_trans hIJ hJK } -lemma le_iff {I J : fractional_ideal f} : I ≤ J ↔ (∀ x ∈ I, x ∈ J) := iff.refl _ +lemma le_iff_mem {I J : fractional_ideal f} : I ≤ J ↔ (∀ x ∈ I, x ∈ J) := +iff.rfl + +@[simp] lemma coe_le_coe {I J : fractional_ideal f} : + (I : submodule R f.codomain) ≤ (J : submodule R f.codomain) ↔ I ≤ J := +iff.rfl lemma zero_le (I : fractional_ideal f) : 0 ≤ I := begin @@ -200,6 +258,9 @@ instance order_bot : order_bot (fractional_ideal f) := @[simp] lemma bot_eq_zero : (⊥ : fractional_ideal f) = 0 := rfl +@[simp] lemma le_zero_iff {I : fractional_ideal f} : I ≤ 0 ↔ I = 0 := +le_bot_iff + lemma eq_zero_iff {I : fractional_ideal f} : I = 0 ↔ (∀ x ∈ I, x = (0 : P)) := ⟨ (λ h x hx, by simpa [h, mem_zero_iff] using hx), (λ h, le_bot_iff.mp (λ x hx, mem_zero_iff.mpr (h x hx))) ⟩ @@ -254,7 +315,7 @@ instance : has_add (fractional_ideal f) := ⟨(⊔)⟩ @[simp] lemma sup_eq_add (I J : fractional_ideal f) : I ⊔ J = I + J := rfl -@[simp] +@[simp, norm_cast] lemma coe_add (I J : fractional_ideal f) : (↑(I + J) : submodule R f.codomain) = I + J := rfl lemma fractional_mul (I J : fractional_ideal f) : is_fractional f (I.1 * J.1) := @@ -282,9 +343,25 @@ begin apply is_integer_smul hx }, end -instance : has_mul (fractional_ideal f) := ⟨λ I J, ⟨I.1 * J.1, fractional_mul I J⟩⟩ +/-- `fractional_ideal.mul` is the product of two fractional ideals, +used to define the `has_mul` instance. -@[simp] +This is only an auxiliary definition: the preferred way of writing `I.mul J` is `I * J`. + +Elaborated terms involving `fractional_ideal` tend to grow quite large, +so by making definitions irreducible, we hope to avoid deep unfolds. +-/ +@[irreducible] +def mul (I J : fractional_ideal f) : fractional_ideal f := +⟨I.1 * J.1, fractional_mul I J⟩ + +local attribute [semireducible] mul + +instance : has_mul (fractional_ideal f) := ⟨λ I J, mul I J⟩ + +@[simp] lemma mul_eq_mul (I J : fractional_ideal f) : mul I J = I * J := rfl + +@[simp, norm_cast] lemma coe_mul (I J : fractional_ideal f) : (↑(I * J) : submodule R f.codomain) = I * J := rfl lemma mul_left_mono (I : fractional_ideal f) : monotone ((*) I) := @@ -293,16 +370,27 @@ lemma mul_left_mono (I : fractional_ideal f) : monotone ((*) I) := lemma mul_right_mono (I : fractional_ideal f) : monotone (λ J, J * I) := λ J J' h, mul_le.mpr (λ x hx y hy, mul_mem_mul (h hx) hy) -instance add_comm_monoid : add_comm_monoid (fractional_ideal f) := +lemma mul_mem_mul {I J : fractional_ideal f} {i j : f.codomain} (hi : i ∈ I) (hj : j ∈ J) : + i * j ∈ I * J := submodule.mul_mem_mul hi hj + +lemma mul_le {I J K : fractional_ideal f} : + I * J ≤ K ↔ (∀ (i ∈ I) (j ∈ J), i * j ∈ K) := +submodule.mul_le + +@[elab_as_eliminator] protected theorem mul_induction_on + {I J : fractional_ideal f} + {C : f.codomain → Prop} {r : f.codomain} (hr : r ∈ I * J) + (hm : ∀ (i ∈ I) (j ∈ J), C (i * j)) + (h0 : C 0) (ha : ∀ x y, C x → C y → C (x + y)) + (hs : ∀ (r : R) x, C x → C (r • x)) : C r := +submodule.mul_induction_on hr hm h0 ha hs + +instance comm_semiring : comm_semiring (fractional_ideal f) := { add_assoc := λ I J K, sup_assoc, add_comm := λ I J, sup_comm, add_zero := λ I, sup_bot_eq, zero_add := λ I, bot_sup_eq, - ..fractional_ideal.has_zero, - ..fractional_ideal.has_add } - -instance comm_monoid : comm_monoid (fractional_ideal f) := -{ mul_assoc := λ I J K, ext (submodule.mul_assoc _ _ _), + mul_assoc := λ I J K, ext (submodule.mul_assoc _ _ _), mul_comm := λ I J, ext (submodule.mul_comm _ _), mul_one := λ I, begin ext, @@ -324,11 +412,7 @@ instance comm_monoid : comm_monoid (fractional_ideal f) := { have : 1 * x ∈ (1 * I) := mul_mem_mul one_mem_one h, rwa [one_mul] at this } end, - ..fractional_ideal.has_mul, - ..fractional_ideal.has_one } - -instance comm_semiring : comm_semiring (fractional_ideal f) := -{ mul_zero := λ I, eq_zero_iff.mpr (λ x hx, submodule.mul_induction_on hx + mul_zero := λ I, eq_zero_iff.mpr (λ x hx, submodule.mul_induction_on hx (λ x hx y hy, by simp [mem_zero_iff.mp hy]) rfl (λ x y hx hy, by simp [hx, hy]) @@ -340,8 +424,65 @@ instance comm_semiring : comm_semiring (fractional_ideal f) := (λ r x hx, by simp [hx])), left_distrib := λ I J K, ext (mul_add _ _ _), right_distrib := λ I J K, ext (add_mul _ _ _), - ..fractional_ideal.add_comm_monoid, - ..fractional_ideal.comm_monoid } + ..fractional_ideal.has_zero, + ..fractional_ideal.has_add, + ..fractional_ideal.has_one, + ..fractional_ideal.has_mul } + +section order + +lemma add_le_add_left {I J : fractional_ideal f} (hIJ : I ≤ J) (J' : fractional_ideal f) : + J' + I ≤ J' + J := +sup_le_sup_left hIJ J' + +lemma mul_le_mul_left {I J : fractional_ideal f} (hIJ : I ≤ J) (J' : fractional_ideal f) : + J' * I ≤ J' * J := +mul_le.mpr (λ k hk j hj, mul_mem_mul hk (hIJ hj)) + +lemma le_self_mul_self {I : fractional_ideal f} (hI: 1 ≤ I) : I ≤ I * I := +begin + convert mul_left_mono I hI, + exact (mul_one I).symm +end + +lemma mul_self_le_self {I : fractional_ideal f} (hI: I ≤ 1) : I * I ≤ I := +begin + convert mul_left_mono I hI, + exact (mul_one I).symm +end + +lemma coe_ideal_le_one {I : ideal R} : (I : fractional_ideal f) ≤ 1 := +λ x hx, let ⟨y, _, hy⟩ := fractional_ideal.mem_coe_ideal.mp hx + in fractional_ideal.mem_one_iff.mpr ⟨y, hy⟩ + +lemma le_one_iff_exists_coe_ideal {J : fractional_ideal f} : + J ≤ (1 : fractional_ideal f) ↔ ∃ (I : ideal R), ↑I = J := +begin + split, + { intro hJ, + refine ⟨⟨{x : R | f.to_map x ∈ J}, _, _, _⟩, _⟩, + { rw [mem_set_of_eq, ring_hom.map_zero], + exact J.val.zero_mem }, + { intros a b ha hb, + rw [mem_set_of_eq, ring_hom.map_add], + exact J.val.add_mem ha hb }, + { intros c x hx, + rw [smul_eq_mul, mem_set_of_eq, ring_hom.map_mul], + exact J.val.smul_mem c hx }, + { ext x, + split, + { rintros ⟨y, hy, eq_y⟩, + rwa ← eq_y }, + { intro hx, + obtain ⟨y, eq_x⟩ := fractional_ideal.mem_one_iff.mp (hJ hx), + rw ← eq_x at *, + exact ⟨y, hx, rfl⟩ } } }, + { rintro ⟨I, hI⟩, + rw ← hI, + apply coe_ideal_le_one }, +end + +end order variables {P' : Type*} [comm_ring P'] {f' : localization_map S P'} variables {P'' : Type*} [comm_ring P''] {f'' : localization_map S P''} @@ -364,7 +505,7 @@ def map (g : f.codomain →ₐ[R] f'.codomain) : fractional_ideal f → fractional_ideal f' := λ I, ⟨submodule.map g.to_linear_map I.1, fractional_map g I⟩ -@[simp] lemma coe_map (g : f.codomain →ₐ[R] f'.codomain) (I : fractional_ideal f) : +@[simp, norm_cast] lemma coe_map (g : f.codomain →ₐ[R] f'.codomain) (I : fractional_ideal f) : ↑(map g I) = submodule.map g.to_linear_map I := rfl @[simp] lemma mem_map {I : fractional_ideal f} {g : f.codomain →ₐ[R] f'.codomain} @@ -380,7 +521,7 @@ ext (submodule.map_id I.1) I.map (g'.comp g) = (I.map g).map g' := ext (submodule.map_comp g.to_linear_map g'.to_linear_map I.1) -@[simp] lemma map_coe_ideal (I : ideal R) : +@[simp, norm_cast] lemma map_coe_ideal (I : ideal R) : (I : fractional_ideal f).map g = I := begin ext x, @@ -393,7 +534,7 @@ begin end @[simp] lemma map_one : -(1 : fractional_ideal f).map g = 1 := + (1 : fractional_ideal f).map g = 1 := map_coe_ideal g 1 @[simp] lemma map_zero : @@ -424,22 +565,66 @@ def map_equiv (g : f.codomain ≃ₐ[R] f'.codomain) : left_inv := λ I, by { rw [←map_comp, alg_equiv.symm_comp, map_id] }, right_inv := λ I, by { rw [←map_comp, alg_equiv.comp_symm, map_id] } } -@[simp] lemma map_equiv_apply (g : f.codomain ≃ₐ[R] f'.codomain) : +@[simp] lemma coe_fun_map_equiv (g : f.codomain ≃ₐ[R] f'.codomain) : + ⇑(map_equiv g) = map g := +rfl + +@[simp] lemma map_equiv_apply (g : f.codomain ≃ₐ[R] f'.codomain) (I : fractional_ideal f) : map_equiv g I = map ↑g I := rfl +@[simp] lemma map_equiv_symm (g : f.codomain ≃ₐ[R] f'.codomain) : + (map_equiv g).symm = map_equiv g.symm := rfl + @[simp] lemma map_equiv_refl : map_equiv alg_equiv.refl = ring_equiv.refl (fractional_ideal f) := ring_equiv.ext (λ x, by simp) +lemma is_fractional_span_iff {s : set f.codomain} : +is_fractional f (span R s) ↔ ∃ a ∈ S, ∀ (b : P), b ∈ s → f.is_integer (f.to_map a * b) := +⟨ λ ⟨a, a_mem, h⟩, ⟨a, a_mem, λ b hb, h b (subset_span hb)⟩, + λ ⟨a, a_mem, h⟩, ⟨a, a_mem, λ b hb, span_induction hb + h + (by { rw mul_zero, exact f.is_integer_zero }) + (λ x y hx hy, by { rw mul_add, exact is_integer_add hx hy }) + (λ s x hx, by { rw algebra.mul_smul_comm, exact is_integer_smul hx }) ⟩ ⟩ + +lemma is_fractional_of_fg {I : submodule R f.codomain} (hI : I.fg) : + is_fractional f I := +begin + rcases hI with ⟨I, rfl⟩, + rcases localization_map.exist_integer_multiples_of_finset f I with ⟨⟨s, hs1⟩, hs⟩, + rw is_fractional_span_iff, + exact ⟨s, hs1, hs⟩, +end + /-- `canonical_equiv f f'` is the canonical equivalence between the fractional ideals in `f.codomain` and in `f'.codomain` -/ -noncomputable def canonical_equiv (f f' : localization_map S P) : +@[irreducible] +noncomputable def canonical_equiv (f : localization_map S P) (f' : localization_map S P') : fractional_ideal f ≃+* fractional_ideal f' := map_equiv { commutes' := λ r, ring_equiv_of_ring_equiv_eq _ _ _, ..ring_equiv_of_ring_equiv f f' (ring_equiv.refl R) (by rw [ring_equiv.to_monoid_hom_refl, submonoid.map_id]) } +@[simp] lemma mem_canonical_equiv_apply {I : fractional_ideal f} {x : f'.codomain} : + x ∈ canonical_equiv f f' I ↔ + ∃ y ∈ I, @localization_map.map _ _ _ _ _ _ _ f (ring_hom.id _) _ (λ ⟨y, hy⟩, hy) _ _ f' y = x := +begin + rw [canonical_equiv, map_equiv_apply, mem_map], + exact ⟨λ ⟨y, mem, eq⟩, ⟨y, mem, eq⟩, λ ⟨y, mem, eq⟩, ⟨y, mem, eq⟩⟩ +end + +@[simp] lemma canonical_equiv_symm (f : localization_map S P) (f' : localization_map S P') : + (canonical_equiv f f').symm = canonical_equiv f' f := +ring_equiv.ext $ λ I, fractional_ideal.ext_iff.mp $ λ x, +by { erw [mem_canonical_equiv_apply, canonical_equiv, map_equiv_symm, map_equiv, mem_map], + exact ⟨λ ⟨y, mem, eq⟩, ⟨y, mem, eq⟩, λ ⟨y, mem, eq⟩, ⟨y, mem, eq⟩⟩ } + +@[simp] lemma canonical_equiv_flip (f : localization_map S P) (f' : localization_map S P') (I) : + canonical_equiv f f' (canonical_equiv f' f I) = I := +by rw [←canonical_equiv_symm, ring_equiv.symm_apply_apply] + end semiring section fraction_map @@ -455,7 +640,7 @@ variables {K K' : Type*} [field K] [field K'] {g : fraction_map R K} {g' : fract variables {I J : fractional_ideal g} (h : g.codomain →ₐ[R] g'.codomain) /-- Nonzero fractional ideals contain a nonzero integer. -/ -lemma exists_ne_zero_mem_is_integer (hI : I ≠ 0) : +lemma exists_ne_zero_mem_is_integer [nontrivial R] (hI : I ≠ 0) : ∃ x ≠ (0 : R), g.to_map x ∈ I := begin obtain ⟨y, y_mem, y_not_mem⟩ := submodule.exists_of_lt (bot_lt_iff_ne_bot.mpr hI), @@ -468,7 +653,7 @@ begin exact smul_mem _ _ y_mem } end -lemma map_ne_zero (hI : I ≠ 0) : I.map h ≠ 0 := +lemma map_ne_zero [nontrivial R] (hI : I ≠ 0) : I.map h ≠ 0 := begin obtain ⟨x, x_ne_zero, hx⟩ := exists_ne_zero_mem_is_integer hI, contrapose! x_ne_zero with map_eq_zero, @@ -476,7 +661,7 @@ begin exact ⟨g.to_map x, hx, h.commutes x⟩, end -@[simp] lemma map_eq_zero_iff : I.map h = 0 ↔ I = 0 := +@[simp] lemma map_eq_zero_iff [nontrivial R] : I.map h = 0 ↔ I = 0 := ⟨imp_of_not_imp_not _ _ (map_ne_zero _), λ hI, hI.symm ▸ map_zero h⟩ @@ -497,7 +682,7 @@ is a field because `R` is a domain. open_locale classical -variables {K : Type*} [field K] {g : fraction_map R K} +variables {R₁ : Type*} [integral_domain R₁] {K : Type*} [field K] {g : fraction_map R₁ K} instance : nontrivial (fractional_ideal g) := ⟨⟨0, 1, λ h, @@ -514,7 +699,7 @@ begin obtain ⟨y', hy'⟩ := hJ y mem_J, use (aI * y'), split, - { apply (non_zero_divisors R).mul_mem haI (mem_non_zero_divisors_iff_ne_zero.mpr _), + { apply (non_zero_divisors R₁).mul_mem haI (mem_non_zero_divisors_iff_ne_zero.mpr _), intro y'_eq_zero, have : g.to_map aJ * y = 0 := by rw [←hy', y'_eq_zero, g.to_map.map_zero], obtain aJ_zero | y_zero := mul_eq_zero.mp this, @@ -531,6 +716,8 @@ noncomputable instance fractional_ideal_has_div : has_div (fractional_ideal g) := ⟨ λ I J, if h : J = 0 then 0 else ⟨I.1 / J.1, fractional_div_of_nonzero h⟩ ⟩ +variables {I J : fractional_ideal g} [ J ≠ 0 ] + noncomputable instance : has_inv (fractional_ideal g) := ⟨λ I, 1 / I⟩ lemma inv_eq {I : fractional_ideal g} : I⁻¹ = 1 / I := rfl @@ -543,15 +730,57 @@ lemma div_nonzero {I J : fractional_ideal g} (h : J ≠ 0) : (I / J) = ⟨I.1 / J.1, fractional_div_of_nonzero h⟩ := dif_neg h -lemma inv_zero : (0 : fractional_ideal g)⁻¹ = 0 := -div_zero +lemma inv_zero : (0 : fractional_ideal g)⁻¹ = 0 := div_zero lemma inv_nonzero {I : fractional_ideal g} (h : I ≠ 0) : I⁻¹ = ⟨(1 : fractional_ideal g) / I, fractional_div_of_nonzero h⟩ := div_nonzero h +@[simp] lemma coe_div {I J : fractional_ideal g} (hJ : J ≠ 0) : + (↑(I / J) : submodule R₁ g.codomain) = ↑I / (↑J : submodule R₁ g.codomain) := +begin + unfold has_div.div, + simp only [dif_neg hJ, coe_mk, val_eq_coe], +end + +lemma mem_div_iff_of_nonzero {I J : fractional_ideal g} (h : J ≠ 0) {x} : + x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I := +by { rw div_nonzero h, exact submodule.mem_div_iff_forall_mul_mem } + +lemma mul_one_div_le_one {I : fractional_ideal g} : I * (1 / I) ≤ 1 := +begin + by_cases hI : I = 0, + { rw [hI, div_zero, mul_zero], + exact zero_le 1 }, + { rw [← coe_le_coe, coe_mul, coe_div hI, coe_one], + apply submodule.mul_one_div_le_one }, +end + +lemma le_self_mul_one_div {I : fractional_ideal g} (hI : I ≤ (1 : fractional_ideal g)) : + I ≤ I * (1 / I) := +begin + by_cases hI_nz : I = 0, + { rw [hI_nz, div_zero, mul_zero], exact zero_le 0 }, + { rw [← coe_le_coe, coe_mul, coe_div hI_nz, coe_one], + rw [← coe_le_coe, coe_one] at hI, + exact submodule.le_self_mul_one_div hI }, +end + +lemma le_div_iff_of_nonzero {I J J' : fractional_ideal g} (hJ' : J' ≠ 0) : + I ≤ J / J' ↔ ∀ (x ∈ I) (y ∈ J'), x * y ∈ J := +⟨ λ h x hx, (mem_div_iff_of_nonzero hJ').mp (h hx), + λ h x hx, (mem_div_iff_of_nonzero hJ').mpr (h x hx) ⟩ + +lemma le_div_iff_mul_le {I J J' : fractional_ideal g} (hJ' : J' ≠ 0) : I ≤ J / J' ↔ I * J' ≤ J := +begin + rw div_nonzero hJ', + convert submodule.le_div_iff_mul_le using 1, + rw [val_eq_coe, val_eq_coe, ←coe_mul], + refl, +end + lemma coe_inv_of_nonzero {I : fractional_ideal g} (h : I ≠ 0) : - (↑(I⁻¹) : submodule R g.codomain) = g.coe_submodule 1 / I := + (↑I⁻¹ : submodule R₁ g.codomain) = g.coe_submodule 1 / I := by { rw inv_nonzero h, refl } @[simp] lemma div_one {I : fractional_ideal g} : I / 1 = I := @@ -563,7 +792,7 @@ begin (g.to_map.map_one ▸ coe_mem_one 1), simp }, { apply mem_div_iff_forall_mul_mem.mpr, rintros y ⟨y', _, y_eq_y'⟩, - rw [mul_comm], + rw mul_comm, convert submodule.smul_mem _ y' h, rw ←y_eq_y', refl } @@ -580,17 +809,16 @@ begin suffices h' : I * (1 / I) = 1, { exact (congr_arg units.inv $ @units.ext _ _ (units.mk_of_mul_eq_one _ _ h) (units.mk_of_mul_eq_one _ _ h') rfl) }, - rw [div_nonzero hI], apply le_antisymm, - { apply submodule.mul_le.mpr _, + { apply mul_le.mpr _, intros x hx y hy, - rw [mul_comm], - exact mem_div_iff_forall_mul_mem.mp hy x hx }, - rw [←h], + rw mul_comm, + exact (mem_div_iff_of_nonzero hI).mp hy x hx }, + rw ← h, apply mul_left_mono I, - apply submodule.le_div_iff.mpr _, + apply (le_div_iff_of_nonzero hI).mpr _, intros y hy x hx, - rw [mul_comm], + rw mul_comm, exact mul_mem_mul hx hy end @@ -598,10 +826,10 @@ theorem mul_inv_cancel_iff {I : fractional_ideal g} : I * I⁻¹ = 1 ↔ ∃ J, I * J = 1 := ⟨λ h, ⟨I⁻¹, h⟩, λ ⟨J, hJ⟩, by rwa [←right_inverse_eq I J hJ]⟩ -variables {K' : Type*} [field K'] {g' : fraction_map R K'} +variables {K' : Type*} [field K'] {g' : fraction_map R₁ K'} -@[simp] lemma map_div (I J : fractional_ideal g) (h : g.codomain ≃ₐ[R] g'.codomain) : - (I / J).map (h : g.codomain →ₐ[R] g'.codomain) = I.map h / J.map h := +@[simp] lemma map_div (I J : fractional_ideal g) (h : g.codomain ≃ₐ[R₁] g'.codomain) : + (I / J).map (h : g.codomain →ₐ[R₁] g'.codomain) = I.map h / J.map h := begin by_cases H : J = 0, { rw [H, div_zero, map_zero, div_zero] }, @@ -609,55 +837,61 @@ begin simp [div_nonzero H, div_nonzero (map_ne_zero _ H), submodule.map_div] } end -@[simp] lemma map_inv (I : fractional_ideal g) (h : g.codomain ≃ₐ[R] g'.codomain) : - (I⁻¹).map (h : g.codomain →ₐ[R] g'.codomain) = (I.map h)⁻¹ := +@[simp] lemma map_inv (I : fractional_ideal g) (h : g.codomain ≃ₐ[R₁] g'.codomain) : + (I⁻¹).map (h : g.codomain →ₐ[R₁] g'.codomain) = (I.map h)⁻¹ := by rw [inv_eq, map_div, map_one, inv_eq] end quotient section principal_ideal_ring -variables {K : Type*} [field K] {g : fraction_map R K} +variables {R₁ : Type*} [integral_domain R₁] {K : Type*} [field K] {g : fraction_map R₁ K} open_locale classical open submodule submodule.is_principal -lemma span_fractional_iff {s : set f.codomain} : - is_fractional f (span R s) ↔ ∃ a ∈ S, ∀ (b : P), b ∈ s → f.is_integer (f.to_map a * b) := -⟨ λ ⟨a, a_mem, h⟩, ⟨a, a_mem, λ b hb, h b (subset_span hb)⟩, - λ ⟨a, a_mem, h⟩, ⟨a, a_mem, λ b hb, span_induction hb - h - (is_integer_smul ⟨0, f.to_map.map_zero⟩) - (λ x y hx hy, by { rw mul_add, exact is_integer_add hx hy }) - (λ s x hx, by { rw algebra.mul_smul_comm, exact is_integer_smul hx }) ⟩ ⟩ - -lemma span_singleton_fractional (x : f.codomain) : is_fractional f (span R {x}) := +lemma is_fractional_span_singleton (x : f.codomain) : is_fractional f (span R {x}) := let ⟨a, ha⟩ := f.exists_integer_multiple x in -span_fractional_iff.mpr ⟨ a.1, a.2, λ x hx, (mem_singleton_iff.mp hx).symm ▸ ha⟩ +is_fractional_span_iff.mpr ⟨ a.1, a.2, λ x hx, (mem_singleton_iff.mp hx).symm ▸ ha⟩ /-- `span_singleton x` is the fractional ideal generated by `x` if `0 ∉ S` -/ +@[irreducible] def span_singleton (x : f.codomain) : fractional_ideal f := -⟨span R {x}, span_singleton_fractional x⟩ +⟨span R {x}, is_fractional_span_singleton x⟩ + +local attribute [semireducible] span_singleton @[simp] lemma coe_span_singleton (x : f.codomain) : (span_singleton x : submodule R f.codomain) = span R {x} := rfl -lemma eq_span_singleton_of_principal (I : fractional_ideal f) [is_principal I.1] : - I = span_singleton (generator I.1) := +@[simp] lemma mem_span_singleton {x y : f.codomain} : + x ∈ span_singleton y ↔ ∃ (z : R), z • y = x := +submodule.mem_span_singleton + +lemma mem_span_singleton_self (x : f.codomain) : + x ∈ span_singleton x := +mem_span_singleton.mpr ⟨1, one_smul _ _⟩ + +lemma eq_span_singleton_of_principal (I : fractional_ideal f) + [is_principal (I : submodule R f.codomain)] : + I = span_singleton (generator (I : submodule R f.codomain)) := ext (span_singleton_generator I.1).symm lemma is_principal_iff (I : fractional_ideal f) : - is_principal I.1 ↔ ∃ x, I = span_singleton x := -⟨ λ h, ⟨@generator _ _ _ _ _ I.1 h, @eq_span_singleton_of_principal _ _ _ _ _ _ I h⟩, - λ ⟨x, hx⟩, { principal := ⟨x, trans (congr_arg _ hx) (coe_span_singleton x)⟩ } ⟩ + is_principal (I : submodule R f.codomain) ↔ ∃ x, I = span_singleton x := +⟨λ h, ⟨@generator _ _ _ _ _ I.1 h, @eq_span_singleton_of_principal _ _ _ _ _ _ I h⟩, + λ ⟨x, hx⟩, { principal := ⟨x, trans (congr_arg _ hx) (coe_span_singleton x)⟩ } ⟩ @[simp] lemma span_singleton_zero : span_singleton (0 : f.codomain) = 0 := by { ext, simp [submodule.mem_span_singleton, eq_comm] } lemma span_singleton_eq_zero_iff {y : f.codomain} : span_singleton y = 0 ↔ y = 0 := -⟨ λ h, span_eq_bot.mp (by simpa using congr_arg subtype.val h : span R {y} = ⊥) y (mem_singleton y), - λ h, by simp [h] ⟩ +⟨λ h, span_eq_bot.mp (by simpa using congr_arg subtype.val h : span R {y} = ⊥) y (mem_singleton y), + λ h, by simp [h] ⟩ + +lemma span_singleton_ne_zero_iff {y : f.codomain} : span_singleton y ≠ 0 ↔ y ≠ 0 := +not_congr span_singleton_eq_zero_iff @[simp] lemma span_singleton_one : span_singleton (1 : f.codomain) = 1 := begin @@ -680,15 +914,38 @@ lemma coe_ideal_span_singleton (x : R) : (↑(span R {x} : ideal R) : fractional_ideal f) = span_singleton (f.to_map x) := begin ext y, - refine mem_coe.trans (iff.trans _ mem_span_singleton.symm), + refine mem_coe_ideal.trans (iff.trans _ mem_span_singleton.symm), split, { rintros ⟨y', hy', rfl⟩, - obtain ⟨x', rfl⟩ := mem_span_singleton.mp hy', + obtain ⟨x', rfl⟩ := submodule.mem_span_singleton.mp hy', use x', rw [smul_eq_mul, f.to_map.map_mul], refl }, { rintros ⟨y', rfl⟩, - exact ⟨y' * x, mem_span_singleton.mpr ⟨y', rfl⟩, f.to_map.map_mul _ _⟩ } + exact ⟨y' * x, submodule.mem_span_singleton.mpr ⟨y', rfl⟩, f.to_map.map_mul _ _⟩ } +end + +@[simp] +lemma canonical_equiv_span_singleton (f : localization_map S P) {P'} [comm_ring P'] + (f' : localization_map S P') (x : f.codomain) : + canonical_equiv f f' (span_singleton x) = + span_singleton (f.map (show ∀ (y : S), ring_hom.id _ y.1 ∈ S, from λ y, y.2) f' x) := +begin + apply ext_iff.mp, + intro y, + split; intro h, + { apply mem_span_singleton.mpr, + obtain ⟨x', hx', rfl⟩ := mem_canonical_equiv_apply.mp h, + obtain ⟨z, rfl⟩ := mem_span_singleton.mp hx', + use z, + rw localization_map.map_smul, + refl }, + { apply mem_canonical_equiv_apply.mpr, + obtain ⟨z, rfl⟩ := mem_span_singleton.mp h, + use f.to_map z * x, + use mem_span_singleton.mpr ⟨z, rfl⟩, + rw [ring_hom.map_mul, localization_map.map_eq], + refl } end lemma mem_singleton_mul {x y : f.codomain} {I : fractional_ideal f} : @@ -696,7 +953,7 @@ lemma mem_singleton_mul {x y : f.codomain} {I : fractional_ideal f} : begin split, { intro h, - apply submodule.mul_induction_on h, + apply fractional_ideal.mul_induction_on h, { intros x' hx' y' hy', obtain ⟨a, ha⟩ := mem_span_singleton.mp hx', use [a • y', I.1.smul_mem a hy'], @@ -711,8 +968,8 @@ begin end lemma mul_generator_self_inv (I : fractional_ideal g) - [submodule.is_principal I.1] (h : I ≠ 0) : - I * span_singleton (generator I.1)⁻¹ = 1 := + [submodule.is_principal (I : submodule R₁ g.codomain)] (h : I ≠ 0) : + I * span_singleton (generator (I : submodule R₁ g.codomain))⁻¹ = 1 := begin -- Rewrite only the `I` that appears alone. conv_lhs { congr, rw eq_span_singleton_of_principal I }, @@ -722,22 +979,81 @@ begin rw [eq_span_singleton_of_principal I, generator_I_eq_zero, span_singleton_zero] end +lemma one_div_span_singleton (x : g.codomain) : + 1 / span_singleton x = span_singleton (x⁻¹) := +if h : x = 0 then by simp [h] else (right_inverse_eq _ _ (by simp [h])).symm + +@[simp] +lemma span_singleton_inv (x : g.codomain) : + (span_singleton x)⁻¹ = span_singleton (x⁻¹) := +one_div_span_singleton x + +lemma invertible_of_principal (I : fractional_ideal g) + [submodule.is_principal (I : submodule R₁ g.codomain)] (h : I ≠ 0) : + I * I⁻¹ = 1 := +mul_inv_cancel_iff.mpr + ⟨span_singleton (generator (I : submodule R₁ g.codomain))⁻¹, mul_generator_self_inv I h⟩ + +lemma invertible_iff_generator_nonzero (I : fractional_ideal g) + [submodule.is_principal (I : submodule R₁ g.codomain)] : + I * I⁻¹ = 1 ↔ generator (I : submodule R₁ g.codomain) ≠ 0 := +begin + split, + { intros hI hg, + apply ne_zero_of_mul_eq_one _ _ hI, + rw [eq_span_singleton_of_principal I, hg, span_singleton_zero] }, + { intro hg, + apply invertible_of_principal, + rw [eq_span_singleton_of_principal I], + intro hI, + have := mem_span_singleton_self (generator (I : submodule R₁ g.codomain)), + rw [hI, mem_zero_iff] at this, + contradiction } +end + +lemma is_principal_inv (I : fractional_ideal g) + [submodule.is_principal (I : submodule R₁ g.codomain)] (h : I ≠ 0) : + submodule.is_principal (I⁻¹).1 := +I⁻¹.is_principal_iff.mpr ⟨_, (right_inverse_eq _ _ (mul_generator_self_inv I h)).symm⟩ + +@[simp] +lemma div_span_singleton (J : fractional_ideal g) (d : g.codomain) : + J / span_singleton d = span_singleton (d⁻¹) * J := +begin + rw ← one_div_span_singleton, + by_cases hd : d = 0, + { simp only [hd, span_singleton_zero, div_zero, zero_mul] }, + have h_spand : span_singleton d ≠ 0 := mt span_singleton_eq_zero_iff.mp hd, + apply le_antisymm, + { intros x hx, + rw [val_eq_coe, coe_div h_spand, submodule.mem_div_iff_forall_mul_mem] at hx, + specialize hx d (mem_span_singleton_self d), + have h_xd : x = d⁻¹ * (x * d), { field_simp [hd] }, + rw [val_eq_coe, coe_mul, one_div_span_singleton, h_xd], + exact submodule.mul_mem_mul (mem_span_singleton_self _) hx }, + { rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_span_singleton, + span_singleton_mul_span_singleton, inv_mul_cancel hd, span_singleton_one, mul_one], + exact le_refl J }, +end + lemma exists_eq_span_singleton_mul (I : fractional_ideal g) : - ∃ (a : R) (aI : ideal R), a ≠ 0 ∧ I = span_singleton (g.to_map a)⁻¹ * aI := + ∃ (a : R₁) (aI : ideal R₁), a ≠ 0 ∧ I = span_singleton (g.to_map a)⁻¹ * aI := begin obtain ⟨a_inv, nonzero, ha⟩ := I.2, have nonzero := mem_non_zero_divisors_iff_ne_zero.mp nonzero, have map_a_nonzero := mt g.to_map_eq_zero_iff.mp nonzero, - use [a_inv, (span_singleton (g.to_map a_inv) * I).1.comap g.lin_coe, nonzero], + use a_inv, + use (span_singleton (g.to_map a_inv) * I).1.comap g.lin_coe, + split, exact nonzero, ext, refine iff.trans _ mem_singleton_mul.symm, split, { intro hx, obtain ⟨x', hx'⟩ := ha x hx, - refine ⟨g.to_map x', mem_coe.mpr ⟨x', (mem_singleton_mul.mpr ⟨x, hx, hx'⟩), rfl⟩, _⟩, + refine ⟨g.to_map x', mem_coe_ideal.mpr ⟨x', (mem_singleton_mul.mpr ⟨x, hx, hx'⟩), rfl⟩, _⟩, erw [hx', ←mul_assoc, inv_mul_cancel map_a_nonzero, one_mul] }, { rintros ⟨y, hy, rfl⟩, - obtain ⟨x', hx', rfl⟩ := mem_coe.mp hy, + obtain ⟨x', hx', rfl⟩ := mem_coe_ideal.mp hy, obtain ⟨y', hy', hx'⟩ := mem_singleton_mul.mp hx', rw lin_coe_apply at hx', erw [hx', ←mul_assoc, inv_mul_cancel map_a_nonzero, one_mul], @@ -746,9 +1062,8 @@ end instance is_principal {R} [integral_domain R] [is_principal_ideal_ring R] {f : fraction_map R K} (I : fractional_ideal f) : (I : submodule R f.codomain).is_principal := - begin +begin obtain ⟨a, aI, -, ha⟩ := exists_eq_span_singleton_mul I, - have := (f.to_map a)⁻¹ * f.to_map (generator aI), use (f.to_map a)⁻¹ * f.to_map (generator aI), suffices : I = span_singleton ((f.to_map a)⁻¹ * f.to_map (generator aI)), { exact congr_arg subtype.val this }, @@ -758,6 +1073,58 @@ end end principal_ideal_ring +variables {R₁ : Type*} [integral_domain R₁] +variables {K : Type*} [field K] {g : fraction_map R₁ K} + +local attribute [instance] classical.prop_decidable + +lemma is_noetherian_zero : is_noetherian R₁ (0 : fractional_ideal g) := +is_noetherian_submodule.mpr (λ I (hI : I ≤ (0 : fractional_ideal g)), + by { rw coe_zero at hI, rw le_bot_iff.mp hI, exact fg_bot }) + +lemma is_noetherian_iff {I : fractional_ideal g} : + is_noetherian R₁ I ↔ ∀ J ≤ I, (J : submodule R₁ g.codomain).fg := +is_noetherian_submodule.trans ⟨λ h J hJ, h _ hJ, λ h J hJ, h ⟨J, is_fractional_of_le hJ⟩ hJ⟩ + +lemma is_noetherian_coe_to_fractional_ideal [is_noetherian_ring R₁] (I : ideal R₁) : + is_noetherian R₁ (I : fractional_ideal g) := +begin + rw is_noetherian_iff, + intros J hJ, + obtain ⟨J, rfl⟩ := le_one_iff_exists_coe_ideal.mp (le_trans hJ coe_ideal_le_one), + exact fg_map (is_noetherian.noetherian J), +end + +lemma is_noetherian_span_singleton_to_map_inv_mul (x : R₁) {I : fractional_ideal g} + (hI : is_noetherian R₁ I) : + is_noetherian R₁ (span_singleton (g.to_map x)⁻¹ * I : fractional_ideal g) := +begin + by_cases hx : x = 0, + { rw [hx, g.to_map.map_zero, _root_.inv_zero, span_singleton_zero, zero_mul], + exact is_noetherian_zero }, + have h_gx : g.to_map x ≠ 0, + from mt (g.to_map.injective_iff.mp (fraction_map.injective g) x) hx, + have h_spanx : span_singleton (g.to_map x) ≠ (0 : fractional_ideal g), + from span_singleton_ne_zero_iff.mpr h_gx, + + rw is_noetherian_iff at ⊢ hI, + intros J hJ, + rw [← div_span_singleton, le_div_iff_mul_le h_spanx] at hJ, + obtain ⟨s, hs⟩ := hI _ hJ, + use s * {(g.to_map x)⁻¹}, + rw [finset.coe_mul, finset.coe_singleton, ← span_mul_span, hs, ← coe_span_singleton, ← coe_mul, + mul_assoc, span_singleton_mul_span_singleton, mul_inv_cancel h_gx, + span_singleton_one, mul_one], +end + +/-- Every fractional ideal of a noetherian integral domain is noetherian. -/ +lemma is_noetherian [is_noetherian_ring R₁] (I : fractional_ideal g) : is_noetherian R₁ I := +begin + obtain ⟨d, J, h_nzd, rfl⟩ := exists_eq_span_singleton_mul I, + apply is_noetherian_span_singleton_to_map_inv_mul, + apply is_noetherian_coe_to_fractional_ideal, +end + end fractional_ideal end ring diff --git a/src/ring_theory/localization.lean b/src/ring_theory/localization.lean index ced5a28e46211..1a2f6db71eb51 100644 --- a/src/ring_theory/localization.lean +++ b/src/ring_theory/localization.lean @@ -160,6 +160,11 @@ lemma to_map_injective : injective (@localization_map.to_map _ _ M S _) := the localization map from `R` to `S`. -/ def is_integer (a : S) : Prop := a ∈ set.range f.to_map +-- TODO: define a subalgebra of `is_integer`s +lemma is_integer_zero : f.is_integer 0 := ⟨0, f.to_map.map_zero⟩ + +lemma is_integer_one : f.is_integer 1 := ⟨1, f.to_map.map_one⟩ + variables {f} lemma is_integer_add {a b} (ha : f.is_integer a) (hb : f.is_integer b) : @@ -959,6 +964,12 @@ lemma map_smul (x : f.codomain) (z : R) : show f.map hy k (f.to_map z * x) = k.to_map (g z) * f.map hy k x, by rw [ring_hom.map_mul, map_eq] +lemma is_noetherian_ring (h : is_noetherian_ring R) : is_noetherian_ring f.codomain := +begin + rw [is_noetherian_ring, is_noetherian_iff_well_founded] at h ⊢, + exact order_embedding.well_founded (f.order_embedding.dual) h +end + end localization_map namespace localization @@ -1075,8 +1086,8 @@ begin exact hM c.2 a hc, end -protected lemma to_map_ne_zero_of_mem_non_zero_divisors {M : submonoid A} (f : localization_map M S) - (hM : M ≤ non_zero_divisors A) (x : non_zero_divisors A) : f.to_map x ≠ 0 := +protected lemma to_map_ne_zero_of_mem_non_zero_divisors [nontrivial R] (f : localization_map M S) + (hM : M ≤ non_zero_divisors R) (x : non_zero_divisors R) : f.to_map x ≠ 0 := map_ne_zero_of_mem_non_zero_divisors (f.injective hM) /-- A `comm_ring` `S` which is the localization of an integral domain `R` at a subset of @@ -1173,8 +1184,8 @@ protected theorem injective [comm_ring K] (φ : fraction_map R K) : function.injective φ.to_map := φ.injective (le_of_eq rfl) -protected lemma to_map_ne_zero_of_mem_non_zero_divisors [comm_ring K] (φ : fraction_map A K) - (x : non_zero_divisors A) : φ.to_map x ≠ 0 := +protected lemma to_map_ne_zero_of_mem_non_zero_divisors [nontrivial R] [comm_ring K] + (φ : fraction_map R K) (x : non_zero_divisors R) : φ.to_map x ≠ 0 := φ.to_map_ne_zero_of_mem_non_zero_divisors (le_of_eq rfl) x /-- A `comm_ring` `K` which is the localization of an integral domain `R` at `R - {0}` is an @@ -1474,7 +1485,7 @@ end is_integral namespace integral_closure -variables {L : Type*} [field K] [field L] {f : fraction_map A K} +variables {L : Type*} [field K] [field L] (f : fraction_map A K) open algebra @@ -1493,6 +1504,8 @@ def fraction_map_of_algebraic [algebra A L] (alg : is_algebraic A L) λ ⟨c, hc⟩, congr_arg (algebra_map _ L) (mul_right_cancel' (mem_non_zero_divisors_iff_ne_zero.mp c.2) hc) ⟩) +variables {K} (L) + /-- If the field `L` is a finite extension of the fraction field of the integral domain `A`, the integral closure of `A` in `L` has fraction field `L`. -/ def fraction_map_of_finite_extension [algebra A L] [algebra f.codomain L] @@ -1535,4 +1548,7 @@ noncomputable def alg_equiv_of_quotient {K : Type*} [field K] (f : fraction_map fraction_ring A ≃ₐ[A] f.codomain := localization.alg_equiv_of_quotient f +instance : algebra A (fraction_ring A) := +(of A).to_map.to_algebra + end fraction_ring