The Hochschild coboundary and cyclic cochains

For a possibly nonunital and nonassociative R-algebra A and an R-module M, an n-cochain is an R-multilinear map φ : Aⁿ⁺¹ → M. This file constructs the Hochschild coboundary b : Cⁿ → Cⁿ⁺¹, (bφ)(a₀, …, aₙ₊₁) = ∑_{j ≤ n} (-1)ʲ φ(a₀, …, aⱼaⱼ₊₁, …, aₙ₊₁) + (-1)ⁿ⁺¹ φ(aₙ₊₁a₀, a₁, …, aₙ), proves b ∘ b = 0 when the multiplication is associative, and shows that b preserves the cyclic cochains, those with φ(aₙ, a₀, …, aₙ₋₁) = (-1)ⁿ φ(a₀, …, aₙ). For unital A and M = R these are the data from which the Hochschild cochain complex of A with coefficients in its dual A* and Connes' cyclic subcomplex can be assembled; the cyclic complex and its cohomology are constructed in TauCeti.RingTheory.CyclicCohomology.Cohomology. Pulling cochains back along a linear map preserves cyclicity, and pulling back along a homomorphism of nonunital algebras commutes with b.

The coboundary is the alternating sum of the cofaces φ ↦ φ ∘ dᵢ, where dᵢ are face maps on tuples. For unital A, these faces and the rotation are part of the Hochschild cyclic module; in the nonunital setting no degeneracies are provided. The two facts above are consequences of identities between faces and the cyclic rotation t(a₀, …, aₙ₊₁) = (aₙ₊₁, a₀, …, aₙ): the simplicial identity dᵢ ∘ d_{j+1} = d_j ∘ dᵢ for i ≤ j, and d₀ ∘ t = d_{n+1}, d_{i+1} ∘ t = t ∘ dᵢ.

Main definitions

• TauCeti.hochschildFace: the faces dᵢ on tuples.
• TauCeti.hochschildCoface: the cofaces φ ↦ φ ∘ dᵢ on multilinear cochains.
• TauCeti.hochschildCoboundary: the Hochschild coboundary b.
• TauCeti.cyclicCochains: the submodule of cyclic cochains.
• TauCeti.cyclicHochschildCoboundary: the restriction of b to cyclic cochains.
• TauCeti.cyclicCochainsMap: the pullback of cyclic cochains along a linear map.

Main results

• TauCeti.hochschildCoboundary_hochschildCoboundary: b (b φ) = 0.
• TauCeti.hochschildCoboundary_mem_cyclicCochains: b maps cyclic cochains to cyclic cochains.
• TauCeti.hochschildCoboundary_apply_eq_zero_of_add_add_mul_eq_zero: the Hochschild coboundary of a cyclic cochain vanishes on a tuple whose cyclically adjacent entries are quasi-inverse.
• TauCeti.apply_update_const_eq_zero_of_isIdempotentElem: an even-degree cyclic cocycle vanishes on (e, …, y, …, e) when e is idempotent and y is tangent to the idempotents at e.
• TauCeti.cyclicHochschildCoboundary_cyclicHochschildCoboundary: the restriction of b to cyclic cochains also squares to zero.
• TauCeti.hochschildCoboundary_zero_eq_zero_iff: the degree-zero cocycles are the traces.
• TauCeti.hochschildCoboundary_compLinearMap: b commutes with pullback along a homomorphism.
• TauCeti.prod_hochschildFace: over a commutative monoid the faces preserve the product of the entries.

References

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

Faces on natural-number indexed sequences

Hochschild faces of tuples

def TauCeti.hochschildFace {A : Type u_1} {n : ℕ} [Mul A] (i : Fin (n + 2)) (a : Fin (n + 2) → A) : Fin (n + 1) → A

The i-th Hochschild face of a tuple (a₀, …, aₙ₊₁). For i ≤ n it multiplies the adjacent entries aᵢ and aᵢ₊₁; the last face is (aₙ₊₁ a₀, a₁, …, aₙ), i.e. the zeroth face of the cyclically rotated tuple (aₙ₊₁, a₀, …, aₙ).

