OAI/Analysis/KadisonKastler/HilbertConjugation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An auxiliary conjugate copy of an arbitrary Hilbert space

Coordinate conjugation supplies the fixed antiunitary used to write the Tomita graph as a complex-linear graph. The polar conjugation is then constructed from that graph; no modular theorem is invoked here.

  1. def OAI.KadisonKastler.coordinateConjugation line 17
  2. theorem OAI.KadisonKastler.exists_hilbert_conjugation line 28
  3. theorem OAI.KadisonKastler.exists_polar_conjugation line 39

    Source documentation

    The graph construction gives an involutive conjugation fixing the state vector and satisfying the full centralizer-vector clause. The commutant clause of modular conjugation is not asserted by this theorem.

    theorem exists_polar_conjugation {M : VonNeumannAlgebra H} (Ω : H)
    (hsep : Function.Injective (algebraVectorMap M Ω))
    (hcyc : DenseRange (algebraVectorMap M Ω)) :
    ∃ J : H ≃ₗᵢ⋆[ℂ] H, Function.Involutive J ∧ J Ω = Ω ∧
      ∀ r : Algebra M,
        (∀ a : Algebra M,
          inner ℂ Ω ((r.val * a.val) Ω) = inner ℂ Ω ((a.val * r.val) Ω)) →
        J (star r.val Ω) = r.val Ω := by
…

    Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.Algebra