English
Auxiliary construction implementing graded commutativity on direct sums of graded components.
Русский
Вспомогательное построение, реализующее градуированную симметрию на прямых суммах градуированных компонентов.
LaTeX
$$$\mathrm{gradedCommAux} : DirectSum \to Module\; R$$$
Lean4
/-- Auxiliary construction used to build `TensorProduct.gradedComm`.
This operates on direct sums of tensors instead of tensors of direct sums. -/
def gradedCommAux : DirectSum _ 𝒜ℬ →ₗ[R] DirectSum _ ℬ𝒜 :=
by
refine DirectSum.toModule R _ _ fun i => ?_
have o := DirectSum.lof R _ ℬ𝒜 i.swap
have s : ℤˣ := ((-1 : ℤˣ) ^ (i.1 * i.2 : ι) : ℤˣ)
exact (s • o) ∘ₗ (TensorProduct.comm R _ _).toLinearMap