Relative cyclic cohomology of a nonunital algebra

For a nonunital algebra A, its cyclic cohomology is not the cohomology of the cyclic cochains on A itself. It is the relative theory of the forced unitization Unitization R A with respect to its scalar subalgebra, that is, the reduced cyclic cohomology of Unitization R A (TauCeti.reducedCyclicCohomology). In degree n, the relative cyclic cochains are the kernel of restriction along the scalar inclusion

R → Unitization R A,

which is the module of reduced cyclic cochains of the forced unitization, and the relative cyclic cochain complex is its reduced cyclic cochain complex. Consequently the reduced API (Hochschild coboundary, functoriality, inclusion into the full cyclic complex, identification as the kernel of scalar restriction) applies verbatim to the relative theory.

What is specific to the forced unitization is the augmentation Unitization R A → R, which splits scalar restriction; this records explicitly the contravariant splitting used by the relative theory. The cocycles, coboundaries, classes and the map to the cyclic cohomology of the forced unitization are the reduced ones (TauCeti.reducedCyclicCocycles, TauCeti.reducedCyclicCohomology.mk, TauCeti.reducedCyclicCohomology.toCyclic) at Unitization R A, and pullback along a homomorphism of nonunital algebras is reduced pullback along the induced map of forced unitizations.

Main definitions

• TauCeti.relativeCyclicCochains: the reduced cyclic cochains of the forced unitization.
• TauCeti.unitizationAugmentationPullback: pullback along the augmentation, a splitting of scalar restriction on the forced unitization.
• TauCeti.relativeCyclicCochainComplex: the relative cyclic cochain complex.
• TauCeti.relativeCyclicCohomology: the relative cyclic cohomology of a nonunital algebra.
• TauCeti.relativeCyclicCohomology.map: pullback along a homomorphism of nonunital algebras.
• TauCeti.relativeCyclicCohomology.toCyclic_map_unitization: naturality of the map to the cyclic cohomology of the forced unitization.

References

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

def TauCeti.unitizationAugmentationPullback (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) : ↥(cyclicCochains R R M n) →ₗ[R] ↥(cyclicCochains R (Unitization R A) M n)

Pullback of scalar cyclic cochains along the augmentation of the forced unitization.

@[simp]

theorem TauCeti.unitizationAugmentationPullback_apply (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) (phi : ↥(cyclicCochains R R M n)) (a : Fin (n + 1) → Unitization R A) : ↑((unitizationAugmentationPullback R A M n) phi) a = ↑phi fun (i : Fin (n + 1)) => (a i).toProd.1

Pullback along the augmentation evaluates a scalar cochain on the scalar components.

@[simp]

theorem TauCeti.scalarCyclicRestriction_comp_unitizationAugmentationPullback (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) : scalarCyclicRestriction R (Unitization R A) M n ∘ₗ unitizationAugmentationPullback R A M n = LinearMap.id

Pullback along the augmentation is a right inverse to scalar restriction on the forced unitization.

theorem TauCeti.scalarCyclicRestriction_unitization_surjective (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) : Function.Surjective ⇑(scalarCyclicRestriction R (Unitization R A) M n)

Scalar restriction on the forced unitization is surjective, split by pullback along the augmentation.

@[reducible, inline]

abbrev TauCeti.relativeCyclicCochains (R : Type u_1) (A : Type u) (M : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) : Submodule R ↥(cyclicCochains R (Unitization R A) M n)

The relative cyclic n-cochains of a nonunital algebra: the reduced cyclic cochains of its forced unitization, that is, cyclic cochains on the forced unitization which vanish when all arguments are scalar.

@[reducible, inline]

