The Koszul sign automorphism of a tensor product

The Koszul sign is often needed without exchanging the two factors, for example in the pairing between a tensor product and the tensor product of its graded duals. This file constructs the linear automorphism acting by (-1)^(p*q) on bidegree (p,q), and proves its evaluation formula, the corresponding inverse formula, and preservation of total degree.

The construction reuses the quadratic twist of an internal grading: the identity choose(p+q,2) = choose(p,2) + choose(q,2) + p*q supplies the sign. The convention follows E. Getzler and J. D. S. Jones, A-infinity algebras and the cyclic bar complex, Section 1.

noncomputable def TauCeti.InternalGrading.koszulTensorTwist {R : Type u} [CommRing R] {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) : TensorProduct R M N ≃ₗ[R] TensorProduct R M N

The Koszul sign automorphism of a graded tensor product. On bidegree (p,q) it multiplies by (-1)^(p*q), without interchanging the factors.

Equations

• G.koszulTensorTwist H = (TensorProduct.congr G.quadraticTwistEquiv H.quadraticTwistEquiv).trans (G.tensorProduct H).quadraticTwistEquiv

theorem TauCeti.InternalGrading.koszulTensorTwist_tmul {R : Type u} [CommRing R] {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) {p q : ℤ} {x : M} {y : N} (hx : x ∈ G.piece p) (hy : y ∈ H.piece q) : (G.koszulTensorTwist H) (x ⊗ₜ[R] y) = (p * q).negOnePow • x ⊗ₜ[R] y

The sign automorphism evaluates to the Koszul sign on homogeneous pure tensors.

theorem TauCeti.InternalGrading.koszulTensorTwist_symm_tmul {R : Type u} [CommRing R] {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) {p q : ℤ} {x : M} {y : N} (hx : x ∈ G.piece p) (hy : y ∈ H.piece q) : (G.koszulTensorTwist H).symm (x ⊗ₜ[R] y) = (p * q).negOnePow • x ⊗ₜ[R] y

The inverse sign automorphism has the same value on homogeneous pure tensors.

theorem TauCeti.InternalGrading.isHomogeneous_koszulTensorTwist {R : Type u} [CommRing R] {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) : LinearMap.IsHomogeneous (↑(G.koszulTensorTwist H)) (G.tensorProduct H).piece (G.tensorProduct H).piece 0

The Koszul sign automorphism preserves total degree.