OAI/Analysis/BoundedHochschild/FiniteProjectionExtension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Extension of embeddings in finite corners

A partial embedding into a finite projection extends whenever an embedding of the larger initial projection exists. This is the cancellation step used in Ringrose, Lectures on the trace in a finite von Neumann algebra, Lemma 5.1. The construction uses only the predual and finiteness, not a trace.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.partialIso_left_support line 26
  2. lemma OAI.BoundedHochschild.KadisonRingrose.partialIso_right_support line 33
  3. theorem OAI.BoundedHochschild.KadisonRingrose.finite_partialIso_extends_in_corner line 42

    Source documentation

    The unitary extending a supported partial isometry can be chosen in the same finite corner. Its ambient initial and final projections are that corner.

    theorem finite_partialIso_extends_in_corner (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {q : M} (hq : IsStarProjection q) (hfinite : FiniteCorner q)
    (v : PartialIso M) (hi : v.initial ≤ q) (hf : v.final ≤ q) :
    ∃ u : M, q * u = u ∧ u * q = u ∧ star u * u = q ∧ u * star u = q ∧
      u * v.initial = v := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteCorner

  4. theorem OAI.BoundedHochschild.KadisonRingrose.finite_partialIso_extension line 60

    Source documentation

    An embedding of a smaller projection into a finite corner extends to an embedding of a larger projection as soon as the latter embeds in that corner.

    theorem finite_partialIso_extension (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {q : M} (hq : IsStarProjection q) (hfinite : FiniteCorner q)
    (v w : PartialIso M) (hvw : v.initial ≤ w.initial)
    (hvq : v.final ≤ q) (hwq : w.final ≤ q) :
    ∃ t : PartialIso M, v ≤ t ∧ t.initial = w.initial ∧ t.final ≤ q := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteCorner