OAI/Analysis/KadisonKastler/NormUltraproduct.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual norm ultraproduct for the infinitesimal normalizer argument

The null sequences form a closed star ideal in the bounded product. Its C-star quotient is the norm ultraproduct used in the infinitesimal normalizer argument.

  1. def OAI.KadisonKastler.NormNullSequence line 22
  2. theorem OAI.KadisonKastler.normNullSequence_add line 26
  3. theorem OAI.KadisonKastler.normNullSequence_mul_left line 33
  4. theorem OAI.KadisonKastler.normNullSequence_mul_right line 42
  5. theorem OAI.KadisonKastler.isClosed_normNullSequence line 50
  6. def OAI.KadisonKastler.normNullClosedIdeal line 67
  7. abbrev OAI.KadisonKastler.NormUltraproduct line 90
  8. instance OAI.KadisonKastler.normUltraproductCStarAlgebra line 95
  9. def OAI.KadisonKastler.normUltraproductMap line 98
  10. theorem OAI.KadisonKastler.normUltraproductMap_surjective line 102
  11. theorem OAI.KadisonKastler.normUltraproductMap_eq_zero_iff line 106
  12. instance OAI.KadisonKastler.normUltraproductNontrivial line 120
  13. theorem OAI.KadisonKastler.exists_selfAdjoint_normUltraproduct_lift line 133

    Source documentation

    Taking the self-adjoint part supplies actual self-adjoint sequence representatives for the implementer produced by Sakai's theorem.

    theorem exists_selfAdjoint_normUltraproduct_lift (ω : Ultrafilter ℕ)
    (a : NormUltraproduct B ω) (ha : IsSelfAdjoint a) :
    ∃ x : VaryingBoundedSequence B, IsSelfAdjoint x ∧ normUltraproductMap B ω x = a := by
…

    Mentions: OAI.KadisonKastler.NormUltraproduct, OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.normUltraproductMap