English
The auxiliary equivalence is compatible with graded commutativity: auxEquiv comm x equals gradedComm (auxEquiv x).
Русский
auxEquiv совместим с градуированной коммутативностью: auxEquiv comm x = gradedComm (auxEquiv x).
LaTeX
$$$\operatorname{auxEquiv}_R(𝒜,ℬ)(\operatorname{comm}_{𝒜,ℬ}(x)) = \operatorname{gradedComm}_R(𝒜·)(ℬ·)(\operatorname{auxEquiv}_R(𝒜,ℬ)(x))$$$
Lean4
@[simp]
theorem comm_coe_tmul_coe {i j : ι} (a : 𝒜 i) (b : ℬ j) :
comm 𝒜 ℬ (a ᵍ⊗ₜb) = (-1 : ℤˣ) ^ (j * i) • (b ᵍ⊗ₜa : ℬ ᵍ⊗[R] 𝒜) :=
(auxEquiv R ℬ 𝒜).injective <|
by
simp_rw [auxEquiv_comm, auxEquiv_tmul, decompose_coe, ← lof_eq_of R, gradedComm_of_tmul_of,
@Units.smul_def _ _ (_) (_), ← Int.cast_smul_eq_zsmul R]
-- Qualified `map_smul` to avoid a TC timeout https://github.com/leanprover-community/mathlib4/pull/8386
rw [LinearEquiv.map_smul, auxEquiv_tmul]
simp_rw [decompose_coe, lof_eq_of]
