Geometric representation of Coxeter groups

This file defines the geometric representation of a Coxeter group.

Main definitions

• Coxeter.geomRep : The geometric representation

Main statements

• Coxeter.orderOf_simple_mul_simple : $s_i s_{i'}$ has the expected order
• Coxeter.simple_inj

TODO

• Pin down the orientation in Coxeter.oangle_stdBasisE

References

• [Bou07] N. Bourbaki, Groupes et algèbres de Lie

@[reducible, inline]

abbrev Coxeter.V (W : Type u_1) [CoxeterGroup W] : Type u_2

Equations

• Coxeter.V W = (Coxeter.CoxeterGroup.B W →₀ ℝ)

noncomputable def Coxeter.stdBasis {W : Type u_1} [CoxeterGroup W] : Module.Basis (CoxeterGroup.B W) ℝ (V W)

Equations

• Coxeter.stdBasis = Finsupp.basisSingleOne

noncomputable def Coxeter.bil {W : Type u_1} [CoxeterGroup W] : LinearMap.BilinForm ℝ (V W)

Equations

• Coxeter.bil = (Coxeter.Matrix.toBilin Coxeter.stdBasis) fun (i i' : Coxeter.CoxeterGroup.B W) => -Real.cos (Real.pi / ↑(Coxeter.CoxeterGroup.M.M i i'))

theorem Coxeter.bil_isSymm {W : Type u_1} [CoxeterGroup W] : bil.IsSymm

@[simp]

theorem Coxeter.bil_eq {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : (bil (stdBasis i)) (stdBasis i') = -Real.cos (Real.pi / ↑(CoxeterGroup.M.M i i'))

@[simp]

theorem Coxeter.bil_diag {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) : (bil (stdBasis i)) (stdBasis i) = 1

theorem Coxeter.bil_off_diag_le {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) (h : i ≠ i') : (bil (stdBasis i)) (stdBasis i') ≤ 0

noncomputable def Coxeter.geomRepAux {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) : V W ≃ₗ[ℝ] V W

Equations

• One or more equations did not get rendered due to their size.

