CentralProjectionPartitions.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Maximal central partitions

Orthogonal central projections have a supremum obtained from their finite sums. A maximal family of projections satisfying any prescribed property therefore has an actual complementary central projection. This construction does not use a trace or a countability hypothesis.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_orthogonal_central_supremum line 30

Source documentation

The supremum of an arbitrary orthogonal central family preserves its common annihilators. In particular, its complement completes the family to a partition.

theorem exists_orthogonal_central_supremum (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (p : I → M) (hp : ∀ i, IsStarProjection (p i))
    (hc : ∀ i a, p i * a = a * p i)
    (horth : ∀ i j, i ≠ j → p i * p j = 0) :
    ∃ q : M, IsStarProjection q ∧ (∀ a : M, q * a = a * q) ∧
      (∀ i, p i * q = p i) ∧
      (∀ a : M, (∀ i, p i * a = 0) → q * a = 0) := by
…

structure OAI.BoundedHochschild.KadisonRingrose.MaximalCentralPartition line 96
Source documentation
A maximal family satisfying P, together with its actual central complement.
```
structure MaximalCentralPartition (M : Type u) [CStarAlgebra M]
    [PartialOrder M] [StarOrderedRing M] (P : M → Prop) where
…
```
theorem OAI.BoundedHochschild.KadisonRingrose.exists_maximal_central_partition line 114
Source documentation
Zorn's lemma and bounded weak-star limits provide a maximal central partition.
```
theorem exists_maximal_central_partition (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (P : M → Prop) : Nonempty (MaximalCentralPartition M P) := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.MaximalCentralPartition