English
For a star-algebra homomorphism f: A →⋆ₐ[R] B and a StarSubalgebra S ⊆ B, the comap S under f is a StarSubalgebra of A consisting of all elements mapped into S by f; i.e., the preimage of S under f.
Русский
Для звездного гомоморфизма f: A →⋆ₐ[R] B и звездной подсалгебры S ⊆ B, comap f S является звездной подсалгеброй A и состоит из всех элементов, чьи образы принадлежат S.
LaTeX
$$$\\mathrm{comap}\;f\\;S = \\{ a \\in A : f(a) \\in S \\}$$$
Lean4
/-- Preimage of a star subalgebra under a star algebra homomorphism. -/
def comap (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) : StarSubalgebra R A :=
{ S.toSubalgebra.comap f.toAlgHom with
star_mem' := @fun a ha => show f (star a) ∈ S from (map_star f a).symm ▸ star_mem ha }
