Split exactness of the rows of the cyclic bicomplex

In degree n, write λ for the signed cyclic operator and N = 1 + λ + ⋯ + λⁿ. When n + 1 is invertible in the commutative coefficient semiring, averaging gives a projection P = N / (n + 1) onto the cyclic cochains. The operator H = (∑ j ≤ n, ∑ k < j, λᵏ) / (n + 1) satisfies (1 - λ) H = H (1 - λ) = 1 - P.

Consequently the row alternating between 1 - λ and N is exact at both kinds of terms: range N = ker (1 - λ) and range (1 - λ) = ker N. These explicit splittings are used to compare the cyclic cochain complex with the total cyclic bicomplex. No multiplication or unit on the argument module is needed for these horizontal identities.

References

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

noncomputable def TauCeti.cyclicAverage (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] (n : ℕ) [Invertible (↑n + 1)] : Module.End R ((Fin (n + 1) → A) →ₘₗ[R] M)

Averaging over cyclic rotations projects onto the cyclic cochains.

theorem TauCeti.cyclicAverage_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (cyclicAverage R A M n) φ = ⅟(↑n + 1) • (cyclicNorm R A M n) φ

The cyclic average is the cyclic norm divided by the number of arguments.

theorem TauCeti.cyclicAverage_mem_cyclicCochains {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (cyclicAverage R A M n) φ ∈ cyclicCochains R A M n

Averaging takes values in the cyclic cochains.

theorem TauCeti.cyclicAverage_apply_of_mem_cyclicCochains {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] {φ : (Fin (n + 1) → A) →ₘₗ[R] M} (hφ : φ ∈ cyclicCochains R A M n) : (cyclicAverage R A M n) φ = φ

Averaging fixes every cyclic cochain.

@[simp]

theorem TauCeti.cyclicAverage_cyclicAverage {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (cyclicAverage R A M n) ((cyclicAverage R A M n) φ) = (cyclicAverage R A M n) φ

The cyclic average is idempotent.

theorem TauCeti.isIdempotentElem_cyclicAverage {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] : IsIdempotentElem (cyclicAverage R A M n)

The cyclic average is an idempotent endomorphism.

@[simp]

theorem TauCeti.cyclicAverage_mul_cyclicAverage {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] : cyclicAverage R A M n * cyclicAverage R A M n = cyclicAverage R A M n

The cyclic average absorbs itself under composition.

@[simp]

theorem TauCeti.cyclicOperator_mul_cyclicAverage {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] : cyclicOperator R A M n * cyclicAverage R A M n = cyclicAverage R A M n

The cyclic average absorbs the cyclic operator on the left: λ P = P.

@[simp]

theorem TauCeti.cyclicAverage_mul_cyclicOperator {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] : cyclicAverage R A M n * cyclicOperator R A M n = cyclicAverage R A M n

The cyclic average absorbs the cyclic operator on the right: P λ = P.

@[simp]

theorem TauCeti.ker_cyclicAverage {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] : LinearMap.ker (cyclicAverage R A M n) = LinearMap.ker (cyclicNorm R A M n)

Averaging and the cyclic norm have the same kernel.

theorem TauCeti.range_cyclicAverage {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] : LinearMap.range (cyclicAverage R A M n) = cyclicCochains R A M n

The image of averaging is exactly the cyclic cochains.

noncomputable def TauCeti.cyclicRowHomotopy (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] (n : ℕ) [Invertible (↑n + 1)] : Module.End R ((Fin (n + 1) → A) →ₘₗ[R] M)

The cyclic row homotopy. Its product with 1 - λ on either side is 1 - P, where P is cyclic averaging.

theorem TauCeti.cyclicRowHomotopy_def (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] (n : ℕ) [Invertible (↑n + 1)] : cyclicRowHomotopy R A M n = ⅟(↑n + 1) • ∑ j ∈ Finset.range (n + 1), ∑ k ∈ Finset.range j, cyclicOperator R A M n ^ k

The explicit finite-sum formula for the cyclic row homotopy.

theorem TauCeti.one_sub_cyclicOperator_mul_cyclicRowHomotopy {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] : (1 - cyclicOperator R A M n) * cyclicRowHomotopy R A M n = 1 - cyclicAverage R A M n

The row homotopy splits 1 - λ on the left, up to the cyclic projection.

theorem TauCeti.cyclicRowHomotopy_mul_one_sub_cyclicOperator {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] : cyclicRowHomotopy R A M n * (1 - cyclicOperator R A M n) = 1 - cyclicAverage R A M n

The row homotopy splits 1 - λ on the right, up to the cyclic projection.

theorem TauCeti.one_sub_cyclicOperator_apply_cyclicRowHomotopy {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (1 - cyclicOperator R A M n) ((cyclicRowHomotopy R A M n) φ) = φ - (cyclicAverage R A M n) φ

Applying the row homotopy gives a preimage of φ - P φ under 1 - λ.

theorem TauCeti.range_cyclicNorm {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] : LinearMap.range (cyclicNorm R A M n) = cyclicCochains R A M n

The cyclic norm surjects onto the cyclic cochains.

theorem TauCeti.range_cyclicNorm_eq_ker_one_sub_cyclicOperator {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] : LinearMap.range (cyclicNorm R A M n) = (1 - cyclicOperator R A M n).ker

Exactness of a cyclic-bicomplex row at a term following N.

theorem TauCeti.range_one_sub_cyclicOperator_eq_ker_cyclicNorm {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} [Invertible (↑n + 1)] : (1 - cyclicOperator R A M n).range = LinearMap.ker (cyclicNorm R A M n)

Exactness of a cyclic-bicomplex row at a term following 1 - λ. For a cochain killed by N, the row homotopy gives an explicit preimage.