English
The map compStarAlgHom' preserves addition of maps: compStarAlgHom'(A,f)(g + h) = compStarAlgHom'(A,f)(g) + compStarAlgHom'(A,f)(h).
Русский
Операция compStarAlgHom' сохраняет сложение отображений: (g+h) под действием compStarAlgHom' равняется сумме образов g и h.
LaTeX
$$$$(\mathrm{compStarAlgHom}'(f)) (g + h) = (\mathrm{compStarAlgHom}'(f))(g) + (\mathrm{compStarAlgHom}'(f))(h)$$$$
Lean4
/-- `ContinuousMap.compStarAlgHom'` as a `StarAlgEquiv` when the continuous map `f` is
actually a homeomorphism. -/
@[simps]
def compStarAlgEquiv' (f : X ≃ₜ Y) : C(Y, A) ≃⋆ₐ[𝕜] C(X, A) :=
{
(f : C(X, Y)).compStarAlgHom' 𝕜 A with
toFun := (f : C(X, Y)).compStarAlgHom' 𝕜 A
invFun := (f.symm : C(Y, X)).compStarAlgHom' 𝕜 A
left_inv := fun g => by
simp only [ContinuousMap.compStarAlgHom'_apply, ContinuousMap.comp_assoc, toContinuousMap_comp_symm,
ContinuousMap.comp_id]
right_inv := fun g => by
simp only [ContinuousMap.compStarAlgHom'_apply, ContinuousMap.comp_assoc, symm_comp_toContinuousMap,
ContinuousMap.comp_id]
map_smul' := fun k a => map_smul ((f : C(X, Y)).compStarAlgHom' 𝕜 A) k a }
