Continuous cyclic and mixed cochain operators

The Hochschild and cyclic operators preserve jointly continuous multilinear cochains on a topological algebra. This file lifts the algebraic operators to native ContinuousMultilinearMaps and proves the mixed-complex identities there. The comparison with algebraic cochains is given by the forgetful map toMultilinearMap, and on cyclic cochains by continuousCyclicCochains.toCyclicCochains. Preservation of cyclic cochains does not require associativity; the Hochschild and bar square-zero identities do. Continuous cyclic cochains pull back along continuous linear maps (continuousCyclicCochainsMap), functorially, and compatibly with the Hochschild coboundary along continuous homomorphisms of nonunital algebras.

No norm, local convexity, completeness or separation is needed for preservation of continuity. The scalar action on the target is continuous for each fixed scalar. For a unital algebra, insertion of the unit gives the continuous bar contraction and hence Connes' operator B. These operations supply the differentials for continuous cyclic cohomology, including on Fréchet algebras. No topology on the space of cochains or quotient cohomology is imposed here.

References

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

The algebraic formulas and identities are those of TauCeti.RingTheory.CyclicCohomology.ConnesOperator.

theorem TauCeti.continuous_hochschildFace (A : Type u_1) [TopologicalSpace A] [Mul A] [ContinuousMul A] {n : ℕ} (i : Fin (n + 2)) : Continuous (hochschildFace i)

Multiplication faces of tuples are continuous for a jointly continuous multiplication.

theorem ContinuousMultilinearMap.continuous_cyclicOperator {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] {n : ℕ} (φ : A [×n + 1]→L[R] M) : Continuous ⇑((TauCeti.cyclicOperator R A M n) φ.toMultilinearMap)

Cyclic permutation with its sign preserves joint continuity.

theorem ContinuousMultilinearMap.continuous_cyclicNorm {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] {n : ℕ} (φ : A [×n + 1]→L[R] M) : Continuous ⇑((TauCeti.cyclicNorm R A M n) φ.toMultilinearMap)

The finite cyclic norm preserves joint continuity.

theorem ContinuousMultilinearMap.continuous_hochschildCoface {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [TopologicalSpace A] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsScalarTower R A A] [SMulCommClass R A A] [ContinuousMul A] {n : ℕ} (φ : A [×n + 1]→L[R] M) (i : Fin (n + 2)) : Continuous ⇑((TauCeti.hochschildCoface R A M i) φ.toMultilinearMap)

Every Hochschild coface preserves joint continuity.

theorem ContinuousMultilinearMap.continuous_hochschildCoboundary {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] {n : ℕ} [IsScalarTower R A A] [SMulCommClass R A A] [ContinuousMul A] (φ : A [×n + 1]→L[R] M) : Continuous ⇑((TauCeti.hochschildCoboundary R A M n) φ.toMultilinearMap)

The Hochschild coboundary preserves joint continuity.

theorem ContinuousMultilinearMap.continuous_barCoboundary {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] {n : ℕ} [IsScalarTower R A A] [SMulCommClass R A A] [ContinuousMul A] (φ : A [×n + 1]→L[R] M) : Continuous ⇑((TauCeti.barCoboundary R A M n) φ.toMultilinearMap)

The bar coboundary preserves joint continuity.

theorem ContinuousMultilinearMap.continuous_barContraction {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] {n : ℕ} [One A] (φ : A [×n + 2]→L[R] M) : Continuous ⇑((TauCeti.barContraction R A M n) φ.toMultilinearMap)

Inserting the unit as the first argument preserves joint continuity.

theorem ContinuousMultilinearMap.continuous_connesB {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] {n : ℕ} [One A] (φ : A [×n + 2]→L[R] M) : Continuous ⇑((TauCeti.connesB R A M n) φ.toMultilinearMap)

Connes' operator preserves joint continuity.

def TauCeti.continuousCyclicOperator (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] (n : ℕ) : Module.End R (A [×n + 1]→L[R] M)

The signed cyclic rotation on continuous multilinear cochains.

@[simp]

