refactor: generalize IsIntegrallyClosed away from fraction fields

Mathlib/Algebra/GCDMonoid/IntegrallyClosed.lean

@@ -30,11 +30,13 @@ theorem IsLocalization.surj_of_gcd_domain (M : Submonoid R) [IsLocalization M A]
   rw [Subtype.coe_mk, hy', ← mul_comm y', mul_assoc]; conv_lhs => rw [hx']
 #align is_localization.surj_of_gcd_domain IsLocalization.surj_of_gcd_domain
 
-instance (priority := 100) GCDMonoid.toIsIntegrallyClosed : IsIntegrallyClosed R :=
+variable [IsFractionRing R A]
+
+instance (priority := 100) GCDMonoid.toIsIntegrallyClosed : IsIntegrallyClosed R A :=
   ⟨fun {X} ⟨p, hp₁, hp₂⟩ => by
     obtain ⟨x, y, hg, he⟩ := IsLocalization.surj_of_gcd_domain (nonZeroDivisors R) X
     have :=
-      Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero (IsFractionRing.injective R <| FractionRing R)
+      Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero (IsFractionRing.injective R A)
         hp₁ y x _ hp₂ (by rw [mul_comm, he])
     have : IsUnit y := by
       rw [isUnit_iff_dvd_one, ← one_pow]

Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

@@ -42,7 +42,7 @@ section
 variable (K L : Type*) [Field K] [Algebra R K] [IsFractionRing R K] [Field L] [Algebra R L]
   [Algebra S L] [Algebra K L] [IsScalarTower R K L] [IsScalarTower R S L]
 
-variable [IsIntegrallyClosed R]
+variable [IsIntegrallyClosed R K]
 
 /-- For integrally closed domains, the minimal polynomial over the ring is the same as the minimal
 polynomial over the fraction field. See `minpoly.isIntegrallyClosed_eq_field_fractions'` if
@@ -71,7 +71,7 @@ end
 
 variable [IsDomain S] [NoZeroSMulDivisors R S]
 
-variable [IsIntegrallyClosed R]
+variable [IsIntegrallyClosed R (FractionRing R)]
 
 /-- For integrally closed rings, the minimal polynomial divides any polynomial that has the
   integral element as root. See also `minpoly.dvd` which relaxes the assumptions on `S`

Mathlib/NumberTheory/FunctionField.lean

@@ -132,8 +132,8 @@ variable [FunctionField Fq F]
 instance : IsFractionRing (ringOfIntegers Fq F) F :=
   integralClosure.isFractionRing_of_finite_extension (RatFunc Fq) F
 
-instance : IsIntegrallyClosed (ringOfIntegers Fq F) :=
-  integralClosure.isIntegrallyClosedOfFiniteExtension (RatFunc Fq)
+instance : IsIntegrallyClosed (ringOfIntegers Fq F) F :=
+  integralClosure.isIntegrallyClosed
 
 instance [IsSeparable (RatFunc Fq) F] : IsNoetherian Fq[X] (ringOfIntegers Fq F) :=
   IsIntegralClosure.isNoetherian _ (RatFunc Fq) F _

Mathlib/NumberTheory/KummerDedekind.lean

@@ -214,7 +214,7 @@ namespace KummerDedekind
 
 open scoped BigOperators Polynomial Classical
 
-variable [IsDomain R] [IsIntegrallyClosed R]
+variable [IsDomain R] [IsIntegrallyClosed R (FractionRing R)]
 
 variable [IsDomain S] [IsDedekindDomain S]
 

Mathlib/NumberTheory/NumberField/Basic.lean

@@ -105,8 +105,8 @@ instance [NumberField K] : IsFractionRing (𝓞 K) K :=
 instance : IsIntegralClosure (𝓞 K) ℤ K :=
   integralClosure.isIntegralClosure _ _
 
-instance [NumberField K] : IsIntegrallyClosed (𝓞 K) :=
-  integralClosure.isIntegrallyClosedOfFiniteExtension ℚ
+instance [NumberField K] : IsIntegrallyClosed (𝓞 K) K :=
+  integralClosure.isIntegrallyClosed
 
 theorem isIntegral_coe (x : 𝓞 K) : IsIntegral ℤ (x : K) :=
   x.2

Mathlib/RingTheory/Bezout.lean

@@ -97,7 +97,8 @@ attribute [local instance] toGCDDomain
 
 -- Note that the proof depends on the `local attribute [instance]` above, and is thus necessary to
 -- be stated.
-instance (priority := 100) [IsDomain R] [IsBezout R] : IsIntegrallyClosed R := by
+instance (priority := 100) {K : Type*} [Field K] [Algebra R K]
+    [IsDomain R] [IsBezout R] [IsFractionRing R K] : IsIntegrallyClosed R K := by
   classical exact GCDMonoid.toIsIntegrallyClosed
 
 theorem _root_.Function.Surjective.isBezout {S : Type v} [CommRing S] (f : R →+* S)

Mathlib/RingTheory/DedekindDomain/Basic.lean

@@ -103,9 +103,17 @@ This is the default implementation, but there are equivalent definitions,
 TODO: Prove that these are actually equivalent definitions.
 -/
 class IsDedekindDomain
-  extends IsDomain A, IsNoetherian A A, DimensionLEOne A, IsIntegrallyClosed A : Prop
+  extends IsDomain A, IsNoetherian A A, DimensionLEOne A, IsIntegrallyClosed A (FractionRing A) :
+  Prop
 #align is_dedekind_domain IsDedekindDomain
 
+/--
+A Dedekind domain is integrally closed, for any choice for field of fractions.
+-/
+theorem IsDedekindDomain.isIntegrallyClosed (K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
+    [IsDedekindDomain A] : IsIntegrallyClosed A K :=
+  (IsLocalization.algEquiv A⁰ _ K).isIntegrallyClosed_iff.mp IsDedekindDomain.toIsIntegrallyClosed
+
 /-- 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. -/
@@ -114,8 +122,8 @@ theorem isDedekindDomain_iff (K : Type*) [Field K] [Algebra A K] [IsFractionRing
       IsDomain A ∧ IsNoetherianRing A ∧ DimensionLEOne A ∧
         ∀ {x : K}, IsIntegral A x → ∃ y, algebraMap A K y = x :=
   ⟨fun _ => ⟨inferInstance, inferInstance, inferInstance,
-             fun {_} => (isIntegrallyClosed_iff K).mp inferInstance⟩,
-   fun ⟨hid, hr, hd, hi⟩ => { hid, hr, hd, (isIntegrallyClosed_iff K).mpr @hi with }⟩
+             fun {_} => (isIntegrallyClosed_fractionRing_iff (FractionRing A) K).mp inferInstance⟩,
+   fun ⟨hid, hr, hd, hi⟩ => { hid, hr, hd, (isIntegrallyClosed_fractionRing_iff _ K).mpr @hi with }⟩
 #align is_dedekind_domain_iff isDedekindDomain_iff
 
 -- See library note [lower instance priority]

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 IsDedekindDomain.toIsIntegrallyClosed hy
+    obtain ⟨z, hz⟩ := (IsIntegrallyClosed_iff _ _).mp IsDedekindDomain.toIsIntegrallyClosed 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

@@ -293,12 +293,12 @@ theorem isNoetherianRing : IsNoetherianRing A := by
   exact I.fg_of_isUnit (IsFractionRing.injective A (FractionRing A)) (h.isUnit hI)
 #align is_dedekind_domain_inv.is_noetherian_ring IsDedekindDomainInv.isNoetherianRing
 
-theorem integrallyClosed : IsIntegrallyClosed A := by
+theorem integrallyClosed : IsIntegrallyClosed A K := 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} => ?_⟩
-  rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot, ←
-    coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ←
+  rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot,
+    ← coe_spanSingleton A⁰ (1 : K), spanSingleton_one, ←
     FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (h.isUnit _)]
   · exact mem_adjoinIntegral_self A⁰ x hx
   · exact fun h => one_ne_zero (eq_zero_iff.mp h 1 (Algebra.adjoin A {x}).one_mem)
@@ -492,6 +492,7 @@ theorem coe_ideal_mul_inv [h : IsDedekindDomain A] (I : Ideal A) (hI0 : I ≠ 
   · rw [hJ0, inv_zero']; exact zero_le _
   intro x hx
   -- In particular, we'll show all `x ∈ J⁻¹` are integral.
+  have := IsDedekindDomain.isIntegrallyClosed A K
   suffices x ∈ integralClosure A K by
     rwa [IsIntegrallyClosed.integralClosure_eq_bot, Algebra.mem_bot, Set.mem_range,
       ← mem_one_iff] at this

Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

@@ -93,7 +93,7 @@ variable [FiniteDimensional K L]
 variable {A K L}
 
 theorem IsIntegralClosure.range_le_span_dualBasis [IsSeparable K L] {ι : Type*} [Fintype ι]
-    [DecidableEq ι] (b : Basis ι K L) (hb_int : ∀ i, IsIntegral A (b i)) [IsIntegrallyClosed A] :
+    [DecidableEq ι] (b : Basis ι K L) (hb_int : ∀ i, IsIntegral A (b i)) [IsIntegrallyClosed A K] :
     LinearMap.range ((Algebra.linearMap C L).restrictScalars A) ≤
     Submodule.span A (Set.range <| (traceForm K L).dualBasis (traceForm_nondegenerate K L) b) := by
   let db := (traceForm K L).dualBasis (traceForm_nondegenerate K L) b
@@ -119,7 +119,7 @@ theorem IsIntegralClosure.range_le_span_dualBasis [IsSeparable K L] {ι : Type*}
 #align is_integral_closure.range_le_span_dual_basis IsIntegralClosure.range_le_span_dualBasis
 
 theorem integralClosure_le_span_dualBasis [IsSeparable K L] {ι : Type*} [Fintype ι] [DecidableEq ι]
-    (b : Basis ι K L) (hb_int : ∀ i, IsIntegral A (b i)) [IsIntegrallyClosed A] :
+    (b : Basis ι K L) (hb_int : ∀ i, IsIntegral A (b i)) [IsIntegrallyClosed A K] :
     Subalgebra.toSubmodule (integralClosure A L) ≤
     Submodule.span A (Set.range <| (traceForm K L).dualBasis (traceForm_nondegenerate K L) b) := by
   refine' le_trans _ (IsIntegralClosure.range_le_span_dualBasis (integralClosure A L) b hb_int)
@@ -187,7 +187,7 @@ variable [IsSeparable K L]
 /- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is
 integrally closed and Noetherian, the integral closure `C` of `A` in `L` is
 Noetherian over `A`. -/
-theorem IsIntegralClosure.isNoetherian [IsIntegrallyClosed A] [IsNoetherianRing A] :
+theorem IsIntegralClosure.isNoetherian [IsIntegrallyClosed A K] [IsNoetherianRing A] :
     IsNoetherian A C := by
   haveI := Classical.decEq L
   obtain ⟨s, b, hb_int⟩ := FiniteDimensional.exists_is_basis_integral A K L
@@ -204,7 +204,7 @@ theorem IsIntegralClosure.isNoetherian [IsIntegrallyClosed A] [IsNoetherianRing
 /- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is
 integrally closed and Noetherian, the integral closure `C` of `A` in `L` is
 Noetherian. -/
-theorem IsIntegralClosure.isNoetherianRing [IsIntegrallyClosed A] [IsNoetherianRing A] :
+theorem IsIntegralClosure.isNoetherianRing [IsIntegrallyClosed A K] [IsNoetherianRing A] :
     IsNoetherianRing C :=
   isNoetherianRing_iff.mpr <| isNoetherian_of_tower A (IsIntegralClosure.isNoetherian A K L C)
 #align is_integral_closure.is_noetherian_ring IsIntegralClosure.isNoetherianRing
@@ -237,7 +237,7 @@ variable {A K}
 /- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is
 integrally closed and Noetherian, the integral closure of `A` in `L` is
 Noetherian. -/
-theorem integralClosure.isNoetherianRing [IsIntegrallyClosed A] [IsNoetherianRing A] :
+theorem integralClosure.isNoetherianRing [IsIntegrallyClosed A K] [IsNoetherianRing A] :
     IsNoetherianRing (integralClosure A L) :=
   IsIntegralClosure.isNoetherianRing A K L (integralClosure A L)
 #align integral_closure.is_noetherian_ring integralClosure.isNoetherianRing
@@ -253,9 +253,10 @@ and `C := integralClosure A L`.
 -/
 theorem IsIntegralClosure.isDedekindDomain [IsDedekindDomain A] : IsDedekindDomain C :=
   have : IsFractionRing C L := IsIntegralClosure.isFractionRing_of_finite_extension A K L C
+  have : IsIntegrallyClosed A K := IsDedekindDomain.isIntegrallyClosed A K
   { IsIntegralClosure.isNoetherianRing A K L C,
     Ring.DimensionLEOne.isIntegralClosure A L C,
-    (isIntegrallyClosed_iff L).mpr fun {x} hx =>
+    (isIntegrallyClosed_fractionRing_iff _ L).mpr fun {x} hx =>
       ⟨IsIntegralClosure.mk' C x (isIntegral_trans (IsIntegralClosure.isIntegral_algebra A L) _ hx),
         IsIntegralClosure.algebraMap_mk' _ _ _⟩ with : IsDedekindDomain C }
 #align is_integral_closure.is_dedekind_domain IsIntegralClosure.isDedekindDomain

Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean

@@ -215,6 +215,7 @@ theorem fromUnit_ker [hn : Fact <| 0 < n] :
     have hi : ↑(_ ^ n : Kˣ)⁻¹ = algebraMap R K _ := by exact congr_arg Units.inv hx
     rw [Units.val_pow_eq_pow_val] at hv
     rw [← inv_pow, Units.inv_mk, Units.val_pow_eq_pow_val] at hi
+    have := IsDedekindDomain.isIntegrallyClosed R K
     rcases IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow (R := R) (x := v) hn.out
         (hv.symm ▸ isIntegral_algebraMap) with
       ⟨v', rfl⟩

Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean

@@ -154,7 +154,8 @@ theorem DiscreteValuationRing.TFAE [IsNoetherianRing R] [LocalRing R] [IsDomain
     (h : ¬IsField R) :
     List.TFAE
       [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R,
-        IsIntegrallyClosed R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime, (maximalIdeal R).IsPrincipal,
+        IsIntegrallyClosed R (FractionRing R) ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime,
+        (maximalIdeal R).IsPrincipal,
         FiniteDimensional.finrank (ResidueField R) (CotangentSpace R) = 1,
         ∀ (I) (_ : I ≠ ⊥), ∃ n : ℕ, I = maximalIdeal R ^ n] := by
   have ne_bot := Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h

Mathlib/RingTheory/Discriminant.lean

@@ -330,8 +330,8 @@ theorem discr_eq_discr_of_toMatrix_coeff_isIntegral [NumberField K] {b : Basis 
 separable extension of `K`. Let `B : PowerBasis K L` be such that `IsIntegral R B.gen`.
 Then for all, `z : L` that are integral over `R`, we have
 `(discr K B.basis) • z ∈ adjoin R ({B.gen} : set L)`. -/
-theorem discr_mul_isIntegral_mem_adjoin [IsSeparable K L] [IsIntegrallyClosed R]
-    [IsFractionRing R K] {B : PowerBasis K L} (hint : IsIntegral R B.gen) {z : L}
+theorem discr_mul_isIntegral_mem_adjoin [IsSeparable K L] [IsIntegrallyClosed R K]
+    {B : PowerBasis K L} (hint : IsIntegral R B.gen) {z : L}
     (hz : IsIntegral R z) : discr K B.basis • z ∈ adjoin R ({B.gen} : Set L) := by
   have hinv : IsUnit (traceMatrix K B.basis).det := by
     simpa [← discr_def] using discr_isUnit_of_basis _ B.basis