Composable words in the bar construction of a graded linear quiver

The reduced bar construction of the total module of morphisms of a graded linear quiver C is spanned by words z₀ ⋯ zₙ₋₁ of morphisms zᵢ : aᵢ ⟶ bᵢ. Such a word is composable from X to Y when the source of each morphism is the target of the next one, aₙ₋₁ = X and b₀ = Y; this is the input order of the operations of an A∞ category. This file introduces the span TauCeti.GradedLinearQuiver.composableWords R X Y of the composable words from X to Y and the span TauCeti.GradedLinearQuiver.nonComposableWords R C of the words which are not composable. Together they span the whole bar construction.

The Taylor maps of A∞ categories and of A∞ functors send composable words to morphisms between the images of their endpoints, and other words to zero. This is the word-level form TauCeti.GradedLinearQuiver.IsWordPathCompatible of path compatibility of their components (TauCeti.GradedLinearQuiver.isWordPathCompatible_iff). Path compatibility propagates through the two constructions out of which bar differentials and bar maps are built: the graded Taylor expansion of a path-compatible endomorphism preserves both spans, and the coalgebra morphism with path-compatible Taylor components along an injective map of objects sends each span to the corresponding span. Moreover, a relation between two Taylor maps which only holds on composable words is inherited by their graded Taylor expansions and by the coalgebra morphisms they generate. These statements are what is needed to compare A∞ structures on categories induced along a non-injective map of objects, where strings which are not composable can become composable after applying the map.

Main definitions

• TauCeti.GradedLinearQuiver.composableWords: the span of the composable words from X to Y.
• TauCeti.GradedLinearQuiver.nonComposableWords: the span of the words which are not composable.
• TauCeti.GradedLinearQuiver.IsWordPathCompatible: a map from words to morphisms sending composable words to morphisms between the images of their endpoints and other words to zero.

Main results

• TauCeti.GradedLinearQuiver.iSup_composableWords_sup_nonComposableWords: composable and non-composable words span the bar construction, so linear maps agreeing on both are equal (TauCeti.GradedLinearQuiver.linearMap_ext_composableWords).
• TauCeti.GradedLinearQuiver.isWordPathCompatible_iff: word-level path compatibility is path compatibility of the restrictions to words of each positive length.
• TauCeti.GradedLinearQuiver.IsWordPathCompatible.coalgHom_mem_composableWords and TauCeti.GradedLinearQuiver.IsWordPathCompatible.coalgHom_mem_nonComposableWords: the coalgebra morphism with path-compatible Taylor components preserves composability.
• TauCeti.GradedLinearQuiver.IsWordPathCompatible.gradedCoderiv_mem_composableWords and TauCeti.GradedLinearQuiver.IsWordPathCompatible.gradedCoderiv_mem_nonComposableWords: so does the graded Taylor expansion of a path-compatible map.
• TauCeti.GradedLinearQuiver.map_coalgHom_of_mem_composableWords and TauCeti.GradedLinearQuiver.map_gradedCoderiv_of_mem_composableWords: relations between Taylor maps on composable words extend to their coalgebra morphisms and graded Taylor expansions.
• TauCeti.GradedLinearQuiver.IsWordPathCompatible.eq_of_totalHomMap_eq: path-compatible maps into a quiver induced along a map of objects are determined by their images on composable words.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 7.
• V. Lyubashenko, Category of A-infinity-categories, Homology, Homotopy and Applications 5 (2003), for the bar construction of an A∞ category over its set of objects.

Composable and non-composable words

noncomputable def TauCeti.GradedLinearQuiver.composableWords (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] (X Y : C) : Submodule R (ReducedTensorWords R (TotalHom R C))

The span of the composable words from X to Y: the words z₀ ⋯ zₙ₋₁ of morphisms zᵢ : aᵢ ⟶ bᵢ, with n positive, in which the source of each morphism is the target of the next one, the source of the last is X and the target of the first is Y.

noncomputable def TauCeti.GradedLinearQuiver.nonComposableWords (R : Type w) [CommRing R] (C : Type u) [GradedLinearQuiver R C] : Submodule R (ReducedTensorWords R (TotalHom R C))

