exist_mem_one_of_mem_two — Mathlib

English

If p0 < p1 < p2 is a chain of primes and x ∈ p2, there exists q between p0 and p2 with x ∈ q and p0 < q < p2.

Русский

Пусть имеется цепочка прим p0 < p1 < p2 и элемент x ∈ p2. Тогда существует прайм q между p0 и p2, такой что x ∈ q и p0 < q < p2.

LaTeX

$$$\\forall p_0

Lean4

theorem exist_mem_one_of_mem_two {p₁ p₀ p₂ : PrimeSpectrum R} (h₀ : p₀ < p₁) (h₁ : p₁ < p₂) {x : R}
    (hx : x ∈ p₂.asIdeal) : ∃ q : (PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂ :=
  by
  let e := IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.1) p₂.1
  have hm : closedPoint (Localization.AtPrime p₂.1) = e.symm ⟨p₂, le_refl p₂⟩ :=
    (PrimeSpectrum.ext Localization.AtPrime.map_eq_maximalIdeal).symm
  obtain ⟨q, hxq, h₀, h₁⟩ :=
    @exist_mem_one_of_mem_maximal_ideal (Localization.AtPrime p₂.1) _ _ _ (e.symm ⟨p₁, h₁.le⟩)
        (e.symm ⟨p₀, (h₀.trans h₁).le⟩) (e.symm.lt_iff_lt.mpr h₀) (by simp [hm, h₁])
        (algebraMap R (Localization.AtPrime p₂.1) x) <|
      by
      rw [← Localization.AtPrime.map_eq_maximalIdeal]
      exact mem_map_of_mem (algebraMap R (Localization.AtPrime p₂.1)) hx
  rw [← e.symm_apply_apply q] at h₀ h₁ hxq
  have hq : (e q).1 < p₂ :=
    by
    have h : e.symm (e q) < e.symm ⟨p₂, le_refl p₂⟩ := h₁.trans_eq Localization.AtPrime.map_eq_maximalIdeal.symm
    rwa [OrderIso.lt_iff_lt, Subtype.mk_lt_mk] at h
  exact Exists.intro (e q).1 ⟨(p₂.1.under_map_of_isLocalizationAtPrime hq.le).le hxq, e.symm.lt_iff_lt.mp h₀, hq⟩

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