Cyclic cohomology of the ground ring

For a commutative ring R and an R-module M, this file computes the cyclic cohomology HCⁿ(R; M) of R regarded as an algebra over itself. Every M-valued n-cochain on R is a product cochain (a₀, …, aₙ) ↦ (a₀ ⋯ aₙ) • m (Mathlib's MultilinearMap.mkPiRing). Every Hochschild face preserves the product of the entries, so the Hochschild coboundary of the product cochain is (∑ᵢ (-1)ⁱ) • (a₀ ⋯ aₙ₊₁) • m: it vanishes in even degree and is the product cochain of the same m in odd degree. Rotating the entries does not change their product, so the product cochain is cyclic exactly when (-1)ⁿ • m = m. These cochain and cocycle computations hold over any commutative semiring R.

Consequently:

• in odd degree there are no nonzero cyclic cocycles, and HCⁿ(R; M) = 0;
• in even degree every cochain is a cyclic cocycle, and m ↦ [(a₀ ⋯ aₙ) • m] maps M onto HCⁿ(R; M). In degree zero it is injective; in positive even degree its kernel is the 2-torsion of M, the values of cyclic cochains of the preceding odd degree.

So HC²ᵏ(R; M) ≅ M whenever multiplication by 2 is injective on M, for instance HC²ᵏ(ℂ) ≅ ℂ and HC²ᵏ⁺¹(ℂ) = 0. Over a general commutative ring, HC²ᵏ⁺²(R; M) ≅ M ⧸ M[2] where M[2] is the 2-torsion submodule.

The same computation shows that the Hochschild cohomology HHⁿ(R, Hom_R(R, M)) vanishes for n ≠ 0: the Hochschild complex is M →0 M →id M →0 M →id ⋯.

This is the unreduced cyclic-cochain theory of the ground ring. As in TauCeti.RingTheory.CyclicCohomology.Cohomology, it agrees with the cyclic-bicomplex theory when R contains ℚ. It contrasts with the reduced theory of TauCeti.RingTheory.CyclicCohomology.Reduced, whose complex for the ground ring is zero.

Main definitions

• TauCeti.cyclicCohomology.mkPiRing: the class in even degree of the product cochain of m.
• TauCeti.cyclicCohomology.selfEquiv: M ≃ HCⁿ(R; M) for even n when M has no 2-torsion.
• TauCeti.cyclicCohomology.selfQuotEquiv: M ⧸ M[2] ≃ HCⁿ(R; M) for even n ≠ 0.

Main results

• TauCeti.hochschildCoboundary_mkPiRing_of_even, TauCeti.hochschildCoboundary_mkPiRing_of_odd: the Hochschild coboundary of a product cochain.
• TauCeti.mkPiRing_mem_cyclicCochains_iff: the product cochain of m is cyclic exactly when (-1)ⁿ • m = m.
• TauCeti.cyclicCocycles_self_of_even, TauCeti.cyclicCocycles_self_of_odd: the cyclic cocycles of the ground ring are all cochains in even degree and zero in odd degree.
• TauCeti.isZero_cyclicCohomology_self_of_odd: HCⁿ(R; M) = 0 for odd n.
• TauCeti.isZero_hochschildCohomology_self: HHⁿ(R, Hom_R(R, M)) = 0 for n ≠ 0.
• TauCeti.cyclicCohomology.mkPiRing_surjective, TauCeti.cyclicCohomology.ker_mkPiRing: the class map is surjective, with kernel the 2-torsion of M in positive even degree.

References

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

Product cochains

@[simp]

theorem TauCeti.hochschildCoboundary_mkPiRing_of_even (R : Type u) (M : Type u_1) [CommSemiring R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (m : M) : (hochschildCoboundary R R M n) (MultilinearMap.mkPiRing R (Fin (n + 1)) m) = 0

In even degree the Hochschild coboundary of a product cochain on the ground ring vanishes.

@[simp]

theorem TauCeti.hochschildCoboundary_mkPiRing_of_odd (R : Type u) (M : Type u_1) [CommSemiring R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Odd n) (m : M) : (hochschildCoboundary R R M n) (MultilinearMap.mkPiRing R (Fin (n + 1)) m) = MultilinearMap.mkPiRing R (Fin (n + 2)) m

In odd degree the Hochschild coboundary of the product cochain (a₀, …, aₙ) ↦ (a₀ ⋯ aₙ) • m is the product cochain (a₀, …, aₙ₊₁) ↦ (a₀ ⋯ aₙ₊₁) • m.

theorem TauCeti.hochschildCoboundary_self_of_even (R : Type u) (M : Type u_1) [CommSemiring R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (φ : (Fin (n + 1) → R) →ₘₗ[R] M) : (hochschildCoboundary R R M n) φ = 0

In even degree the Hochschild coboundary of every cochain on the ground ring vanishes.

theorem TauCeti.hochschildCoboundary_self_of_odd (R : Type u) (M : Type u_1) [CommSemiring R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Odd n) (φ : (Fin (n + 1) → R) →ₘₗ[R] M) : (hochschildCoboundary R R M n) φ = MultilinearMap.mkPiRing R (Fin (n + 2)) (φ fun (x : Fin (n + 1)) => 1)

In odd degree the Hochschild coboundary of a cochain on the ground ring is the product cochain of its value at (1, …, 1).

theorem TauCeti.mkPiRing_mem_cyclicCochains_iff {R : Type u} {M : Type u_1} [CommSemiring R] [AddCommGroup M] [Module R M] {n : ℕ} {m : M} : MultilinearMap.mkPiRing R (Fin (n + 1)) m ∈ cyclicCochains R R M n ↔ (-1) ^ n • m = m

The product cochain (a₀, …, aₙ) ↦ (a₀ ⋯ aₙ) • m is cyclic exactly when (-1)ⁿ • m = m.

theorem TauCeti.mkPiRing_mem_cyclicCochains_iff_of_odd {R : Type u} {M : Type u_1} [CommSemiring R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Odd n) {m : M} : MultilinearMap.mkPiRing R (Fin (n + 1)) m ∈ cyclicCochains R R M n ↔ 2 • m = 0

In odd degree the product cochain of m is cyclic exactly when 2 • m = 0.

Cyclic cocycles

theorem TauCeti.cyclicCochains_self_of_even (R : Type u) (M : Type u_1) [CommSemiring R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) : cyclicCochains R R M n = ⊤

In even degree every cochain on the ground ring is cyclic.

theorem TauCeti.cyclicCocycles_self_of_even (R : Type u) (M : Type u_1) [CommSemiring R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) : cyclicCocycles R R M n = ⊤

In even degree every cyclic cochain on the ground ring is a cocycle.

theorem TauCeti.cyclicCocycles_self_of_odd (R : Type u) (M : Type u_1) [CommSemiring R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Odd n) : cyclicCocycles R R M n = ⊥

In odd degree the ground ring has no nonzero cyclic cocycles.

Even cocycle representatives

Cyclic cohomology

theorem TauCeti.isZero_cyclicCohomology_self_of_odd (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Odd n) : CategoryTheory.Limits.IsZero (cyclicCohomology R R M n)

The cyclic cohomology of the ground ring vanishes in odd degree.

Hochschild cohomology

theorem TauCeti.isZero_hochschildCohomology_self (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : n ≠ 0) : CategoryTheory.Limits.IsZero (hochschildCohomology R R M n)

The Hochschild cohomology HHⁿ(R, Hom_R(R, M)) of the ground ring vanishes in positive degree: in even degree every cochain is the coboundary of a product cochain, and in odd degree the only cocycle is zero.

noncomputable def TauCeti.cyclicCohomology.mkPiRing (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) (hn : Even n) : M →ₗ[R] ↑(cyclicCohomology R R M n)

For even n, the class in HCⁿ(R; M) of the product cochain (a₀, …, aₙ) ↦ (a₀ ⋯ aₙ) • m.

theorem TauCeti.cyclicCohomology.mkPiRing_apply (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (m : M) : (mkPiRing R M n hn) m = (mk R R M n) ⟨⟨MultilinearMap.mkPiRing R (Fin (n + 1)) m, ⋯⟩, ⋯⟩

mkPiRing R M n hn m is the class of the product cochain of m.

theorem TauCeti.cyclicCohomology.mk_eq_mkPiRing (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (φ : ↥(cyclicCocycles R R M n)) : (mk R R M n) φ = (mkPiRing R M n hn) (↑↑φ fun (x : Fin (n + 1)) => 1)

In even degree the class of a cyclic cocycle φ is the class of the product cochain of its value φ(1, …, 1).

theorem TauCeti.cyclicCohomology.mkPiRing_surjective (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) : Function.Surjective ⇑(mkPiRing R M n hn)

In even degree every cyclic cohomology class of the ground ring is the class of a product cochain.

theorem TauCeti.cyclicCohomology.mkPiRing_eq_zero_iff {R : Type u} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (hn₀ : n ≠ 0) {m : M} : (mkPiRing R M n hn) m = 0 ↔ 2 • m = 0

In positive even degree the class of the product cochain of m vanishes exactly when 2 • m = 0: the coboundaries are the product cochains of 2-torsion elements, which are cyclic in the preceding odd degree.

theorem TauCeti.cyclicCohomology.ker_mkPiRing (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (hn₀ : n ≠ 0) : (mkPiRing R M n hn).ker = Submodule.torsionBy R M 2

In positive even degree the kernel of the class map is the 2-torsion of M.

theorem TauCeti.cyclicCohomology.mkPiRing_zero_injective (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {even_zero : Even 0} : Function.Injective ⇑(mkPiRing R M 0 even_zero)

In degree zero the class map is injective.

theorem TauCeti.cyclicCohomology.mkPiRing_injective (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (h2 : IsSMulRegular M 2) : Function.Injective ⇑(mkPiRing R M n hn)

In even degree the class map is injective when M has no 2-torsion.

noncomputable def TauCeti.cyclicCohomology.selfEquiv (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (h2 : IsSMulRegular M 2) : M ≃ₗ[R] ↑(cyclicCohomology R R M n)

If multiplication by 2 is injective on M, then HCⁿ(R; M) ≅ M in every even degree n, by the class of the product cochain. In particular HC²ᵏ(ℂ) ≅ ℂ.

@[simp]

theorem TauCeti.cyclicCohomology.selfEquiv_apply (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (h2 : IsSMulRegular M 2) (m : M) : (selfEquiv R M hn h2) m = (mkPiRing R M n hn) m

selfEquiv sends m to the class of its product cochain.

@[simp]

theorem TauCeti.cyclicCohomology.selfEquiv_symm_mk (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (h2 : IsSMulRegular M 2) (φ : ↥(cyclicCocycles R R M n)) : (selfEquiv R M hn h2).symm ((mk R R M n) φ) = ↑↑φ fun (x : Fin (n + 1)) => 1

The inverse of selfEquiv evaluates a representing cocycle at (1, …, 1).

noncomputable def TauCeti.cyclicCohomology.selfQuotEquiv (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (hn₀ : n ≠ 0) : (M ⧸ Submodule.torsionBy R M 2) ≃ₗ[R] ↑(cyclicCohomology R R M n)

In positive even degree HCⁿ(R; M) is the quotient of M by its 2-torsion, by the class of the product cochain.

@[simp]

theorem TauCeti.cyclicCohomology.selfQuotEquiv_mk (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (hn₀ : n ≠ 0) (m : M) : (selfQuotEquiv R M hn hn₀) (Submodule.Quotient.mk m) = (mkPiRing R M n hn) m

selfQuotEquiv sends the class of m to the class of its product cochain.

@[simp]

theorem TauCeti.cyclicCohomology.selfQuotEquiv_symm_mk (R : Type u) (M : Type u_1) [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : Even n) (hn₀ : n ≠ 0) (φ : ↥(cyclicCocycles R R M n)) : (selfQuotEquiv R M hn hn₀).symm ((mk R R M n) φ) = Submodule.Quotient.mk (↑↑φ fun (x : Fin (n + 1)) => 1)

The inverse of selfQuotEquiv sends a represented cohomology class to the quotient class of the representing cocycle's value at (1, …, 1).