Bounded-convergence topology of continuous cyclic cochain operators

The cyclic, Hochschild and mixed-complex operators on jointly continuous multilinear cochains are continuous for uniform convergence on bounded sets of tuples. We use the native topology on ContinuousMultilinearMap from Mathlib. By Bornology.isVonNBounded_pi_iff, bounded sets of tuples are contained in products of bounded coordinate sets, so this is also uniform convergence on products of bounded sets.

In particular the cyclic Hochschild differential is continuous on the cyclic subspaces with their induced topologies, and pullback of cyclic cochains along a continuous linear map is continuous. These facts apply to locally convex algebras without requiring local convexity, completeness, separation, a norm on the algebra, or closed differential ranges. Multiplication must be jointly continuous. The operators are defined on the naive cochains of a nonunital algebra; no comparison with the relative complex of its forced unitization is asserted here.

References

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

The topology is Mathlib's native topology on continuous multilinear maps. Operator continuity reuses UniformOnFun.precomp_uniformContinuous, and the bounded-image argument reuses Bornology.IsVonNBounded.image_multilinear'.

theorem TauCeti.continuous_continuousCyclicOperator (𝕜 : Type u_1) (A : Type u_2) (M : Type u_3) [NormedField 𝕜] [AddCommGroup A] [Module 𝕜 A] [TopologicalSpace A] [AddCommGroup M] [Module 𝕜 M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul 𝕜 M] (n : ℕ) : Continuous ⇑(continuousCyclicOperator 𝕜 A M n)

Signed cyclic rotation is continuous for bounded convergence of cochains.

theorem TauCeti.continuous_continuousCyclicNorm (𝕜 : Type u_1) (A : Type u_2) (M : Type u_3) [NormedField 𝕜] [AddCommGroup A] [Module 𝕜 A] [TopologicalSpace A] [AddCommGroup M] [Module 𝕜 M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul 𝕜 M] (n : ℕ) : Continuous ⇑(continuousCyclicNorm 𝕜 A M n)

The finite cyclic norm is continuous for bounded convergence of cochains.

theorem TauCeti.isVonNBounded_image_hochschildFace (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNonAssocRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [TopologicalSpace A] [ContinuousMul A] {n : ℕ} {s : Set (Fin (n + 2) → A)} (hs : Bornology.IsVonNBounded 𝕜 s) (i : Fin (n + 2)) : Bornology.IsVonNBounded 𝕜 (hochschildFace i '' s)

A Hochschild face sends bounded sets of tuples to bounded sets of tuples.

theorem TauCeti.continuous_continuousHochschildCoboundary (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNonAssocRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [TopologicalSpace A] [ContinuousMul A] (M : Type u_3) [AddCommGroup M] [Module 𝕜 M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul 𝕜 M] (n : ℕ) : Continuous ⇑(continuousHochschildCoboundary 𝕜 A M n)

The Hochschild coboundary is continuous for bounded convergence of cochains.

theorem TauCeti.continuous_continuousBarCoboundary (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNonAssocRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [TopologicalSpace A] [ContinuousMul A] (M : Type u_3) [AddCommGroup M] [Module 𝕜 M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul 𝕜 M] (n : ℕ) : Continuous ⇑(continuousBarCoboundary 𝕜 A M n)

The bar coboundary is continuous for bounded convergence of cochains.

theorem TauCeti.continuous_continuousCyclicHochschildCoboundary (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNonAssocRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [TopologicalSpace A] [ContinuousMul A] (M : Type u_3) [AddCommGroup M] [Module 𝕜 M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul 𝕜 M] (n : ℕ) : Continuous ⇑(continuousCyclicHochschildCoboundary 𝕜 A M n)

The cyclic Hochschild differential is continuous on the cyclic cochain subspaces.

theorem TauCeti.continuous_continuousBarContraction (𝕜 : Type u_1) (A : Type u_2) (M : Type u_3) [NormedField 𝕜] [AddCommGroup A] [Module 𝕜 A] [TopologicalSpace A] [ContinuousSMul 𝕜 A] [One A] [AddCommGroup M] [Module 𝕜 M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul 𝕜 M] (n : ℕ) : Continuous ⇑(continuousBarContraction 𝕜 A M n)

Insertion of the unit is continuous for bounded convergence of cochains.

theorem TauCeti.continuous_continuousConnesB (𝕜 : Type u_1) (A : Type u_2) (M : Type u_3) [NormedField 𝕜] [AddCommGroup A] [Module 𝕜 A] [TopologicalSpace A] [ContinuousSMul 𝕜 A] [One A] [AddCommGroup M] [Module 𝕜 M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul 𝕜 M] (n : ℕ) : Continuous ⇑(continuousConnesB 𝕜 A M n)

Connes' operator is continuous for bounded convergence of cochains.

theorem TauCeti.continuous_continuousCyclicCochainsMap {𝕜 : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [NormedField 𝕜] [AddCommGroup A] [Module 𝕜 A] [TopologicalSpace A] [AddCommGroup B] [Module 𝕜 B] [TopologicalSpace B] [AddCommGroup M] [Module 𝕜 M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul 𝕜 M] (f : A →L[𝕜] B) (n : ℕ) : Continuous ⇑(continuousCyclicCochainsMap M f n)

Pullback of continuous cyclic cochains is continuous for bounded convergence.