English
For star-algebra homomorphisms φ: A →⋆ₐ B and ψ: B →⋆ₐ C, precomposition with φ and ψ yields a functorial map compStarAlgHom X (ψ ∘ φ) = compStarAlgHom X ψ ∘ compStarAlgHom X φ between spaces of continuous maps, respecting continuity of the coefficients.
Русский
Для звездно-алгебраических однородных отображений φ: A →⋆ₐ B и ψ: B →⋆ₐ C, композиция предсоставления образует естественную карту между пространствами непрерывных отображений, совместимую с непрерывностью коэффициентов.
LaTeX
$$$\mathrm{compStarAlgHom}\,X(ψ\circ φ) = (\mathrm{compStarAlgHom}\,X\,ψ) \circ (\mathrm{compStarAlgHom}\,X\,φ)$$$
Lean4
/-- Post-composition with a continuous star algebra homomorphism is a star algebra homomorphism
between spaces of continuous maps. -/
@[simps]
def compStarAlgHom (φ : A →⋆ₐ[𝕜] B) (hφ : Continuous φ) : C(X, A) →⋆ₐ[𝕜] C(X, B)
where
toFun f := (⟨φ, hφ⟩ : C(A, B)).comp f
map_one' := ext fun _ => map_one φ
map_mul' f g := ext fun x => map_mul φ (f x) (g x)
map_zero' := ext fun _ => map_zero φ
map_add' f g := ext fun x => map_add φ (f x) (g x)
commutes' r := ext fun _x => AlgHomClass.commutes φ r
map_star' f := ext fun x => map_star φ (f x)