The span of the non-composable words: the words z₀ ⋯ zₙ₋₁ of morphisms zᵢ : aᵢ ⟶ bᵢ, with n positive, in which the source of some morphism is not the target of the next one.

theorem TauCeti.GradedLinearQuiver.of_tprod_mem_composableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} (hn : 0 < n) {a b : ℕ → C} {z : ℕ → TotalHom R C} (hz : ∀ i < n, z i ∈ (homInclusion (a i) (b i)).range) (hab : IsComposableString a b n) : (ReducedTensorWords.of R (TotalHom R C) ⟨n, hn⟩) ((PiTensorProduct.tprod R) fun (i : Fin n) => z ↑i) ∈ composableWords R (a (n - 1)) (b 0)

A word of morphisms along a composable string is a composable word from the source of its last morphism to the target of its first.

theorem TauCeti.GradedLinearQuiver.of_tprod_mem_nonComposableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} (hn : 0 < n) {a b : ℕ → C} {z : ℕ → TotalHom R C} (hz : ∀ i < n, z i ∈ (homInclusion (a i) (b i)).range) (hab : ¬IsComposableString a b n) : (ReducedTensorWords.of R (TotalHom R C) ⟨n, hn⟩) ((PiTensorProduct.tprod R) fun (i : Fin n) => z ↑i) ∈ nonComposableWords R C

A word of morphisms along a string which is not composable is a non-composable word.

theorem TauCeti.GradedLinearQuiver.composableWords_induction {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {X Y : C} {P : ReducedTensorWords R (TotalHom R C) → Prop} (word : ∀ (n : ℕ) (hn : 0 < n) (a b : ℕ → C) (z : ℕ → TotalHom R C), (∀ i < n, z i ∈ (homInclusion (a i) (b i)).range) → IsComposableString a b n → a (n - 1) = X → b 0 = Y → P ((ReducedTensorWords.of R (TotalHom R C) ⟨n, hn⟩) ((PiTensorProduct.tprod R) fun (i : Fin n) => z ↑i))) (zero : P 0) (add : ∀ (x y : ReducedTensorWords R (TotalHom R C)), P x → P y → P (x + y)) (smul : ∀ (r : R) (x : ReducedTensorWords R (TotalHom R C)), P x → P (r • x)) {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ composableWords R X Y) : P w

Induction on composable words: a property of words closed under sums and scalar multiples and holding on the words along composable strings from X to Y holds on all composable words from X to Y.

theorem TauCeti.GradedLinearQuiver.nonComposableWords_induction {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {P : ReducedTensorWords R (TotalHom R C) → Prop} (word : ∀ (n : ℕ) (hn : 0 < n) (a b : ℕ → C) (z : ℕ → TotalHom R C), (∀ i < n, z i ∈ (homInclusion (a i) (b i)).range) → ¬IsComposableString a b n → P ((ReducedTensorWords.of R (TotalHom R C) ⟨n, hn⟩) ((PiTensorProduct.tprod R) fun (i : Fin n) => z ↑i))) (zero : P 0) (add : ∀ (x y : ReducedTensorWords R (TotalHom R C)), P x → P y → P (x + y)) (smul : ∀ (r : R) (x : ReducedTensorWords R (TotalHom R C)), P x → P (r • x)) {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ nonComposableWords R C) : P w

Induction on non-composable words: a property of words closed under sums and scalar multiples and holding on the words along strings which are not composable holds on all non-composable words.

theorem TauCeti.GradedLinearQuiver.iSup_composableWords_sup_nonComposableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] : (⨆ (X : C), ⨆ (Y : C), composableWords R X Y) ⊔ nonComposableWords R C = ⊤

Composable and non-composable words span the bar construction.

theorem TauCeti.GradedLinearQuiver.linearMap_ext_composableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {M : Type u_1} [AddCommMonoid M] [Module R M] {f g : ReducedTensorWords R (TotalHom R C) →ₗ[R] M} (hc : ∀ (X Y : C), ∀ w ∈ composableWords R X Y, f w = g w) (hn : ∀ w ∈ nonComposableWords R C, f w = g w) : f = g

Two linear maps out of the bar construction which agree on composable and on non-composable words are equal.

Building composable words

theorem TauCeti.GradedLinearQuiver.ofLetter_mem_composableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {X Y : C} {u : TotalHom R C} (hu : u ∈ (homInclusion X Y).range) : (ReducedTensorWords.ofLetter R (TotalHom R C)) u ∈ composableWords R X Y

A single morphism X ⟶ Y is a composable word from X to Y.

theorem TauCeti.GradedLinearQuiver.subword_mem_composableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} {a b : ℕ → C} {z : ℕ → TotalHom R C} (hz : ∀ i < n, z i ∈ (homInclusion (a i) (b i)).range) {p s : ℕ} (hab : IsComposableString (fun (j : ℕ) => a (p + j)) (fun (j : ℕ) => b (p + j)) s) (hs : 0 < s) (hps : p + s ≤ n) : ReducedTensorWords.subword R (fun (i : Fin n) => z ↑i) p s ∈ composableWords R (a (p + s - 1)) (b p)

