TracialHomCompression.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact recovery of a commutator through trace-preserving embeddings. This is the final direction of the ultrapower transfer: a bound on the constant subalgebra's compressed commutator bounds the original operator.

theorem OAI.KadisonSimilarity.gnsGeometry_preserves_trace line 26
theorem OAI.KadisonSimilarity.tracialRangeIsometry_inclusion line 34
Source documentation
Factoring the GNS embedding through the completed range is exact.
```
theorem tracialRangeIsometry_inclusion :
    (V).toContinuousLinearMap.comp (U).toContinuousLinearMap = (J).toContinuousLinearMap := by
…
```

theorem OAI.KadisonSimilarity.tracialRangeIsometry_left line 46

Source documentation

The range-space isometry intertwines the actual left representations.

theorem tracialRangeIsometry_left (a : A) :
    ((G).baseRepresentation φ.range (φ.rangeRestrict a)).comp (U).toContinuousLinearMap =
      (U).toContinuousLinearMap.comp (τA.gnsStarAlgHom a) := by
…

theorem OAI.KadisonSimilarity.norm_commutator_le_tracial_range_compression line 63

Source documentation

No norm is lost when using a bound on the compressed constant algebra to recover the original commutator. Only compression equality is needed.

theorem norm_commutator_le_tracial_range_compression
    (T : τA.GNS →L[ℂ] τA.GNS) (S : τB.GNS →L[ℂ] τB.GNS)
    (hT : (J).toContinuousLinearMap.adjoint.comp (S.comp (J).toContinuousLinearMap) = T)
    (a : A) :
    ‖commutator T (τA.gnsStarAlgHom a)‖ ≤
      ‖(G).baseOperator φ.range (commutator S (τB.gnsStarAlgHom (φ a)))‖ := by
…

Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.gnsTracialHomIsometry_comp line 90

Source documentation

GNS embeddings compose on the completed Hilbert spaces.

theorem gnsTracialHomIsometry_comp :
    (gnsTracialHomIsometry τB τC ψ hψ).toContinuousLinearMap.comp
      (gnsTracialHomIsometry τA τB φ hφ).toContinuousLinearMap =
    (gnsTracialHomIsometry τA τC (ψ.comp φ)
      (fun a => (hψ (φ a)).trans (hφ a))).toContinuousLinearMap := by
…

Mentions: OAI.KadisonSimilarity.gnsTracialHomIsometry