theorem TauCeti.toMultilinearMap_continuousCyclicOperator (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] (n : ℕ) (φ : A [×n + 1]→L[R] M) : ((continuousCyclicOperator R A M n) φ).toMultilinearMap = (cyclicOperator R A M n) φ.toMultilinearMap

Forgetting continuity recovers the algebraic cyclic rotation.

@[simp]

theorem TauCeti.continuousCyclicOperator_apply (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] (n : ℕ) (φ : A [×n + 1]→L[R] M) (a : Fin (n + 1) → A) : ((continuousCyclicOperator R A M n) φ) a = ((cyclicOperator R A M n) φ.toMultilinearMap) a

Evaluation of the continuous cyclic rotation agrees with the algebraic formula.

def TauCeti.continuousCyclicNorm (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] (n : ℕ) : Module.End R (A [×n + 1]→L[R] M)

The cyclic norm on continuous multilinear cochains.

@[simp]

theorem TauCeti.toMultilinearMap_continuousCyclicNorm (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] (n : ℕ) (φ : A [×n + 1]→L[R] M) : ((continuousCyclicNorm R A M n) φ).toMultilinearMap = (cyclicNorm R A M n) φ.toMultilinearMap

Forgetting continuity recovers the algebraic cyclic norm.

@[simp]

theorem TauCeti.continuousCyclicNorm_apply (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] (n : ℕ) (φ : A [×n + 1]→L[R] M) (a : Fin (n + 1) → A) : ((continuousCyclicNorm R A M n) φ) a = ((cyclicNorm R A M n) φ.toMultilinearMap) a

Evaluation of the continuous cyclic norm agrees with the algebraic formula.

def TauCeti.continuousHochschildCoboundary (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] [IsScalarTower R A A] [SMulCommClass R A A] [ContinuousMul A] (n : ℕ) : (A [×n + 1]→L[R] M) →ₗ[R] A [×n + 2]→L[R] M

The Hochschild coboundary on continuous multilinear cochains.

@[simp]

theorem TauCeti.toMultilinearMap_continuousHochschildCoboundary (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] [IsScalarTower R A A] [SMulCommClass R A A] [ContinuousMul A] (n : ℕ) (φ : A [×n + 1]→L[R] M) : ((continuousHochschildCoboundary R A M n) φ).toMultilinearMap = (hochschildCoboundary R A M n) φ.toMultilinearMap

Forgetting continuity recovers the algebraic Hochschild coboundary.

@[simp]

theorem TauCeti.continuousHochschildCoboundary_apply (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] [IsScalarTower R A A] [SMulCommClass R A A] [ContinuousMul A] (n : ℕ) (φ : A [×n + 1]→L[R] M) (a : Fin (n + 2) → A) : ((continuousHochschildCoboundary R A M n) φ) a = ((hochschildCoboundary R A M n) φ.toMultilinearMap) a

Evaluation of the continuous Hochschild coboundary agrees with the algebraic formula.

def TauCeti.continuousBarCoboundary (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] [IsScalarTower R A A] [SMulCommClass R A A] [ContinuousMul A] (n : ℕ) : (A [×n + 1]→L[R] M) →ₗ[R] A [×n + 2]→L[R] M

The bar coboundary on continuous multilinear cochains.

@[simp]

theorem TauCeti.toMultilinearMap_continuousBarCoboundary (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] [IsScalarTower R A A] [SMulCommClass R A A] [ContinuousMul A] (n : ℕ) (φ : A [×n + 1]→L[R] M) : ((continuousBarCoboundary R A M n) φ).toMultilinearMap = (barCoboundary R A M n) φ.toMultilinearMap

Forgetting continuity recovers the algebraic bar coboundary.

@[simp]

theorem TauCeti.continuousBarCoboundary_apply (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] [IsScalarTower R A A] [SMulCommClass R A A] [ContinuousMul A] (n : ℕ) (φ : A [×n + 1]→L[R] M) (a : Fin (n + 2) → A) : ((continuousBarCoboundary R A M n) φ) a = ((barCoboundary R A M n) φ.toMultilinearMap) a

Evaluation of the continuous bar coboundary agrees with the algebraic formula.

