OAI/Analysis/KadisonKastler/TomitaCentralizerConjugation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.tomitaPolarCoordinates_centralizer line 15
2. theorem OAI.KadisonKastler.tomitaPolarConjugation_centralizer line 30

   Source documentation

   On centralizer vectors the polar conjugation is precisely adjoint.

   theorem tomitaPolarConjugation_centralizer (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
       (hsep : Function.Injective (algebraVectorMap M Ω))
       (hcyc : DenseRange (algebraVectorMap M Ω)) (r : Algebra M)
       (hr : ∀ a : Algebra M,
         inner ℂ Ω ((r.val * a.val) Ω) = inner ℂ Ω ((a.val * r.val) Ω)) :
       tomitaPolarConjugation J Ω hsep hcyc (r.val Ω) = star r.val Ω := by
   …

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

3. theorem OAI.KadisonKastler.tomitaPolarConjugation_star_centralizer line 63

   Source documentation

   Modular conjugation agrees with the adjoint on centralizer vectors.

   theorem tomitaPolarConjugation_star_centralizer (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
       (hsep : Function.Injective (algebraVectorMap M Ω))
       (hcyc : DenseRange (algebraVectorMap M Ω)) (r : Algebra M)
       (hr : ∀ a : Algebra M,
         inner ℂ Ω ((r.val * a.val) Ω) = inner ℂ Ω ((a.val * r.val) Ω)) :
       tomitaPolarConjugation J Ω hsep hcyc (star r.val Ω) = r.val Ω := by
   …

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