The brace and the Gerstenhaber bracket of suspended Hochschild cochains

Let M carry an internal ℤ-grading G and let T = Tᶜ(M) be its reduced tensor coalgebra. A linear map F : T ⟶ M of degree p (a suspended Hochschild cochain, when M is a suspension sA) has a graded Taylor expansion D F = ReducedTensorWords.gradedCoderiv G F p, the coderivation of twist parameter p with letter component F. Following Getzler and Jones, the brace of F with g of degree q is

F{g} = F ∘ D g,

which inserts g into every block of consecutive letters with the Koszul sign of moving it past the letters before the block, and the Gerstenhaber bracket is its graded commutator

[F, g] = F{g} - (-1)^(p * q) • g{F}.

The whole structure comes from one fact about coderivations: the graded commutator b₁ ∘ b₂ - (-1)^(p * q) • b₂ ∘ b₁ of graded coderivations, homogeneous of the degrees p and q of their twist parameters, is a graded coderivation of twist parameter p + q (IsGradedCoderivation.comp_sub_smul_comp). Since a graded coderivation is determined by its letter component, D [F, g] is the graded commutator of D F and D g (gradedCoderiv_gerstenhaberBracket), and the identities of a graded Lie algebra follow from those of graded commutators of endomorphisms: the brace is a graded right pre-Lie product, and the bracket is graded antisymmetric and satisfies the graded Jacobi identity.

For a Taylor map F of odd degree, F{F} is the letter component of the square D F ∘ D F, which is an ordinary coderivation; so D F squares to zero exactly when F{F} = 0. In degree one this identifies square-zero bar differentials, that is A∞ structures, with solutions of the brace equation m{m} = 0. More generally, for a family φ of Taylor maps of odd degree the composites D φᵢ ∘ D φⱼ are not coderivations, but their sums over the antidiagonals i + j = k are: the terms for (i, j) and (j, i) combine to a graded commutator and the diagonal terms are squares. This is the expansion of the brace equation for a formal power series of Taylor maps.

Main definitions

• TauCeti.ReducedTensorWords.brace: the brace F{g} of two Taylor maps.
• TauCeti.ReducedTensorWords.gerstenhaberBracket: their Gerstenhaber bracket [F, g].

Main results

• TauCeti.ReducedTensorWords.gradedCoderiv_gerstenhaberBracket: the coderivation of a Gerstenhaber bracket is the graded commutator of the coderivations.
• TauCeti.ReducedTensorWords.gradedCoderiv_brace_self: for odd degree, the coderivation of F{F} is the square of the coderivation of F.
• TauCeti.ReducedTensorWords.gradedCoderiv_comp_self_eq_zero_iff: for odd degree, the coderivation squares to zero exactly when the brace equation F{F} = 0 holds.
• TauCeti.ReducedTensorWords.gradedCoderiv_sum_antidiagonal_brace: for a family of Taylor maps of odd degree, the coderivation of ∑_{i + j = k} φᵢ{φⱼ} is ∑_{i + j = k} D φᵢ ∘ D φⱼ.
• TauCeti.ReducedTensorWords.brace_brace_sub_smul_brace_brace: the graded right pre-Lie identity F{g}{h} - (-1)^(q * r) • F{h}{g} = F{[g, h]}.
• TauCeti.ReducedTensorWords.gerstenhaberBracket_swap: graded antisymmetry of the bracket.
• TauCeti.ReducedTensorWords.leibniz_gerstenhaberBracket: the graded Jacobi identity, in Leibniz form.

References

• E. Getzler and J. D. S. Jones, A-infinity algebras and the cyclic bar complex, Illinois Journal of Mathematics 34 (1990), 256--283, Sections 1--2.
• M. Gerstenhaber, The cohomology structure of an associative ring, Annals of Mathematics 78 (1963), 267--288.

The brace and the Gerstenhaber bracket

noncomputable def TauCeti.ReducedTensorWords.brace {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M ℤ) (F g : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) : ReducedTensorWords R M →ₗ[R] M

