Cyclic cohomology

The cyclic cochains C_λⁿ(A; M) of an algebra A, the M-valued multilinear maps φ in n + 1 arguments with φ(aₙ, a₀, …, aₙ₋₁) = (-1)ⁿ φ(a₀, …, aₙ), form a subcomplex of the Hochschild cochains. This file assembles them into Connes' cyclic cochain complex cyclicCochainComplex R A M, a cochain complex of R-modules indexed by ℕ, and defines the cyclic cohomology HCⁿ(A; M) of a unital algebra as its categorical cohomology. This is Connes' definition by cyclic cochains; over a ring containing ℚ it agrees with the cohomology of the cyclic bicomplex (TauCeti.RingTheory.CyclicCohomology.Bicomplex).

The cyclic cocycles and coboundaries are also described concretely, as submodules of the cyclic cochains, and cyclicCohomology.mk sends a cocycle to its class: it is surjective, and its kernel consists exactly of the coboundaries, so linear maps out of cyclic cohomology are described by cyclicCohomology.desc. In degree zero there are no coboundaries and the cocycles are the traces, so HC⁰(A; M) is the module of M-valued traces on A.

A homomorphism of nonunital algebras f : A →ₙₐ[R] B pulls cyclic cochains back along f, giving a cochain map cyclicCochainComplex R B M ⟶ cyclicCochainComplex R A M and a map on cyclic cohomology, contravariantly functorial in f. The homomorphism is not required to preserve units, since the algebra maps from A to the differential graded algebras of cycles need not.

The concrete cocycles and coboundaries are defined for nonassociative, nonunital semirings when the R-action on M commutes with itself. Associativity is required to show that every coboundary is a cocycle. A cyclic coboundary vanishes on tuples of cyclically adjacent quasi-inverse entries, without an associativity assumption. The categorical complex and cohomology use a commutative ring.

The cochain complex is defined for nonunital algebras. Its cohomology is only named cyclic cohomology for unital A: the cyclic cohomology of a nonunital algebra is instead defined through its forced unitization, and in general differs from the cohomology of this complex.

Main definitions

• TauCeti.cyclicCochainComplex: the cyclic cochain complex.
• TauCeti.cyclicCocycles, TauCeti.cyclicCoboundaries: cyclic cocycles and coboundaries.
• TauCeti.cyclicCohomology: the cyclic cohomology HCⁿ(A; M).
• TauCeti.cyclicCohomology.mk: the class of a cyclic cocycle.
• TauCeti.cyclicCohomology.desc: the linear map out of cyclic cohomology induced by a linear map on cyclic cocycles vanishing on cyclic coboundaries.
• TauCeti.cyclicCochainComplexMap, TauCeti.cyclicCohomology.map: pullback along a homomorphism of nonunital algebras, induced by TauCeti.cyclicCochainsMap.

Main results

• TauCeti.apply_eq_zero_of_mem_cyclicCoboundaries_of_add_add_mul_eq_zero: a cyclic coboundary vanishes on a tuple whose cyclically adjacent entries are quasi-inverse.
• TauCeti.cyclicCohomology.mk_surjective, TauCeti.cyclicCohomology.mk_eq_zero_iff: cyclic cohomology is the quotient of cyclic cocycles by cyclic coboundaries.
• TauCeti.cyclicCohomology.zeroEquiv, TauCeti.mem_cyclicCocycles_zero_iff: HC⁰(A; M) is the module of M-valued traces on A.
• TauCeti.cyclicCohomology.map_id, TauCeti.cyclicCohomology.map_comp: functoriality.

References

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

The concrete description of cohomology classes through mk follows the pattern of the de Rham cohomology file TauCeti.Geometry.Manifold.DeRham.Basic.

def TauCeti.cyclicCocycles (R : Type u_1) (A : Type u) (M : Type u_2) [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 : ℕ) : Submodule R ↥(cyclicCochains R A M n)

The cyclic n-cocycles: the cyclic cochains annihilated by the Hochschild coboundary.

