OAI/Analysis/KadisonSimilarity/FreeProduct/FreeHeadCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Surjectivity and left-action covariance of the first-factor tensor map.

  1. theorem OAI.KadisonSimilarity.centered_word_mem_freeHead_range line 19
  2. theorem OAI.KadisonSimilarity.freeHeadIsometry_surjective line 37
  3. def OAI.KadisonSimilarity.freeHeadEquiv line 52
  4. theorem OAI.KadisonSimilarity.freeHeadIsometry_covariance line 59
  5. def OAI.KadisonSimilarity.freeTracialHeadCoordinates line 88

    Source documentation

    The raw head coordinates of the reduced product, with their actual left multiplication action.

    def freeTracialHeadCoordinates (hτ : G.trace 1 = 1) (hf : ScalarFree G.trace A D)
    (hgen : ReducedWordGenerated G A D) :
    TracialHeadCoordinates (G.baseGeometry D) G D.subtype (centeredWordSpace G A D true) where
…

    Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.ReducedWordGenerated, OAI.KadisonSimilarity.TracialHeadCoordinates, OAI.KadisonSimilarity.centeredWordSpace

  6. theorem OAI.KadisonSimilarity.freeTracialHeadCoordinates_vacuum line 104