OAI/Analysis/KadisonSimilarity/Representation/GeneratedEmbeddings.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual copies of the two factors inside their generated algebra. The range identifications align the GNS recovery operator with the factor generation, freeness, and matrix tower used by the local theorem.

  1. theorem OAI.KadisonSimilarity.range_codRestrict_eq_comap line 20
  2. theorem OAI.KadisonSimilarity.codRestrict_range_isClosed line 30
  3. theorem OAI.KadisonSimilarity.generatedEmbeddings_factorsTraciallyGenerate line 36
  4. theorem OAI.KadisonSimilarity.generatedEmbeddings_scalarFree line 50
  5. theorem OAI.KadisonSimilarity.generatedEmbedding_preserves_trace line 68
  6. def OAI.KadisonSimilarity.generatedEmbeddingMatrices line 75

    Source documentation

    The matrix tower lives on the same native GNS space as the recovered operator, and on the exact range of the embedded free factor.

    def generatedEmbeddingMatrices
    (M : NestedTracialMatrices (A := I) τR.toLinearMap (gnsTracialVector τR)) :=
…

    Mentions: OAI.KadisonSimilarity.NestedTracialMatrices, OAI.KadisonSimilarity.gnsTracialVector

  7. def OAI.KadisonSimilarity.generatedEmbeddingRealSequence line 82