mk_bijective_iff_eq_bot — Mathlib

English

The canonical quotient map mk I is bijective if and only if I is the zero ideal; equivalently, the quotient does not identify any nonzero elements.

Русский

Каноническое отображение mk I является биективным тогда и только тогда, когда I = ⊥; эквивалентно тому, что нулевой идеал и нет ненулевых элементов, которые совпадают в фактор-кольце.

LaTeX

$$Function.Bijective (mk I) ↔ I = ⊥$$

Lean4

theorem mk_bijective_iff_eq_bot (I : Ideal A) [I.IsTwoSided] : Function.Bijective (mk I) ↔ I = ⊥ :=
  by
  constructor
  · intro h
    rw [← map_eq_bot_iff_of_injective h.1]
    exact (map_eq_bot_iff_le_ker _).mpr <| le_of_eq mk_ker.symm
  · exact fun h => ⟨(injective_iff_ker_eq_bot _).mpr <| by rw [mk_ker, h], mk_surjective⟩

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