feat(ring_theory): define integrally closed domains (#8893)

In this follow-up to #8882, we define the notion of an integrally closed domain `R`, which contains all integral elements of `Frac(R)`.
We show the equivalence to `is_integral_closure R R K` for a field of fractions `K`.
We provide instances for `is_dedekind_domain`s, `unique_fractorization_monoid`s, and to the integers of a valuation. In particular, the rational root theorem provides a proof that `ℤ` is integrally closed.



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

src/algebra/algebra/basic.lean

@@ -603,6 +603,10 @@ def snd : A × B →ₐ[R] B :=
 
 end prod
 
+lemma algebra_map_eq_apply (f : A →ₐ[R] B) {y : R} {x : A} (h : algebra_map R A y = x) :
+  algebra_map R B y = f x :=
+h ▸ (f.commutes _).symm
+
 end semiring
 
 section comm_semiring
@@ -1031,6 +1035,11 @@ instance apply_smul_comm_class : smul_comm_class R (A₁ ≃ₐ[R] A₁) A₁ :=
 instance apply_smul_comm_class' : smul_comm_class (A₁ ≃ₐ[R] A₁) R A₁ :=
 { smul_comm := λ e r a, (e.to_linear_equiv.map_smul r a) }
 
+@[simp] lemma algebra_map_eq_apply (e : A₁ ≃ₐ[R] A₂) {y : R} {x : A₁} :
+  (algebra_map R A₂ y = e x) ↔ (algebra_map R A₁ y = x) :=
+⟨λ h, by simpa using e.symm.to_alg_hom.algebra_map_eq_apply h,
+ λ h, e.to_alg_hom.algebra_map_eq_apply h⟩
+
 end semiring
 
 section comm_semiring

src/ring_theory/dedekind_domain.lean

@@ -6,6 +6,7 @@ Authors: Kenji Nakagawa, Anne Baanen, Filippo A. E. Nuccio
 import ring_theory.discrete_valuation_ring
 import ring_theory.fractional_ideal
 import ring_theory.ideal.over
+import ring_theory.integrally_closed
 
 /-!
 # Dedekind domains
@@ -84,21 +85,20 @@ TODO: Prove that these are actually equivalent definitions.
 class is_dedekind_domain : Prop :=
 (is_noetherian_ring : is_noetherian_ring A)
 (dimension_le_one : dimension_le_one A)
-(is_integrally_closed : integral_closure A (fraction_ring A) = ⊥)
+(is_integrally_closed : is_integrally_closed A)
 
 -- See library note [lower instance priority]
-attribute [instance, priority 100] is_dedekind_domain.is_noetherian_ring
+attribute [instance, priority 100]
+  is_dedekind_domain.is_noetherian_ring is_dedekind_domain.is_integrally_closed
 
-/-- An integral domain is a Dedekind domain iff and only if it is not a field, is
+/-- An integral domain is a Dedekind domain iff and only if it is
 Noetherian, has dimension ≤ 1, and is integrally closed in a given fraction field.
 In particular, this definition does not depend on the choice of this fraction field. -/
 lemma is_dedekind_domain_iff (K : Type*) [field K] [algebra A K] [is_fraction_ring A K] :
-  is_dedekind_domain A ↔
-    is_noetherian_ring A ∧ dimension_le_one A ∧ integral_closure A K = ⊥ :=
-⟨λ ⟨hr, hd, hi⟩, ⟨hr, hd,
-  by rw [←integral_closure_map_alg_equiv (fraction_ring.alg_equiv A K), hi, algebra.map_bot]⟩,
- λ ⟨hr, hd, hi⟩, ⟨hr, hd,
-  by rw [←integral_closure_map_alg_equiv (fraction_ring.alg_equiv A K).symm, hi, algebra.map_bot]⟩⟩
+  is_dedekind_domain A ↔ is_noetherian_ring A ∧ dimension_le_one A ∧
+    (∀ {x : K}, is_integral A x → ∃ y, algebra_map A K y = x) :=
+⟨λ ⟨hr, hd, hi⟩, ⟨hr, hd, λ x, (is_integrally_closed_iff K).mp hi⟩,
+ λ ⟨hr, hd, hi⟩, ⟨hr, hd, (is_integrally_closed_iff K).mpr @hi⟩⟩
 
 /--
 A Dedekind domain is an integral domain that is Noetherian, and the
@@ -315,13 +315,12 @@ begin
   exact I.fg_of_is_unit (is_fraction_ring.injective A (fraction_ring A)) (h.is_unit hI)
 end
 
-lemma integrally_closed : integral_closure A (fraction_ring A) = ⊥ :=
+lemma integrally_closed : is_integrally_closed A :=
 begin
-  rw eq_bot_iff,
   -- It suffices to show that for integral `x`,
   -- `A[x]` (which is a fractional ideal) is in fact equal to `A`.
-  rintros x hx,
-  rw [← subalgebra.mem_to_submodule, algebra.to_submodule_bot,
+  refine ⟨λ x hx, _⟩,
+  rw [← set.mem_range, ← algebra.mem_bot, ← subalgebra.mem_to_submodule, algebra.to_submodule_bot,
       ← coe_span_singleton A⁰ (1 : fraction_ring A), fractional_ideal.span_singleton_one,
       ← fractional_ideal.adjoin_integral_eq_one_of_is_unit x hx (h.is_unit _)],
   { exact mem_adjoin_integral_self A⁰ x hx },
@@ -531,7 +530,7 @@ begin
   intros x hx,
   -- In particular, we'll show all `x ∈ J⁻¹` are integral.
   suffices : x ∈ integral_closure A K,
-  { rwa [((is_dedekind_domain_iff _ _).mp h).2.2, algebra.mem_bot, set.mem_range,
+  { rwa [is_integrally_closed.integral_closure_eq_bot, algebra.mem_bot, set.mem_range,
          ← fractional_ideal.mem_one_iff] at this;
       assumption },
   -- For that, we'll find a subalgebra that is f.g. as a module and contains `x`.

src/ring_theory/integral_closure.lean

@@ -114,6 +114,10 @@ theorem is_integral_alg_hom (f : A →ₐ[R] B) {x : A} (hx : is_integral R x) :
 let ⟨p, hp, hpx⟩ :=
 hx in ⟨p, hp, by rw [← aeval_def, aeval_alg_hom_apply, aeval_def, hpx, f.map_zero]⟩
 
+@[simp]
+theorem is_integral_alg_equiv (f : A ≃ₐ[R] B) {x : A} : is_integral R (f x) ↔ is_integral R x :=
+⟨λ h, by simpa using is_integral_alg_hom f.symm.to_alg_hom h, is_integral_alg_hom f.to_alg_hom⟩
+
 theorem is_integral_of_is_scalar_tower [algebra A B] [is_scalar_tower R A B]
   (x : B) (hx : is_integral R x) : is_integral A x :=
 let ⟨p, hp, hpx⟩ := hx in

src/ring_theory/integrally_closed.lean

@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2021 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+import ring_theory.integral_closure
+import ring_theory.localization
+
+/-!
+# Integrally closed rings
+
+An integrally closed domain `R` contains all the elements of `Frac(R)` that are
+integral over `R`. A special case of integrally closed domains are the Dedekind domains.
+
+## Main definitions
+
+* `is_integrally_closed R` states `R` contains all integral elements of `Frac(R)`
+
+## Main results
+
+* `is_integrally_closed_iff K`, where `K` is a fraction field of `R`, states `R`
+  is integrally closed iff it is the integral closure of `R` in `K`
+-/
+
+open_locale non_zero_divisors
+
+/-- `R` is integrally closed if all integral elements of `Frac(R)` are also elements of `R`.
+
+This definition uses `fraction_ring R` to denote `Frac(R)`. See `is_integrally_closed_iff`
+if you want to choose another field of fractions for `R`.
+-/
+class is_integrally_closed (R : Type*) [integral_domain R] : Prop :=
+(algebra_map_eq_of_integral :
+  ∀ {x : fraction_ring R}, is_integral R x → ∃ y, algebra_map R (fraction_ring R) y = x)
+
+section iff
+
+variables {R : Type*} [integral_domain R] (K : Type*) [field K] [algebra R K] [is_fraction_ring R K]
+
+/-- `R` is integrally closed iff all integral elements of its fraction field `K`
+are also elements of `R`. -/
+theorem is_integrally_closed_iff :
+  is_integrally_closed R ↔ ∀ {x : K}, is_integral R x → ∃ y, algebra_map R K y = x :=
+begin
+  let e : K ≃ₐ[R] fraction_ring R := is_localization.alg_equiv R⁰_ _,
+  split,
+  { rintros ⟨cl⟩,
+    refine λ x hx, _,
+    obtain ⟨y, hy⟩ := cl ((is_integral_alg_equiv e).mpr hx),
+    exact ⟨y, e.algebra_map_eq_apply.mp hy⟩ },
+  { rintros cl,
+    refine ⟨λ x hx, _⟩,
+    obtain ⟨y, hy⟩ := cl ((is_integral_alg_equiv e.symm).mpr hx),
+    exact ⟨y, e.symm.algebra_map_eq_apply.mp hy⟩ },
+end
+
+/-- `R` is integrally closed iff it is the integral closure of itself in its field of fractions. -/
+theorem is_integrally_closed_iff_is_integral_closure :
+  is_integrally_closed R ↔ is_integral_closure R R K :=
+(is_integrally_closed_iff K).trans $
+begin
+  let e : K ≃ₐ[R] fraction_ring R := is_localization.alg_equiv R⁰_ _,
+  split,
+  { intros cl,
+    refine ⟨is_fraction_ring.injective _ _, λ x, ⟨cl, _⟩⟩,
+    rintros ⟨y, y_eq⟩,
+    rw ← y_eq,
+    exact is_integral_algebra_map },
+  { rintros ⟨-, cl⟩ x hx,
+    exact cl.mp hx }
+end
+
+end iff
+
+namespace is_integrally_closed
+
+variables {R : Type*} [integral_domain R] [iic : is_integrally_closed R]
+variables {K : Type*} [field K] [algebra R K] [is_fraction_ring R K]
+
+instance : is_integral_closure R R K :=
+(is_integrally_closed_iff_is_integral_closure K).mp iic
+
+include iic
+
+lemma is_integral_iff {x : K} : is_integral R x ↔ ∃ y, algebra_map R K y = x :=
+is_integral_closure.is_integral_iff
+
+omit iic
+variables {R} (K)
+lemma integral_closure_eq_bot_iff :
+  integral_closure R K = ⊥ ↔ is_integrally_closed R :=
+begin
+  refine eq_bot_iff.trans _,
+  split,
+  { rw is_integrally_closed_iff K,
+    intros h x hx,
+    exact set.mem_range.mp (algebra.mem_bot.mp (h hx)),
+    assumption },
+  { intros h x hx,
+    rw [algebra.mem_bot, set.mem_range],
+    exactI is_integral_iff.mp hx },
+end
+
+include iic
+variables (R K)
+@[simp] lemma integral_closure_eq_bot : integral_closure R K = ⊥ :=
+(integral_closure_eq_bot_iff K).mpr ‹_›
+
+end is_integrally_closed

src/ring_theory/polynomial/rational_root.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 
+import ring_theory.integrally_closed
 import ring_theory.polynomial.scale_roots
-import ring_theory.localization
 
 /-!
 # Rational root theorem and integral root theorem
@@ -122,8 +122,9 @@ lemma integer_of_integral {x : K} :
   is_integral A x → is_integer A x :=
 λ ⟨p, hp, hx⟩, is_integer_of_is_root_of_monic hp hx
 
-lemma integrally_closed : integral_closure A K = ⊥ :=
-eq_bot_iff.mpr (λ x hx, algebra.mem_bot.mpr (integer_of_integral hx))
+@[priority 100] -- See library note [lower instance priority]
+instance : is_integrally_closed A :=
+⟨λ x, integer_of_integral⟩
 
 end unique_factorization_monoid
 

src/ring_theory/valuation/integral.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 
-import ring_theory.integral_closure
+import ring_theory.integrally_closed
 import ring_theory.valuation.integers
 
 /-!
@@ -46,6 +46,17 @@ bot_unique $ λ r hr, let ⟨x, hx⟩ := hv.3 (hv.mem_of_integral hr) in algebra
 
 end comm_ring
 
+section fraction_field
+
+variables {K : Type u} {Γ₀ : Type v} [field K] [linear_ordered_comm_group_with_zero Γ₀]
+variables {v : valuation K Γ₀} {O : Type w} [integral_domain O] [algebra O K] [is_fraction_ring O K]
+variables (hv : integers v O)
+
+lemma integrally_closed : is_integrally_closed O :=
+(is_integrally_closed.integral_closure_eq_bot_iff K).mp (valuation.integers.integral_closure hv)
+
+end fraction_field
+
 end integers
 
 end valuation