PreparedPairCyclicity.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Cyclicity from the common left and right vector actions

The projection onto the closed commutant orbit belongs to the original von Neumann algebra. Common vector actions make it commute with the irreducible common subalgebra, so its scalar value is one. Applying the same argument to the commutant proves both cyclicity and separation. No cyclicity or standard-form conclusion is assumed.

theorem OAI.KadisonKastler.commutant_orbit_invariant_of_common_vector line 23

Source documentation

A common right vector value makes the left action preserve the closed commutant orbit.

theorem commutant_orbit_invariant_of_common_vector
    (N : VonNeumannAlgebra H) (Ω : H)
    (r : H →L[ℂ] H) (hr : r ∈ N)
    (s : H →L[ℂ] H) (hs : s ∈ N.commutant)
    (hvector : r Ω = s Ω)
    {ξ : H} (hξ : ξ ∈ Generator.vectorOrbitClosure N.commutant.toStarSubalgebra Ω) :
    r ξ ∈ Generator.vectorOrbitClosure N.commutant.toStarSubalgebra Ω := by
…

Mentions: OAI.Generator.vectorOrbitClosure

theorem OAI.KadisonKastler.commutant_orbitClosure_eq_top_of_relative_scalar line 43

Source documentation

Irreducibility and common vector actions force the commutant orbit to be all of the actual Hilbert space.

theorem commutant_orbitClosure_eq_top_of_relative_scalar
    (N : VonNeumannAlgebra H) (R : StarSubalgebra ℂ (H →L[ℂ] H))
    (hRN : R ≤ N.toStarSubalgebra) (Ω : H) (hΩ : Ω ≠ 0)
    (hirr : ∀ T ∈ N, (∀ r ∈ R, r * T = T * r) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hvector : ∀ r ∈ R, ∃ s ∈ N.commutant, r Ω = s Ω) :
    Generator.vectorOrbitClosure N.commutant.toStarSubalgebra Ω = ⊤ := by
…

Mentions: OAI.Generator.vectorOrbitClosure

theorem OAI.KadisonKastler.commutant_orbit_dense_of_relative_scalar line 85

Source documentation

The corresponding dense-range formulation is suitable for uniqueness of operators on the commutant orbit.

theorem commutant_orbit_dense_of_relative_scalar
    (N : VonNeumannAlgebra H) (R : StarSubalgebra ℂ (H →L[ℂ] H))
    (hRN : R ≤ N.toStarSubalgebra) (Ω : H) (hΩ : Ω ≠ 0)
    (hirr : ∀ T ∈ N, (∀ r ∈ R, r * T = T * r) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hvector : ∀ r ∈ R, ∃ s ∈ N.commutant, r Ω = s Ω) :
    DenseRange (fun x : Algebra N.commutant => x.val Ω) := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.preparedPair_dense_orbits line 100

Source documentation

The common left/right vector correspondence gives both dense orbits. Only the two relative scalar-commutant statements are used.

theorem preparedPair_dense_orbits
    (N : VonNeumannAlgebra H)
    (R S : StarSubalgebra ℂ (H →L[ℂ] H))
    (hRN : R ≤ N.toStarSubalgebra) (hSN : S ≤ N.commutant.toStarSubalgebra)
    (Ω : H) (hΩ : Ω ≠ 0)
    (hirrR : ∀ T ∈ N, (∀ r ∈ R, r * T = T * r) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hirrS : ∀ T ∈ N.commutant, (∀ s ∈ S, s * T = T * s) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hRS : ∀ r ∈ R, ∃ s ∈ S, r Ω = s Ω)
    (hSR : ∀ s ∈ S, ∃ r ∈ R, s Ω = r Ω) :
    DenseRange (fun x : Algebra N => x.val Ω) ∧
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.separating_of_dense_commutant_orbit line 129

Source documentation

A vector cyclic for the commutant separates the original algebra.

theorem separating_of_dense_commutant_orbit
    (N : VonNeumannAlgebra H) (Ω : H)
    (hcyclic : DenseRange (fun x : Algebra N.commutant => x.val Ω))
    (a : Algebra N) (ha : a.val Ω = 0) : a = 0 := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.preparedPair_cyclic_separating line 143

Source documentation

In the prepared-pair argument, the actual common vector is cyclic and separating for both sides; no separate standard-position premise remains.

theorem preparedPair_cyclic_separating
    (N : VonNeumannAlgebra H)
    (R S : StarSubalgebra ℂ (H →L[ℂ] H))
    (hRN : R ≤ N.toStarSubalgebra) (hSN : S ≤ N.commutant.toStarSubalgebra)
    (Ω : H) (hΩ : Ω ≠ 0)
    (hirrR : ∀ T ∈ N, (∀ r ∈ R, r * T = T * r) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hirrS : ∀ T ∈ N.commutant, (∀ s ∈ S, s * T = T * s) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hRS : ∀ r ∈ R, ∃ s ∈ S, r Ω = s Ω)
    (hSR : ∀ s ∈ S, ∃ r ∈ R, s Ω = r Ω) :
    DenseRange (fun x : Algebra N => x.val Ω) ∧
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.preparedPair_cyclic_separating_of_conjugate_algebra line 168

Source documentation

The source's central-vector identity supplies both vector correspondences when the right algebra is the conjugate of the left one.

theorem preparedPair_cyclic_separating_of_conjugate_algebra
    (N : VonNeumannAlgebra H)
    (R S : StarSubalgebra ℂ (H →L[ℂ] H))
    (hRN : R ≤ N.toStarSubalgebra) (hSN : S ≤ N.commutant.toStarSubalgebra)
    (J : H ≃ₗᵢ⋆[ℂ] H)
    (hS : (S : Set (H →L[ℂ] H)) = conjugationOperator J '' (R : Set (H →L[ℂ] H)))
    (Ω : H) (hΩ : Ω ≠ 0)
    (hirrR : ∀ T ∈ N, (∀ r ∈ R, r * T = T * r) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hirrS : ∀ T ∈ N.commutant, (∀ s ∈ S, s * T = T * s) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hcentral : ∀ r ∈ R, r Ω = conjugationOperator J (star r) Ω) :
…

Mentions: OAI.KadisonKastler.conjugationOperator