The Hochschild cochain complex and its cohomology

The M-valued multilinear cochains Cⁿ(A; M) of an algebra A, the maps φ : Aⁿ⁺¹ → M, form the Hochschild cochain complex hochschildCochainComplex R A M under the Hochschild coboundary b. Here M is only an R-module, and a degree-n cochain takes n + 1 arguments. Currying the first argument identifies these cochains with the Hom_R(A, M)-valued cochains in n arguments, and b with the Hochschild coboundary of the bimodule Hom_R(A, M), whose actions are (x f y)(a) = f (y a x) (TauCeti.multilinearCurryFirstEquiv_hochschildCoboundary). So for a unital algebra A the cohomology of this complex is, in Connes' cochain description, the Hochschild cohomology HHⁿ(A, Hom_R(A, M)) of A with coefficients in Hom_R(A, M), and not the Hochschild cohomology with coefficients in M. For M = R it is HHⁿ(A, A*), the Hochschild cohomology of A with coefficients in its dual bimodule.

The complex and its cohomology are defined for nonunital associative algebras. For a nonunital algebra this is the naive cochain complex, rather than the relative complex of its forced unitization.

The concrete cocycles and coboundaries are defined over semirings when the R-action on M commutes with itself. The categorical complex and cohomology use a commutative ring.

As for cyclic cohomology, hochschildCohomology.mk sends a Hochschild cocycle to its class; it is surjective and its kernel consists exactly of the coboundaries, so linear maps out of Hochschild cohomology are described by hochschildCohomology.desc. In degree zero there are no coboundaries and the cocycles are the traces.

Main definitions

• TauCeti.hochschildCochainComplex: the Hochschild cochain complex.
• TauCeti.hochschildCocycles, TauCeti.hochschildCoboundaries: Hochschild cocycles and coboundaries.
• TauCeti.hochschildCohomology: the cohomology of the Hochschild cochain complex; for a unital algebra it is the Hochschild cohomology HHⁿ(A, Hom_R(A, M)).
• TauCeti.hochschildCohomology.mk: the class of a Hochschild cocycle.
• TauCeti.hochschildCohomology.desc: the linear map out of Hochschild cohomology induced by a linear map on Hochschild cocycles vanishing on Hochschild coboundaries.

Main results

• TauCeti.hochschildCohomology.mk_surjective, TauCeti.hochschildCohomology.mk_eq_zero_iff: Hochschild cohomology is the quotient of the cocycles by the coboundaries.
• TauCeti.mem_hochschildCocycles_zero_iff: the Hochschild 0-cocycles are the traces.

References

• A. Connes, Noncommutative Geometry, Chapter III, §1.
• J.-L. Loday, Cyclic Homology, §2.2.

