TypeIIIProjectionComparison.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Nonzero projections in separably acting type III factors

A nonfinite projection contains a proper isometry and hence countably many orthogonal copies of a nonzero defect. Factoriality supplies a countable source partition under this defect. It embeds the identity into the original projection; concrete Schroeder--Bernstein gives the required equivalence.

theorem OAI.KadisonKastler.projection_equivalent_one_of_not_finite_of_projection_countability line 28
Source documentation
A nonfinite projection in a separably acting factor is equivalent to its identity. The type III hypothesis is needed only to supply nonfiniteness.
```
theorem projection_equivalent_one_of_not_finite_of_projection_countability
    (hFamilies : HasCountableProjectionFamilies M) (hM : ScalarCenter M)
    (p : AlgebraProjection M) (hInfinite : ¬ FiniteProjectionIn M p.val) :
    p.Equivalent (⟨1, IsStarProjection.one _⟩ : AlgebraProjection M) := by
…
```
Mentions: OAI.KadisonKastler.HasCountableProjectionFamilies, OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.FiniteProjectionIn
theorem OAI.KadisonKastler.projection_equivalent_one_of_not_finite line 69
theorem OAI.KadisonKastler.TypeIIIFactor.exists_isometry_onto_projection_of_projection_countability line 78
Source documentation
Every nonzero projection in the concrete type III factor is the range of an isometry in the same algebra.
```
theorem TypeIIIFactor.exists_isometry_onto_projection_of_projection_countability
    (hM : TypeIIIFactor M) (hFamilies : HasCountableProjectionFamilies M)
    (p : Algebra M) (hp : IsStarProjection p) (hne : p ≠ 0) :
    ∃ v : Algebra M, star v * v = 1 ∧ v * star v = p := by
…
```
Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.HasCountableProjectionFamilies, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.TypeIIIFactor.exists_isometry_onto_projection line 90
theorem OAI.KadisonKastler.publishedTypeIIIProjectionComparison line 98
Source documentation
The type III projection-comparison input is a theorem of the existing concrete projection and partial-isometry development.
```
theorem publishedTypeIIIProjectionComparison : PublishedTypeIIIProjectionComparison.{u} := by
…
```