Graded coalgebra morphisms of reduced tensor coalgebras

Let M and N carry internal integer gradings G and H, and give their reduced tensor coalgebras Tᶜ(M) and Tᶜ(N) the total letter degree. This file combines the ungraded correspondence between coalgebra morphisms Tᶜ(M) ⟶ Tᶜ(N) and their Taylor components (TauCeti.ReducedTensorWords.coalgHomEquivTaylor) with the grading, and with graded coderivations.

First, the Taylor expansion coalgHom f of a degree-zero family of components f is itself of degree zero: each word f(B₁) ⋯ f(B_k) produced from a cut of a homogeneous word into blocks has the total degree of the word.

Second, for linear maps F F' : Tᶜ(M) ⟶ Tᶜ(N), a coderivation along F and F' with twist parameter q is a linear map D : Tᶜ(M) ⟶ Tᶜ(N) satisfying

Δ ∘ D = (D ⊗ F') ∘ Δ + (F ⊗ D) ∘ (τ ⊗ 1) ∘ Δ,

with τ the letterwise Koszul twist of Tᶜ(M) of parameter q. Such a map is determined by its letter component, by induction along the conilpotence filtration, whatever F and F' are. Coderivations along a pair of maps are stable under composition with coalgebra morphisms on either side. Three instances drive the applications: if F and F' are coalgebra morphisms then F - F' is an untwisted coderivation along F and F'; if F has degree zero and b_M, b_N are graded coderivations then b_N ∘ F and F ∘ b_M are coderivations along F and F; and if D is an odd coderivation along F and F', and both maps intertwine odd coderivations b_M and b_N, then b_N ∘ D + D ∘ b_M is an untwisted coderivation along F and F'.

Hence a degree-zero coalgebra morphism F intertwines two q-twisted graded coderivations b_M of Tᶜ(M) and b_N of Tᶜ(N) as soon as it does so after projection onto single letters: b_N ∘ F = F ∘ b_M if and only if π ∘ b_N ∘ F = π ∘ F ∘ b_M, where π : Tᶜ(N) ⟶ N is the letter projection. Applied to bar constructions, this is the statement that an A∞ morphism is determined by, and may be constructed from, Taylor components satisfying the suspended component equation. In the same way, the homotopy equation F - F' = b_N ∘ D + D ∘ b_M for an odd coderivation D along coalgebra morphisms holds as soon as it holds on letter components; this is the component equation of a homotopy between A∞ morphisms.

Main definitions

• TauCeti.ReducedTensorWords.IsGradedCoderivationAlong: the co-Leibniz rule of a coderivation along a pair of maps.

Main results

• TauCeti.ReducedTensorWords.isHomogeneous_coalgHom: the Taylor expansion of degree-zero components has degree zero.
• TauCeti.ReducedTensorWords.IsGradedCoderivationAlong.eq_of_letter_comp_eq: a coderivation along a pair of maps is determined by its letter component.
• TauCeti.ReducedTensorWords.IsCoalgHom.isGradedCoderivationAlong_sub: the difference of two coalgebra morphisms is a coderivation along them.
• TauCeti.ReducedTensorWords.IsGradedCoderivationAlong.comp_add_comp: the commutator of an odd coderivation along a pair of maps with odd coderivations intertwined by them.
• TauCeti.ReducedTensorWords.IsCoalgHom.comp_eq_comp_iff_letter_comp_eq: a degree-zero coalgebra morphism intertwines two graded coderivations exactly when it does so on letter components.
• TauCeti.ReducedTensorWords.IsGradedCoderivationAlong.sub_eq_comp_add_comp_iff: the homotopy equation holds exactly when it holds on letter components.
• TauCeti.ReducedTensorWords.IsCoalgHom.isHomogeneous_linearEquiv_symm: the inverse of a degree-zero coalgebra automorphism is homogeneous of degree zero.

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.4 and 3.6.

theorem TauCeti.ReducedTensorWords.isHomogeneous_coalgHom {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {H : InternalGrading R N} {f : ReducedTensorWords R M →ₗ[R] N} (hf : LinearMap.IsHomogeneous f (gradedPiece G) H.piece 0) : LinearMap.IsHomogeneous (coalgHom R f) (gradedPiece G) (gradedPiece H) 0

The Taylor expansion of components of degree zero has degree zero: every word f(B₁) ⋯ f(B_k) it produces from a homogeneous word has the total degree of that word.

Coderivations along coalgebra morphisms

def TauCeti.ReducedTensorWords.IsGradedCoderivationAlong {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (q : ℤ) (F F' D : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N) : Prop

A graded coderivation along F and F' with twist parameter q, also called an (F, F')-coderivation: a linear map D : Tᶜ(M) ⟶ Tᶜ(N) satisfying the co-Leibniz rule

Δ ∘ D = (D ⊗ F') ∘ Δ + (F ⊗ D) ∘ (τ ⊗ 1) ∘ Δ,

in which τ = ReducedTensorWords.map (InternalGrading.koszulTwist G q) is the letterwise Koszul twist of the source and acts on the left half of every cut. On a word z of homogeneous letters, summing over the cuts w₁ ⊗ w₂ of z,

Δ (D z) = ∑ (D w₁ ⊗ F' w₂ + (-1)^(q * |w₁|) • (F w₁ ⊗ D w₂)).

For F = F' = id this is IsGradedCoderivation G q. Homogeneity of D is not part of the condition.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.ReducedTensorWords.isGradedCoderivationAlong_iff {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {q : ℤ} {F F' D : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} : IsGradedCoderivationAlong G q F F' D ↔ deconcatenation R N ∘ₗ D = TensorProduct.map D F' ∘ₗ deconcatenation R M + TensorProduct.map F D ∘ₗ LinearMap.rTensor (ReducedTensorWords R M) (map R (G.koszulTwist q)) ∘ₗ deconcatenation R M

The co-Leibniz identity of a coderivation along a pair of maps, as a reusable Iff: this exposes the body of the predicate to consumers in other modules.

theorem TauCeti.ReducedTensorWords.IsGradedCoderivationAlong.deconcatenation_apply {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {q : ℤ} {F F' D : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hD : IsGradedCoderivationAlong G q F F' D) (z : ReducedTensorWords R M) : (deconcatenation R N) (D z) = (TensorProduct.map D F') ((deconcatenation R M) z) + (TensorProduct.map F D) ((LinearMap.rTensor (ReducedTensorWords R M) (map R (G.koszulTwist q))) ((deconcatenation R M) z))

The co-Leibniz identity of a coderivation along a pair of maps, applied to an element.

theorem TauCeti.ReducedTensorWords.isGradedCoderivationAlong_id_id_iff {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {G : InternalGrading R M} {q : ℤ} {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} : IsGradedCoderivationAlong G q LinearMap.id LinearMap.id b ↔ IsGradedCoderivation G q b

The coderivations along the identity on both sides are the graded coderivations.

theorem TauCeti.ReducedTensorWords.IsGradedCoderivationAlong.eq_of_letter_comp_eq {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {q : ℤ} {F F' D₁ D₂ : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (h₁ : IsGradedCoderivationAlong G q F F' D₁) (h₂ : IsGradedCoderivationAlong G q F F' D₂) (hl : letter R N ∘ₗ D₁ = letter R N ∘ₗ D₂) : D₁ = D₂

A coderivation along a pair of maps is determined by its letter component: two coderivations along the same pair of maps whose letter components agree are equal. This is an induction along the conilpotence filtration of the source, and it holds for arbitrary F and F'.

theorem TauCeti.ReducedTensorWords.isGradedCoderivationAlong_zero {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (q : ℤ) (F F' : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N) : IsGradedCoderivationAlong G q F F' 0

The zero map is a coderivation along every pair of maps.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.comp_isGradedCoderivationAlong {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {P : Type uP} [AddCommMonoid P] [Module R P] {K : ReducedTensorWords R N →ₗ[R] ReducedTensorWords R P} (hK : IsCoalgHom R K) {q : ℤ} {F F' D : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hD : IsGradedCoderivationAlong G q F F' D) : IsGradedCoderivationAlong G q (K ∘ₗ F) (K ∘ₗ F') (K ∘ₗ D)

Following a coderivation along F and F' by a coalgebra morphism K gives a coderivation along K ∘ F and K ∘ F'.

theorem TauCeti.ReducedTensorWords.IsGradedCoderivationAlong.comp_isCoalgHom {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {L : Type uL} [AddCommMonoid L] [Module R L] {E : InternalGrading R L} {q : ℤ} {F F' D : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hD : IsGradedCoderivationAlong G q F F' D) {K : ReducedTensorWords R L →ₗ[R] ReducedTensorWords R M} (hK : IsCoalgHom R K) (hK₀ : LinearMap.IsHomogeneous K (gradedPiece E) (gradedPiece G) 0) : IsGradedCoderivationAlong E q (F ∘ₗ K) (F' ∘ₗ K) (D ∘ₗ K)

Precomposing a coderivation along F and F' with a degree-zero coalgebra morphism K gives a coderivation along F ∘ K and F' ∘ K: the morphism commutes with the letterwise Koszul twists.

theorem TauCeti.ReducedTensorWords.IsGradedCoderivation.comp_isCoalgHom {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {H : InternalGrading R N} {q : ℤ} {b : ReducedTensorWords R N →ₗ[R] ReducedTensorWords R N} (hb : IsGradedCoderivation H q b) {F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hF : IsCoalgHom R F) (hF₀ : LinearMap.IsHomogeneous F (gradedPiece G) (gradedPiece H) 0) : IsGradedCoderivationAlong G q F F (b ∘ₗ F)

A coalgebra morphism F followed by a graded coderivation of the target is a coderivation along F and F, provided F has degree zero.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.comp_isGradedCoderivation {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {q : ℤ} {F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hF : IsCoalgHom R F) {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hb : IsGradedCoderivation G q b) : IsGradedCoderivationAlong G q F F (F ∘ₗ b)

A graded coderivation of the source followed by a coalgebra morphism F is a coderivation along F and F.

Intertwining graded coderivations

theorem TauCeti.ReducedTensorWords.IsCoalgHom.comp_eq_comp_of_letter_comp_eq {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {H : InternalGrading R N} {F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hF : IsCoalgHom R F) (hF₀ : LinearMap.IsHomogeneous F (gradedPiece G) (gradedPiece H) 0) {q : ℤ} {bM : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} {bN : ReducedTensorWords R N →ₗ[R] ReducedTensorWords R N} (hbM : IsGradedCoderivation G q bM) (hbN : IsGradedCoderivation H q bN) (hl : letter R N ∘ₗ bN ∘ₗ F = letter R N ∘ₗ F ∘ₗ bM) : bN ∘ₗ F = F ∘ₗ bM

A degree-zero coalgebra morphism intertwines a q-twisted graded coderivation of Tᶜ(M) with one of Tᶜ(N) as soon as it does so after projection onto single letters: both composites are coderivations along F and F.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.comp_eq_comp_iff_letter_comp_eq {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {H : InternalGrading R N} {F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hF : IsCoalgHom R F) (hF₀ : LinearMap.IsHomogeneous F (gradedPiece G) (gradedPiece H) 0) {q : ℤ} {bM : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} {bN : ReducedTensorWords R N →ₗ[R] ReducedTensorWords R N} (hbM : IsGradedCoderivation G q bM) (hbN : IsGradedCoderivation H q bN) : bN ∘ₗ F = F ∘ₗ bM ↔ letter R N ∘ₗ bN ∘ₗ F = letter R N ∘ₗ F ∘ₗ bM

A degree-zero coalgebra morphism intertwines a q-twisted graded coderivation of Tᶜ(M) with one of Tᶜ(N) if and only if it does so after projection onto single letters.

Differences of coalgebra morphisms and odd coderivations

theorem TauCeti.ReducedTensorWords.IsCoalgHom.isGradedCoderivationAlong_sub {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {G : InternalGrading R M} {F F' : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hF : IsCoalgHom R F) (hF' : IsCoalgHom R F') : IsGradedCoderivationAlong G 0 F F' (F - F')

The difference of two coalgebra morphisms F and F' is an untwisted coderivation along F and F': Δ (F - F') = ((F - F') ⊗ F' + F ⊗ (F - F')) Δ.

theorem TauCeti.ReducedTensorWords.IsGradedCoderivationAlong.comp_add_comp {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {G : InternalGrading R M} {H : InternalGrading R N} {q r s : ℤ} {F F' D : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} {bM : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} {bN : ReducedTensorWords R N →ₗ[R] ReducedTensorWords R N} (hD : IsGradedCoderivationAlong G q F F' D) (hD₁ : LinearMap.IsHomogeneous D (gradedPiece G) (gradedPiece H) r) (hr : (q * r).negOnePow = -1) (hbM : IsGradedCoderivation G q bM) (hbM₁ : LinearMap.IsHomogeneous bM (gradedPiece G) (gradedPiece G) s) (hs : (q * s).negOnePow = -1) (hbN : IsGradedCoderivation H q bN) (hF₀ : LinearMap.IsHomogeneous F (gradedPiece G) (gradedPiece H) 0) (hF : bN ∘ₗ F = F ∘ₗ bM) (hF' : bN ∘ₗ F' = F' ∘ₗ bM) : IsGradedCoderivationAlong G 0 F F' (bN ∘ₗ D + D ∘ₗ bM)

Let D be an odd coderivation along F and F', where F has degree zero and both F and F' intertwine odd graded coderivations b_M of Tᶜ(M) and b_N of Tᶜ(N). Then b_N ∘ D + D ∘ b_M is an untwisted coderivation along F and F'. The cross terms cancel in pairs because D and b_M anticommute with the letterwise Koszul twist.

theorem TauCeti.ReducedTensorWords.IsGradedCoderivationAlong.sub_eq_comp_add_comp_iff {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {G : InternalGrading R M} {H : InternalGrading R N} {q r s : ℤ} {F F' D : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} {bM : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} {bN : ReducedTensorWords R N →ₗ[R] ReducedTensorWords R N} (hD : IsGradedCoderivationAlong G q F F' D) (hD₁ : LinearMap.IsHomogeneous D (gradedPiece G) (gradedPiece H) r) (hr : (q * r).negOnePow = -1) (hbM : IsGradedCoderivation G q bM) (hbM₁ : LinearMap.IsHomogeneous bM (gradedPiece G) (gradedPiece G) s) (hs : (q * s).negOnePow = -1) (hbN : IsGradedCoderivation H q bN) (hFc : IsCoalgHom R F) (hF'c : IsCoalgHom R F') (hF₀ : LinearMap.IsHomogeneous F (gradedPiece G) (gradedPiece H) 0) (hF : bN ∘ₗ F = F ∘ₗ bM) (hF' : bN ∘ₗ F' = F' ∘ₗ bM) : F - F' = bN ∘ₗ D + D ∘ₗ bM ↔ letter R N ∘ₗ (F - F') = letter R N ∘ₗ (bN ∘ₗ D + D ∘ₗ bM)

The homotopy equation is determined by its letter component. Under the hypotheses of IsGradedCoderivationAlong.comp_add_comp, if F' is also a coalgebra morphism, then F - F' = b_N ∘ D + D ∘ b_M holds as soon as it holds after projection onto single letters.

Inverses

theorem TauCeti.ReducedTensorWords.IsCoalgHom.isHomogeneous_linearEquiv_symm {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {H : InternalGrading R N} {e : ReducedTensorWords R M ≃ₗ[R] ReducedTensorWords R N} (he : IsCoalgHom R ↑e) (he₀ : LinearMap.IsHomogeneous (↑e) (gradedPiece G) (gradedPiece H) 0) : LinearMap.IsHomogeneous (↑e.symm) (gradedPiece H) (gradedPiece G) 0

The inverse of a degree-zero linear equivalence of reduced tensor coalgebras which is a coalgebra morphism is again homogeneous of degree zero.