@[simp]

theorem TauCeti.mem_cyclicCocycles_iff (R : Type u_1) (A : Type u) (M : Type u_2) [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)} : φ ∈ cyclicCocycles R A M n ↔ (hochschildCoboundary R A M n) ↑φ = 0

A cyclic cochain is a cocycle exactly when its Hochschild coboundary vanishes.

def TauCeti.cyclicCoboundaries (R : Type u_1) (A : Type u) (M : Type u_2) [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 : ℕ) : Submodule R ↥(cyclicCochains R A M n)

The cyclic n-coboundaries: zero in degree zero, and the image of the Hochschild coboundary of cyclic n-cochains in degree n + 1.

@[simp]

theorem TauCeti.cyclicCoboundaries_zero (R : Type u_1) (A : Type u) (M : Type u_2) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] : cyclicCoboundaries R A M 0 = ⊥

There are no nonzero cyclic coboundaries in degree zero.

theorem TauCeti.cyclicCoboundaries_succ (R : Type u_1) (A : Type u) (M : Type u_2) [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 : ℕ) : cyclicCoboundaries R A M (n + 1) = (cyclicHochschildCoboundary R A M n).range

In positive degree the cyclic coboundaries are the image of the Hochschild coboundary.

@[simp]

theorem TauCeti.mem_cyclicCoboundaries_succ_iff (R : Type u_1) (A : Type u) (M : Type u_2) [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 + 1))} : φ ∈ cyclicCoboundaries R A M (n + 1) ↔ ∃ (ψ : ↥(cyclicCochains R A M n)), (cyclicHochschildCoboundary R A M n) ψ = φ

A cyclic (n + 1)-cochain is a coboundary exactly when it is the Hochschild coboundary of a cyclic n-cochain.

theorem TauCeti.apply_eq_zero_of_mem_cyclicCoboundaries_of_add_add_mul_eq_zero {R : Type u_1} {A : Type u} {M : Type u_2} [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)} (hφ : φ ∈ cyclicCoboundaries R A M n) {x : Fin (n + 1) → A} (hx : ∀ (i : Fin (n + 1)), x ((finRotate (n + 1)) i) + x i + x i * x ((finRotate (n + 1)) i) = 0) : ↑φ x = 0

A cyclic coboundary vanishes on a tuple whose cyclically adjacent entries xᵢ, xᵢ₊₁ are quasi-inverse, xᵢ₊₁ + xᵢ + xᵢxᵢ₊₁ = 0.

theorem TauCeti.mem_cyclicCocycles_zero_iff (R : Type u_1) (A : Type u) (M : Type u_2) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {φ : ↥(cyclicCochains R A M 0)} : φ ∈ cyclicCocycles R A M 0 ↔ ∀ (x y : A), (↑φ fun (x_1 : Fin (0 + 1)) => x * y) = ↑φ fun (x_1 : Fin (0 + 1)) => y * x

A cyclic 0-cochain is a cocycle exactly when it is a trace.

theorem TauCeti.cyclicCochainsMap_mem_cyclicCocycles {R : Type u_1} {A : Type u} {M : Type u_2} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] [SMulCommClass R R M] {B : Type u} [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) {n : ℕ} {φ : ↥(cyclicCochains R B M n)} (hφ : φ ∈ cyclicCocycles R B M n) : (cyclicCochainsMap M (↑f) n) φ ∈ cyclicCocycles R A M n

The pullback of a cyclic cocycle is a cyclic cocycle.

theorem TauCeti.cyclicCoboundaries_le_cyclicCocycles (R : Type u_1) (A : Type u) (M : Type u_2) [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 : ℕ) : cyclicCoboundaries R A M n ≤ cyclicCocycles R A M n

Every cyclic coboundary is a cyclic cocycle.

def TauCeti.cyclicCochainComplex (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) ℕ

Connes' cyclic cochain complex C_λ⁰ → C_λ¹ → ⋯: in degree n the cyclic M-valued n-cochains on A, with the Hochschild coboundary as differential.

