OAI/Analysis/KadisonSimilarity/Representation/CanonicalGeneratedModel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual generated algebra for two embedded tracial factors. Its containment, generation, freeness and matrix tower follow from the concrete embeddings; there is no separately chosen generated-algebra model.

  1. def OAI.KadisonSimilarity.canonicalGeneratedAlgebra line 20
  2. instance OAI.KadisonSimilarity.canonicalGeneratedAlgebra_isClosed line 23
  3. theorem OAI.KadisonSimilarity.canonicalGenerated_first_mem line 28
  4. theorem OAI.KadisonSimilarity.canonicalGenerated_second_mem line 32
  5. def OAI.KadisonSimilarity.canonicalGeneratedFirst line 36
  6. def OAI.KadisonSimilarity.canonicalGeneratedSecond line 40
  7. def OAI.KadisonSimilarity.canonicalGeneratedTrace line 44
  8. def OAI.KadisonSimilarity.canonicalGeneratedGeometry line 47
  9. theorem OAI.KadisonSimilarity.canonicalGenerated_generation line 53

    Source documentation

    Generation is a property of the constructed algebra, with the same factor ranges used by the commutator recovery theorem.

    theorem canonicalGenerated_generation :
    (canonicalGeneratedGeometry τ htr φ ψ).FactorsTraciallyGenerate
      (canonicalGeneratedFirst τ htr φ ψ).range
      (canonicalGeneratedSecond τ htr φ ψ).range :=
…

    Mentions: OAI.KadisonSimilarity.canonicalGeneratedGeometry, OAI.KadisonSimilarity.canonicalGeneratedFirst, OAI.KadisonSimilarity.canonicalGeneratedSecond

  10. theorem OAI.KadisonSimilarity.canonicalGenerated_freeness line 62
  11. theorem OAI.KadisonSimilarity.canonicalGenerated_faithful line 69
  12. def OAI.KadisonSimilarity.canonicalGeneratedMatrices line 80

    Source documentation

    The source matrix tower is transported into this exact generated model.

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

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

  13. def OAI.KadisonSimilarity.canonicalGeneratedRealSequence line 85