map_adjoin — Mathlib

English

For a star-algebra homomorphism f, the image of the adjoin of s in A maps to the adjoin of the image of s in B.

Русский

Образ подалгебры adjoin_R s через f совпадает с подалгеброй, порождённой образами элементов s.

LaTeX

$$$ \\mathrm{map}\\; f\\; (\\mathrm{adjoin}_R s) = \\mathrm{adjoin}_R (f''s) $$$

Lean4

theorem map_adjoin (f : A →⋆ₐ[R] B) (s : Set A) : map f (adjoin R s) = adjoin R (f '' s) :=
  GaloisConnection.l_comm_of_u_comm Set.image_preimage (gc_map_comap f) StarAlgebra.gc StarAlgebra.gc fun _ => rfl

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