maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow

English

For a DVR O with valuation v and irreducible ϖ, for every n ∈ N, the nth power of the maximal ideal corresponds to {y ∈ O | v(y) ≤ v(ϖ)^n}.

Русский

Для DVR O с оценкой v и неприводимого ϖ верно: (maximalIdeal O)^n соответствует {y ∈ O | v(y) ≤ v(ϖ)^n}.

LaTeX

$$For irreducible ϖ and n ∈ ℕ, ((IsLocalRing.maximalIdeal O)^n : Set O) = {y : O | v(y) ≤ v(ϖ)^n}$$

Lean4

theorem maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow :
    letI : IsDomain O := hv.hom_inj.isDomain
    ∀ [IsDiscreteValuationRing O] {ϖ : O} (_h : Irreducible ϖ) (n : ℕ),
      ((IsLocalRing.maximalIdeal O ^ n : Ideal O) : Set O) =
        {y : O | v (algebraMap O K y) ≤ v (algebraMap O K ϖ) ^ n} :=
  by
  letI : IsDomain O := hv.hom_inj.isDomain
  intro _ ϖ h n
  have : (v (algebraMap O K ϖ)) ^ n = v (algebraMap O K (ϖ ^ n)) := by simp
  rw [this, ← hv.coe_span_singleton_eq_setOf_le_v_algebraMap, ← Ideal.span_singleton_pow, ← h.maximalIdeal_eq]

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