TracialCornerRepresentations.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual corner representations on the completed tracial Hilbert corners.

instance OAI.KadisonSimilarity.TracialCornerGeometry.cornerSubmodule_complete line 17
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerAction_mem line 21
Source documentation
Left multiplication by a corner element preserves both support equations.
```
theorem cornerAction_mem (a : CStarCorner e he) (x : H) (hx : x ∈ G.corner e r) :
    G.left (a : P) x ∈ G.corner e r := by
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner
def OAI.KadisonSimilarity.TracialCornerGeometry.cornerAction line 30
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerAction_coe line 33
def OAI.KadisonSimilarity.TracialCornerGeometry.cornerRepresentation line 37
Source documentation
The identity of ePe is e, acting as the identity on eL²(P)r.
```
def cornerRepresentation : CStarCorner e he →⋆ₐ[ℂ] (G.corner e r →L[ℂ] G.corner e r) where
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerRepresentation_coe line 76
theorem OAI.KadisonSimilarity.TracialCornerGeometry.corner_inclusion_intertwines line 79
theorem OAI.KadisonSimilarity.TracialCornerGeometry.corner_adjoint_intertwines line 83
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerRepresentation_cyclic line 96
Source documentation
The geometric cyclicity result now applies to the actual algebra ePe and its actual left representation, with no abstract-coordinate hypotheses.
```
theorem cornerRepresentation_cyclic (hr : IsStarProjection r) (v : P)
    (hv : star v * v = r) (hev : e * (v * star v) = v * star v) :
    CyclicStarRepresentation (G.cornerRepresentation e he r) :=
…
```
Mentions: OAI.KadisonSimilarity.CyclicStarRepresentation
def OAI.KadisonSimilarity.TracialCornerGeometry.faithfulRightAction line 105
Source documentation
Faithfulness of the dense tracial algebra vectors makes right multiplication faithful, as required by the full-column theorem.
```
def faithfulRightAction (hV : Function.Injective G.vector) :
    TracialRightAction (P := P) (H := H) where
…
```
Mentions: OAI.KadisonSimilarity.TracialRightAction