English
Equivalences as in DVR TFAE for similarly structured setups; no extra assumptions beyond Noetherian local domain not field.
Русский
Эквивалентности DVR TFAE применимы и в аналогичных обстановках; требуется Noetherian локальное доменное кольцо не являющееся полем.
LaTeX
$$tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain$$
Lean4
/-- The following are equivalent for a
Noetherian local domain that is not a field `(R, m, k)`:
0. `R` is a discrete valuation ring
1. `R` is a valuation ring
2. `R` is a Dedekind domain
3. `R` is integrally closed with a unique non-zero prime ideal
4. `m` is principal
5. `dimₖ m/m² = 1`
6. Every nonzero ideal is a power of `m`.
Also see `tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain` for a version without `¬ IsField R`.
-/
theorem TFAE [IsNoetherianRing R] [IsLocalRing R] [IsDomain R] (h : ¬IsField R) :
List.TFAE
[IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R,
IsIntegrallyClosed R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime, (maximalIdeal R).IsPrincipal,
finrank (ResidueField R) (CotangentSpace R) = 1, ∀ (I) (_ : I ≠ ⊥), ∃ n : ℕ, I = maximalIdeal R ^ n] :=
by
have : finrank (ResidueField R) (CotangentSpace R) = 1 ↔ finrank (ResidueField R) (CotangentSpace R) ≤ 1 := by
simp [Nat.le_one_iff_eq_zero_or_eq_one, finrank_cotangentSpace_eq_zero_iff, h]
rw [this]
have : maximalIdeal R ≠ ⊥ := isField_iff_maximalIdeal_eq.not.mp h
convert tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain R
· exact ⟨fun _ ↦ inferInstance, fun h ↦ { h with not_a_field' := this }⟩
·
exact
⟨fun h P h₁ h₂ ↦ h.unique ⟨h₁, h₂⟩ ⟨this, inferInstance⟩, fun H ↦
⟨_, ⟨this, inferInstance⟩, fun P hP ↦ H P hP.1 hP.2⟩⟩