abbrev TauCeti.relativeCyclicCochainComplex (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 relative cyclic cochain complex of a nonunital algebra: the reduced cyclic cochain complex of its forced unitization, whose degree-n term is the kernel of scalar restriction on cyclic cochains of the forced unitization.

@[reducible, inline]

noncomputable abbrev TauCeti.relativeCyclicCohomology (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 : ℕ) : ModuleCat R

The relative cyclic cohomology of a nonunital algebra: the reduced cyclic cohomology of its forced unitization, the cohomology of the kernel of scalar restriction on the cyclic cochain complex of the forced unitization.

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

The map on relative cyclic cohomology induced contravariantly by a homomorphism of nonunital algebras: the map on reduced cyclic cohomology induced by the induced map of forced unitizations.

@[simp]

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

The induced map sends the class of a relative cocycle to the class of its pullback along the induced map of forced unitizations.

@[simp]

theorem TauCeti.relativeCyclicCohomology.map_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] (n : ℕ) : map M (NonUnitalAlgHom.id R A) n = CategoryTheory.CategoryStruct.id (relativeCyclicCohomology R A M n)

The identity homomorphism induces the identity on relative cyclic cohomology.

theorem TauCeti.relativeCyclicCohomology.map_comp {R : Type u_1} {A B C : Type u} {M : Type u_2} [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [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] [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)

Relative cyclic cohomology is contravariantly functorial.

theorem TauCeti.relativeCyclicCohomology.toCyclic_map_unitization {R : Type u_1} {A : Type u} {M : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] {B : Type u} [NonUnitalRing B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) (n : ℕ) (c : ↑(relativeCyclicCohomology R B M n)) : (CategoryTheory.ConcreteCategory.hom (reducedCyclicCohomology.toCyclic R (Unitization R A) M n)) ((CategoryTheory.ConcreteCategory.hom (map M f n)) c) = (CategoryTheory.ConcreteCategory.hom (cyclicCohomology.map M (NonUnitalAlgHomClass.toNonUnitalAlgHom (Unitization.map f)) n)) ((CategoryTheory.ConcreteCategory.hom (reducedCyclicCohomology.toCyclic R (Unitization R B) M n)) c)

The map to the cyclic cohomology of the forced unitization is natural for homomorphisms of nonunital algebras.

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

Pullback of cyclic cochain complexes along the augmentation.

theorem TauCeti.unitizationAugmentationPullbackComplexMap_f (R A : Type u) (M : Type u_1) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((unitizationAugmentationPullbackComplexMap R A M).f n) (cyclicCochainComplexXIso R (Unitization R A) M n).hom = CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R R M n).hom (ModuleCat.ofHom (unitizationAugmentationPullback R A M n))

Under the identifications cyclicCochainComplexXIso, the components of pullback along the augmentation are pullback of cyclic cochains along the augmentation.

theorem TauCeti.unitizationAugmentationPullbackComplexMap_f_assoc (R A : Type u) (M : Type u_1) [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 (Unitization R A) M n) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((unitizationAugmentationPullbackComplexMap R A M).f n) (CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R (Unitization R A) M n).hom h) = CategoryTheory.CategoryStruct.comp (cyclicCochainComplexXIso R R M n).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (unitizationAugmentationPullback R A M n)) h)

Under the identifications cyclicCochainComplexXIso, the components of pullback along the augmentation are pullback of cyclic cochains along the augmentation.

theorem TauCeti.unitizationAugmentationPullbackComplexMap_f_apply (R A : Type u) (M : Type u_1) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] (n : ℕ) (x : ↑((cyclicCochainComplex R R M).X n)) : (CategoryTheory.ConcreteCategory.hom (cyclicCochainComplexXIso R (Unitization R A) M n).hom) ((CategoryTheory.ConcreteCategory.hom ((unitizationAugmentationPullbackComplexMap R A M).f n)) x) = (unitizationAugmentationPullback R A M n) ((CategoryTheory.ConcreteCategory.hom (cyclicCochainComplexXIso R R M n).hom) x)

Under the identifications cyclicCochainComplexXIso, the components of pullback along the augmentation are pullback of cyclic cochains along the augmentation.

@[simp]

theorem TauCeti.unitizationAugmentationPullbackComplexMap_comp_scalarCyclicRestrictionComplexMap (R A : Type u) (M : Type u_1) [CommRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [AddCommGroup M] [Module R M] : CategoryTheory.CategoryStruct.comp (unitizationAugmentationPullbackComplexMap R A M) (scalarCyclicRestrictionComplexMap R (Unitization R A) M) = CategoryTheory.CategoryStruct.id (cyclicCochainComplex R R M)

Pullback along the augmentation splits scalar restriction on the forced unitization as a cochain map.