TracialUltrapowerGNS.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The GNS space of the tracial quotient embeds isometrically in the Hilbert ultrapower. This is the bounded-algebra-sequence subspace used in the finite-factor transfer.

def OAI.KadisonSimilarity.algebraSequenceVector line 21
Source documentation
A bounded algebra sequence, viewed as a bounded family of GNS vectors.
```
def algebraSequenceVector (x : ℕ →ᵇ A) :
    UltraPreHilbert (fun _ : ℕ => τ.GNS) ω :=
…
```
def OAI.KadisonSimilarity.algebraSequenceVectorLinear line 30
Source documentation
Algebra sequences act linearly on the bounded-vector subspace.
```
def algebraSequenceVectorLinear : (ℕ →ᵇ A) →ₗ[ℂ]
    HilbertUltraproduct (fun _ : ℕ => τ.GNS) ω where
…
```
theorem OAI.KadisonSimilarity.algebraSequenceVector_norm line 50
theorem OAI.KadisonSimilarity.algebraSequenceVector_null line 61
def OAI.KadisonSimilarity.quotientGNSVector line 69
Source documentation
The algebra-sequence map factors through the actual tracial quotient.
```
def quotientGNSVector : Ultrapower τ h1 ω htr →ₗ[ℂ]
    HilbertUltraproduct (fun _ : ℕ => τ.GNS) ω :=
…
```
theorem OAI.KadisonSimilarity.quotientGNSVector_mk line 75
def OAI.KadisonSimilarity.quotientPreGNSIsometry line 80
Source documentation
The tracial quotient's Hilbert norm is the ultralimit Hilbert norm.
```
def quotientPreGNSIsometry : (quotientTrace τ h1 ω htr).PreGNS →ₗᵢ[ℂ]
    HilbertUltraproduct (fun _ : ℕ => τ.GNS) ω where
…
```
def OAI.KadisonSimilarity.tracialUltrapowerGNSInclusion line 98
Source documentation
The closed GNS subspace of the Hilbert ultrapower, constructed by completion.
```
def tracialUltrapowerGNSInclusion : (quotientTrace τ h1 ω htr).GNS →ₗᵢ[ℂ]
    HilbertUltraproduct (fun _ : ℕ => τ.GNS) ω where
…
```
theorem OAI.KadisonSimilarity.tracialUltrapowerGNSInclusion_mk line 111