def TauCeti.hochschildCocycles (R : Type u_1) (A : Type u) (M : Type u_2) [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : Submodule R ((Fin (n + 1) → A) →ₘₗ[R] M)

The Hochschild n-cocycles: the n-cochains annihilated by the Hochschild coboundary.

@[simp]

theorem TauCeti.mem_hochschildCocycles_iff {R : Type u_1} {A : Type u} {M : Type u_2} [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} {φ : (Fin (n + 1) → A) →ₘₗ[R] M} : φ ∈ hochschildCocycles R A M n ↔ (hochschildCoboundary R A M n) φ = 0

A cochain is a Hochschild cocycle exactly when its Hochschild coboundary vanishes.

def TauCeti.hochschildCoboundaries (R : Type u_1) (A : Type u) (M : Type u_2) [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : Submodule R ((Fin (n + 1) → A) →ₘₗ[R] M)

The Hochschild n-coboundaries: zero in degree zero, and the image of the Hochschild coboundary of n-cochains in degree n + 1.

@[simp]

theorem TauCeti.hochschildCoboundaries_zero (R : Type u_1) (A : Type u) (M : Type u_2) [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] : hochschildCoboundaries R A M 0 = ⊥

There are no nonzero Hochschild coboundaries in degree zero.

theorem TauCeti.hochschildCoboundaries_succ (R : Type u_1) (A : Type u) (M : Type u_2) [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : hochschildCoboundaries R A M (n + 1) = (hochschildCoboundary R A M n).range

In positive degree the Hochschild coboundaries are the image of the Hochschild coboundary.

@[simp]

theorem TauCeti.mem_hochschildCoboundaries_succ_iff {R : Type u_1} {A : Type u} {M : Type u_2} [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} {φ : (Fin (n + 2) → A) →ₘₗ[R] M} : φ ∈ hochschildCoboundaries R A M (n + 1) ↔ ∃ (ψ : (Fin (n + 1) → A) →ₘₗ[R] M), (hochschildCoboundary R A M n) ψ = φ

An (n + 1)-cochain is a Hochschild coboundary exactly when it is the Hochschild coboundary of an n-cochain.

theorem TauCeti.hochschildCoboundaries_le_hochschildCocycles (R : Type u_1) (A : Type u) (M : Type u_2) [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : hochschildCoboundaries R A M n ≤ hochschildCocycles R A M n

Every Hochschild coboundary is a Hochschild cocycle.

theorem TauCeti.mem_hochschildCocycles_zero_iff {R : Type u_1} {A : Type u} {M : Type u_2} [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {φ : (Fin 1 → A) →ₘₗ[R] M} : φ ∈ hochschildCocycles R A M 0 ↔ ∀ (x y : A), (φ fun (x_1 : Fin 1) => x * y) = φ fun (x_1 : Fin 1) => y * x

A 0-cochain is a Hochschild cocycle exactly when it is a trace.

def TauCeti.hochschildCochainComplex (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] : CochainComplex (ModuleCat R) ℕ

The Hochschild cochain complex C⁰ → C¹ → ⋯: in degree n the M-valued n-cochains on A, the multilinear maps in n + 1 arguments, with the Hochschild coboundary as differential.

def TauCeti.hochschildCochainComplexXIso (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) : (hochschildCochainComplex R A M).X n ≅ ↧((Fin (n + 1) → A) →ₘₗ[R] M)

The degree-n term of the Hochschild cochain complex is the module of n-cochains.

theorem TauCeti.hochschildCochainComplex_d (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((hochschildCochainComplex R A M).d n (n + 1)) (hochschildCochainComplexXIso R A M (n + 1)).hom = CategoryTheory.CategoryStruct.comp (hochschildCochainComplexXIso R A M n).hom (ModuleCat.ofHom (hochschildCoboundary R A M n))

Under the identifications hochschildCochainComplexXIso, the differential of the Hochschild cochain complex is the Hochschild coboundary.

theorem TauCeti.hochschildCochainComplex_d_assoc (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) {Z : ModuleCat R} (h : ↧((Fin (n + 1 + 1) → A) →ₘₗ[R] M) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((hochschildCochainComplex R A M).d n (n + 1)) (CategoryTheory.CategoryStruct.comp (hochschildCochainComplexXIso R A M (n + 1)).hom h) = CategoryTheory.CategoryStruct.comp (hochschildCochainComplexXIso R A M n).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (hochschildCoboundary R A M n)) h)

Under the identifications hochschildCochainComplexXIso, the differential of the Hochschild cochain complex is the Hochschild coboundary.

theorem TauCeti.hochschildCochainComplex_d_apply (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) (x : ↑((hochschildCochainComplex R A M).X n)) : (CategoryTheory.ConcreteCategory.hom (hochschildCochainComplexXIso R A M (n + 1)).hom) ((CategoryTheory.ConcreteCategory.hom ((hochschildCochainComplex R A M).d n (n + 1))) x) = (hochschildCoboundary R A M n) ((CategoryTheory.ConcreteCategory.hom (hochschildCochainComplexXIso R A M n).hom) x)

Under the identifications hochschildCochainComplexXIso, the differential of the Hochschild cochain complex is the Hochschild coboundary.

@[reducible, inline]

noncomputable abbrev TauCeti.hochschildCohomology (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) : ModuleCat R

The cohomology of the Hochschild cochain complex of A with M-valued cochains in n + 1 arguments. For a unital algebra A, in Connes' cochain description this is the Hochschild cohomology HHⁿ(A, Hom_R(A, M)) of A with coefficients in the bimodule Hom_R(A, M), not with coefficients in M; for M = R it is HHⁿ(A, A*), with coefficients in the dual bimodule.

noncomputable def TauCeti.hochschildCohomology.mk (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) : ↥(hochschildCocycles R A M n) →ₗ[R] ↑(hochschildCohomology R A M n)

The Hochschild cohomology class of a Hochschild cocycle.

theorem TauCeti.hochschildCohomology.mk_eq_homologyπ (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {n : ℕ} (φ : ↥(hochschildCocycles R A M n)) (z : ↑(HomologicalComplex.cycles (hochschildCochainComplex R A M) n)) (hz : (CategoryTheory.ConcreteCategory.hom (hochschildCochainComplexXIso R A M n).hom) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (hochschildCochainComplex R A M) n)) z) = ↑φ) : (mk R A M n) φ = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (hochschildCochainComplex R A M) n)) z

The class of a Hochschild cocycle φ is the homology class of any cycle of the Hochschild cochain complex whose underlying cochain is φ.

theorem TauCeti.hochschildCohomology.mk_surjective (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) : Function.Surjective ⇑(mk R A M n)

Every Hochschild cohomology class is the class of a Hochschild cocycle.

@[simp]

theorem TauCeti.hochschildCohomology.mk_eq_zero_iff (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) (φ : ↥(hochschildCocycles R A M n)) : (mk R A M n) φ = 0 ↔ ↑φ ∈ hochschildCoboundaries R A M n

A Hochschild cocycle has zero cohomology class exactly when it is a Hochschild coboundary.

theorem TauCeti.hochschildCohomology.mk_eq_mk_iff (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) (φ ψ : ↥(hochschildCocycles R A M n)) : (mk R A M n) φ = (mk R A M n) ψ ↔ ↑φ - ↑ψ ∈ hochschildCoboundaries R A M n

Two Hochschild cocycles have the same class exactly when they differ by a Hochschild coboundary.

theorem TauCeti.hochschildCohomology.linearMap_ext {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {n : ℕ} {f g : ↑(hochschildCohomology R A M n) →ₗ[R] N} (h : f ∘ₗ mk R A M n = g ∘ₗ mk R A M n) : f = g

Two linear maps out of Hochschild cohomology agree once they agree on classes of cocycles.

theorem TauCeti.hochschildCohomology.linearMap_ext_iff {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {n : ℕ} {f g : ↑(hochschildCohomology R A M n) →ₗ[R] N} : f = g ↔ f ∘ₗ mk R A M n = g ∘ₗ mk R A M n

noncomputable def TauCeti.hochschildCohomology.desc {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (n : ℕ) (f : ↥(hochschildCocycles R A M n) →ₗ[R] N) (hf : ∀ (φ : ↥(hochschildCocycles R A M n)), ↑φ ∈ hochschildCoboundaries R A M n → f φ = 0) : ↑(hochschildCohomology R A M n) →ₗ[R] N

A linear map on Hochschild cocycles that vanishes on Hochschild coboundaries descends to Hochschild cohomology.

@[simp]

theorem TauCeti.hochschildCohomology.desc_mk {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (n : ℕ) (f : ↥(hochschildCocycles R A M n) →ₗ[R] N) (hf : ∀ (φ : ↥(hochschildCocycles R A M n)), ↑φ ∈ hochschildCoboundaries R A M n → f φ = 0) (φ : ↥(hochschildCocycles R A M n)) : (desc n f hf) ((mk R A M n) φ) = f φ

The descended map sends the class of a cocycle to the value of the original map.

@[simp]

theorem TauCeti.hochschildCohomology.desc_comp_mk {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (n : ℕ) (f : ↥(hochschildCocycles R A M n) →ₗ[R] N) (hf : ∀ (φ : ↥(hochschildCocycles R A M n)), ↑φ ∈ hochschildCoboundaries R A M n → f φ = 0) : desc n f hf ∘ₗ mk R A M n = f

The descended map composed with the class map is the original map.