English
The functor C(X, ·)₀ →⋆ₙₐ[M] C(X, S)₀ sending a zero-preserving star-algebra homomorphism φ: R →⋆ₙₐ[M] S to the postcomposition φ ∘ -, yields a nonunital star-algebra homomorphism between zero-preserving continuous map spaces, respecting the star and algebraic structures.
Русский
Функтор C(X, ·)₀ →⋆ₙₐ[M] C(X, S)₀ отправляет нуль-сохраняющий звездо-алгебр-гомоморфизм φ: R →⋆ₙₐ[M] S в гомоморфизм после композиции φ ∘ -, сохраняя структуру звезды и алгебры.
LaTeX
$$$\text{nonUnitalStarAlgHomPostcomp}: C(X,R)₀ \to⋆ₙₐ[M] C(X,S)₀$$$
Lean4
/-- The functor `C(X, ·)₀` from non-unital topological star algebras (with non-unital continuous
star homomorphisms) to non-unital star algebras. -/
@[simps apply]
def nonUnitalStarAlgHom_postcomp (φ : R →⋆ₙₐ[M] S) (hφ : Continuous φ) : C(X, R)₀ →⋆ₙₐ[M] C(X, S)₀
where
toFun := .comp ⟨⟨φ, hφ⟩, by simp⟩
map_zero' := ext <| by simp
map_add' _ _ := ext <| by simp
map_mul' _ _ := ext <| by simp
map_star' _ := ext <| by simp [map_star]
map_smul' r f := ext <| by simp