def TauCeti.cyclicCochainComplexXIso (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 : ℕ) : (cyclicCochainComplex R A M).X n ≅ ↧↥(cyclicCochains R A M n)

The degree-n term of the cyclic cochain complex is the module of cyclic n-cochains.

theorem TauCeti.cyclicCochainComplex_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] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((cyclicCochainComplex R A M).d n (n + 1)) (cyclicCochainComplexXIso R A M (n + 1)).hom = CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R A M n).hom (ModuleCat.ofHom (cyclicHochschildCoboundary R A M n))

Under the identifications cyclicCochainComplexXIso, the differential of the cyclic cochain complex is the Hochschild coboundary.

theorem TauCeti.cyclicCochainComplex_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] (n : ℕ) {Z : ModuleCat R} (h : ↧↥(cyclicCochains R A M (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cyclicCochainComplex R A M).d n (n + 1)) (CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R A M (n + 1)).hom h) = CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R A M n).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (cyclicHochschildCoboundary R A M n)) h)

Under the identifications cyclicCochainComplexXIso, the differential of the cyclic cochain complex is the Hochschild coboundary.

theorem TauCeti.cyclicCochainComplex_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] (n : ℕ) (x : ↑((cyclicCochainComplex R A M).X n)) : (CategoryTheory.ConcreteCategory.hom (cyclicCochainComplexXIso R A M (n + 1)).hom) ((CategoryTheory.ConcreteCategory.hom ((cyclicCochainComplex R A M).d n (n + 1))) x) = (cyclicHochschildCoboundary R A M n) ((CategoryTheory.ConcreteCategory.hom (cyclicCochainComplexXIso R A M n).hom) x)

Under the identifications cyclicCochainComplexXIso, the differential of the cyclic cochain complex is the Hochschild coboundary.

theorem TauCeti.mem_cyclicCocycles_iff_complex (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 : ℕ) (φ : ↥(cyclicCochains R A M n)) : φ ∈ cyclicCocycles R A M n ↔ (CategoryTheory.ConcreteCategory.hom ((cyclicCochainComplex R A M).d n (n + 1))) ((CategoryTheory.ConcreteCategory.hom (cyclicCochainComplexXIso R A M n).inv) φ) = 0

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

def TauCeti.cyclicCochainComplexMap {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] {B : Type u} [NonUnitalSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) : cyclicCochainComplex R B M ⟶ cyclicCochainComplex R A M

The cochain map between cyclic cochain complexes induced by a homomorphism of nonunital algebras.

theorem TauCeti.cyclicCochainComplexMap_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] {B : Type u} [NonUnitalSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((cyclicCochainComplexMap M f).f n) (cyclicCochainComplexXIso R A M n).hom = CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R B M n).hom (ModuleCat.ofHom (cyclicCochainsMap M (↑f) n))

Under the identifications cyclicCochainComplexXIso, the induced cochain map is the pullback of cyclic cochains. This holds by definition, the identifications being identities.

theorem TauCeti.cyclicCochainComplexMap_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] {B : Type u} [NonUnitalSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) (n : ℕ) {Z : ModuleCat R} (h : ↧↥(cyclicCochains R A M n) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cyclicCochainComplexMap M f).f n) (CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R A M n).hom h) = CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R B M n).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (cyclicCochainsMap M (↑f) n)) h)

Under the identifications cyclicCochainComplexXIso, the induced cochain map is the pullback of cyclic cochains. This holds by definition, the identifications being identities.

theorem TauCeti.cyclicCochainComplexMap_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] {B : Type u} [NonUnitalSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) (n : ℕ) (x : ↑((cyclicCochainComplex R B M).X n)) : (CategoryTheory.ConcreteCategory.hom (cyclicCochainComplexXIso R A M n).hom) ((CategoryTheory.ConcreteCategory.hom ((cyclicCochainComplexMap M f).f n)) x) = (cyclicCochainsMap M (↑f) n) ((CategoryTheory.ConcreteCategory.hom (cyclicCochainComplexXIso R B M n).hom) x)

