The cyclic operator, the bar coboundary and Connes' operator B

For an R-algebra A and an R-module M, this file constructs the operators on the M-valued multilinear cochains Cⁿ of A from which Connes' cyclic bicomplex and the (b, B) mixed complex are built:

• the cyclic operator λ : Cⁿ → Cⁿ, (λφ)(a₀, …, aₙ) = (-1)ⁿ φ(aₙ, a₀, …, aₙ₋₁), whose fixed points are the cyclic cochains and which satisfies λⁿ⁺¹ = 1;
• the cyclic norm N = 1 + λ + ⋯ + λⁿ;
• the bar coboundary b' : Cⁿ → Cⁿ⁺¹, the alternating sum of all Hochschild cofaces but the last one;
• for unital A, the contraction s : Cⁿ⁺¹ → Cⁿ, (sφ)(a₀, …, aₙ) = φ(1, a₀, …, aₙ), of the bar complex;
• Connes' operator B = N s (1 - λ) : Cⁿ⁺¹ → Cⁿ.

The identities (1 - λ) b = b' (1 - λ) and b N = N b' are the commutation relations of the cyclic bicomplex, whose columns alternate between b and -b' and whose rows alternate between 1 - λ and N. Together with b' s + s b' = 1 they give B ∘ B = 0 and b B + B b = 0, so that (C*, b, B) is a mixed complex. These are the cochain (transposed) forms of the chain-level identities in Loday's book; for example B is the transpose of (1 - t) s N. The operator B vanishes on cyclic cochains and takes values in them.

The bicomplex identities hold for nonunital and nonassociative A; among the results here only b' ∘ b' = 0 uses associativity, and the identities for B only use that 1 is a left unit.

Main definitions

• TauCeti.cyclicOperator: the cyclic operator λ.
• TauCeti.cyclicNorm: the cyclic norm N.
• TauCeti.barCoboundary: the bar coboundary b'.
• TauCeti.barContraction: the contraction s of the bar complex of a unital algebra.
• TauCeti.connesB: Connes' operator B.

Main results

• TauCeti.cyclicOperator_pow_eq_one: λⁿ⁺¹ = 1.
• TauCeti.mem_cyclicCochains_iff_cyclicOperator_apply_eq_self: the cyclic cochains are the fixed points of λ.
• TauCeti.barCoboundary_barCoboundary: b' ∘ b' = 0.
• TauCeti.one_sub_cyclicOperator_comp_hochschildCoboundary: (1 - λ) b = b' (1 - λ).
• TauCeti.hochschildCoboundary_comp_cyclicNorm: b N = N b'.
• TauCeti.barCoboundary_comp_barContraction_add_barContraction_comp_barCoboundary: b' s + s b' = 1.
• TauCeti.connesB_comp_connesB: B ∘ B = 0.
• TauCeti.hochschildCoboundary_comp_connesB_add_connesB_comp_hochschildCoboundary: b B + B b = 0.
• TauCeti.connesB_hochschildCoboundary_zero: B b = 0 on degree-zero cochains.

References

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

The cyclic operator and the cyclic norm

