JointFiberCommutants.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Central elements of a joint fiber representation

For commuting sources B,C, a central element of the represented bicommutant of B commutes with the full joint bicommutant. The proof uses norm generation of the joint source, with no normality assertion for a pointwise fiber representation.

theorem OAI.KadisonSimilarity.joint_source_representation_mem line 24

Source documentation

A representation of the joint norm closure lands in any closed star algebra containing the represented copies of both sources.

theorem joint_source_representation_mem
    (B C : StarSubalgebra ℂ A)
    (σ : jointCStarSource B C →⋆ₐ[ℂ] (K →L[ℂ] K))
    (N : StarSubalgebra ℂ (K →L[ℂ] K)) (hN : IsClosed (N : Set (K →L[ℂ] K)))
    (hB : ∀ b : B, σ (StarSubalgebra.inclusion (le_jointCStarSource_left B C) b) ∈ N)
    (hC : ∀ c : C, σ (StarSubalgebra.inclusion (le_jointCStarSource_right B C) c) ∈ N)
    (s : jointCStarSource B C) : σ s ∈ N := by
…

Mentions: OAI.KadisonSimilarity.jointCStarSource, OAI.KadisonSimilarity.le_jointCStarSource_left, OAI.KadisonSimilarity.le_jointCStarSource_right

theorem OAI.KadisonSimilarity.joint_second_mem_first_commutant line 52

Source documentation

The represented second source commutes with the bicommutant of the first source, since the two original sources commute.

theorem joint_second_mem_first_commutant
    (B C : StarSubalgebra ℂ A)
    [IsClosed (B : Set A)] [IsClosed (C : Set A)]
    (hBC : ∀ b : B, ∀ c : C, (b : A) * (c : A) = (c : A) * (b : A))
    (σ : jointCStarSource B C →⋆ₐ[ℂ] (K →L[ℂ] K)) (c : C) :
    σ (StarSubalgebra.inclusion (le_jointCStarSource_right B C) c) ∈
      (representationVonNeumannAlgebra
        (σ.comp (StarSubalgebra.inclusion (le_jointCStarSource_left B C)))).commutant := by
…

Mentions: OAI.KadisonSimilarity.jointCStarSource, OAI.KadisonSimilarity.le_jointCStarSource_right, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.le_jointCStarSource_left

theorem OAI.KadisonSimilarity.joint_center_mem_joint_commutant line 73

Source documentation

Centrality in the first represented bicommutant gives commutation with the entire joint representation.

theorem joint_center_mem_joint_commutant
    (B C : StarSubalgebra ℂ A)
    [IsClosed (B : Set A)] [IsClosed (C : Set A)]
    (hBC : ∀ b : B, ∀ c : C, (b : A) * (c : A) = (c : A) * (b : A))
    (σ : jointCStarSource B C →⋆ₐ[ℂ] (K →L[ℂ] K)) (T : K →L[ℂ] K)
    (hT : T ∈ vonNeumannCenter (representationVonNeumannAlgebra
      (σ.comp (StarSubalgebra.inclusion (le_jointCStarSource_left B C))))) :
    T ∈ (representationVonNeumannAlgebra σ).commutant := by
…

Mentions: OAI.KadisonSimilarity.jointCStarSource, OAI.KadisonSimilarity.vonNeumannCenter, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.le_jointCStarSource_left

theorem OAI.KadisonSimilarity.joint_center_commutes_joint_bicommutant line 116

Source documentation

In particular a central first-source operator commutes with every operator in the represented joint bicommutant, including rank-one tests.

theorem joint_center_commutes_joint_bicommutant
    (B C : StarSubalgebra ℂ A)
    [IsClosed (B : Set A)] [IsClosed (C : Set A)]
    (hBC : ∀ b : B, ∀ c : C, (b : A) * (c : A) = (c : A) * (b : A))
    (σ : jointCStarSource B C →⋆ₐ[ℂ] (K →L[ℂ] K)) (T Q : K →L[ℂ] K)
    (hT : T ∈ vonNeumannCenter (representationVonNeumannAlgebra
      (σ.comp (StarSubalgebra.inclusion (le_jointCStarSource_left B C)))))
    (hQ : Q ∈ representationVonNeumannAlgebra σ) : T * Q = Q * T :=
…

Mentions: OAI.KadisonSimilarity.jointCStarSource, OAI.KadisonSimilarity.vonNeumannCenter, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.le_jointCStarSource_left