Under the identifications cyclicCochainComplexXIso, the induced cochain map is the pullback of cyclic cochains. This holds by definition, the identifications being identities.

@[simp]

theorem TauCeti.cyclicCochainComplexMap_id {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] : cyclicCochainComplexMap M (NonUnitalAlgHom.id R A) = CategoryTheory.CategoryStruct.id (cyclicCochainComplex R A M)

The identity homomorphism induces the identity cochain map.

theorem TauCeti.cyclicCochainComplexMap_comp {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] {B C : Type u} [NonUnitalSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [NonUnitalSemiring C] [Module R C] [IsScalarTower R C C] [SMulCommClass R C C] (f : A →ₙₐ[R] B) (g : B →ₙₐ[R] C) : cyclicCochainComplexMap M (g.comp f) = CategoryTheory.CategoryStruct.comp (cyclicCochainComplexMap M g) (cyclicCochainComplexMap M f)

The induced cochain map is contravariantly functorial.

@[reducible, inline]

noncomputable abbrev TauCeti.cyclicCohomology (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : ModuleCat R

The cyclic cohomology HCⁿ(A; M) of a unital algebra A with coefficients in M, the cohomology of the cyclic cochain complex. For M = R this is Connes' cyclic cohomology HCⁿ(A), defined by cyclic cochains: over a ground ring containing ℚ it agrees with the cohomology of the cyclic bicomplex (TauCeti.RingTheory.CyclicCohomology.Bicomplex), and over other rings the two can differ.

noncomputable def TauCeti.cyclicCohomology.mk (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : ↥(cyclicCocycles R A M n) →ₗ[R] ↑(cyclicCohomology R A M n)

The cyclic cohomology class of a cyclic cocycle.

theorem TauCeti.cyclicCohomology.mk_eq_homologyπ (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {n : ℕ} (φ : ↥(cyclicCocycles R A M n)) (z : ↑(HomologicalComplex.cycles (cyclicCochainComplex R A M) n)) (hz : (CategoryTheory.ConcreteCategory.hom (cyclicCochainComplexXIso R A M n).hom) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (cyclicCochainComplex R A M) n)) z) = ↑φ) : (mk R A M n) φ = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (cyclicCochainComplex R A M) n)) z

The class of a cyclic cocycle φ is the homology class of any cycle of the cyclic cochain complex whose underlying cochain is φ.

