toContinuousMapHom — Mathlib

English

There is a canonical map from the star-algebra homomorphisms to the underlying continuous maps, given by forgetting the extra star-structure.

Русский

Существует каноническое отображение из гомоморфизмов звёздной алгебры к их базовым непрерывным отображениям без учета звезды.

LaTeX

$$$\\text{coe\_toContinuousMapHom} : (\\text{ContinuousMapZero} \\to \\text{ContinuousMap}) \\to \\text{...}$$$

Lean4

/-- The coercion `C(X, R)₀ → C(X, R)` bundled as a non-unital star algebra homomorphism. -/
@[simps]
def toContinuousMapHom [StarRing R] [ContinuousStar R] : C(X, R)₀ →⋆ₙₐ[R] C(X, R)
    where
  toFun f := f
  map_smul' _ _ := rfl
  map_zero' := rfl
  map_add' _ _ := rfl
  map_mul' _ _ := rfl
  map_star' _ := rfl

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