The bounded Hochschild coboundary of a bounded bimodule

Let A be a possibly nonunital normed algebra over a nontrivially normed field 𝕜 and E a normed space. A bounded bimodule structure on E is given by two bounded bilinear maps L R : A →L[𝕜] E →L[𝕜] E, with a · x = L a x and x · a = R a x, satisfying L (a * b) x = L a (L b x), R (a * b) x = R b (R a x) and L a (R b x) = R b (L a x). The actions need not be contractive or unital.

A bounded Hochschild n-cochain of A with coefficients in E is a bounded n-multilinear map T : Aⁿ → E, i.e. an element of ContinuousMultilinearMap 𝕜 (fun _ : Fin n ↦ A) E; the 0-cochains are the constant maps, i.e. the elements of E. This file constructs the bounded Hochschild coboundary δ : Cⁿ(A, E) → Cⁿ⁺¹(A, E),

(δT)(a₀, …, aₙ) = L a₀ (T (a₁, …, aₙ)) + ∑_{j < n} (-1)ʲ⁺¹ T(a₀, …, aⱼaⱼ₊₁, …, aₙ) + (-1)ⁿ⁺¹ R aₙ (T (a₀, …, aₙ₋₁)),

as a bounded linear map, the alternating sum of bounded cofaces ∂ᵢ. The operator norm of δ is at most ‖L‖ + n + ‖R‖. The cofaces satisfy the cosimplicial identities, so δ ∘ δ = 0. In low degrees the coboundary of a constant cochain x is the inner derivation a ↦ L a x - R a x, so the degree-zero cocycles are the central elements of E, and the degree-one cocycles are the bounded derivations D (a * b) = L a (D b) + R b (D a).

The inner cofaces are the bounded versions of TauCeti.hochschildCoface, and the cosimplicial identities come from those of the coface formulas TauCeti.hochschildBimoduleCofaceFun; the algebraic coboundary with coefficients in a bimodule over a unital algebra is TauCeti.hochschildBimoduleCoboundary. The present construction keeps the actions as bounded bilinear maps, so that it applies to nonunital Banach algebras and to bimodules whose actions are not unital.

Main definitions

• ContinuousLinearMap.hochschildBimoduleCoface: the bounded cofaces ∂ᵢ.
• ContinuousLinearMap.hochschildBimoduleCoboundary: the bounded Hochschild coboundary δ = ∑ᵢ (-1)ⁱ ∂ᵢ.

Main results

• ContinuousLinearMap.hochschildBimoduleCoboundary_apply_eq_add_sum_add: the explicit formula for δ.
• ContinuousLinearMap.norm_hochschildBimoduleCoboundary_le: ‖δ‖ ≤ ‖L‖ + n + ‖R‖.
• ContinuousLinearMap.hochschildBimoduleCoface_hochschildBimoduleCoface: the cosimplicial identities ∂_{j+1} ∘ ∂ᵢ = ∂ᵢ ∘ ∂_j for i ≤ j.
• ContinuousLinearMap.hochschildBimoduleCoboundary_hochschildBimoduleCoboundary: δ (δ T) = 0.
• ContinuousLinearMap.hochschildBimoduleCoboundary_constOfIsEmpty_eq_zero_iff: the degree-zero cocycles are the central elements.
• ContinuousLinearMap.hochschildBimoduleCoboundary_ofSubsingleton_eq_zero_iff: the degree-one cocycles are the bounded derivations.

References

• B. E. Johnson, Cohomology in Banach algebras, Mem. Amer. Math. Soc. 127 (1972).
• H. G. Dales, Banach Algebras and Automatic Continuity, §2.8.
• A. Ya. Helemskii, The Homology of Banach and Topological Algebras, Chapter I.