@[simp]

theorem TauCeti.hochschildFace_castSucc {A : Type u_1} {n : ℕ} [Mul A] (j : Fin (n + 1)) (a : Fin (n + 2) → A) : hochschildFace j.castSucc a = j.castSucc.contractNth (fun (x1 x2 : A) => x1 * x2) a

The j-th Hochschild face for j ≤ n multiplies the entries j and j + 1.

theorem TauCeti.hochschildFace_last_eq_contractNth {A : Type u_1} {n : ℕ} [Mul A] (a : Fin (n + 2) → A) : hochschildFace (Fin.last (n + 1)) a = Fin.contractNth 0 (fun (x1 x2 : A) => x1 * x2) (a ∘ ⇑(Equiv.symm (finRotate (n + 2))))

The last Hochschild face is the zeroth face of the cyclically rotated tuple.

@[simp]

theorem TauCeti.hochschildFace_last {A : Type u_1} {n : ℕ} [Mul A] (a : Fin (n + 2) → A) : hochschildFace (Fin.last (n + 1)) a = Fin.cons (a (Fin.last (n + 1)) * a 0) fun (k : Fin n) => a k.castSucc.succ

The last Hochschild face is (aₙ₊₁ a₀, a₁, …, aₙ).

theorem TauCeti.hochschildFace_zero_comp_finRotate_symm {A : Type u_1} {n : ℕ} [Mul A] (a : Fin (n + 2) → A) : hochschildFace 0 (a ∘ ⇑(Equiv.symm (finRotate (n + 2)))) = hochschildFace (Fin.last (n + 1)) a

The zeroth face of the rotated tuple (aₙ₊₁, a₀, …, aₙ) is the last face of a.

theorem TauCeti.hochschildFace_succ_comp_finRotate_symm {A : Type u_1} {n : ℕ} [Mul A] (i : Fin (n + 1)) (a : Fin (n + 2) → A) : hochschildFace i.succ (a ∘ ⇑(Equiv.symm (finRotate (n + 2)))) = hochschildFace i.castSucc a ∘ ⇑(Equiv.symm (finRotate (n + 1)))

The faces commute with cyclic rotation: d_{i+1} ∘ t = t ∘ dᵢ.

theorem TauCeti.comp_hochschildFace {A : Type u_1} {n : ℕ} [Mul A] {B : Type u_2} {F : Type u_3} [Mul B] [FunLike F A B] [MulHomClass F A B] (f : F) (i : Fin (n + 2)) (a : Fin (n + 2) → A) : ⇑f ∘ hochschildFace i a = hochschildFace i (⇑f ∘ a)

A multiplicative map commutes with the Hochschild faces.

theorem TauCeti.hochschildFace_const_of_isIdempotentElem {A : Type u_1} {n : ℕ} [Mul A] {x : A} (hx : IsIdempotentElem x) (i : Fin (n + 2)) : (hochschildFace i fun (x_1 : Fin (n + 2)) => x) = fun (x_1 : Fin (n + 1)) => x

Every Hochschild face fixes a constant tuple whose entry is idempotent.

theorem TauCeti.hochschildFace_castSucc_eq_succ_of_apply_succ_eq_one {A : Type u_1} {n : ℕ} [MulOneClass A] (a : Fin (n + 2) → A) (j : Fin (n + 1)) (ha : a j.succ = 1) : hochschildFace j.castSucc a = hochschildFace j.succ a

The two Hochschild faces adjacent to a noninitial unit argument agree.

@[simp]

theorem TauCeti.prod_hochschildFace {A : Type u_1} {n : ℕ} [CommMonoid A] (i : Fin (n + 2)) (a : Fin (n + 2) → A) : ∏ k : Fin (n + 1), hochschildFace i a k = ∏ k : Fin (n + 2), a k

In a commutative monoid every Hochschild face preserves the product of the entries.

