English
For Noetherian local domain R that is not a field, the same list of equivalences holds as in the DVR TFAE statement.
Русский
Для локального домена R, не являющегося полем, выполняется тот же набор эквивалентностей, что и в DVR TFAE.
LaTeX
$$tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain$$
Lean4
/-- Let `(R, m, k)` be a Noetherian local domain (possibly a field).
The following are equivalent:
0. `R` is a PID
1. `R` is a valuation ring
2. `R` is a Dedekind domain
3. `R` is integrally closed with at most one non-zero prime ideal
4. `m` is principal
5. `dimₖ m/m² ≤ 1`
6. Every nonzero ideal is a power of `m`.
Also see `IsDiscreteValuationRing.TFAE` for a version assuming `¬ IsField R`.
-/
theorem tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain [IsNoetherianRing R] [IsLocalRing R] [IsDomain R] :
List.TFAE
[IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
IsIntegrallyClosed R ∧ ∀ P : Ideal R, P ≠ ⊥ → P.IsPrime → P = maximalIdeal R, (maximalIdeal R).IsPrincipal,
finrank (ResidueField R) (CotangentSpace R) ≤ 1, ∀ I ≠ ⊥, ∃ n : ℕ, I = maximalIdeal R ^ n] :=
by
tfae_have 1 → 2 := fun _ ↦ inferInstance
tfae_have 2 → 1 := fun _ ↦ ((IsBezout.TFAE (R := R)).out 0 1).mp ‹_›
tfae_have 1 → 4
| H => ⟨inferInstance, fun P hP hP' ↦ eq_maximalIdeal (hP'.isMaximal hP)⟩
tfae_have 4 → 3 := fun ⟨h₁, h₂⟩ ↦ { h₁ with maximalOfPrime := (h₂ _ · · ▸ maximalIdeal.isMaximal R) }
tfae_have 3 → 5 := fun h ↦ maximalIdeal_isPrincipal_of_isDedekindDomain R
tfae_have 6 ↔ 5 := finrank_cotangentSpace_le_one_iff
tfae_have 5 → 7 := exists_maximalIdeal_pow_eq_of_principal R
tfae_have 7 → 2 := by
rw [ValuationRing.iff_ideal_total]
intro H
constructor
intro I J
by_cases hI : I = ⊥; · subst hI; left; exact bot_le
by_cases hJ : J = ⊥; · subst hJ; right; exact bot_le
obtain ⟨n, rfl⟩ := H I hI
obtain ⟨m, rfl⟩ := H J hJ
exact (le_total m n).imp Ideal.pow_le_pow_right Ideal.pow_le_pow_right
tfae_finish
