English
There is a construction 'copy' that produces a star-algebra homomorphism with a specified new underlying function, preserving all structure.
Русский
Существует конструктор 'copy', который даёт звездно-алгебра-гомоморфизм с заданной новой функцией основания, сохраняя всю структуру.
LaTeX
$$$\mathrm{copy}(f,f',h): A \to⋆ₐ[R] B$ is a StarAlgHom with $toFun=f'$, and preserves all algebra and star structures.$$
Lean4
/-- Copy of a `StarAlgHom` with a new `toFun` equal to the old one. Useful
to fix definitional equalities. -/
protected def copy (f : A →⋆ₐ[R] B) (f' : A → B) (h : f' = f) : A →⋆ₐ[R] B
where
toFun := f'
map_one' := h.symm ▸ map_one f
map_mul' := h.symm ▸ map_mul f
map_zero' := h.symm ▸ map_zero f
map_add' := h.symm ▸ map_add f
commutes' := h.symm ▸ AlgHomClass.commutes f
map_star' := h.symm ▸ map_star f