theorem TauCeti.hochschildFace_hochschildFace {A : Type u_1} {n : ℕ} [Semigroup A] {i j : Fin (n + 2)} (hij : i ≤ j) (a : Fin (n + 3) → A) : hochschildFace i (hochschildFace j.succ a) = hochschildFace j (hochschildFace i.castSucc a)

The simplicial identity dᵢ ∘ d_{j+1} = d_j ∘ dᵢ for i ≤ j between Hochschild faces.

Cochains and the Hochschild coboundary

def TauCeti.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] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] {n : ℕ} (i : Fin (n + 2)) : ((Fin (n + 1) → A) →ₘₗ[R] M) →ₗ[R] (Fin (n + 2) → A) →ₘₗ[R] M

The i-th Hochschild coface, sending an n-cochain φ (a multilinear map in n + 1 arguments) to the (n + 1)-cochain a ↦ φ (dᵢ a).

@[simp]

theorem TauCeti.hochschildCoface_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] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] {n : ℕ} (i : Fin (n + 2)) (φ : (Fin (n + 1) → A) →ₘₗ[R] M) (a : Fin (n + 2) → A) : ((hochschildCoface R A M i) φ) a = φ (hochschildFace i a)

The i-th coface evaluates a cochain on the i-th Hochschild face of the tuple.

Cyclic cochains

def TauCeti.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 : ℕ) : Submodule R ((Fin (n + 1) → A) →ₘₗ[R] M)

The cyclic n-cochains: the multilinear maps φ in n + 1 arguments with φ(aₙ, a₀, …, aₙ₋₁) = (-1)ⁿ φ(a₀, …, aₙ).

@[simp]

theorem TauCeti.mem_cyclicCochains_iff {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 ↔ ∀ (a : Fin (n + 1) → A), φ (a ∘ ⇑(Equiv.symm (finRotate (n + 1)))) = (-1) ^ n • φ a

A cochain is cyclic exactly when rotating its arguments multiplies its value by (-1)ⁿ.

@[simp]

theorem TauCeti.cyclicCochains_apply_finRotate_symm (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 : ℕ} (φ : ↥(cyclicCochains R A M n)) (a : Fin (n + 1) → A) : ↑φ (a ∘ ⇑(Equiv.symm (finRotate (n + 1)))) = (-1) ^ n • ↑φ a

A bundled cyclic cochain satisfies the characteristic cyclic rotation identity.

theorem TauCeti.apply_const_eq_neg_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) (hn : Odd n) (x : A) : (φ fun (x_1 : Fin (n + 1)) => x) = -φ fun (x_1 : Fin (n + 1)) => x

On a constant tuple, a cyclic cochain of odd degree takes a value v with v = -v.

@[simp]

theorem TauCeti.cyclicCochains_zero (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] : cyclicCochains R A M 0 = ⊤

Every 0-cochain is cyclic.

theorem TauCeti.mem_cyclicCochains_one_iff {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] {φ : (Fin 2 → A) →ₘₗ[R] M} : φ ∈ cyclicCochains R A M 1 ↔ ∀ (x y : A), φ ![y, x] = -φ ![x, y]

A 1-cochain is cyclic exactly when it is antisymmetric: φ(a₁, a₀) = -φ(a₀, a₁).

theorem TauCeti.mem_cyclicCochains_two_iff {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] {φ : (Fin 3 → A) →ₘₗ[R] M} : φ ∈ cyclicCochains R A M 2 ↔ ∀ (x y z : A), φ ![z, x, y] = φ ![x, y, z]

A 2-cochain is cyclic exactly when it is invariant under cyclic rotation of its arguments: φ(a₂, a₀, a₁) = φ(a₀, a₁, a₂).

theorem MultilinearMap.map_update_mul_of_add_add_mul_eq_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_4} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [AddCommGroup M] [Module R M] [DecidableEq ι] (f : (ι → A) →ₘₗ[R] M) (r : ι → A) (j : ι) {p q : A} (h : q + p + p * q = 0) : f (Function.update r j (p * q)) = -(f (Function.update r j p) + f (Function.update r j q))