def TauCeti.continuousBarContraction (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M] [One A] [ContinuousAdd M] (n : ℕ) : (A [×n + 2]→L[R] M) →ₗ[R] A [×n + 1]→L[R] M

The unit-inserting contraction on continuous multilinear cochains.

@[simp]

theorem TauCeti.toMultilinearMap_continuousBarContraction (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M] [One A] [ContinuousAdd M] (n : ℕ) (φ : A [×n + 2]→L[R] M) : ((continuousBarContraction R A M n) φ).toMultilinearMap = (barContraction R A M n) φ.toMultilinearMap

Forgetting continuity recovers the algebraic unit-inserting contraction.

@[simp]

theorem TauCeti.continuousBarContraction_apply (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M] [One A] [ContinuousAdd M] (n : ℕ) (φ : A [×n + 2]→L[R] M) (a : Fin (n + 1) → A) : ((continuousBarContraction R A M n) φ) a = ((barContraction R A M n) φ.toMultilinearMap) a

Evaluation of the continuous unit insertion agrees with the algebraic formula.

def TauCeti.continuousConnesB (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M] [One A] [IsTopologicalAddGroup M] (n : ℕ) : (A [×n + 2]→L[R] M) →ₗ[R] A [×n + 1]→L[R] M

Connes' operator on continuous multilinear cochains.

@[simp]

theorem TauCeti.toMultilinearMap_continuousConnesB (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M] [One A] [IsTopologicalAddGroup M] (n : ℕ) (φ : A [×n + 2]→L[R] M) : ((continuousConnesB R A M n) φ).toMultilinearMap = (connesB R A M n) φ.toMultilinearMap

Forgetting continuity recovers the algebraic Connes operator.

@[simp]

theorem TauCeti.continuousConnesB_apply (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M] [One A] [IsTopologicalAddGroup M] (n : ℕ) (φ : A [×n + 2]→L[R] M) (a : Fin (n + 1) → A) : ((continuousConnesB R A M n) φ) a = ((connesB R A M n) φ.toMultilinearMap) a

Evaluation of the continuous Connes operator agrees with the algebraic formula.

def TauCeti.continuousCyclicCochains (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M] [ContinuousAdd M] (n : ℕ) : Submodule R (A [×n + 1]→L[R] M)

The submodule of jointly continuous cochains satisfying the signed cyclic relation.

@[simp]

theorem TauCeti.mem_continuousCyclicCochains_iff (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M] [ContinuousAdd M] {n : ℕ} {φ : A [×n + 1]→L[R] M} : φ ∈ continuousCyclicCochains R A M n ↔ φ.toMultilinearMap ∈ cyclicCochains R A M n

A continuous cochain is cyclic precisely when its underlying algebraic cochain is cyclic.

theorem TauCeti.continuousCyclicNorm_mem_continuousCyclicCochains (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M] [IsTopologicalAddGroup M] {n : ℕ} (φ : A [×n + 1]→L[R] M) : (continuousCyclicNorm R A M n) φ ∈ continuousCyclicCochains R A M n

The cyclic norm of a continuous cochain is cyclic.

theorem TauCeti.continuousConnesB_mem_continuousCyclicCochains (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M] [IsTopologicalAddGroup M] [One A] {n : ℕ} (φ : A [×n + 2]→L[R] M) : (continuousConnesB R A M n) φ ∈ continuousCyclicCochains R A M n

Connes' operator takes continuous cochains to continuous cyclic cochains.

theorem TauCeti.continuousConnesB_eq_zero_of_mem_continuousCyclicCochains (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M] [IsTopologicalAddGroup M] [One A] {n : ℕ} {φ : A [×n + 2]→L[R] M} (hφ : φ ∈ continuousCyclicCochains R A M (n + 1)) : (continuousConnesB R A M n) φ = 0

Connes' operator vanishes on continuous cyclic cochains.

@[simp]

theorem TauCeti.continuousConnesB_continuousConnesB (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M] [IsTopologicalAddGroup M] [One A] {n : ℕ} (φ : A [×n + 3]→L[R] M) : (continuousConnesB R A M n) ((continuousConnesB R A M (n + 1)) φ) = 0