The brace F{g} of two Taylor maps, Gerstenhaber's composition product of suspended Hochschild cochains: F after the graded Taylor expansion of g at twist parameter q. On a word of homogeneous letters it inserts g into every block of consecutive letters, with the Koszul sign of moving g past the letters before the block, and applies F to the result.

theorem TauCeti.ReducedTensorWords.brace_def {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (F g : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) : brace G F g q = F ∘ₗ gradedCoderiv G g q

theorem TauCeti.ReducedTensorWords.brace_zero_apply {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (F g : ReducedTensorWords R M →ₗ[R] M) (z : ReducedTensorWords R M) : (brace G F g 0) z = F ((coderiv R g) z)

At twist parameter zero, the brace F{g} applies F after the ungraded Taylor expansion of g.

theorem TauCeti.ReducedTensorWords.isHomogeneous_brace {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} {F g : ReducedTensorWords R M →ₗ[R] M} {p q : ℤ} (hF : LinearMap.IsHomogeneous F (gradedPiece G) (G.piece ℤ) p) (hg : LinearMap.IsHomogeneous g (gradedPiece G) (G.piece ℤ) q) : LinearMap.IsHomogeneous (brace G F g q) (gradedPiece G) (G.piece ℤ) (p + q)

The brace of a Taylor map of degree p with one of degree q has degree p + q.

theorem TauCeti.ReducedTensorWords.letter_comp_gradedCoderiv_comp_gradedCoderiv {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (F g : ReducedTensorWords R M →ₗ[R] M) (p q : ℤ) : letter R M ∘ₗ gradedCoderiv G F p ∘ₗ gradedCoderiv G g q = brace G F g q

The brace is the letter component of the composite of the two graded coderivations.

@[simp]

theorem TauCeti.ReducedTensorWords.brace_add_left {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (F₁ F₂ g : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) : brace G (F₁ + F₂) g q = brace G F₁ g q + brace G F₂ g q

The brace is additive in its first argument.

@[simp]

theorem TauCeti.ReducedTensorWords.brace_smul_left {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (c : R) (F g : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) : brace G (c • F) g q = c • brace G F g q

The brace is R-linear in its first argument.

@[simp]

theorem TauCeti.ReducedTensorWords.brace_zero_left {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (g : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) : brace G 0 g q = 0

The brace of the zero map with any Taylor map vanishes.

@[simp]

theorem TauCeti.ReducedTensorWords.brace_add_right {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (F g₁ g₂ : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) : brace G F (g₁ + g₂) q = brace G F g₁ q + brace G F g₂ q

The brace is additive in its second argument, since the graded Taylor expansion is.

@[simp]

theorem TauCeti.ReducedTensorWords.brace_smul_right {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (c : R) (F g : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) : brace G F (c • g) q = c • brace G F g q

The brace is R-linear in its second argument, since the graded Taylor expansion is.

@[simp]

theorem TauCeti.ReducedTensorWords.brace_zero_right {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (F : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) : brace G F 0 q = 0

The brace of a Taylor map with the zero map vanishes.

noncomputable def TauCeti.ReducedTensorWords.gerstenhaberBracket {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M ℤ) (p q : ℤ) (F g : ReducedTensorWords R M →ₗ[R] M) : ReducedTensorWords R M →ₗ[R] M

The Gerstenhaber bracket [F, g] = F{g} - (-1)^(p * q) g{F} of a Taylor map F of degree p with a Taylor map g of degree q, the graded commutator of the brace.

theorem TauCeti.ReducedTensorWords.gerstenhaberBracket_def {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (p q : ℤ) (F g : ReducedTensorWords R M →ₗ[R] M) : gerstenhaberBracket G p q F g = brace G F g q - negOnePowCast R (p * q) • brace G g F p

@[simp]

theorem TauCeti.ReducedTensorWords.gerstenhaberBracket_add_left {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (p q : ℤ) (F₁ F₂ g : ReducedTensorWords R M →ₗ[R] M) : gerstenhaberBracket G p q (F₁ + F₂) g = gerstenhaberBracket G p q F₁ g + gerstenhaberBracket G p q F₂ g

The Gerstenhaber bracket is additive in its first argument.

@[simp]

theorem TauCeti.ReducedTensorWords.gerstenhaberBracket_add_right {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (p q : ℤ) (F g₁ g₂ : ReducedTensorWords R M →ₗ[R] M) : gerstenhaberBracket G p q F (g₁ + g₂) = gerstenhaberBracket G p q F g₁ + gerstenhaberBracket G p q F g₂

The Gerstenhaber bracket is additive in its second argument.

@[simp]

theorem TauCeti.ReducedTensorWords.gerstenhaberBracket_smul_left {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (p q : ℤ) (c : R) (F g : ReducedTensorWords R M →ₗ[R] M) : gerstenhaberBracket G p q (c • F) g = c • gerstenhaberBracket G p q F g

The Gerstenhaber bracket is R-linear in its first argument.

@[simp]

theorem TauCeti.ReducedTensorWords.gerstenhaberBracket_smul_right {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (p q : ℤ) (c : R) (F g : ReducedTensorWords R M →ₗ[R] M) : gerstenhaberBracket G p q F (c • g) = c • gerstenhaberBracket G p q F g

The Gerstenhaber bracket is R-linear in its second argument.

@[simp]

theorem TauCeti.ReducedTensorWords.gerstenhaberBracket_zero_left {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (p q : ℤ) (g : ReducedTensorWords R M →ₗ[R] M) : gerstenhaberBracket G p q 0 g = 0

The Gerstenhaber bracket of the zero map with any Taylor map vanishes.

@[simp]

theorem TauCeti.ReducedTensorWords.gerstenhaberBracket_zero_right {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (p q : ℤ) (F : ReducedTensorWords R M →ₗ[R] M) : gerstenhaberBracket G p q F 0 = 0

The Gerstenhaber bracket of a Taylor map with the zero map vanishes.

theorem TauCeti.ReducedTensorWords.isHomogeneous_gerstenhaberBracket {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} {F g : ReducedTensorWords R M →ₗ[R] M} {p q : ℤ} (hF : LinearMap.IsHomogeneous F (gradedPiece G) (G.piece ℤ) p) (hg : LinearMap.IsHomogeneous g (gradedPiece G) (G.piece ℤ) q) : LinearMap.IsHomogeneous (gerstenhaberBracket G p q F g) (gradedPiece G) (G.piece ℤ) (p + q)

The Gerstenhaber bracket of Taylor maps of degrees p and q has degree p + q.

theorem TauCeti.ReducedTensorWords.gradedCoderiv_gerstenhaberBracket {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} {F g : ReducedTensorWords R M →ₗ[R] M} {p q : ℤ} (hF : LinearMap.IsHomogeneous F (gradedPiece G) (G.piece ℤ) p) (hg : LinearMap.IsHomogeneous g (gradedPiece G) (G.piece ℤ) q) : gradedCoderiv G (gerstenhaberBracket G p q F g) (p + q) = gradedCoderiv G F p ∘ₗ gradedCoderiv G g q - negOnePowCast R (p * q) • gradedCoderiv G g q ∘ₗ gradedCoderiv G F p

The graded coderivation of a Gerstenhaber bracket is the graded commutator of the graded coderivations. For Taylor maps F of degree p and g of degree q, D [F, g] = D F ∘ D g - (-1)^(p * q) • D g ∘ D F, where D is the graded Taylor expansion at twist parameter equal to the degree.

theorem TauCeti.ReducedTensorWords.gradedCoderiv_brace_self {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} {F : ReducedTensorWords R M →ₗ[R] M} {q : ℤ} (hF : LinearMap.IsHomogeneous F (gradedPiece G) (G.piece ℤ) q) (hq : Odd q) : gradedCoderiv G (brace G F F q) (q + q) = gradedCoderiv G F q ∘ₗ gradedCoderiv G F q

For a Taylor map F of odd degree q, the graded Taylor expansion of the brace F{F} is the square of the graded Taylor expansion of F.

theorem TauCeti.ReducedTensorWords.gradedCoderiv_comp_self_eq_zero_iff {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} {F : ReducedTensorWords R M →ₗ[R] M} {q : ℤ} (hF : LinearMap.IsHomogeneous F (gradedPiece G) (G.piece ℤ) q) (hq : Odd q) : gradedCoderiv G F q ∘ₗ gradedCoderiv G F q = 0 ↔ brace G F F q = 0

The square-zero equation is the brace equation. For a Taylor map F of odd degree q, the graded Taylor expansion of F squares to zero exactly when F{F} = 0.

theorem TauCeti.ReducedTensorWords.gradedCoderiv_sum_antidiagonal_brace {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} {φ : ℕ → ReducedTensorWords R M →ₗ[R] M} {q : ℤ} {k : ℕ} (hφ : ∀ i ≤ k, LinearMap.IsHomogeneous (φ i) (gradedPiece G) (G.piece ℤ) q) (hq : Odd q) : gradedCoderiv G (∑ x ∈ Finset.antidiagonal k, brace G (φ x.1) (φ x.2) q) (q + q) = ∑ x ∈ Finset.antidiagonal k, gradedCoderiv G (φ x.1) q ∘ₗ gradedCoderiv G (φ x.2) q

Brace squares of a family of odd Taylor maps. If φ i has odd degree q for every i ≤ k, the graded Taylor expansion of ∑_{i + j = k} φ i {φ j} is ∑_{i + j = k} D (φ i) ∘ D (φ j). This is the coefficient of tᵏ in the square of the coderivation of a formal power series ∑ tⁱ φ i.

theorem TauCeti.ReducedTensorWords.gerstenhaberBracket_swap {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (p q : ℤ) (F g : ReducedTensorWords R M →ₗ[R] M) : gerstenhaberBracket G q p g F = -negOnePowCast R (p * q) • gerstenhaberBracket G p q F g

The Gerstenhaber bracket is graded antisymmetric: [g, F] = -(-1)^(p * q) • [F, g] for F of degree p and g of degree q.

theorem TauCeti.ReducedTensorWords.brace_brace_sub_smul_brace_brace {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} (F : ReducedTensorWords R M →ₗ[R] M) {g h : ReducedTensorWords R M →ₗ[R] M} {q r : ℤ} (hg : LinearMap.IsHomogeneous g (gradedPiece G) (G.piece ℤ) q) (hh : LinearMap.IsHomogeneous h (gradedPiece G) (G.piece ℤ) r) : brace G (brace G F g q) h r - negOnePowCast R (q * r) • brace G (brace G F h r) g q = brace G F (gerstenhaberBracket G q r g h) (q + r)

The brace is a right graded pre-Lie product. The graded commutator of the two ways of bracing F successively with g of degree q and h of degree r is the brace of F with their Gerstenhaber bracket: F{g}{h} - (-1)^(q * r) • F{h}{g} = F{[g, h]}.

theorem TauCeti.ReducedTensorWords.leibniz_gerstenhaberBracket {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M ℤ} {F g h : ReducedTensorWords R M →ₗ[R] M} {p q r : ℤ} (hF : LinearMap.IsHomogeneous F (gradedPiece G) (G.piece ℤ) p) (hg : LinearMap.IsHomogeneous g (gradedPiece G) (G.piece ℤ) q) (hh : LinearMap.IsHomogeneous h (gradedPiece G) (G.piece ℤ) r) : gerstenhaberBracket G p (q + r) F (gerstenhaberBracket G q r g h) = gerstenhaberBracket G (p + q) r (gerstenhaberBracket G p q F g) h + negOnePowCast R (p * q) • gerstenhaberBracket G q (p + r) g (gerstenhaberBracket G p r F h)

The graded Jacobi identity for the Gerstenhaber bracket, in Leibniz form: bracketing with F of degree p is a graded derivation of the bracket of g of degree q and h of degree r, [F, [g, h]] = [[F, g], h] + (-1)^(p * q) • [g, [F, h]].