Extending reduced endomorphisms to tensor words

TauCeti.TensorWords = ⨆_{n ≥ 0} M^{⊗ n} is the coaugmented tensor coalgebra and TauCeti.ReducedTensorWords = ⨆_{n ≥ 1} M^{⊗ n} the reduced one, sitting in it as the summand of the words of positive length by TauCeti.TensorWords.reducedInclusion, with retraction TauCeti.TensorWords.reducedProjection. Any endomorphism of the reduced words therefore has a canonical extension to all tensor words, the one that is zero on the empty word: TauCeti.TensorWords.extendReduced.

The extension is what carries the coderivation theory of the reduced coalgebra over to the coaugmented one, whose coproduct admits the two degenerate cuts at the ends of a word. The extension preserves the three properties that the module and bimodule theories need from a coderivation over b: the square-zero law TauCeti.TensorWords.extendReduced_sq, homogeneity in the total letter degree TauCeti.TensorWords.isHomogeneous_extendReduced, and the q-twisted co-Leibniz identity TauCeti.TensorWords.isGradedCoderivation_extendReduced.

Main definitions

• TauCeti.TensorWords.extendReduced: extend an endomorphism of the reduced words by zero on the empty word.

Main results

• TauCeti.TensorWords.extendReduced_comp_reducedInclusion: the extension restricts to the endomorphism it extends.
• TauCeti.TensorWords.extendReduced_sq: the extension of a square-zero endomorphism squares to zero.
• TauCeti.TensorWords.isHomogeneous_extendReduced: the extension of a homogeneous endomorphism is homogeneous of the same degree in the total letter degree.
• TauCeti.TensorWords.isGradedCoderivation_extendReduced: the extension of a q-twisted graded coderivation of the reduced words is one of the coaugmented words.

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, Section 3.6.

noncomputable def TauCeti.TensorWords.extendReduced {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M) : TensorWords R M →ₗ[R] TensorWords R M

The extension of an endomorphism of the reduced tensor words to all tensor words: it deletes the empty word, applies the endomorphism, and includes the result, so that the empty word is annihilated.

Equations

• TauCeti.TensorWords.extendReduced f = TauCeti.TensorWords.reducedInclusion R M ∘ₗ f ∘ₗ TauCeti.TensorWords.reducedProjection R M

@[simp]

theorem TauCeti.TensorWords.extendReduced_apply {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M) (w : TensorWords R M) : (extendReduced f) w = (reducedInclusion R M) (f ((reducedProjection R M) w))

On a word the extension is the inclusion of the value of the endomorphism on the positive-length part of that word.

@[simp]

theorem TauCeti.TensorWords.extendReduced_of_zero {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M) (z : TensorPower R 0 M) : (extendReduced f) ((of R M 0) z) = 0

The extension annihilates every word of length zero.

@[simp]

theorem TauCeti.TensorWords.extendReduced_one {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M) : (extendReduced f) 1 = 0

The extension annihilates the empty word.

theorem TauCeti.TensorWords.extendReduced_of {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M) {n : ℕ} (hn : 0 < n) (z : TensorPower R n M) : (extendReduced f) ((of R M n) z) = (reducedInclusion R M) (f ((ReducedTensorWords.of R M ⟨n, hn⟩) z))

On a word of positive length the extension is the inclusion of the value of the endomorphism.

theorem TauCeti.TensorWords.extendReduced_comp_reducedInclusion {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M) : extendReduced f ∘ₗ reducedInclusion R M = reducedInclusion R M ∘ₗ f

The extension agrees with the endomorphism it extends on the words of positive length.

theorem TauCeti.TensorWords.extendReduced_reducedInclusion {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M) (w : ReducedTensorWords R M) : (extendReduced f) ((reducedInclusion R M) w) = (reducedInclusion R M) (f w)

The extension acts on the words of positive length as the endomorphism it extends.

@[simp]

theorem TauCeti.TensorWords.extendReduced_sq {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M) (hf : f ∘ₗ f = 0) : extendReduced f ∘ₗ extendReduced f = 0

The extension of a square-zero endomorphism squares to zero.

theorem TauCeti.TensorWords.isHomogeneous_extendReduced {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M} {r : ℤ} {f : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hf : LinearMap.IsHomogeneous f (ReducedTensorWords.gradedPiece G) (ReducedTensorWords.gradedPiece G) r) : LinearMap.IsHomogeneous (extendReduced f) (gradedPiece G) (gradedPiece G) r

The extension of a homogeneous endomorphism of the reduced words is homogeneous of the same degree in the total letter degree of the coaugmented words.

theorem TauCeti.TensorWords.isGradedCoderivation_extendReduced {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M} {q : ℤ} {f : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hf : ReducedTensorWords.IsGradedCoderivation G q f) : IsGradedCoderivation G q (extendReduced f)

The extension of a q-twisted graded coderivation of the reduced tensor words is a q-twisted graded coderivation of the coaugmented ones.