The continuous Connes operator squares to zero.

theorem TauCeti.continuousHochschildCoboundary_mem_continuousCyclicCochains (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] [TopologicalSpace A] [ContinuousMul A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] {n : ℕ} {φ : A [×n + 1]→L[R] M} (hφ : φ ∈ continuousCyclicCochains R A M n) : (continuousHochschildCoboundary R A M n) φ ∈ continuousCyclicCochains R A M (n + 1)

The Hochschild coboundary preserves continuous cyclic cochains.

def TauCeti.continuousCyclicHochschildCoboundary (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] [TopologicalSpace A] [ContinuousMul A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] (n : ℕ) : ↥(continuousCyclicCochains R A M n) →ₗ[R] ↥(continuousCyclicCochains R A M (n + 1))

The Hochschild coboundary restricted to continuous cyclic cochains.

@[simp]

theorem TauCeti.coe_continuousCyclicHochschildCoboundary (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] [TopologicalSpace A] [ContinuousMul A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] {n : ℕ} (φ : ↥(continuousCyclicCochains R A M n)) : ↑((continuousCyclicHochschildCoboundary R A M n) φ) = (continuousHochschildCoboundary R A M n) ↑φ

The restricted coboundary agrees with the continuous Hochschild coboundary.

@[simp]

theorem TauCeti.continuousHochschildCoboundary_continuousHochschildCoboundary (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] [TopologicalSpace A] [ContinuousMul A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] {n : ℕ} (φ : A [×n + 1]→L[R] M) : (continuousHochschildCoboundary R A M (n + 1)) ((continuousHochschildCoboundary R A M n) φ) = 0

The continuous Hochschild coboundary squares to zero.

@[simp]

theorem TauCeti.continuousBarCoboundary_continuousBarCoboundary (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] [TopologicalSpace A] [ContinuousMul A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] {n : ℕ} (φ : A [×n + 1]→L[R] M) : (continuousBarCoboundary R A M (n + 1)) ((continuousBarCoboundary R A M n) φ) = 0

The continuous bar coboundary squares to zero.

@[simp]

theorem TauCeti.continuousCyclicHochschildCoboundary_continuousCyclicHochschildCoboundary (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] [TopologicalSpace A] [ContinuousMul A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] {n : ℕ} (φ : ↥(continuousCyclicCochains R A M n)) : (continuousCyclicHochschildCoboundary R A M (n + 1)) ((continuousCyclicHochschildCoboundary R A M n) φ) = 0

The restricted continuous cyclic differential squares to zero.

@[simp]

theorem TauCeti.continuousBarContraction_continuousBarCoboundary_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] [TopologicalSpace A] [ContinuousMul A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] (φ : A [×1]→L[R] M) : (continuousBarContraction R A M 0) ((continuousBarCoboundary R A M 0) φ) = φ

In degree zero, insertion of the unit contracts the continuous bar differential.

theorem TauCeti.continuousBarCoboundary_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] [TopologicalSpace A] [ContinuousMul A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] {n : ℕ} (φ : A [×n + 2]→L[R] M) : (continuousBarCoboundary R A M n) ((continuousBarContraction R A M n) φ) + (continuousBarContraction R A M (n + 1)) ((continuousBarCoboundary R A M (n + 1)) φ) = φ

In positive degrees, insertion of the unit contracts the continuous bar differential.

theorem TauCeti.continuousHochschildCoboundary_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] [TopologicalSpace A] [ContinuousMul A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] {n : ℕ} (φ : A [×n + 2]→L[R] M) : (continuousHochschildCoboundary R A M n) ((continuousConnesB R A M n) φ) + (continuousConnesB R A M (n + 1)) ((continuousHochschildCoboundary R A M (n + 1)) φ) = 0

The continuous Hochschild and Connes operators anticommute.

def TauCeti.continuousCyclicCochains.toCyclicCochains (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] (n : ℕ) : ↥(continuousCyclicCochains R A M n) →ₗ[R] ↥(cyclicCochains R A M n)

Forgetting continuity, as a linear map from continuous cyclic cochains to cyclic cochains.

