The total complex of the cyclic bicomplex

For an R-algebra A and an R-module M, write C^q for the M-valued multilinear maps in q + 1 arguments on A. Connes' cyclic bicomplex has the module C^q in every column p of row q. Its horizontal differentials C^q → C^q alternate between 1 - λ (out of even columns) and the cyclic norm N (out of odd columns). Its vertical differentials C^q → C^(q+1) alternate between the Hochschild coboundary b (in even columns) and -b' (in odd columns), where b' is the bar coboundary. The relations (1 - λ) b = b' (1 - λ) and b N = N b' make adjacent squares anticommute, so the sum of the two differentials squares to zero on the total complex.

The degree-m term of the total complex is ⊕_{p + q = m} C^q. Here it is the submodule cyclicTotalCochains R A M m of families (x_q)_{q ∈ ℕ} with x_q ∈ C^q and x_q = 0 for q > m; the component x_q sits in column m - q. Indexing by rows avoids natural-number subtraction in the types of the components.

Column zero is the Hochschild cochain complex, and the kernel of its outgoing horizontal map 1 - λ is the module of cyclic cochains. Hence including a cyclic cochain into column zero gives a cochain map cyclicCochainComplexToTotal R A M from Connes' cyclic cochain complex to the total complex. When q + 1 is invertible in R, the rows of the bicomplex are exact away from column zero (TauCeti.RingTheory.CyclicCohomology.RowExactness), and this cochain map is a quasi-isomorphism. So over a ring containing ℚ, cyclic cohomology defined by cyclic cochains is the cohomology of the total cyclic bicomplex.

The total cochain modules require only additive commutative monoids of coefficients. Constructing the total differential and its compatibility with cyclic cochains uses bilinear multiplication on A; associativity is needed for the total differential to square to zero.

Main definitions

• TauCeti.cyclicBicomplexHorizontal: the horizontal differential out of column p of row q.
• TauCeti.cyclicBicomplexVertical: the vertical differential in column p out of row q.
• TauCeti.cyclicTotalCochains: the degree-m term of the total complex.
• TauCeti.cyclicTotalDifferential: the total differential.
• TauCeti.cyclicTotalComplex: the total complex, a cochain complex of R-modules.
• TauCeti.cyclicCochainsToTotal, TauCeti.cyclicCochainComplexToTotal: the inclusion of cyclic cochains into column zero, and the resulting cochain map.
• TauCeti.cyclicTotalHomologyMk: the class of a total cocycle in the cohomology of the total complex.

Main results

• TauCeti.range_cyclicBicomplexHorizontal_eq_ker_cyclicBicomplexHorizontal: the rows are exact away from column zero.
• TauCeti.cyclicBicomplexVertical_comp_cyclicBicomplexHorizontal: adjacent squares of the bicomplex anticommute.
• TauCeti.cyclicTotalDifferential_cyclicTotalDifferential: the total differential squares to zero.
• TauCeti.quasiIsoAt_cyclicCochainComplexToTotal: in degree m, the inclusion of the cyclic cochain complex is a quasi-isomorphism when q + 1 is invertible for every q < m.
• TauCeti.quasiIso_cyclicCochainComplexToTotal: over a ring containing ℚ, the inclusion is a quasi-isomorphism.
• TauCeti.homologyMap_cyclicCochainComplexToTotal_mk: the inclusion sends the class of a cyclic cocycle to the class of the same cochain in column zero.

References

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

The differentials of the cyclic bicomplex

def TauCeti.cyclicBicomplexHorizontal (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] (p q : ℕ) : Module.End R ((Fin (q + 1) → A) →ₘₗ[R] M)

The horizontal differential of the cyclic bicomplex out of column p in row q: 1 - λ out of an even column and the cyclic norm N out of an odd column.

@[simp]

