DerivationCyclicPowers.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Countable cyclic multiplicity of a one-implementer extension

If a cyclic representation is generated by a source algebra and a self-adjoint derivation implementer, powers of that implementer applied to the cyclic vector generate the representation as a source module. Consequently the source commutant has countable projection families.

theorem OAI.KadisonKastler.denseRange_derivation_power_span line 22

theorem OAI.KadisonKastler.derivation_extension_commutant_countable line 82

Source documentation

Countability needed by the spatial splitting proof, even when the source or its cyclic representation is nonseparable.

theorem derivation_extension_commutant_countable
    (φ : A →⋆ₐ[ℂ] B) (d : B) (hdsa : IsSelfAdjoint d)
    (hgen : NormGeneratedExtension φ d)
    (D : A →L[ℂ] A) (hd : ∀ a, φ (D a) = d * φ a - φ a * d)
    (π : B →⋆ₐ[ℂ] (H →L[ℂ] H)) (ξ : H)
    (hcyc : DenseRange (fun b => π b ξ)) :
    HasCountableProjectionFamilies
      (generatedVonNeumannAlgebra (π.comp φ).range).commutant := by
…

Mentions: OAI.KadisonKastler.NormGeneratedExtension, OAI.KadisonKastler.HasCountableProjectionFamilies, OAI.KadisonKastler.generatedVonNeumannAlgebra