JointRankOneFactors.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Countable rank-one tests in the joint representation force the first source's represented von Neumann algebra to be a factor.

theorem OAI.KadisonSimilarity.joint_first_scalar_center_of_rankOne line 17

Source documentation

No measurable selection is needed: centrality and dense rank-one tests in the joint bicommutant force each central operator to be scalar.

theorem joint_first_scalar_center_of_rankOne
    (B C : StarSubalgebra ℂ A)
    [IsClosed (B : Set A)] [IsClosed (C : Set A)]
    (hBC : ∀ b : B, ∀ c : C, (b : A) * (c : A) = (c : A) * (b : A))
    (σ : jointCStarSource B C →⋆ₐ[ℂ] (K →L[ℂ] K))
    (d : ι → K) (hd : DenseRange d)
    (hRank : ∀ i j, InnerProductSpace.rankOne ℂ (d i) (d j) ∈
      representationVonNeumannAlgebra σ) :
    ∀ a : (representationVonNeumannAlgebra
      (σ.comp (StarSubalgebra.inclusion (le_jointCStarSource_left B C)))).toStarSubalgebra,
      (∀ b, a * b = b * a) → ∃ c : ℂ, a = algebraMap ℂ _ c := by
…

Mentions: OAI.KadisonSimilarity.jointCStarSource, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.le_jointCStarSource_left