TraceFreeHalving.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Halving projections without a trace

Orthogonality of initial and final projections is preserved by increasing chains of partial isometries. A maximal such partial isometry exhausts any projection in an algebra with no nonzero abelian corners.

lemma OAI.BoundedHochschild.KadisonRingrose.orthogonal_partialIso_chain_upper line 26

Source documentation

The initial/final orthogonality condition is closed under chain suprema.

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

theorem OAI.BoundedHochschild.KadisonRingrose.exists_trace_free_halving line 66
Source documentation
Every projection in a von Neumann algebra without abelian corners is the sum of the orthogonal initial and final projections of a partial isometry.
```
theorem exists_trace_free_halving (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hII : PopaTypeII.NoAbelianCorners M) {p : M} (hp : IsStarProjection p) :
    ∃ v : PartialIso M, v.initial * v.final = 0 ∧ v.initial + v.final = p := by
…
```
Mentions: OAI.PopaTypeII.NoAbelianCorners

theorem OAI.BoundedHochschild.KadisonRingrose.trace_free_halve_projection line 138

Source documentation

Corner-isometry form of trace-free halving, matching the tracial API.

theorem trace_free_halve_projection (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hII : PopaTypeII.NoAbelianCorners M) {p : M} (hp : IsStarProjection p) :
    ∃ v : PopaCorners.CornerIso p p, v.initial * v.final = 0 ∧
      v.initial + v.final = p := by
…

Mentions: OAI.PopaTypeII.NoAbelianCorners, OAI.PopaCorners.CornerIso