gradedComm_algebraMap — Mathlib

English

The graded braiding on a tensor product with an algebra-map tensor respects the scalar action on both sides.

Русский

Градуированное браидинг-отображение на тензорном произведении с алгебраобразом учитывает скалярное действие слева и справа.

LaTeX

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

Lean4

theorem gradedComm_algebraMap [DirectSum.GSemiring 𝒜] [DirectSum.GSemiring ℬ] [DirectSum.GAlgebra R 𝒜]
    [DirectSum.GAlgebra R ℬ] (r : R) : gradedComm R 𝒜 ℬ (algebraMap R _ r) = algebraMap R _ r :=
  (gradedComm_algebraMap_tmul R 𝒜 ℬ r 1).trans (Algebra.TensorProduct.algebraMap_apply' r).symm

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