A composable block of a word of morphisms is a composable word from the source of its last morphism to the target of its first.

theorem TauCeti.GradedLinearQuiver.subword_mem_nonComposableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} {a b : ℕ → C} {z : ℕ → TotalHom R C} (hz : ∀ i < n, z i ∈ (homInclusion (a i) (b i)).range) {p s : ℕ} (hab : ¬IsComposableString (fun (j : ℕ) => a (p + j)) (fun (j : ℕ) => b (p + j)) s) (hps : p + s ≤ n) : ReducedTensorWords.subword R (fun (i : Fin n) => z ↑i) p s ∈ nonComposableWords R C

A block of a word of morphisms which is not composable is a non-composable word.

theorem TauCeti.GradedLinearQuiver.exists_subword_mem_composableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} {a b : ℕ → C} {z : ℕ → TotalHom R C} (hz : ∀ i < n, z i ∈ (homInclusion (a i) (b i)).range) (hab : IsComposableString a b n) (p s : ℕ) : ∃ (X : C) (Y : C), ReducedTensorWords.subword R (fun (i : Fin n) => z ↑i) p s ∈ composableWords R X Y

Every block of a word along a composable string is a composable word between some objects.

theorem TauCeti.GradedLinearQuiver.replaceBlock_mem_range_homInclusion {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n p d : ℕ} {a b : ℕ → C} {y : ℕ → TotalHom R C} (hy : ∀ i < n, y i ∈ (homInclusion (a i) (b i)).range) {e : TotalHom R C} (he : e ∈ (homInclusion (a (p + d - 1)) (b p)).range) (hpd : p + d ≤ n) (i : ℕ) : i < p + 1 + (n - p - d) → replaceBlock y p d e i ∈ (homInclusion (replaceBlock a p d (a (p + d - 1)) i) (replaceBlock b p d (b p) i)).range

Replacing a block of a string of morphisms aᵢ ⟶ bᵢ by a morphism from the source of the last morphism of the block to the target of its first gives a string of morphisms between the replaced objects.

theorem TauCeti.GradedLinearQuiver.prepend_mem_composableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {X Y Z : C} {u : TotalHom R C} (hu : u ∈ (homInclusion Y Z).range) {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ composableWords R X Y) : ((ReducedTensorWords.prepend R (TotalHom R C)) u) w ∈ composableWords R X Z

Prepending a morphism Y ⟶ Z to a composable word from X to Y gives a composable word from X to Z.

theorem TauCeti.GradedLinearQuiver.prepend_mem_nonComposableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {Y Z : C} {u : TotalHom R C} (hu : u ∈ (homInclusion Y Z).range) {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ nonComposableWords R C) : ((ReducedTensorWords.prepend R (TotalHom R C)) u) w ∈ nonComposableWords R C

Prepending a morphism to a non-composable word gives a non-composable word.

