OAI/Analysis/KadisonKastler/DerivationStarReduction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Reduction to anti-star derivations

Sakai's spatial construction treats derivations satisfying D (star x) = -star (D x). Every bounded complex derivation is a complex linear combination of two such derivations. That decomposition transfers innerness from anti-star derivations to arbitrary bounded complex derivations.

  1. theorem OAI.KadisonKastler.derivation_central_idempotent_eq_zero line 23

    Source documentation

    A derivation vanishes on an idempotent which commutes with its image. In particular it vanishes on every central projection.

    theorem derivation_central_idempotent_eq_zero (D : A →L[ℂ] A)
    (hD : ∀ x y, D (x * y) = D x * y + x * D y)
    (p : A) (hp : p * p = p) (hc : Commute p (D p)) : D p = 0 := by
…
  2. def OAI.KadisonKastler.starConjugateMap line 47
  3. theorem OAI.KadisonKastler.starConjugateMap_apply line 53
  4. theorem OAI.KadisonKastler.starConjugateMap_leibniz line 56
  5. theorem OAI.KadisonKastler.leibniz_combination line 64
  6. theorem OAI.KadisonKastler.exists_antiStar_derivation_decomposition line 74
  7. theorem OAI.KadisonKastler.inner_derivation_of_antiStar_inner line 104