OAI/Analysis/BoundedHochschild/ProperlyInfiniteCorners.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Corner transport and finiteness obstructions for properly infinite projections.

  1. def OAI.BoundedHochschild.KadisonRingrose.partialIsoFromCorner line 18
  2. lemma OAI.BoundedHochschild.KadisonRingrose.partialIsoFromCorner_initial line 23
  3. lemma OAI.BoundedHochschild.KadisonRingrose.partialIsoFromCorner_final line 28
  4. lemma OAI.BoundedHochschild.KadisonRingrose.properlyInfinite_from_corner line 33
  5. lemma OAI.BoundedHochschild.KadisonRingrose.properlyInfinite_finite_eq_zero line 40
  6. lemma OAI.BoundedHochschild.KadisonRingrose.finiteAlgebra_of_equiv line 51
  7. lemma OAI.BoundedHochschild.KadisonRingrose.finiteCorner_of_equivalent line 60
  8. lemma OAI.BoundedHochschild.KadisonRingrose.properlyInfinite_central_cut line 66
  9. theorem OAI.BoundedHochschild.KadisonRingrose.exists_properlyInfinite_subprojection line 92

    Source documentation

    Every infinite corner contains a nonzero properly infinite projection.

    theorem exists_properlyInfinite_subprojection (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p : M} (hp : IsStarProjection p) (h : ¬ FiniteCorner p) :
    ∃ q : M, IsStarProjection q ∧ q ≤ p ∧ q ≠ 0 ∧ ProperlyInfiniteProjection q := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteCorner, OAI.BoundedHochschild.KadisonRingrose.ProperlyInfiniteProjection