theorem TauCeti.GradedLinearQuiver.prepend_mem_nonComposableWords_of_ne {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {X Y Y' Z : C} {u : TotalHom R C} (hu : u ∈ (homInclusion Y Z).range) {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ composableWords R X Y') (hne : Y' ≠ Y) : ((ReducedTensorWords.prepend R (TotalHom R C)) u) w ∈ nonComposableWords R C

Prepending a morphism Y ⟶ Z to a composable word from X to Y', where Y' ≠ Y, gives a non-composable word.

theorem TauCeti.GradedLinearQuiver.map_mem_composableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {φ : C → D} {Θ : TotalHom R C →ₗ[R] TotalHom R D} (hΘ : ∀ (X Y : C) (f : ↑(homModule X Y)), Θ ((homInclusion X Y) f) ∈ (homInclusion (φ X) (φ Y)).range) {X Y : C} {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ composableWords R X Y) : (ReducedTensorWords.map R Θ) w ∈ composableWords R (φ X) (φ Y)

A linear map of total modules sending morphisms X ⟶ Y to morphisms φ X ⟶ φ Y, applied to every letter, sends composable words from X to Y to composable words from φ X to φ Y.

theorem TauCeti.GradedLinearQuiver.map_mem_nonComposableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {φ : C → D} {Θ : TotalHom R C →ₗ[R] TotalHom R D} (hΘ : ∀ (X Y : C) (f : ↑(homModule X Y)), Θ ((homInclusion X Y) f) ∈ (homInclusion (φ X) (φ Y)).range) (hφ : Function.Injective φ) {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ nonComposableWords R C) : (ReducedTensorWords.map R Θ) w ∈ nonComposableWords R D

A linear map of total modules sending morphisms X ⟶ Y to morphisms φ X ⟶ φ Y, along an injective map of objects φ and applied to every letter, sends non-composable words to non-composable words.

Word-level path compatibility

structure TauCeti.GradedLinearQuiver.IsWordPathCompatible {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] (φ : C → D) (t : ReducedTensorWords R (TotalHom R C) →ₗ[R] TotalHom R D) : Prop

A linear map t from the bar construction of C to the total module of morphisms of D is path-compatible on words along a map of objects φ : C → D when it sends composable words from X to Y to morphisms φ X ⟶ φ Y and non-composable words to zero. The Taylor maps of A∞ categories (along the identity) and of A∞ functors (along their object maps) are of this kind; see TauCeti.GradedLinearQuiver.isWordPathCompatible_iff for the comparison with path compatibility of their components.

• mem_range_of_mem_composableWords {X Y : C} {w : ReducedTensorWords R (TotalHom R C)} : w ∈ composableWords R X Y → t w ∈ (homInclusion (φ X) (φ Y)).range

  A composable word from X to Y is sent to a morphism φ X ⟶ φ Y.

• eq_zero_of_mem_nonComposableWords {w : ReducedTensorWords R (TotalHom R C)} : w ∈ nonComposableWords R C → t w = 0

  A non-composable word is sent to zero.

theorem TauCeti.GradedLinearQuiver.isWordPathCompatible_iff {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {φ : C → D} {t : ReducedTensorWords R (TotalHom R C) →ₗ[R] TotalHom R D} : IsWordPathCompatible φ t ↔ ∀ (n : ℕ) (hn : 0 < n), IsPathCompatible φ ((t ∘ₗ ReducedTensorWords.of R (TotalHom R C) ⟨n, hn⟩).compMultilinearMap (PiTensorProduct.tprod R))

Word-level path compatibility is path compatibility on words of each length. A linear map from the bar construction is path-compatible on words exactly when its restriction to words of every positive length n, as a multilinear map of n morphisms, is path-compatible.

theorem TauCeti.GradedLinearQuiver.IsWordPathCompatible.comp_map {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {E : Type u''} [GradedLinearQuiver R E] {φ : C → D} {ψ : D → E} {t : ReducedTensorWords R (TotalHom R D) →ₗ[R] TotalHom R E} (ht : IsWordPathCompatible ψ t) {Θ : TotalHom R C →ₗ[R] TotalHom R D} (hΘ : ∀ (X Y : C) (f : ↑(homModule X Y)), Θ ((homInclusion X Y) f) ∈ (homInclusion (φ X) (φ Y)).range) (hφ : Function.Injective φ) : IsWordPathCompatible (ψ ∘ φ) (t ∘ₗ ReducedTensorWords.map R Θ)

Precomposing a path-compatible map with a letterwise map of total modules along an injective map of objects gives a path-compatible map.

theorem TauCeti.GradedLinearQuiver.IsWordPathCompatible.eq_of_totalHomMap_eq {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {B : Type u''} {G : B → D} {κ : C → InducedQuiver D G} {t₁ t₂ : ReducedTensorWords R (TotalHom R C) →ₗ[R] TotalHom R (InducedQuiver D G)} (h₁ : IsWordPathCompatible κ t₁) (h₂ : IsWordPathCompatible κ t₂) (h : ∀ (X Y : C), ∀ w ∈ composableWords R X Y, (InducedQuiver.totalHomMap R G) (t₁ w) = (InducedQuiver.totalHomMap R G) (t₂ w)) : t₁ = t₂

Path-compatible maps into an induced quiver are determined by their images. Two maps from words to the morphisms of the quiver induced along G, path-compatible along the same map of objects, are equal as soon as their images under the map of total modules agree on composable words: on a composable word both values lie in a single hom module, on which the map of total modules is injective.

theorem TauCeti.GradedLinearQuiver.isWordPathCompatible_letter {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] : IsWordPathCompatible id (ReducedTensorWords.letter R (TotalHom R C))

The letter of a word is path-compatible on words: a single morphism X ⟶ Y is a composable word from X to Y, and every non-composable word has length at least two.

The coalgebra morphism of path-compatible Taylor components

theorem TauCeti.GradedLinearQuiver.IsWordPathCompatible.coalgHom_mem_composableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {φ : C → D} {t : ReducedTensorWords R (TotalHom R C) →ₗ[R] TotalHom R D} (ht : IsWordPathCompatible φ t) {X Y : C} {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ composableWords R X Y) : (ReducedTensorWords.coalgHom R t) w ∈ composableWords R (φ X) (φ Y)

The coalgebra morphism with path-compatible Taylor components preserves composable words. It sends composable words from X to Y to composable words from φ X to φ Y.

theorem TauCeti.GradedLinearQuiver.IsWordPathCompatible.coalgHom_mem_nonComposableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {φ : C → D} {t : ReducedTensorWords R (TotalHom R C) →ₗ[R] TotalHom R D} (ht : IsWordPathCompatible φ t) (hφ : Function.Injective φ) {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ nonComposableWords R C) : (ReducedTensorWords.coalgHom R t) w ∈ nonComposableWords R D

The coalgebra morphism with path-compatible Taylor components preserves non-composable words, along an injective map of objects.

theorem TauCeti.GradedLinearQuiver.IsWordPathCompatible.comp_coalgHom {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {φ : C → D} {t : ReducedTensorWords R (TotalHom R C) →ₗ[R] TotalHom R D} {E : Type u''} [GradedLinearQuiver R E] {ψ : D → E} {s : ReducedTensorWords R (TotalHom R D) →ₗ[R] TotalHom R E} (hs : IsWordPathCompatible ψ s) (ht : IsWordPathCompatible φ t) (hφ : Function.Injective φ) : IsWordPathCompatible (ψ ∘ φ) (s ∘ₗ ReducedTensorWords.coalgHom R t)

Composing a path-compatible map with the coalgebra morphism of path-compatible Taylor components along an injective map of objects gives a path-compatible map.

theorem TauCeti.GradedLinearQuiver.map_coalgHom_of_mem_composableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {M₁ : Type u_1} {N : Type u_2} {N₁ : Type u_3} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid N] [Module R N] [AddCommMonoid N₁] [Module R N₁] {Θ : TotalHom R C →ₗ[R] M₁} {Θ' : N →ₗ[R] N₁} {t : ReducedTensorWords R (TotalHom R C) →ₗ[R] N} {t₁ : ReducedTensorWords R M₁ →ₗ[R] N₁} (h : ∀ (X Y : C), ∀ w ∈ composableWords R X Y, Θ' (t w) = t₁ ((ReducedTensorWords.map R Θ) w)) {X Y : C} {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ composableWords R X Y) : (ReducedTensorWords.map R Θ') ((ReducedTensorWords.coalgHom R t) w) = (ReducedTensorWords.coalgHom R t₁) ((ReducedTensorWords.map R Θ) w)

Relations on composable words extend to coalgebra morphisms. If the Taylor maps t and t₁ are related through letterwise maps Θ and Θ' on composable words, then so are the coalgebra morphisms they generate.

Graded Taylor expansions of path-compatible maps

theorem TauCeti.GradedLinearQuiver.koszulTwist_shift_mem_range {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] (c q : ℤ) {X Y : C} {u : TotalHom R C} (hu : u ∈ (homInclusion X Y).range) : (((totalGrading R C).shift c).koszulTwist q) u ∈ (homInclusion X Y).range

The Koszul twist of a shift of the total grading preserves each hom module.

theorem TauCeti.GradedLinearQuiver.IsWordPathCompatible.gradedCoderiv_mem_composableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {t : ReducedTensorWords R (TotalHom R C) →ₗ[R] TotalHom R C} (ht : IsWordPathCompatible id t) (c q : ℤ) {X Y : C} {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ composableWords R X Y) : (ReducedTensorWords.gradedCoderiv ((totalGrading R C).shift c) t q) w ∈ composableWords R X Y

The graded Taylor expansion of a path-compatible map preserves composable words: for a shift of the total grading, it sends composable words from X to Y to composable words from X to Y.

theorem TauCeti.GradedLinearQuiver.IsWordPathCompatible.gradedCoderiv_mem_nonComposableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {t : ReducedTensorWords R (TotalHom R C) →ₗ[R] TotalHom R C} (ht : IsWordPathCompatible id t) (c q : ℤ) {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ nonComposableWords R C) : (ReducedTensorWords.gradedCoderiv ((totalGrading R C).shift c) t q) w ∈ nonComposableWords R C

The graded Taylor expansion of a path-compatible map preserves non-composable words, for a shift of the total grading.

theorem TauCeti.GradedLinearQuiver.IsWordPathCompatible.comp_gradedCoderiv {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {t : ReducedTensorWords R (TotalHom R C) →ₗ[R] TotalHom R C} {D : Type u'} [GradedLinearQuiver R D] {φ : C → D} {s : ReducedTensorWords R (TotalHom R C) →ₗ[R] TotalHom R D} (hs : IsWordPathCompatible φ s) (ht : IsWordPathCompatible id t) (c q : ℤ) : IsWordPathCompatible φ (s ∘ₗ ReducedTensorWords.gradedCoderiv ((totalGrading R C).shift c) t q)

Composing a path-compatible map with the graded Taylor expansion of a path-compatible map gives a path-compatible map.

theorem TauCeti.GradedLinearQuiver.map_gradedCoderiv_of_mem_composableWords {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {t : ReducedTensorWords R (TotalHom R C) →ₗ[R] TotalHom R C} {M₁ : Type u_1} [AddCommMonoid M₁] [Module R M₁] {G : InternalGrading R (TotalHom R C) ℤ} {G₁ : InternalGrading R M₁ ℤ} {Θ : TotalHom R C →ₗ[R] M₁} (hΘ : LinearMap.IsHomogeneous Θ (G.piece ℤ) (G₁.piece ℤ) 0) {t₁ : ReducedTensorWords R M₁ →ₗ[R] M₁} (h : ∀ (X Y : C), ∀ w ∈ composableWords R X Y, Θ (t w) = t₁ ((ReducedTensorWords.map R Θ) w)) (q : ℤ) {X Y : C} {w : ReducedTensorWords R (TotalHom R C)} (hw : w ∈ composableWords R X Y) : (ReducedTensorWords.map R Θ) ((ReducedTensorWords.gradedCoderiv G t q) w) = (ReducedTensorWords.gradedCoderiv G₁ t₁ q) ((ReducedTensorWords.map R Θ) w)

Relations on composable words extend to graded Taylor expansions. If a degree-preserving letterwise map Θ relates the Taylor maps t and t₁ on composable words, it relates their graded Taylor expansions on composable words.