English
Given a continuous star algebra homomorphism φ: A →⋆ₐ[𝕜] B and a continuous map h: X → A, precomposition with h yields a star algebra homomorphism φ ∘ h from C(X, A) to C(X, B).
Русский
При заданном непрерывном звездообразном однородном отображении φ: A →⋆ₐ[𝕜] B и непрерывной карте h: X → A, предварительная композиция даёт звездооднородное отображение φ ∘ h от C(X, A) к C(X, B).
LaTeX
$$$\text{compStarAlgHom}'(f): C(Y,A) \to⋆ₐ[𝕜] C(X,A)$ defined by $g \mapsto g \circ f$; equivalently, $f$ induces a star-algebra homomorphism $C(Y,A) \to C(X,A)$ by precomposition.$$
Lean4
/-- The functorial map taking `f : C(X, Y)` to `C(Y, A) →⋆ₐ[𝕜] C(X, A)` given by pre-composition
with the continuous function `f`. See `ContinuousMap.compMonoidHom'` and
`ContinuousMap.compAddMonoidHom'`, `ContinuousMap.compRightAlgHom` for bundlings of
pre-composition into a `MonoidHom`, an `AddMonoidHom` and an `AlgHom`, respectively, under
suitable assumptions on `A`. -/
@[simps]
def compStarAlgHom' (f : C(X, Y)) : C(Y, A) →⋆ₐ[𝕜] C(X, A)
where
toFun g := g.comp f
map_one' := one_comp _
map_mul' _ _ := rfl
map_zero' := zero_comp f
map_add' _ _ := rfl
commutes' _ := rfl
map_star' _ := rfl
