ReducedWordAutomorphisms.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Dense reduced words provide the tracial generation needed to turn published factor embeddings into actual free-product automorphisms.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.reducedWord_mem_factorAlgebra line 18
Source documentation
Every bounded reduced word belongs to the algebra generated by the factors.
```
theorem reducedWord_mem_factorAlgebra (n : ℕ) (d : D) (b : A)
    (a : Fin n → A) (c : Fin n → D) :
    (d : P) * alternatingProduct (fun i => (a i : P)) (fun i => (c i : P)) * (b : P) ∈
      factorAlgebra A D := by
…
```
Mentions: OAI.KadisonSimilarity.alternatingProduct, OAI.KadisonSimilarity.TracialCornerGeometry.factorAlgebra
theorem OAI.KadisonSimilarity.TracialCornerGeometry.factorsTraciallyGenerate_of_reducedWordGenerated line 45
Source documentation
The ordinary reduced-word density supplies the tracial algebraic generation; no separate factor-generation hypothesis is required for automorphism extension.
```
theorem factorsTraciallyGenerate_of_reducedWordGenerated
    (hgen : ReducedWordGenerated G A D) : G.FactorsTraciallyGenerate A D := by
…
```
Mentions: OAI.KadisonSimilarity.ReducedWordGenerated

def OAI.KadisonSimilarity.TracialCornerGeometry.matrixAutomorphismOfReducedWords line 67

Source documentation

Existence of the ambient matrix-conjugation automorphism follows from the published two-factor extension and the actual reduced-word density.

def matrixAutomorphismOfReducedWords
    (hgen : ReducedWordGenerated G A D) (hfaithful : Function.Injective G.vector)
    {α : Type*} [Fintype α] [DecidableEq α]
    (ι : Matrix α α ℂ →⋆ₐ[ℂ] D) (hext : G.MatrixConjugationExtensionInput D ι A)
    (u : Matrix.unitaryGroup α ℂ) : P ≃⋆ₐ[ℂ] P :=
…

Mentions: OAI.KadisonSimilarity.ReducedWordGenerated