TracialSubalgebraModels.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The normal algebra generated inside the ultrapower is represented on its own tracial GNS space. Restriction of the positive trace and its exact Hilbert-space identification require no further analytic input.

def OAI.KadisonSimilarity.restrictedPositiveTrace line 18
Source documentation
Restrict the actual positive functional to a closed star subalgebra.
```
def restrictedPositiveTrace : L →ₚ[ℂ] ℂ :=
…
```
theorem OAI.KadisonSimilarity.restrictedPositiveTrace_apply line 22
theorem OAI.KadisonSimilarity.restrictedPositiveTrace_one line 25
theorem OAI.KadisonSimilarity.restrictedPositiveTrace_tracial line 28
theorem OAI.KadisonSimilarity.restrictedPositiveTrace_faithful line 33
def OAI.KadisonSimilarity.restrictedTracialGNSInclusion line 40
Source documentation
The inclusion of the generated algebra induces its concrete GNS inclusion.
```
def restrictedTracialGNSInclusion :
    (restrictedPositiveTrace τ L).GNS →ₗᵢ[ℂ] τ.GNS :=
…
```
Mentions: OAI.KadisonSimilarity.restrictedPositiveTrace
theorem OAI.KadisonSimilarity.restrictedTracialGNSInclusion_vector line 44
theorem OAI.KadisonSimilarity.restrictedTracialGNSInclusion_range line 50
Source documentation
Its range is exactly the completed algebra-vector subspace.
```
theorem restrictedTracialGNSInclusion_range
    (htr : ∀ a b : P, τ (a * b) = τ (b * a)) :
    Set.range (restrictedTracialGNSInclusion τ L) =
      ((gnsTracialGeometry τ htr).baseSpace L : Set τ.GNS) := by
…
```
Mentions: OAI.KadisonSimilarity.restrictedTracialGNSInclusion, OAI.KadisonSimilarity.gnsTracialGeometry