theorem Coxeter.geomRepAux_apply {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (x : V W) : (geomRepAux i) x = x - (2 * (bil (stdBasis i)) x) • stdBasis i

theorem Coxeter.geomRepAux_involutive {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) : Function.Involutive ⇑(geomRepAux i)

theorem Coxeter.orderOf_geomRepAux_mul_geomRepAux₁ {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) (h : CoxeterGroup.M.M i i' = 1) : orderOf (geomRepAux i * geomRepAux i') = 1

@[simp]

theorem Coxeter.geomRepAux_stdBasis {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) : (geomRepAux i) (stdBasis i) = -stdBasis i

def Coxeter.E {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : Submodule ℝ (V W)

Equations

• Coxeter.E i i' = Finsupp.supported ℝ ℝ {i, i'}

theorem Coxeter.E_eq_span {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : E i i' = Submodule.span ℝ {stdBasis i, stdBasis i'}

theorem Coxeter.mem_E_iff {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) (v : V W) : v ∈ E i i' ↔ ∃ (x : ℝ) (y : ℝ), v = x • stdBasis i + y • stdBasis i'

theorem Coxeter.E_symm {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : E i i' = E i' i

theorem Coxeter.bil_restrict_E_diag {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) (x y : ℝ) : (bil (x • stdBasis i + y • stdBasis i')) (x • stdBasis i + y • stdBasis i') = (x - y * Real.cos (Real.pi / ↑(CoxeterGroup.M.M i i'))) ^ 2 + (y * Real.sin (Real.pi / ↑(CoxeterGroup.M.M i i'))) ^ 2

theorem Coxeter.bil_restrict_E_isSymm {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : (bil.restrict (E i i')).IsSymm

theorem Coxeter.bil_restrict_E_nonneg {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : (bil.restrict (E i i')).IsNonneg

theorem Coxeter.bil_restrict_E_isPosSemidef {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : (bil.restrict (E i i')).IsPosSemidef

Bourbaki Ch V, §4, Proposition 1

theorem Coxeter.bil_restrict_E_nondegenerate_iff {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) (h : i ≠ i') : (bil.restrict (E i i')).Nondegenerate ↔ CoxeterGroup.M.M i i' ≠ 0

Bourbaki Ch V, §4, Proposition 1 (continued)

theorem Coxeter.geomRepAux_E_perp_left {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) (z : V W) : z ∈ Submodule.orthogonalBilin bil (E i i') → (geomRepAux i) z = z

theorem Coxeter.geomRepAux_E_perp_right {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) (z : V W) : z ∈ Submodule.orthogonalBilin bil (E i i') → (geomRepAux i') z = z

theorem Coxeter.geomRepAux_E_left {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : Set.MapsTo ⇑(geomRepAux i) ↑(E i i') ↑(E i i')

theorem Coxeter.geomRepAux_E_right {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : Set.MapsTo ⇑(geomRepAux i') ↑(E i i') ↑(E i i')

theorem Coxeter.geomRepAux_E_2 {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : Set.MapsTo ⇑(geomRepAux i * geomRepAux i') ↑(E i i') ↑(E i i')

theorem Coxeter.restrict_geomRepAux_mul {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : (↑(geomRepAux i * geomRepAux i')).restrict ⋯ = (↑(geomRepAux i)).restrict ⋯ ∘ₗ (↑(geomRepAux i')).restrict ⋯

theorem Coxeter.geomRepAux_mul_geomRepAux_pow₀ {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) (h : CoxeterGroup.M.M i i' = 0) (n : ℕ) : ((geomRepAux i * geomRepAux i') ^ n) (stdBasis i) = (2 * n) • (stdBasis i + stdBasis i') + stdBasis i

theorem Coxeter.orderOf_geomRepAux_mul_geomRepAux₀ {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) (h : CoxeterGroup.M.M i i' = 0) : orderOf (geomRepAux i * geomRepAux i') = 0

theorem Coxeter.index_ne {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : i ≠ i'

noncomputable def Coxeter.e {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : ↑{i, i'} ≃ Fin 2

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Coxeter.stdBasisE {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : Module.Basis (Fin 2) ℝ ↥(E i i')

Equations

• Coxeter.stdBasisE i i' = (Finsupp.basisSingleOne.map (Finsupp.supportedEquivFinsupp {i, i'}).symm).reindex (Coxeter.e i i')

@[simp]

theorem Coxeter.stdBasisE_0 {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : ↑((stdBasisE i i') 0) = stdBasis i

@[simp]

theorem Coxeter.stdBasisE_1 {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : ↑((stdBasisE i i') 1) = stdBasis i'

instance Coxeter.instFiniteDimensionalRealSubtypeVMemSubmoduleE {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : FiniteDimensional ℝ ↥(E i i')

theorem Coxeter.finrank_E_eq_two {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : Module.finrank ℝ ↥(E i i') = 2

instance Coxeter.instFactEqNatFinrankRealSubtypeVMemSubmoduleEOfNat {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : Fact (Module.finrank ℝ ↥(E i i') = 2)

theorem Coxeter.E_sup_orthogonal {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : E i i' ⊔ Submodule.orthogonalBilin bil (E i i') = ⊤

theorem Coxeter.orderOf_geomRepAux_mul_geomRepAux_eq_orderOf_restrict {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] (m : ℕ) : (geomRepAux i * geomRepAux i') ^ m = 1 ↔ (↑(geomRepAux i * geomRepAux i')).restrict ⋯ ^ m = 1

@[instance_reducible]

noncomputable instance Coxeter.instCoreRealSubtypeVMemSubmoduleE {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : PreInnerProductSpace.Core ℝ ↥(E i i')

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Coxeter.instCoreRealSubtypeVMemSubmoduleE_1 {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : InnerProductSpace.Core ℝ ↥(E i i')

Equations

• Coxeter.instCoreRealSubtypeVMemSubmoduleE_1 i i' = { toCore := Coxeter.instCoreRealSubtypeVMemSubmoduleE i i', definite := ⋯ }

@[instance_reducible]

noncomputable instance Coxeter.instNormedAddCommGroupSubtypeVMemSubmoduleRealE {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : NormedAddCommGroup ↥(E i i')

Equations

• Coxeter.instNormedAddCommGroupSubtypeVMemSubmoduleRealE i i' = InnerProductSpace.Core.toNormedAddCommGroup

@[instance_reducible]

noncomputable instance Coxeter.instInnerProductSpaceRealSubtypeVMemSubmoduleE {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : InnerProductSpace ℝ ↥(E i i')

Equations

• Coxeter.instInnerProductSpaceRealSubtypeVMemSubmoduleE i i' = InnerProductSpace.ofCore inferInstance

@[simp]

theorem Coxeter.norm_stdBasisE_0 {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : ‖(stdBasisE i i') 0‖ = 1

@[simp]

theorem Coxeter.norm_stdBasisE_1 {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : ‖(stdBasisE i i') 1‖ = 1

@[simp]

theorem Coxeter.inner_stdBasisE_0_1 {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : inner ℝ ((stdBasisE i i') 0) ((stdBasisE i i') 1) = -Real.cos (Real.pi / ↑(CoxeterGroup.M.M i i'))

theorem Coxeter.oangle_stdBasisE {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : ∃ (o : Orientation ℝ (↥(E i i')) (Fin 2)), o.oangle ((stdBasisE i i') 0) ((stdBasisE i i') 1) = ↑(Real.pi - Real.pi / ↑(CoxeterGroup.M.M i i'))

theorem Coxeter.restrict_geomRepAux_left_eq_reflect {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : (↑(geomRepAux i)).restrict ⋯ = ↑(reflect ⋯)

theorem Coxeter.restrict_geomRepAux_right_eq_reflect {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : (↑(geomRepAux i')).restrict ⋯ = ↑(reflect ⋯)

theorem Coxeter.restrict_geomRepAux_mul_geomRep_aux_eq_rotate {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : ∃ (o : Orientation ℝ (↥(E i i')) (Fin 2)), (↑(geomRepAux i * geomRepAux i')).restrict ⋯ = ↑(o.rotation ↑(2 * Real.pi / ↑(CoxeterGroup.M.M i i'))).toLinearEquiv

theorem Coxeter.orderOf_geomRepAux_mul_geomRepAux₂ {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) [Fact (CoxeterGroup.M.M i i' ≥ 2)] : orderOf (geomRepAux i * geomRepAux i') = CoxeterGroup.M.M i i'

theorem Coxeter.geomRepAux_liftable {W : Type u_1} [CoxeterGroup W] : CoxeterGroup.M.IsLiftable geomRepAux

noncomputable def Coxeter.geomRep {W : Type u_1} [CoxeterGroup W] : W →* V W ≃ₗ[ℝ] V W

The geometric representation

Equations

• Coxeter.geomRep = Coxeter.CoxeterGroup.cs.lift ⟨Coxeter.geomRepAux, ⋯⟩

theorem Coxeter.geomRep_simple {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) : geomRep (CoxeterGroup.cs.simple i) = geomRepAux i

theorem Coxeter.geomRep_simple_apply {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (x : V W) : (geomRep (CoxeterGroup.cs.simple i)) x = x - (2 * (bil (stdBasis i)) x) • stdBasis i

theorem Coxeter.orderOf_geomRep_simple_mul_simple {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : orderOf (geomRep (CoxeterGroup.cs.simple i * CoxeterGroup.cs.simple i')) = CoxeterGroup.M.M i i'

theorem Coxeter.orderOf_simple_mul_simple {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : orderOf (CoxeterGroup.cs.simple i * CoxeterGroup.cs.simple i') = CoxeterGroup.M.M i i'

theorem Coxeter.simple_inj {W : Type u_1} [CoxeterGroup W] : Function.Injective CoxeterGroup.cs.simple

theorem Coxeter.finite_generating_set {W : Type u_1} [CoxeterGroup W] [Finite W] : Finite (CoxeterGroup.B W)