gradedComm_tmul_algebraMap — Mathlib

English

When the right tensor factor is algebraMap r, the graded commutativity distributes that scalar to the swapped position.

Русский

Когда в правом факторе тензора стоит algebraMap r, знак браидинга переносит скаляр в противоположное положение.

LaTeX

$$$$ gradedComm_R(\mathcal{A},\mathcal{B})(algebraMap_R(r) \otimes b) = b \otimes algebraMap_R(r). $$$$

Lean4

theorem gradedComm_tmul_algebraMap [DirectSum.GSemiring ℬ] [DirectSum.GAlgebra R ℬ] (a : ⨁ i, 𝒜 i) (r : R) :
    gradedComm R 𝒜 ℬ (a ⊗ₜ algebraMap R _ r) = algebraMap R _ r ⊗ₜ a :=
  gradedComm_tmul_of_zero _ _ _ _ _

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