TracialMatrixColumns.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The matrix-unit column coordinates of a concrete tracial corner.

def OAI.KadisonSimilarity.TracialCornerGeometry.cornerToRightColumn line 19
Source documentation
Forget only the left support of a two-sided corner.
```
def cornerToRightColumn : G.corner e r →ₗᵢ[ℂ] G.corner 1 r where
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerToRightColumn_coe line 27
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerToRightColumn_adjoint line 30
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerToRightColumn_projection line 40

def OAI.KadisonSimilarity.TracialCornerGeometry.ambientCornerColumns line 52

Source documentation

The finite range decomposition in the ambient Hilbert space.

def ambientCornerColumns {n : ℕ} (v : Fin n → P)
    (hv : ∀ i j, star (v i) * v j = if i = j then e else 0)
    (hsum : ∑ i, v i * star (v i) = 1) :
    FiniteOrthogonalColumns (G.corner e 1) H n :=
…

Mentions: OAI.KadisonSimilarity.FiniteOrthogonalColumns

def OAI.KadisonSimilarity.TracialCornerGeometry.supportedCornerColumns line 63

Source documentation

The same finite range decomposition in the right-supported column.

def supportedCornerColumns (hr : IsStarProjection r) {n : ℕ} (v : Fin n → P)
    (hv : ∀ i j, star (v i) * v j = if i = j then e else 0)
    (hsum : ∑ i, v i * star (v i) = 1) :
    FiniteOrthogonalColumns (G.corner e r) (G.corner 1 r) n :=
…

Mentions: OAI.KadisonSimilarity.FiniteOrthogonalColumns

def OAI.KadisonSimilarity.TracialCornerGeometry.cornerMatrixEntry line 72
Source documentation
Matrix entries of an arbitrary algebra element, as actual elements of the unital corner algebra.
```
def cornerMatrixEntry {n : ℕ} (v : Fin n → P)
    (hv : ∀ i j, star (v i) * v j = if i = j then e else 0)
    (a : P) (i j : Fin n) : CStarCorner e he :=
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerRepresentation_compression line 84
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerRepresentation_supported_compression line 96

theorem OAI.KadisonSimilarity.TracialCornerGeometry.ambientCornerColumns_entry line 115

Source documentation

The ambient matrix coordinate entries are the actual elements vᵢ* a vⱼ of ePe.

theorem ambientCornerColumns_entry {n : ℕ} (v : Fin n → P)
    (hv : ∀ i j, star (v i) * v j = if i = j then e else 0)
    (hsum : ∑ i, v i * star (v i) = 1) (a : P) (i j : Fin n) :
    G.cornerRepresentation e he 1 (cornerMatrixEntry e he v hv a i j) =
      ((G.ambientCornerColumns e he v hv hsum).inclusion i).adjoint.comp
        ((G.left a).comp ((G.ambientCornerColumns e he v hv hsum).inclusion j)) := by
…

Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.cornerMatrixEntry

theorem OAI.KadisonSimilarity.TracialCornerGeometry.supportedCornerColumns_entry line 125

def OAI.KadisonSimilarity.TracialCornerGeometry.fullColumnCoordinates line 138

Source documentation

Both coordinate unitaries and every entry in the full-column theorem are now constructed from the same finite family in the tracial algebra.

def fullColumnCoordinates (hr : IsStarProjection r) {n : ℕ} (v : Fin n → P)
    (hv : ∀ i j, star (v i) * v j = if i = j then e else 0)
    (hsum : ∑ i, v i * star (v i) = 1) :
    FullColumnCoordinates G.left (G.rightColumnRepresentation r)
      (G.cornerRepresentation e he 1) (G.cornerRepresentation e he r) n :=
…

Mentions: OAI.KadisonSimilarity.FullColumnCoordinates