ring_dimensionLEOne — Mathlib

English

A ring with Krull dimension at most 1 localizes to a ring with Krull dimension at most 1.

Русский

Кольцо с размерностью Крull ≤ 1 локализация даёт кольцо с размерностью ≤ 1.

LaTeX

$$$\text{Ring.DimensionLEOne}(R) \Rightarrow \text{Ring.DimensionLEOne}(R_m)$ under localization$$

Lean4

instance ring_dimensionLEOne [h : IsDedekindDomainDvr A] : Ring.DimensionLEOne A where
  maximalOfPrime := by
    intro p hp hpp
    rcases p.exists_le_maximal (Ideal.IsPrime.ne_top hpp) with ⟨q, hq, hpq⟩
    let f := (IsLocalization.orderIsoOfPrime q.primeCompl (Localization.AtPrime q)).symm
    let P := f ⟨p, hpp, hpq.disjoint_compl_left⟩
    let Q := f ⟨q, hq.isPrime, Set.disjoint_left.mpr fun _ a => a⟩
    have hinj : Function.Injective (algebraMap A (Localization.AtPrime q)) :=
      IsLocalization.injective (Localization.AtPrime q) q.primeCompl_le_nonZeroDivisors
    have hp1 : P.1 ≠ ⊥ := fun x => hp ((p.map_eq_bot_iff_of_injective hinj).mp x)
    have hq1 : Q.1 ≠ ⊥ := fun x => (ne_bot_of_le_ne_bot hp hpq) ((q.map_eq_bot_iff_of_injective hinj).mp x)
    rcases
      (IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime (Localization.AtPrime q)).mp
        (h.is_dvr_at_nonzero_prime q (ne_bot_of_le_ne_bot hp hpq) hq.isPrime) with
      ⟨_, huq⟩
    rw [show p = q from Subtype.val_inj.mpr <| f.injective <| Subtype.val_inj.mp (huq.unique ⟨hp1, P.2⟩ ⟨hq1, Q.2⟩)]
    exact hq

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