def TauCeti.cyclicOperator (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : Module.End R ((Fin (n + 1) → A) →ₘₗ[R] M)

The cyclic operator λ on n-cochains, (λφ)(a₀, …, aₙ) = (-1)ⁿ φ(aₙ, a₀, …, aₙ₋₁).

@[simp]

theorem TauCeti.cyclicOperator_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (a : Fin (n + 1) → A) : ((cyclicOperator R A M n) φ) a = (-1) ^ n • φ (a ∘ ⇑(Equiv.symm (finRotate (n + 1))))

The cyclic operator rotates the arguments cyclically and multiplies by (-1)ⁿ.

theorem TauCeti.cyclicOperator_pow_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (k : ℕ) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (a : Fin (n + 1) → A) : ((cyclicOperator R A M n ^ k) φ) a = (-1) ^ (n * k) • φ (a ∘ ⇑(Equiv.symm (finRotate (n + 1) ^ k)))

The powers of the cyclic operator: (λᵏφ)(a) = (-1)ⁿᵏ φ(a ∘ t⁻ᵏ) for the cyclic rotation t of the arguments.

theorem TauCeti.cyclicOperator_pow_eq_one {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : cyclicOperator R A M n ^ (n + 1) = 1

The cyclic operator on n-cochains has order dividing n + 1.

theorem TauCeti.mem_cyclicCochains_iff_cyclicOperator_apply_eq_self {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} {φ : (Fin (n + 1) → A) →ₘₗ[R] M} : φ ∈ cyclicCochains R A M n ↔ (cyclicOperator R A M n) φ = φ

The cyclic cochains are the fixed points of the cyclic operator.

def TauCeti.cyclicNorm (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : Module.End R ((Fin (n + 1) → A) →ₘₗ[R] M)

The cyclic norm N = 1 + λ + ⋯ + λⁿ on n-cochains.

theorem TauCeti.cyclicNorm_def (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : cyclicNorm R A M n = ∑ k ∈ Finset.range (n + 1), cyclicOperator R A M n ^ k

The cyclic norm is the sum of the powers λᵏ, k ≤ n, of the cyclic operator.

theorem TauCeti.cyclicNorm_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (a : Fin (n + 1) → A) : ((cyclicNorm R A M n) φ) a = ∑ k ∈ Finset.range (n + 1), (-1) ^ (n * k) • φ (a ∘ ⇑(Equiv.symm (finRotate (n + 1) ^ k)))

The cyclic norm evaluates as the signed sum of φ over the cyclic rotations of the arguments.

@[simp]

theorem TauCeti.cyclicOperator_mul_cyclicNorm {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} : cyclicOperator R A M n * cyclicNorm R A M n = cyclicNorm R A M n

The cyclic norm absorbs the cyclic operator on the left: λ N = N.

@[simp]

theorem TauCeti.cyclicNorm_mul_cyclicOperator {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} : cyclicNorm R A M n * cyclicOperator R A M n = cyclicNorm R A M n

The cyclic norm absorbs the cyclic operator on the right: N λ = N.

@[simp]

theorem TauCeti.cyclicOperator_pow_mul_cyclicNorm {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (k : ℕ) : cyclicOperator R A M n ^ k * cyclicNorm R A M n = cyclicNorm R A M n

The cyclic norm absorbs every power of the cyclic operator on the left.

@[simp]

theorem TauCeti.cyclicNorm_mul_cyclicOperator_pow {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (k : ℕ) : cyclicNorm R A M n * cyclicOperator R A M n ^ k = cyclicNorm R A M n

The cyclic norm absorbs every power of the cyclic operator on the right.

theorem TauCeti.cyclicNorm_mem_cyclicCochains {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (cyclicNorm R A M n) φ ∈ cyclicCochains R A M n

The cyclic norm of any cochain is a cyclic cochain.

theorem TauCeti.cyclicNorm_apply_of_mem_cyclicCochains {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} {φ : (Fin (n + 1) → A) →ₘₗ[R] M} (hφ : φ ∈ cyclicCochains R A M n) : (cyclicNorm R A M n) φ = (↑n + 1) • φ

On a cyclic cochain, the cyclic norm is multiplication by the number of arguments.

theorem TauCeti.ker_one_sub_cyclicOperator {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} : (1 - cyclicOperator R A M n).ker = cyclicCochains R A M n

The fixed-point submodule of the cyclic operator is the kernel of 1 - λ.

Hochschild faces of tuples starting with a given entry

theorem TauCeti.hochschildFace_zero_cons_one {A : Type u_1} {n : ℕ} [MulOneClass A] (a : Fin (n + 1) → A) : hochschildFace 0 (Fin.cons 1 a) = a

The zeroth Hochschild face of (1, a₀, …, aₙ) is (a₀, …, aₙ).

theorem TauCeti.hochschildFace_succ_castSucc_cons {A : Type u_1} {n : ℕ} [Mul A] (i : Fin (n + 1)) (x : A) (a : Fin (n + 2) → A) : hochschildFace i.succ.castSucc (Fin.cons x a) = Fin.cons x (hochschildFace i.castSucc a)

A Hochschild face other than the last one of (x, a₀, …, aₙ₊₁) is x followed by the previous face of (a₀, …, aₙ₊₁).

The cyclic operator and the Hochschild cofaces

theorem TauCeti.cyclicOperator_hochschildCoface_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (cyclicOperator R A M (n + 1)) ((hochschildCoface R A M 0) φ) = (-1) ^ (n + 1) • (hochschildCoface R A M (Fin.last (n + 1))) φ

The cyclic operator turns the zeroth coface into the last one: λ (δ₀ φ) = (-1)ⁿ⁺¹ δₙ₊₁ φ.

theorem TauCeti.cyclicOperator_hochschildCoface_succ {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (i : Fin (n + 1)) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (cyclicOperator R A M (n + 1)) ((hochschildCoface R A M i.succ) φ) = -(hochschildCoface R A M i.castSucc) ((cyclicOperator R A M n) φ)

The cyclic operator moves the cofaces down: λ (δᵢ₊₁ φ) = -δᵢ (λ φ).

theorem TauCeti.cyclicOperator_pow_hochschildCoface {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (k : ℕ) (hk : k < n + 2) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (cyclicOperator R A M (n + 1) ^ k) ((hochschildCoface R A M ⟨k, hk⟩) φ) = (-1) ^ k • (hochschildCoface R A M 0) ((cyclicOperator R A M n ^ k) φ)

The k-th power of the cyclic operator moves the k-th coface to the zeroth one: λᵏ (δₖ φ) = (-1)ᵏ δ₀ (λᵏ φ).

The bar coboundary and the cyclic bicomplex

def TauCeti.barCoboundary (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : ((Fin (n + 1) → A) →ₘₗ[R] M) →ₗ[R] (Fin (n + 2) → A) →ₘₗ[R] M

The bar coboundary b' : Cⁿ → Cⁿ⁺¹, the alternating sum ∑_{i ≤ n} (-1)ⁱ δᵢ of the Hochschild cofaces other than the last one.

@[simp]

theorem TauCeti.barCoboundary_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (a : Fin (n + 2) → A) : ((barCoboundary R A M n) φ) a = ∑ j : Fin (n + 1), (-1) ^ ↑j • φ (j.castSucc.contractNth (fun (x1 x2 : A) => x1 * x2) a)

The bar coboundary evaluates as the alternating sum of φ on the contractions of adjacent entries, (b'φ)(a₀, …, aₙ₊₁) = ∑_{j ≤ n} (-1)ʲ φ(a₀, …, aⱼaⱼ₊₁, …, aₙ₊₁).

theorem TauCeti.hochschildCoboundary_eq_barCoboundary_add {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (hochschildCoboundary R A M n) φ = (barCoboundary R A M n) φ + (-1) ^ (n + 1) • (hochschildCoface R A M (Fin.last (n + 1))) φ

The Hochschild coboundary is the bar coboundary plus the signed last coface.

theorem TauCeti.cyclicOperator_hochschildCoboundary {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (cyclicOperator R A M (n + 1)) ((hochschildCoboundary R A M n) φ) = (barCoboundary R A M n) ((cyclicOperator R A M n) φ) + (-1) ^ (n + 1) • (hochschildCoface R A M (Fin.last (n + 1))) φ

Conjugating the Hochschild coboundary by the cyclic operator gives the bar coboundary up to the last coface: λ (b φ) = b' (λ φ) + (-1)ⁿ⁺¹ δₙ₊₁ φ.

theorem TauCeti.one_sub_cyclicOperator_comp_hochschildCoboundary (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : (1 - cyclicOperator R A M (n + 1)) ∘ₗ hochschildCoboundary R A M n = barCoboundary R A M n ∘ₗ (1 - cyclicOperator R A M n)

The first commutation relation of the cyclic bicomplex: (1 - λ) b = b' (1 - λ).

theorem TauCeti.hochschildCoboundary_comp_cyclicNorm (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : hochschildCoboundary R A M n ∘ₗ cyclicNorm R A M n = cyclicNorm R A M (n + 1) ∘ₗ barCoboundary R A M n

The second commutation relation of the cyclic bicomplex: b N = N b'.

@[simp]

theorem TauCeti.barCoboundary_barCoboundary {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 1) → A) →ₘₗ[R] M) : (barCoboundary R A M (n + 1)) ((barCoboundary R A M n) φ) = 0

The bar coboundary squares to zero.

The contraction of the bar complex and Connes' operator B

def TauCeti.barContraction (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [One A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : ((Fin (n + 2) → A) →ₘₗ[R] M) →ₗ[R] (Fin (n + 1) → A) →ₘₗ[R] M

The contraction s : Cⁿ⁺¹ → Cⁿ of the bar complex, (sφ)(a₀, …, aₙ) = φ(1, a₀, …, aₙ).

@[simp]

theorem TauCeti.barContraction_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [One A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 2) → A) →ₘₗ[R] M) (a : Fin (n + 1) → A) : ((barContraction R A M n) φ) a = φ (Fin.cons 1 a)

The contraction evaluates φ with 1 inserted as the zeroth argument.

def TauCeti.connesB (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [One A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : ((Fin (n + 2) → A) →ₘₗ[R] M) →ₗ[R] (Fin (n + 1) → A) →ₘₗ[R] M

Connes' operator B = N s (1 - λ) : Cⁿ⁺¹ → Cⁿ on the cochains of a unital algebra.

theorem TauCeti.connesB_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [One A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 2) → A) →ₘₗ[R] M) : (connesB R A M n) φ = (cyclicNorm R A M n) ((barContraction R A M n) (φ - (cyclicOperator R A M (n + 1)) φ))

Connes' operator evaluates as B φ = N (s (φ - λ φ)).

theorem TauCeti.connesB_mem_cyclicCochains {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [One A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 2) → A) →ₘₗ[R] M) : (connesB R A M n) φ ∈ cyclicCochains R A M n

Connes' operator B takes values in the cyclic cochains.

theorem TauCeti.connesB_eq_zero_of_mem_cyclicCochains {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [One A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} {φ : (Fin (n + 2) → A) →ₘₗ[R] M} (hφ : φ ∈ cyclicCochains R A M (n + 1)) : (connesB R A M n) φ = 0

Connes' operator B vanishes on cyclic cochains.

@[simp]

theorem TauCeti.connesB_connesB {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [One A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 3) → A) →ₘₗ[R] M) : (connesB R A M n) ((connesB R A M (n + 1)) φ) = 0

Connes' operator B squares to zero.

theorem TauCeti.connesB_comp_connesB (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [One A] [Module R A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : connesB R A M n ∘ₗ connesB R A M (n + 1) = 0

Connes' operator B squares to zero, as a composite of linear maps.

@[simp]

theorem TauCeti.barContraction_barCoboundary_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (φ : (Fin 1 → A) →ₘₗ[R] M) : (barContraction R A M 0) ((barCoboundary R A M 0) φ) = φ

The contraction s is a contracting homotopy of the bar complex in degree zero: s (b' φ) = φ.

theorem TauCeti.barCoboundary_barContraction_add_barContraction_barCoboundary {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 2) → A) →ₘₗ[R] M) : (barCoboundary R A M n) ((barContraction R A M n) φ) + (barContraction R A M (n + 1)) ((barCoboundary R A M (n + 1)) φ) = φ

The contraction s is a contracting homotopy of the bar complex in positive degrees: b' (s φ) + s (b' φ) = φ.

theorem TauCeti.hochschildCoboundary_connesB_add_connesB_hochschildCoboundary {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (φ : (Fin (n + 2) → A) →ₘₗ[R] M) : (hochschildCoboundary R A M n) ((connesB R A M n) φ) + (connesB R A M (n + 1)) ((hochschildCoboundary R A M (n + 1)) φ) = 0

Connes' operator B anticommutes with the Hochschild coboundary: b (B φ) + B (b φ) = 0.

theorem TauCeti.hochschildCoboundary_comp_connesB_add_connesB_comp_hochschildCoboundary (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (n : ℕ) : hochschildCoboundary R A M n ∘ₗ connesB R A M n + connesB R A M (n + 1) ∘ₗ hochschildCoboundary R A M (n + 1) = 0

Connes' operator B anticommutes with the Hochschild coboundary, as linear maps: b B + B b = 0.

@[simp]

theorem TauCeti.connesB_hochschildCoboundary_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] (φ : (Fin 1 → A) →ₘₗ[R] M) : (connesB R A M 0) ((hochschildCoboundary R A M 0) φ) = 0

The mixed-complex identity at the bottom degree: B (b φ) = 0 for every degree-zero cochain φ.