Cyclic cohomology, spectral triples and noncommutative tori
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremTauCeti.quasiIso_cyclicCochainComplexToTotal#
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.
TauCeti.quasiIso_cyclicCochainComplexToTotal.{u, u_1, u_2} (R : Type u_1) (A : Type u)
(M : Type u_2) [CommRing R] [NonUnitalSemiring A] [_root_.Module R A] [IsScalarTower R A A]
[SMulCommClass R A A] [AddCommGroup M] [_root_.Module R M] [Algebra ℚ R] :
QuasiIso (TauCeti.cyclicCochainComplexToTotal R A M)
DefinitionTauCeti.cyclicCohomology.selfEquiv#
If multiplication by 2 is injective on M, then HCⁿ(R; M) ≅ M in every even degree n,
by the class of the product cochain. In particular HC²ᵏ(ℂ) ≅ ℂ.
TauCeti.cyclicCohomology.selfEquiv.{u, u_1} (R : Type u) (M : Type u_1) [CommRing R]
[AddCommGroup M] [_root_.Module R M] {n : ℕ} (hn : Even n) (h2 : IsSMulRegular M 2) :
M ≃ₗ[R] ↑(TauCeti.cyclicCohomology R R M n)
TheoremTauCeti.isZero_cyclicCohomology_self_of_odd#
The cyclic cohomology of the ground ring vanishes in odd degree.
TauCeti.isZero_cyclicCohomology_self_of_odd.{u, u_1} (R : Type u) (M : Type u_1) [CommRing R]
[AddCommGroup M] [_root_.Module R M] {n : ℕ} (hn : Odd n) :
CategoryTheory.Limits.IsZero (TauCeti.cyclicCohomology R R M n)
TheoremConjugation invariance of the even pairing#
Conjugating an idempotent by a unit does not change its even pairing with cyclic cohomology.
TauCeti.cyclicCohomology.evenPairing_units_conj.{u_1, u_2, u_3} {R : Type u_1} {A : Type u_2}
{M : Type u_3} [Field R] [CharZero R] [Ring A] [Algebra R A] [AddCommGroup M] [_root_.Module R M]
(u : Aˣ) {e : A} (he : IsIdempotentElem e) (hue : IsIdempotentElem (↑u * e * ↑u⁻¹)) (m : ℕ) :
TauCeti.cyclicCohomology.evenPairing (↑u * e * ↑u⁻¹) hue m =
TauCeti.cyclicCohomology.evenPairing e he m
Lean
Formalized in Tau Ceti as TauCeti.cyclicCohomology.evenPairing_units_conj.
Sources
DefinitionConnes' odd pairing#
Connes' odd pairing ⟨[u], [φ]⟩ = (1 + i)⁻¹ 2⁻ⁿ Γ(n/2 + 1)⁻¹ φ(u⁻¹ - 1, u - 1, …, u - 1)
of an invertible u with cyclic cohomology classes of odd degree n = 2m + 1.
TauCeti.cyclicCohomology.oddPairing.{u_1, u_2} {A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A]
[AddCommGroup M] [_root_.Module ℂ M] (u : Aˣ) (m : ℕ) :
↑(TauCeti.cyclicCohomology ℂ A M (2 * m + 1)) →ₗ[ℂ] M
Used by 2
TheoremStabilization of the odd pairing#
enlarging an invertible matrix u to the block diagonal
matrix u ⊕ 1 does not change its odd pairing.
TauCeti.cyclicCohomology.oddPairing_matrixExtension_of_val_eq_fromBlocks_one.{u_1, u_2, u_3, u_4}
{A : Type u_1} {M : Type u_2} [Ring A] [Algebra ℂ A] [AddCommGroup M] [_root_.Module ℂ M]
{ι : Type u_3} {κ : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
{w : (Matrix (ι ⊕ κ) (ι ⊕ κ) A)ˣ} {u : (Matrix ι ι A)ˣ} (hw : ↑w = Matrix.fromBlocks (↑u) 0 0 1)
(m : ℕ) (c : ↑(TauCeti.cyclicCohomology ℂ A M (2 * m + 1))) :
(TauCeti.cyclicCohomology.oddPairing w m)
((TauCeti.cyclicCohomology.matrixExtension M (ι ⊕ κ) (2 * m + 1)) c) =
(TauCeti.cyclicCohomology.oddPairing u m)
((TauCeti.cyclicCohomology.matrixExtension M ι (2 * m + 1)) c)
Lean
Formalized in Tau Ceti as TauCeti.cyclicCohomology.oddPairing_matrixExtension_of_val_eq_fromBlocks_one.
Sources
- Tau Ceti documentation:
TauCeti.cyclicCohomology.oddPairing_matrixExtension_of_val_eq_fromBlocks_one - Source of
TauCeti.cyclicCohomology.oddPairing_matrixExtension_of_val_eq_fromBlocks_onein TauCeti/RingTheory/CyclicCohomology/OddPairing/Basic.lean - Tau Ceti roadmap status: Cyclic cohomology, spectral triples and noncommutative tori
Uses 2 · Used by 1
DefinitionTauCeti.cycleCocycle#
The character of a cycle, as a cyclic cocycle.
TauCeti.cycleCocycle.{u_1, u_2, u_3, u_4} {R : Type u_1} {A : Type u_2} {Ω : Type u_3}
{M : Type u_4} [CommRing R] [NonUnitalSemiring A] [_root_.Module R A] [Ring Ω] [Algebra R Ω]
[AddCommGroup M] [_root_.Module R M] {d : Ω →ₗ[R] Ω} {τ : Ω →ₗ[R] M} {ρ : A →ₙₐ[R] Ω} {n : ℕ}
{𝒜 : ℤ → Submodule R Ω} [GradedAlgebra 𝒜] [IsScalarTower R A A] [SMulCommClass R A A]
(hd : TauCeti.IsDGAlgebra 𝒜 d) (hρ : ∀ (a : A), ρ a ∈ 𝒜 0)
(hτ : TauCeti.IsClosedGradedTrace 𝒜 d n τ) : ↥(TauCeti.cyclicCocycles R A M n)
AbbreviationTauCeti.relativeCyclicCohomology#
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.
TauCeti.relativeCyclicCohomology.{u, u_1, u_2} (R : Type u_1) (A : Type u) (M : Type u_2)
[CommRing R] [NonUnitalSemiring A] [_root_.Module R A] [IsScalarTower R A A] [SMulCommClass R A A]
[AddCommGroup M] [_root_.Module R M] (n : ℕ) : ModuleCat R
Used by 1
DefinitionTauCeti.cyclicCohomology.matrixExtension#
The map HCⁿ(A; M) → HCⁿ(Matrix ι ι A; M) on cyclic cohomology induced by matrix extension of
cyclic cocycles.
TauCeti.cyclicCohomology.matrixExtension.{u_4, u_5, u_6, u_7} {R : Type u_4} {A : Type u_5}
(M : Type u_6) [AddCommGroup M] (ι : Type u_7) [Fintype ι] (n : ℕ) [CommRing R]
[_root_.Module R M] [Ring A] [Algebra R A] [DecidableEq ι] :
↑(TauCeti.cyclicCohomology R A M n) →ₗ[R] ↑(TauCeti.cyclicCohomology R (Matrix ι ι A) M n)
Used by 2
DefinitionTauCeti.continuousCyclicCochains#
The submodule of jointly continuous cochains satisfying the signed cyclic relation.
TauCeti.continuousCyclicCochains.{u_1, u_2, u_3} (R : Type u_1) (A : Type u_2) (M : Type u_3)
[Semiring R] [AddCommMonoid A] [_root_.Module R A] [TopologicalSpace A] [AddCommGroup M]
[_root_.Module R M] [SMulCommClass R R M] [TopologicalSpace M] [ContinuousConstSMul R M]
[ContinuousAdd M] (n : ℕ) : Submodule R (A [×n + 1]→L[R] M)
TheoremTauCeti.continuous_continuousConnesB#
Connes' operator is continuous for bounded convergence of cochains.
TauCeti.continuous_continuousConnesB.{u_1, u_2, u_3} (𝕜 : Type u_1) (A : Type u_2) (M : Type u_3)
[NormedField 𝕜] [AddCommGroup A] [_root_.Module 𝕜 A] [TopologicalSpace A] [ContinuousSMul 𝕜 A]
[One A] [AddCommGroup M] [_root_.Module 𝕜 M] [TopologicalSpace M] [IsTopologicalAddGroup M]
[ContinuousConstSMul 𝕜 M] (n : ℕ) : Continuous ⇑(TauCeti.continuousConnesB 𝕜 A M n)
TheoremConnes' 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).
TauCeti.relativeAlgebraicK1.oddPairing_mk_mk.{u_1, u_2} {A : Type u_1} {M : Type u_2}
[NonUnitalRing A] [_root_.Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [AddCommGroup M]
[_root_.Module ℂ M] (m n : ℕ) (u : GL (Fin n) (Unitization ℂ A))
(hu : (TauCeti.AlgebraicK1.mk (Unitization ℂ A) n) u ∈ TauCeti.relativeAlgebraicK1 ℂ A)
(φ : ↥(TauCeti.reducedCyclicCocycles ℂ (Unitization ℂ A) M (2 * m + 1))) :
(Multiplicative.toAdd
((TauCeti.relativeAlgebraicK1.oddPairing A M m)
⟨(TauCeti.AlgebraicK1.mk (Unitization ℂ A) n) u, hu⟩))
((TauCeti.reducedCyclicCohomology.mk ℂ (Unitization ℂ A) M (2 * m + 1)) φ) =
((1 + Complex.I)⁻¹ * (2 ^ (2 * m + 1))⁻¹ * (↑(Real.Gamma ((2 * ↑m + 1) / 2 + 1)))⁻¹) •
((TauCeti.matrixCochainExtension (Fin n) (2 * m + 1)) ↑↑↑φ) fun k =>
if Even ↑k then ↑u⁻¹ - 1 else ↑u - 1
Uses 4
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.