DihedralWordAlgebra.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The ordinary dihedral word span is a unital star subalgebra. This reduces its L²-density to density of the algebra generated by the two symmetries, without assuming a normal-form density statement.

theorem OAI.KadisonSimilarity.DihedralWordAlgebra.reflection_zpow line 17
Source documentation
Moving a reflection through any integer rotation power.
```
theorem reflection_zpow (d w : G) (hc : d * w = w⁻¹ * d) (l : ℤ) :
    d * w ^ l = w ^ (-l) * d := by
…
```
theorem OAI.KadisonSimilarity.DihedralWordAlgebra.reflection_rotation line 23
Source documentation
The rotation exponent changes sign when its left factor is a reflection.
```
theorem reflection_rotation (d w : G) (hc : d * w = w⁻¹ * d) (l m : ℤ) :
    (w ^ l * d) * w ^ m = w ^ (l - m) * d := by
…
```

theorem OAI.KadisonSimilarity.DihedralWordAlgebra.reflection_reflection line 29

Source documentation

The product of two reflection-coset words is a rotation.

theorem reflection_reflection (d w : G) (hd : d * d = 1)
    (hc : d * w = w⁻¹ * d) (l m : ℤ) :
    (w ^ l * d) * (w ^ m * d) = w ^ (l - m) := by
…

def OAI.KadisonSimilarity.DihedralWordAlgebra.wordSet line 39
Source documentation
Rotation words and reflection-coset words, as elements of the algebra.
```
def wordSet (d w : Pˣ) : Set P :=
…
```
theorem OAI.KadisonSimilarity.DihedralWordAlgebra.wordSet_mul line 44
Source documentation
Normal forms are closed under multiplication.
```
theorem wordSet_mul (d w : Pˣ) (hd : d * d = 1) (hc : d * w = w⁻¹ * d)
    {a b : P} (ha : a ∈ wordSet d w) (hb : b ∈ wordSet d w) : a * b ∈ wordSet d w := by
…
```
Mentions: OAI.KadisonSimilarity.DihedralWordAlgebra.wordSet
theorem OAI.KadisonSimilarity.DihedralWordAlgebra.wordSet_star line 65
Source documentation
Taking adjoints preserves the two normal forms.
```
theorem wordSet_star (d w : Pˣ) (hc : d * w = w⁻¹ * d)
    (hdstar : star d = d) (hwstar : star w = w⁻¹)
    {a : P} (ha : a ∈ wordSet d w) : star a ∈ wordSet d w := by
…
```
Mentions: OAI.KadisonSimilarity.DihedralWordAlgebra.wordSet

theorem OAI.KadisonSimilarity.DihedralWordAlgebra.span_mul line 79

Source documentation

Bilinearity extends multiplication closure to the full linear span.

theorem span_mul (d w : Pˣ) (hd : d * d = 1) (hc : d * w = w⁻¹ * d)
    {a b : P} (ha : a ∈ Submodule.span ℂ (wordSet d w))
    (hb : b ∈ Submodule.span ℂ (wordSet d w)) :
    a * b ∈ Submodule.span ℂ (wordSet d w) := by
…

Mentions: OAI.KadisonSimilarity.DihedralWordAlgebra.wordSet

theorem OAI.KadisonSimilarity.DihedralWordAlgebra.span_star line 107

Source documentation

Conjugate linearity extends adjoint closure to the word span.

theorem span_star (d w : Pˣ) (hc : d * w = w⁻¹ * d)
    (hdstar : star d = d) (hwstar : star w = w⁻¹)
    {a : P} (ha : a ∈ Submodule.span ℂ (wordSet d w)) :
    star a ∈ Submodule.span ℂ (wordSet d w) := by
…

Mentions: OAI.KadisonSimilarity.DihedralWordAlgebra.wordSet

def OAI.KadisonSimilarity.DihedralWordAlgebra.spanStarAlgebra line 119

Source documentation

The span itself is the required unital star subalgebra.

def spanStarAlgebra (d w : Pˣ) (hd : d * d = 1) (hc : d * w = w⁻¹ * d)
    (hdstar : star d = d) (hwstar : star w = w⁻¹) : StarSubalgebra ℂ P where
…

theorem OAI.KadisonSimilarity.DihedralWordAlgebra.spanStarAlgebra_toSubmodule line 131
theorem OAI.KadisonSimilarity.DihedralWordAlgebra.reflection_mem line 137
Source documentation
The normal-form span contains the reflection.
```
theorem reflection_mem (d w : Pˣ) (hd : d * d = 1) (hc : d * w = w⁻¹ * d)
    (hdstar : star d = d) (hwstar : star w = w⁻¹) :
    (d : P) ∈ spanStarAlgebra d w hd hc hdstar hwstar :=
…
```
Mentions: OAI.KadisonSimilarity.DihedralWordAlgebra.spanStarAlgebra
theorem OAI.KadisonSimilarity.DihedralWordAlgebra.rotation_mem line 143
Source documentation
The normal-form span contains the rotation.
```
theorem rotation_mem (d w : Pˣ) (hd : d * d = 1) (hc : d * w = w⁻¹ * d)
    (hdstar : star d = d) (hwstar : star w = w⁻¹) :
    (w : P) ∈ spanStarAlgebra d w hd hc hdstar hwstar :=
…
```
Mentions: OAI.KadisonSimilarity.DihedralWordAlgebra.spanStarAlgebra

