StatePreservingWeakLimit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

State-preserving weak limits of matrix retractions

The limiting map retains the vector state on the larger algebra. Its restriction is a bimodular expectation onto the smaller algebra.

theorem OAI.KadisonKastler.exists_state_preserving_weak_retraction line 24

Source documentation

Retain both the range and the state when passing to a weak ultralimit.

theorem exists_state_preserving_weak_retraction
    (hNM : N ≤ M) (τ : TracialRepresentation N)
    (F : ℕ → (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H))
    (hF : ∀ n, ‖F n‖ ≤ 1) (hmem : ∀ n T, F n T ∈ N)
    (hfix : ∀ a : Algebra N, Tendsto (fun n => F n a.val τ.vector) atTop
      (𝓝 (a.val τ.vector)))
    (hstate : ∀ n (a : Algebra M),
      inner ℂ τ.vector (F n a.val τ.vector) = inner ℂ τ.vector (a.val τ.vector)) :
    ∃ P : Algebra M →L[ℂ] Algebra N,
      ‖P‖ ≤ 1 ∧
      (∀ a : Algebra N, P (coordinateInclusion hNM a) = a) ∧
      (∀ a : Algebra M,
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.retraction_bimodule line 71

Source documentation

A contractive retraction onto a von Neumann algebra is bimodular.

theorem retraction_bimodule (hNM : N ≤ M) (P : Algebra M →L[ℂ] Algebra N)
    (hP : ‖P‖ ≤ 1) (hfix : ∀ a : Algebra N, P (coordinateInclusion hNM a) = a) :
    (∀ (a : Algebra N) (x : Algebra M),
      P (coordinateInclusion hNM a * x) = a * P x) ∧
    (∀ (a : Algebra N) (x : Algebra M),
      P (x * coordinateInclusion hNM a) = P x * a) := by
…

Mentions: OAI.KadisonKastler.Algebra