TracialCoverReduction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Reduction of the structural input to local tracial corners

The global central decomposition follows from a local consequence of the finite von Neumann algebra trace theorem: every nonzero finite central type-II corner contains a nonzero faithfully normally tracial central corner. The maximal-family argument, the exceptional summand, and all corner identifications are proved here. Only the local trace existence statement remains an input (Blackadar, III.2.5.7--8).

def OAI.BoundedHochschild.KadisonRingrose.LocalTracialCutInput line 30
Source documentation
The remaining local consequence of the finite-algebra trace theorem.
```
def LocalTracialCutInput (M : Type u) [CStarAlgebra M]
    [PartialOrder M] [StarOrderedRing M] : Prop :=
…
```
theorem OAI.BoundedHochschild.KadisonRingrose.centralDecompositionInput_of_local_tracial_cuts line 42
Source documentation
The global structural input is reduced to local tracial existence, with the maximal central partition constructed from the given predual.
```
theorem centralDecompositionInput_of_local_tracial_cuts
    (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (hlocal : LocalTracialCutInput M) :
    CentralDecompositionInput M := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.LocalTracialCutInput, OAI.BoundedHochschild.KadisonRingrose.CentralDecompositionInput
theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_local_tracial_cuts line 104
Source documentation
The global theorem now requires only the local trace construction and the classical non-II₁ vanishing theorem.
```
theorem primitive_of_local_tracial_cuts (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hlocal : LocalTracialCutInput M) (hclassical : ClassicalVanishingInput.{u})
    {n : ℕ} (f : Cochain M (n + 2)) (hf : ∀ x, differentialValue f x = 0) :
    ∃ g : Cochain M (n + 1), ∀ x, differentialValue g x = f x :=
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.LocalTracialCutInput, OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue