English
Localizing a domain of Krull dimension ≤ 1 yields another ring with Krull dimension ≤ 1.
Русский
Локализация домена Krull размерности ≤ 1 даёт другой круг с размерностью ≤ 1.
LaTeX
$$$\forall R \text{/{Ring}},\; M \le R^\circ \Rightarrow \operatorname{Ring.DimensionLEOne} (\text{Localization } M R) $$
Lean4
/-- Localizing a domain of Krull dimension `≤ 1` gives another ring of Krull dimension `≤ 1`.
Note that the same proof can/should be generalized to preserving any Krull dimension,
once we have a suitable definition.
-/
theorem localization {R : Type*} (Rₘ : Type*) [CommRing R] [IsDomain R] [CommRing Rₘ] [Algebra R Rₘ] {M : Submonoid R}
[IsLocalization M Rₘ] (hM : M ≤ R⁰) [h : Ring.DimensionLEOne R] : Ring.DimensionLEOne Rₘ :=
⟨by
intro p hp0 hpp
refine Ideal.isMaximal_def.mpr ⟨hpp.ne_top, Ideal.maximal_of_no_maximal fun P hpP hPm => ?_⟩
have hpP' : (⟨p, hpp⟩ : { p : Ideal Rₘ // p.IsPrime }) < ⟨P, hPm.isPrime⟩ := hpP
rw [← (IsLocalization.orderIsoOfPrime M Rₘ).lt_iff_lt] at hpP'
haveI : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) p) := ((IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩).2.1
haveI : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) P) :=
((IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, hPm.isPrime⟩).2.1
have hlt : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P := hpP'
refine h.not_lt_lt ⊥ (Ideal.comap _ _) (Ideal.comap _ _) ⟨?_, hlt⟩
exact IsLocalization.bot_lt_comap_prime _ _ hM _ hp0⟩
