OAI/Analysis/KadisonSimilarity/Tracial/OppositeTracialGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Right multiplication is the left representation of the opposite algebra. This transfers the proved bounded-ball normality criterion to its actual range.

  1. def OAI.KadisonSimilarity.TracialCornerGeometry.rightRepresentation line 17
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightRepresentation_apply line 47
  3. def OAI.KadisonSimilarity.TracialCornerGeometry.oppositeGeometry line 50
  4. theorem OAI.KadisonSimilarity.TracialCornerGeometry.oppositeGeometry_vector line 74
  5. theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightRepresentation_normal_range line 78

    Source documentation

    The right range is a von Neumann algebra when the original left range is normal.

    theorem rightRepresentation_normal_range (h1 : G.trace 1 = 1)
    (hf : Function.Injective G.vector) (M : VonNeumannAlgebra H)
    (hrange : G.left.range = M.toStarSubalgebra) :
    G.rightRepresentation.range =
      (representationVonNeumannAlgebra G.rightRepresentation).toStarSubalgebra := by
…

    Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra