MatrixUnitCoordinates.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Hilbert coordinates from a finite orthogonal family of corner inclusions

The two matrix-unit equations construct the coordinate unitaries used in the full-column theorem. The action of an arbitrary operator is then its actual matrix of corner compressions.

structure OAI.KadisonSimilarity.FiniteOrthogonalColumns line 25

Source documentation

The elementary operator equations supplied by a complete finite system of matrix-unit columns.

structure FiniteOrthogonalColumns (F H : Type*)
    [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (n : ℕ) where
…

theorem OAI.KadisonSimilarity.FiniteOrthogonalColumns.adjoint_inclusion_apply line 37
theorem OAI.KadisonSimilarity.FiniteOrthogonalColumns.adjoint_assembly_comp_assembly line 45
Source documentation
Orthogonality makes assembly an isometry.
```
theorem adjoint_assembly_comp_assembly :
    (sumColumns U.inclusion).adjoint.comp (sumColumns U.inclusion) =
      ContinuousLinearMap.id ℂ (HilbertCopies F n) := by
…
```
Mentions: OAI.KadisonSimilarity.sumColumns, OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.FiniteOrthogonalColumns.assembly_comp_adjoint_assembly line 58
Source documentation
Completeness of the family makes assembly onto the full Hilbert space.
```
theorem assembly_comp_adjoint_assembly :
    (sumColumns U.inclusion).comp (sumColumns U.inclusion).adjoint =
      ContinuousLinearMap.id ℂ H := by
…
```
Mentions: OAI.KadisonSimilarity.sumColumns
def OAI.KadisonSimilarity.FiniteOrthogonalColumns.unitary line 67
Source documentation
The coordinate unitary is constructed from the finite matrix-unit columns.
```
def unitary : HilbertCopies F n ≃ₗᵢ[ℂ] H :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.FiniteOrthogonalColumns.unitary_apply line 75
theorem OAI.KadisonSimilarity.FiniteOrthogonalColumns.unitary_symm_apply line 78
theorem OAI.KadisonSimilarity.FiniteOrthogonalColumns.unitary_single line 81
theorem OAI.KadisonSimilarity.FiniteOrthogonalColumns.coordinates_operator line 88
Source documentation
Arbitrary operators act in the constructed coordinates by their corner compression matrix.
```
theorem coordinates_operator (T : H →L[ℂ] H) (x : H) :
    U.unitary.symm (T x) =
      matrixOperator (fun i j => (U.inclusion i).adjoint.comp (T.comp (U.inclusion j)))
        (U.unitary.symm x) := by
…
```
Mentions: OAI.KadisonSimilarity.matrixOperator
theorem OAI.KadisonSimilarity.FiniteOrthogonalColumns.unitary_matrixUnit line 99
Source documentation
A coordinate matrix unit is the actual matrix unit formed from the two corner inclusions.
```
theorem unitary_matrixUnit (i j : Fin n) (x : H) :
    U.unitary (copyMatrixUnit i j (U.unitary.symm x)) =
      U.inclusion i ((U.inclusion j).adjoint x) := by
…
```
Mentions: OAI.KadisonSimilarity.copyMatrixUnit

def OAI.KadisonSimilarity.fullColumnCoordinatesOfColumns line 116

Source documentation

Realize the full-column coordinates from the actual corner inclusion operators and their common matrix of algebra entries.

def fullColumnCoordinatesOfColumns
    (L : P →⋆ₐ[ℂ] (H →L[ℂ] H)) (Lr : P →⋆ₐ[ℂ] (D →L[ℂ] D))
    (ρ : C →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K))
    {n : ℕ} (U : FiniteOrthogonalColumns F H n) (V : FiniteOrthogonalColumns K D n)
    (entry : P → Matrix (Fin n) (Fin n) C)
    (hU : ∀ a i j, ρ (entry a i j) =
      (U.inclusion i).adjoint.comp ((L a).comp (U.inclusion j)))
    (hV : ∀ a i j, σ (entry a i j) =
      (V.inclusion i).adjoint.comp ((Lr a).comp (V.inclusion j))) :
    FullColumnCoordinates L Lr ρ σ n where
…

Mentions: OAI.KadisonSimilarity.FiniteOrthogonalColumns, OAI.KadisonSimilarity.FullColumnCoordinates

theorem OAI.KadisonSimilarity.fullColumnCoordinatesOfColumns_corner line 138

Source documentation

The corner used by the full-column theorem is the concrete rectangular compression of the given operator.

theorem fullColumnCoordinatesOfColumns_corner
    (L : P →⋆ₐ[ℂ] (H →L[ℂ] H)) (Lr : P →⋆ₐ[ℂ] (D →L[ℂ] D))
    (ρ : C →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K))
    {n : ℕ} (U : FiniteOrthogonalColumns F H n) (V : FiniteOrthogonalColumns K D n)
    (entry : P → Matrix (Fin n) (Fin n) C)
    (hU : ∀ a i j, ρ (entry a i j) =
      (U.inclusion i).adjoint.comp ((L a).comp (U.inclusion j)))
    (hV : ∀ a i j, σ (entry a i j) =
      (V.inclusion i).adjoint.comp ((Lr a).comp (V.inclusion j)))
    (G : D →L[ℂ] H) (i : Fin n) :
    (fullColumnCoordinatesOfColumns L Lr ρ σ U V entry hU hV).corner i G =
      (U.inclusion i).adjoint.comp (G.comp (V.inclusion i)) := by
…

Mentions: OAI.KadisonSimilarity.FiniteOrthogonalColumns, OAI.KadisonSimilarity.fullColumnCoordinatesOfColumns

theorem OAI.KadisonSimilarity.matrixUnit_intertwining_in_coordinates line 157

Source documentation

Intertwining the actual matrix units becomes the scalar matrix-unit commutation required by the full-column theorem.

theorem matrixUnit_intertwining_in_coordinates
    {n : ℕ} (U : FiniteOrthogonalColumns F H n) (V : FiniteOrthogonalColumns K D n)
    (G : D →L[ℂ] H) (i : Fin n)
    (hG : ∀ j : Fin n,
      G.comp ((V.inclusion i).comp (V.inclusion j).adjoint) =
        ((U.inclusion i).comp (U.inclusion j).adjoint).comp G) :
    ∀ j : Fin n,
      (U.unitary.symm.toContinuousLinearEquiv.toContinuousLinearMap.comp
        (G.comp V.unitary.toContinuousLinearEquiv.toContinuousLinearMap)).comp
          (copyMatrixUnit i j) =
      (copyMatrixUnit i j).comp
        (U.unitary.symm.toContinuousLinearEquiv.toContinuousLinearMap.comp
…

Mentions: OAI.KadisonSimilarity.FiniteOrthogonalColumns, OAI.KadisonSimilarity.copyMatrixUnit