evalStarAlgHom — Mathlib

English

The map compStarAlgHom' respects scalar multiplication and algebra structure, i.e., (φ, hφ) acts compatibly with the algebra operations on C(X,A).

Русский

Представление compStarAlgHom' сохраняет умножение по скалярам и алгебраические структуры, т.е. сохраняется совместимость с операциями алгебры на C(X,A).

LaTeX

$$$(\mathrm{compStarAlgHom}'(f)) (k \cdot g) = k \cdot (\mathrm{compStarAlgHom}'(f))(g)$$$

Lean4

/-- Evaluation of continuous maps at a point, bundled as a star algebra homomorphism. -/
@[simps!]
def evalStarAlgHom [StarRing R] [ContinuousStar R] (x : X) : C(X, R) →⋆ₐ[S] R :=
  { ContinuousMap.evalAlgHom S R x with map_star' := fun _ => rfl }

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