Matrix extensions of multilinear cochains

The generalized matrix trace extends a scalar cochain to matrices by summing over closed paths of matrix indices. This construction is multilinear, preserves signed cyclicity, and recovers the original cochain on a single diagonal corner. Matrix extension commutes with cyclic rotation, the cyclic norm, insertion of the unit, and Connes' operator B. It is the cochain-level input to matrix Morita invariance and pairings with idempotents and invertibles.

No multiplication on the coefficient module is needed. The cochain constructions work over any semiring whose action on the coefficient module commutes with itself. In degree zero the construction is ordinary matrix trace followed by the original linear functional.

Matrix extension commutes with every Hochschild coface, hence with the Hochschild coboundary: (bφ)#Tr = b(φ#Tr). For the faces multiplying adjacent entries this is the expansion of a matrix product over the intermediate index, which lengthens a closed index path by one; the last face is reduced to the zeroth by cyclic rotation. Consequently matrix extension maps cyclic cocycles and coboundaries to cyclic cocycles and coboundaries, and induces a map HCⁿ(A; M) → HCⁿ(Matrix ι ι A; M) on cyclic cohomology.

The convention follows Connes, Noncommutative Geometry, Chapter III, §1. The construction uses MultilinearMap.compLinearMap and Matrix.entryLinearMap.

Main definitions

• TauCeti.matrixCochainExtension: the matrix extension φ ↦ φ#Tr.
• TauCeti.matrixCyclicCochainExtension: its restriction to cyclic cochains.
• TauCeti.cyclicCohomology.matrixExtension: the induced map on cyclic cohomology.

Main results

• TauCeti.matrixCochainExtension_cyclic: matrix extension preserves signed cyclicity.
• TauCeti.matrixCochainExtension_fromBlocks_zero₁₂_zero₂₁: matrix extension is additive on block-diagonal matrices, the cochain-level input to additivity of the pairings on direct sums.
• TauCeti.matrixCochainExtension_diagonal: on diagonal matrices, matrix extension is the sum of the original cochain over the diagonal positions.
• TauCeti.matrixCochainExtension_hochschildCoface, TauCeti.matrixCochainExtension_hochschildCoboundary: compatibility with the cofaces and the Hochschild coboundary.
• TauCeti.cyclicCohomology.matrixExtension_map: on cyclic cohomology, matrix extension is natural for algebra homomorphisms.

noncomputable def TauCeti.matrixCochainExtension {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] (ι : Type u_4) [Fintype ι] (n : ℕ) : ((Fin (n + 1) → A) →ₘₗ[R] M) →ₗ[R] (Fin (n + 1) → Matrix ι ι A) →ₘₗ[R] M

Extend a degree-n cochain to square matrices by the generalized matrix trace: sum φ(a₀(i₀,i₁), …, aₙ(iₙ,i₀)) over all closed index paths.

@[simp]

