The character of a cycle

Connes' cycles are the geometric source of cyclic cocycles. A cycle of dimension n over an algebra A consists of a differential graded algebra (Ω, d), a closed graded trace ∫ : Ωⁿ → M and a homomorphism ρ : A → Ω⁰. Its character is the cochain

τ(a₀, …, aₙ) = ∫ ρ(a₀) dρ(a₁) ⋯ dρ(aₙ),

and this file proves that it is a cyclic cocycle: the graded trace property together with closedness gives the cyclic symmetry τ(aₙ, a₀, …, aₙ₋₁) = (-1)ⁿ τ(a₀, …, aₙ), and the Leibniz rule in degree zero together with the trace property gives bτ = 0.

The graded algebra Ω is unital, with its grading stored internally as for TauCeti.IsDGAlgebra. The algebra A may be nonunital, and ρ is a homomorphism of nonunital algebras: even when A has a unit, ρ need not preserve it. This is needed, for instance, to realize the cyclic cocycle (a, b, c) ↦ abc on ℂ, which is nonzero on (1, 1, 1), by universal forms over the forced unitization.

The trace is a linear functional ∫ : Ω → M on the whole algebra, of which only the restriction to degree n is constrained: closedness asks ∫ dω = 0 for ω of degree n - 1, and the graded trace property ∫ xy = (-1) ^ (pq) ∫ yx is asked for x of degree p and y of degree q with p + q = n. Composing a functional on Ωⁿ with the projection to degree n gives such a map.

The Ω-valued cochain (a₀, …, aₙ) ↦ ρ(a₀) dρ(a₁) ⋯ dρ(aₙ) is TauCeti.cycleForm. Its bar coboundary is (-1)ⁿ ρ(a₀) dρ(a₁) ⋯ dρ(aₙ) ρ(aₙ₊₁), which is the algebraic heart of the cocycle identity.

Main definitions

• TauCeti.IsClosedGradedTrace: a closed graded trace of dimension n on a graded algebra with a differential.
• TauCeti.cycleForm: the cochain (a₀, …, aₙ) ↦ ρ(a₀) dρ(a₁) ⋯ dρ(aₙ) with values in Ω.
• TauCeti.cycleCharacter: the character (a₀, …, aₙ) ↦ ∫ ρ(a₀) dρ(a₁) ⋯ dρ(aₙ) of a cycle.
• TauCeti.cycleCocycle: the character of a cycle, as a cyclic cocycle.

Main results

• TauCeti.barCoboundary_cycleForm: the bar coboundary of TauCeti.cycleForm.
• TauCeti.cycleCharacter_mem_cyclicCochains: the character of a cycle is a cyclic cochain.
• TauCeti.hochschildCoboundary_cycleCharacter_apply: the Hochschild coboundary of the character measures the failure of τ to commute with zero-forms.
• TauCeti.hochschildCoboundary_cycleCharacter: the character of a cycle is a Hochschild cocycle.
• TauCeti.cycleCharacter_comp: the character of the cycle pulled back along a homomorphism is the pulled-back character.
• TauCeti.cycleCocycle_comp: the same naturality for the character as a cyclic cocycle.

References

• A. Connes, Noncommutative Geometry, Chapter III, §1 (cycles and their characters).
• A. Connes, Noncommutative differential geometry, Publ. Math. IHÉS 62 (1985), Part II, §1.

Closed graded traces

structure TauCeti.IsClosedGradedTrace {R : Type u_1} {Ω : Type u_3} {M : Type u_4} [CommRing R] [Ring Ω] [Algebra R Ω] [AddCommGroup M] [Module R M] (𝒜 : ℤ → Submodule R Ω) (d : Ω →ₗ[R] Ω) (n : ℕ) (τ : Ω →ₗ[R] M) : Prop

A closed graded trace of dimension n on the graded algebra 𝒜 with differential d: a linear map τ which vanishes on the differentials of elements of degree n - 1 and satisfies τ (x * y) = (-1) ^ (p q) τ (y * x) for x of degree p and y of degree q with p + q = n. Only the restriction of τ to degree n is constrained.

• map_map_eq_zero {x : Ω} : x ∈ 𝒜 (↑n - 1) → τ (d x) = 0

  The trace vanishes on exact forms of top degree.

• map_mul_comm {p q : ℤ} {x y : Ω} : x ∈ 𝒜 p → y ∈ 𝒜 q → p + q = ↑n → τ (x * y) = (p * q).negOnePow • τ (y * x)

  The graded trace property in total degree n.