theorem TauCeti.cyclicBicomplexHorizontal_of_even {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {p q : ℕ} (hp : Even p) : cyclicBicomplexHorizontal R A M p q = 1 - cyclicOperator R A M q

Out of an even column the horizontal differential is 1 - λ.

@[simp]

theorem TauCeti.cyclicBicomplexHorizontal_of_odd {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {p q : ℕ} (hp : Odd p) : cyclicBicomplexHorizontal R A M p q = cyclicNorm R A M q

Out of an odd column the horizontal differential is the cyclic norm N.

@[simp]

theorem TauCeti.cyclicBicomplexHorizontal_add_two (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] (p q : ℕ) : cyclicBicomplexHorizontal R A M (p + 2) q = cyclicBicomplexHorizontal R A M p q

The horizontal differentials are periodic of period two in the column.

@[simp]

theorem TauCeti.cyclicBicomplexHorizontal_succ_mul_cyclicBicomplexHorizontal {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {p q : ℕ} : cyclicBicomplexHorizontal R A M (p + 1) q * cyclicBicomplexHorizontal R A M p q = 0

Two consecutive horizontal differentials compose to zero: N (1 - λ) = 0 = (1 - λ) N.

@[simp]

theorem TauCeti.cyclicBicomplexHorizontal_cyclicBicomplexHorizontal {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {p q : ℕ} (φ : (Fin (q + 1) → A) →ₘₗ[R] M) : (cyclicBicomplexHorizontal R A M (p + 1) q) ((cyclicBicomplexHorizontal R A M p q) φ) = 0

Two consecutive horizontal differentials compose to zero, on elements.

theorem TauCeti.range_cyclicBicomplexHorizontal_eq_ker_cyclicBicomplexHorizontal (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] (p q : ℕ) [Invertible (↑q + 1)] : LinearMap.range (cyclicBicomplexHorizontal R A M p q) = LinearMap.ker (cyclicBicomplexHorizontal R A M (p + 1) q)

When q + 1 is invertible, the rows of the cyclic bicomplex are exact away from column zero: the image of the horizontal differential into column p + 1 is the kernel of the one out of it.

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

The vertical differential of the cyclic bicomplex in column p out of row q: the Hochschild coboundary b in an even column and minus the bar coboundary, -b', in an odd column.

@[simp]

theorem TauCeti.cyclicBicomplexVertical_of_even {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {p q : ℕ} (hp : Even p) : cyclicBicomplexVertical R A M p q = hochschildCoboundary R A M q

In an even column the vertical differential is the Hochschild coboundary b.

@[simp]

theorem TauCeti.cyclicBicomplexVertical_of_odd {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {p q : ℕ} (hp : Odd p) : cyclicBicomplexVertical R A M p q = -barCoboundary R A M q

In an odd column the vertical differential is -b'.

@[simp]

theorem TauCeti.cyclicBicomplexVertical_add_two (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (p q : ℕ) : cyclicBicomplexVertical R A M (p + 2) q = cyclicBicomplexVertical R A M p q

The vertical differentials are periodic of period two in the column.

theorem TauCeti.cyclicBicomplexVertical_comp_cyclicBicomplexHorizontal (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (p q : ℕ) : cyclicBicomplexVertical R A M (p + 1) q ∘ₗ cyclicBicomplexHorizontal R A M p q = -cyclicBicomplexHorizontal R A M p (q + 1) ∘ₗ cyclicBicomplexVertical R A M p q

Adjacent squares of the cyclic bicomplex anticommute: going right then up is minus going up then right. In even columns this is (1 - λ) b = b' (1 - λ), in odd columns b N = N b'.

theorem TauCeti.cyclicBicomplexVertical_cyclicBicomplexHorizontal {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {p q : ℕ} (φ : (Fin (q + 1) → A) →ₘₗ[R] M) : (cyclicBicomplexVertical R A M (p + 1) q) ((cyclicBicomplexHorizontal R A M p q) φ) = -(cyclicBicomplexHorizontal R A M p (q + 1)) ((cyclicBicomplexVertical R A M p q) φ)

Adjacent squares of the cyclic bicomplex anticommute, on elements.

@[simp]

theorem TauCeti.cyclicBicomplexVertical_cyclicBicomplexVertical {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {p q : ℕ} (φ : (Fin (q + 1) → A) →ₘₗ[R] M) : (cyclicBicomplexVertical R A M p (q + 1)) ((cyclicBicomplexVertical R A M p q) φ) = 0

Two consecutive vertical differentials compose to zero: b ∘ b = 0 and b' ∘ b' = 0.

theorem TauCeti.cyclicBicomplexVertical_comp_cyclicBicomplexVertical (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (p q : ℕ) : cyclicBicomplexVertical R A M p (q + 1) ∘ₗ cyclicBicomplexVertical R A M p q = 0

Two consecutive vertical differentials compose to zero, as a composite of linear maps.

The total complex

def TauCeti.cyclicTotalCochains (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] (m : ℕ) : Submodule R ((q : ℕ) → (Fin (q + 1) → A) →ₘₗ[R] M)

The degree-m term ⊕_{p + q = m} C^q of the total complex of the cyclic bicomplex: the families (x_q)_q of M-valued q-cochains with x_q = 0 for q > m. The component x_q lies in column m - q.

@[simp]

theorem TauCeti.mem_cyclicTotalCochains_iff {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] {m : ℕ} {x : (q : ℕ) → (Fin (q + 1) → A) →ₘₗ[R] M} : x ∈ cyclicTotalCochains R A M m ↔ ∀ (q : ℕ), m < q → x q = 0

A family of cochains lies in total degree m exactly when it vanishes above row m.

@[simp]

theorem TauCeti.coe_cyclicTotalCochains_apply_of_lt {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] {m q : ℕ} (x : ↥(cyclicTotalCochains R A M m)) (hq : m < q) : ↑x q = 0

A total cochain of degree m vanishes in every row q > m.

theorem TauCeti.single_mem_cyclicTotalCochains {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] {m k : ℕ} (hk : k ≤ m) (φ : (Fin (k + 1) → A) →ₘₗ[R] M) : Pi.single k φ ∈ cyclicTotalCochains R A M m

A cochain placed in row k ≤ m is a total cochain of degree m.

theorem TauCeti.cyclicTotalCochains_mono {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid M] [Module R M] : Monotone (cyclicTotalCochains R A M)

A total cochain of degree m is a total cochain of every degree n ≥ m.

def TauCeti.cyclicCochainsToTotal (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] (m : ℕ) : ↥(cyclicCochains R A M m) →ₗ[R] ↥(cyclicTotalCochains R A M m)

The inclusion of cyclic m-cochains into column zero of the total complex.

@[simp]

theorem TauCeti.coe_cyclicCochainsToTotal_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] {m : ℕ} (φ : ↥(cyclicCochains R A M m)) : ↑((cyclicCochainsToTotal R A M m) φ) = Pi.single m ↑φ

A cyclic cochain is included as the family concentrated in row m, column zero.

theorem TauCeti.cyclicCochainsToTotal_injective (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommGroup M] [Module R M] (m : ℕ) : Function.Injective ⇑(cyclicCochainsToTotal R A M m)

The inclusion of cyclic cochains into column zero is injective.

def TauCeti.cyclicTotalDifferential (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (m : ℕ) : ↥(cyclicTotalCochains R A M m) →ₗ[R] ↥(cyclicTotalCochains R A M (m + 1))

The differential D = d_h + d_v of the total complex of the cyclic bicomplex, from total degree m to total degree m + 1.

@[simp]

theorem TauCeti.cyclicTotalDifferential_apply_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {m : ℕ} (x : ↥(cyclicTotalCochains R A M m)) : ↑((cyclicTotalDifferential R A M m) x) 0 = (cyclicBicomplexHorizontal R A M m 0) (↑x 0)

In row zero, the total differential is the horizontal differential out of column m.

@[simp]

theorem TauCeti.cyclicTotalDifferential_apply_succ {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {m : ℕ} (x : ↥(cyclicTotalCochains R A M m)) (q : ℕ) : ↑((cyclicTotalDifferential R A M m) x) (q + 1) = (cyclicBicomplexVertical R A M (m - q) q) (↑x q) + (cyclicBicomplexHorizontal R A M (m - (q + 1)) (q + 1)) (↑x (q + 1))

In row q + 1, the total differential adds the vertical differential of the component in row q, in column m - q, to the horizontal differential of the component in row q + 1.

@[simp]

theorem TauCeti.cyclicTotalDifferential_cyclicCochainsToTotal {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {m : ℕ} (φ : ↥(cyclicCochains R A M m)) : (cyclicTotalDifferential R A M m) ((cyclicCochainsToTotal R A M m) φ) = (cyclicCochainsToTotal R A M (m + 1)) ((cyclicHochschildCoboundary R A M m) φ)

The inclusion into column zero commutes with the differentials: the total differential of a cyclic cochain φ is (1 - λ) φ = 0 in column one plus b φ in column zero.

@[simp]

theorem TauCeti.cyclicTotalDifferential_cyclicTotalDifferential {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {m : ℕ} (x : ↥(cyclicTotalCochains R A M m)) : (cyclicTotalDifferential R A M (m + 1)) ((cyclicTotalDifferential R A M m) x) = 0

The total differential squares to zero.

theorem TauCeti.cyclicTotalDifferential_comp_cyclicTotalDifferential (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (m : ℕ) : cyclicTotalDifferential R A M (m + 1) ∘ₗ cyclicTotalDifferential R A M m = 0

The total differential squares to zero, as a composite of linear maps.

The total complex and the comparison with cyclic cochains

def TauCeti.cyclicTotalComplex (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] : CochainComplex (ModuleCat R) ℕ

The total complex of Connes' cyclic bicomplex, a cochain complex of R-modules indexed by ℕ.

def TauCeti.cyclicTotalComplexXIso (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (m : ℕ) : (cyclicTotalComplex R A M).X m ≅ ↧↥(cyclicTotalCochains R A M m)

The degree-m term of the total complex is the module of total cochains of degree m.

theorem TauCeti.cyclicTotalComplex_d (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (m : ℕ) : CategoryTheory.CategoryStruct.comp ((cyclicTotalComplex R A M).d m (m + 1)) (cyclicTotalComplexXIso R A M (m + 1)).hom = CategoryTheory.CategoryStruct.comp (cyclicTotalComplexXIso R A M m).hom (ModuleCat.ofHom (cyclicTotalDifferential R A M m))

Under the identifications cyclicTotalComplexXIso, the differential of the total complex is the total differential.

theorem TauCeti.cyclicTotalComplex_d_assoc (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (m : ℕ) {Z : ModuleCat R} (h : ↧↥(cyclicTotalCochains R A M (m + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cyclicTotalComplex R A M).d m (m + 1)) (CategoryTheory.CategoryStruct.comp (cyclicTotalComplexXIso R A M (m + 1)).hom h) = CategoryTheory.CategoryStruct.comp (cyclicTotalComplexXIso R A M m).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (cyclicTotalDifferential R A M m)) h)

Under the identifications cyclicTotalComplexXIso, the differential of the total complex is the total differential.

theorem TauCeti.cyclicTotalComplex_d_apply (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (m : ℕ) (x : ↑((cyclicTotalComplex R A M).X m)) : (CategoryTheory.ConcreteCategory.hom (cyclicTotalComplexXIso R A M (m + 1)).hom) ((CategoryTheory.ConcreteCategory.hom ((cyclicTotalComplex R A M).d m (m + 1))) x) = (cyclicTotalDifferential R A M m) ((CategoryTheory.ConcreteCategory.hom (cyclicTotalComplexXIso R A M m).hom) x)

Under the identifications cyclicTotalComplexXIso, the differential of the total complex is the total differential.

def TauCeti.cyclicCochainComplexToTotal (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] : cyclicCochainComplex R A M ⟶ cyclicTotalComplex R A M

The cochain map from Connes' cyclic cochain complex to the total complex of the cyclic bicomplex, including cyclic cochains into column zero.

theorem TauCeti.cyclicCochainComplexToTotal_f (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (m : ℕ) : CategoryTheory.CategoryStruct.comp ((cyclicCochainComplexToTotal R A M).f m) (cyclicTotalComplexXIso R A M m).hom = CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R A M m).hom (ModuleCat.ofHom (cyclicCochainsToTotal R A M m))

Under the identifications of the terms of both complexes, the cochain map to the total complex is the inclusion cyclicCochainsToTotal into column zero.

theorem TauCeti.cyclicCochainComplexToTotal_f_assoc (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (m : ℕ) {Z : ModuleCat R} (h : ↧↥(cyclicTotalCochains R A M m) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cyclicCochainComplexToTotal R A M).f m) (CategoryTheory.CategoryStruct.comp (cyclicTotalComplexXIso R A M m).hom h) = CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R A M m).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (cyclicCochainsToTotal R A M m)) h)

Under the identifications of the terms of both complexes, the cochain map to the total complex is the inclusion cyclicCochainsToTotal into column zero.

theorem TauCeti.cyclicCochainComplexToTotal_f_apply (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (m : ℕ) (x : ↑((cyclicCochainComplex R A M).X m)) : (CategoryTheory.ConcreteCategory.hom (cyclicTotalComplexXIso R A M m).hom) ((CategoryTheory.ConcreteCategory.hom ((cyclicCochainComplexToTotal R A M).f m)) x) = (cyclicCochainsToTotal R A M m) ((CategoryTheory.ConcreteCategory.hom (cyclicCochainComplexXIso R A M m).hom) x)

Under the identifications of the terms of both complexes, the cochain map to the total complex is the inclusion cyclicCochainsToTotal into column zero.

theorem TauCeti.quasiIsoAt_cyclicCochainComplexToTotal (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (m : ℕ) (hR : ∀ q < m, IsUnit (↑q + 1)) : QuasiIsoAt (cyclicCochainComplexToTotal R A M) m

Cyclic cochains compute the cohomology of the cyclic bicomplex. In degree m, the inclusion of Connes' cyclic cochain complex into column zero of the total complex of the cyclic bicomplex is a quasi-isomorphism, provided q + 1 is invertible in R for every q < m.

theorem TauCeti.quasiIso_cyclicCochainComplexToTotal (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [Algebra ℚ R] : QuasiIso (cyclicCochainComplexToTotal R A M)

Over a ring containing ℚ, the inclusion of Connes' cyclic cochain complex into the total complex of the cyclic bicomplex is a quasi-isomorphism: cyclic cohomology defined by cyclic cochains is the cohomology of the total cyclic bicomplex.

theorem TauCeti.bijective_homologyMap_cyclicCochainComplexToTotal (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [Algebra ℚ R] (n : ℕ) : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap (cyclicCochainComplexToTotal R A M) n))

Over a ring containing ℚ, the inclusion of cyclic cochains into column zero is bijective on cohomology.

Total cohomology classes

theorem TauCeti.mem_ker_cyclicTotalDifferential_iff (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) (x : ↥(cyclicTotalCochains R A M n)) : x ∈ (cyclicTotalDifferential R A M n).ker ↔ (CategoryTheory.ConcreteCategory.hom ((cyclicTotalComplex R A M).d n (n + 1))) ((CategoryTheory.ConcreteCategory.hom (cyclicTotalComplexXIso R A M n).inv) x) = 0

A total cochain is a total cocycle exactly when the differential of the total complex kills it.

noncomputable def TauCeti.cyclicTotalHomologyMk (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) : ↥(cyclicTotalDifferential R A M n).ker →ₗ[R] ↑(HomologicalComplex.homology (cyclicTotalComplex R A M) n)

The class of a total cocycle in the cohomology of the total complex.

theorem TauCeti.cyclicTotalHomologyMk_eq_homologyπ {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {n : ℕ} (x : ↥(cyclicTotalDifferential R A M n).ker) (z : ↑(HomologicalComplex.cycles (cyclicTotalComplex R A M) n)) (hz : (CategoryTheory.ConcreteCategory.hom (cyclicTotalComplexXIso R A M n).hom) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (cyclicTotalComplex R A M) n)) z) = ↑x) : (cyclicTotalHomologyMk R A M n) x = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (cyclicTotalComplex R A M) n)) z

The class of a total cocycle is the homology class of any cycle of the total complex whose underlying total cochain is that cocycle.

theorem TauCeti.cyclicTotalHomologyMk_surjective {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) : Function.Surjective ⇑(cyclicTotalHomologyMk R A M n)

Every class in the cohomology of the total complex is the class of a total cocycle.

@[simp]

theorem TauCeti.cyclicTotalHomologyMk_zero_eq_zero_iff {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (x : ↥(cyclicTotalDifferential R A M 0).ker) : (cyclicTotalHomologyMk R A M 0) x = 0 ↔ x = 0

A total cocycle of degree zero has zero class exactly when it vanishes.

@[simp]

theorem TauCeti.cyclicTotalHomologyMk_succ_eq_zero_iff {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {n : ℕ} (x : ↥(cyclicTotalDifferential R A M (n + 1)).ker) : (cyclicTotalHomologyMk R A M (n + 1)) x = 0 ↔ ∃ (w : ↥(cyclicTotalCochains R A M n)), (cyclicTotalDifferential R A M n) w = ↑x

A total cocycle of degree n + 1 has zero class exactly when it is a total coboundary.

theorem TauCeti.cyclicCochainsToTotal_mem_ker {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {m : ℕ} (φ : ↥(cyclicCocycles R A M m)) : (cyclicCochainsToTotal R A M m) ↑φ ∈ (cyclicTotalDifferential R A M m).ker

A cyclic cocycle, included into column zero, is a total cocycle.

@[simp]

theorem TauCeti.homologyMap_cyclicCochainComplexToTotal_mk {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {m : ℕ} (φ : ↥(cyclicCocycles R A M m)) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap (cyclicCochainComplexToTotal R A M) m)) ((cyclicCohomology.mk R A M m) φ) = (cyclicTotalHomologyMk R A M m) ⟨(cyclicCochainsToTotal R A M m) ↑φ, ⋯⟩

The inclusion of cyclic cochains into column zero sends the class of a cyclic cocycle to the class of the corresponding total cocycle.