not_denselyOrdered_of_isPrincipalIdealRing

English

If O is a principal ideal ring, then range(v) is not densely ordered.

Русский

Если O является кольцом с принципиальными идеалами, то образ v не плотный по порядку.

LaTeX

$$¬ DenselyOrdered (range v)$$

Lean4

theorem not_denselyOrdered_of_isPrincipalIdealRing [IsPrincipalIdealRing O] (hv : Integers v O) :
    ¬DenselyOrdered (range v) := by
  intro H
  set I : Ideal O :=
    { carrier := v ∘ algebraMap O F ⁻¹' Iio (1 : Γ₀)
      add_mem' := fun {a b} ha hb ↦ by simpa using map_add_lt v ha hb
      zero_mem' := by simp
      smul_mem' := by
        intro c x
        simp only [mem_preimage, Function.comp_apply, mem_Iio, smul_eq_mul, map_mul]
        intro hx
        exact Right.mul_lt_one_of_le_of_lt (hv.map_le_one c) hx }
  obtain ⟨x, hx₁, hx⟩ :
    ∃ x, v (algebraMap O F x) < 1 ∧ v (algebraMap O F x) ∈ upperBounds (Iio 1 ∩ range (v ∘ algebraMap O F)) := by
    simpa [I, IsGreatest, hv.isPrincipal_iff_exists_isGreatest, ← image_preimage_eq_inter_range] using
      IsPrincipalIdealRing.principal I
  obtain ⟨y, hy, hy₁⟩ : ∃ y, v (algebraMap O F x) < v y ∧ v y < 1 := by
    simpa only [Subtype.exists, Subtype.mk_lt_mk, exists_range_iff, exists_prop] using
      H.dense ⟨v (algebraMap O F x), mem_range_self _⟩ ⟨1, 1, v.map_one⟩ hx₁
  obtain ⟨z, rfl⟩ := hv.exists_of_le_one hy₁.le
  exact hy.not_ge <| hx ⟨hy₁, mem_range_self _⟩

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