surjective_algebraMap_iff — Mathlib

English

For a field-based setting, surjectivity of the algebra map algebraMap R A is equivalent to the top subalgebra equal to the bottom subalgebra.

Русский

Для поля F и кольца A условие сюръективности алгебраического отображения algebraMap R A эквивалентно равенству верхней и нижней подалгебр.

LaTeX

$$$ \\text{surjective_algebraMap_iff} : \\mathrm{Function.Surjective} (\\mathrm{algebraMap} R A) \\;\\iff\\; (\\top : \\mathrm{Subalgebra} R A) = \\bot $$$

Lean4

theorem surjective_algebraMap_iff : Function.Surjective (algebraMap R A) ↔ (⊤ : Subalgebra R A) = ⊥ :=
  ⟨fun h =>
    eq_bot_iff.2 fun y _ =>
      let ⟨_x, hx⟩ := h y
      hx ▸ Subalgebra.algebraMap_mem _ _,
    fun h y => Algebra.mem_bot.1 <| eq_bot_iff.1 h (Algebra.mem_top : y ∈ _)⟩

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