theorem TauCeti.IsClosedGradedTrace.map_mul_comm_of_mem_zero {R : Type u_1} {Ω : Type u_3} {M : Type u_4} [CommRing R] [Ring Ω] [Algebra R Ω] [AddCommGroup M] [Module R M] {𝒜 : ℤ → Submodule R Ω} {d : Ω →ₗ[R] Ω} {n : ℕ} {τ : Ω →ₗ[R] M} (hτ : IsClosedGradedTrace 𝒜 d n τ) {x y : Ω} (hx : x ∈ 𝒜 0) (hy : y ∈ 𝒜 ↑n) : τ (x * y) = τ (y * x)

A closed graded trace commutes with a factor of degree zero.

The forms ρ(a₀) dρ(a₁) ⋯ dρ(aₙ)

def TauCeti.cycleForm {R : Type u_1} {A : Type u_2} {Ω : Type u_3} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] (d : Ω →ₗ[R] Ω) (ρ : A →ₙₐ[R] Ω) (n : ℕ) : (Fin (n + 1) → A) →ₘₗ[R] Ω

The Ω-valued n-cochain (a₀, …, aₙ) ↦ ρ(a₀) dρ(a₁) ⋯ dρ(aₙ) of a cycle.

theorem TauCeti.cycleForm_apply {R : Type u_1} {A : Type u_2} {Ω : Type u_3} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] {d : Ω →ₗ[R] Ω} {ρ : A →ₙₐ[R] Ω} {n : ℕ} (a : Fin (n + 1) → A) : (cycleForm d ρ n) a = ρ (a 0) * (List.ofFn fun (i : Fin n) => d (ρ (a i.succ))).prod

The defining formula ρ(a₀) dρ(a₁) ⋯ dρ(aₙ).

@[simp]

theorem TauCeti.cycleForm_zero_apply {R : Type u_1} {A : Type u_2} {Ω : Type u_3} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] {d : Ω →ₗ[R] Ω} {ρ : A →ₙₐ[R] Ω} (a : Fin 1 → A) : (cycleForm d ρ 0) a = ρ (a 0)

In degree zero the form is ρ(a₀).

theorem TauCeti.cycleForm_succ_apply {R : Type u_1} {A : Type u_2} {Ω : Type u_3} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] {d : Ω →ₗ[R] Ω} {ρ : A →ₙₐ[R] Ω} {n : ℕ} (a : Fin (n + 2) → A) : (cycleForm d ρ (n + 1)) a = (cycleForm d ρ n) (Fin.init a) * d (ρ (a (Fin.last (n + 1))))

The form of degree n + 1 is that of degree n on the first arguments, multiplied on the right by dρ(aₙ₊₁).

theorem TauCeti.cycleForm_comp {R : Type u_1} {A : Type u_2} {Ω : Type u_3} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] {d : Ω →ₗ[R] Ω} {ρ : A →ₙₐ[R] Ω} {n : ℕ} {B : Type u_5} [NonUnitalSemiring B] [Module R B] (f : B →ₙₐ[R] A) : cycleForm d (ρ.comp f) n = (cycleForm d ρ n).compLinearMap fun (x : Fin (n + 1)) => ↑f

Pulling the form back along a homomorphism f gives the form of ρ ∘ f.

theorem TauCeti.cycleForm_mem {R : Type u_1} {A : Type u_2} {Ω : Type u_3} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] {d : Ω →ₗ[R] Ω} {ρ : A →ₙₐ[R] Ω} {n : ℕ} {𝒜 : ℤ → Submodule R Ω} [GradedAlgebra 𝒜] (hd : IsDGAlgebra 𝒜 d) (hρ : ∀ (a : A), ρ a ∈ 𝒜 0) (a : Fin (n + 1) → A) : (cycleForm d ρ n) a ∈ 𝒜 ↑n

The form ρ(a₀) dρ(a₁) ⋯ dρ(aₙ) has degree n.

theorem TauCeti.map_cycleForm {R : Type u_1} {A : Type u_2} {Ω : Type u_3} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] {d : Ω →ₗ[R] Ω} {ρ : A →ₙₐ[R] Ω} {n : ℕ} {𝒜 : ℤ → Submodule R Ω} [GradedAlgebra 𝒜] (hd : IsDGAlgebra 𝒜 d) (a : Fin (n + 1) → A) : d ((cycleForm d ρ n) a) = (List.ofFn fun (i : Fin (n + 1)) => d (ρ (a i))).prod

