MatrixFactor.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Factor and finite properties of the represented matrix algebra

theorem OAI.KadisonKastler.projection_map_equiv line 18
theorem OAI.KadisonKastler.equiv_smul_one line 23
theorem OAI.KadisonKastler.isometry_coisometry_of_faithfulTrace line 28

theorem OAI.KadisonKastler.proper_projection_pullback line 50

Source documentation

Pulling a proper split of the final projection back through its partial isometry gives a proper split of the original larger projection.

theorem proper_projection_pullback (p v f r : B) (hp : IsStarProjection p)
    (hr : IsStarProjection r) (hvp : v * p = v) (hv : v * star v = f)
    (hfr : f * r = r) (hrf : r * f = r) (hr0 : r ≠ 0) (hrf' : r ≠ f) :
    ∃ q : B, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q := by
…

theorem OAI.KadisonKastler.matrix_scalar_center line 83
theorem OAI.KadisonKastler.matrixVonNeumann_scalar_center line 104
theorem OAI.KadisonKastler.matrixVonNeumann_nonzero line 130
theorem OAI.KadisonKastler.matrixVonNeumann_weaklyClosed line 143
theorem OAI.KadisonKastler.matrixVonNeumann_finite line 147
theorem OAI.KadisonKastler.exists_matrix_corner_link line 156
Source documentation
A nonzero projection has a nonzero partial-isometry link to a coordinate corner.
```
theorem exists_matrix_corner_link (M : VonNeumannAlgebra H)
    (p : Algebra (matrixVonNeumann (ι := ι) M))
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.matrix_corner_split line 189
Source documentation
Splits in a diagonal matrix corner transport to the represented algebra.
```
theorem matrix_corner_split (M : VonNeumannAlgebra H)
    (hM : Generator.IsII1Factor M.toStarSubalgebra) (i : ι)
    (f : Algebra (matrixVonNeumann (ι := ι) M)) (hf : IsStarProjection f) (hf0 : f ≠ 0)
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.matrixVonNeumann_diffuse line 226
Source documentation
Finite matrices over a diffuse represented algebra have no minimal nonzero projections.
```
theorem matrixVonNeumann_diffuse (M : VonNeumannAlgebra H)
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (p : Algebra (matrixVonNeumann (ι := ι) M))
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.matrixVonNeumann_isII1Factor line 238
Source documentation
The represented finite matrix amplification is again a II₁ factor.
```
theorem matrixVonNeumann_isII1Factor (M : VonNeumannAlgebra H)
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (τ : FaithfulTracialState (Algebra M)) :
    Generator.IsII1Factor (matrixVonNeumann (ι := ι) M).toStarSubalgebra where
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann