bot_quotient_isMaximal_iff — Mathlib

English

In a ring R, the bottom ideal of the quotient ring R/I is maximal if and only if I is a maximal ideal in R.

Русский

В кольце R нулевой идеал в R/I максимален тогда и только тогда, когда I максимальный идеал в R.

LaTeX

$$$ (\bot : \text{Ideal}(R/I)).IsMaximal \iff I.IsMaximal $$$

Lean4

@[simp]
theorem bot_quotient_isMaximal_iff (I : Ideal R) [I.IsTwoSided] : (⊥ : Ideal (R ⧸ I)).IsMaximal ↔ I.IsMaximal :=
  ⟨fun hI => mk_ker (I := I) ▸ comap_isMaximal_of_surjective (Quotient.mk I) Quotient.mk_surjective (K := ⊥) (H := hI),
    fun hI => by
    letI := Quotient.divisionRing I
    exact bot_isMaximal⟩

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