Matrix extension of relative cyclic cochains #
A relative cyclic cochain on the forced unitization A⁺ = Unitization R A vanishes when all its
arguments are scalar. Its matrix extension φ#Tr is a sum of values of φ on entries of the
matrix arguments, so it vanishes when all its arguments are scalar matrices, that is matrices with
entries in the image of R → A⁺. This is why the classes of scalar matrices pair trivially with
relative cyclic cohomology.
Main results #
TauCeti.matrixCochainExtension_map_algebraMap_eq_zero: the matrix extension of a relative cyclic cochain vanishes when all its arguments are scalar matrices.
References #
- A. Connes, Noncommutative Geometry, Chapter III, §1 and §3.
- J.-L. Loday, Cyclic Homology, §1.4.
theorem
TauCeti.matrixCochainExtension_map_algebraMap_eq_zero
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[CommSemiring R]
[NonUnitalSemiring A]
[Module R A]
[IsScalarTower R A A]
[SMulCommClass R A A]
[AddCommGroup M]
[Module R M]
{ι : Type u_4}
[Fintype ι]
{n : ℕ}
(φ : ↥(relativeCyclicCochains R A M n))
(a : Fin (n + 1) → Matrix ι ι R)
:
(((matrixCochainExtension ι n) ↑↑φ) fun (k : Fin (n + 1)) => (a k).map ⇑(algebraMap R (Unitization R A))) = 0
The matrix extension of a relative cyclic cochain vanishes when all its arguments are scalar matrices.