theorem OAI.KadisonSimilarity.DihedralWordAlgebra.second_symmetry_mem line 149

Source documentation

The other symmetry is the reflection times the rotation.

theorem second_symmetry_mem (d s : Pˣ) (hd : d * d = 1)
    (hc : d * (d * s) = (d * s)⁻¹ * d)
    (hdstar : star d = d) (hwstar : star (d * s) = (d * s)⁻¹) :
    (s : P) ∈ spanStarAlgebra d (d * s) hd hc hdstar hwstar := by
…

Mentions: OAI.KadisonSimilarity.DihedralWordAlgebra.spanStarAlgebra

theorem OAI.KadisonSimilarity.DihedralWordAlgebra.generated_le_span line 164

Source documentation

Thus every finite algebraic star word in the two symmetries belongs to the linear span of dihedral normal forms.

theorem generated_le_span (d s : Pˣ) (hd : d * d = 1)
    (hc : d * (d * s) = (d * s)⁻¹ * d)
    (hdstar : star d = d) (hwstar : star (d * s) = (d * s)⁻¹) :
    StarAlgebra.adjoin ℂ ({(d : P), (s : P)} : Set P) ≤
      spanStarAlgebra d (d * s) hd hc hdstar hwstar := by
…

Mentions: OAI.KadisonSimilarity.DihedralWordAlgebra.spanStarAlgebra

theorem OAI.KadisonSimilarity.DihedralWordAlgebra.map_mem_word_span line 177
Source documentation
A linear map takes the ordinary word span into the span of its word vectors.
```
theorem map_mem_word_span {H : Type*} [AddCommGroup H] [Module ℂ H]
    (V : P →ₗ[ℂ] H) (d w : Pˣ) {a : P}
    (ha : a ∈ Submodule.span ℂ (wordSet d w)) :
    V a ∈ Submodule.span ℂ (V '' wordSet d w) := by
…
```
Mentions: OAI.KadisonSimilarity.DihedralWordAlgebra.wordSet
theorem OAI.KadisonSimilarity.TracialCornerGeometry.image_dihedralWordSet line 195
Source documentation
The algebraic and Hilbert-space versions of the normal-form set agree.
```
theorem image_dihedralWordSet (d w : Pˣ) :
    G.vector '' DihedralWordAlgebra.wordSet d w = G.dihedralGroupWordVectors d w := by
…
```
Mentions: OAI.KadisonSimilarity.DihedralWordAlgebra.wordSet

theorem OAI.KadisonSimilarity.TracialCornerGeometry.group_word_density_of_generated_density line 209

Source documentation

Density of the ordinary generated star algebra supplies exactly the dihedral group-word span used by the centered corner argument.

theorem group_word_density_of_generated_density
    (d s : Pˣ) (hdi : d⁻¹ = d) (hsi : s⁻¹ = s)
    (hdstar : star d = d) (hsstar : star s = s) (x : P)
    (hspan : G.vector x ∈ (Submodule.span ℂ
      (G.vector '' (StarAlgebra.adjoin ℂ ({(d : P), (s : P)} : Set P) : Set P))).topologicalClosure) :
    G.vector x ∈ (Submodule.span ℂ (G.dihedralGroupWordVectors d (d * s))).topologicalClosure := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.scalarFree_corner_of_generated_word_density line 230

Source documentation

Corner freeness reduces to ordinary L²-density of the algebra generated by the two centered symmetries.

theorem scalarFree_corner_of_generated_word_density
    (D A C : StarSubalgebra ℂ P) (hf : ScalarFree G.trace D A) (hτ : G.trace 1 = 1)
    (d s : Pˣ) (hd : (d : P) ∈ D) (hs : (s : P) ∈ A)
    (hd0 : G.trace (d : P) = 0) (hs0 : G.trace (s : P) = 0)
    (hdi : d⁻¹ = d) (hsi : s⁻¹ = s) (hdstar : star d = d) (hsstar : star s = s)
    (hp : IsStarProjection (dihedralHalfProjection d))
    (hpC : dihedralHalfProjection d ∈ C)
    (hspan : ∀ x : CStarCorner (dihedralHalfProjection d) hp, (x : P) ∈ C →
      G.vector (x : P) ∈ (Submodule.span ℂ
        (G.vector '' (StarAlgebra.adjoin ℂ ({(d : P), (s : P)} : Set P) : Set P))).topologicalClosure) :
    ScalarFree (CStarCorner.normalizedTrace (dihedralHalfProjection d) hp G.trace)
      (CStarCorner.subalgebra (dihedralHalfProjection d) hp D
…

Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.CStarCorner.normalizedTrace, OAI.KadisonSimilarity.CStarCorner.subalgebra