Conditional.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra line 17
Source documentation
The finite condition used in the von Neumann type decomposition.
```
def FiniteAlgebra (N : Type u) [CStarAlgebra N] : Prop :=
…
```
def OAI.BoundedHochschild.KadisonRingrose.NoTypeII1Summand line 21
Source documentation
There is no nonzero finite central corner with no type I central part.
```
def NoTypeII1Summand (N : Type u) [CStarAlgebra N]
    [PartialOrder N] [StarOrderedRing N] : Prop :=
…
```
def OAI.BoundedHochschild.KadisonRingrose.TracialTypeII line 28
Source documentation
Precisely the trace data needed by the proved tracial primitive theorem.
```
def TracialTypeII (N : Type u) [CStarAlgebra N]
    [PartialOrder N] [StarOrderedRing N] : Prop :=
…
```
structure OAI.BoundedHochschild.KadisonRingrose.CentralDecomposition line 37
Source documentation
The structural input supplies one exceptional corner and tracial II₁ corners.
```
structure CentralDecomposition (M : Type u) [CStarAlgebra M]
    [PartialOrder M] [StarOrderedRing M] where
…
```
def OAI.BoundedHochschild.KadisonRingrose.CentralDecompositionInput line 49
Source documentation
Blackadar's central type decomposition, specialized to the application.
```
def CentralDecompositionInput (M : Type u) [CStarAlgebra M]
    [PartialOrder M] [StarOrderedRing M] : Prop :=
…
```
def OAI.BoundedHochschild.KadisonRingrose.ClassicalVanishingInput line 53
theorem OAI.BoundedHochschild.KadisonRingrose.TracialTypeII.primitive line 60

theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_published_inputs line 75

Source documentation

The manuscript's global assembly, conditional only on the two cited inputs.

theorem primitive_of_published_inputs (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hdecomp : CentralDecompositionInput 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 := by
…

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

theorem OAI.BoundedHochschild.KadisonRingrose.vanishing_of_published_inputs line 114
Source documentation
Theorem 1.1, including vanishing of the actual-image cohomology quotient.
```
theorem vanishing_of_published_inputs [WStarAlgebra M]
    (hdecomp : CentralDecompositionInput M) (hclassical : ClassicalVanishingInput.{u})
    (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.KadisonRingrose.CentralDecompositionInput, OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differential, OAI.BoundedHochschild.incomingDifferential, OAI.BoundedHochschild.Cohomology