refactor: turn DimensionLEOne into a class (#5833)

The predicate that a ring has Krull dimension at most one was a regular `def`. I believe we should turn it into a class because:
 * The property follows from the ring structure, e.g. because it is a PID or because it is an integral closure.
 * We pass it around as a whole hypothesis, something instance synthesis can deal well with.
 * It makes the definition of `IsDedekindDomain` the conjunction of a number of classes, so we could switch to `extends` for all its fields.

The main change in API is the addition of `Ideal.IsPrime.isMaximal` which is a restatement of the Krull dimension property with convenient dot notation: turn a prime ideal into a maximal ideal given the hypothesis that it's not zero.

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Should.20.60IsDedekindDomain.60.20extend.20.60IsDomain.60.3F/near/374515392

Author: Vierkantor

Mathlib/RingTheory/DedekindDomain/Basic.lean

@@ -45,41 +45,47 @@ variable (R A K : Type _) [CommRing R] [CommRing A] [Field K]
 open scoped nonZeroDivisors Polynomial
 
 /-- A ring `R` has Krull dimension at most one if all nonzero prime ideals are maximal. -/
-def Ring.DimensionLEOne : Prop :=
-  ∀ (p) (_ : p ≠ (⊥ : Ideal R)), p.IsPrime → p.IsMaximal
+class Ring.DimensionLEOne : Prop :=
+  (maximalOfPrime : ∀ {p : Ideal R}, p ≠ ⊥ → p.IsPrime → p.IsMaximal)
 #align ring.dimension_le_one Ring.DimensionLEOne
 
 open Ideal Ring
 
+theorem Ideal.IsPrime.isMaximal {R : Type _} [CommRing R] [DimensionLEOne R]
+    {p : Ideal R} (h : p.IsPrime) (hp : p ≠ ⊥) : p.IsMaximal :=
+  DimensionLEOne.maximalOfPrime hp h
+
 namespace Ring
 
-theorem DimensionLEOne.principal_ideal_ring [IsDomain A] [IsPrincipalIdealRing A] :
-    DimensionLEOne A := fun _ nonzero _ =>
-  IsPrime.to_maximal_ideal nonzero
+instance DimensionLEOne.principal_ideal_ring [IsDomain A] [IsPrincipalIdealRing A] :
+    DimensionLEOne A where
+  maximalOfPrime := fun nonzero _ =>
+    IsPrime.to_maximal_ideal nonzero
 #align ring.dimension_le_one.principal_ideal_ring Ring.DimensionLEOne.principal_ideal_ring
 
 theorem DimensionLEOne.isIntegralClosure (B : Type _) [CommRing B] [IsDomain B] [Nontrivial R]
     [Algebra R A] [Algebra R B] [Algebra B A] [IsScalarTower R B A] [IsIntegralClosure B R A]
-    (h : DimensionLEOne R) : DimensionLEOne B := fun p ne_bot _ =>
-  IsIntegralClosure.isMaximal_of_isMaximal_comap A p
-    (h _ (IsIntegralClosure.comap_ne_bot A ne_bot) inferInstance)
+    [DimensionLEOne R] : DimensionLEOne B where
+  maximalOfPrime := fun {p} ne_bot _ =>
+    IsIntegralClosure.isMaximal_of_isMaximal_comap (R := R) A p
+      (Ideal.IsPrime.isMaximal inferInstance (IsIntegralClosure.comap_ne_bot A ne_bot))
 #align ring.dimension_le_one.is_integral_closure Ring.DimensionLEOne.isIntegralClosure
 
-nonrec theorem DimensionLEOne.integralClosure [Nontrivial R] [IsDomain A] [Algebra R A]
-    (h : DimensionLEOne R) : DimensionLEOne (integralClosure R A) :=
-  h.isIntegralClosure R A (integralClosure R A)
+nonrec instance DimensionLEOne.integralClosure [Nontrivial R] [IsDomain A] [Algebra R A]
+    [DimensionLEOne R] : DimensionLEOne (integralClosure R A) :=
+  DimensionLEOne.isIntegralClosure R A (integralClosure R A)
 #align ring.dimension_le_one.integral_closure Ring.DimensionLEOne.integralClosure
 
 variable {R}
 
-theorem DimensionLEOne.not_lt_lt (h : Ring.DimensionLEOne R) (p₀ p₁ p₂ : Ideal R) [hp₁ : p₁.IsPrime]
+theorem DimensionLEOne.not_lt_lt [Ring.DimensionLEOne R] (p₀ p₁ p₂ : Ideal R) [hp₁ : p₁.IsPrime]
     [hp₂ : p₂.IsPrime] : ¬(p₀ < p₁ ∧ p₁ < p₂)
-  | ⟨h01, h12⟩ => h12.ne ((h p₁ (bot_le.trans_lt h01).ne' hp₁).eq_of_le hp₂.ne_top h12.le)
+  | ⟨h01, h12⟩ => h12.ne ((hp₁.isMaximal (bot_le.trans_lt h01).ne').eq_of_le hp₂.ne_top h12.le)
 #align ring.dimension_le_one.not_lt_lt Ring.DimensionLEOne.not_lt_lt
 
-theorem DimensionLEOne.eq_bot_of_lt (h : Ring.DimensionLEOne R) (p P : Ideal R) [p.IsPrime]
+theorem DimensionLEOne.eq_bot_of_lt [Ring.DimensionLEOne R] (p P : Ideal R) [p.IsPrime]
     [P.IsPrime] (hpP : p < P) : p = ⊥ :=
-  by_contra fun hp0 => h.not_lt_lt ⊥ p P ⟨Ne.bot_lt hp0, hpP⟩
+  by_contra fun hp0 => not_lt_lt ⊥ p P ⟨Ne.bot_lt hp0, hpP⟩
 #align ring.dimension_le_one.eq_bot_of_lt Ring.DimensionLEOne.eq_bot_of_lt
 
 end Ring
@@ -105,7 +111,8 @@ class IsDedekindDomain : Prop where
 #align is_dedekind_domain IsDedekindDomain
 
 -- See library note [lower instance priority]
-attribute [instance 100] IsDedekindDomain.isNoetherianRing IsDedekindDomain.isIntegrallyClosed
+attribute [instance 100] IsDedekindDomain.dimensionLEOne IsDedekindDomain.isNoetherianRing
+  IsDedekindDomain.isIntegrallyClosed
 
 /-- 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.

Mathlib/RingTheory/DedekindDomain/Dvr.lean

@@ -70,7 +70,7 @@ once we have a suitable definition.
 -/
 theorem Ring.DimensionLEOne.localization {R : Type _} (Rₘ : Type _) [CommRing R] [IsDomain R]
     [CommRing Rₘ] [Algebra R Rₘ] {M : Submonoid R} [IsLocalization M Rₘ] (hM : M ≤ R⁰)
-    (h : Ring.DimensionLEOne R) : Ring.DimensionLEOne Rₘ := by
+    (h : Ring.DimensionLEOne R) : Ring.DimensionLEOne Rₘ := ⟨by
   intro p hp0 hpp
   refine' Ideal.isMaximal_def.mpr ⟨hpp.ne_top, Ideal.maximal_of_no_maximal fun P hpP hPm => _⟩
   have hpP' : (⟨p, hpp⟩ : { p : Ideal Rₘ // p.IsPrime }) < ⟨P, hPm.isPrime⟩ := hpP
@@ -81,7 +81,7 @@ theorem Ring.DimensionLEOne.localization {R : Type _} (Rₘ : Type _) [CommRing
     ((IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, hPm.isPrime⟩).2.1
   have _ : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P := hpP'
   refine' h.not_lt_lt ⊥ (Ideal.comap _ _) (Ideal.comap _ _) ⟨_, hpP'⟩
-  exact IsLocalization.bot_lt_comap_prime _ _ hM _ hp0
+  exact IsLocalization.bot_lt_comap_prime _ _ hM _ hp0⟩
 #align ring.dimension_le_one.localization Ring.DimensionLEOne.localization
 
 /-- The localization of a Dedekind domain is a Dedekind domain. -/

Mathlib/RingTheory/DedekindDomain/Ideal.lean

@@ -306,7 +306,7 @@ theorem integrallyClosed : IsIntegrallyClosed A := by
 
 open Ring
 
-theorem dimensionLEOne : DimensionLEOne A := by
+theorem dimensionLEOne : DimensionLEOne A := ⟨by
   -- We're going to show that `P` is maximal because any (maximal) ideal `M`
   -- that is strictly larger would be `⊤`.
   rintro P P_ne hP
@@ -340,7 +340,7 @@ theorem dimensionLEOne : DimensionLEOne A := by
   obtain ⟨zy, hzy, zy_eq⟩ := (mem_coeIdeal A⁰).mp zy_mem
   rw [IsFractionRing.injective A (FractionRing A) zy_eq] at hzy
   -- But `P` is a prime ideal, so `z ∉ P` implies `y ∈ P`, as desired.
-  exact mem_coeIdeal_of_mem A⁰ (Or.resolve_left (hP.mem_or_mem hzy) hzp)
+  exact mem_coeIdeal_of_mem A⁰ (Or.resolve_left (hP.mem_or_mem hzy) hzp)⟩
 #align is_dedekind_domain_inv.dimension_le_one IsDedekindDomainInv.dimensionLEOne
 
 /-- Showing one side of the equivalence between the definitions
@@ -381,7 +381,7 @@ theorem exists_multiset_prod_cons_le_and_prod_not_le [IsDedekindDomain A] (hNF :
       rwa [Ne.def, ← Multiset.cons_erase hPZ', Multiset.prod_cons, Ideal.mul_eq_bot, not_or, ←
         this] at hprodZ
     -- By maximality of `P` and `M`, we have that `P ≤ M` implies `P = M`.
-    have hPM' := (IsDedekindDomain.dimensionLEOne _ hP0 P.IsPrime).eq_of_le hM.ne_top hPM
+    have hPM' := (P.IsPrime.isMaximal hP0).eq_of_le hM.ne_top hPM
     subst hPM'
     -- By minimality of `Z`, erasing `P` from `Z` is exactly what we need.
     refine ⟨Z.erase P, ?_, ?_⟩
@@ -989,7 +989,7 @@ variable (v : HeightOneSpectrum R) {R}
 
 namespace HeightOneSpectrum
 
-instance isMaximal : v.asIdeal.IsMaximal := dimensionLEOne v.asIdeal v.ne_bot v.isPrime
+instance isMaximal : v.asIdeal.IsMaximal := v.isPrime.isMaximal v.ne_bot
 #align is_dedekind_domain.height_one_spectrum.is_maximal IsDedekindDomain.HeightOneSpectrum.isMaximal
 
 theorem prime : Prime v.asIdeal := Ideal.prime_of_isPrime v.ne_bot v.isPrime
@@ -1005,7 +1005,7 @@ theorem associates_irreducible : Irreducible <| Associates.mk v.asIdeal :=
 
 /-- An equivalence between the height one and maximal spectra for rings of Krull dimension 1. -/
 def equivMaximalSpectrum (hR : ¬IsField R) : HeightOneSpectrum R ≃ MaximalSpectrum R where
-  toFun v := ⟨v.asIdeal, dimensionLEOne v.asIdeal v.ne_bot v.isPrime⟩
+  toFun v := ⟨v.asIdeal, v.isPrime.isMaximal v.ne_bot⟩
   invFun v :=
     ⟨v.asIdeal, v.IsMaximal.isPrime, Ring.ne_bot_of_isMaximal_of_not_isField v.IsMaximal hR⟩
   left_inv := fun ⟨_, _, _⟩ => rfl
@@ -1029,7 +1029,7 @@ theorem iInf_localization_eq_bot [Algebra R K] [hK : IsFractionRing R K] :
     exact fun _ => Algebra.mem_bot.mpr ⟨algebra_map_inv x, algebra_map_right_inv x⟩
   all_goals rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]
   · exact fun hx ⟨v, hv⟩ => hx ((equivMaximalSpectrum hR).symm ⟨v, hv⟩)
-  · exact fun hx ⟨v, hv, hbot⟩ => hx ⟨v, dimensionLEOne v hbot hv⟩
+  · exact fun hx ⟨v, hv, hbot⟩ => hx ⟨v, hv.isMaximal hbot⟩
 #align is_dedekind_domain.height_one_spectrum.infi_localization_eq_bot IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot
 
 end HeightOneSpectrum
@@ -1192,9 +1192,9 @@ open scoped BigOperators
 
 variable {R}
 
-theorem Ring.DimensionLeOne.prime_le_prime_iff_eq (h : Ring.DimensionLEOne R) {P Q : Ideal R}
+theorem Ring.DimensionLeOne.prime_le_prime_iff_eq [Ring.DimensionLEOne R] {P Q : Ideal R}
     [hP : P.IsPrime] [hQ : Q.IsPrime] (hP0 : P ≠ ⊥) : P ≤ Q ↔ P = Q :=
-  ⟨(h P hP0 hP).eq_of_le hQ.ne_top, Eq.le⟩
+  ⟨(hP.isMaximal hP0).eq_of_le hQ.ne_top, Eq.le⟩
 #align ring.dimension_le_one.prime_le_prime_iff_eq Ring.DimensionLeOne.prime_le_prime_iff_eq
 
 theorem Ideal.coprime_of_no_prime_ge {I J : Ideal R} (h : ∀ P, I ≤ P → J ≤ P → ¬IsPrime P) :
@@ -1290,9 +1290,9 @@ theorem IsDedekindDomain.inf_prime_pow_eq_prod {ι : Type _} (s : Finset ι) (f
   haveI := Ideal.isPrime_of_prime (prime b (Finset.mem_insert_of_mem hb))
   refine coprime a (Finset.mem_insert_self a s) b (Finset.mem_insert_of_mem hb) ?_ ?_
   · rintro rfl; contradiction
-  · refine ((Ring.DimensionLeOne.prime_le_prime_iff_eq IsDedekindDomain.dimensionLEOne ?_).mp
+  · refine ((Ring.DimensionLeOne.prime_le_prime_iff_eq ?_).mp
       (Ideal.le_of_pow_le_prime hPa)).trans
-      ((Ring.DimensionLeOne.prime_le_prime_iff_eq IsDedekindDomain.dimensionLEOne ?_).mp
+      ((Ring.DimensionLeOne.prime_le_prime_iff_eq ?_).mp
       (Ideal.le_of_pow_le_prime hPb)).symm
     exact (prime a (Finset.mem_insert_self a s)).ne_zero
     exact (prime b (Finset.mem_insert_of_mem hb)).ne_zero
@@ -1314,9 +1314,9 @@ noncomputable def IsDedekindDomain.quotientEquivPiOfProdEq {ι : Type _} [Fintyp
       haveI := Ideal.isPrime_of_prime (prime i)
       haveI := Ideal.isPrime_of_prime (prime j)
       refine coprime i j hij ?_
-      refine ((Ring.DimensionLeOne.prime_le_prime_iff_eq IsDedekindDomain.dimensionLEOne ?_).mp
+      refine ((Ring.DimensionLeOne.prime_le_prime_iff_eq ?_).mp
         (Ideal.le_of_pow_le_prime hPi)).trans
-        ((Ring.DimensionLeOne.prime_le_prime_iff_eq IsDedekindDomain.dimensionLEOne ?_).mp
+        ((Ring.DimensionLeOne.prime_le_prime_iff_eq ?_).mp
           (Ideal.le_of_pow_le_prime hPj)).symm
       exact (prime i).ne_zero
       exact (prime j).ne_zero)

Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

@@ -253,7 +253,7 @@ and `C := integralClosure A L`.
 -/
 theorem IsIntegralClosure.isDedekindDomain [h : IsDedekindDomain A] : IsDedekindDomain C :=
   haveI : IsFractionRing C L := IsIntegralClosure.isFractionRing_of_finite_extension A K L C
-  ⟨IsIntegralClosure.isNoetherianRing A K L C, h.dimensionLEOne.isIntegralClosure _ L _,
+  ⟨IsIntegralClosure.isNoetherianRing A K L C, h.dimensionLEOne.isIntegralClosure L _,
     (isIntegrallyClosed_iff L).mpr fun {x} hx =>
       ⟨IsIntegralClosure.mk' C x (isIntegral_trans (IsIntegralClosure.isIntegral_algebra A L) _ hx),
         IsIntegralClosure.algebraMap_mk' _ _ _⟩⟩

Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean

@@ -103,7 +103,7 @@ theorem maximalIdeal_isPrincipal_of_isDedekindDomain [LocalRing R] [IsDomain R]
     · exact sInf_le ⟨hle, inferInstance⟩
     · refine'
         le_sInf fun I hI =>
-          (eq_maximalIdeal <| IsDedekindDomain.dimensionLEOne _ (fun e => ha₂ _) hI.2).ge
+          (eq_maximalIdeal <| hI.2.isMaximal (fun e => ha₂ _)).ge
       rw [← Ideal.span_singleton_eq_bot, eq_bot_iff, ← e]; exact hI.1
   have : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a} := by
     rw [← this]; apply Ideal.exists_radical_pow_le_of_fg; exact IsNoetherian.noetherian _
@@ -177,8 +177,8 @@ theorem DiscreteValuationRing.TFAE [IsNoetherianRing R] [LocalRing R] [IsDomain
   tfae_have 4 → 3
   · rintro ⟨h₁, h₂⟩;
     exact
-      ⟨inferInstance, fun I hI hI' =>
-        ExistsUnique.unique h₂ ⟨ne_bot, inferInstance⟩ ⟨hI, hI'⟩ ▸ maximalIdeal.isMaximal R, h₁⟩
+      ⟨inferInstance, ⟨fun hI hI' =>
+        ExistsUnique.unique h₂ ⟨ne_bot, inferInstance⟩ ⟨hI, hI'⟩ ▸ maximalIdeal.isMaximal R⟩, h₁⟩
   tfae_have 3 → 5
   · intro h; exact maximalIdeal_isPrincipal_of_isDedekindDomain R
   tfae_have 5 → 6