PublishedProperInfiniteProjection.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Countable copies of a full projection

Blackadar, Operator Algebras, III.1.3.6 (author PDF, printed p.243), asserts that a full projection in a properly infinite, locally countably decomposable von Neumann algebra admits a countable orthogonal family of equivalent projections with strong sum one. Separably acting algebras are countably decomposable. The input below is only this projection assertion.

The projection's central support is the already constructed orbit-closure projection. Proper infiniteness is expressed by two isometries with orthogonal ranges. No trace, corner type, or perturbation conclusion is part of this published input.

Primary source: https://bruceblackadar.com/Mathematics/Cycr.pdf

structure OAI.KadisonKastler.ProperlyInfiniteIdentity line 36
Source documentation
The ordinary two-isometry description of a nonzero properly infinite identity. The cross product states that the two range projections are orthogonal.
```
structure ProperlyInfiniteIdentity (M : VonNeumannAlgebra H) : Prop where
…
```
structure OAI.KadisonKastler.CountableProjectionCopies line 42
Source documentation
Actual equivalent projection copies and their strong sum.
```
structure CountableProjectionCopies (M : VonNeumannAlgebra H) (p : AlgebraProjection M) where
…
```
def OAI.KadisonKastler.PublishedProperInfiniteProjectionCopies line 51
Source documentation
Blackadar III.1.3.6 restricted to separably acting algebras.
```
def PublishedProperInfiniteProjectionCopies : Prop :=
…
```

theorem OAI.KadisonKastler.finiteProjectionIn_of_equivalent line 58

Source documentation

Finiteness is preserved by Murray--von Neumann equivalence.

theorem finiteProjectionIn_of_equivalent (p q : AlgebraProjection M)
    (hfinite : FiniteProjectionIn M p.val) (v : Algebra M)
    (hvi : star v * v = p.val) (hvf : v * star v = q.val) :
    FiniteProjectionIn M q.val := by
…

Mentions: OAI.KadisonKastler.FiniteProjectionIn, OAI.KadisonKastler.Algebra

def OAI.KadisonKastler.CountableProjectionCopies.rebasedPartial line 108
theorem OAI.KadisonKastler.CountableProjectionCopies.rebased_initial line 110
theorem OAI.KadisonKastler.CountableProjectionCopies.rebased_final line 121
def OAI.KadisonKastler.CountableProjectionCopies.fullMatrixCorner line 133
Source documentation
The actual countable matrix units after rebasing to the first final projection.
```
def fullMatrixCorner : FullMatrixCorner (typeIIIInitialSpace (D.projection 0)) :=
…
```
Mentions: OAI.KadisonKastler.FullMatrixCorner, OAI.KadisonKastler.typeIIIInitialSpace
theorem OAI.KadisonKastler.CountableProjectionCopies.fullMatrixCorner_mem line 138
theorem OAI.KadisonKastler.CountableProjectionCopies.first_nonzero line 143
theorem OAI.KadisonKastler.CountableProjectionCopies.first_finite line 151

theorem OAI.KadisonKastler.exists_finite_fullMatrixCorner_of_full_projection line 159

Source documentation

A chosen finite nonzero full projection produces a finite full matrix corner.

theorem exists_finite_fullMatrixCorner_of_full_projection
    [TopologicalSpace.SeparableSpace H]
    (hPublished : PublishedProperInfiniteProjectionCopies.{u})
    (hInfinite : ProperlyInfiniteIdentity M) (p : AlgebraProjection M)
    (hfull : (centralSupport p).val = 1) (hp : p.val ≠ 0)
    (hfinite : FiniteProjectionIn M p.val) :
    ∃ q : AlgebraProjection M, q.val ≠ 0 ∧ FiniteProjectionIn M q.val ∧
      ∃ F : FullMatrixCorner (typeIIIInitialSpace q), ∀ i j, F.entry i j ∈ M := by
…

Mentions: OAI.KadisonKastler.ProperlyInfiniteIdentity, OAI.KadisonKastler.FiniteProjectionIn, OAI.KadisonKastler.FullMatrixCorner, OAI.KadisonKastler.typeIIIInitialSpace

theorem OAI.KadisonKastler.exists_finite_fullMatrixCorner_of_factor line 172

Source documentation

In a factor, nonzeroness supplies the full-central-support hypothesis.

theorem exists_finite_fullMatrixCorner_of_factor
    [TopologicalSpace.SeparableSpace H]
    (hPublished : PublishedProperInfiniteProjectionCopies.{u})
    (hInfinite : ProperlyInfiniteIdentity M) (hfactor : ScalarCenter M)
    (p : AlgebraProjection M) (hp : p.val ≠ 0) (hfinite : FiniteProjectionIn M p.val) :
    ∃ q : AlgebraProjection M, q.val ≠ 0 ∧ FiniteProjectionIn M q.val ∧
      ∃ F : FullMatrixCorner (typeIIIInitialSpace q), ∀ i j, F.entry i j ∈ M := by
…

Mentions: OAI.KadisonKastler.ProperlyInfiniteIdentity, OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.FiniteProjectionIn, OAI.KadisonKastler.FullMatrixCorner, OAI.KadisonKastler.typeIIIInitialSpace