PartialIsometryChains.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Suprema of chains of partial isometries

The initial projections have a supremum. A weak-star cluster point of the partial isometries agrees with each member on its initial projection. The common-annihilator property of the supremum then identifies its initial projection, without a trace or multiplication of two varying weak-star nets.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_partialIso_chain_supremum line 29

Source documentation

A nonempty chain of partial isometries has a least upper bound, whose initial and final projections respect every projection bound on the chain.

theorem exists_partialIso_chain_supremum (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (c : Set (PartialIso M)) (hc : IsChain (· ≤ ·) c) (hne : c.Nonempty) :
    ∃ w : PartialIso M, (∀ v ∈ c, v ≤ w) ∧
      (∀ z : PartialIso M, (∀ v ∈ c, v ≤ z) → w ≤ z) ∧
      (∀ r : M, IsStarProjection r → (∀ v ∈ c, v.initial ≤ r) → w.initial ≤ r) ∧
      (∀ r : M, IsStarProjection r → (∀ v ∈ c, v.final ≤ r) → w.final ≤ r) := by
…

theorem OAI.BoundedHochschild.KadisonRingrose.partialIso_chain_upper line 158

Source documentation

Projection bounds are retained by an upper bound of a chain of partial isometries, without a tracial state.

theorem partialIso_chain_upper (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p q : M} (hp : IsStarProjection p) (hq : IsStarProjection q)
    (c : Set (PartialIso M)) (hc : IsChain (· ≤ ·) c) (hne : c.Nonempty)
    (hs : ∀ v ∈ c, v.initial ≤ p ∧ v.final ≤ q) :
    ∃ w : PartialIso M, w.initial ≤ p ∧ w.final ≤ q ∧ ∀ v ∈ c, v ≤ w := by
…