PublishedFiniteType.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The type-II part of the published type stability lemma

Christensen--Sinclair--Smith--White, Perturbations of C-algebraic invariants*, GAFA 20 (2010), 368--397, Lemma 3.5 (author manuscript pp. 9--10), proves that two von Neumann algebras with the same centre and distance less than 1/10 have the same finite type I, type II₁ and infinite central parts. Here only diffuseness of the neighbour of a II₁ factor is retained. The centre and finiteness conclusions are already proved locally.

Primary author manuscript: https://eprints.gla.ac.uk/25426/1/25426.pdf

theorem OAI.KadisonKastler.concreteCenter_eq_of_scalar line 25

Source documentation

Two concrete scalar centres are literally the same algebra.

theorem concreteCenter_eq_of_scalar {M N : VonNeumannAlgebra H}
    (hM : ∀ c : Algebra M, (∀ a : Algebra M, a * c = c * a) →
      ∃ z : ℂ, c = z • (1 : Algebra M))
    (hN : ∀ c : Algebra N, (∀ a : Algebra N, a * c = c * a) →
      ∃ z : ℂ, c = z • (1 : Algebra N)) :
    concreteCenter M = concreteCenter N := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.concreteCenter

def OAI.KadisonKastler.PublishedFiniteType line 48
Source documentation
The application-specific part of CSSW (2010), Lemma 3.5. No spatial equivalence or perturbation estimate is included in this published input.
```
def PublishedFiniteType : Prop :=
…
```
theorem OAI.KadisonKastler.isII1Factor_of_near_of_published line 56
Source documentation
Combining the published type conclusion with the proved finite-neighbour and scalar-centre lemmas gives the II₁ predicate.
```
theorem isII1Factor_of_near_of_published
    (hpub : PublishedFiniteType (H := H)) {M N : VonNeumannAlgebra H}
…
```
Mentions: OAI.KadisonKastler.PublishedFiniteType