OAI/Analysis/BoundedHochschild/AbelianPartitions.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Common finite partitions for commuting projections

A finite family of projections in a commutative C⋆-algebra admits a common orthogonal partition of unity. Adjoining one projection refines every cell by multiplication with that projection and its complement. Zero cells are retained, so no nonzero or trace assumptions are needed.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.split_same line 23
  2. lemma OAI.BoundedHochschild.KadisonRingrose.split_cross line 29
  3. lemma OAI.BoundedHochschild.KadisonRingrose.decides_mul line 37
  4. theorem OAI.BoundedHochschild.KadisonRingrose.exists_refining_partition line 44

    Source documentation

    A common orthogonal partition of unity for any finite family of projections.

    theorem exists_refining_partition (S : Finset {q : M // IsStarProjection q}) :
    ∃ (n : ℕ) (p : Fin n → M),
      (∀ i, IsStarProjection (p i)) ∧
      (∀ i j, i ≠ j → p i * p j = 0) ∧
      (∑ i, p i) = 1 ∧
      (∀ q ∈ S, ∀ i, q.val * p i = 0 ∨ q.val * p i = p i) := by
…