Homotopy and conjugation invariance of the even pairing

Let φ be a cyclic cocycle of even degree on an algebra A. This file shows that the value φ(e, …, e) on an idempotent e, and hence Connes' even pairing ⟨[e], [φ]⟩, is unchanged by moving e along a polynomial path of idempotents and by conjugating e by an invertible element. These are the invariances needed before the even pairing can descend from idempotents to K₀.

The argument has three steps.

• Infinitesimal invariance. If e is idempotent and y is tangent to the idempotents at e, that is e y + y e = y, then φ(e, …, y, …, e) = 0 in every slot. Indeed y = x e - e x for x = y e - e y, and evaluating bφ = 0 on (x, e, …, e) gives φ(x e, e, …, e) = φ(e x, e, …, e) in even degree; cyclicity moves the distinguished entry to any slot. This is TauCeti.apply_update_const_eq_zero_of_isIdempotentElem, proved in TauCeti.RingTheory.CyclicCohomology.Cochain.
• Polynomial homotopy invariance. For an idempotent e(X) with coefficients in A, the derivative of t ↦ φ(e(t), …, e(t)) is a sum of such infinitesimal terms, because e′ = e e′ + e′ e. By the zero-derivative principle of MultilinearMap.apply_eval_algebraMap_eq_of_linearDeriv_eq_zero, it is constant.
• Conjugation invariance. For N² = 0 the path t ↦ (1 + tN) e (1 - tN) joins e to (1 + N) e (1 - N). In 2 × 2 matrices, conjugating the corner e ⊕ 0 by !![0, u; -u⁻¹, 0], a product of three such unipotents, gives the corner 0 ⊕ u⁻¹ e u; matrix extension φ#Tr recovers φ on either corner.

Applied to the algebra Matrix ι ι A, the conjugation statements cover conjugation of idempotent matrices by invertible matrices.

Main results

• TauCeti.apply_const_eval_algebraMap_eq: invariance of φ(e, …, e) along polynomial paths of idempotents.
• TauCeti.apply_const_units_conj: invariance of φ(e, …, e) under conjugation by a unit.
• TauCeti.cyclicCohomology.evenPairing_eval_algebraMap_eq and TauCeti.cyclicCohomology.evenPairing_units_conj: the corresponding invariances of the even pairing.
• TauCeti.cyclicCohomology.evenPairing_matrixExtension_eq_of_mul_eq: Murray–von Neumann invariance, for idempotent matrices e = a * b and f = b * a of possibly different sizes.

References

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

theorem TauCeti.apply_const_eval_algebraMap_eq {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] {n : ℕ} (hn : Even n) {φ : (Fin (n + 1) → A) →ₘₗ[R] M} (hφ : φ ∈ cyclicCochains R A M n) (hbφ : (hochschildCoboundary R A M n) φ = 0) {e : Polynomial A} (he : IsIdempotentElem e) (s t : R) : (φ fun (x : Fin (n + 1)) => Polynomial.eval ((algebraMap R A) s) e) = φ fun (x : Fin (n + 1)) => Polynomial.eval ((algebraMap R A) t) e

Polynomial homotopy invariance. Let φ be a cyclic cocycle of even degree and e an idempotent polynomial with coefficients in A. Then φ(e(t), …, e(t)) does not depend on the scalar t.

theorem TauCeti.apply_const_units_conj {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] {n : ℕ} (hn : Even n) {φ : (Fin (n + 1) → A) →ₘₗ[R] M} (hφ : φ ∈ cyclicCochains R A M n) (hbφ : (hochschildCoboundary R A M n) φ = 0) (u : Aˣ) {e : A} (he : IsIdempotentElem e) : (φ fun (x : Fin (n + 1)) => ↑u * e * ↑u⁻¹) = φ fun (x : Fin (n + 1)) => e

Conjugation invariance. Conjugating an idempotent e by a unit u preserves the value φ(e, …, e) of a cyclic cocycle φ of even degree.

theorem TauCeti.cyclicCohomology.evenPairing_eval_algebraMap_eq {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 : Polynomial A} (he : IsIdempotentElem e) (s t : R) (hs : IsIdempotentElem (Polynomial.eval ((algebraMap R A) s) e)) (ht : IsIdempotentElem (Polynomial.eval ((algebraMap R A) t) e)) (m : ℕ) : evenPairing (Polynomial.eval ((algebraMap R A) s) e) hs m = evenPairing (Polynomial.eval ((algebraMap R A) t) e) ht m

Polynomial homotopy invariance of the even pairing. For an idempotent polynomial e with coefficients in A, the even pairing with e(t) does not depend on the scalar t.

theorem TauCeti.cyclicCohomology.evenPairing_units_conj {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] (u : Aˣ) {e : A} (he : IsIdempotentElem e) (hue : IsIdempotentElem (↑u * e * ↑u⁻¹)) (m : ℕ) : evenPairing (↑u * e * ↑u⁻¹) hue m = evenPairing e he m

Conjugation invariance of the even pairing. Conjugating an idempotent by a unit does not change its even pairing with cyclic cohomology.

theorem TauCeti.cyclicCohomology.evenPairing_matrixExtension_eq_of_mul_eq {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) {a : Matrix ι κ A} {b : Matrix κ ι A} (hab : a * b = e) (hba : b * a = f) (m : ℕ) (c : ↑(cyclicCohomology R A M (2 * m))) : (evenPairing e he m) ((matrixExtension M ι (2 * m)) c) = (evenPairing f hf m) ((matrixExtension M κ (2 * m)) c)

Murray–von Neumann invariance of the even pairing. If idempotent matrices e and f, possibly of different sizes, factor as e = a * b and f = b * a through rectangular matrices, then they have the same even pairing with every cyclic cohomology class of A.