map_top — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_top (f : A →ₐ[R] B) : (⊤ : Subalgebra R A).map f = f.range :=
  SetLike.coe_injective Set.image_univ

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