maximalIdeal_eq_setOf_le_v_algebraMap

English

Let O be a DVR with valuation v. For any irreducible ϖ ∈ O, the maximal ideal of O equals {y ∈ O | v(y) ≤ v(ϖ)} (via the O→K embedding).

Русский

Пусть O — DVR с оценкой v. Для любого неприводимого ϖ ∈ O максимальный идеал O задаётся как множество элементов y ∈ O с v(y) ≤ v(ϖ) (через вложение в полную форму).

LaTeX

$$\\text{Let } O \\text{ be DVR with valuation } v:\\n(\\text{IsDiscreteValuationRing } O) \\Rightarrow (\\text{maximalIdeal } O) = \\{ y \\in O : v(y) \\le v(\\varpi) \\} $$

Lean4

theorem maximalIdeal_eq_setOf_le_v_algebraMap :
    letI : IsDomain O := hv.hom_inj.isDomain
    ∀ [IsDiscreteValuationRing O] {ϖ : O} (_h : Irreducible ϖ),
      (IsLocalRing.maximalIdeal O : Set O) = {y : O | v (algebraMap O K y) ≤ v (algebraMap O K ϖ)} :=
  by
  letI : IsDomain O := hv.hom_inj.isDomain
  intro _ _ h
  rw [← hv.coe_span_singleton_eq_setOf_le_v_algebraMap, ← h.maximalIdeal_eq]

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