instIsPrimeSuppOfNontrivialOfNoZeroDivisors

English

The support of a valuation is a prime ideal: under mild hypotheses (nontrivial value group with no zero divisors), supp(v) is a prime ideal of R.

Русский

Опора оценивания является prime-идеалом: при некоторых предпосылках (ненулевой группы значений и отсутствие делителей нуля) supp(v) — примарный идеал кольца R.

LaTeX

$$$\operatorname{IsPrime}(\operatorname{supp}(v))$$$

Lean4

/-- The support of a valuation is a prime ideal. -/
instance [Nontrivial Γ₀] [NoZeroDivisors Γ₀] : Ideal.IsPrime (supp v) :=
  ⟨fun h =>
    one_ne_zero (α := Γ₀) <|
      calc
        1 = v 1 := v.map_one.symm
        _ = 0 := by rw [← mem_supp_iff, h]; exact Submodule.mem_top,
    fun {x y} hxy => by
    simp only [mem_supp_iff] at hxy ⊢
    rw [v.map_mul x y] at hxy
    exact eq_zero_or_eq_zero_of_mul_eq_zero hxy⟩

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