TypeICyclicGeneration.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Transporting weak generation through the minimal cyclic representation

theorem OAI.KadisonKastler.typeICyclic_inverse_mem_of_generated_unitBall line 21

Source documentation

The inverse minimal cyclic representation preserves the weak closure needed for generation. The proof uses bounded approximation and weak compactness in the original representation.

theorem typeICyclic_inverse_mem_of_generated_unitBall (hM : ScalarCenter M)
    (p : AlgebraProjection M) (hp : IsMinimalProjectionIn M p)
    (ξ : H) (hξ : ξ ≠ 0) (hpξ : p.val.val ξ = ξ)
    (Q : VonNeumannAlgebra H) (hQM : Q ≤ M)
    (A : StarSubalgebra ℂ (typeICyclicSpace M ξ →L[ℂ] typeICyclicSpace M ξ))
    (hA : ∀ T ∈ A, ((typeICyclicEquiv hM p hp ξ hξ hpξ).symm T).val ∈ Q)
    (T : typeICyclicSpace M ξ →L[ℂ] typeICyclicSpace M ξ)
    (hT : T ∈ generatedVonNeumannAlgebra A) (hnT : ‖T‖ ≤ 1) :
    ((typeICyclicEquiv hM p hp ξ hξ hpξ).symm T).val ∈ Q := by
…

Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.IsMinimalProjectionIn, OAI.KadisonKastler.typeICyclicSpace, OAI.KadisonKastler.typeICyclicEquiv, OAI.KadisonKastler.generatedVonNeumannAlgebra

theorem OAI.KadisonKastler.typeICyclic_inverse_mem_of_generated line 76

Source documentation

Weak generation transports to the original type I representation.

theorem typeICyclic_inverse_mem_of_generated (hM : ScalarCenter M)
    (p : AlgebraProjection M) (hp : IsMinimalProjectionIn M p)
    (ξ : H) (hξ : ξ ≠ 0) (hpξ : p.val.val ξ = ξ)
    (Q : VonNeumannAlgebra H) (hQM : Q ≤ M)
    (A : StarSubalgebra ℂ (typeICyclicSpace M ξ →L[ℂ] typeICyclicSpace M ξ))
    (hA : ∀ T ∈ A, ((typeICyclicEquiv hM p hp ξ hξ hpξ).symm T).val ∈ Q)
    (T : typeICyclicSpace M ξ →L[ℂ] typeICyclicSpace M ξ)
    (hT : T ∈ generatedVonNeumannAlgebra A) :
    ((typeICyclicEquiv hM p hp ξ hξ hpξ).symm T).val ∈ Q := by
…

def OAI.KadisonKastler.typeICyclicGroup line 113

Source documentation

Transfer a generating unitary group from the minimal cyclic space.

def typeICyclicGroup {G : Type*} [Group G] (hM : ScalarCenter M)
    (p : AlgebraProjection M) (hp : IsMinimalProjectionIn M p)
    (ξ : H) (hξ : ξ ≠ 0) (hpξ : p.val.val ξ = ξ)
    (U : G →* unitary (typeICyclicSpace M ξ →L[ℂ] typeICyclicSpace M ξ)) :
    G →* unitary (Algebra M) where
…

Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.IsMinimalProjectionIn, OAI.KadisonKastler.typeICyclicSpace, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.typeICyclicGroup_generates line 123