Homotopy invariance and multiplicativity of the odd pairing

Let φ be a cyclic cocycle of odd degree 2m + 1 on a unital algebra A, and for an invertible u write f(u) = φ(u⁻¹ - 1, u - 1, …, u⁻¹ - 1, u - 1) for the value entering Connes' odd pairing ⟨[u], [φ]⟩. This file shows that f is unchanged along polynomial paths of invertibles, that it vanishes on square-zero unipotents 1 + N, and that it is multiplicative, f(uv) = f(u) + f(v). Consequently the odd pairing is a homomorphism from the group of invertibles, invariant under conjugation and vanishing on commutators and on the elementary subgroup TauCeti.elementarySubgroup: these are the relations through which it descends to algebraic K₁ = GL_∞(A) / E_∞(A).

The argument has three steps.

• Infinitesimal invariance. Write x = u⁻¹ - 1 and y = u - 1, which are quasi-inverse in both orders. A tangent vector (x', y') to this relation satisfies y' + x' + x'y + xy' = 0. Evaluating bφ = 0 on (z, x, y, …, x, y) and telescoping the inner faces, which split because adjacent entries are quasi-inverse, gives φ(z + zx, y, x, …, y) = φ(x, y, …, x, z + yz). For z = x' + x'y the two entries are x' and -y', and cyclicity then shows that the derivative ∑ₖ φ(…, x' or y' in slot k, …) vanishes (TauCeti.linearDeriv_eq_zero_of_add_add_mul_eq_zero).
• Polynomial homotopy invariance. For an invertible polynomial u(X) with coefficients in A, the zero-derivative principle MultilinearMap.apply_eval_algebraMap_eq_of_linearDeriv_eq_zero shows that f(u(t)) does not depend on the scalar t. The path t ↦ u(1 + tN) for N² = 0 then shows f(u(1 + N)) = f(u).
• Multiplicativity. In 2 × 2 matrices over A, the block diagonal matrix v ⊕ v⁻¹ is a product of six square-zero unipotents, so (uv) ⊕ 1 = (u ⊕ v)(v ⊕ v⁻¹) has the same value of the matrix extension φ#Tr as u ⊕ v. Matrix extension is additive on diagonal matrices, so f(uv) = f(u) + f(v).

Main results

• TauCeti.linearDeriv_eq_zero_of_add_add_mul_eq_zero: infinitesimal invariance of an odd-degree cyclic cocycle on alternating quasi-inverse tuples.
• TauCeti.apply_units_eval_algebraMap_eq: invariance along polynomial paths of invertibles.
• TauCeti.apply_units_mul: multiplicativity, f(uv) = f(u) + f(v).
• TauCeti.cyclicCohomology.oddPairing_map_evalAlgebraMapRingHom_eq: polynomial homotopy invariance of the odd pairing.
• TauCeti.cyclicCohomology.oddPairing_mul, TauCeti.cyclicCohomology.oddPairing_inv and TauCeti.cyclicCohomology.oddPairing_conj: the odd pairing is a homomorphism on invertibles and is invariant under conjugation.
• TauCeti.cyclicCohomology.oddPairingHom: the odd pairing bundled as a homomorphism from the group of invertibles.
• TauCeti.cyclicCohomology.oddPairing_eq_zero_of_val_eq_one_add and TauCeti.cyclicCohomology.oddPairing_eq_zero_of_val_eq_one_add_single: the odd pairing vanishes on square-zero unipotents, in particular on elementary matrices.
• TauCeti.cyclicCohomology.oddPairing_eq_zero_of_mem_commutator and TauCeti.cyclicCohomology.oddPairing_eq_zero_of_mem_elementarySubgroup: the odd pairing vanishes on the commutator subgroup and on the elementary subgroup.

References

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