theorem TauCeti.matrixCochainExtension_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] (ι : Type u_4) [Fintype ι] (n : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (a : Fin (n + 1) → Matrix ι ι A) : ((matrixCochainExtension ι n) φ) a = ∑ p : Fin (n + 1) → ι, φ fun (j : Fin (n + 1)) => a j (p j) (p ((finRotate (n + 1)) j))

The closed-path formula for the matrix extension.

theorem TauCeti.matrixCochainExtension_cyclic {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] (ι : Type u_4) [Fintype ι] (n : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (c : R) (hφ : ∀ (x : Fin (n + 1) → A), φ (x ∘ ⇑(Equiv.symm (finRotate (n + 1)))) = c • φ x) (a : Fin (n + 1) → Matrix ι ι A) : ((matrixCochainExtension ι n) φ) (a ∘ ⇑(Equiv.symm (finRotate (n + 1)))) = c • ((matrixCochainExtension ι n) φ) a

Any signed cyclicity relation of a cochain is inherited by its matrix extension. Over a ring, degree-n cyclic cochains have c = (-1 : R) ^ n.

theorem TauCeti.matrixCochainExtension_mem_cyclicCochains {R : Type u_4} [Semiring R] {A : Type u_5} {M : Type u_6} [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (ι : Type u_7) [Fintype ι] (n : ℕ) (φ : ↥(cyclicCochains R A M n)) : (matrixCochainExtension ι n) ↑φ ∈ cyclicCochains R (Matrix ι ι A) M n

Matrix extension sends cyclic cochains to cyclic cochains.

noncomputable def TauCeti.matrixCyclicCochainExtension {R : Type u_4} [Semiring R] {A : Type u_5} {M : Type u_6} [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (ι : Type u_7) [Fintype ι] (n : ℕ) : ↥(cyclicCochains R A M n) →ₗ[R] ↥(cyclicCochains R (Matrix ι ι A) M n)

Extension of cyclic cochains to square matrix algebras.

@[simp]

theorem TauCeti.coe_matrixCyclicCochainExtension_apply {R : Type u_4} [Semiring R] {A : Type u_5} {M : Type u_6} [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (ι : Type u_7) [Fintype ι] (n : ℕ) (φ : ↥(cyclicCochains R A M n)) : ↑((matrixCyclicCochainExtension ι n) φ) = (matrixCochainExtension ι n) ↑φ

The underlying cochain of a matrix-extended cyclic cochain is its generalized matrix trace.

@[simp]

theorem TauCeti.matrixCochainExtension_unique {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] (ι : Type u_4) [Fintype ι] [Unique ι] (n : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (a : Fin (n + 1) → Matrix ι ι A) : ((matrixCochainExtension ι n) φ) a = φ fun (j : Fin (n + 1)) => a j default default

On a one-by-one matrix algebra, matrix extension is the original cochain.

theorem TauCeti.matrixCochainExtension_submatrix {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] (ι : Type u_4) (κ : Type u_5) [Fintype ι] [Fintype κ] (e : ι ↪ κ) (n : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (a : Fin (n + 1) → Matrix κ κ A) (ha : ∀ (j : Fin (n + 1)), ∀ r ∉ Set.range ⇑e, ∀ (s : κ), a j r s = 0) : (((matrixCochainExtension ι n) φ) fun (j : Fin (n + 1)) => (a j).submatrix ⇑e ⇑e) = ((matrixCochainExtension κ n) φ) a

Extension is unchanged by restricting matrices to an embedded index set, provided all rows outside that set vanish. In particular, it is unchanged by zero stabilization.

theorem TauCeti.matrixCochainExtension_submatrix_equiv {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] (ι : Type u_4) (κ : Type u_5) [Fintype ι] [Fintype κ] (e : ι ≃ κ) (n : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (a : Fin (n + 1) → Matrix κ κ A) : (((matrixCochainExtension ι n) φ) fun (j : Fin (n + 1)) => (a j).submatrix ⇑e ⇑e) = ((matrixCochainExtension κ n) φ) a

Relabeling the matrix indices does not change the generalized trace.

theorem TauCeti.matrixCochainExtension_fromBlocks_zero₁₂_zero₂₁ {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] (ι : Type u_4) (κ : Type u_5) [Fintype ι] [Fintype κ] (n : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (a : Fin (n + 1) → Matrix ι ι A) (b : Fin (n + 1) → Matrix κ κ A) : (((matrixCochainExtension (ι ⊕ κ) n) φ) fun (j : Fin (n + 1)) => Matrix.fromBlocks (a j) 0 0 (b j)) = ((matrixCochainExtension ι n) φ) a + ((matrixCochainExtension κ n) φ) b

The matrix extension of a tuple of block-diagonal matrices is the sum of the matrix extensions of the two tuples of diagonal blocks.

@[simp]

theorem TauCeti.matrixCochainExtension_fromBlocks_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] (ι : Type u_4) (κ : Type u_5) [Fintype ι] [Fintype κ] (n : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (a : Fin (n + 1) → Matrix ι ι A) : (((matrixCochainExtension (ι ⊕ κ) n) φ) fun (j : Fin (n + 1)) => Matrix.fromBlocks (a j) 0 0 0) = ((matrixCochainExtension ι n) φ) a

Adding a zero diagonal block leaves the matrix extension unchanged.

theorem TauCeti.matrixCochainExtension_diagonal {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] (ι : Type u_4) [Fintype ι] [DecidableEq ι] (n : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (d : Fin (n + 1) → ι → A) : (((matrixCochainExtension ι n) φ) fun (j : Fin (n + 1)) => Matrix.diagonal (d j)) = ∑ i : ι, φ fun (j : Fin (n + 1)) => d j i

The matrix extension of a tuple of diagonal matrices is the sum, over the diagonal positions, of the original cochain on the diagonal entries.

@[simp]

theorem TauCeti.matrixCochainExtension_single {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] (ι : Type u_4) [Fintype ι] [DecidableEq ι] (r : ι) (n : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (x : Fin (n + 1) → A) : (((matrixCochainExtension ι n) φ) fun (j : Fin (n + 1)) => Matrix.single r r (x j)) = φ x

Restricting to a diagonal matrix corner recovers the original cochain in every degree.

theorem TauCeti.matrixCochainExtension_injective {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] (ι : Type u_4) [Fintype ι] [Nonempty ι] (n : ℕ) : Function.Injective ⇑(matrixCochainExtension ι n)

Matrix extension is injective for every nonempty matrix index type.

theorem TauCeti.matrixCyclicCochainExtension_injective {R : Type u_4} [Semiring R] {A : Type u_5} {M : Type u_6} [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (ι : Type u_7) [Fintype ι] [Nonempty ι] (n : ℕ) : Function.Injective ⇑(matrixCyclicCochainExtension ι n)

Matrix extension is injective on cyclic cochains for a nonempty matrix index type.

@[simp]

theorem TauCeti.matrixCochainExtension_zero_eq_trace {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] (ι : Type u_4) [Fintype ι] (φ : (Fin 1 → A) →ₘₗ[R] M) (a : Matrix ι ι A) : (((matrixCochainExtension ι 0) φ) fun (x : Fin (0 + 1)) => a) = φ fun (x : Fin 1) => a.trace

In degree zero, matrix extension is ordinary trace followed by the unary cochain.

theorem TauCeti.matrixCochainExtension_compMultilinearMap {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] {N : Type u_4} [AddCommMonoid N] [Module R N] [SMulCommClass R R N] (ι : Type u_5) [Fintype ι] (n : ℕ) (f : M →ₗ[R] N) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (matrixCochainExtension ι n) (f.compMultilinearMap φ) = f.compMultilinearMap ((matrixCochainExtension ι n) φ)

Applying a linear map to the cochain values commutes with matrix extension.

theorem TauCeti.matrixCochainExtension_compLinearMap {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] {B : Type u_4} [AddCommMonoid B] [Module R B] (ι : Type u_5) [Fintype ι] (n : ℕ) (f : B →ₗ[R] A) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (matrixCochainExtension ι n) (φ.compLinearMap fun (x : Fin (n + 1)) => f) = ((matrixCochainExtension ι n) φ).compLinearMap fun (x : Fin (n + 1)) => f.mapMatrix

Pulling a cochain back along a linear map commutes with entrywise application of that map to its matrix arguments. Algebra homomorphisms are a special case.

Compatibility with the Hochschild coboundary

theorem TauCeti.matrixCochainExtension_hochschildCoface {R : Type u_4} {A : Type u_5} {M : Type u_6} [NonUnitalNonAssocSemiring A] [AddCommMonoid M] [Semiring R] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [Module R M] [SMulCommClass R R M] (ι : Type u_7) [Fintype ι] (n : ℕ) (i : Fin (n + 2)) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (matrixCochainExtension ι (n + 1)) ((hochschildCoface R A M i) φ) = (hochschildCoface R (Matrix ι ι A) M i) ((matrixCochainExtension ι n) φ)

Matrix extension commutes with each Hochschild coface.

theorem TauCeti.matrixCochainExtension_hochschildCoboundary {R : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (ι : Type u_7) [Fintype ι] (n : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (matrixCochainExtension ι (n + 1)) ((hochschildCoboundary R A M n) φ) = (hochschildCoboundary R (Matrix ι ι A) M n) ((matrixCochainExtension ι n) φ)

Matrix extension commutes with the Hochschild coboundary: (bφ)#Tr = b(φ#Tr).

theorem TauCeti.cyclicHochschildCoboundary_matrixCyclicCochainExtension {R : Type u_4} {A : Type u_5} {M : Type u_6} [AddCommGroup M] {ι : Type u_7} [Fintype ι] {n : ℕ} [Semiring R] [Module R M] [SMulCommClass R R M] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (φ : ↥(cyclicCochains R A M n)) : (cyclicHochschildCoboundary R (Matrix ι ι A) M n) ((matrixCyclicCochainExtension ι n) φ) = (matrixCyclicCochainExtension ι (n + 1)) ((cyclicHochschildCoboundary R A M n) φ)

Matrix extension of cyclic cochains commutes with the Hochschild coboundary.

theorem TauCeti.matrixCyclicCochainExtension_mem_cyclicCocycles {R : Type u_4} {A : Type u_5} {M : Type u_6} [AddCommGroup M] {ι : Type u_7} [Fintype ι] {n : ℕ} [Semiring R] [Module R M] [SMulCommClass R R M] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {φ : ↥(cyclicCochains R A M n)} (hφ : φ ∈ cyclicCocycles R A M n) : (matrixCyclicCochainExtension ι n) φ ∈ cyclicCocycles R (Matrix ι ι A) M n

Matrix extension maps cyclic cocycles to cyclic cocycles.

theorem TauCeti.matrixCyclicCochainExtension_mem_cyclicCoboundaries {R : Type u_4} {A : Type u_5} {M : Type u_6} [AddCommGroup M] {ι : Type u_7} [Fintype ι] {n : ℕ} [Semiring R] [Module R M] [SMulCommClass R R M] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {φ : ↥(cyclicCochains R A M n)} (hφ : φ ∈ cyclicCoboundaries R A M n) : (matrixCyclicCochainExtension ι n) φ ∈ cyclicCoboundaries R (Matrix ι ι A) M n

Matrix extension maps cyclic coboundaries to cyclic coboundaries.

noncomputable def TauCeti.cyclicCohomology.matrixExtension {R : Type u_4} {A : Type u_5} (M : Type u_6) [AddCommGroup M] (ι : Type u_7) [Fintype ι] (n : ℕ) [CommRing R] [Module R M] [Ring A] [Algebra R A] [DecidableEq ι] : ↑(cyclicCohomology R A M n) →ₗ[R] ↑(cyclicCohomology R (Matrix ι ι A) M n)

The map HCⁿ(A; M) → HCⁿ(Matrix ι ι A; M) on cyclic cohomology induced by matrix extension of cyclic cocycles.

@[simp]

theorem TauCeti.cyclicCohomology.matrixExtension_mk {R : Type u_4} {A : Type u_5} {M : Type u_6} [AddCommGroup M] {ι : Type u_7} [Fintype ι] {n : ℕ} [CommRing R] [Module R M] [Ring A] [Algebra R A] [DecidableEq ι] (φ : ↥(cyclicCocycles R A M n)) : (matrixExtension M ι n) ((mk R A M n) φ) = (mk R (Matrix ι ι A) M n) ⟨(matrixCyclicCochainExtension ι n) ↑φ, ⋯⟩

The induced map sends the class of a cyclic cocycle to the class of its matrix extension.

theorem TauCeti.cyclicCohomology.matrixExtension_map {R : Type u_4} {A : Type u_5} {M : Type u_6} [AddCommGroup M] {ι : Type u_7} [Fintype ι] {n : ℕ} [CommRing R] [Module R M] [Ring A] [Algebra R A] [DecidableEq ι] {B : Type u_5} [Ring B] [Algebra R B] (f : A →ₐ[R] B) (c : ↑(cyclicCohomology R B M n)) : (matrixExtension M ι n) ((CategoryTheory.ConcreteCategory.hom (map M (NonUnitalAlgHomClass.toNonUnitalAlgHom f) n)) c) = (CategoryTheory.ConcreteCategory.hom (map M (NonUnitalAlgHomClass.toNonUnitalAlgHom f.mapMatrix) n)) ((matrixExtension M ι n) c)

Matrix extension is natural: it commutes with pullback along an algebra homomorphism f : A →ₐ[R] B and along its entrywise extension Matrix ι ι A →ₐ[R] Matrix ι ι B.

theorem TauCeti.matrixCochainExtension_cyclicOperator {R : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (ι : Type u_7) [Fintype ι] (n : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (matrixCochainExtension ι n) ((cyclicOperator R A M n) φ) = (cyclicOperator R (Matrix ι ι A) M n) ((matrixCochainExtension ι n) φ)

Matrix extension commutes with the cyclic operator.

theorem TauCeti.matrixCochainExtension_cyclicNorm {R : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (ι : Type u_7) [Fintype ι] (n : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (matrixCochainExtension ι n) ((cyclicNorm R A M n) φ) = (cyclicNorm R (Matrix ι ι A) M n) ((matrixCochainExtension ι n) φ)

Matrix extension commutes with the cyclic norm.

theorem TauCeti.matrixCochainExtension_barContraction {R : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring R] [AddCommMonoid A] [One A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (ι : Type u_7) [Fintype ι] [DecidableEq ι] (n : ℕ) (φ : (Fin (n + 2) → A) →ₘₗ[R] M) : (matrixCochainExtension ι n) ((barContraction R A M n) φ) = (barContraction R (Matrix ι ι A) M n) ((matrixCochainExtension ι (n + 1)) φ)

Matrix extension commutes with insertion of the unit in the first cochain argument.

theorem TauCeti.matrixCochainExtension_connesB {R : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring R] [AddCommMonoid A] [One A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (ι : Type u_7) [Fintype ι] [DecidableEq ι] (n : ℕ) (φ : (Fin (n + 2) → A) →ₘₗ[R] M) : (matrixCochainExtension ι n) ((connesB R A M n) φ) = (connesB R (Matrix ι ι A) M n) ((matrixCochainExtension ι (n + 1)) φ)

Matrix extension commutes with Connes' operator B.