TracialSupportedColumns.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Support projections and represented right columns in a concrete tracial Hilbert space. These are the ambient spaces used by the full-column lemma.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.right_one line 19
theorem OAI.KadisonSimilarity.TracialCornerGeometry.right_zero line 26
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerProjection_adjoint line 33

theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerInto_eq_adjoint line 42

Source documentation

The support-equation projection is the actual orthogonal projection onto the completed two-sided Hilbert corner.

theorem cornerInto_eq_adjoint (e r : P) (he : IsStarProjection e) (hr : IsStarProjection r) :
    G.cornerInto e r he.isIdempotentElem hr.isIdempotentElem =
      (G.corner e r).toSubmodule.subtypeL.adjoint := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.corner_inclusion_adjoint line 58
theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightColumn_mem line 64
def OAI.KadisonSimilarity.TracialCornerGeometry.rightColumnAction line 72
theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightColumnAction_coe line 75
def OAI.KadisonSimilarity.TracialCornerGeometry.rightColumnRepresentation line 80
Source documentation
Left multiplication by the full algebra on a right-supported Hilbert column. No standard-form representation theorem is used here.
```
def rightColumnRepresentation (r : P) : P →⋆ₐ[ℂ] (G.corner 1 r →L[ℂ] G.corner 1 r) where
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightColumnRepresentation_coe line 100
theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightColumn_inclusion_intertwines line 103
theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightColumn_projection line 109
Source documentation
The adjoint of the inclusion is the right support projection and is a left-module map; this supplies the projection data of the full-column lemma.
```
theorem rightColumn_projection (r : P) (hr : IsStarProjection r) :
    (G.corner 1 r).toSubmodule.subtypeL.comp
      (G.corner 1 r).toSubmodule.subtypeL.adjoint = G.right r := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightColumn_adjoint_intertwines line 115