constₐ — Mathlib

English

The constant map from Y to LocallyConstant(X,Y) is an AlgHom from Y to LocallyConstant(X,Y) when Y is a semiring with an associated algebra structure over R.

Русский

Постоянное отображение из Y в LocallyConstant(X,Y) является AlgHom из Y в LocallyConstant(X,Y) при наличии структуры алгебры над R.

LaTeX

$$$\\mathrm{const}_{\\mathsf{A}} : Y \\to_{\\mathsf{A}}[R] \\operatorname{LocallyConstant}(X,Y)$ with $\\mathrm{toRingHom}$ and $\\mathrm{commutes}$ properties.$$

Lean4

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

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