EmbeddedWordActions.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Actual embedded matrix actions supply the action record used by the invariant-word classification. Adjoint covariance follows from the represented star and inverse laws, and the source/test formulas from tracial word covariance.

theorem OAI.KadisonSimilarity.hilbertTensorLift_adjoint line 19
theorem OAI.KadisonSimilarity.endpointHeadAction_adjoint line 28
theorem OAI.KadisonSimilarity.tracialUnitaryConjugation_mul_inv line 58
Source documentation
Inverse matrix conjugations cancel on the entire tracial Hilbert space, by their algebraic action on its dense represented vectors.
```
theorem tracialUnitaryConjugation_mul_inv (u : Matrix.unitaryGroup α ℂ) (x : E) :
    tracialUnitaryConjugation τ V L ι hinner htrace hdense u
      (tracialUnitaryConjugation τ V L ι hinner htrace hdense u⁻¹ x) = x := by
…
```
Mentions: OAI.KadisonSimilarity.tracialUnitaryConjugation
theorem OAI.KadisonSimilarity.centeredUnitaryConjugation_mul_inv line 79

theorem OAI.KadisonSimilarity.tracialMatrixWordAction_mul_inv line 87

Source documentation

The inverse word action is obtained by inverting the actual matrix unitary.

theorem tracialMatrixWordAction_mul_inv (u : Matrix.unitaryGroup α ℂ) (n : ℕ) :
    (tracialMatrixWordAction τ V L ι hinner hleft htrace hdense u n).toContinuousLinearMap.comp
      (tracialMatrixWordAction τ V L ι hinner hleft htrace hdense u⁻¹ n).toContinuousLinearMap =
        ContinuousLinearMap.id ℂ (EndpointTensor E (centeredSubspace (V 1)) n) := by
…

Mentions: OAI.KadisonSimilarity.tracialMatrixWordAction, OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.centeredSubspace

theorem OAI.KadisonSimilarity.tracialMatrixWordAction_adjoint line 100

Source documentation

The adjoint action on completed words is the inverse matrix action.

theorem tracialMatrixWordAction_adjoint (u : Matrix.unitaryGroup α ℂ) (n : ℕ) :
    (tracialMatrixWordAction τ V L ι hinner hleft htrace hdense u n).toContinuousLinearMap.adjoint =
      (tracialMatrixWordAction τ V L ι hinner hleft htrace hdense u⁻¹ n).toContinuousLinearMap := by
…

Mentions: OAI.KadisonSimilarity.tracialMatrixWordAction

def OAI.KadisonSimilarity.embeddedWordMatrixActions line 150
Source documentation
The action record for the invariant classification, obtained from actual representations and the two raw word inclusion formulas alone.
```
def embeddedWordMatrixActions :
    WordLevelMatrixActions (tracialMatrixTowerOfEmbeddings τ V L hinner hleft M htrace S hsize) U where
…
```
Mentions: OAI.KadisonSimilarity.WordLevelMatrixActions, OAI.KadisonSimilarity.tracialMatrixTowerOfEmbeddings