A multilinear map evaluated on a product pq of quasi-inverse elements, q + p + pq = 0, in one slot is minus the sum of its values on p and on q in that slot.

theorem MultilinearMap.map_contractNth_castSucc_of_add_add_mul_eq_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [AddCommGroup M] [Module R M] {n : ℕ} (f : (Fin (n + 1) → A) →ₘₗ[R] M) (x : Fin (n + 2) → A) (j : Fin (n + 1)) (h : x j.succ + x j.castSucc + x j.castSucc * x j.succ = 0) : f (j.castSucc.contractNth (fun (x1 x2 : A) => x1 * x2) x) = -(f (j.succ.removeNth x) + f (j.castSucc.removeNth x))

A multilinear map evaluated on a tuple x with the quasi-inverse entries j and j + 1 multiplied together is minus the sum of its values on x with entry j + 1 or entry j deleted.

def TauCeti.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) →ₗ[R] (Fin (n + 2) → A) →ₘₗ[R] M

The Hochschild coboundary b on M-valued cochains of A, the alternating sum ∑ᵢ (-1)ⁱ φ ∘ dᵢ of the cofaces. Explicitly (hochschildCoboundary_apply_eq_sum_contractNth_add), (bφ)(a₀, …, aₙ₊₁) = ∑_{j ≤ n} (-1)ʲ φ(a₀, …, aⱼaⱼ₊₁, …, aₙ₊₁) + (-1)ⁿ⁺¹ φ(aₙ₊₁a₀, a₁, …, aₙ).

@[simp]

theorem TauCeti.hochschildCoboundary_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) : ((hochschildCoboundary R A M n) φ) a = ∑ i : Fin (n + 2), (-1) ^ ↑i • φ (hochschildFace i a)

The Hochschild coboundary evaluates as the alternating sum of φ on the faces of the tuple.

theorem TauCeti.hochschildCoboundary_apply_eq_sum_contractNth_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) (a : Fin (n + 2) → A) : ((hochschildCoboundary R A M n) φ) a = ∑ j : Fin (n + 1), (-1) ^ ↑j • φ (j.castSucc.contractNth (fun (x1 x2 : A) => x1 * x2) a) + (-1) ^ (n + 1) • φ (Fin.cons (a (Fin.last (n + 1)) * a 0) fun (k : Fin n) => a k.castSucc.succ)

The Hochschild coboundary in the explicit form of the multiplication of adjacent entries, followed by the cyclic term.

@[simp]

theorem TauCeti.hochschildCoboundary_hochschildCoboundary (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) : (hochschildCoboundary R A M (n + 1)) ((hochschildCoboundary R A M n) φ) = 0

The Hochschild coboundary squares to zero.

theorem TauCeti.hochschildCoboundary_comp_hochschildCoboundary (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 : ℕ} : hochschildCoboundary R A M (n + 1) ∘ₗ hochschildCoboundary R A M n = 0

The Hochschild coboundary squares to zero, as a composite of linear maps.

theorem TauCeti.hochschildCoboundary_zero_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] (φ : (Fin 1 → A) →ₘₗ[R] M) (a : Fin 2 → A) : ((hochschildCoboundary R A M 0) φ) a = (φ fun (x : Fin 1) => a 0 * a 1) - φ fun (x : Fin 1) => a 1 * a 0

In degree zero, (bφ)(a₀, a₁) = φ(a₀a₁) - φ(a₁a₀).

theorem TauCeti.hochschildCoboundary_one_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] (φ : (Fin 2 → A) →ₘₗ[R] M) (a : Fin 3 → A) : ((hochschildCoboundary R A M 1) φ) a = φ ![a 0 * a 1, a 2] - φ ![a 0, a 1 * a 2] + φ ![a 2 * a 0, a 1]

In degree one, (bφ)(a₀, a₁, a₂) = φ(a₀a₁, a₂) - φ(a₀, a₁a₂) + φ(a₂a₀, a₁).

