SemifiniteFactor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix corners in semifinite diffuse factors

The type-II-infinity predicate uses scalar center, two orthogonal isometries, projection semifiniteness, and diffuseness. Choosing one finite nonzero projection and applying the countable-copy theorem constructs the matrix corner and its II₁ factor structure. There is no trace or stability conclusion in the type predicate. Projection semifiniteness is exactly the criterion in Blackadar III.1.4.2; III.1.4.6 identifies the properly infinite continuous semifinite part as type II∞.

structure OAI.KadisonKastler.TypeIIInfinityFactor line 28
Source documentation
The projection-theoretic description of a type II∞ factor.
```
structure TypeIIInfinityFactor (M : VonNeumannAlgebra H) : Prop where
…
```
theorem OAI.KadisonKastler.TypeIIInfinityFactor.exists_nonzero_finite_projection line 37
Source documentation
One finite nonzero projection is selected from projection semifiniteness.
```
theorem TypeIIInfinityFactor.exists_nonzero_finite_projection (hM : TypeIIInfinityFactor M) :
    ∃ p : AlgebraProjection M, p.val ≠ 0 ∧ FiniteProjectionIn M p.val := by
…
```
Mentions: OAI.KadisonKastler.TypeIIInfinityFactor, OAI.KadisonKastler.FiniteProjectionIn
structure OAI.KadisonKastler.FiniteFullMatrixCornerData line 48
Source documentation
The geometric corner data, including the proved II₁ structure of the initial represented corner.
```
structure FiniteFullMatrixCornerData (M : VonNeumannAlgebra H) where
…
```
theorem OAI.KadisonKastler.TypeIIInfinityFactor.nonempty_finiteMatrixCornerData line 60
Source documentation
A type II∞ factor has the concrete finite full matrix-corner data needed for semifinite perturbation.
```
theorem TypeIIInfinityFactor.nonempty_finiteMatrixCornerData
    [TopologicalSpace.SeparableSpace H] (hM : TypeIIInfinityFactor M)
    (hCopies : PublishedProperInfiniteProjectionCopies.{u}) :
    Nonempty (FiniteFullMatrixCornerData M) := by
…
```
Mentions: OAI.KadisonKastler.TypeIIInfinityFactor, OAI.KadisonKastler.FiniteFullMatrixCornerData