CanonicalAmplificationCorner.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The initial corner of the actual amplification

Compression to the initial matrix coordinate recovers precisely the original algebra. In the canonical Hilbert sum this is the transported original representation, so a finite diffuse factor gives an actual finite diffuse initial corner.

theorem OAI.KadisonKastler.FullMatrixCorner.blockElement_zero_zero line 25
theorem OAI.KadisonKastler.FullMatrixCorner.matrixEntry_cornerExtension line 30
theorem OAI.KadisonKastler.FullMatrixCorner.cornerExtension_mem_amplifiedAlgebra_iff line 36
Source documentation
Extension by zero belongs to the amplification exactly when the corner operator belongs to its original algebra.
```
theorem cornerExtension_mem_amplifiedAlgebra_iff
    (M : VonNeumannAlgebra E) (T : E →L[ℂ] E) :
    cornerExtension E T ∈ F.amplifiedAlgebra M ↔ T ∈ M := by
…
```
Mentions: OAI.KadisonKastler.cornerExtension
theorem OAI.KadisonKastler.FullMatrixCorner.representedCorner_amplifiedAlgebra line 53
Source documentation
The represented first corner of the amplification is the input algebra itself.
```
theorem representedCorner_amplifiedAlgebra (M : VonNeumannAlgebra E) :
    representedCorner E (F.amplifiedAlgebra M)
      (F.zero_zero ▸ F.entry_mem_amplifiedAlgebra M 0 0) = M := by
…
```
Mentions: OAI.KadisonKastler.representedCorner
theorem OAI.KadisonKastler.canonicalInitialProjection_mem line 64
theorem OAI.KadisonKastler.representedCorner_canonicalAmplifiedAlgebra line 71
Source documentation
In canonical coordinates the first corner is exactly the spatially transported original algebra.
```
theorem representedCorner_canonicalAmplifiedAlgebra (M : VonNeumannAlgebra H) :
    representedCorner (canonicalInitialSpace H) (canonicalAmplifiedAlgebra H M)
      (canonicalInitialProjection_mem H M) = canonicalCornerAlgebra H M :=
…
```
Mentions: OAI.KadisonKastler.representedCorner, OAI.KadisonKastler.canonicalInitialSpace, OAI.KadisonKastler.canonicalAmplifiedAlgebra, OAI.KadisonKastler.canonicalInitialProjection_mem, OAI.KadisonKastler.canonicalCornerAlgebra
theorem OAI.KadisonKastler.representedCorner_canonicalAmplifiedAlgebra_isII1 line 76