English
A refined formula for gradedMul on tmul of more general tensors expresses a sign and bilinear combination.
Русский
Уточненная формула для gradedMul на tmul обобщённых тензоров выражает знак и билинейную комбинацию.
LaTeX
$$$$ gradedMul_R( a_1 \otimes \ell(b_1), a_2 \otimes b_2 ) = (-1)^{j_1 i_2} (a_1 a_2) \otimes (b_1 b_2). $$$$
Lean4
theorem tmul_of_gradedMul_of_tmul (j₁ i₂ : ι) (a₁ : ⨁ i, 𝒜 i) (b₁ : ℬ j₁) (a₂ : 𝒜 i₂) (b₂ : ⨁ i, ℬ i) :
gradedMul R 𝒜 ℬ (a₁ ⊗ₜ lof R _ ℬ j₁ b₁) (lof R _ 𝒜 i₂ a₂ ⊗ₜ b₂) =
(-1 : ℤˣ) ^ (j₁ * i₂) • ((a₁ * lof R _ 𝒜 _ a₂) ⊗ₜ (lof R _ ℬ _ b₁ * b₂)) :=
by
rw [gradedMul]
dsimp only [curry_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_tmul, map_tmul,
LinearMap.id_coe, id_eq, assoc_symm_tmul, LinearMap.rTensor_tmul, LinearMap.lTensor_tmul]
rw [mul_comm j₁ i₂, gradedComm_of_tmul_of]
-- the tower smul lemmas elaborate too slowly
rw [Units.smul_def, Units.smul_def, ← Int.cast_smul_eq_zsmul R, ← Int.cast_smul_eq_zsmul R]
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specialize `map_smul` to avoid timeouts.
rw [← smul_tmul', LinearEquiv.map_smul, tmul_smul, LinearEquiv.map_smul, LinearMap.map_smul]
dsimp
