CentralVanishing.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Vanishing for central partitions into proved cases

This is an unconditional application of the tracial argument and the full operator algebra homotopy. Its structural hypothesis gives actual central corners, each either faithfully normally tracial of type II₁ or explicitly isomorphic to a full operator algebra. It makes no cohomological assumptions. It does not assert that every von Neumann algebra has such a partition.

def OAI.BoundedHochschild.KadisonRingrose.FullOperatorAlgebra line 27
Source documentation
An actual presentation as a full algebra of Hilbert-space operators.
```
def FullOperatorAlgebra (N : Type u) [CStarAlgebra N] : Prop :=
…
```
theorem OAI.BoundedHochschild.KadisonRingrose.FullOperatorAlgebra.primitive line 31
structure OAI.BoundedHochschild.KadisonRingrose.TracialOperatorPartition line 43
Source documentation
A central partition into two classes for which the primitive is proved.
```
structure TracialOperatorPartition (M : Type u) [CStarAlgebra M]
    [PartialOrder M] [StarOrderedRing M] where
…
```

theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_tracial_operator_partition line 58

Source documentation

Uniform primitives assemble across an arbitrary, possibly uncountable center.

theorem primitive_of_tracial_operator_partition
    (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (D : TracialOperatorPartition M)
    {n : ℕ} (f : Cochain M (n + 2)) (hf : ∀ x, differentialValue f x = 0) :
    ∃ g : Cochain M (n + 1), ‖g‖ ≤ 12 * ‖f‖ + ((n + 1 : ℕ) : ℝ) * ‖f‖ ∧
      ∀ x, differentialValue g x = f x := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.TracialOperatorPartition, OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue

theorem OAI.BoundedHochschild.KadisonRingrose.vanishing_of_tracial_operator_partition line 88
Source documentation
Actual-image cohomology vanishes under this structural, non-cohomological hypothesis.
```
theorem vanishing_of_tracial_operator_partition [WStarAlgebra M]
    (D : TracialOperatorPartition M) (k : ℕ) (hk : 2 ≤ k) :
    Subsingleton (Cohomology M k) := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.TracialOperatorPartition, OAI.BoundedHochschild.Cohomology