CyclicGraphEmbedding.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A closable cyclic orbit map gives an isometric subrepresentation. The closed graph is itself a cyclic reducing representation, and its two coordinate maps yield the embedding by polar decomposition.

def OAI.KadisonSimilarity.pairRepresentation line 18

Source documentation

Direct sum of two star representations, with the Hilbert product norm.

def pairRepresentation (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) :
    A →⋆ₐ[ℂ] (RectangularSum H K →L[ℂ] RectangularSum H K) where
…

Mentions: OAI.KadisonSimilarity.RectangularSum

theorem OAI.KadisonSimilarity.pairRepresentation_fst line 38
theorem OAI.KadisonSimilarity.pairRepresentation_snd line 44

def OAI.KadisonSimilarity.cyclicGraph line 50

Source documentation

The closed cyclic graph of the orbit map σ(a)Ω ↦ ρ(a)ξ.

def cyclicGraph (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (Ω : H) (ξ : K) :=
…

theorem OAI.KadisonSimilarity.cyclic_embedding_of_closable_graph line 56

Source documentation

Trivial vertical part of the closed cyclic graph is exactly the closability condition needed by the polar construction.

theorem cyclic_embedding_of_closable_graph
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (Ω : H) (ξ : K) (hξ : DenseRange (fun a : A => ρ a ξ))
    (hclose : ∀ x : cyclicGraph σ ρ Ω ξ,
      (x : RectangularSum H K).fst = 0 → (x : RectangularSum H K).snd = 0) :
    ∃ J : K →ₗᵢ[ℂ] H, ∀ a,
      J.toContinuousLinearMap.comp (ρ a) = (σ a).comp J.toContinuousLinearMap := by
…

Mentions: OAI.KadisonSimilarity.cyclicGraph, OAI.KadisonSimilarity.RectangularSum