FullMatrixInjectivity.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The type I algebra generated by full countable matrix units

Taking the commutant of the diagonal corner operators realizes the scalar matrix factor directly. Its matrix coefficients are scalar, so it lies in any von Neumann algebra containing the original matrix units.

def OAI.KadisonKastler.FullMatrixCorner.scalarMatrixAlgebra line 27
Source documentation
The scalar matrix algebra, as the commutant of diagonal corner operators.
```
def scalarMatrixAlgebra : VonNeumannAlgebra H where
…
```
theorem OAI.KadisonKastler.FullMatrixCorner.mem_scalarMatrixAlgebra_iff line 34
theorem OAI.KadisonKastler.FullMatrixCorner.entry_mem_scalarMatrixAlgebra line 45

theorem OAI.KadisonKastler.FullMatrixCorner.scalarMatrixAlgebra_coefficient line 52

Source documentation

Each corner coefficient of a scalar matrix operator is scalar.

theorem scalarMatrixAlgebra_coefficient {T : H →L[ℂ] H}
    (hT : T ∈ F.scalarMatrixAlgebra) (i j : ℕ) :
    ∃ z : ℂ, F.matrixEntry T i j = z • (1 : E →L[ℂ] E) := by
…

theorem OAI.KadisonKastler.FullMatrixCorner.scalarMatrixAlgebra_le line 66
Source documentation
Every represented scalar matrix operator lies in any algebra containing the entries.
```
theorem scalarMatrixAlgebra_le (M : VonNeumannAlgebra H)
    (hF : ∀ i j, F.entry i j ∈ M) : F.scalarMatrixAlgebra ≤ M := by
…
```

theorem OAI.KadisonKastler.FullMatrixCorner.eq_inflate_of_commutes_entries line 76

Source documentation

A matrix-commuting operator is diagonal with one constant corner.

theorem eq_inflate_of_commutes_entries (T : H →L[ℂ] H)
    (hT : ∀ i j, T * F.entry i j = F.entry i j * T) :
    T = F.inflateHom (F.matrixEntry T 0 0) := by
…

theorem OAI.KadisonKastler.FullMatrixCorner.scalarMatrixAlgebra_center line 96
Source documentation
The scalar matrix algebra has scalar center in its original representation.
```
theorem scalarMatrixAlgebra_center : ScalarCenter F.scalarMatrixAlgebra := by
…
```
Mentions: OAI.KadisonKastler.ScalarCenter
def OAI.KadisonKastler.FullMatrixCorner.scalarMatrixInitialProjection line 105
Source documentation
The initial diagonal projection in the scalar matrix algebra.
```
def scalarMatrixInitialProjection : AlgebraProjection F.scalarMatrixAlgebra :=
…
```
theorem OAI.KadisonKastler.FullMatrixCorner.scalarMatrixInitialProjection_ne_zero line 110
theorem OAI.KadisonKastler.FullMatrixCorner.scalarMatrixInitialProjection_minimal line 120
Source documentation
The initial diagonal is minimal: every supported corner is scalar.
```
theorem scalarMatrixInitialProjection_minimal [Nontrivial E] :
    IsMinimalProjectionIn F.scalarMatrixAlgebra F.scalarMatrixInitialProjection := by
…
```
Mentions: OAI.KadisonKastler.IsMinimalProjectionIn
theorem OAI.KadisonKastler.FullMatrixCorner.scalarMatrixAlgebra_isInjective line 154
Source documentation
A full countable matrix system sits in a concrete injective type I algebra.
```
theorem scalarMatrixAlgebra_isInjective : IsInjective F.scalarMatrixAlgebra := by
…
```
Mentions: OAI.KadisonKastler.IsInjective
theorem OAI.KadisonKastler.FullMatrixCorner.exists_injective_algebra_containing_entries line 172
Source documentation
The matrix preparation can use this type I algebra without an AFD hypothesis.
```
theorem exists_injective_algebra_containing_entries (M : VonNeumannAlgebra H)
    (hF : ∀ i j, F.entry i j ∈ M) :
    ∃ S : VonNeumannAlgebra H, S ≤ M ∧ IsInjective S ∧ ∀ i j, F.entry i j ∈ S :=
…
```
Mentions: OAI.KadisonKastler.IsInjective