OAI/Analysis/KadisonKastler/IrreducibleTracialState.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.vector_state_central_of_commuting_right_representatives line 20

   Source documentation

   Commuting right representatives of the common algebra make the vector state central over that algebra.

   theorem vector_state_central_of_commuting_right_representatives
       (M R : VonNeumannAlgebra H) (hRM : R ≤ M) (ξ : H)
       (hright : ∀ r : Algebra R, ∃ b : H →L[ℂ] H,
         b ∈ M.commutant ∧ b ξ = r.val ξ ∧ star b ξ = star r.val ξ)
       (r : Algebra R) (a : Algebra M) :
       inner ℂ ξ ((coordinateInclusion hRM r * a).val ξ) =
         inner ℂ ξ ((a * coordinateInclusion hRM r).val ξ) := by
   …

   Mentions: OAI.KadisonKastler.Algebra

2. theorem OAI.KadisonKastler.ii1_vector_state_eq_trace_of_relative_central line 44
3. def OAI.KadisonKastler.standardTracialPosition_of_relative_central line 68

   Source documentation

   Once cyclicity is known, relative centrality supplies all remaining standard tracial position data.

   def standardTracialPosition_of_relative_central
       (M R : VonNeumannAlgebra H) (hRM : R ≤ M)
       (hM : Generator.IsII1Factor M.toStarSubalgebra)
       (hirr : ∀ a : Algebra M, a.val ∈ R.commutant → ∃ c : ℂ, a = c • 1)
       (ξ : H) (hξ : ‖ξ‖ = 1)
       (hcentral : ∀ (r : Algebra R) (a : Algebra M),
         inner ℂ ξ ((coordinateInclusion hRM r * a).val ξ) =
         inner ℂ ξ ((a * coordinateInclusion hRM r).val ξ))
       (hcyclic : DenseRange (algebraVectorMap M ξ)) : StandardTracialPosition M where
   …

   Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.StandardTracialPosition