noncomputable def ContinuousLinearMap.hochschildBimoduleCoface {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (L R : A →L[𝕜] E →L[𝕜] E) (i : Fin (n + 2)) : (A [×n]→L[𝕜] E) →L[𝕜] A [×n + 1]→L[𝕜] E

The i-th bounded Hochschild coface, sending a bounded cochain T in n arguments to a bounded cochain in n + 1 arguments: the zeroth coface acts by the first entry through L, the last coface acts by the last entry through R, and the others multiply two adjacent entries.

@[simp]

theorem ContinuousLinearMap.hochschildBimoduleCoface_zero_apply {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (L R : A →L[𝕜] E →L[𝕜] E) (T : A [×n]→L[𝕜] E) (a : Fin (n + 1) → A) : ((L.hochschildBimoduleCoface R 0) T) a = (L (a 0)) (T (Fin.tail a))

The zeroth coface acts by the first entry on the left.

@[simp]

theorem ContinuousLinearMap.hochschildBimoduleCoface_last_apply {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (L R : A →L[𝕜] E →L[𝕜] E) (T : A [×n]→L[𝕜] E) (a : Fin (n + 1) → A) : ((L.hochschildBimoduleCoface R (Fin.last (n + 1))) T) a = (R (a (Fin.last n))) (T (Fin.init a))

The last coface acts by the last entry on the right.

@[simp]

theorem ContinuousLinearMap.hochschildBimoduleCoface_castSucc_succ_apply {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (L R : A →L[𝕜] E →L[𝕜] E) (j : Fin n) (T : A [×n]→L[𝕜] E) (a : Fin (n + 1) → A) : ((L.hochschildBimoduleCoface R j.castSucc.succ) T) a = T (j.castSucc.contractNth (fun (x1 x2 : A) => x1 * x2) a)

The inner cofaces multiply two adjacent entries.

theorem ContinuousLinearMap.hochschildBimoduleCoface_succ_castSucc_apply {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (L R : A →L[𝕜] E →L[𝕜] E) (j : Fin n) (T : A [×n]→L[𝕜] E) (a : Fin (n + 1) → A) : ((L.hochschildBimoduleCoface R j.succ.castSucc) T) a = T (j.castSucc.contractNth (fun (x1 x2 : A) => x1 * x2) a)

The inner cofaces multiply two adjacent entries, with the index written as j.succ.castSucc rather than j.castSucc.succ.

theorem ContinuousLinearMap.hochschildBimoduleCoface_hochschildBimoduleCoface {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (L R : A →L[𝕜] E →L[𝕜] E) (hL : ∀ (a b : A) (x : E), (L (a * b)) x = (L a) ((L b) x)) (hR : ∀ (a b : A) (x : E), (R (a * b)) x = (R b) ((R a) x)) (hLR : ∀ (a b : A) (x : E), (L a) ((R b) x) = (R b) ((L a) x)) {i j : Fin (n + 2)} (hij : i ≤ j) (T : A [×n]→L[𝕜] E) : (L.hochschildBimoduleCoface R j.succ) ((L.hochschildBimoduleCoface R i) T) = (L.hochschildBimoduleCoface R i.castSucc) ((L.hochschildBimoduleCoface R j) T)

The cosimplicial identity ∂_{j+1} ∘ ∂ᵢ = ∂ᵢ ∘ ∂_j for i ≤ j, for a bounded bimodule.

noncomputable def ContinuousLinearMap.hochschildBimoduleCoboundary {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (L R : A →L[𝕜] E →L[𝕜] E) (n : ℕ) : (A [×n]→L[𝕜] E) →L[𝕜] A [×n + 1]→L[𝕜] E

The bounded Hochschild coboundary δ on bounded cochains with coefficients in the bimodule given by the actions L and R, the alternating sum ∑ᵢ (-1)ⁱ ∂ᵢ of the cofaces. Explicitly (ContinuousLinearMap.hochschildBimoduleCoboundary_apply_eq_add_sum_add), `(δT)(a₀, …, aₙ) = L a₀ (T (a₁, …, aₙ)) + ∑_{j < n} (-1)ʲ⁺¹ T(a₀, …, aⱼaⱼ₊₁, …, aₙ)

• (-1)ⁿ⁺¹ R aₙ (T (a₀, …, aₙ₋₁))`.

@[simp]

theorem ContinuousLinearMap.hochschildBimoduleCoboundary_apply {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (L R : A →L[𝕜] E →L[𝕜] E) (T : A [×n]→L[𝕜] E) (a : Fin (n + 1) → A) : ((L.hochschildBimoduleCoboundary R n) T) a = ∑ i : Fin (n + 2), (-1) ^ ↑i • ((L.hochschildBimoduleCoface R i) T) a

The coboundary evaluates as the alternating sum of the cofaces.

theorem ContinuousLinearMap.hochschildBimoduleCoboundary_apply_eq_add_sum_add {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (L R : A →L[𝕜] E →L[𝕜] E) (T : A [×n]→L[𝕜] E) (a : Fin (n + 1) → A) : ((L.hochschildBimoduleCoboundary R n) T) a = (L (a 0)) (T (Fin.tail a)) + ∑ j : Fin n, (-1) ^ (↑j + 1) • T (j.castSucc.contractNth (fun (x1 x2 : A) => x1 * x2) a) + (-1) ^ (n + 1) • (R (a (Fin.last n))) (T (Fin.init a))

The bounded Hochschild coboundary in explicit form.

theorem ContinuousLinearMap.norm_hochschildBimoduleCoboundary_le {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (L R : A →L[𝕜] E →L[𝕜] E) : ‖L.hochschildBimoduleCoboundary R n‖ ≤ ‖L‖ + ↑n + ‖R‖

The operator norm of the bounded Hochschild coboundary on n-cochains is at most ‖L‖ + n + ‖R‖.

@[simp]

theorem ContinuousLinearMap.hochschildBimoduleCoboundary_hochschildBimoduleCoboundary {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (L R : A →L[𝕜] E →L[𝕜] E) (hL : ∀ (a b : A) (x : E), (L (a * b)) x = (L a) ((L b) x)) (hR : ∀ (a b : A) (x : E), (R (a * b)) x = (R b) ((R a) x)) (hLR : ∀ (a b : A) (x : E), (L a) ((R b) x) = (R b) ((L a) x)) (T : A [×n]→L[𝕜] E) : (L.hochschildBimoduleCoboundary R (n + 1)) ((L.hochschildBimoduleCoboundary R n) T) = 0

The bounded Hochschild coboundary squares to zero.

theorem ContinuousLinearMap.hochschildBimoduleCoboundary_comp_hochschildBimoduleCoboundary {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (L R : A →L[𝕜] E →L[𝕜] E) (hL : ∀ (a b : A) (x : E), (L (a * b)) x = (L a) ((L b) x)) (hR : ∀ (a b : A) (x : E), (R (a * b)) x = (R b) ((R a) x)) (hLR : ∀ (a b : A) (x : E), (L a) ((R b) x) = (R b) ((L a) x)) : L.hochschildBimoduleCoboundary R (n + 1) ∘SL L.hochschildBimoduleCoboundary R n = 0

The bounded Hochschild coboundary squares to zero, as a composite of bounded linear maps.

theorem ContinuousLinearMap.hochschildBimoduleCoboundary_constOfIsEmpty {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (L R : A →L[𝕜] E →L[𝕜] E) (x : E) (a : Fin 1 → A) : ((L.hochschildBimoduleCoboundary R 0) (ContinuousMultilinearMap.constOfIsEmpty 𝕜 (fun (x : Fin 0) => A) x)) a = (L (a 0)) x - (R (a 0)) x

The coboundary of the degree-zero cochain with value x is the inner derivation a ↦ L a x - R a x.

theorem ContinuousLinearMap.hochschildBimoduleCoboundary_constOfIsEmpty_eq_zero_iff {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (L R : A →L[𝕜] E →L[𝕜] E) (x : E) : (L.hochschildBimoduleCoboundary R 0) (ContinuousMultilinearMap.constOfIsEmpty 𝕜 (fun (x : Fin 0) => A) x) = 0 ↔ ∀ (a : A), (L a) x = (R a) x

A degree-zero cochain is a cocycle exactly when its value lies in the centre of the bimodule.

theorem ContinuousLinearMap.hochschildBimoduleCoboundary_ofSubsingleton {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (L R : A →L[𝕜] E →L[𝕜] E) (D : A →L[𝕜] E) (a : Fin 2 → A) : ((L.hochschildBimoduleCoboundary R 1) ((ContinuousMultilinearMap.ofSubsingleton 𝕜 A E 0) D)) a = (L (a 0)) (D (a 1)) - D (a 0 * a 1) + (R (a 1)) (D (a 0))

The coboundary of a degree-one cochain D: (δD)(a₀, a₁) = L a₀ (D a₁) - D (a₀ a₁) + R a₁ (D a₀).

theorem ContinuousLinearMap.hochschildBimoduleCoboundary_ofSubsingleton_eq_zero_iff {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (L R : A →L[𝕜] E →L[𝕜] E) (D : A →L[𝕜] E) : (L.hochschildBimoduleCoboundary R 1) ((ContinuousMultilinearMap.ofSubsingleton 𝕜 A E 0) D) = 0 ↔ ∀ (a b : A), D (a * b) = (L a) (D b) + (R b) (D a)

A degree-one cochain is a cocycle exactly when it is a bounded derivation into the bimodule: D (a * b) = L a (D b) + R b (D a).