@[simp]

theorem TauCeti.continuousCyclicCochains.coe_toCyclicCochains (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] {n : ℕ} (φ : ↥(continuousCyclicCochains R A M n)) : ↑((toCyclicCochains R A M n) φ) = (↑φ).toMultilinearMap

Forgetting continuity keeps the underlying multilinear map.

theorem TauCeti.continuousCyclicCochains.toCyclicCochains_injective (R : Type u_1) (A : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] (n : ℕ) : Function.Injective ⇑(toCyclicCochains R A M n)

Forgetting continuity is injective.

theorem TauCeti.continuousCyclicCochains.toCyclicCochains_continuousCyclicHochschildCoboundary {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] [TopologicalSpace A] [ContinuousMul A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] {n : ℕ} (φ : ↥(continuousCyclicCochains R A M n)) : (toCyclicCochains R A M (n + 1)) ((continuousCyclicHochschildCoboundary R A M n) φ) = (cyclicHochschildCoboundary R A M n) ((toCyclicCochains R A M n) φ)

Forgetting continuity commutes with the Hochschild coboundary.

def TauCeti.continuousCyclicCochainsMap {R : Type u_1} {A : Type u_2} {B : Type u_3} (M : Type u_5) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommMonoid B] [Module R B] [TopologicalSpace B] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] (f : A →L[R] B) (n : ℕ) : ↥(continuousCyclicCochains R B M n) →ₗ[R] ↥(continuousCyclicCochains R A M n)

The pullback φ ↦ φ ∘ (f × ⋯ × f) of continuous cyclic cochains along a continuous linear map.

@[simp]

theorem TauCeti.coe_continuousCyclicCochainsMap_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommMonoid B] [Module R B] [TopologicalSpace B] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] (f : A →L[R] B) {n : ℕ} (φ : ↥(continuousCyclicCochains R B M n)) : ↑((continuousCyclicCochainsMap M f n) φ) = (↑φ).compContinuousLinearMap fun (x : Fin (n + 1)) => f

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

theorem TauCeti.continuousCyclicCochains.toCyclicCochains_continuousCyclicCochainsMap {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommMonoid B] [Module R B] [TopologicalSpace B] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] (f : A →L[R] B) {n : ℕ} (φ : ↥(continuousCyclicCochains R B M n)) : (toCyclicCochains R A M n) ((continuousCyclicCochainsMap M f n) φ) = (cyclicCochainsMap M (↑f) n) ((toCyclicCochains R B M n) φ)

Forgetting continuity commutes with pullback.

@[simp]

theorem TauCeti.continuousCyclicCochainsMap_id {R : Type u_1} {A : Type u_2} (M : Type u_5) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] (n : ℕ) : continuousCyclicCochainsMap M (ContinuousLinearMap.id R A) n = LinearMap.id

Pulling back along the identity is the identity.

theorem TauCeti.continuousCyclicCochainsMap_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid A] [Module R A] [TopologicalSpace A] [AddCommMonoid B] [Module R B] [TopologicalSpace B] [AddCommMonoid C] [Module R C] [TopologicalSpace C] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] (f : A →L[R] B) (g : B →L[R] C) (n : ℕ) : continuousCyclicCochainsMap M (g ∘SL f) n = continuousCyclicCochainsMap M f n ∘ₗ continuousCyclicCochainsMap M g n

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

theorem TauCeti.continuousCyclicHochschildCoboundary_continuousCyclicCochainsMap {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [TopologicalSpace A] [ContinuousMul A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [TopologicalSpace B] [ContinuousMul B] [AddCommGroup M] [Module R M] [SMulCommClass R R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] (f : A →ₙₐ[R] B) (hf : Continuous ⇑f) {n : ℕ} (φ : ↥(continuousCyclicCochains R B M n)) : (continuousCyclicHochschildCoboundary R A M n) ((continuousCyclicCochainsMap M { toLinearMap := ↑f, cont := hf } n) φ) = (continuousCyclicCochainsMap M { toLinearMap := ↑f, cont := hf } (n + 1)) ((continuousCyclicHochschildCoboundary R B M n) φ)

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