theorem TauCeti.cyclicCohomology.mk_surjective (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : Function.Surjective ⇑(mk R A M n)

Every cyclic cohomology class is the class of a cyclic cocycle.

@[simp]

theorem TauCeti.cyclicCohomology.mk_eq_zero_iff (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) (φ : ↥(cyclicCocycles R A M n)) : (mk R A M n) φ = 0 ↔ ↑φ ∈ cyclicCoboundaries R A M n

A cyclic cocycle has zero cohomology class exactly when it is a cyclic coboundary.

theorem TauCeti.cyclicCohomology.mk_eq_mk_iff (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) (φ ψ : ↥(cyclicCocycles R A M n)) : (mk R A M n) φ = (mk R A M n) ψ ↔ ↑φ - ↑ψ ∈ cyclicCoboundaries R A M n

Two cyclic cocycles have the same class exactly when they differ by a cyclic coboundary.

theorem TauCeti.cyclicCohomology.mk_zero_injective (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] : Function.Injective ⇑(mk R A M 0)

In degree zero the class map is injective: there are no nonzero cyclic coboundaries.

noncomputable def TauCeti.cyclicCohomology.zeroEquiv (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] : ↥(cyclicCocycles R A M 0) ≃ₗ[R] ↑(cyclicCohomology R A M 0)

HC⁰(A; M) is the module of cyclic 0-cocycles. Every 0-cochain is cyclic (cyclicCochains_zero) and the 0-cocycles are the traces (mem_cyclicCocycles_zero_iff), so this identifies HC⁰(A; M) with the module of M-valued traces on A.

@[simp]

theorem TauCeti.cyclicCohomology.zeroEquiv_apply (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (φ : ↥(cyclicCocycles R A M 0)) : (zeroEquiv R A M) φ = (mk R A M 0) φ

The equivalence zeroEquiv sends a cyclic 0-cocycle to its class.

theorem TauCeti.cyclicCohomology.linearMap_ext {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {n : ℕ} {f g : ↑(cyclicCohomology R A M n) →ₗ[R] N} (h : f ∘ₗ mk R A M n = g ∘ₗ mk R A M n) : f = g

Two linear maps out of cyclic cohomology agree once they agree on classes of cocycles.

theorem TauCeti.cyclicCohomology.linearMap_ext_iff {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {n : ℕ} {f g : ↑(cyclicCohomology R A M n) →ₗ[R] N} : f = g ↔ f ∘ₗ mk R A M n = g ∘ₗ mk R A M n

noncomputable def TauCeti.cyclicCohomology.desc {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (n : ℕ) (f : ↥(cyclicCocycles R A M n) →ₗ[R] N) (hf : ∀ (φ : ↥(cyclicCocycles R A M n)), ↑φ ∈ cyclicCoboundaries R A M n → f φ = 0) : ↑(cyclicCohomology R A M n) →ₗ[R] N

A linear map on cyclic cocycles that vanishes on cyclic coboundaries descends to cyclic cohomology.

@[simp]

theorem TauCeti.cyclicCohomology.desc_mk {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (n : ℕ) (f : ↥(cyclicCocycles R A M n) →ₗ[R] N) (hf : ∀ (φ : ↥(cyclicCocycles R A M n)), ↑φ ∈ cyclicCoboundaries R A M n → f φ = 0) (φ : ↥(cyclicCocycles R A M n)) : (desc n f hf) ((mk R A M n) φ) = f φ

The descended map sends the class of a cocycle to the value of the original map.

@[simp]

theorem TauCeti.cyclicCohomology.desc_comp_mk {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (n : ℕ) (f : ↥(cyclicCocycles R A M n) →ₗ[R] N) (hf : ∀ (φ : ↥(cyclicCocycles R A M n)), ↑φ ∈ cyclicCoboundaries R A M n → f φ = 0) : desc n f hf ∘ₗ mk R A M n = f

The descended map composed with the class map is the original map.

noncomputable def TauCeti.cyclicCohomology.map {R : Type u_1} {A : Type u} (M : Type u_2) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {B : Type u} [Ring B] [Algebra R B] (f : A →ₙₐ[R] B) (n : ℕ) : cyclicCohomology R B M n ⟶ cyclicCohomology R A M n

The map on cyclic cohomology induced by a homomorphism of nonunital algebras between unital algebras; the homomorphism need not preserve the unit.

@[simp]

theorem TauCeti.cyclicCohomology.map_mk {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {B : Type u} [Ring B] [Algebra R B] (f : A →ₙₐ[R] B) {n : ℕ} (φ : ↥(cyclicCocycles R B M n)) : (CategoryTheory.ConcreteCategory.hom (map M f n)) ((mk R B M n) φ) = (mk R A M n) ⟨(cyclicCochainsMap M (↑f) n) ↑φ, ⋯⟩

The induced map sends the class of a cocycle to the class of its pullback.

@[simp]

theorem TauCeti.cyclicCohomology.map_id {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : map M (NonUnitalAlgHom.id R A) n = CategoryTheory.CategoryStruct.id (cyclicCohomology R A M n)

The identity homomorphism induces the identity on cyclic cohomology.

theorem TauCeti.cyclicCohomology.map_comp {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {B C : Type u} [Ring B] [Algebra R B] [Ring C] [Algebra R C] (f : A →ₙₐ[R] B) (g : B →ₙₐ[R] C) (n : ℕ) : map M (g.comp f) n = CategoryTheory.CategoryStruct.comp (map M g n) (map M f n)

Cyclic cohomology is contravariantly functorial.