isDedekindDomain — Mathlib

English

If A is a Dedekind domain, then its localization at any given maximal condition is also Dedekind.

Русский

Если A — Дедекендова домена, то локализация по любой максимальной идеале также Дедекендова.

LaTeX

$$$[IsDedekindDomain A] \Rightarrow \forall P [P.IsPrime], IsDedekindDomain (Localization.AtPrime P) $$

Lean4

/-- The localization of a Dedekind domain is a Dedekind domain. -/
theorem isDedekindDomain [IsDedekindDomain A] {M : Submonoid A} (hM : M ≤ A⁰) (Aₘ : Type*) [CommRing Aₘ] [IsDomain Aₘ]
    [Algebra A Aₘ] [IsLocalization M Aₘ] : IsDedekindDomain Aₘ :=
  by
  have h : ∀ y : M, IsUnit (algebraMap A (FractionRing A) y) :=
    by
    rintro ⟨y, hy⟩
    exact IsUnit.mk0 _ (mt IsFractionRing.to_map_eq_zero_iff.mp (nonZeroDivisors.ne_zero (hM hy)))
  letI : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (IsLocalization.lift h)
  haveI : IsScalarTower A Aₘ (FractionRing A) :=
    IsScalarTower.of_algebraMap_eq fun x => (IsLocalization.lift_eq h x).symm
  haveI : IsFractionRing Aₘ (FractionRing A) := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M _ _
  refine (isDedekindDomain_iff _ (FractionRing A)).mpr ⟨?_, ?_, ?_, ?_⟩
  · infer_instance
  · exact IsLocalization.isNoetherianRing M _ inferInstance
  · exact Ring.DimensionLEOne.localization Aₘ hM
  · intro x hx
    obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _
    obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp IsDedekindRing.toIsIntegralClosure hy
    refine ⟨IsLocalization.mk' Aₘ z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr ?_⟩
    rw [hz, ← Algebra.smul_def]
    rfl

Похожие утверждения