StandardEmbeddingAssembly.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Assemble embeddings of the cyclic summands into the countable standard representation. The countability and Hilbert-sum construction are proved; only the embeddings of the individual cyclic representations are parameters.

theorem OAI.KadisonSimilarity.CyclicDecompositionData.isHilbertSum line 22
Source documentation
The actual total orthogonal cyclic family is a Hilbert direct sum.
```
theorem isHilbertSum : IsHilbertSum ℂ D.Space D.summands.inclusion := by
…
```
def OAI.KadisonSimilarity.countableSingleIsometry line 39
theorem OAI.KadisonSimilarity.countableAmplify_single line 46

theorem OAI.KadisonSimilarity.countable_embedding_of_cyclic_embeddings line 54

Source documentation

Countably many cyclic intertwiners combine into one isometric intertwiner on the original separable representation.

theorem countable_embedding_of_cyclic_embeddings
    [TopologicalSpace.SeparableSpace H]
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (D : CyclicDecompositionData σ.range)
    (J : ∀ i, D.Space i →ₗᵢ[ℂ] K)
    (hJ : ∀ i a, (J i).toContinuousLinearMap.comp (D.representation σ i a) =
      (ρ a).comp (J i).toContinuousLinearMap) :
    ∃ I : H →ₗᵢ[ℂ] CountableCopies K,
      ∀ a, I.toContinuousLinearMap.comp (σ a) =
        (countableAmplify (ρ a)).comp I.toContinuousLinearMap := by
…

Mentions: OAI.KadisonSimilarity.CyclicDecompositionData, OAI.KadisonSimilarity.CountableCopies, OAI.KadisonSimilarity.countableAmplify