CyclicStandardEmbedding.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Equality of vector functionals constructs a cyclic intertwining isometry. Countable cyclic assembly then gives the standard embedding required by the finite-factor application.

theorem OAI.KadisonSimilarity.cyclic_isometry_of_orbit_norms line 20

Source documentation

The isometry on a dense cyclic orbit extends to the complete Hilbert space and retains its intertwining identity.

theorem cyclic_isometry_of_orbit_norms
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (ξ : H) (η : K) (hξ : DenseRange (fun a : A => σ a ξ))
    (hn : ∀ a, ‖σ a ξ‖ = ‖ρ a η‖) :
    ∃ J : H →ₗᵢ[ℂ] K, ∀ a,
      J.toContinuousLinearMap.comp (σ a) = (ρ a).comp J.toContinuousLinearMap := by
…

theorem OAI.KadisonSimilarity.orbit_norms_of_vector_functionals line 55

Source documentation

Equality of vector functionals supplies the norm identity on each cyclic orbit by testing the positive square a* a.

theorem orbit_norms_of_vector_functionals
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (ξ : H) (η : K)
    (h : ∀ a, inner ℂ ξ (σ a ξ) = inner ℂ η (ρ a η)) (a : A) :
    ‖σ a ξ‖ = ‖ρ a η‖ := by
…

theorem OAI.KadisonSimilarity.normal_standard_embedding_of_vector_realization line 76

Source documentation

Once the normal vector-functional realization is constructed, the standard embedding follows without a separate decomposition assumption.

theorem normal_standard_embedding_of_vector_realization
    [TopologicalSpace.SeparableSpace H]
    (τ : A →ₚ[ℂ] ℂ) (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hvector : ∀ ξ : H, ∃ η : τ.GNS, ∀ a,
      inner ℂ ξ (σ a ξ) = inner ℂ η (τ.gnsStarAlgHom a η)) :
    HiaiNormalStandardEmbeddingInput τ σ := by
…

Mentions: OAI.KadisonSimilarity.HiaiNormalStandardEmbeddingInput