GNSTracialGeometry.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The actual tracial GNS representation supplies the Hilbert geometry used in the free-corner argument. Trace-preserving homomorphisms induce isometric embeddings which intertwine the concrete left actions.

def OAI.KadisonSimilarity.gnsTracialVector line 18
Source documentation
The canonical algebra vector in the completed GNS space.
```
def gnsTracialVector (τ : A →ₚ[ℂ] ℂ) : A →ₗ[ℂ] τ.GNS :=
…
```
theorem OAI.KadisonSimilarity.gnsTracialVector_apply line 21
theorem OAI.KadisonSimilarity.gnsTracialVector_inner line 24
theorem OAI.KadisonSimilarity.gnsTracialVector_dense line 29
theorem OAI.KadisonSimilarity.gnsTracialVector_left line 33
def OAI.KadisonSimilarity.gnsTracialGeometry line 42
Source documentation
The concrete tracial geometry is obtained directly from the GNS construction, rather than assumed as separate representation data.
```
def gnsTracialGeometry (τ : A →ₚ[ℂ] ℂ)
    (htr : ∀ a b : A, τ (a * b) = τ (b * a)) : TracialCornerGeometry A τ.GNS where
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry
theorem OAI.KadisonSimilarity.gnsTracialGeometry_trace line 52
theorem OAI.KadisonSimilarity.gnsTracialGeometry_vector line 56
theorem OAI.KadisonSimilarity.gnsTracialGeometry_left line 60
theorem OAI.KadisonSimilarity.gnsTracialGeometry_trace_one line 64
theorem OAI.KadisonSimilarity.gnsTracialVector_injective line 68
theorem OAI.KadisonSimilarity.gnsTracialHom_norm line 83
def OAI.KadisonSimilarity.gnsTracialHomIsometry line 90
Source documentation
The GNS isometry induced by a trace-preserving star homomorphism.
```
def gnsTracialHomIsometry : τA.GNS →ₗᵢ[ℂ] τB.GNS :=
…
```
theorem OAI.KadisonSimilarity.gnsTracialHomIsometry_vector line 94

theorem OAI.KadisonSimilarity.gnsTracialHomIsometry_left line 101

Source documentation

Intertwining holds on every completed GNS vector.

theorem gnsTracialHomIsometry_left (a : A) (ξ : τA.GNS) :
    gnsTracialHomIsometry τA τB φ hφ (τA.gnsStarAlgHom a ξ) =
      τB.gnsStarAlgHom (φ a) (gnsTracialHomIsometry τA τB φ hφ ξ) := by
…

Mentions: OAI.KadisonSimilarity.gnsTracialHomIsometry

theorem OAI.KadisonSimilarity.gnsTracialHomIsometry_intertwines line 109