The even pairing of cyclic cohomology with idempotents

Let A be a unital algebra over a field R of characteristic zero and M an R-module. For an idempotent e of A and a cyclic M-valued cocycle φ of degree 2m, the value (m!)⁻¹ φ(e, …, e) depends only on the cyclic cohomology class of φ. This file constructs the resulting linear map HC²ᵐ(A; M) → M. Composed with matrix extension HC²ᵐ(A; M) → HC²ᵐ(Matrix ι ι A; M), it gives Connes' even pairing ⟨[e], [φ]⟩ = (m!)⁻¹ (φ#Tr)(e, …, e) of idempotent matrices with cyclic cohomology, the pairing from which the Chern character of K₀ is built.

The pairing descends to cohomology because every Hochschild face fixes the constant tuple (e, …, e): if φ = bψ with ψ cyclic of odd degree, then φ(e, …, e) = ψ(e, …, e), while cyclicity in odd degree forces ψ(e, …, e) = -ψ(e, …, e).

Main definitions

• TauCeti.cyclicCohomology.evenPairing: the pairing HC²ᵐ(A; M) → M with an idempotent.

Main results

• TauCeti.apply_const_eq_zero_of_mem_cyclicCoboundaries: when 2 is invertible, an even-degree cyclic coboundary vanishes on constant idempotent tuples.
• TauCeti.cyclicCohomology.evenPairing_mk: the pairing evaluated on the class of a cocycle.
• TauCeti.cyclicCohomology.evenPairing_zero: the zero idempotent pairs to zero.
• TauCeti.cyclicCohomology.evenPairing_matrixExtension_mk: Connes' formula ⟨[e], [φ]⟩ = (m!)⁻¹ (φ#Tr)(e, …, e) for an idempotent matrix e.
• TauCeti.cyclicCohomology.evenPairing_fromBlocks_matrixExtension: the pairing is additive on direct sums, ⟨[e ⊕ f], [φ]⟩ = ⟨[e], [φ]⟩ + ⟨[f], [φ]⟩.

References

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

theorem TauCeti.apply_const_eq_zero_of_mem_cyclicCoboundaries {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [Invertible 2] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (hn : Even n) {φ : ↥(cyclicCochains R A M n)} (hφ : φ ∈ cyclicCoboundaries R A M n) {e : A} (he : IsIdempotentElem e) : (↑φ fun (x : Fin (n + 1)) => e) = 0

When 2 is invertible, a cyclic coboundary of even degree vanishes on a constant tuple with idempotent entry. Associativity is not required: each Hochschild face fixes this tuple.

noncomputable def TauCeti.cyclicCohomology.evenPairing {R : Type u_1} {A : Type u_2} {M : Type u_3} [Field R] [CharZero R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (e : A) (he : IsIdempotentElem e) (m : ℕ) : ↑(cyclicCohomology R A M (2 * m)) →ₗ[R] M

The even pairing ⟨[e], [φ]⟩ = (m!)⁻¹ φ(e, …, e) of an idempotent e with cyclic cohomology classes of degree 2m.

@[simp]

theorem TauCeti.cyclicCohomology.evenPairing_mk {R : Type u_1} {A : Type u_2} {M : Type u_3} [Field R] [CharZero R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (e : A) (he : IsIdempotentElem e) (m : ℕ) (φ : ↥(cyclicCocycles R A M (2 * m))) : (evenPairing e he m) ((mk R A M (2 * m)) φ) = (↑m.factorial)⁻¹ • ↑↑φ fun (x : Fin (2 * m + 1)) => e

The even pairing of an idempotent e with the class of a cyclic cocycle φ is (m!)⁻¹ φ(e, …, e).

@[simp]

theorem TauCeti.cyclicCohomology.evenPairing_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [Field R] [CharZero R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (m : ℕ) : evenPairing 0 ⋯ m = 0

The even pairing of the zero idempotent vanishes.

theorem TauCeti.cyclicCohomology.evenPairing_matrixExtension_mk {R : Type u_1} {A : Type u_2} {M : Type u_3} [Field R] [CharZero R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (e : Matrix ι ι A) (he : IsIdempotentElem e) (m : ℕ) (φ : ↥(cyclicCocycles R A M (2 * m))) : (evenPairing e he m) ((matrixExtension M ι (2 * m)) ((mk R A M (2 * m)) φ)) = (↑m.factorial)⁻¹ • ((matrixCochainExtension ι (2 * m)) ↑↑φ) fun (x : Fin (2 * m + 1)) => e

Connes' even pairing of an idempotent matrix e with cyclic cohomology: on the class of a cyclic cocycle φ of degree 2m, it is (m!)⁻¹ (φ#Tr)(e, …, e).

theorem TauCeti.cyclicCohomology.evenPairing_fromBlocks_matrixExtension {R : Type u_1} {A : Type u_2} {M : Type u_3} [Field R] [CharZero R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {ι : Type u_4} {κ : Type u_5} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {e : Matrix ι ι A} {f : Matrix κ κ A} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (m : ℕ) (c : ↑(cyclicCohomology R A M (2 * m))) : (evenPairing (Matrix.fromBlocks e 0 0 f) ⋯ m) ((matrixExtension M (ι ⊕ κ) (2 * m)) c) = (evenPairing e he m) ((matrixExtension M ι (2 * m)) c) + (evenPairing f hf m) ((matrixExtension M κ (2 * m)) c)

Additivity of the even pairing on direct sums: the even pairing of the block-diagonal idempotent matrix e ⊕ f is the sum of the even pairings of e and f.