TracialWordActions.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The represented left head action follows from the ordinary product formula in the reduced-word model. It is not extra covariance data.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseRepresentation_baseVector line 30

def OAI.KadisonSimilarity.TracialCornerGeometry.tracialWordHeadAction line 36

Source documentation

Left multiplication acts only on the first other-factor endpoint.

def tracialWordHeadAction (n : ℕ) (a : D) :
    MultiplicityWordSpace (WordMultiplicity (G.baseVector A 1)) (G.baseSpace D)
      (centeredSubspace (G.baseVector D 1)) n →L[ℂ]
    MultiplicityWordSpace (WordMultiplicity (G.baseVector A 1)) (G.baseSpace D)
      (centeredSubspace (G.baseVector D 1)) n :=
…

Mentions: OAI.KadisonSimilarity.MultiplicityWordSpace, OAI.KadisonSimilarity.WordMultiplicity, OAI.KadisonSimilarity.centeredSubspace

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialWordHeadAction_tensor line 43
theorem OAI.KadisonSimilarity.TracialWordFormula.left_head line 67
Source documentation
The actual represented left action intertwines with the completed head action, by equality on the dense bounded word vectors.
```
theorem left_head (hU : TracialWordFormula G A D U) (hτ : G.trace 1 = 1)
    (n : ℕ) (x : D) :
    (G.left (x : P)).comp (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp (G.tracialWordHeadAction A D n x) := by
…
```
Mentions: OAI.KadisonSimilarity.TracialWordFormula