GeneratedGNSModels.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The algebra generated inside a tracial ambient algebra has its own canonical GNS model. Ambient algebra-vector density gives native factor generation, and scalar freeness and faithful vectors restrict directly.

theorem OAI.KadisonSimilarity.restrictedGNS_factorsTraciallyGenerate line 22

Source documentation

Ordinary ambient L² generation becomes factor generation in the canonical GNS space of the generated algebra, without changing models.

theorem restrictedGNS_factorsTraciallyGenerate (hA : A ≤ L) (hD : D ≤ L)
    (hdense : ∀ a : L, gnsTracialVector τ (a : P) ∈
      closure (Set.range ((gnsTracialVector τ).comp
        (factorAlgebra A D).subtype.toLinearMap))) :
    (gnsTracialGeometry (restrictedPositiveTrace τ L)
      (restrictedPositiveTrace_tracial τ L htr)).FactorsTraciallyGenerate
        (A.comap L.subtype) (D.comap L.subtype) := by
…

Mentions: OAI.KadisonSimilarity.gnsTracialVector, OAI.KadisonSimilarity.gnsTracialGeometry, OAI.KadisonSimilarity.restrictedPositiveTrace, OAI.KadisonSimilarity.restrictedPositiveTrace_tracial

theorem OAI.KadisonSimilarity.restrictedGNS_scalarFree line 56
Source documentation
Freeness of the two ambient factors restricts to the canonical trace of the generated subalgebra.
```
theorem restrictedGNS_scalarFree (hfree : ScalarFree τ.toLinearMap A D) :
    ScalarFree
      (gnsTracialGeometry (restrictedPositiveTrace τ L)
        (restrictedPositiveTrace_tracial τ L htr)).trace
      (A.comap L.subtype) (D.comap L.subtype) := by
…
```
Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.gnsTracialGeometry, OAI.KadisonSimilarity.restrictedPositiveTrace, OAI.KadisonSimilarity.restrictedPositiveTrace_tracial
theorem OAI.KadisonSimilarity.restrictedGNS_vector_injective line 67
Source documentation
Faithfulness of the ambient trace makes the native generated-algebra GNS vectors injective.
```
theorem restrictedGNS_vector_injective
    (hf : ∀ a : P, τ (star a * a) = 0 → a = 0) :
    Function.Injective
      (gnsTracialGeometry (restrictedPositiveTrace τ L)
        (restrictedPositiveTrace_tracial τ L htr)).vector :=
…
```
Mentions: OAI.KadisonSimilarity.gnsTracialGeometry, OAI.KadisonSimilarity.restrictedPositiveTrace, OAI.KadisonSimilarity.restrictedPositiveTrace_tracial