OAI/Analysis/BoundedHochschild/PartialIsoProducts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Products of composable partial isometries and comparison of complements.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.partialIso_product_initial line 19
  2. def OAI.BoundedHochschild.KadisonRingrose.composePartialIso line 28

    Source documentation

    Compose two partial isometries when the final support of the second lies in the initial support of the first.

    def composePartialIso (v w : PartialIso M) (h : w.final ≤ v.initial) : PartialIso M :=
…
  3. lemma OAI.BoundedHochschild.KadisonRingrose.composePartialIso_initial line 32
  4. lemma OAI.BoundedHochschild.KadisonRingrose.composePartialIso_final_le line 35
  5. theorem OAI.BoundedHochschild.KadisonRingrose.finite_complement_subequivalence line 43

    Source documentation

    Finiteness reverses subequivalence on complementary projections.

    theorem finite_complement_subequivalence (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) {p q : M} (hp : IsStarProjection p)
    (hq : IsStarProjection q) (v : PartialIso M)
    (hi : v.initial = p) (hf : v.final ≤ q) :
    ∃ w : PartialIso M, w.initial = 1 - q ∧ w.final ≤ 1 - p := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra