OAI/Analysis/PureInfiniteness/ExactFiniteAbelianization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact finite spectral abelianization in the norm ultrapower. The witness comes from polynomial norm conditions; multiplicativity is not inferred from centrality of a completely positive map.

  1. def OAI.WeakPureInfiniteness.finiteAbelianizationTest line 23
  2. lemma OAI.WeakPureInfiniteness.finiteAbelianizationTest_nonneg line 33
  3. theorem OAI.WeakPureInfiniteness.ultrapower_finite_abelianization_exact line 40
  4. theorem OAI.WeakPureInfiniteness.ultrapower_finite_relative_abelianization line 104

    Source documentation

    Relative support and commutation are consequences of preserving both moments, not assumptions about the completely positive compression.

    theorem ultrapower_finite_relative_abelianization (hP : MainGap.PropertyP A)
    (a : I → N) (ha : ∀ i, 0 ≤ a i) (hc : ∀ i j, Commute (a i) (a j))
    (b : N) (hb : IsSelfAdjoint b) :
    ∃ v : N, ‖v‖ ≤ 1 ∧ (∀ i, a i * v = v * a i ∧ (star v * v) * a i = a i) ∧
      ∀ i, Commute (a i) (star v * b * v) := by
…

    Mentions: OAI.MainGap.PropertyP