CentralProjectionSuprema.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Suprema of chains of central projections

A nonempty chain of central projections has a central projection supremum. A bounded weak-star cluster point is a projection because multiplication by each member of the chain eventually stabilizes. The same limiting argument preserves annihilation of any fixed element. No trace is used.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_central_projection_chain_supremum_with_limit line 26

Source documentation

A chain of central projections has a least projection upper bound, preserving any common right annihilator.

theorem exists_central_projection_chain_supremum_with_limit
    (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (S : Set M) (hne : S.Nonempty) (hchain : IsChain (· ≤ ·) S)
    (hproj : ∀ q ∈ S, IsStarProjection q)
    (hcentral : ∀ q ∈ S, ∀ a : M, q * a = a * q) :
    ∃ p : M, IsStarProjection p ∧ (∀ a : M, p * a = a * p) ∧
      (∀ q ∈ S, q ≤ p) ∧
      (∀ r : M, IsStarProjection r → (∀ q ∈ S, q ≤ r) → p ≤ r) ∧
      (∀ a : M, (∀ q ∈ S, q * a = 0) → p * a = 0) ∧
      ∃ U : Ultrafilter S, (U : Filter S) ≤ atTop ∧
        PredualTendsto e (fun q : S => (q : M)) (U : Filter S) p := by
…

Mentions: OAI.BoundedHochschild.PredualTendsto

theorem OAI.BoundedHochschild.KadisonRingrose.exists_central_projection_chain_supremum line 98

Source documentation

A chain of central projections has a least projection upper bound, preserving any common right annihilator.

theorem exists_central_projection_chain_supremum
    (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (S : Set M) (hne : S.Nonempty) (hchain : IsChain (· ≤ ·) S)
    (hproj : ∀ q ∈ S, IsStarProjection q)
    (hcentral : ∀ q ∈ S, ∀ a : M, q * a = a * q) :
    ∃ p : M, IsStarProjection p ∧ (∀ a : M, p * a = a * p) ∧
      (∀ q ∈ S, q ≤ p) ∧
      (∀ r : M, IsStarProjection r → (∀ q ∈ S, q ≤ r) → p ≤ r) ∧
      (∀ a : M, (∀ q ∈ S, q * a = 0) → p * a = 0) := by
…