English
Let f be a nonunital star algebra homomorphism. Restricting its codomain to its image range f yields a nonunital star algebra homomorphism from the domain to the range, i.e., rangeRestrict(f): A →⋆ₙₐ[R] (range f).
Русский
Пусть f — отображение алгебры со звёздочкой без единицы, сохраняющее структуру. Ограничение кодом к диапазону image(f) задаёт неприводимый к единице звёздный ненулевой однородный гомоморфизм: rangeRestrict(f): A →⋆ₙₐ[R] (range f).
LaTeX
$$$\mathrm{rangeRestrict}(f) : A \to\!\!\! _{R}^{\ast} (\mathrm{range}(f)).$$$
Lean4
/-- Restrict the codomain of a non-unital star algebra homomorphism `f` to `f.range`.
This is the bundled version of `Set.rangeFactorization`. -/
abbrev rangeRestrict (f : F) : A →⋆ₙₐ[R] (NonUnitalStarAlgHom.range f : NonUnitalStarSubalgebra R B) :=
NonUnitalStarAlgHom.codRestrict f (NonUnitalStarAlgHom.range f) (NonUnitalStarAlgHom.mem_range_self f)
