finite_quotient_maximalIdeal_pow_of_finite_residueField

English

If the residue field is finite, then for every n, the quotient ring 𝒪[K] / 𝓂[K]^n is finite.

Русский

Если остаточное поле конечное, то для каждого n кольцо 𝒪[K] / 𝓂[K]^n конечно.

LaTeX

$$$$\forall n \in \mathbb{N},\; \#\big( \mathcal{O}_K / \mathfrak{m}_K^n \big) < \infty.$$$$

Lean4

theorem finite_quotient_maximalIdeal_pow_of_finite_residueField [IsDiscreteValuationRing 𝒪[K]] (h : Finite 𝓀[K])
    (n : ℕ) : Finite (𝒪[K] ⧸ 𝓂[K] ^ n) := by
  induction n with
  | zero =>
    simp only [pow_zero, Ideal.one_eq_top]
    exact Finite.of_fintype (↥𝒪[K] ⧸ ⊤)
  | succ n ih =>
    have : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n := Ideal.pow_le_pow_right (by simp)
    replace ih := Finite.of_equiv _ (DoubleQuot.quotQuotEquivQuotOfLE this).symm.toEquiv
    suffices Finite (Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n)) from
      Finite.of_finite_quot_finite_ideal (I := Ideal.map (Ideal.Quotient.mk _) (𝓂[K] ^ n))
    exact
      @Finite.of_equiv _ _ h
        ((Ideal.quotEquivPowQuotPowSuccEquiv (IsPrincipalIdealRing.principal 𝓂[K])
              (IsDiscreteValuationRing.not_a_field _) n).trans
          (Ideal.powQuotPowSuccEquivMapMkPowSuccPow _ n))

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