CentralVectorSpace.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Central vectors and the relative commutant

The central-vector space used in Haagerup's construction is a closed complex subspace. A one-dimensional central-vector space detects an irreducible inclusion once its generating vector is separating.

def OAI.KadisonKastler.centralVectorSpace line 22
Source documentation
Vectors on which left and conjugate-right multiplication agree.
```
def centralVectorSpace (N : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) : Submodule ℂ H where
…
```
theorem OAI.KadisonKastler.mem_centralVectorSpace line 32
theorem OAI.KadisonKastler.centralVectorSpace_isClosed line 36
instance OAI.KadisonKastler.centralVectorSpace_complete line 43
theorem OAI.KadisonKastler.centralVectorSpace_antitone line 47

theorem OAI.KadisonKastler.centralVectorSpace_invariant line 53

Source documentation

The relative commutant acts on central vectors.

theorem centralVectorSpace_invariant (J : H ≃ₗᵢ⋆[ℂ] H)
    (hright : ∀ a : Algebra N, conjugationOperator J (star a).val ∈ M.commutant)
    (T : H →L[ℂ] H) (hT : T ∈ M)
    (hcomm : ∀ a : Algebra N, a.val * T = T * a.val)
    {ξ : H} (hξ : ξ ∈ centralVectorSpace N J) : T ξ ∈ centralVectorSpace N J := by
…

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

theorem OAI.KadisonKastler.scalar_relative_commutant_of_centralVectorSpace line 67

Source documentation

A separating central vector spanning all central vectors forces irreducibility.

theorem scalar_relative_commutant_of_centralVectorSpace
    (J : H ≃ₗᵢ⋆[ℂ] H)
    (hright : ∀ a : Algebra N, conjugationOperator J (star a).val ∈ M.commutant)
    (ξ : H) (hξ : ξ ∈ centralVectorSpace N J)
    (hline : centralVectorSpace N J ≤ Submodule.span ℂ {ξ})
    (hsep : Function.Injective (fun a : Algebra M => a.val ξ))
    (T : H →L[ℂ] H) (hT : T ∈ M)
    (hcomm : ∀ a : Algebra N, a.val * T = T * a.val) :
    ∃ z : ℂ, T = z • (1 : H →L[ℂ] H) := by
…

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

theorem OAI.KadisonKastler.centralVectorSpace_conjugate line 85