OAI/Analysis/BoundedHochschild/OrthogonalPartialIsoSums.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Countable orthogonal sums of partial isometries

These sums supply the actual shift operators used in the properly infinite case. Both initial and final projections are identified by their least-upper- bound properties; no trace is used.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.partialIso_finset_sum_data line 24
  2. def OAI.BoundedHochschild.KadisonRingrose.partialIsoFinsetSum line 46
  3. lemma OAI.BoundedHochschild.KadisonRingrose.partialIsoFinsetSum_coe line 52
  4. lemma OAI.BoundedHochschild.KadisonRingrose.partialIsoFinsetSum_initial line 57
  5. lemma OAI.BoundedHochschild.KadisonRingrose.partialIsoFinsetSum_final line 62
  6. lemma OAI.BoundedHochschild.KadisonRingrose.partialIsoFinsetSum_mono line 66
  7. theorem OAI.BoundedHochschild.KadisonRingrose.exists_countable_partialIso_sum line 91

    Source documentation

    A countable family with mutually orthogonal initial and final projections has a sum whose initial and final projections are the respective suprema.

    theorem exists_countable_partialIso_sum (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (v : ℕ → PartialIso M)
    (hi : ∀ i j, i ≠ j → (v i).initial * (v j).initial = 0)
    (hf : ∀ i j, i ≠ j → (v i).final * (v j).final = 0) :
    ∃ w : PartialIso M, (∀ i, (v i).initial ≤ w.initial) ∧
      (∀ i, (v i).final ≤ w.final) ∧
      (∀ p : M, IsStarProjection p → (∀ i, (v i).initial ≤ p) → w.initial ≤ p) ∧
      (∀ p : M, IsStarProjection p → (∀ i, (v i).final ≤ p) → w.final ≤ p) := by
…