CenterAlgebra.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Recovering scalar centre from central projections

The centre is represented as the intersection with the concrete commutant. Spectral approximation in this von Neumann algebra reduces scalarity of its whole algebra to triviality of its projections.

def OAI.KadisonKastler.vonNeumannIntersection line 21
Source documentation
The intersection of two concrete von Neumann algebras.
```
def vonNeumannIntersection (M N : VonNeumannAlgebra H) : VonNeumannAlgebra H where
…
```
def OAI.KadisonKastler.concreteCenter line 39
Source documentation
The concrete centre, retaining its von Neumann structure.
```
def concreteCenter (N : VonNeumannAlgebra H) : VonNeumannAlgebra H :=
…
```

theorem OAI.KadisonKastler.scalar_center_of_trivial_central_projections line 44

Source documentation

Spectral approximation upgrades trivial central projections to scalar centre. No finiteness or trace is needed for this upgrade.

theorem scalar_center_of_trivial_central_projections (N : VonNeumannAlgebra H)
    (hproj : ∀ q : Algebra N, IsStarProjection q →
      (∀ a : Algebra N, a * q = q * a) → q = 0 ∨ q = 1)
    (c : Algebra N) (hc : ∀ a : Algebra N, a * c = c * a) :
    ∃ z : ℂ, c = z • (1 : Algebra N) := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.scalar_center_of_near_II1 line 84
Source documentation
The nearby algebra has scalar centre; the faithful trace is constructed from the given concrete II₁ factor.
```
theorem scalar_center_of_near_II1 {M N : VonNeumannAlgebra H}
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hgap : kkDistance M N < 1 / 10) :
    ∀ c : Algebra N, (∀ a : Algebra N, a * c = c * a) →
      ∃ z : ℂ, c = z • (1 : Algebra N) := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.finite_factor_of_near_II1 line 101

Source documentation

The full finite-neighbor conclusion for an initial II₁ factor: the nearby algebra is finite and has scalar centre.

theorem finite_factor_of_near_II1 {M N : VonNeumannAlgebra H}
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hgap : kkDistance M N < 1 / 10) :
    (∀ c : Algebra N, (∀ a : Algebra N, a * c = c * a) →
      ∃ z : ℂ, c = z • (1 : Algebra N)) ∧
    (∀ v : Algebra N, star v * v = 1 → v * star v = 1) := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.Algebra