Reduced deconcatenation is coassociative #
TauCeti.ReducedTensorWords.deconcatenation cuts a nonempty tensor word at every nontrivial
position. This file proves that it is coassociative by including a reduced word into
TauCeti.TensorWords, using coassociativity of full deconcatenation there, and projecting every
tensor factor back to positive length. The two degenerate cuts contain an empty-word factor and
therefore vanish under the projection, leaving exactly reduced deconcatenation.
Main results #
TauCeti.ReducedTensorWords.deconcatenation_coassoc: reduced deconcatenation is coassociative.
References #
- E. Getzler and J. D. S. Jones, A-infinity algebras and the cyclic bar complex, Sections 1--2.
- B. Keller, Introduction to A-infinity algebras and modules, Sections 3.1 and 3.6.
theorem
TauCeti.ReducedTensorWords.deconcatenation_coassoc
(R : Type uR)
(M : Type uM)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
↑(TensorProduct.assoc R (ReducedTensorWords R M) (ReducedTensorWords R M) (ReducedTensorWords R M)) ∘ₗ LinearMap.rTensor (ReducedTensorWords R M) (deconcatenation R M) ∘ₗ deconcatenation R M = LinearMap.lTensor (ReducedTensorWords R M) (deconcatenation R M) ∘ₗ deconcatenation R M
Reduced deconcatenation is coassociative: cutting a reduced word twice gives the same sum of three blocks whether the second cut is made in the left or right factor.