RegularCoreInjective.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

An injective algebra containing the countable matrix units

The factorial periodic stages are actual increasing full matrix algebras. Their generated von Neumann algebra contains every original matrix unit by strong approximation. Only the already stated published implication from increasing finite-dimensional approximation to injectivity is used.

def OAI.KadisonKastler.matrixUnitsInAlgebra line 24

Source documentation

Restriction of a concrete matrix-unit system to a von Neumann algebra that contains each of its entries.

def matrixUnitsInAlgebra {ι : Type*} [Fintype ι] [DecidableEq ι]
    (A : MatrixUnitSystem ι (H →L[ℂ] H)) (M : VonNeumannAlgebra H)
    (hA : ∀ i j, A.entry i j ∈ M) : MatrixUnitSystem ι (Algebra M) where
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.matrixUnitsInAlgebra_concreteHom line 42
theorem OAI.KadisonKastler.matrixUnitsInAlgebra_concreteAlgebra line 50
def OAI.KadisonKastler.FullMatrixCorner.periodicStage line 66
Source documentation
The full matrix stage of factorial size inside the containing algebra.
```
def periodicStage (M : VonNeumannAlgebra H) (hM : ∀ i j, F.entry i j ∈ M)
    (n : ℕ) : FiniteMatrixStage M where
…
```
theorem OAI.KadisonKastler.FullMatrixCorner.periodicStage_concreteAlgebra line 73
theorem OAI.KadisonKastler.FullMatrixCorner.periodicStage_monotone line 80

def OAI.KadisonKastler.FullMatrixCorner.periodicVonNeumann line 92

Source documentation

The actual von Neumann algebra generated by the increasing periodic matrix stages.

def periodicVonNeumann (M : VonNeumannAlgebra H) (hM : ∀ i j, F.entry i j ∈ M) :
    VonNeumannAlgebra H := FiniteMatrixStage.generatedVonNeumann (F.periodicStage M hM)

theorem OAI.KadisonKastler.FullMatrixCorner.periodicVonNeumann_le line 95
theorem OAI.KadisonKastler.FullMatrixCorner.periodicEntryApprox_mem_periodicVonNeumann line 99
theorem OAI.KadisonKastler.FullMatrixCorner.entry_mem_periodicVonNeumann line 109
theorem OAI.KadisonKastler.FullMatrixCorner.exists_injective_matrix_subalgebra line 121
Source documentation
The countable matrix units lie in an injective subalgebra of their original ambient algebra. Injectivity uses only the published AFD implication; the stage construction and inclusion are proved above.
```
theorem exists_injective_matrix_subalgebra [TopologicalSpace.SeparableSpace H]
    (hpub : PublishedIncreasingMatrixInjectivity (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedIncreasingMatrixInjectivity