FiniteMatrixInjectivity.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Injectivity of a concrete full matrix algebra

The diagonal matrix units are minimal projections. Thus the concrete type-I injectivity theorem applies to each finite matrix stage.

theorem OAI.KadisonKastler.scalarCenter_of_matrixUnits_surjective line 24
Source documentation
Full matrix units give precisely the scalar center.
```
theorem scalarCenter_of_matrixUnits_surjective
    (E : MatrixUnitSystem ι (Algebra M)) (hE : Function.Surjective E.hom) :
    ScalarCenter M := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ScalarCenter
def OAI.KadisonKastler.matrixUnitDiagonalProjection line 47
Source documentation
A specified diagonal matrix unit, as an algebra projection.
```
def matrixUnitDiagonalProjection (E : MatrixUnitSystem ι (Algebra M)) (o : ι) :
    AlgebraProjection M :=
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.matrixUnitDiagonalProjection_minimal line 53
Source documentation
Each specified diagonal unit is minimal in the full matrix image.
```
theorem matrixUnitDiagonalProjection_minimal
    (E : MatrixUnitSystem ι (Algebra M)) (hE : Function.Surjective E.hom) (o : ι) :
    IsMinimalProjectionIn M (matrixUnitDiagonalProjection E o) := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.IsMinimalProjectionIn, OAI.KadisonKastler.matrixUnitDiagonalProjection
theorem OAI.KadisonKastler.minimalProjection_of_matrixUnits_surjective line 86
Source documentation
Every full matrix algebra contains a minimal projection.
```
theorem minimalProjection_of_matrixUnits_surjective
    (E : MatrixUnitSystem ι (Algebra M)) (hE : Function.Surjective E.hom) (o : ι) :
    ∃ p : AlgebraProjection M, IsMinimalProjectionIn M p :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.IsMinimalProjectionIn
theorem OAI.KadisonKastler.isInjective_of_matrixUnits_surjective line 92
Source documentation
A full matrix algebra is injective in its given Hilbert representation.
```
theorem isInjective_of_matrixUnits_surjective
    (E : MatrixUnitSystem ι (Algebra M)) (hE : Function.Surjective E.hom) :
    IsInjective M := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.IsInjective
def OAI.KadisonKastler.matrixUnitConcreteAlgebra line 100
Source documentation
The concrete finite matrix image, with its proved weak closedness.
```
def matrixUnitConcreteAlgebra (E : MatrixUnitSystem ι (Algebra M)) :
    VonNeumannAlgebra H :=
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.matrixUnitConcreteAlgebra_le line 106
Source documentation
The represented matrix image stays in its original algebra.
```
theorem matrixUnitConcreteAlgebra_le (E : MatrixUnitSystem ι (Algebra M)) :
    matrixUnitConcreteAlgebra E ≤ M := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixUnitConcreteAlgebra
def OAI.KadisonKastler.concreteMatrixUnits line 112
Source documentation
The same matrix units regarded inside their concrete image.
```
def concreteMatrixUnits (E : MatrixUnitSystem ι (Algebra M)) :
    MatrixUnitSystem ι (Algebra (matrixUnitConcreteAlgebra E)) where
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixUnitConcreteAlgebra
theorem OAI.KadisonKastler.concreteMatrixUnits_hom line 131
theorem OAI.KadisonKastler.concreteMatrixUnits_surjective line 140
theorem OAI.KadisonKastler.isInjective_matrixUnitConcreteAlgebra line 148
Source documentation
No injectivity assumption is needed for any finite matrix stage.
```
theorem isInjective_matrixUnitConcreteAlgebra (E : MatrixUnitSystem ι (Algebra M)) :
    IsInjective (matrixUnitConcreteAlgebra E) :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.IsInjective, OAI.KadisonKastler.matrixUnitConcreteAlgebra
theorem OAI.KadisonKastler.isInjective_matrixUnitConcreteAlgebra_all line 155
Source documentation
The zero Hilbert space causes no exception to stage injectivity.
```
theorem isInjective_matrixUnitConcreteAlgebra_all
    (E : MatrixUnitSystem ι (Algebra M)) : IsInjective (matrixUnitConcreteAlgebra E) := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.IsInjective, OAI.KadisonKastler.matrixUnitConcreteAlgebra