UltrapowerFreePositionTransfer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Commutation and small-corner estimates pass to the concrete free copy inside the prescribed subfactor ultrapower. Recovery of the original commutator uses the exact constant GNS embedding.

theorem OAI.KadisonSimilarity.tracialUltrapowerCompression_commutes_range line 30

Source documentation

An operator commuting with the original subfactor commutes with its entire included ultrapower after the actual Hilbert compression.

theorem tracialUltrapowerCompression_commutes_range
    (T : τB.GNS →L[ℂ] τB.GNS)
    (hcomm : ∀ a, T.comp (τB.gnsStarAlgHom (φ a)) =
      (τB.gnsStarAlgHom (φ a)).comp T) :
    ∀ x : (Φ).range,
      (tracialUltrapowerCompression τB hB ω trB T).comp ((τQ).gnsStarAlgHom (x : _)) =
        ((τQ).gnsStarAlgHom (x : _)).comp (tracialUltrapowerCompression τB hB ω trB T) := by
…

Mentions: OAI.KadisonSimilarity.tracialUltrapowerCompression

theorem OAI.KadisonSimilarity.tracialUltrapowerCompression_commutes_subalgebra line 53

Source documentation

Every smaller subalgebra of the included ultrapower inherits commutation.

theorem tracialUltrapowerCompression_commutes_subalgebra
    (D : StarSubalgebra ℂ (Ultrapower τB hB ω trB)) (hD : D ≤ (Φ).range)
    (T : τB.GNS →L[ℂ] τB.GNS)
    (hcomm : ∀ a, T.comp (τB.gnsStarAlgHom (φ a)) =
      (τB.gnsStarAlgHom (φ a)).comp T) :
    ∀ x : D,
      (tracialUltrapowerCompression τB hB ω trB T).comp ((τQ).gnsStarAlgHom (x : _)) =
        ((τQ).gnsStarAlgHom (x : _)).comp (tracialUltrapowerCompression τB hB ω trB T) :=
…

Mentions: OAI.KadisonSimilarity.tracialUltrapowerCompression

theorem OAI.KadisonSimilarity.included_ultrapower_traceCornerBound line 66

Source documentation

The exact strict trace gap gives the small-corner predicate consumed by the original free-corner theorem on any contained free subfactor.

theorem included_ultrapower_traceCornerBound
    (rounding : SpectralProjectionRoundingInput τA)
    (D : StarSubalgebra ℂ (Ultrapower τB hB ω trB)) (hD : D ≤ (Φ).range)
    (T : τB.GNS →L[ℂ] τB.GNS) {ε s t : ℝ} (hε : 0 ≤ ε) (hts : t < s)
    (hcorner : ∀ (q : A) (hq : IsStarProjection q), (τA q).re ≤ s →
      ∀ z : CStarCorner (φ q) (hq.map φ),
        ‖commutator T (τB.gnsStarAlgHom (z : B))‖ ≤ ε * ‖z‖) :
    (G).TraceCornerBound D (tracialUltrapowerCompression τB hB ω trB T) t ε := by
…

Mentions: OAI.KadisonSimilarity.SpectralProjectionRoundingInput, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.tracialUltrapowerCompression

theorem OAI.KadisonSimilarity.norm_commutator_le_ultrapower_constant_compression line 97

Source documentation

The final constant-subspace compression recovers the original commutator with no loss in its norm bound.

theorem norm_commutator_le_ultrapower_constant_compression
    (T : τB.GNS →L[ℂ] τB.GNS) (b : B) :
    ‖commutator T (τB.gnsStarAlgHom b)‖ ≤
      ‖(G).baseOperator (constant τB hB ω trB).range
        (commutator (tracialUltrapowerCompression τB hB ω trB T)
          ((τQ).gnsStarAlgHom (constant τB hB ω trB b)))‖ :=
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.tracialUltrapowerCompression