The total-degree decomposition of a finite tensor product

If each factor is the internal direct sum of its homogeneous pieces, the total-degree pieces of their finite tensor product also form an internal direct sum. This equips the existing TauCeti.PiTensorProduct.totalDegreePiece with DirectSum.Decomposition, so that every tensor has a unique finite homogeneous expansion. In particular the construction applies to tensor products of total resolutions, where a comparison map is assembled degree by degree.

The construction distributes the tensor product over the direct sums using Mathlib's PiTensorProduct.ofDirectSumEquiv, then collects multidegrees with the same sum. It needs no flatness hypothesis: the inclusions of the homogeneous pieces are split. For an empty family, the empty tensor product is concentrated in degree zero; the same construction covers this case.

@[instance_reducible]

noncomputable instance TauCeti.PiTensorProduct.totalDegreePieceDecomposition {R : Type u} [CommSemiring R] {ι : Type v} [Fintype ι] {A : Type w} [AddCommMonoid A] [DecidableEq A] {M : ι → Type z} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (ℳ : (i : ι) → A → Submodule R (M i)) [hℳ : (i : ι) → DirectSum.Decomposition (ℳ i)] : DirectSum.Decomposition (totalDegreePiece ι ℳ)

The total-degree pieces of a finite tensor product decompose it whenever the homogeneous pieces decompose every factor. The inverse to recomposition first expands each factor and then collects the finitely many multidegrees by their sum.