evalₐ — Mathlib

English

Evaluation as an algebra hom: for a fixed x, the map that takes a locally constant function to its value at x is an algebra hom.

Русский

Оценка в точке как алгеброгомоморфизм: отображение f ↦ f(x) является алгеброгомоморфизмом.

LaTeX

$$$\operatorname{eval}_a(R): X \to \operatorname{AlgHom}(\operatorname{LocallyConstant}(X,Y), Y)$$$

Lean4

/-- Evaluation as an `AlgHom` -/
@[simps!]
def evalₐ (R : Type*) [CommSemiring R] [Semiring Y] [Algebra R Y] (x : X) : LocallyConstant X Y →ₐ[R] Y :=
  (Pi.evalAlgHom _ _ x).comp (coeFnAlgHom R)

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