Tensor products of internally graded modules

The tensor product of internally ℤ-graded modules is graded by total degree. Its degree-n piece is the sum of the images of

G.piece p ⊗ H.piece (n - p)

inside the ambient tensor product. These pieces form an internal direct sum: first use DirectSum.IsInternal.tensorProduct for the bidegree decomposition, then collect bidegrees with the same sum.

The resulting grading has the expected API on pure tensors. In particular, a tensor of elements of degrees p and q has degree p + q, and tensoring homogeneous linear maps adds their degrees. This is the tensor-product compatibility requested in Layer 0 of the DGAInfinity roadmap and supplies the grading used by tensor products of DG objects.

Main definitions

• TauCeti.InternalGrading.tensorProduct: the internal total-degree grading.

Main results

• TauCeti.InternalGrading.tensorProduct_piece_eq_iSup: the degree-n piece is the sum over G.piece p ⊗ H.piece (n - p).
• TauCeti.InternalGrading.tmul_mem_tensorProduct: degrees add on pure tensors.
• TauCeti.InternalGrading.piTensorProduct_ext: linear maps from a finite tensor product agree when they agree on pure tensors of homogeneous elements.
• TauCeti.LinearMap.IsHomogeneous.tensorProduct: tensoring homogeneous maps adds their degrees.
• TauCeti.InternalGrading.isHomogeneous_assoc_symm: reassociation preserves total degree.
• TauCeti.InternalGrading.koszulTwist_tensorProduct: the Koszul twist of the total grading is the tensor product of the Koszul twists of the factors.

The proof reuses Tau Ceti's two-factor internal decomposition theorem DirectSum.IsInternal.tensorProduct; no formalization is vendored.

theorem TauCeti.InternalGrading.piTensorProduct_ext {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] (G : InternalGrading R M) {n : ℕ} {f g : (PiTensorProduct R fun (x : Fin n) => M) →ₗ[R] N} (h : ∀ (q : Fin n → (d : ℤ) × ↥(G.piece d)), f ((PiTensorProduct.tprod R) fun (i : Fin n) => ↑(q i).snd) = g ((PiTensorProduct.tprod R) fun (i : Fin n) => ↑(q i).snd)) : f = g

Two linear maps from a finite tensor product of an internally graded module agree if they agree on pure tensors of homogeneous elements.

noncomputable def TauCeti.InternalGrading.tensorProduct {R : Type u} [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) : InternalGrading R (TensorProduct R M N)

The tensor product of internally graded modules, graded by total degree.

Equations

• G.tensorProduct H = { piece := TauCeti.InternalGrading.tensorProductPiece✝ G H, isInternal := ⋯ }

theorem TauCeti.InternalGrading.tensorProduct_piece_eq_iSup {R : Type u} [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) (n : ℤ) : (G.tensorProduct H).piece n = ⨆ (p : ℤ), Submodule.map₂ (TensorProduct.mk R M N) (G.piece p) (H.piece (n - p))

The degree-n piece of the tensor-product grading is the sum of the tensor-product images whose first degree is p and whose second degree is n - p.

theorem TauCeti.InternalGrading.tmul_mem_tensorProduct {R : Type u} [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid 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) : x ⊗ₜ[R] y ∈ (G.tensorProduct H).piece (p + q)

A pure tensor of elements of degrees p and q is homogeneous of degree p + q in the tensor-product grading.

theorem TauCeti.InternalGrading.isHomogeneous_assoc_symm {R : Type u} [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] (G : InternalGrading R M) (H : InternalGrading R N) (K : InternalGrading R P) : LinearMap.IsHomogeneous (↑(TensorProduct.assoc R M N P).symm) (G.tensorProduct (H.tensorProduct K)).piece ((G.tensorProduct H).tensorProduct K).piece 0

Reassociating a triple tensor product preserves total degree.

theorem TauCeti.InternalGrading.koszulTwist_tensorProduct {R : Type u} [CommRing R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) (q : ℤ) : (G.tensorProduct H).koszulTwist q = TensorProduct.map (G.koszulTwist q) (H.koszulTwist q)

The Koszul twist for the total grading of a tensor product is the tensor product of the Koszul twists of the factors.

theorem TauCeti.LinearMap.IsHomogeneous.tensorProduct {R : Type u} [CommSemiring R] {M : Type v} {N : Type w} {M' : Type v'} {N' : Type w'} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N'] {G : InternalGrading R M} {H : InternalGrading R N} {G' : InternalGrading R M'} {H' : InternalGrading R N'} {f : M →ₗ[R] M'} {g : N →ₗ[R] N'} {a b : ℤ} (hf : IsHomogeneous f G.piece G'.piece a) (hg : IsHomogeneous g H.piece H'.piece b) : IsHomogeneous (TensorProduct.map f g) (G.tensorProduct H).piece (G'.tensorProduct H').piece (a + b)

Tensoring homogeneous linear maps adds their degrees for the total tensor-product gradings.