TracialAutomorphismWords.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The matrix-unitary word formula is derived from the algebraic product formula and the actual implementation of a trace-preserving automorphism.

def OAI.KadisonSimilarity.TracialCornerGeometry.baseMatrixWordAction line 28
Source documentation
The genuine endpoint action on the tracial Hilbert space of the other factor.
```
def baseMatrixWordAction (n : ℕ) :
    EndpointTensor (G.baseSpace D) (centeredSubspace (G.baseVector D 1)) n →ₗᵢ[ℂ]
      EndpointTensor (G.baseSpace D) (centeredSubspace (G.baseVector D 1)) n :=
…
```
Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.centeredSubspace
theorem OAI.KadisonSimilarity.TracialCornerGeometry.centeredMatrixConjugation_letter line 36

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseMatrixWordAction_endpoint line 51

Source documentation

The completed endpoint action sends every bounded tensor word to the word whose other-factor letters have been conjugated.

theorem baseMatrixWordAction_endpoint (n : ℕ) (d : D) (c : Fin n → D)
    (hc : ∀ i, G.trace (c i : P) = 0) :
    G.baseMatrixWordAction D ι u n (tracialEndpointWord G D n d c hc) =
      tracialEndpointWord G D n (matrixConjugateLetter D ι u d)
        (fun i => matrixConjugateLetter D ι u (c i))
        (fun i => (G.trace_matrixConjugateLetter D ι u (c i)).trans (hc i)) := by
…

Mentions: OAI.KadisonSimilarity.tracialEndpointWord, OAI.KadisonSimilarity.TracialCornerGeometry.matrixConjugateLetter

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseMatrixWordAction_tensor line 80

Source documentation

The multiplicity letters are fixed, and the endpoint letters are conjugated by the represented matrix unitary.

theorem baseMatrixWordAction_tensor (n : ℕ) (d : D) (b : A)
    (a : Fin n → A) (c : Fin n → D)
    (ha : ∀ i, G.trace (a i : P) = 0) (hc : ∀ i, G.trace (c i : P) = 0) :
    hilbertTensorLift (G.baseMatrixWordAction D ι u n).toContinuousLinearMap
      (tracialWordTensor G A D n d b a c ha hc) =
    tracialWordTensor G A D n (matrixConjugateLetter D ι u d) b a
      (fun i => matrixConjugateLetter D ι u (c i)) ha
      (fun i => (G.trace_matrixConjugateLetter D ι u (c i)).trans (hc i)) := by
…

Mentions: OAI.KadisonSimilarity.hilbertTensorLift, OAI.KadisonSimilarity.tracialWordTensor, OAI.KadisonSimilarity.TracialCornerGeometry.matrixConjugateLetter

theorem OAI.KadisonSimilarity.automorphism_alternatingProduct line 94
Source documentation
A star-algebra automorphism transports a finite alternating product letterwise.
```
theorem automorphism_alternatingProduct (θ : P ≃⋆ₐ[ℂ] P) {n : ℕ}
    (a c : Fin n → P) :
    θ (alternatingProduct a c) =
      alternatingProduct (fun i => θ (a i)) (fun i => θ (c i)) := by
…
```
Mentions: OAI.KadisonSimilarity.alternatingProduct

theorem OAI.KadisonSimilarity.TracialWordFormula.automorphism_word line 128

Source documentation

On bounded tracial words, automorphism covariance is a consequence of multiplicativity, factor fixation, and the reduced-word product formula.

theorem automorphism_word (hU : TracialWordFormula G A D U)
    (n : ℕ) (d : D) (b : A) (a : Fin n → A) (c : Fin n → D)
    (ha : ∀ i, G.trace (a i : P) = 0) (hc : ∀ i, G.trace (c i : P) = 0) :
    G.automorphismUnitary θ hθ
      (U.inclusion n (tracialWordTensor G A D n d b a c ha hc)) =
    U.inclusion n (hilbertTensorLift (G.baseMatrixWordAction D ι u n).toContinuousLinearMap
      (tracialWordTensor G A D n d b a c ha hc)) := by
…

Mentions: OAI.KadisonSimilarity.TracialWordFormula, OAI.KadisonSimilarity.tracialWordTensor, OAI.KadisonSimilarity.hilbertTensorLift

theorem OAI.KadisonSimilarity.TracialWordFormula.intertwining_of_bounded_words line 141

Source documentation

A bounded word intertwining identity extends from the actual algebra letters to the entire completed word level.

theorem intertwining_of_bounded_words (hτ : G.trace 1 = 1) (n : ℕ)
    (W : H →L[ℂ] H)
    (T : 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)
    (hword : ∀ (d : D) (b : A) (a : Fin n → A) (c : Fin n → D)
      (ha : ∀ i, G.trace (a i : P) = 0) (hc : ∀ i, G.trace (c i : P) = 0),
      W (U.inclusion n (tracialWordTensor G A D n d b a c ha hc)) =
        U.inclusion n (T (tracialWordTensor G A D n d b a c ha hc))) :
    W.comp (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp T := by
…

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

theorem OAI.KadisonSimilarity.TracialWordFormula.automorphism_level line 163

Source documentation

Equality on the bounded algebra words extends the automorphism action to its genuine completed-word intertwining identity.

theorem automorphism_level (hU : TracialWordFormula G A D U)
    (hτ : G.trace 1 = 1) (n : ℕ) :
    (G.automorphismUnitary θ hθ).toContinuousLinearEquiv.toContinuousLinearMap.comp
        (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp
        (hilbertTensorLift (G.baseMatrixWordAction D ι u n).toContinuousLinearMap) := by
…

Mentions: OAI.KadisonSimilarity.TracialWordFormula, OAI.KadisonSimilarity.hilbertTensorLift

theorem OAI.KadisonSimilarity.TracialWordFormula.matrix_extension_level line 177

Source documentation

The matrix action needed for finite-stage word classification is obtained from the published factor extension, rather than supplied as tensor covariance.

theorem matrix_extension_level
    (hgen : G.FactorsTraciallyGenerate A D) (hfaithful : Function.Injective G.vector)
    (hext : G.MatrixConjugationExtensionInput D ι A)
    (hU : TracialWordFormula G A D U) (hτ : G.trace 1 = 1) (n : ℕ) :
    (G.matrixExtensionUnitaryRepresentation A D ι hgen hfaithful hext u : H →L[ℂ] H).comp
        (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp
        (hilbertTensorLift (G.baseMatrixWordAction D ι u n).toContinuousLinearMap) := by
…

Mentions: OAI.KadisonSimilarity.TracialWordFormula, OAI.KadisonSimilarity.hilbertTensorLift