gradedCommAux_comp_gradedCommAux — Mathlib

English

The braiding operation on tensor products of externally graded algebras is an involution: applying the braiding twice yields the identity.

Русский

Оперaция браидинга над тензорными произведениями внешне-градуированных алгебр является инволюцией: применение браидинга дважды даёт тождество.

LaTeX

$$$$\; gradedCommAux_R(\mathcal{A},\mathcal{B}) \circ gradedCommAux_R(\mathcal{B},\mathcal{A}) = \mathrm{Id}. $$$$

Lean4

@[simp]
theorem gradedCommAux_comp_gradedCommAux : gradedCommAux R 𝒜 ℬ ∘ₗ gradedCommAux R ℬ 𝒜 = LinearMap.id :=
  by
  ext i a b
  dsimp
  rw [gradedCommAux_lof_tmul, LinearMap.map_smul_of_tower, gradedCommAux_lof_tmul, smul_smul, mul_comm i.2 i.1,
    Int.units_mul_self, one_smul]

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