compStarAlgHom_comp — Mathlib

English

The operation compStarAlgHom(X) assigns to a star-algebra homomorphism φ: A →⋆ₐ B and a continuous map h: X → A a star-algebra homomorphism from C(X, A) to C(X, B) given by post-composition with φ, i.e., map f to φ ∘ f.

Русский

Операция compStarAlgHom задаёт звездную алгебраическую гомоморфизм от C(X,A) к C(X,B) путём композиции с φ: f ↦ φ ∘ f.

LaTeX

$$$\mathrm{compStarAlgHom}\,X\; (φ) : C(X,A) \to⋆ₐ B C(X,B)$ определена таким образом, что $f \mapsto φ \circ f$$$

Lean4

/-- `ContinuousMap.compStarAlgHom` is functorial. -/
theorem compStarAlgHom_comp (φ : A →⋆ₐ[𝕜] B) (ψ : B →⋆ₐ[𝕜] C) (hφ : Continuous φ) (hψ : Continuous ψ) :
    compStarAlgHom X (ψ.comp φ) (hψ.comp hφ) = (compStarAlgHom X ψ hψ).comp (compStarAlgHom X φ hφ) :=
  rfl

Похожие утверждения