TraceFreeComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Projection comparison before constructing a trace

Maximal partial isometries and the central comparison theorem are constructed directly from a predual. Their proofs do not presuppose the trace whose existence is needed in the finite-algebra reduction.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_maximal_partialIso line 28

Source documentation

The unmatched remainders of a maximal partial isometry have no connecting corner.

theorem exists_maximal_partialIso (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p q : M} (hp : IsStarProjection p) (hq : IsStarProjection q) :
    ∃ v : PartialIso M, v.initial ≤ p ∧ v.final ≤ q ∧
      ∀ a : M, (q - v.final) * a * (p - v.initial) = 0 := by
…

theorem OAI.BoundedHochschild.KadisonRingrose.trace_free_central_comparison line 71

Source documentation

Murray--von Neumann comparison over complementary central parts, with no trace assumption. This is the structural comparison used before trace existence.

theorem trace_free_central_comparison (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p q : M} (hp : IsStarProjection p) (hq : IsStarProjection q) :
    ∃ (z : M) (v : PartialIso M), CentralProjection z ∧ v.initial ≤ p ∧ v.final ≤ q ∧
      z * v.final = z * q ∧ (1 - z) * v.initial = (1 - z) * p := by
…