MatrixCornerCommutant.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Explicit identification of a matrix diagonal corner with its commutant.

def OAI.BoundedHochschild.KadisonRingrose.matrixCornerCommutantEquiv line 19
Source documentation
The matrix coefficient map identifies a diagonal corner with the full matrix commutant. Its inverse is multiplication by that diagonal projection.
```
def matrixCornerCommutantEquiv :
    PopaCorner.algebra (E.diagonal_proj i) ≃⋆ₐ[ℂ] E.commutant where
…
```
Mentions: OAI.PopaCorner.algebra
def OAI.BoundedHochschild.KadisonRingrose.isometryCornerEquiv line 55
Source documentation
An isometry identifies the whole algebra with its range corner.
```
def isometryCornerEquiv (v : PartialIso M) (hi : v.initial = 1) :
    M ≃⋆ₐ[ℂ] PopaCorner.algebra v.final_proj := by
…
```
Mentions: OAI.PopaCorner.algebra