TracialBaseSpace.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

The completed base Hilbert space of a represented tracial star algebra, its actual inclusion, and compression of the ambient left action.

def OAI.KadisonSimilarity.TracialCornerGeometry.baseAlgebraVectors line 20
Source documentation
The algebraic vectors coming from the specified star subalgebra.
```
def baseAlgebraVectors : A →ₗ[ℂ] H := G.vector.comp A.subtype.toLinearMap
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseAlgebraVectors_apply line 22
def OAI.KadisonSimilarity.TracialCornerGeometry.baseSpace line 26
Source documentation
The actual closed base subspace, with no independent density input.
```
def baseSpace : ClosedSubmodule ℂ H := (G.baseAlgebraVectors A).range.closure
```
instance OAI.KadisonSimilarity.TracialCornerGeometry.baseSpace_complete line 28
def OAI.KadisonSimilarity.TracialCornerGeometry.baseVector line 32
Source documentation
The dense algebra-vector map into its Hilbert completion.
```
def baseVector : A →ₗ[ℂ] G.baseSpace A :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseVector_coe line 36
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseVector_dense line 39
def OAI.KadisonSimilarity.TracialCornerGeometry.baseInclusion line 47
Source documentation
The canonical isometry from the completed base into the ambient space.
```
def baseInclusion : G.baseSpace A →ₗᵢ[ℂ] H := (G.baseSpace A).toSubmodule.subtypeₗᵢ
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseInclusion_apply line 49
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseInclusion_vector line 51
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseInclusion_adjoint line 54
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseInclusion_adjoint_self line 59
def OAI.KadisonSimilarity.TracialCornerGeometry.baseOperator line 66
Source documentation
Compression of an ambient bounded operator to the completed base.
```
def baseOperator (Y : H →L[ℂ] H) : G.baseSpace A →L[ℂ] G.baseSpace A :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseOperator_adjoint line 70
def OAI.KadisonSimilarity.TracialCornerGeometry.baseCompression line 76
Source documentation
The actual compressed left action on arbitrary ambient algebra elements.
```
def baseCompression : P →ₗ[ℂ] (G.baseSpace A →L[ℂ] G.baseSpace A) where
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseCompression_apply line 85
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseCompression_one line 88

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseCompression_inner line 95

Source documentation

The coefficient formula required by the tracial Fourier compression.

theorem baseCompression_inner (a b : A) (x : P) :
    inner ℂ (G.baseVector A a) (G.baseCompression A x (G.baseVector A b)) =
      G.trace (star (a : P) * x * (b : P)) := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseVector_inner line 106
Source documentation
The base Hilbert inner product is the original tracial one.
```
theorem baseVector_inner (a b : A) :
    inner ℂ (G.baseVector A a) (G.baseVector A b) =
      G.trace (star (a : P) * (b : P)) := G.inner_vector _ _
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseSpace_invariant line 111
Source documentation
Left multiplication by the subalgebra preserves the completed base.
```
theorem baseSpace_invariant (a : A) (x : H) (hx : x ∈ G.baseSpace A) :
    G.left (a : P) x ∈ G.baseSpace A := by
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.baseAction line 121
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseAction_coe line 124
def OAI.KadisonSimilarity.TracialCornerGeometry.baseRepresentation line 129
Source documentation
The restriction to the star subalgebra is a genuine unital star representation on the completed base space.
```
def baseRepresentation : A →⋆ₐ[ℂ] (G.baseSpace A →L[ℂ] G.baseSpace A) where
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseRepresentation_coe line 149
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseInclusion_intertwines line 152
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseCompression_subalgebra line 156

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseOperator_intertwines line 165

Source documentation

Preservation of the base subspace gives the actual compressed intertwining identity.

theorem baseOperator_intertwines (Y : H →L[ℂ] H)
    (hY : ∀ x ∈ G.baseSpace A, Y x ∈ G.baseSpace A) :
    Y.comp (G.baseInclusion A).toContinuousLinearMap =
      (G.baseInclusion A).toContinuousLinearMap.comp (G.baseOperator A Y) := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseCompression_commutator line 178

Source documentation

A reducing base subspace makes the compressed commutator exactly the compression of the ambient commutator.

theorem baseCompression_commutator (Y : H →L[ℂ] H)
    (hY : ∀ x ∈ G.baseSpace A, Y x ∈ G.baseSpace A)
    (hYstar : ∀ x ∈ G.baseSpace A, Y.adjoint x ∈ G.baseSpace A) (x : P) :
    commutator (G.baseOperator A Y) (G.baseCompression A x) =
      G.baseOperator A (commutator Y (G.left x)) := by
…

Mentions: OAI.KadisonSimilarity.commutator