map_bot — Mathlib

English

Let f: A →ₐ[R] B be an algebra homomorphism. Then the image of the bottom subalgebra of A under f is the bottom subalgebra of B.

Русский

Пусть f: A →ₐ[R] B является алгебраическим отображением. Тогда образ нулевой подалгебры A под действием f равен нулевой подалгебре B.

LaTeX

$$$ (\\bot : \\mathrm{Subalgebra} R A).map f = \\bot $$$

Lean4

@[simp]
theorem map_bot (f : A →ₐ[R] B) : (⊥ : Subalgebra R A).map f = ⊥ :=
  Subalgebra.toSubmodule_injective <| by
    simpa only [Subalgebra.map_toSubmodule, toSubmodule_bot] using Submodule.map_one _

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