algebraMap_gradedMul — Mathlib

English

Algebra maps interact with gradedMul in a way that mimics linearity and compatibility with the grading.

Русский

Алгебраобраза взаимодействуют с gradedMul так же, как линейность и совместимость со степенями градации.

LaTeX

$$$$ gradedMul_R( x, algebraMap_R(r) ) = algebraMap_R(r) \otimes x. $$$$

Lean4

theorem algebraMap_gradedMul (r : R) (x : (⨁ i, 𝒜 i) ⊗[R] (⨁ i, ℬ i)) :
    gradedMul R 𝒜 ℬ (algebraMap R _ r ⊗ₜ 1) x = r • x :=
  by
  suffices gradedMul R 𝒜 ℬ (algebraMap R _ r ⊗ₜ 1) = DistribMulAction.toLinearMap R _ r by
    exact DFunLike.congr_fun this x
  ext ia a ib b
  dsimp
  erw [tmul_of_gradedMul_of_tmul]
  rw [zero_mul, uzpow_zero, one_smul, smul_tmul']
  erw [one_mul, _root_.Algebra.smul_def]

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