OAI/Analysis/KadisonKastler/NormalTypeIII1Transport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Type III₁ transport for specified normal representation changes

  1. theorem OAI.KadisonKastler.TypeIII1Factor.of_normalStarAlgEquiv line 20
  2. theorem OAI.KadisonKastler.TypeIII1Factor.of_normalStarAlgEquiv_symm line 37
  3. theorem OAI.KadisonKastler.TypeIII1Factor.of_normalHom line 56

    Source documentation

    Pull the type conclusion back through a faithful normal representation with a specified concrete range.

    theorem TypeIII1Factor.of_normalHom (hN : TypeIII1Factor N)
    (φ : Algebra M →⋆ₐ[ℂ] (K →L[ℂ] K)) (hfaith : Function.Injective φ)
    (hφ : BoundedWeakNormal M φ) (hmem : ∀ a, φ a ∈ N)
    (hrange : generatedVonNeumannAlgebra φ.range = N)
    (ξ : K) (hξ : ‖ξ‖ = 1) (hc : DenseRange (algebraVectorMap N ξ))
    (hs : Function.Injective (algebraVectorMap N ξ)) (m : ModularSpectralResolution N ξ) :
    TypeIII1Factor M :=
…

    Mentions: OAI.KadisonKastler.TypeIII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.BoundedWeakNormal, OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.ModularSpectralResolution