RepresentationCenterTransport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Scalar centers and exact representation conjugacy

An algebra equivalence between the ambient operator algebras transports the represented bicommutants and their centers. In particular, identifying two equal projection ranges does not change the factor-fiber criterion.

theorem OAI.KadisonSimilarity.representation_bicommutant_map_mem line 20
theorem OAI.KadisonSimilarity.representation_bicommutant_map_mem_iff line 39
theorem OAI.KadisonSimilarity.representation_commutant_map_mem line 51
theorem OAI.KadisonSimilarity.representation_center_map_mem line 63

theorem OAI.KadisonSimilarity.scalar_center_of_representation_equiv line 74

Source documentation

The scalar-center condition used for factor fibers is unchanged by an exact star-algebra conjugacy of the representations.

theorem scalar_center_of_representation_equiv
    (θ : (H →L[ℂ] H) ≃⋆ₐ[ℂ] (K →L[ℂ] K))
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (hθ : ∀ a, θ (σ a) = ρ a)
    (hρ : ∀ a : (representationVonNeumannAlgebra ρ).toStarSubalgebra,
      (∀ b, a * b = b * a) → ∃ c : ℂ, a = algebraMap ℂ _ c) :
    ∀ a : (representationVonNeumannAlgebra σ).toStarSubalgebra,
      (∀ b, a * b = b * a) → ∃ c : ℂ, a = algebraMap ℂ _ c := by
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra