OAI/Analysis/PureInfiniteness/AbelianRangeExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The abelian-range extension of KR02 Proposition 7.13, stated using the inclusion homomorphisms of the separable algebras. It provides an actual one-step inner map in the norm ultrapower.

  1. theorem OAI.WeakPureInfiniteness.exists_abelian_range_compression line 24
  2. theorem OAI.WeakPureInfiniteness.abelian_range_extension_cpc line 42

    Source documentation

    The completely positive contraction accompanying the actual compressor.

    theorem abelian_range_extension_cpc (hP : MainGap.PropertyP A)
    (β : B →⋆ₙₐ[ℂ] N) (γ : C →⋆ₙₐ[ℂ] N) :
    ∃ v : N, ∃ T : B →L[ℂ] N,
      ‖v‖ ≤ 1 ∧ (∀ b, T b = star v * β b * v) ∧
      CompletelyPositive T ∧ ‖T‖ ≤ 1 ∧
      (∀ c, star v * γ c * v = γ c) ∧ ∀ x y, Commute (T x) (T y) := by
…

    Mentions: OAI.MainGap.PropertyP, OAI.WeakPureInfiniteness.CompletelyPositive