Hochschild cochains with coefficients in the dual bimodule

Let A be an algebra over a commutative semiring R and N an R-module. The linear maps A →ₗ[R] N form an A-bimodule under (x • f) y = f (y * x) and (op x • f) y = f (x * y). For N = R this is the algebraic dual A* with (x φ x') y = φ (x' y x). Whenever N is itself an A-module, A →ₗ[R] N also carries the pointwise action (x • f) y = x • f y, so the dual actions are scoped instances in TauCeti.DualBimodule, as for Mathlib's TensorProduct.RightActions.

Currying the first argument (TauCeti.multilinearCurryFirstEquiv) identifies the N-valued cochains in n + 1 arguments, the degree-n cochains on which the Hochschild coboundary b of TauCeti.RingTheory.CyclicCohomology.Cochain acts, with the (A →ₗ[R] N)-valued cochains in n arguments. Under this identification b is the coboundary δ with coefficients in the dual bimodule: the face multiplying a₀ a₁ is the left action of a₁, and the cyclic face (aₙ₊₁ a₀, a₁, …, aₙ) is the right action of aₙ₊₁. Thus the cochain complex underlying cyclic cohomology is the Hochschild complex of A with coefficients in its dual.

Main results

• TauCeti.hochschildBimoduleCoface_multilinearCurryFirstEquiv: each coface with coefficients in the dual bimodule is the corresponding Hochschild coface of the uncurried cochain.
• TauCeti.multilinearCurryFirstEquiv_hochschildCoboundary: currying intertwines b and δ.
• TauCeti.hochschildCoboundary_multilinearCurryFirstEquiv_symm: the same comparison read in the other direction.

References

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

@[instance_reducible]

def TauCeti.DualBimodule.instSMul {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid N] [Module R N] : SMul A (A →ₗ[R] N)

The left action (x • f) y = f (y * x) of A on linear maps out of A.

@[instance_reducible]

def TauCeti.DualBimodule.instSMulOp {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid N] [Module R N] : SMul Aᵐᵒᵖ (A →ₗ[R] N)

The right action (op x • f) y = f (x * y) of A on linear maps out of A.

@[simp]

theorem TauCeti.DualBimodule.smul_linearMap_apply {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid N] [Module R N] (x : A) (f : A →ₗ[R] N) (y : A) : (x • f) y = f (y * x)

The left action of the dual bimodule precomposes with right multiplication.

@[simp]

theorem TauCeti.DualBimodule.op_smul_linearMap_apply {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid N] [Module R N] (x : Aᵐᵒᵖ) (f : A →ₗ[R] N) (y : A) : (x • f) y = f (MulOpposite.unop x * y)

The right action of the dual bimodule precomposes with left multiplication.

@[instance_reducible]

def TauCeti.DualBimodule.instModule {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid N] [Module R N] : Module A (A →ₗ[R] N)

Linear maps out of A form a left A-module under (x • f) y = f (y * x).

@[instance_reducible]

def TauCeti.DualBimodule.instModuleOp {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid N] [Module R N] : Module Aᵐᵒᵖ (A →ₗ[R] N)

Linear maps out of A form a left Aᵐᵒᵖ-module under (op x • f) y = f (x * y).

theorem TauCeti.DualBimodule.instSMulCommClass {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid N] [Module R N] : SMulCommClass A Aᵐᵒᵖ (A →ₗ[R] N)

The two actions of the dual bimodule commute.

theorem TauCeti.DualBimodule.instIsScalarTower {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid N] [Module R N] : IsScalarTower R A (A →ₗ[R] N)

The left action of the dual bimodule is R-linear.

theorem TauCeti.DualBimodule.instIsScalarTowerOp {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid N] [Module R N] : IsScalarTower R Aᵐᵒᵖ (A →ₗ[R] N)

The right action of the dual bimodule is R-linear.

theorem TauCeti.hochschildBimoduleCoface_multilinearCurryFirstEquiv {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup N] [Module R N] {n : ℕ} (i : Fin (n + 2)) (φ : (Fin (n + 1) → A) →ₘₗ[R] N) (a : Fin (n + 1) → A) (x : A) : (((hochschildBimoduleCoface R A (A →ₗ[R] N) i) ((multilinearCurryFirstEquiv R (fun (x : Fin (n + 1)) => A) N) φ)) a) x = φ (hochschildFace i (Fin.cons x a))

Each coface with coefficients in the dual bimodule is the corresponding Hochschild coface of the uncurried cochain.

theorem TauCeti.multilinearCurryFirstEquiv_hochschildCoboundary {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup N] [Module R N] {n : ℕ} (φ : (Fin (n + 1) → A) →ₘₗ[R] N) : (multilinearCurryFirstEquiv R (fun (x : Fin (n + 2)) => A) N) ((hochschildCoboundary R A N n) φ) = (hochschildBimoduleCoboundary R A (A →ₗ[R] N) n) ((multilinearCurryFirstEquiv R (fun (x : Fin (n + 1)) => A) N) φ)

Under currying of the first argument, the Hochschild coboundary b of N-valued cochains is the Hochschild coboundary δ with coefficients in the dual bimodule A →ₗ[R] N.

theorem TauCeti.hochschildCoboundary_multilinearCurryFirstEquiv_symm {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup N] [Module R N] {n : ℕ} (ψ : (Fin n → A) →ₘₗ[R] A →ₗ[R] N) : (hochschildCoboundary R A N n) ((multilinearCurryFirstEquiv R (fun (x : Fin (n + 1)) => A) N).symm ψ) = (multilinearCurryFirstEquiv R (fun (x : Fin (n + 2)) => A) N).symm ((hochschildBimoduleCoboundary R A (A →ₗ[R] N) n) ψ)

Uncurrying the first argument turns the Hochschild coboundary δ with coefficients in the dual bimodule into the Hochschild coboundary b of N-valued cochains.