The differential of ρ(a₀) dρ(a₁) ⋯ dρ(aₙ) is dρ(a₀) dρ(a₁) ⋯ dρ(aₙ).

theorem TauCeti.barCoboundary_cycleForm {R : Type u_1} {A : Type u_2} {Ω : Type u_3} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] {d : Ω →ₗ[R] Ω} {ρ : A →ₙₐ[R] Ω} {n : ℕ} {𝒜 : ℤ → Submodule R Ω} [GradedAlgebra 𝒜] [IsScalarTower R A A] [SMulCommClass R A A] (hd : IsDGAlgebra 𝒜 d) (hρ : ∀ (a : A), ρ a ∈ 𝒜 0) (a : Fin (n + 2) → A) : ((barCoboundary R A Ω n) (cycleForm d ρ n)) a = (-1) ^ n • ((cycleForm d ρ n) (Fin.init a) * ρ (a (Fin.last (n + 1))))

The bar coboundary of ρ(a₀) dρ(a₁) ⋯ dρ(aₙ) telescopes to (-1)ⁿ ρ(a₀) dρ(a₁) ⋯ dρ(aₙ) ρ(aₙ₊₁).

The character of a cycle

def TauCeti.cycleCharacter {R : Type u_1} {A : Type u_2} {Ω : Type u_3} {M : Type u_4} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] [AddCommGroup M] [Module R M] (d : Ω →ₗ[R] Ω) (τ : Ω →ₗ[R] M) (ρ : A →ₙₐ[R] Ω) (n : ℕ) : (Fin (n + 1) → A) →ₘₗ[R] M

The character of a cycle: the n-cochain (a₀, …, aₙ) ↦ τ (ρ(a₀) dρ(a₁) ⋯ dρ(aₙ)).

@[simp]

theorem TauCeti.cycleCharacter_apply {R : Type u_1} {A : Type u_2} {Ω : Type u_3} {M : Type u_4} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] [AddCommGroup M] [Module R M] {d : Ω →ₗ[R] Ω} {τ : Ω →ₗ[R] M} {ρ : A →ₙₐ[R] Ω} {n : ℕ} (a : Fin (n + 1) → A) : (cycleCharacter d τ ρ n) a = τ ((cycleForm d ρ n) a)

The character evaluates the trace on the form ρ(a₀) dρ(a₁) ⋯ dρ(aₙ).

theorem TauCeti.cycleCharacter_comp {R : Type u_1} {A : Type u_2} {Ω : Type u_3} {M : Type u_4} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] [AddCommGroup M] [Module R M] {d : Ω →ₗ[R] Ω} {τ : Ω →ₗ[R] M} {ρ : A →ₙₐ[R] Ω} {n : ℕ} {B : Type u_5} [NonUnitalSemiring B] [Module R B] (f : B →ₙₐ[R] A) : cycleCharacter d τ (ρ.comp f) n = (cycleCharacter d τ ρ n).compLinearMap fun (x : Fin (n + 1)) => ↑f

The character of the cycle pulled back along a homomorphism f is the pullback of the character along f.

theorem TauCeti.cycleCharacter_mem_cyclicCochains {R : Type u_1} {A : Type u_2} {Ω : Type u_3} {M : Type u_4} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] [AddCommGroup M] [Module R M] {d : Ω →ₗ[R] Ω} {τ : Ω →ₗ[R] M} {ρ : A →ₙₐ[R] Ω} {n : ℕ} {𝒜 : ℤ → Submodule R Ω} [GradedAlgebra 𝒜] (hd : IsDGAlgebra 𝒜 d) (hρ : ∀ (a : A), ρ a ∈ 𝒜 0) (hτ : IsClosedGradedTrace 𝒜 d n τ) : cycleCharacter d τ ρ n ∈ cyclicCochains R A M n

The character of a cycle is a cyclic cochain: τ(aₙ, a₀, …, aₙ₋₁) = (-1)ⁿ τ(a₀, …, aₙ).

theorem TauCeti.hochschildCoboundary_cycleCharacter_apply {R : Type u_1} {A : Type u_2} {Ω : Type u_3} {M : Type u_4} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] [AddCommGroup M] [Module R M] {d : Ω →ₗ[R] Ω} {τ : Ω →ₗ[R] M} {ρ : A →ₙₐ[R] Ω} {n : ℕ} {𝒜 : ℤ → Submodule R Ω} [GradedAlgebra 𝒜] [IsScalarTower R A A] [SMulCommClass R A A] (hd : IsDGAlgebra 𝒜 d) (hρ : ∀ (a : A), ρ a ∈ 𝒜 0) (a : Fin (n + 2) → A) : ((hochschildCoboundary R A M n) (cycleCharacter d τ ρ n)) a = (-1) ^ n • (τ ((cycleForm d ρ n) (Fin.init a) * ρ (a (Fin.last (n + 1)))) - τ (ρ (a (Fin.last (n + 1))) * (cycleForm d ρ n) (Fin.init a)))

