Reduced cyclic cohomology of a unital algebra

For a unital algebra A over R, reduced cyclic cochains are cyclic cochains on A whose restriction to the scalar subalgebra vanishes. Thus they are the kernel of restriction along the unit-preserving scalar inclusion R → A. The Hochschild coboundary preserves this kernel and defines the reduced cyclic cochain complex.

The relative cyclic cohomology of a possibly nonunital algebra A (TauCeti.relativeCyclicCohomology) is the reduced cyclic cohomology of its forced unitization Unitization R A. It is a different functor of A from the reduced theory here, which uses the given unit of A: the reduced complex of the ground ring is zero, whereas the relative forced-unitization cohomology of a unital algebra recovers its full cyclic theory.

Main definitions

• TauCeti.scalarCyclicRestriction: restriction to the scalar subalgebra.
• TauCeti.reducedCyclicCochains: the kernel of scalar restriction.
• TauCeti.reducedCyclicCocycles, TauCeti.reducedCyclicCoboundaries: concrete cocycles and coboundaries.
• TauCeti.reducedCyclicCochainComplex: the reduced cyclic cochain complex.
• TauCeti.reducedCyclicCohomology: reduced cyclic cohomology.
• TauCeti.reducedCyclicCohomology.mk: the class of a reduced cyclic cocycle.
• TauCeti.reducedCyclicCochainsMap: contravariant pullback along a unital algebra homomorphism.
• TauCeti.reducedCyclicCohomology.toCyclic: the map from reduced cyclic cohomology to cyclic cohomology induced by the inclusion of reduced cochains.

References

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

