CommonRightProjection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Right actions and the common subalgebra projection

The right action of a common unitary reduces the closed subspace generated by the common algebra and the standard vector. Thus equality of the two basic constructions gives the cross-commutant membership required for the common right-action argument, without identifying the whole commutant.

def OAI.KadisonKastler.conjugationUnitary line 21

Source documentation

Conjugating a unitary by an involutive conjugation is unitary.

def conjugationUnitary (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (u : unitary (H →L[ℂ] H)) : unitary (H →L[ℂ] H) :=
…

theorem OAI.KadisonKastler.conjugationUnitary_coe line 44
theorem OAI.KadisonKastler.conjugationOperator_star_unitary line 48

theorem OAI.KadisonKastler.vectorOrbitClosure_invariant_of_orbit line 68

Source documentation

A bounded operator preserving the algebra orbit also preserves its closed linear span.

theorem vectorOrbitClosure_invariant_of_orbit
    (R : StarSubalgebra ℂ (H →L[ℂ] H)) (Ω : H) (T : H →L[ℂ] H)
    (hT : ∀ x : R, ∃ y : R, T (x.val Ω) = y.val Ω)
    {ξ : H} (hξ : ξ ∈ Generator.vectorOrbitClosure R Ω) :
    T ξ ∈ Generator.vectorOrbitClosure R Ω := by
…

Mentions: OAI.Generator.vectorOrbitClosure

theorem OAI.KadisonKastler.conjugationOperator_commute_orbitProjection line 84

Source documentation

Right multiplication by a common unitary commutes with the orthogonal projection onto the common algebra's cyclic subspace.

theorem conjugationOperator_commute_orbitProjection
    (N : VonNeumannAlgebra H) (R : StarSubalgebra ℂ (H →L[ℂ] H))
    (hRN : R ≤ N.toStarSubalgebra) (J : H ≃ₗᵢ⋆[ℂ] H)
    (hJinv : Function.Involutive J) (Ω : H)
    (hJ : ∀ x : Algebra N, J (x.val Ω) = (star x).val Ω)
    (u : unitary (H →L[ℂ] H)) (hu : (u : H →L[ℂ] H) ∈ R) :
    (Generator.vectorOrbitClosure R Ω).starProjection * conjugationOperator J u =
      conjugationOperator J u * (Generator.vectorOrbitClosure R Ω).starProjection := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.Generator.vectorOrbitClosure, OAI.KadisonKastler.conjugationOperator

theorem OAI.KadisonKastler.mem_commutant_of_equal_basicConstruction line 114

Source documentation

Equality of the two basic constructions transports a commutant member which also commutes with their common projection.

theorem mem_commutant_of_equal_basicConstruction
    (M N : VonNeumannAlgebra H) (e q : H →L[ℂ] H)
    (hbasic : Set.centralizer (Set.centralizer ((M : Set (H →L[ℂ] H)) ∪ {e})) =
      Set.centralizer (Set.centralizer ((N : Set (H →L[ℂ] H)) ∪ {e})))
    (hq : q ∈ N.commutant) (he : e * q = q * e) : q ∈ M.commutant := by
…

theorem OAI.KadisonKastler.common_rightAction_of_equal_basicConstruction line 136

Source documentation

The basic-construction equality gives the common right action for every unitary of the common algebra, with no description of either full commutant required.

theorem common_rightAction_of_equal_basicConstruction
    (M N : VonNeumannAlgebra H) (R : StarSubalgebra ℂ (H →L[ℂ] H))
    (hRM : R ≤ M.toStarSubalgebra) (hRN : R ≤ N.toStarSubalgebra)
    (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H) (hJ₂ : Function.Involutive J₂) (Ω : H)
    (hM : ∀ x : Algebra M, J₁ (x.val Ω) = (star x).val Ω)
    (hN : ∀ x : Algebra N, J₂ (x.val Ω) = (star x).val Ω)
    (hcyclic : DenseRange (fun x : Algebra M => x.val Ω))
    (hcyclicN : DenseRange (fun x : Algebra N => x.val Ω))
    (hbasic :
      Set.centralizer (Set.centralizer ((M : Set (H →L[ℂ] H)) ∪
        {(Generator.vectorOrbitClosure R Ω).starProjection})) =
      Set.centralizer (Set.centralizer ((N : Set (H →L[ℂ] H)) ∪
…

Mentions: OAI.KadisonKastler.Algebra, OAI.Generator.vectorOrbitClosure