OAI/Analysis/KadisonSimilarity/Derivation/DerivationDefectSpace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The reducing defect space of a factorized derivation. It will provide the sharp implementing operator in the commutant-distance formula.

  1. def OAI.KadisonSimilarity.derivationDefect line 16
  2. def OAI.KadisonSimilarity.derivationDefectSpace line 20
  3. theorem OAI.KadisonSimilarity.derivationDefect_mem line 24
  4. theorem OAI.KadisonSimilarity.derivationDefect_mul line 31
  5. theorem OAI.KadisonSimilarity.derivationDefectSpace_invariant line 40
  6. theorem OAI.KadisonSimilarity.derivationDefectSpace_intertwines line 58

    Source documentation

    The left factor intertwines the two representations on the defect space.

    theorem derivationDefectSpace_intertwines
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (π : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (U : K →L[ℂ] H) (W : H →L[ℂ] K) (δ : A →L[ℂ] (H →L[ℂ] H))
    (hδ : ∀ a b, δ (a * b) = (σ a).comp (δ b) + (δ a).comp (σ b))
    (hF : ∀ a, U.comp ((π a).comp W) = δ a) (hUW : U.comp W = 0)
    (b : A) (x : K) (hx : x ∈ derivationDefectSpace σ π W) :
    U (π b x) = σ b (U x) := by
…

    Mentions: OAI.KadisonSimilarity.derivationDefectSpace