CommonFiberRepresentations.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Genuine representations of a norm-separable algebra on the fibers of the common spectral model. The old unit supplies the projection onto the fibers of the original Hilbert space.

theorem OAI.KadisonSimilarity.exists_conull_common_representations line 27

Source documentation

Every commuting norm-separable algebra has genuine unital fiber representations after adjoining the ambient identity.

theorem exists_conull_common_representations
    (σ : B →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hσ : ∀ b a, σ b * π a = π a * σ b) :
    ∃ s : Set (WeakDual.characterSpace ℂ A), MeasurableSet s ∧
      (cyclicCommonBaseMeasure π D) sᶜ = 0 ∧
      ∃ ρ : ∀ _x : s, Unitization ℂ B →⋆ₐ[ℂ]
          (ScalarHilbertCoordinates D.generators →L[ℂ] ScalarHilbertCoordinates D.generators),
        ∀ (b : B) (f : CommonCyclicHilbert π D),
          ∀ᵐ (x : s) ∂Measure.comap ((↑) : s → WeakDual.characterSpace ℂ A)
              (cyclicCommonBaseMeasure π D),
            isometricExtension (cyclicCommonEmbedding π D) (σ b) f x =
              ρ x (Unitization.inr b) (f x) := by
…

Mentions: OAI.KadisonSimilarity.cyclicCommonBaseMeasure, OAI.KadisonSimilarity.ScalarHilbertCoordinates, OAI.KadisonSimilarity.CommonCyclicHilbert, OAI.KadisonSimilarity.isometricExtension, OAI.KadisonSimilarity.cyclicCommonEmbedding

theorem OAI.KadisonSimilarity.exists_common_nonunital_representations line 53

Source documentation

Extending the conull representation by zero gives genuine nonunital representations at every point, retaining the action of the original algebra.

theorem exists_common_nonunital_representations
    (σ : B →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hσ : ∀ b a, σ b * π a = π a * σ b) :
    ∃ ρ : WeakDual.characterSpace ℂ A → B →⋆ₙₐ[ℂ]
        (ScalarHilbertCoordinates D.generators →L[ℂ] ScalarHilbertCoordinates D.generators),
      ∀ (b : B) (f : CommonCyclicHilbert π D),
        ∀ᵐ x ∂cyclicCommonBaseMeasure π D,
          isometricExtension (cyclicCommonEmbedding π D) (σ b) f x = ρ x b (f x) := by
…

Mentions: OAI.KadisonSimilarity.ScalarHilbertCoordinates, OAI.KadisonSimilarity.CommonCyclicHilbert, OAI.KadisonSimilarity.cyclicCommonBaseMeasure, OAI.KadisonSimilarity.isometricExtension, OAI.KadisonSimilarity.cyclicCommonEmbedding