def TauCeti.scalarCyclicRestriction (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : ↥(cyclicCochains R A M n) →ₗ[R] ↥(cyclicCochains R R M n)

Restriction of cyclic cochains on a unital algebra to its scalar subalgebra.

@[simp]

theorem TauCeti.scalarCyclicRestriction_apply (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) (phi : ↥(cyclicCochains R A M n)) (a : Fin (n + 1) → R) : ↑((scalarCyclicRestriction R A M n) phi) a = ↑phi fun (i : Fin (n + 1)) => (algebraMap R A) (a i)

Scalar restriction evaluates a cochain on arguments coming from the scalar subalgebra.

def TauCeti.reducedCyclicCochains (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : Submodule R ↥(cyclicCochains R A M n)

The reduced cyclic n-cochains of a unital algebra: cyclic cochains which vanish on the scalar subalgebra.

theorem TauCeti.mem_reducedCyclicCochains_iff (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] {n : ℕ} {phi : ↥(cyclicCochains R A M n)} : phi ∈ reducedCyclicCochains R A M n ↔ (scalarCyclicRestriction R A M n) phi = 0

A cyclic cochain is reduced exactly when its scalar restriction vanishes.

@[simp]

theorem TauCeti.mem_reducedCyclicCochains_iff_forall (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] {n : ℕ} {phi : ↥(cyclicCochains R A M n)} : phi ∈ reducedCyclicCochains R A M n ↔ ∀ (a : Fin (n + 1) → R), (↑phi fun (i : Fin (n + 1)) => (algebraMap R A) (a i)) = 0

A cyclic cochain is reduced exactly when it vanishes whenever all its arguments are scalars.

theorem TauCeti.cyclicHochschildCoboundary_mem_reducedCyclicCochains (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] {n : ℕ} (phi : ↥(reducedCyclicCochains R A M n)) : (cyclicHochschildCoboundary R A M n) ↑phi ∈ reducedCyclicCochains R A M (n + 1)

The Hochschild coboundary of a reduced cyclic cochain is reduced.

def TauCeti.reducedCyclicHochschildCoboundary (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : ↥(reducedCyclicCochains R A M n) →ₗ[R] ↥(reducedCyclicCochains R A M (n + 1))

The Hochschild coboundary restricted to reduced cyclic cochains.

@[simp]

theorem TauCeti.coe_reducedCyclicHochschildCoboundary_apply (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) (phi : ↥(reducedCyclicCochains R A M n)) : ↑((reducedCyclicHochschildCoboundary R A M n) phi) = (cyclicHochschildCoboundary R A M n) ↑phi

The reduced Hochschild coboundary has the ordinary cyclic Hochschild coboundary as its underlying cochain.

theorem TauCeti.reducedCyclicHochschildCoboundary_reducedCyclicHochschildCoboundary (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) (phi : ↥(reducedCyclicCochains R A M n)) : (reducedCyclicHochschildCoboundary R A M (n + 1)) ((reducedCyclicHochschildCoboundary R A M n) phi) = 0

The reduced Hochschild coboundary squares to zero.

theorem TauCeti.reducedCyclicHochschildCoboundary_comp_reducedCyclicHochschildCoboundary (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : reducedCyclicHochschildCoboundary R A M (n + 1) ∘ₗ reducedCyclicHochschildCoboundary R A M n = 0

The reduced Hochschild coboundary squares to zero as a composite of linear maps.

def TauCeti.reducedCyclicCocycles (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : Submodule R ↥(reducedCyclicCochains R A M n)

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

@[simp]

theorem TauCeti.mem_reducedCyclicCocycles_iff (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] {n : ℕ} {phi : ↥(reducedCyclicCochains R A M n)} : phi ∈ reducedCyclicCocycles R A M n ↔ (reducedCyclicHochschildCoboundary R A M n) phi = 0

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

theorem TauCeti.coe_mem_cyclicCocycles_iff_mem_reducedCyclicCocycles {R : Type u_1} {A : Type u} {M : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] {n : ℕ} {phi : ↥(reducedCyclicCochains R A M n)} : ↑phi ∈ cyclicCocycles R A M n ↔ phi ∈ reducedCyclicCocycles R A M n

A reduced cyclic cochain is a cyclic cocycle exactly when it is a reduced cyclic cocycle.

def TauCeti.reducedCyclicCoboundaries (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : Submodule R ↥(reducedCyclicCochains R A M n)

The reduced cyclic coboundaries: zero in degree zero, and in positive degree the image of the reduced Hochschild coboundary.

@[simp]

theorem TauCeti.reducedCyclicCoboundaries_zero (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] : reducedCyclicCoboundaries R A M 0 = ⊥

There are no nonzero reduced cyclic coboundaries in degree zero.

theorem TauCeti.reducedCyclicCoboundaries_succ (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : reducedCyclicCoboundaries R A M (n + 1) = (reducedCyclicHochschildCoboundary R A M n).range

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

@[simp]

theorem TauCeti.mem_reducedCyclicCoboundaries_succ_iff (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] {n : ℕ} {phi : ↥(reducedCyclicCochains R A M (n + 1))} : phi ∈ reducedCyclicCoboundaries R A M (n + 1) ↔ ∃ (psi : ↥(reducedCyclicCochains R A M n)), (reducedCyclicHochschildCoboundary R A M n) psi = phi

A reduced cyclic cochain in positive degree is a coboundary exactly when it is the reduced Hochschild coboundary of a reduced cochain in the preceding degree.

theorem TauCeti.reducedCyclicCoboundaries_le_reducedCyclicCocycles (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : reducedCyclicCoboundaries R A M n ≤ reducedCyclicCocycles R A M n

Every reduced cyclic coboundary is a reduced cyclic cocycle.

def TauCeti.reducedCyclicCochainComplex (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] : CochainComplex (ModuleCat R) ℕ

The reduced cyclic cochain complex of a unital algebra. Its degree-n term is the kernel of restriction from cyclic cochains on the algebra to cyclic cochains on the ground ring.

def TauCeti.reducedCyclicCochainComplexXIso (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : (reducedCyclicCochainComplex R A M).X n ≅ ↧↥(reducedCyclicCochains R A M n)

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

theorem TauCeti.reducedCyclicCochainComplex_d (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((reducedCyclicCochainComplex R A M).d n (n + 1)) (reducedCyclicCochainComplexXIso R A M (n + 1)).hom = CategoryTheory.CategoryStruct.comp (reducedCyclicCochainComplexXIso R A M n).hom (ModuleCat.ofHom (reducedCyclicHochschildCoboundary R A M n))

Under the canonical identifications of the terms, the differential of the reduced cyclic cochain complex is the reduced Hochschild coboundary.

theorem TauCeti.reducedCyclicCochainComplex_d_assoc (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) {Z : ModuleCat R} (h : ↧↥(reducedCyclicCochains R A M (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((reducedCyclicCochainComplex R A M).d n (n + 1)) (CategoryTheory.CategoryStruct.comp (reducedCyclicCochainComplexXIso R A M (n + 1)).hom h) = CategoryTheory.CategoryStruct.comp (reducedCyclicCochainComplexXIso R A M n).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (reducedCyclicHochschildCoboundary R A M n)) h)

Under the canonical identifications of the terms, the differential of the reduced cyclic cochain complex is the reduced Hochschild coboundary.

theorem TauCeti.reducedCyclicCochainComplex_d_apply (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) (x : ↑((reducedCyclicCochainComplex R A M).X n)) : (CategoryTheory.ConcreteCategory.hom (reducedCyclicCochainComplexXIso R A M (n + 1)).hom) ((CategoryTheory.ConcreteCategory.hom ((reducedCyclicCochainComplex R A M).d n (n + 1))) x) = (reducedCyclicHochschildCoboundary R A M n) ((CategoryTheory.ConcreteCategory.hom (reducedCyclicCochainComplexXIso R A M n).hom) x)

Under the canonical identifications of the terms, the differential of the reduced cyclic cochain complex is the reduced Hochschild coboundary.

@[reducible, inline]

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

Reduced cyclic cohomology of a unital algebra.

theorem TauCeti.mem_reducedCyclicCocycles_iff_complex (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) (phi : ↥(reducedCyclicCochains R A M n)) : phi ∈ reducedCyclicCocycles R A M n ↔ (CategoryTheory.ConcreteCategory.hom ((reducedCyclicCochainComplex R A M).d n (n + 1))) ((CategoryTheory.ConcreteCategory.hom (reducedCyclicCochainComplexXIso R A M n).inv) phi) = 0

A reduced cyclic cochain is a cocycle exactly when the differential of the reduced cyclic cochain complex kills the corresponding element of the complex.

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

The reduced cyclic cohomology class of a reduced cyclic cocycle.

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

Every reduced cyclic cohomology class is represented by a reduced cyclic cocycle.

@[simp]

theorem TauCeti.reducedCyclicCohomology.mk_eq_zero_iff (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) (phi : ↥(reducedCyclicCocycles R A M n)) : (mk R A M n) phi = 0 ↔ ↑phi ∈ reducedCyclicCoboundaries R A M n

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

theorem TauCeti.reducedCyclicCohomology.mk_eq_mk_iff (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) (phi psi : ↥(reducedCyclicCocycles R A M n)) : (mk R A M n) phi = (mk R A M n) psi ↔ ↑phi - ↑psi ∈ reducedCyclicCoboundaries R A M n

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

theorem TauCeti.cyclicCochainsMap_mem_reducedCyclicCochains {R : Type u_1} {A : Type u} {B : Type v} {M : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommGroup M] [Module R M] (f : A →ₐ[R] B) {n : ℕ} (phi : ↥(reducedCyclicCochains R B M n)) : (cyclicCochainsMap M f.toLinearMap n) ↑phi ∈ reducedCyclicCochains R A M n

Pullback along a unital algebra homomorphism preserves reduced cyclic cochains.

def TauCeti.reducedCyclicCochainsMap {R : Type u_1} {A : Type u} {B : Type v} (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommGroup M] [Module R M] (f : A →ₐ[R] B) (n : ℕ) : ↥(reducedCyclicCochains R B M n) →ₗ[R] ↥(reducedCyclicCochains R A M n)

Pullback of reduced cyclic cochains along a unital algebra homomorphism.

@[simp]

theorem TauCeti.coe_reducedCyclicCochainsMap_apply {R : Type u_1} {A : Type u} {B : Type v} {M : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommGroup M] [Module R M] (f : A →ₐ[R] B) (n : ℕ) (phi : ↥(reducedCyclicCochains R B M n)) : ↑((reducedCyclicCochainsMap M f n) phi) = (cyclicCochainsMap M f.toLinearMap n) ↑phi

The underlying cyclic cochain of a reduced pullback is ordinary pullback.

@[simp]

theorem TauCeti.reducedCyclicCochainsMap_id {R : Type u_1} {A : Type u} {M : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : reducedCyclicCochainsMap M (AlgHom.id R A) n = LinearMap.id

Pullback along the identity is the identity on reduced cyclic cochains.

theorem TauCeti.reducedCyclicCochainsMap_comp {R : Type u_1} {A : Type u} {B : Type v} {C : Type w} {M : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [AddCommGroup M] [Module R M] (f : A →ₐ[R] B) (g : B →ₐ[R] C) (n : ℕ) : reducedCyclicCochainsMap M (g.comp f) n = reducedCyclicCochainsMap M f n ∘ₗ reducedCyclicCochainsMap M g n

Pullback of reduced cyclic cochains is contravariantly functorial.

theorem TauCeti.reducedCyclicHochschildCoboundary_reducedCyclicCochainsMap {R : Type u_1} {A : Type u} {B : Type v} {M : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommGroup M] [Module R M] (f : A →ₐ[R] B) (n : ℕ) (phi : ↥(reducedCyclicCochains R B M n)) : (reducedCyclicHochschildCoboundary R A M n) ((reducedCyclicCochainsMap M f n) phi) = (reducedCyclicCochainsMap M f (n + 1)) ((reducedCyclicHochschildCoboundary R B M n) phi)

Reduced pullback commutes with the reduced Hochschild coboundary.

theorem TauCeti.reducedCyclicCochainsMap_mem_reducedCyclicCocycles {R : Type u_1} {A : Type u} {B : Type v} {M : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommGroup M] [Module R M] (f : A →ₐ[R] B) {n : ℕ} (phi : ↥(reducedCyclicCocycles R B M n)) : (reducedCyclicCochainsMap M f n) ↑phi ∈ reducedCyclicCocycles R A M n

Pullback along a unital algebra homomorphism sends reduced cyclic cocycles to reduced cyclic cocycles.

def TauCeti.reducedCyclicCochainComplexMap {R : Type u_1} {A B : Type u} (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommGroup M] [Module R M] (f : A →ₐ[R] B) : reducedCyclicCochainComplex R B M ⟶ reducedCyclicCochainComplex R A M

The cochain map between reduced cyclic complexes induced contravariantly by a unital algebra homomorphism.

theorem TauCeti.reducedCyclicCochainComplexMap_f {R : Type u_1} {A B : Type u} {M : Type u_2} [CommRing R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommGroup M] [Module R M] (f : A →ₐ[R] B) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((reducedCyclicCochainComplexMap M f).f n) (reducedCyclicCochainComplexXIso R A M n).hom = CategoryTheory.CategoryStruct.comp (reducedCyclicCochainComplexXIso R B M n).hom (ModuleCat.ofHom (reducedCyclicCochainsMap M f n))

The components of reduced pullback are the pullback maps on reduced cyclic cochains.

theorem TauCeti.reducedCyclicCochainComplexMap_f_assoc {R : Type u_1} {A B : Type u} {M : Type u_2} [CommRing R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommGroup M] [Module R M] (f : A →ₐ[R] B) (n : ℕ) {Z : ModuleCat R} (h : ↧↥(reducedCyclicCochains R A M n) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((reducedCyclicCochainComplexMap M f).f n) (CategoryTheory.CategoryStruct.comp (reducedCyclicCochainComplexXIso R A M n).hom h) = CategoryTheory.CategoryStruct.comp (reducedCyclicCochainComplexXIso R B M n).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (reducedCyclicCochainsMap M f n)) h)

The components of reduced pullback are the pullback maps on reduced cyclic cochains.

theorem TauCeti.reducedCyclicCochainComplexMap_f_apply {R : Type u_1} {A B : Type u} {M : Type u_2} [CommRing R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommGroup M] [Module R M] (f : A →ₐ[R] B) (n : ℕ) (x : ↑((reducedCyclicCochainComplex R B M).X n)) : (CategoryTheory.ConcreteCategory.hom (reducedCyclicCochainComplexXIso R A M n).hom) ((CategoryTheory.ConcreteCategory.hom ((reducedCyclicCochainComplexMap M f).f n)) x) = (reducedCyclicCochainsMap M f n) ((CategoryTheory.ConcreteCategory.hom (reducedCyclicCochainComplexXIso R B M n).hom) x)

The components of reduced pullback are the pullback maps on reduced cyclic cochains.

@[simp]

theorem TauCeti.reducedCyclicCochainComplexMap_id {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] : reducedCyclicCochainComplexMap M (AlgHom.id R A) = CategoryTheory.CategoryStruct.id (reducedCyclicCochainComplex R A M)

The identity homomorphism induces the identity reduced cochain map.

theorem TauCeti.reducedCyclicCochainComplexMap_comp {R : Type u_1} {A B C : Type u} {M : Type u_2} [CommRing R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [AddCommGroup M] [Module R M] (f : A →ₐ[R] B) (g : B →ₐ[R] C) : reducedCyclicCochainComplexMap M (g.comp f) = CategoryTheory.CategoryStruct.comp (reducedCyclicCochainComplexMap M g) (reducedCyclicCochainComplexMap M f)

Reduced cochain-complex pullback is contravariantly functorial.

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

The map on reduced cyclic cohomology induced contravariantly by a unital algebra homomorphism.

@[simp]

theorem TauCeti.reducedCyclicCohomology.map_mk {R : Type u_1} {A B : Type u} {M : Type u_2} [CommRing R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommGroup M] [Module R M] (f : A →ₐ[R] B) {n : ℕ} (phi : ↥(reducedCyclicCocycles R B M n)) : (CategoryTheory.ConcreteCategory.hom (map M f n)) ((mk R B M n) phi) = (mk R A M n) ⟨(reducedCyclicCochainsMap M f n) ↑phi, ⋯⟩

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

@[simp]

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

The identity homomorphism induces the identity on reduced cyclic cohomology.

theorem TauCeti.reducedCyclicCohomology.map_comp {R : Type u_1} {A B C : Type u} {M : Type u_2} [CommRing R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [AddCommGroup M] [Module R M] (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)

Reduced cyclic cohomology is contravariantly functorial.

def TauCeti.reducedCyclicCochainComplexι (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] : reducedCyclicCochainComplex R A M ⟶ cyclicCochainComplex R A M

The inclusion of the reduced cyclic cochain complex into the full cyclic cochain complex.

theorem TauCeti.reducedCyclicCochainComplexι_f (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((reducedCyclicCochainComplexι R A M).f n) (cyclicCochainComplexXIso R A M n).hom = CategoryTheory.CategoryStruct.comp (reducedCyclicCochainComplexXIso R A M n).hom (ModuleCat.ofHom (reducedCyclicCochains R A M n).subtype)

The components of the reduced-complex inclusion are the inclusions of reduced cochains.

theorem TauCeti.reducedCyclicCochainComplexι_f_assoc (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) {Z : ModuleCat R} (h : ↧↥(cyclicCochains R A M n) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((reducedCyclicCochainComplexι R A M).f n) (CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R A M n).hom h) = CategoryTheory.CategoryStruct.comp (reducedCyclicCochainComplexXIso R A M n).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (reducedCyclicCochains R A M n).subtype) h)

The components of the reduced-complex inclusion are the inclusions of reduced cochains.

theorem TauCeti.reducedCyclicCochainComplexι_f_apply (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) (x : ↑((reducedCyclicCochainComplex R A M).X n)) : (CategoryTheory.ConcreteCategory.hom (cyclicCochainComplexXIso R A M n).hom) ((CategoryTheory.ConcreteCategory.hom ((reducedCyclicCochainComplexι R A M).f n)) x) = ↑((CategoryTheory.ConcreteCategory.hom (reducedCyclicCochainComplexXIso R A M n).hom) x)

The components of the reduced-complex inclusion are the inclusions of reduced cochains.

noncomputable def TauCeti.reducedCyclicCohomology.toCyclic (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : reducedCyclicCohomology R A M n ⟶ cyclicCohomology R A M n

The map from reduced cyclic cohomology to cyclic cohomology induced by the inclusion of reduced cyclic cochains.

@[simp]

theorem TauCeti.reducedCyclicCohomology.toCyclic_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 : ℕ} (phi : ↥(reducedCyclicCocycles R A M n)) : (CategoryTheory.ConcreteCategory.hom (toCyclic R A M n)) ((mk R A M n) phi) = (cyclicCohomology.mk R A M n) ⟨↑↑phi, ⋯⟩

The class of a reduced cyclic cocycle maps to its class as a cyclic cocycle.

theorem TauCeti.reducedCyclicCohomology.toCyclic_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 : ℕ) (c : ↑(reducedCyclicCohomology R B M n)) : (CategoryTheory.ConcreteCategory.hom (toCyclic R A M n)) ((CategoryTheory.ConcreteCategory.hom (map M f n)) c) = (CategoryTheory.ConcreteCategory.hom (cyclicCohomology.map M (NonUnitalAlgHomClass.toNonUnitalAlgHom f) n)) ((CategoryTheory.ConcreteCategory.hom (toCyclic R B M n)) c)

The map to cyclic cohomology is natural for unital algebra homomorphisms.

def TauCeti.scalarCyclicRestrictionComplexMap (R A : Type u) (M : Type u_1) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] : cyclicCochainComplex R A M ⟶ cyclicCochainComplex R R M

Restriction of cyclic cochain complexes along the scalar inclusion.

theorem TauCeti.scalarCyclicRestrictionComplexMap_f (R A : Type u) (M : Type u_1) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((scalarCyclicRestrictionComplexMap R A M).f n) (cyclicCochainComplexXIso R R M n).hom = CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R A M n).hom (ModuleCat.ofHom (scalarCyclicRestriction R A M n))

The components of scalar restriction of cyclic cochain complexes are scalar restriction of cyclic cochains.

theorem TauCeti.scalarCyclicRestrictionComplexMap_f_assoc (R A : Type u) (M : Type u_1) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) {Z : ModuleCat R} (h : ↧↥(cyclicCochains R R M n) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((scalarCyclicRestrictionComplexMap R A M).f n) (CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R R M n).hom h) = CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R A M n).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (scalarCyclicRestriction R A M n)) h)

The components of scalar restriction of cyclic cochain complexes are scalar restriction of cyclic cochains.

theorem TauCeti.scalarCyclicRestrictionComplexMap_f_apply (R A : Type u) (M : Type u_1) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) (x : ↑((cyclicCochainComplex R A M).X n)) : (CategoryTheory.ConcreteCategory.hom (cyclicCochainComplexXIso R R M n).hom) ((CategoryTheory.ConcreteCategory.hom ((scalarCyclicRestrictionComplexMap R A M).f n)) x) = (scalarCyclicRestriction R A M n) ((CategoryTheory.ConcreteCategory.hom (cyclicCochainComplexXIso R A M n).hom) x)

The components of scalar restriction of cyclic cochain complexes are scalar restriction of cyclic cochains.

@[simp]

theorem TauCeti.reducedCyclicCochainComplexι_comp_scalarCyclicRestrictionComplexMap (R A : Type u) (M : Type u_1) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] : CategoryTheory.CategoryStruct.comp (reducedCyclicCochainComplexι R A M) (scalarCyclicRestrictionComplexMap R A M) = 0

The reduced-complex inclusion followed by scalar restriction is zero.

@[simp]

theorem TauCeti.reducedCyclicCochainComplexι_comp_scalarCyclicRestrictionComplexMap_assoc (R A : Type u) (M : Type u_1) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] {Z : CochainComplex (ModuleCat R) ℕ} (h : cyclicCochainComplex R R M ⟶ Z) : CategoryTheory.CategoryStruct.comp (reducedCyclicCochainComplexι R A M) (CategoryTheory.CategoryStruct.comp (scalarCyclicRestrictionComplexMap R A M) h) = CategoryTheory.CategoryStruct.comp 0 h

The reduced-complex inclusion followed by scalar restriction is zero.

noncomputable def TauCeti.reducedCyclicCochainComplexIsKernel (R A : Type u) (M : Type u_1) [CommRing R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (reducedCyclicCochainComplexι R A M) ⋯)

The reduced cyclic cochain complex is the kernel of scalar restriction on the full cyclic cochain complex.

@[simp]

theorem TauCeti.scalarCyclicRestriction_self (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommGroup M] [Module R M] (n : ℕ) : scalarCyclicRestriction R R M n = LinearMap.id

Restriction from the ground ring to its own scalar subalgebra is the identity.

@[simp]

theorem TauCeti.reducedCyclicCochains_self (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommGroup M] [Module R M] (n : ℕ) : reducedCyclicCochains R R M n = ⊥

Every reduced cyclic cochain on the ground ring is zero.

theorem TauCeti.isZero_reducedCyclicCochainComplex_self (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : CategoryTheory.Limits.IsZero (reducedCyclicCochainComplex R R M)

The reduced cyclic cochain complex of the ground ring is a zero object.

theorem TauCeti.isZero_reducedCyclicCohomology_self (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) : CategoryTheory.Limits.IsZero (reducedCyclicCohomology R R M n)

Reduced cyclic cohomology of the ground ring vanishes in every degree.

@[simp]

theorem TauCeti.reducedCyclicCochains_of_subsingleton (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [Subsingleton A] [AddCommGroup M] [Module R M] (n : ℕ) : reducedCyclicCochains R A M n = ⊥

Every reduced cyclic cochain on a zero algebra is zero.

theorem TauCeti.isZero_reducedCyclicCochainComplex_of_subsingleton (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [Subsingleton A] [AddCommGroup M] [Module R M] : CategoryTheory.Limits.IsZero (reducedCyclicCochainComplex R A M)

The reduced cyclic cochain complex of a zero algebra is a zero object.

theorem TauCeti.isZero_reducedCyclicCohomology_of_subsingleton (R : Type u_1) (A : Type u) (M : Type u_2) [CommRing R] [Semiring A] [Algebra R A] [Subsingleton A] [AddCommGroup M] [Module R M] (n : ℕ) : CategoryTheory.Limits.IsZero (reducedCyclicCohomology R A M n)

Reduced cyclic cohomology of a zero algebra vanishes in every degree.