English
IsDedekindDomain A iff A is a domain, Noetherian, dim ≤ 1, and satisfies integral-existence in K.
Русский
IsDedekindDomain A эквивалентно тому, что A — область, Noetherian, dim ≤ 1 и существует интегральное представление в K.
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 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. -/
theorem isDedekindDomain_iff (K : Type*) [CommRing K] [Algebra A K] [IsFractionRing A K] :
IsDedekindDomain A ↔
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 }⟩
-- See library note [lower instance priority]
