TracialCornerCyclicity.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

Cyclicity of finite tracial corners from dense algebra vectors and partial-isometry transport. No corner cyclicity or density is assumed.

structure OAI.KadisonSimilarity.TracialCornerGeometry line 16

Source documentation

The concrete data of a tracial Hilbert representation.

structure TracialCornerGeometry (P H : Type*) [CStarAlgebra P]
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] where
…

def OAI.KadisonSimilarity.TracialCornerGeometry.conjugation line 30
theorem OAI.KadisonSimilarity.TracialCornerGeometry.conjugation_vector line 33
def OAI.KadisonSimilarity.TracialCornerGeometry.right line 37
Source documentation
Actual right multiplication, obtained from the tracial conjugation.
```
def right (b : P) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.right_vector line 41
theorem OAI.KadisonSimilarity.TracialCornerGeometry.right_mul line 46
theorem OAI.KadisonSimilarity.TracialCornerGeometry.right_mul_apply line 52
theorem OAI.KadisonSimilarity.TracialCornerGeometry.right_left line 56
theorem OAI.KadisonSimilarity.TracialCornerGeometry.right_adjoint line 62
def OAI.KadisonSimilarity.TracialCornerGeometry.corner line 75
Source documentation
The actual Hilbert corner, defined by its two support equations.
```
def corner (e r : P) : ClosedSubmodule ℂ H where
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.mem_corner line 81
def OAI.KadisonSimilarity.TracialCornerGeometry.cornerProjection line 86
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerProjection_vector line 88
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerProjection_mem line 93
def OAI.KadisonSimilarity.TracialCornerGeometry.cornerInto line 111
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerInto_coe line 116
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerInto_self line 119
theorem OAI.KadisonSimilarity.TracialCornerGeometry.corner_vectors_dense line 128
Source documentation
Corner density is derived from the dense algebra vectors by a surjective continuous projection.
```
theorem corner_vectors_dense (e r : P) (he : IsIdempotentElem e) (hr : IsIdempotentElem r) :
    DenseRange (fun a : P => G.cornerInto e r he hr (G.vector a)) := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.right_transfer_mem line 134
theorem OAI.KadisonSimilarity.TracialCornerGeometry.right_transfer_back_mem line 149
def OAI.KadisonSimilarity.TracialCornerGeometry.rightTransferMap line 163
def OAI.KadisonSimilarity.TracialCornerGeometry.rightTransferBack line 168
theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightTransferMap_coe line 173
theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightTransferBack_coe line 176
theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightTransfer_norm line 180
theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightTransfer_rightInverse line 191
def OAI.KadisonSimilarity.TracialCornerGeometry.rightTransfer line 201
Source documentation
Right multiplication by v* is the actual unitary from eL²r onto eL²(vv*); its inverse is right multiplication by v.
```
def rightTransfer (e r v : P) (hv : star v * v = r) :
    G.corner e r ≃ₗᵢ[ℂ] G.corner e (v * star v) :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightTransfer_coe line 207
theorem OAI.KadisonSimilarity.range_projection_of_initial_projection line 213
Source documentation
The range projection of an algebraic partial isometry is a projection.
```
theorem range_projection_of_initial_projection (r v : P) (hr : IsStarProjection r)
    (hv : star v * v = r) : IsStarProjection (v * star v) := by
…
```

theorem OAI.KadisonSimilarity.tracial_corner_cyclic_of_partial_isometry line 236

Source documentation

A partial isometry transports the corner to one where the range projection is a cyclic vector. The only corner-algebra data are its concrete left action and the fact that every compression eae is represented.

theorem tracial_corner_cyclic_of_partial_isometry
    (G : TracialCornerGeometry P H) (e r : P) (he : IsStarProjection e) (hr : IsStarProjection r)
    (σ : C →⋆ₐ[ℂ] (G.corner e r →L[ℂ] G.corner e r)) (ι : C → P)
    (hfull : ∀ a : P, ∃ c : C, ι c = e * a * e)
    (haction : ∀ (c : C) (x : G.corner e r), (σ c x : H) = G.left (ι c) x)
    (v : P) (hv : star v * v = r) (hev : e * (v * star v) = v * star v) :
    CyclicStarRepresentation σ := by
…

Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.CyclicStarRepresentation

theorem OAI.KadisonSimilarity.tracialCornerCyclicityInput_of_geometry line 280

Source documentation

The local cyclicity input in the full-column theorem is derived from the actual tracial geometry and corner-algebra coordinates.

theorem tracialCornerCyclicityInput_of_geometry
    (G : TracialCornerGeometry P H) (e r : P) (he : IsStarProjection e) (hr : IsStarProjection r)
    (σ : C →⋆ₐ[ℂ] (G.corner e r →L[ℂ] G.corner e r)) (ι : C → P)
    (hfull : ∀ a : P, ∃ c : C, ι c = e * a * e)
    (haction : ∀ (c : C) (x : G.corner e r), (σ c x : H) = G.left (ι c) x) :
    TracialCornerCyclicityInput e r σ :=
…

Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.TracialCornerCyclicityInput