refactor(RingTheory/IntegrallyClosed): generalize to `IsIntegrallyClo…

…sedIn` (#7857)

This refactor adds a new definition `IsIntegrallyClosedIn R A` equal to `IsIntegralClosure R A A`, and redefines `IsIntegrallyClosed R` to equal `IsIntegrallyClosed R (FractionRing A)`. This should make it possible and convenient to generalize away from the fraction fields.

This also more closely approximates the conventions of the Stacks project.

This is a second attempt at the refactor, after #7116 which was much more messy.

Mathlib/Algebra/GCDMonoid/IntegrallyClosed.lean

@@ -32,7 +32,7 @@ theorem IsLocalization.surj_of_gcd_domain [GCDMonoid R] (M : Submonoid R) [IsLoc
 
 instance (priority := 100) GCDMonoid.toIsIntegrallyClosed
     [h : Nonempty (GCDMonoid R)] : IsIntegrallyClosed R :=
-  ⟨fun {X} ⟨p, hp₁, hp₂⟩ => by
+  (isIntegrallyClosed_iff (FractionRing R)).mpr fun {X} ⟨p, hp₁, hp₂⟩ => by
     cases h
     obtain ⟨x, y, hg, he⟩ := IsLocalization.surj_of_gcd_domain (nonZeroDivisors R) X
     have :=
@@ -45,5 +45,5 @@ instance (priority := 100) GCDMonoid.toIsIntegrallyClosed
           (gcd_pow_left_dvd_pow_gcd.trans <| pow_dvd_pow_of_dvd (isUnit_iff_dvd_one.1 hg) _)
     use x * (this.unit⁻¹ : _)
     erw [map_mul, ← Units.coe_map_inv, eq_comm, Units.eq_mul_inv_iff_mul_eq]
-    exact he⟩
+    exact he
 #align gcd_monoid.to_is_integrally_closed GCDMonoid.toIsIntegrallyClosed

Mathlib/RingTheory/DedekindDomain/Basic.lean

@@ -105,7 +105,7 @@ The integral closure condition is independent of the choice of field of fraction
 use `isDedekindRing_iff` to prove `IsDedekindRing` for a given `fraction_map`.
 -/
 class IsDedekindRing
-  extends IsNoetherian A A, DimensionLEOne A, IsIntegrallyClosed A : Prop
+  extends IsNoetherian A A, DimensionLEOne A, IsIntegralClosure A A (FractionRing A) : Prop
 
 /-- An integral domain is a Dedekind domain if and only if it is
 Noetherian, has dimension ≤ 1, and is integrally closed in a given fraction field.

Mathlib/RingTheory/DedekindDomain/Dvr.lean

@@ -102,7 +102,7 @@ theorem IsLocalization.isDedekindDomain [IsDedekindDomain A] {M : Submonoid A} (
   · exact Ring.DimensionLEOne.localization Aₘ hM
   · intro x hx
     obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _
-    obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp IsDedekindRing.toIsIntegrallyClosed hy
+    obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp IsDedekindRing.toIsIntegralClosure hy
     refine' ⟨IsLocalization.mk' Aₘ z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr _⟩
     rw [hz, ← Algebra.smul_def]
     rfl

Mathlib/RingTheory/DedekindDomain/Ideal.lean

@@ -294,7 +294,7 @@ theorem isNoetherianRing : IsNoetherianRing A := by
 theorem integrallyClosed : IsIntegrallyClosed A := by
   -- It suffices to show that for integral `x`,
   -- `A[x]` (which is a fractional ideal) is in fact equal to `A`.
-  refine ⟨fun {x hx} => ?_⟩
+  refine (isIntegrallyClosed_iff (FractionRing A)).mpr (fun {x hx} => ?_)
   rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot,
     Submodule.one_eq_span, ← coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ←
     FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (h.isUnit _)]

Mathlib/RingTheory/IntegralClosure.lean

@@ -879,6 +879,16 @@ protected theorem RingHom.IsIntegral.trans
   Algebra.IsIntegral.trans hf hg
 #align ring_hom.is_integral_trans RingHom.IsIntegral.trans
 
+/-- If `R → A → B` is an algebra tower, `C` is the integral closure of `R` in `B`
+and `A` is integral over `R`, then `C` is the integral closure of `A` in `B`. -/
+lemma IsIntegralClosure.tower_top {B C : Type*} [CommRing C] [CommRing B]
+    [Algebra R B] [Algebra A B] [Algebra C B] [IsScalarTower R A B]
+    [IsIntegralClosure C R B] (hRA : Algebra.IsIntegral R A) :
+    IsIntegralClosure C A B :=
+  ⟨IsIntegralClosure.algebraMap_injective _ R _,
+   fun hx => (IsIntegralClosure.isIntegral_iff).mp (isIntegral_trans hRA _ hx),
+   fun hx => ((IsIntegralClosure.isIntegral_iff (R := R)).mpr hx).tower_top⟩
+
 theorem RingHom.isIntegral_of_surjective (hf : Function.Surjective f) : f.IsIntegral :=
   fun x ↦ (hf x).recOn fun _y hy ↦ hy ▸ f.isIntegralElem_map
 #align ring_hom.is_integral_of_surjective RingHom.isIntegral_of_surjective

Mathlib/RingTheory/IntegrallyClosed.lean

@@ -16,114 +16,225 @@ integral over `R`. A special case of integrally closed rings are the Dedekind do
 
 ## Main definitions
 
+* `IsIntegrallyClosedIn R A` states `R` contains all integral elements of `A`
 * `IsIntegrallyClosed R` states `R` contains all integral elements of `Frac(R)`
 
 ## Main results
 
 * `isIntegrallyClosed_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`
+
+## TODO: Related notions
+
+The following definitions are closely related, especially in their applications in Mathlib.
+
+A *normal domain* is a domain that is integrally closed in its field of fractions.
+[Stacks: normal domain](https://stacks.math.columbia.edu/tag/037B#0309)
+Normal domains are the major use case of `IsIntegrallyClosed` at the time of writing, and we have
+quite a few results that can be moved wholesale to a new `NormalDomain` definition.
+In fact, before PR #6126 `IsIntegrallyClosed` was exactly defined to be a normal domain.
+(So you might want to copy some of its API when you define normal domains.)
+
+A normal ring means that localizations at all prime ideals are normal domains.
+[Stacks: normal ring](https://stacks.math.columbia.edu/tag/037B#00GV)
+This implies `IsIntegrallyClosed`,
+[Stacks: Tag 034M](https://stacks.math.columbia.edu/tag/037B#034M)
+but is equivalent to it only under some conditions (reduced + finitely many minimal primes),
+[Stacks: Tag 030C](https://stacks.math.columbia.edu/tag/037B#030C)
+in which case it's also equivalent to being a finite product of normal domains.
+
+We'd need to add these conditions if we want exactly the products of Dedekind domains.
+
+In fact noetherianity is sufficient to guarantee finitely many minimal primes, so `IsDedekindRing`
+could be defined as `IsReduced`, `IsNoetherian`, `Ring.DimensionLEOne`, and either
+`IsIntegrallyClosed` or `NormalDomain`. If we use `NormalDomain` then `IsReduced` is automatic,
+but we could also consider a version of `NormalDomain` that only requires the localizations are
+`IsIntegrallyClosed` but may not be domains, and that may not equivalent to the ring itself being
+`IsIntegallyClosed` (even for noetherian rings?).
 -/
 
 
 open scoped nonZeroDivisors Polynomial
 
 open Polynomial
 
+/-- `R` is integrally closed in `A` if all integral elements of `A` are also elements of `R`.
+-/
+abbrev IsIntegrallyClosedIn (R A : Type*) [CommRing R] [CommRing A] [Algebra R A] :=
+  IsIntegralClosure R R A
+
 /-- `R` is integrally closed if all integral elements of `Frac(R)` are also elements of `R`.
 
 This definition uses `FractionRing R` to denote `Frac(R)`. See `isIntegrallyClosed_iff`
 if you want to choose another field of fractions for `R`.
 -/
-class IsIntegrallyClosed (R : Type*) [CommRing R] : Prop where
-  /-- All integral elements of `Frac(R)` are also elements of `R`. -/
-  algebraMap_eq_of_integral :
-    ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, algebraMap R (FractionRing R) y = x
+abbrev IsIntegrallyClosed (R : Type*) [CommRing R] := IsIntegrallyClosedIn R (FractionRing R)
 #align is_integrally_closed IsIntegrallyClosed
 
 section Iff
 
 variable {R : Type*} [CommRing R]
+variable {A B : Type*} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
+
+/-- Being integrally closed is preserved under injective algebra homomorphisms. -/
+theorem AlgHom.isIntegrallyClosedIn (f : A →ₐ[R] B) (hf : Function.Injective f) :
+    IsIntegrallyClosedIn R B → IsIntegrallyClosedIn R A := by
+  rintro ⟨inj, cl⟩
+  refine ⟨Function.Injective.of_comp (f := f) ?_, fun hx => ?_, ?_⟩
+  · convert inj
+    aesop
+  · obtain ⟨y, fx_eq⟩ := cl.mp ((isIntegral_algHom_iff f hf).mpr hx)
+    aesop
+  · rintro ⟨y, rfl⟩
+    apply (isIntegral_algHom_iff f hf).mp
+    aesop
+
+/-- Being integrally closed is preserved under algebra isomorphisms. -/
+theorem AlgEquiv.isIntegrallyClosedIn (e : A ≃ₐ[R] B) :
+    IsIntegrallyClosedIn R A ↔ IsIntegrallyClosedIn R B :=
+  ⟨AlgHom.isIntegrallyClosedIn e.symm e.symm.injective, AlgHom.isIntegrallyClosedIn e e.injective⟩
+
 variable (K : Type*) [CommRing K] [Algebra R K] [IsFractionRing R K]
 
+/-- `R` is integrally closed iff it is the integral closure of itself in its field of fractions. -/
+theorem isIntegrallyClosed_iff_isIntegrallyClosedIn :
+    IsIntegrallyClosed R ↔ IsIntegrallyClosedIn R K :=
+  (IsLocalization.algEquiv R⁰ _ _).isIntegrallyClosedIn
+
+/-- `R` is integrally closed iff it is the integral closure of itself in its field of fractions. -/
+theorem isIntegrallyClosed_iff_isIntegralClosure : IsIntegrallyClosed R ↔ IsIntegralClosure R R K :=
+  isIntegrallyClosed_iff_isIntegrallyClosedIn K
+#align is_integrally_closed_iff_is_integral_closure isIntegrallyClosed_iff_isIntegralClosure
+
+/-- `R` is integrally closed in `A` iff all integral elements of `A` are also elements of `R`. -/
+theorem isIntegrallyClosedIn_iff {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] :
+    IsIntegrallyClosedIn R A ↔
+      Function.Injective (algebraMap R A) ∧
+        ∀ {x : A}, IsIntegral R x → ∃ y, algebraMap R A y = x := by
+  constructor
+  · rintro ⟨_, cl⟩
+    aesop
+  · rintro ⟨inj, cl⟩
+    refine ⟨inj, by aesop, ?_⟩
+    rintro ⟨y, rfl⟩
+    apply isIntegral_algebraMap
+
 /-- `R` is integrally closed iff all integral elements of its fraction field `K`
 are also elements of `R`. -/
 theorem isIntegrallyClosed_iff :
     IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, algebraMap R K y = x := by
-  let e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ _ _
-  constructor
-  · rintro ⟨cl⟩
-    refine' fun hx => _
-    obtain ⟨y, hy⟩ := cl ((isIntegral_algEquiv e).mpr hx)
-    exact ⟨y, e.algebraMap_eq_apply.mp hy⟩
-  · rintro cl
-    refine' ⟨fun hx => _⟩
-    obtain ⟨y, hy⟩ := cl ((isIntegral_algEquiv e.symm).mpr hx)
-    exact ⟨y, e.symm.algebraMap_eq_apply.mp hy⟩
+  simp [isIntegrallyClosed_iff_isIntegrallyClosedIn K, isIntegrallyClosedIn_iff,
+        IsFractionRing.injective R K]
 #align is_integrally_closed_iff isIntegrallyClosed_iff
 
-/-- `R` is integrally closed iff it is the integral closure of itself in its field of fractions. -/
-theorem isIntegrallyClosed_iff_isIntegralClosure : IsIntegrallyClosed R ↔ IsIntegralClosure R R K :=
-  (isIntegrallyClosed_iff K).trans <| by
-    constructor
-    · intro cl
-      refine' ⟨IsFractionRing.injective R K, ⟨cl, _⟩⟩
-      rintro ⟨y, y_eq⟩
-      rw [← y_eq]
-      exact isIntegral_algebraMap
-    · rintro ⟨-, cl⟩ x hx
-      exact cl.mp hx
-#align is_integrally_closed_iff_is_integral_closure isIntegrallyClosed_iff_isIntegralClosure
-
 end Iff
 
+namespace IsIntegrallyClosedIn
+
+variable {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] [iic : IsIntegrallyClosedIn R A]
+
+theorem algebraMap_eq_of_integral {x : A} : IsIntegral R x → ∃ y : R, algebraMap R A y = x :=
+  IsIntegralClosure.isIntegral_iff.mp
+
+theorem isIntegral_iff {x : A} : IsIntegral R x ↔ ∃ y : R, algebraMap R A y = x :=
+  IsIntegralClosure.isIntegral_iff
+
+theorem exists_algebraMap_eq_of_isIntegral_pow {x : A} {n : ℕ} (hn : 0 < n)
+    (hx : IsIntegral R <| x ^ n) : ∃ y : R, algebraMap R A y = x :=
+  isIntegral_iff.mp <| hx.of_pow hn
+
+theorem exists_algebraMap_eq_of_pow_mem_subalgebra {A : Type*} [CommRing A] [Algebra R A]
+    {S : Subalgebra R A} [IsIntegrallyClosedIn S A] {x : A} {n : ℕ} (hn : 0 < n)
+    (hx : x ^ n ∈ S) : ∃ y : S, algebraMap S A y = x :=
+  exists_algebraMap_eq_of_isIntegral_pow hn <| isIntegral_iff.mpr ⟨⟨x ^ n, hx⟩, rfl⟩
+
+variable (A)
+
+theorem integralClosure_eq_bot_iff (hRA : Function.Injective (algebraMap R A)) :
+    integralClosure R A = ⊥ ↔ IsIntegrallyClosedIn R A := by
+  refine eq_bot_iff.trans ?_
+  constructor
+  · intro h
+    refine ⟨ hRA, fun hx => Set.mem_range.mp (Algebra.mem_bot.mp (h hx)), ?_⟩
+    · rintro ⟨y, rfl⟩
+      apply isIntegral_algebraMap
+  · intro h x hx
+    rw [Algebra.mem_bot, Set.mem_range]
+    exact isIntegral_iff.mp hx
+
+variable (R)
+
+@[simp]
+theorem integralClosure_eq_bot [NoZeroSMulDivisors R A] [Nontrivial A] : integralClosure R A = ⊥ :=
+  (integralClosure_eq_bot_iff A (NoZeroSMulDivisors.algebraMap_injective _ _)).mpr ‹_›
+
+variable {A} {B : Type*} [CommRing B]
+
+/-- If `R` is the integral closure of `S` in `A`, then it is integrally closed in `A`. -/
+lemma of_isIntegralClosure [Algebra R B] [Algebra A B] [IsScalarTower R A B]
+    [IsIntegralClosure A R B] :
+    IsIntegrallyClosedIn A B :=
+  IsIntegralClosure.tower_top (IsIntegralClosure.isIntegral R B)
+
+variable {R}
+
+lemma _root_.IsIntegralClosure.of_isIntegrallyClosedIn
+    [Algebra R B] [Algebra A B] [IsScalarTower R A B]
+    [IsIntegrallyClosedIn A B] (hRA : Algebra.IsIntegral R A) :
+    IsIntegralClosure A R B := by
+  refine ⟨IsIntegralClosure.algebraMap_injective _ A _, fun {x} ↦
+    ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (IsIntegral.tower_top (A := A) hx), ?_⟩⟩
+  rintro ⟨y, rfl⟩
+  exact IsIntegral.map (IsScalarTower.toAlgHom A A B) (hRA y)
+
+end IsIntegrallyClosedIn
+
 namespace IsIntegrallyClosed
 
 variable {R S : Type*} [CommRing R] [CommRing S] [id : IsDomain R] [iic : IsIntegrallyClosed R]
 variable {K : Type*} [CommRing K] [Algebra R K] [ifr : IsFractionRing R K]
 
+/-- Note that this is not a duplicate instance, since `IsIntegrallyClosed R` is instead defined
+as `IsIntegrallyClosed R R (FractionRing R)`. -/
 instance : IsIntegralClosure R R K :=
   (isIntegrallyClosed_iff_isIntegralClosure K).mp iic
 
+theorem algebraMap_eq_of_integral {x : K} : IsIntegral R x → ∃ y : R, algebraMap R K y = x :=
+  IsIntegralClosure.isIntegral_iff.mp
+
 theorem isIntegral_iff {x : K} : IsIntegral R x ↔ ∃ y : R, algebraMap R K y = x :=
-  IsIntegralClosure.isIntegral_iff
+  IsIntegrallyClosedIn.isIntegral_iff
 #align is_integrally_closed.is_integral_iff IsIntegrallyClosed.isIntegral_iff
 
 theorem exists_algebraMap_eq_of_isIntegral_pow {x : K} {n : ℕ} (hn : 0 < n)
     (hx : IsIntegral R <| x ^ n) : ∃ y : R, algebraMap R K y = x :=
-  isIntegral_iff.mp <| hx.of_pow hn
+  IsIntegrallyClosedIn.exists_algebraMap_eq_of_isIntegral_pow hn hx
 #align is_integrally_closed.exists_algebra_map_eq_of_is_integral_pow IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow
 
 theorem exists_algebraMap_eq_of_pow_mem_subalgebra {K : Type*} [CommRing K] [Algebra R K]
     {S : Subalgebra R K} [IsIntegrallyClosed S] [IsFractionRing S K] {x : K} {n : ℕ} (hn : 0 < n)
     (hx : x ^ n ∈ S) : ∃ y : S, algebraMap S K y = x :=
-  exists_algebraMap_eq_of_isIntegral_pow hn <| isIntegral_iff.mpr ⟨⟨x ^ n, hx⟩, rfl⟩
+  IsIntegrallyClosedIn.exists_algebraMap_eq_of_pow_mem_subalgebra hn hx
 #align is_integrally_closed.exists_algebra_map_eq_of_pow_mem_subalgebra IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebra
 
 variable (R S K)
 
 lemma _root_.IsIntegralClosure.of_isIntegrallyClosed
     [Algebra S R] [Algebra S K] [IsScalarTower S R K] (hRS : Algebra.IsIntegral S R) :
-    IsIntegralClosure R S K := by
-  refine ⟨IsLocalization.injective _ le_rfl, fun {x} ↦
-    ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (IsIntegral.tower_top (A := R) hx), ?_⟩⟩
-  rintro ⟨y, rfl⟩
-  exact IsIntegral.map (IsScalarTower.toAlgHom S R K) (hRS y)
+    IsIntegralClosure R S K :=
+  IsIntegralClosure.of_isIntegrallyClosedIn hRS
 
 variable {R}
 
-theorem integralClosure_eq_bot_iff : integralClosure R K = ⊥ ↔ IsIntegrallyClosed R := by
-  refine' eq_bot_iff.trans _
-  constructor
-  · rw [isIntegrallyClosed_iff K]
-    intro h x hx
-    exact Set.mem_range.mp (Algebra.mem_bot.mp (h hx))
-  · intro h x hx
-    rw [Algebra.mem_bot, Set.mem_range]
-    exact isIntegral_iff.mp hx
+theorem integralClosure_eq_bot_iff : integralClosure R K = ⊥ ↔ IsIntegrallyClosed R :=
+  (IsIntegrallyClosedIn.integralClosure_eq_bot_iff _ (IsFractionRing.injective _ _)).trans
+    (isIntegrallyClosed_iff_isIntegrallyClosedIn _).symm
 #align is_integrally_closed.integral_closure_eq_bot_iff IsIntegrallyClosed.integralClosure_eq_bot_iff
 
 variable (R)
 
+/-- This is almost a duplicate of `IsIntegrallyClosedIn.integralClosure_eq_bot`,
+except the `NoZeroSMulDivisors` hypothesis isn't inferred automatically from `IsFractionRing`. -/
 @[simp]
 theorem integralClosure_eq_bot : integralClosure R K = ⊥ :=
   (integralClosure_eq_bot_iff K).mpr ‹_›

Mathlib/RingTheory/Polynomial/RationalRoot.lean

@@ -129,7 +129,7 @@ theorem integer_of_integral {x : K} : IsIntegral A x → IsInteger A x := fun 
 
 -- See library note [lower instance priority]
 instance (priority := 100) instIsIntegrallyClosed : IsIntegrallyClosed A :=
-  ⟨fun {_} => integer_of_integral⟩
+  (isIntegrallyClosed_iff (FractionRing A)).mpr fun {_} => integer_of_integral
 #align unique_factorization_monoid.is_integrally_closed UniqueFactorizationMonoid.instIsIntegrallyClosed
 
 end UniqueFactorizationMonoid