theorem TauCeti.linearDeriv_eq_zero_of_add_add_mul_eq_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [NonUnitalRing A] [Module R A] [AddCommGroup M] [Module R M] {m : ℕ} {φ : (Fin (2 * m + 2) → A) →ₘₗ[R] M} [IsScalarTower R A A] [SMulCommClass R A A] (hφ : φ ∈ cyclicCochains R A M (2 * m + 1)) (hbφ : (hochschildCoboundary R A M (2 * m + 1)) φ = 0) {x y x' y' : A} (hxy : y + x + x * y = 0) (hyx : x + y + y * x = 0) (h' : y' + x' + x' * y + x * y' = 0) : ((φ.linearDeriv fun (k : Fin (2 * m + 2)) => if Even ↑k then x else y) fun (k : Fin (2 * m + 2)) => if Even ↑k then x' else y') = 0

Infinitesimal invariance on alternating quasi-inverse tuples. Let φ be a cyclic cocycle of odd degree 2m + 1, and let x and y be quasi-inverse in both orders. If (x', y') is tangent to this relation, y' + x' + x'y + xy' = 0, then the derivative of φ at (x, y, …, x, y) in the direction (x', y', …, x', y') vanishes.

theorem TauCeti.apply_units_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] {m : ℕ} {φ : (Fin (2 * m + 2) → A) →ₘₗ[R] M} (hφ : φ ∈ cyclicCochains R A M (2 * m + 1)) (hbφ : (hochschildCoboundary R A M (2 * m + 1)) φ = 0) (u : (Polynomial A)ˣ) (s t : R) : (φ fun (k : Fin (2 * m + 2)) => if Even ↑k then Polynomial.eval ((algebraMap R A) s) ↑u⁻¹ - 1 else Polynomial.eval ((algebraMap R A) s) ↑u - 1) = φ fun (k : Fin (2 * m + 2)) => if Even ↑k then Polynomial.eval ((algebraMap R A) t) ↑u⁻¹ - 1 else Polynomial.eval ((algebraMap R A) t) ↑u - 1

Polynomial homotopy invariance. Let φ be a cyclic cocycle of odd degree 2m + 1 and u an invertible polynomial with coefficients in A. Then φ(u(t)⁻¹ - 1, u(t) - 1, …, u(t)⁻¹ - 1, u(t) - 1) does not depend on the scalar t.

theorem TauCeti.apply_units_mul {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 : ℕ} {φ : (Fin (2 * m + 2) → A) →ₘₗ[R] M} (hφ : φ ∈ cyclicCochains R A M (2 * m + 1)) (hbφ : (hochschildCoboundary R A M (2 * m + 1)) φ = 0) (u v : Aˣ) : (φ fun (k : Fin (2 * m + 2)) => if Even ↑k then ↑(u * v)⁻¹ - 1 else ↑(u * v) - 1) = (φ fun (k : Fin (2 * m + 2)) => if Even ↑k then ↑u⁻¹ - 1 else ↑u - 1) + φ fun (k : Fin (2 * m + 2)) => if Even ↑k then ↑v⁻¹ - 1 else ↑v - 1

Multiplicativity. For a cyclic cocycle φ of odd degree 2m + 1, the value f(u) = φ(u⁻¹ - 1, u - 1, …, u⁻¹ - 1, u - 1) satisfies f(uv) = f(u) + f(v).

theorem TauCeti.cyclicCohomology.oddPairing_map_evalAlgebraMapRingHom_eq {A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A] [AddCommGroup M] [Module ℂ M] (u : (Polynomial A)ˣ) (s t : ℂ) (m : ℕ) : oddPairing ((Units.map ↑(Polynomial.evalAlgebraMapRingHom A s)) u) m = oddPairing ((Units.map ↑(Polynomial.evalAlgebraMapRingHom A t)) u) m

Polynomial homotopy invariance of the odd pairing. For an invertible polynomial u with coefficients in A, the odd pairing with u(t) does not depend on the scalar t.

@[simp]

theorem TauCeti.cyclicCohomology.oddPairing_mul {A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A] [AddCommGroup M] [Module ℂ M] (u v : Aˣ) (m : ℕ) : oddPairing (u * v) m = oddPairing u m + oddPairing v m

Multiplicativity of the odd pairing: ⟨[uv], [φ]⟩ = ⟨[u], [φ]⟩ + ⟨[v], [φ]⟩.

