toTensorAlgebra_galgebra_toFun — Mathlib

English

The graded algebra lift is compatible with the scalar map: applying the lift to a scalar equals the algebra map of that scalar.

Русский

Поднятие градационной алгебры совместимо с отображением скаляра: применение подъёма к скаляру равняется алгебраическому отображению этого скаляра.

LaTeX

$$$ toTensorAlgebra (DirectSum.GAlgebra.toFun (R := R) (A := fun n => ⨂[R]^n M) r) = algebraMap _ _ r $$$

Lean4

@[simp]
theorem toTensorAlgebra_galgebra_toFun (r : R) :
    TensorPower.toTensorAlgebra (DirectSum.GAlgebra.toFun (R := R) (A := fun n => ⨂[R]^n M) r) = algebraMap _ _ r := by
  rw [TensorPower.galgebra_toFun_def, TensorPower.algebraMap₀_eq_smul_one, LinearMap.map_smul,
    TensorPower.toTensorAlgebra_gOne, Algebra.algebraMap_eq_smul_one]

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