map_toSubalgebra — Mathlib

English

For a StarSubalgebra S ⊆ A and a star-algebra homomorphism f: A →⋆ₐ[R] B, the subalgebra obtained by mapping S via f, when viewed as a subalgebra of B, coincides with the image of the underlying subalgebra S under f.

Русский

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

LaTeX

$$$(S.map f).toSubalgebra = S.toSubalgebra.map f.toAlgHom$$$

Lean4

theorem map_toSubalgebra {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} :
    (S.map f).toSubalgebra = S.toSubalgebra.map f.toAlgHom :=
  SetLike.coe_injective rfl

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