@[simp]

theorem TauCeti.cyclicCohomology.oddPairing_inv {A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A] [AddCommGroup M] [Module ℂ M] (u : Aˣ) (m : ℕ) : oddPairing u⁻¹ m = -oddPairing u m

The odd pairing of the inverse is the negative of the odd pairing.

noncomputable def TauCeti.cyclicCohomology.oddPairingHom (A : Type u_1) (M : Type u_2) [Ring A] [Algebra ℂ A] [AddCommGroup M] [Module ℂ M] (m : ℕ) : Aˣ →* Multiplicative (↑(cyclicCohomology ℂ A M (2 * m + 1)) →ₗ[ℂ] M)

The odd pairing in degree 2m + 1 as a homomorphism from the group of invertibles to the additive group of functionals on cyclic cohomology, written multiplicatively.

@[simp]

theorem TauCeti.cyclicCohomology.oddPairingHom_apply {A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A] [AddCommGroup M] [Module ℂ M] (u : Aˣ) (m : ℕ) : (oddPairingHom A M m) u = Multiplicative.ofAdd (oddPairing u m)

The bundled odd pairing evaluates to the odd pairing.

theorem TauCeti.cyclicCohomology.mem_ker_oddPairingHom {A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A] [AddCommGroup M] [Module ℂ M] {u : Aˣ} {m : ℕ} : u ∈ (oddPairingHom A M m).ker ↔ oddPairing u m = 0

An invertible lies in the kernel of the bundled odd pairing exactly when its odd pairing vanishes.

theorem TauCeti.cyclicCohomology.oddPairing_conj {A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A] [AddCommGroup M] [Module ℂ M] (g u : Aˣ) (m : ℕ) : oddPairing (g * u * g⁻¹) m = oddPairing u m

Conjugation invariance of the odd pairing. Conjugating an invertible by another invertible does not change its odd pairing with cyclic cohomology.

theorem TauCeti.cyclicCohomology.oddPairing_eq_zero_of_val_eq_one_add {A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A] [AddCommGroup M] [Module ℂ M] (e : Aˣ) {N : A} (he : ↑e = 1 + N) (hN : N * N = 0) (m : ℕ) : oddPairing e m = 0

The odd pairing vanishes on a square-zero unipotent 1 + N.

theorem TauCeti.cyclicCohomology.oddPairing_eq_zero_of_val_eq_one_add_single {A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A] [AddCommGroup M] [Module ℂ M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (e : (Matrix ι ι A)ˣ) {i j : ι} (hij : i ≠ j) {c : A} (he : ↑e = 1 + Matrix.single i j c) (m : ℕ) : oddPairing e m = 0

Vanishing of the odd pairing on elementary matrices: the odd pairing of an invertible matrix 1 + c Eᵢⱼ with i ≠ j vanishes.

theorem TauCeti.cyclicCohomology.oddPairing_eq_zero_of_mem_commutator {A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A] [AddCommGroup M] [Module ℂ M] {u : Aˣ} (hu : u ∈ commutator Aˣ) (m : ℕ) : oddPairing u m = 0

The odd pairing vanishes on the commutator subgroup of the group of invertibles.

theorem TauCeti.cyclicCohomology.oddPairing_eq_zero_of_mem_elementarySubgroup {A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A] [AddCommGroup M] [Module ℂ M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] {u : GL ι A} (hu : u ∈ elementarySubgroup ι A) (m : ℕ) : oddPairing u m = 0

Vanishing of the odd pairing on the elementary subgroup: the odd pairing of an invertible matrix generated by elementary matrices 1 + c Eᵢⱼ vanishes.

theorem TauCeti.cyclicCohomology.oddPairing_mul_of_mem_elementarySubgroup {A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A] [AddCommGroup M] [Module ℂ M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (u : GL ι A) {e : GL ι A} (he : e ∈ elementarySubgroup ι A) (m : ℕ) : oddPairing (u * e) m = oddPairing u m

The odd pairing is constant on cosets of the elementary subgroup.