isOpen_iff_finite_quotient — Mathlib

English

For any R with the stated hypotheses, an ideal I is open in R if and only if the quotient R/I is finite.

Русский

При данных гипотезах кольца R идеал I открыт тогда и только тогда, когда фактор кольца R/I конечно.

LaTeX

$$$ IsOpen(I) \iff Finite(R / I) $$$

Lean4

theorem isOpen_iff_finite_quotient {I : Ideal R} : IsOpen (X := R) I ↔ Finite (R ⧸ I) :=
  by
  refine ⟨AddSubgroup.quotient_finite_of_isOpen I.toAddSubgroup, fun H ↦ ?_⟩
  obtain ⟨n, hn⟩ := exists_maximalIdeal_pow_le_of_isArtinianRing_quotient I
  exact
    AddSubgroup.isOpen_mono (H₁ := (maximalIdeal R ^ n).toAddSubgroup) (H₂ := I.toAddSubgroup) hn
      (isOpen_maximalIdeal_pow R n)

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