theorem TauCeti.hochschildCoboundary_two_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] (φ : (Fin 3 → A) →ₘₗ[R] M) (a : Fin 4 → A) : ((hochschildCoboundary R A M 2) φ) a = φ ![a 0 * a 1, a 2, a 3] - φ ![a 0, a 1 * a 2, a 3] + φ ![a 0, a 1, a 2 * a 3] - φ ![a 3 * a 0, a 1, a 2]

In degree two, (bφ)(a₀, a₁, a₂, a₃) is φ(a₀a₁, a₂, a₃) - φ(a₀, a₁a₂, a₃) + φ(a₀, a₁, a₂a₃) - φ(a₃a₀, a₁, a₂).

theorem TauCeti.hochschildCoboundary_zero_eq_zero_iff (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] (φ : (Fin 1 → A) →ₘₗ[R] M) : (hochschildCoboundary R A M 0) φ = 0 ↔ ∀ (x y : A), (φ fun (x_1 : Fin 1) => x * y) = φ fun (x_1 : Fin 1) => y * x

A degree-zero cochain is a Hochschild cocycle exactly when it is a trace.

theorem TauCeti.hochschildCoboundary_apply_const_of_isIdempotentElem {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) {e : A} (he : IsIdempotentElem e) : (((hochschildCoboundary R A M n) φ) fun (x : Fin (n + 2)) => e) = if Even n then 0 else φ fun (x : Fin (n + 1)) => e

All faces fix a constant tuple with idempotent entry, so on such a tuple the Hochschild coboundary of a degree-n cochain vanishes for even n and is the cochain itself for odd n.

theorem TauCeti.hochschildCoboundary_mem_cyclicCochains (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} (hφ : φ ∈ cyclicCochains R A M n) : (hochschildCoboundary R A M n) φ ∈ cyclicCochains R A M (n + 1)

The Hochschild coboundary preserves cyclic cochains. When the multiplication is associative, so that b ∘ b = 0, the cyclic cochains therefore form a subcomplex.

theorem TauCeti.hochschildCoboundary_apply_eq_zero_of_add_add_mul_eq_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} (hψ : ψ ∈ cyclicCochains R A M n) {x : Fin (n + 2) → A} (hx : ∀ (i : Fin (n + 2)), x ((finRotate (n + 2)) i) + x i + x i * x ((finRotate (n + 2)) i) = 0) : ((hochschildCoboundary R A M n) ψ) x = 0

The Hochschild coboundary of a cyclic cochain vanishes on quasi-inverse chains. If the cyclically adjacent entries xᵢ, xᵢ₊₁ (indices modulo n + 2) of a tuple satisfy xᵢ₊₁ + xᵢ + xᵢxᵢ₊₁ = 0, then (bψ)(x₀, …, xₙ₊₁) = 0 for every cyclic n-cochain ψ.

def TauCeti.cyclicHochschildCoboundary (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 : ℕ) : ↥(cyclicCochains R A M n) →ₗ[R] ↥(cyclicCochains R A M (n + 1))

The Hochschild coboundary b restricted to the submodules of cyclic cochains, as a linear map C_λⁿ → C_λⁿ⁺¹. It squares to zero when the multiplication is associative.

@[simp]

theorem TauCeti.coe_cyclicHochschildCoboundary_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 : ℕ} (φ : ↥(cyclicCochains R A M n)) : ↑((cyclicHochschildCoboundary R A M n) φ) = (hochschildCoboundary R A M n) ↑φ

The restricted coboundary agrees with b on underlying cochains.

@[simp]

theorem TauCeti.cyclicHochschildCoboundary_cyclicHochschildCoboundary (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 : ℕ} (φ : ↥(cyclicCochains R A M n)) : (cyclicHochschildCoboundary R A M (n + 1)) ((cyclicHochschildCoboundary R A M n) φ) = 0

The restricted coboundary on cyclic cochains squares to zero.

