gradedComm_of_zero_tmul — Mathlib

English

When swapping with a homogeneous zero-degree component, the sign is trivial and we simply swap.

Русский

При обмене с нулевой степенью компонента знак тривиален; простая перестановка.

LaTeX

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

Lean4

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

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