galgebra_toFun_def — Mathlib

English

The evaluation map on the graded algebra used to define the action of R on the graded tensor powers is exactly the algebra map algebraMap₀.

Русский

Оценочная отображение для градуированной алгебры, задающее действие R на градуированные тензорные степени, совпадает с отображением algebraMap₀.

LaTeX

$$$ DirectSum.GAlgebra.toFun (A := fun i \\mapsto ⨂[R]^i M) r = algebraMap_0(r) $$$

Lean4

theorem galgebra_toFun_def (r : R) : DirectSum.GAlgebra.toFun (A := fun i ↦ ⨂[R]^i M) r = algebraMap₀ r :=
  rfl

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