English
An integral domain A is Dedekind iff it is Noetherian, has dimension ≤ 1, and is integrally closed in a fraction field; this equivalence is independent of the chosen fraction field.
Русский
Целое кольцо A есть Дедекиндово тогда и только тогда, когда оно Noetherian, имеет размерность ≤ 1 и интегрально замкнуто внутри некоторого дробного поля, причем эквивалентность независима от выбора дробного поля.
LaTeX
$$IsDedekindDomain A ↔ (IsDomain A ∧ IsNoetherianRing A ∧ DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ y, algebraMap A K y = x)$$
Lean4
/-- 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.
In particular, this definition does not depend on the choice of this fraction field. -/
theorem isDedekindRing_iff (K : Type*) [CommRing K] [Algebra A K] [IsFractionRing A K] :
IsDedekindRing A ↔ IsNoetherianRing A ∧ DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ y, algebraMap A K y = x :=
⟨fun _ => ⟨inferInstance, inferInstance, fun {_} => (isIntegrallyClosed_iff K).mp inferInstance⟩, fun ⟨hr, hd, hi⟩ =>
{ hr, hd, (isIntegrallyClosed_iff K).mpr @hi with }⟩