theorem TauCeti.cyclicHochschildCoboundary_comp_cyclicHochschildCoboundary (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 : ℕ} : cyclicHochschildCoboundary R A M (n + 1) ∘ₗ cyclicHochschildCoboundary R A M n = 0

The restricted coboundary on cyclic cochains squares to zero, as a composite of linear maps.

theorem TauCeti.apply_update_const_eq_zero_of_isIdempotentElem {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} (hn : Even n) {φ : (Fin (n + 1) → A) →ₘₗ[R] M} (hφ : φ ∈ cyclicCochains R A M n) (hbφ : (hochschildCoboundary R A M n) φ = 0) {e y : A} (he : IsIdempotentElem e) (hy : e * y + y * e = y) (k : Fin (n + 1)) : φ (Function.update (fun (x : Fin (n + 1)) => e) k y) = 0

Infinitesimal invariance of the even pairing. Let φ be a cyclic cocycle of even degree and e an idempotent. If y is tangent to the idempotents at e, that is e y + y e = y, then φ vanishes on the tuple (e, …, e) with one entry replaced by y.

Pullback of cochains

theorem TauCeti.compLinearMap_mem_cyclicCochains {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] (f : A →ₗ[R] B) {φ : (Fin (n + 1) → B) →ₘₗ[R] M} (hφ : φ ∈ cyclicCochains R B M n) : (φ.compLinearMap fun (x : Fin (n + 1)) => f) ∈ cyclicCochains R A M n

Pulling a cyclic cochain back along a linear map gives a cyclic cochain.

def TauCeti.cyclicCochainsMap {R : Type u_1} {A : Type u_2} {B : Type u_3} (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] (f : A →ₗ[R] B) (n : ℕ) : ↥(cyclicCochains R B M n) →ₗ[R] ↥(cyclicCochains R A M n)

The pullback φ ↦ φ ∘ (f × ⋯ × f) of cyclic cochains along a linear map. This is built directly rather than from MultilinearMap.compLinearMapₗ, which needs R to be commutative.

@[simp]

theorem TauCeti.coe_cyclicCochainsMap_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] (f : A →ₗ[R] B) (φ : ↥(cyclicCochains R B M n)) : ↑((cyclicCochainsMap M f n) φ) = (↑φ).compLinearMap fun (x : Fin (n + 1)) => f

The pullback of a cyclic cochain evaluates the cochain on the images of the arguments.

@[simp]

theorem TauCeti.cyclicCochainsMap_id {R : Type u_1} {A : Type u_2} (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [AddCommMonoid A] [Module R A] (n : ℕ) : cyclicCochainsMap M LinearMap.id n = LinearMap.id

Pulling back along the identity is the identity.

theorem TauCeti.cyclicCochainsMap_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [AddCommMonoid C] [Module R C] (f : A →ₗ[R] B) (g : B →ₗ[R] C) (n : ℕ) : cyclicCochainsMap M (g ∘ₗ f) n = cyclicCochainsMap M f n ∘ₗ cyclicCochainsMap M g n

Pulling back along a composite is the composite of the pullbacks, in the opposite order.

theorem TauCeti.hochschildCoboundary_compLinearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) (φ : (Fin (n + 1) → B) →ₘₗ[R] M) : (hochschildCoboundary R A M n) (φ.compLinearMap fun (x : Fin (n + 1)) => ↑f) = ((hochschildCoboundary R B M n) φ).compLinearMap fun (x : Fin (n + 2)) => ↑f

The Hochschild coboundary commutes with pulling cochains back along a homomorphism of nonunital algebras.

theorem TauCeti.cyclicHochschildCoboundary_cyclicCochainsMap {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {n : ℕ} [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) (φ : ↥(cyclicCochains R B M n)) : (cyclicHochschildCoboundary R A M n) ((cyclicCochainsMap M (↑f) n) φ) = (cyclicCochainsMap M (↑f) (n + 1)) ((cyclicHochschildCoboundary R B M n) φ)

Pulling cyclic cochains back along a homomorphism of nonunital algebras commutes with the Hochschild coboundary.