Main.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.BoundedHochschild.KadisonRingrose.bounded_primitive line 79

Source documentation

Every bounded higher cocycle on a von Neumann algebra has a bounded primitive. No complete-boundedness or normality assumption is required.

theorem bounded_primitive
    {M X : Type u} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M]
    [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X]
    (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) {n : ℕ} (f : Cochain M (n + 2))
    (hf : differential f = 0) :
    ∃ g : Cochain M (n + 1), differential g = f := by
…

Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differential

theorem OAI.BoundedHochschild.KadisonRingrose.vanishing line 93
Source documentation
Theorem 1.1: ordinary bounded Hochschild cohomology vanishes in every degree at least two, with the actual image of the differential.
```
theorem vanishing
    {M : Type u} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M] [WStarAlgebra M]
    (k : ℕ) (hk : 2 ≤ k) :
    (∀ f : Cochain M k, differential f = 0 →
      ∃ g : Cochain M (k - 1), incomingDifferential M k g = f) ∧
    Subsingleton (Cohomology M k) := by
…
```
Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differential, OAI.BoundedHochschild.incomingDifferential, OAI.BoundedHochschild.Cohomology

theorem OAI.BoundedHochschild.KadisonRingrose.normal_tracial_primitive line 107

Source documentation

A separately normal higher cocycle on a tracial type II₁ algebra has an actual bounded primitive with norm at most its own norm.

theorem normal_tracial_primitive
    {M X : Type u} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M]
    [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X]
    (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (τ : M →ₚ[ℂ] ℂ)
    (hτ : TraceInPredual e τ) (htr : ∀ a b : M, τ (a * b) = τ (b * a))
    (hfaith : ∀ a : M, τ (star a * a) = 0 → a = 0) (h1 : τ 1 = 1)
    (hII : PopaTypeII.NoTypeICentralPart M) {n : ℕ}
    (f : Cochain M (n + 2)) (hf : differential f = 0)
    (hn : SeparatelyNormal e f) :
    ∃ g : Cochain M (n + 1), ‖g‖ ≤ ‖f‖ ∧ differential g = f := by
…

Mentions: OAI.BoundedHochschild.TraceInPredual, OAI.PopaTypeII.NoTypeICentralPart, OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differential, OAI.BoundedHochschild.SeparatelyNormal