coeFnAlgHom — Mathlib

English

There is a canonical algebra homomorphism which regards a continuous map as a function, i.e., for f in C(α,A), the map to α → A equals its evaluation.

Русский

Существует канонический алгеброгомоморфизм, который рассматривает непрерывную карту как обычную функцию: для f в C(α,A) отображение в α → A равно его значению.

LaTeX

$$$\\mathrm{coeFnAlgHom}: C(α,A) \\to_{R} (α \\to A), \\quad \\mathrm{coeFnAlgHom}(f) = (x \\mapsto f(x)).$$$

Lean4

/-- Coercion to a function as an `AlgHom`. -/
@[simps!]
def coeFnAlgHom : C(α, A) →ₐ[R] α → A :=
  { (ContinuousMap.coeFnRingHom : C(α, A) →+* _) with commutes' := fun _ => rfl }

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