gradedComm_tmul_of_zero — Mathlib

English

If the A-component is arbitrary and the B-component lies in degree 0, braiding simply commutes without a sign.

Русский

Если компонент A произволен, а компонент B имеет градуировку 0, браидинг просто переставляет без знака.

LaTeX

$$$$ gradedComm_R(\mathcal{A},\mathcal{B})(a \otimes b) = b \otimes a, \quad b\in \mathcal{B}_0. $$$$

Lean4

theorem gradedComm_tmul_of_zero (a : ⨁ i, 𝒜 i) (b : ℬ 0) : gradedComm R 𝒜 ℬ (a ⊗ₜ lof R _ ℬ 0 b) = lof R _ ℬ _ b ⊗ₜ a :=
  by
  suffices
    (gradedComm R 𝒜 ℬ).toLinearMap ∘ₗ (TensorProduct.mk R (⨁ i, 𝒜 i) (⨁ i, ℬ i)).flip (lof R _ ℬ 0 b) =
      TensorProduct.mk R _ _ (lof R _ ℬ 0 b)
    from DFunLike.congr_fun this a
  ext i a
  dsimp
  rw [gradedComm_of_tmul_of, zero_mul, uzpow_zero, one_smul]

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