The internal total-degree grading of tensor words

The total-letter-degree pieces of the coaugmented tensor coalgebra form an internal direct sum. Thus every tensor word has a unique finite decomposition by cohomological degree, independently of its decomposition by tensor length. The empty word has degree zero.

TensorWords.grading uses the existing TensorWords.gradedPiece submodules. Its Koszul twist is the letterwise extension of the twist of the generating module. This identifies the sign in the coalgebra coderivation equation with the sign of the total grading, and allows the cofree bar comodule to use the tensor-product grading.

The independence proof uses degree projections obtained by extending multilinear maps on homogeneous pieces. No freeness or flatness assumption on the generating module is needed.

References

• E. Getzler and J. D. Jones, A-infinity algebras and the cyclic bar complex, Sections 1–2.
• B. Keller, Introduction to A-infinity algebras and modules, Section 3.6.

theorem TauCeti.TensorWords.iSupIndep_gradedPiece {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) : iSupIndep (gradedPiece G)

Distinct total-letter-degree pieces are independent, including in characteristic two.

theorem TauCeti.TensorWords.isInternal_gradedPiece {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) : DirectSum.IsInternal (gradedPiece G)

The total-degree pieces of the coaugmented tensor coalgebra form an internal direct sum.

noncomputable def TauCeti.TensorWords.grading {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) : InternalGrading R (TensorWords R M)

Tensor words graded by the sum of the cohomological degrees of their letters.

Equations

• TauCeti.TensorWords.grading G = { piece := TauCeti.TensorWords.gradedPiece G, isInternal := ⋯ }

@[simp]

theorem TauCeti.TensorWords.grading_piece {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) : (grading G).piece = gradedPiece G

The internal grading uses the total-letter-degree pieces.

@[instance_reducible]

noncomputable instance TauCeti.TensorWords.instDecompositionIntSubmoduleGradedPiece {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) : DirectSum.Decomposition (gradedPiece G)

Total-degree decomposition is available on the existing degree pieces.

Equations

• TauCeti.TensorWords.instDecompositionIntSubmoduleGradedPiece G = DirectSum.IsInternal.chooseDecomposition (TauCeti.TensorWords.gradedPiece G) ⋯

theorem TauCeti.TensorWords.coe_decompose_of_tprod {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) {n : ℕ} (d : Fin n → ℤ) (x : Fin n → M) (hx : ∀ (i : Fin n), x i ∈ G.piece (d i)) (p : ℤ) : ↑(((DirectSum.decompose (gradedPiece G)) ((of R M n) ((PiTensorProduct.tprod R) x))) p) = if ∑ i : Fin n, d i = p then (of R M n) ((PiTensorProduct.tprod R) x) else 0

The degree-p component of a homogeneous pure word is that word when its total degree is p, and zero otherwise.

theorem TauCeti.TensorWords.one_mem_gradedPiece {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) : 1 ∈ gradedPiece G 0

The empty word belongs to degree zero.

theorem TauCeti.TensorWords.counit_eq_zero_of_mem_gradedPiece {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) {p : ℤ} {w : TensorWords R M} (hw : w ∈ gradedPiece G p) (hp : p ≠ 0) : (counit R M) w = 0

The counit is supported in total cohomological degree zero.

@[simp]

theorem TauCeti.TensorWords.koszulTwist_grading {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) (q : ℤ) : (grading G).koszulTwist q = map (G.koszulTwist q)

The total-degree Koszul twist is exactly the letterwise Koszul twist.

theorem TauCeti.TensorWords.isHomogeneous_deconcatenation {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) : LinearMap.IsHomogeneous (deconcatenation R M) (grading G).piece ((grading G).tensorProduct (grading G)).piece 0

Deconcatenation preserves total cohomological degree: the degrees of the two cut halves add to the degree of the original word.

theorem TauCeti.TensorWords.isHomogeneous_rid_comp_lTensor_counit {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {N : Type uN} [AddCommGroup N] [Module R N] (G : InternalGrading R N) (H : InternalGrading R M) : LinearMap.IsHomogeneous (↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit) (G.tensorProduct (grading H)).piece G.piece 0

Applying the tensor-coalgebra counit to the tensor-word factor preserves total degree for the tensor-product grading of N ⊗ Tᶜ(M): only the degree-zero part of the tensor word survives.