The Hochschild coboundary of the character of a cycle, for an arbitrary functional τ: (bτ)(a₀, …, aₙ₊₁) = (-1)ⁿ (τ(X ρ(aₙ₊₁)) - τ(ρ(aₙ₊₁) X)) with X = ρ(a₀) dρ(a₁) ⋯ dρ(aₙ).

theorem TauCeti.hochschildCoboundary_cycleCharacter {R : Type u_1} {A : Type u_2} {Ω : Type u_3} {M : Type u_4} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] [AddCommGroup M] [Module R M] {d : Ω →ₗ[R] Ω} {τ : Ω →ₗ[R] M} {ρ : A →ₙₐ[R] Ω} {n : ℕ} {𝒜 : ℤ → Submodule R Ω} [GradedAlgebra 𝒜] [IsScalarTower R A A] [SMulCommClass R A A] (hd : IsDGAlgebra 𝒜 d) (hρ : ∀ (a : A), ρ a ∈ 𝒜 0) (hτ : IsClosedGradedTrace 𝒜 d n τ) : (hochschildCoboundary R A M n) (cycleCharacter d τ ρ n) = 0

The character of a cycle is a Hochschild cocycle.

def TauCeti.cycleCocycle {R : Type u_1} {A : Type u_2} {Ω : Type u_3} {M : Type u_4} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] [AddCommGroup M] [Module R M] {d : Ω →ₗ[R] Ω} {τ : Ω →ₗ[R] M} {ρ : A →ₙₐ[R] Ω} {n : ℕ} {𝒜 : ℤ → Submodule R Ω} [GradedAlgebra 𝒜] [IsScalarTower R A A] [SMulCommClass R A A] (hd : IsDGAlgebra 𝒜 d) (hρ : ∀ (a : A), ρ a ∈ 𝒜 0) (hτ : IsClosedGradedTrace 𝒜 d n τ) : ↥(cyclicCocycles R A M n)

The character of a cycle, as a cyclic cocycle.

@[simp]

theorem TauCeti.coe_cycleCocycle {R : Type u_1} {A : Type u_2} {Ω : Type u_3} {M : Type u_4} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] [AddCommGroup M] [Module R M] {d : Ω →ₗ[R] Ω} {τ : Ω →ₗ[R] M} {ρ : A →ₙₐ[R] Ω} {n : ℕ} {𝒜 : ℤ → Submodule R Ω} [GradedAlgebra 𝒜] [IsScalarTower R A A] [SMulCommClass R A A] (hd : IsDGAlgebra 𝒜 d) (hρ : ∀ (a : A), ρ a ∈ 𝒜 0) (hτ : IsClosedGradedTrace 𝒜 d n τ) : ↑↑(cycleCocycle hd hρ hτ) = cycleCharacter d τ ρ n

The underlying cochain of the cyclic cocycle of a cycle is its character.

theorem TauCeti.cycleCocycle_comp {R : Type u_1} {A : Type u_2} {Ω : Type u_3} {M : Type u_4} [CommRing R] [NonUnitalSemiring A] [Module R A] [Ring Ω] [Algebra R Ω] [AddCommGroup M] [Module R M] {d : Ω →ₗ[R] Ω} {τ : Ω →ₗ[R] M} {ρ : A →ₙₐ[R] Ω} {n : ℕ} {𝒜 : ℤ → Submodule R Ω} [GradedAlgebra 𝒜] [IsScalarTower R A A] [SMulCommClass R A A] {B : Type u_5} [NonUnitalSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : B →ₙₐ[R] A) (hd : IsDGAlgebra 𝒜 d) (hρ : ∀ (a : A), ρ a ∈ 𝒜 0) (hτ : IsClosedGradedTrace 𝒜 d n τ) : ↑(cycleCocycle hd ⋯ hτ) = (cyclicCochainsMap M (↑f) n) ↑(cycleCocycle hd hρ hτ)

The cyclic cocycle of the cycle pulled back along a homomorphism f is the pullback of the cyclic cocycle along f.