English
The map sending a star-algebra morphism ψ : A →⋆ₐ[𝕜] B to the induced map between spectra is continuous and natural with respect to composition.
Русский
При отображении гомоморфизма звёздных алгебр ψ: A →⋆ₐ[𝕜] B на соответствующий переход между спектрами сохраняется непрерывность и совместимость с композицией.
LaTeX
$$$compContinuousMap(\\\\psi): C(CharacterSpace_{𝕜} B, CharacterSpace_{𝕜} A) \\\\text{ defined by } (compContinuousMap(\\\\psi))(\\\\phi)=\\\\,\\\\phi\\\\circ\\\\psi.$$$
Lean4
/-- The functorial map taking `ψ : A →⋆ₐ[ℂ] B` to a continuous function
`characterSpace ℂ B → characterSpace ℂ A` obtained by pre-composition with `ψ`. -/
@[simps]
noncomputable def compContinuousMap (ψ : A →⋆ₐ[𝕜] B) : C(characterSpace 𝕜 B, characterSpace 𝕜 A)
where
toFun φ := equivAlgHom.symm ((equivAlgHom φ).comp ψ.toAlgHom)
continuous_toFun :=
Continuous.subtype_mk (continuous_of_continuous_eval fun a => map_continuous <| gelfandTransform 𝕜 B (ψ a)) _
