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 grading is used by tensor products of differential graded 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.tensorProduct_piece_le: a submodule containing every homogeneous pure tensor of total degree n contains the degree-n piece.
• 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 and 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 construction reuses DirectSum.IsInternal.tensorProduct for the bidegree decomposition and DirectSum.IsInternal.iSup_fiber to collect equal total degrees.

theorem TauCeti.InternalGrading.piTensorProduct_ext {R : Type u} [CommSemiring R] {ι : Type u_1} [Finite ι] {M : ι → Type v} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : Type w} [AddCommMonoid N] [Module R N] (G : (i : ι) → InternalGrading R (M i) ℤ) {f g : PiTensorProduct R M →ₗ[R] N} (h : ∀ (q : (i : ι) → (d : ℤ) × ↥((G i).piece ℤ d)), f (⨂ₜ[R] (i : ι), ↑(q i).snd) = g (⨂ₜ[R] (i : ι), ↑(q i).snd)) : f = g

Two linear maps from a tensor product of a finite family of internally graded modules 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.

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.tensorProduct_piece_le {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 : ℤ} {C : Submodule R (TensorProduct R M N)} (h : ∀ (p : ℤ), ∀ x ∈ G.piece ℤ p, ∀ y ∈ H.piece ℤ (n - p), x ⊗ₜ[R] y ∈ C) : (G.tensorProduct H).piece ℤ n ≤ C

A submodule containing every pure tensor of homogeneous elements of total degree n contains the whole degree-n piece of 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.isHomogeneous_assoc {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)) (((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.

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

Tensoring a homogeneous map with the identity on the right preserves its degree.