def AffineWeylGroupData.weylActionAddAut {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupData E) (w : ↥d.weylGroup) : AddAut ↥d.corootLattice

The additive automorphism of the coroot lattice $Λ(\check Φ)$ induced by an element $w$ of the linear Weyl group.

def AffineWeylGroupData.weylActionMulAutHom {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupData E) : ↥d.weylGroup →* MulAut (Multiplicative ↥d.corootLattice)

The induced homomorphism $W → \mathrm{MulAut}(\mathrm{Multiplicative}\ Λ(\check Φ))$ used to form the semidirect product $W_a = Λ(\check Φ) ⋊ W$.

@[reducible, inline]

abbrev AffineWeylGroupData.AffineWeylSemidirect {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupData E) : Type u_1

The abstract semidirect product $Λ(\check Φ) ⋊ W$ associated to the affine Weyl group data.

structure AffineWeylSemidirectData (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] extends AffineWeylGroupFullData E : Type u_2

Data witnessing that a concrete subgroup of $\mathrm{Isom}(E)$ realizes the affine Weyl group as a semidirect product: every element decomposes as a linear part plus a coroot translation, with the linear part in $W$ and the translation in $Λ(\check Φ)$, and every pair $(w, v) ∈ W × Λ(\check Φ)$ is realized.

• roots : Set E
• roots_ne_zero (α : E) : α ∈ self.roots → α ≠ 0
• roots_reduced (α : E) : α ∈ self.roots → ∀ (t : ℝ), t • α ∈ self.roots → t = 1 ∨ t = -1
• weylGroup : Subgroup (E ≃ₗᵢ[ℝ] E)
• corootLattice : AddSubgroup E
• weylGroup_stable_corootLattice (w : E ≃ₗᵢ[ℝ] E) : w ∈ self.weylGroup → ∀ v ∈ self.corootLattice, w v ∈ self.corootLattice
• roots_finite : self.roots.Finite
• coroot : E → E
• coroot_def (α : E) : α ∈ self.roots → self.coroot α = (2 / inner ℝ α α) • α
• coroot_mem_lattice (α : E) : α ∈ self.roots → self.coroot α ∈ self.corootLattice
• crystallographic (α : E) : α ∈ self.roots → ∀ β ∈ self.roots, ∃ (n : ℤ), inner ℝ (self.coroot α) β = ↑n
• weylGroup_stable_roots (w : E ≃ₗᵢ[ℝ] E) : w ∈ self.weylGroup → ∀ α ∈ self.roots, w α ∈ self.roots
• corootLattice_int (α : E) : α ∈ self.roots → ∀ v ∈ self.corootLattice, ∃ (m : ℤ), inner ℝ v α = ↑m
• affineWeylSubgroup : Subgroup (E ≃ᵃⁱ[ℝ] E)
• affine_decomp (g : E ≃ᵃⁱ[ℝ] E) : g ∈ self.affineWeylSubgroup → ∀ (x : E), g x = (linearPartHom g) x + g 0
• translationPart_mem (g : E ≃ᵃⁱ[ℝ] E) : g ∈ self.affineWeylSubgroup → g 0 ∈ self.corootLattice
• linearPart_mem (g : E ≃ᵃⁱ[ℝ] E) : g ∈ self.affineWeylSubgroup → linearPartHom g ∈ self.weylGroup
• pair_mem (w : E ≃ₗᵢ[ℝ] E) : w ∈ self.weylGroup → ∀ v ∈ self.corootLattice, ∃ g ∈ self.affineWeylSubgroup, linearPartHom g = w ∧ g 0 = v

@[reducible, inline]

abbrev AffineWeylSemidirectData.SemiType {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylSemidirectData E) : Type u_1

Shorthand for the abstract semidirect product type.

noncomputable def AffineWeylSemidirectData.toSemidirect {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylSemidirectData E) (g : ↥d.affineWeylSubgroup) : d.SemiType

Map sending $g ∈ W_a$ to the pair $(g\cdot 0,\ \mathrm{linearPart}(g))$ in the semidirect product.

theorem AffineWeylSemidirectData.ext_of_decomp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylSemidirectData E) (g₁ g₂ : ↥d.affineWeylSubgroup) (hlin : linearPartHom ↑g₁ = linearPartHom ↑g₂) (htrans : ↑g₁ 0 = ↑g₂ 0) : g₁ = g₂

Two elements of $W_a$ with the same linear part and translation part agree.

theorem AffineWeylSemidirectData.toSemidirect_injective {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylSemidirectData E) : Function.Injective d.toSemidirect

The map $g \mapsto (g\cdot 0, \mathrm{linearPart}(g))$ is injective.

theorem AffineWeylSemidirectData.toSemidirect_surjective {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylSemidirectData E) : Function.Surjective d.toSemidirect

Every pair $(w, v) ∈ W × Λ(\check Φ)$ comes from some $g ∈ W_a$.

theorem AffineWeylSemidirectData.toSemidirect_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylSemidirectData E) (g₁ g₂ : ↥d.affineWeylSubgroup) : d.toSemidirect (g₁ * g₂) = d.toSemidirect g₁ * d.toSemidirect g₂

The map toSemidirect is multiplicative: it preserves the group law of $W_a$.

noncomputable def AffineWeylSemidirectData.affineWeyl_semidirect_equiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylSemidirectData E) : ↥d.affineWeylSubgroup ≃* d.SemiType

The promised group isomorphism $W_a ≃ Λ(\check Φ) ⋊ W$.

def AffineWeylGroup.affineReflections {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Wa : AffineWeylGroup E) : Set (E ≃ᵃⁱ[ℝ] E)

The set of affine reflections of the affine Weyl group $W_a$.

theorem AffineWeylGroup.reflections_generate_affineWeylGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Wa : AffineWeylGroup E) : Subgroup.closure Wa.affineReflections = Wa.reflGroup.group

The affine Weyl group is generated by its affine reflections.

theorem AffineWeylGroupFullData.coroot_translation_is_product_of_reflections {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) (α : E) (hα : α ∈ d.roots) (v : E) : v + d.coroot α = d.affineReflFun α 1 (d.affineReflFun α 0 v)

Translation by $\check α$ is the product of two affine reflections $s_{α,1} s_{α,0}$.