gradedComm_algebraMap_tmul — Mathlib

English

The graded braiding commutes with algebra maps in a natural way, swapping the order on pure algebra-map tensors.

Русский

Градуированный браидинг естественно совместим с алгебраобразами: при перестановке модуля сохраняется правильный обмен.

LaTeX

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

Lean4

theorem gradedComm_algebraMap_tmul [DirectSum.GSemiring 𝒜] [DirectSum.GAlgebra R 𝒜] (r : R) (b : ⨁ i, ℬ i) :
    gradedComm R 𝒜 ℬ (algebraMap R _ r ⊗ₜ b) = b ⊗ₜ algebraMap R _ r :=
  gradedComm_of_zero_tmul _ _ _ _ _

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