ConjugateRightIrreducibility.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Relative irreducibility in the conjugate right algebra

The scalar relative commutant property transports through the actual conjugate-linear operator map. In standard position its ambient image is the commutant, so the source's left irreducibility supplies the right one. The same central-vector identity supplies both orbit correspondences.

theorem OAI.KadisonKastler.conjugateRightAlgebra_mono line 19

theorem OAI.KadisonKastler.relative_irreducibility_conjugateRightAlgebra line 27

Source documentation

Scalar relative commutants are preserved by conjugation.

theorem relative_irreducibility_conjugateRightAlgebra
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (R M : VonNeumannAlgebra H)
    (hirr : ∀ T ∈ M, (∀ r ∈ R, r * T = T * r) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H)) :
    ∀ T ∈ conjugateRightAlgebra J hJ M,
      (∀ r ∈ conjugateRightAlgebra J hJ R, r * T = T * r) →
        ∃ z : ℂ, T = z • (1 : H →L[ℂ] H) := by
…

Mentions: OAI.KadisonKastler.conjugateRightAlgebra

theorem OAI.KadisonKastler.relative_irreducibility_commutant_of_conjugation line 46

Source documentation

The right relative commutant in a standard-position source is scalar.

theorem relative_irreducibility_commutant_of_conjugation
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (R M : VonNeumannAlgebra H)
    (hJM : conjugateRightAlgebra J hJ M = M.commutant)
    (hirr : ∀ T ∈ M, (∀ r ∈ R, r * T = T * r) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H)) :
    ∀ T ∈ M.commutant,
      (∀ r ∈ conjugateRightAlgebra J hJ R, r * T = T * r) →
        ∃ z : ℂ, T = z • (1 : H →L[ℂ] H) := by
…

Mentions: OAI.KadisonKastler.conjugateRightAlgebra

theorem OAI.KadisonKastler.commonRightVector_orbit_correspondence line 60

Source documentation

The central-vector identity gives both directions of the left/right orbit correspondence, including the adjoint required in the reverse one.

theorem commonRightVector_orbit_correspondence
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (R : VonNeumannAlgebra H) (Ω : H)
    (hvector : ∀ r ∈ R, conjugationOperator J (star r) Ω = r Ω) :
    (∀ r ∈ R, ∃ s ∈ conjugateRightAlgebra J hJ R, r Ω = s Ω) ∧
    (∀ s ∈ conjugateRightAlgebra J hJ R, ∃ r ∈ R, s Ω = r Ω) := by
…

Mentions: OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.conjugateRightAlgebra

theorem OAI.KadisonKastler.cyclic_separating_of_commonRight_irreducibility line 76

Source documentation

The two relative scalar commutants and the common-vector identity give actual cyclic and separating vectors for a neighbor.

theorem cyclic_separating_of_commonRight_irreducibility
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (R N : VonNeumannAlgebra H) (hRN : R ≤ N)
    (hSN : conjugateRightAlgebra J hJ R ≤ N.commutant)
    (Ω : H) (hΩ : Ω ≠ 0)
    (hirrR : ∀ T ∈ N, (∀ r ∈ R, r * T = T * r) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hirrS : ∀ T ∈ N.commutant,
      (∀ s ∈ conjugateRightAlgebra J hJ R, s * T = T * s) →
        ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hvector : ∀ r ∈ R, conjugationOperator J (star r) Ω = r Ω) :
    DenseRange (fun x : Algebra N => x.val Ω) ∧
…

Mentions: OAI.KadisonKastler.conjugateRightAlgebra, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.cyclic_separating_of_relative_irreducible_conjugation line 97

Source documentation

If J M J = M′, left relative irreducibility already supplies both relative scalar commutants needed by the common-vector argument.

theorem cyclic_separating_of_relative_irreducible_conjugation
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (R M : VonNeumannAlgebra H) (hRM : R ≤ M)
    (hJM : conjugateRightAlgebra J hJ M = M.commutant)
    (Ω : H) (hΩ : Ω ≠ 0)
    (hirr : ∀ T ∈ M, (∀ r ∈ R, r * T = T * r) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hvector : ∀ r ∈ R, conjugationOperator J (star r) Ω = r Ω) :
    DenseRange (fun x : Algebra M => x.val Ω) ∧
      DenseRange (fun x : Algebra M.commutant => x.val Ω) ∧
      (∀ a : Algebra M, a.val Ω = 0 → a = 0) ∧
      (∀ a : Algebra M.commutant, a.val Ω = 0 → a = 0) := by
…

Mentions: OAI.KadisonKastler.conjugateRightAlgebra, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.Algebra