Documentation

TauCeti.RingTheory.CyclicCohomology.OddPairing.Relative

The odd pairing of a nonunital algebra #

Let A be a possibly nonunital complex algebra and A⁺ = Unitization ℂ A its forced unitization. The cyclic cohomology of A is the relative cyclic cohomology HCⁿ(A; M), the cohomology of the cyclic cochains on A⁺ vanishing when all arguments are scalar, and its K₁ is the relative K₁, the kernel of K₁(A⁺) → K₁(ℂ). This file defines Connes' odd pairing between them: a relative class x ∈ K₁(A⁺) pairs with c ∈ HC²ᵐ⁺¹(A; M) through Connes' odd pairing of K₁(A⁺) with the image of c in the cyclic cohomology HC²ᵐ⁺¹(A⁺; M) of the forced unitization.

For an invertible matrix u over A⁺ with a relative class and a relative cyclic cocycle φ, the pairing is Connes' formula (1 + i)⁻¹ 2⁻ⁿ Γ(n/2 + 1)⁻¹ (φ#Tr)(u⁻¹ - 1, u - 1, …, u⁻¹ - 1, u - 1) with n = 2m + 1.

The matrix extension of a relative cyclic cochain vanishes when all its arguments are scalar matrices, so the classes of scalar matrices pair trivially with relative cyclic cohomology. Since K₁(A⁺) is the product of relative K₁ and the classes of scalar matrices, the pairing of an arbitrary class of A⁺ with a relative cyclic class is the pairing of its relative part: no information is lost by restricting to relative K₁. The pairing is natural for homomorphisms of nonunital algebras.

Main definitions #

Main results #

References #

source
@[simp]
theorem TauCeti.AlgebraicK1.oddPairing_map_algebraMap_toUnitization_eq_zero {A : Type u_1} {M : Type u_2} [NonUnitalRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [AddCommGroup M] [Module ℂ M] (m : ℕ) (y : AlgebraicK1 ℂ) (c : ↑(relativeCyclicCohomology ℂ A M (2 * m + 1))) :
(Multiplicative.toAdd ((oddPairing (Unitization ℂ A) M m) ((map (algebraMap ℂ (Unitization ℂ A))) y))) ((CategoryTheory.ConcreteCategory.hom (reducedCyclicCohomology.toCyclic ℂ (Unitization ℂ A) M (2 * m + 1))) c) = 0

Scalar classes pair trivially: the image in K₁(A⁺) of a class of K₁(ℂ) pairs to zero with every relative cyclic cohomology class.

source
noncomputable def TauCeti.relativeAlgebraicK1.oddPairing (A : Type u_1) (M : Type u_2) [NonUnitalRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [AddCommGroup M] [Module ℂ M] (m : ℕ) :
↥(relativeAlgebraicK1 ℂ A) →* Multiplicative (↑(relativeCyclicCohomology ℂ A M (2 * m + 1)) →ₗ[ℂ] M)

Connes' odd pairing of relative K₁ with relative cyclic cohomology in degree 2m + 1: a relative class of K₁(A⁺) is sent to the functional c ↦ ⟨x, c⟩ on HC²ᵐ⁺¹(A; M), Connes' odd pairing of x with the image of c in the cyclic cohomology of the forced unitization. It is a homomorphism to the additive group of functionals, written multiplicatively.

Instances For
    source
    theorem TauCeti.relativeAlgebraicK1.oddPairing_apply {A : Type u_1} {M : Type u_2} [NonUnitalRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [AddCommGroup M] [Module ℂ M] (m : ℕ) (x : ↥(relativeAlgebraicK1 ℂ A)) (c : ↑(relativeCyclicCohomology ℂ A M (2 * m + 1))) :
    (Multiplicative.toAdd ((oddPairing A M m) x)) c = (Multiplicative.toAdd ((AlgebraicK1.oddPairing (Unitization ℂ A) M m) ↑x)) ((CategoryTheory.ConcreteCategory.hom (reducedCyclicCohomology.toCyclic ℂ (Unitization ℂ A) M (2 * m + 1))) c)

    The odd pairing of a relative class x with a relative cyclic class c is the odd pairing of x with the image of c in the cyclic cohomology of the forced unitization.

    source
    theorem TauCeti.relativeAlgebraicK1.oddPairing_mk_mk {A : Type u_1} {M : Type u_2} [NonUnitalRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [AddCommGroup M] [Module ℂ M] (m n : ℕ) (u : GL (Fin n) (Unitization ℂ A)) (hu : (AlgebraicK1.mk (Unitization ℂ A) n) u ∈ relativeAlgebraicK1 ℂ A) (φ : ↥(reducedCyclicCocycles ℂ (Unitization ℂ A) M (2 * m + 1))) :
    (Multiplicative.toAdd ((oddPairing A M m) ⟨(AlgebraicK1.mk (Unitization ℂ A) n) u, hu⟩)) ((reducedCyclicCohomology.mk ℂ (Unitization ℂ A) M (2 * m + 1)) φ) = ((1 + Complex.I)⁻¹ * (2 ^ (2 * m + 1))⁻¹ * (↑(Real.Gamma ((2 * ↑m + 1) / 2 + 1)))⁻¹) • ((matrixCochainExtension (Fin n) (2 * m + 1)) ↑↑↑φ) fun (k : Fin (2 * m + 1 + 1)) => if Even ↑k then ↑u⁻¹ - 1 else ↑u - 1

    Connes' formula for the relative odd pairing: an invertible matrix u over A⁺ with a relative class pairs with the class of a relative cyclic cocycle φ of degree n = 2m + 1 as (1 + i)⁻¹ 2⁻ⁿ Γ(n/2 + 1)⁻¹ (φ#Tr)(u⁻¹ - 1, u - 1, …, u⁻¹ - 1, u - 1).

    source
    @[simp]
    theorem TauCeti.relativeAlgebraicK1.oddPairing_projection {A : Type u_1} {M : Type u_2} [NonUnitalRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [AddCommGroup M] [Module ℂ M] (m : ℕ) (x : AlgebraicK1 (Unitization ℂ A)) (c : ↑(relativeCyclicCohomology ℂ A M (2 * m + 1))) :
    (Multiplicative.toAdd ((oddPairing A M m) ((projection ℂ A) x))) c = (Multiplicative.toAdd ((AlgebraicK1.oddPairing (Unitization ℂ A) M m) x)) ((CategoryTheory.ConcreteCategory.hom (reducedCyclicCohomology.toCyclic ℂ (Unitization ℂ A) M (2 * m + 1))) c)

    The pairing of an arbitrary class of A⁺ sees only its relative part: a class x of A⁺ pairs with a relative cyclic class as its relative part x · s(ε(x))⁻¹ does.

    source
    theorem TauCeti.relativeAlgebraicK1.oddPairing_map {A : Type u_1} {M : Type u_2} [NonUnitalRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [AddCommGroup M] [Module ℂ M] {B : Type u_1} [NonUnitalRing B] [Module ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B] (f : A →ₙₐ[ℂ] B) (m : ℕ) (x : ↥(relativeAlgebraicK1 ℂ A)) :
    Multiplicative.toAdd ((oddPairing B M m) ((map f) x)) = Multiplicative.toAdd ((oddPairing A M m) x) ∘ₗ ModuleCat.Hom.hom (relativeCyclicCohomology.map M f (2 * m + 1))

    Naturality of the relative odd pairing: for a homomorphism of nonunital algebras f : A →ₙₐ[ℂ] B, the image of a relative class x pairs with a relative cyclic class of B as x pairs with the pullback of the class along f.