coeFnAlgHom — Mathlib

English

There is a natural AlgHom from LocallyConstant(X,Y) to the function algebra X→Y, given by evaluation at each point, compatible with algebra structure.

Русский

Существует естественный AlgHom от LocallyConstant(X,Y) к алгебре функций X→Y, задаваемый по точкам вычислением, совместимый с алгебраической структурой.

LaTeX

$$$\operatorname{coeFnAlgHom}: \operatorname{LocallyConstant}(X,Y) \to_{\mathrm{Alg}} (R)\,(X \to Y)$$$

Lean4

/-- `DFunLike.coe` as an `AlgHom`. -/
@[simps!]
def coeFnAlgHom (R : Type*) [CommSemiring R] [Semiring Y] [Algebra R Y] : LocallyConstant X Y →ₐ[R] X → Y
    where
  toRingHom := coeFnRingHom
  commutes' _ := rfl

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