OAI/Analysis/KadisonKastler/RestrictedInnerDerivation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Restricting a spatial commutator to an invariant C-star subalgebra

An injective star homomorphism reflects the algebraic identities and the norm bound. Thus invariance under an ambient commutator gives an actual bounded derivation on the source algebra.

  1. theorem OAI.KadisonKastler.exists_restricted_inner_derivation line 21
  2. theorem OAI.KadisonKastler.exists_selfAdjoint_ambient_correction line 62