feat (LinearAlgebra/RootSystem/Defs): define Weyl group (#15702)

This PR defines the Weyl group of a root pairing, and its permutation representation on the indexing set of roots.

Co-authored-by: Deepro Choudhury

Author: ScottCarnahan

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

@@ -242,6 +242,16 @@ instance sup_normal (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊔
     refine ⟨g * h * g⁻¹, hH.conj_mem h hh g, g * k * g⁻¹, hK.conj_mem k hk g, ?_⟩
     simp only [mul_assoc, inv_mul_cancel_left]
 
+@[to_additive]
+theorem smul_mem_of_mem_closure_of_mem {X : Type*} [MulAction G X] {s : Set G} {t : Set X}
+    (hs : ∀ g ∈ s, g⁻¹ ∈ s) (hst : ∀ᵉ (g ∈ s) (x ∈ t), g • x ∈ t) {g : G}
+    (hg : g ∈ Subgroup.closure s) {x : X} (hx : x ∈ t) : g • x ∈ t := by
+  induction hg using Subgroup.closure_induction'' generalizing x with
+  | one => simpa
+  | mem g' hg' => exact hst g' hg' x hx
+  | inv_mem g' hg' => exact hst g'⁻¹ (hs g' hg') x hx
+  | mul _ _ _ _ h₁ h₂ => rw [mul_smul]; exact h₁ (h₂ hx)
+
 @[to_additive]
 theorem smul_opposite_image_mul_preimage' (g : G) (h : Gᵐᵒᵖ) (s : Set G) :
     (fun y => h • y) '' ((g * ·) ⁻¹' s) = (g * ·) ⁻¹' ((fun y => h • y) '' s) := by

Mathlib/LinearAlgebra/RootSystem/Defs.lean

@@ -16,25 +16,25 @@ This file contains basic definitions for root systems and root data.
  * `RootPairing`: Given two perfectly-paired `R`-modules `M` and `N` (over some commutative ring
    `R`) a root pairing with indexing set `ι` is the data of an `ι`-indexed subset of `M`
    ("the roots") an `ι`-indexed subset of `N` ("the coroots"), and an `ι`-indexed set of
-   permutations of `ι` such that each root-coroot pair
-   evaluates to `2`, and the permutation attached to each element of `ι` is compatible with the
-   reflections on the corresponding roots and coroots.
+   permutations of `ι` such that each root-coroot pair evaluates to `2`, and the permutation
+   attached to each element of `ι` is compatible with the reflections on the corresponding roots and
+   coroots.
  * `RootDatum`: A root datum is a root pairing for which the roots and coroots take values in
    finitely-generated free Abelian groups.
  * `RootSystem`: A root system is a root pairing for which the roots span their ambient module.
  * `RootPairing.IsCrystallographic`: A root pairing is said to be crystallographic if the pairing
    between a root and coroot is always an integer.
- * `RootPairing.IsReduced`: A root pairing is said to be reduced if it never contains the double of
-   a root.
+ * `RootPairing.IsReduced`: A root pairing is said to be reduced if two linearly dependent roots are
+   always related by a sign.
+ * `RootPairing.weylGroup`: The group of linear isomorphisms on `M` generated by reflections.
+ * `RootPairing.weylGroupToPerm`: The permutation representation of the Weyl group on `ι`.
 
 ## TODO
 
-* Put more API theorems in the Defs file.
-* Introduce the Weyl Group, and its action on the indexing set.
-* Base change of root pairings (may need flatness).
-* Isomorphism of root pairings.
-* Crystallographic root systems are isomorphic to base changes of root systems over `ℤ`: Take
-  `M₀` and `N₀` to be the `ℤ`-span of roots and coroots.
+ * Base change of root pairings (may need flatness; perhaps should go in a different file).
+ * Isomorphism of root pairings.
+ * Crystallographic root systems are isomorphic to base changes of root systems over `ℤ`: Take
+   `M₀` and `N₀` to be the `ℤ`-span of roots and coroots.
 
 ## Implementation details
 
@@ -115,6 +115,8 @@ required to be the dual of `M`. -/
 structure RootSystem extends RootPairing ι R M N :=
   span_eq_top : span R (range root) = ⊤
 
+attribute [simp] RootSystem.span_eq_top
+
 namespace RootPairing
 
 variable {ι R M N}
@@ -189,6 +191,28 @@ lemma reflection_same (x : M) :
     P.reflection i (P.reflection i x) = x :=
   Module.involutive_reflection (P.coroot_root_two i) x
 
+@[simp]
+lemma reflection_inv :
+    (P.reflection i)⁻¹ = P.reflection i :=
+  rfl
+
+@[simp]
+lemma reflection_sq :
+    P.reflection i ^ 2 = 1 :=
+  mul_eq_one_iff_eq_inv.mpr rfl
+
+@[simp]
+lemma reflection_perm_sq :
+    P.reflection_perm i ^ 2 = 1 := by
+  ext j
+  refine Embedding.injective P.root ?_
+  simp only [sq, Equiv.Perm.mul_apply, root_reflection_perm, reflection_same, Equiv.Perm.one_apply]
+
+@[simp]
+lemma reflection_perm_inv :
+    (P.reflection_perm i)⁻¹ = P.reflection_perm i :=
+  (mul_eq_one_iff_eq_inv.mp <| P.reflection_perm_sq i).symm
+
 lemma bijOn_reflection_root :
     BijOn (P.reflection i) (range P.root) (range P.root) :=
   Module.bijOn_reflection_of_mapsTo _ <| P.mapsTo_reflection_root i
@@ -230,6 +254,16 @@ lemma coreflection_same (x : N) :
     P.coreflection i (P.coreflection i x) = x :=
   Module.involutive_reflection (P.flip.coroot_root_two i) x
 
+@[simp]
+lemma coreflection_inv :
+    (P.coreflection i)⁻¹ = P.coreflection i :=
+  rfl
+
+@[simp]
+lemma coreflection_sq :
+    P.coreflection i ^ 2 = 1 :=
+  mul_eq_one_iff_eq_inv.mpr rfl
+
 lemma bijOn_coreflection_coroot : BijOn (P.coreflection i) (range P.coroot) (range P.coroot) :=
   bijOn_reflection_root P.flip i
 
@@ -280,6 +314,150 @@ lemma isReduced_iff : P.IsReduced ↔ ∀ i j : ι, i ≠ j →
     · exact Or.inl (congrArg P.root h')
     · exact Or.inr (h i j h' hLin)
 
+/-- The `Weyl group` of a root pairing is the group of automorphisms of the weight space generated
+by reflections in roots. -/
+def weylGroup : Subgroup (M ≃ₗ[R] M) :=
+  Subgroup.closure (range P.reflection)
+
+lemma reflection_mem_weylGroup : P.reflection i ∈ P.weylGroup :=
+  Subgroup.subset_closure <| mem_range_self i
+
+lemma mem_range_root_of_mem_range_reflection_of_mem_range_root
+    {r : M ≃ₗ[R] M} {α : M} (hr : r ∈ range P.reflection) (hα : α ∈ range P.root) :
+    r • α ∈ range P.root := by
+  obtain ⟨i, rfl⟩ := hr
+  obtain ⟨j, rfl⟩ := hα
+  exact ⟨P.reflection_perm i j, P.root_reflection_perm i j⟩
+
+lemma mem_range_coroot_of_mem_range_coreflection_of_mem_range_coroot
+    {r : N ≃ₗ[R] N} {α : N} (hr : r ∈ range P.coreflection) (hα : α ∈ range P.coroot) :
+    r • α ∈ range P.coroot := by
+  obtain ⟨i, rfl⟩ := hr
+  obtain ⟨j, rfl⟩ := hα
+  exact ⟨P.reflection_perm i j, P.coroot_reflection_perm i j⟩
+
+lemma exists_root_eq_smul_of_mem_weylGroup {w : M ≃ₗ[R] M} (hw : w ∈ P.weylGroup) (i : ι) :
+    ∃ j, P.root j = w • P.root i :=
+  Subgroup.smul_mem_of_mem_closure_of_mem (by simp)
+    (fun _ h _ ↦ P.mem_range_root_of_mem_range_reflection_of_mem_range_root h) hw (mem_range_self i)
+
+/-- The permutation representation of the Weyl group induced by `reflection_perm`. -/
+def weylGroupToPerm : P.weylGroup →* Equiv.Perm ι where
+  toFun w :=
+  { toFun := fun i => (P.exists_root_eq_smul_of_mem_weylGroup w.2 i).choose
+    invFun := fun i => (P.exists_root_eq_smul_of_mem_weylGroup w⁻¹.2 i).choose
+    left_inv := fun i => by
+      obtain ⟨w, hw⟩ := w
+      apply P.root.injective
+      rw [(P.exists_root_eq_smul_of_mem_weylGroup ((Subgroup.inv_mem_iff P.weylGroup).mpr hw)
+          ((P.exists_root_eq_smul_of_mem_weylGroup hw i).choose)).choose_spec,
+        (P.exists_root_eq_smul_of_mem_weylGroup hw i).choose_spec, inv_smul_smul]
+    right_inv := fun i => by
+      obtain ⟨w, hw⟩ := w
+      have hw' : w⁻¹ ∈ P.weylGroup := (Subgroup.inv_mem_iff P.weylGroup).mpr hw
+      apply P.root.injective
+      rw [(P.exists_root_eq_smul_of_mem_weylGroup hw
+          ((P.exists_root_eq_smul_of_mem_weylGroup hw' i).choose)).choose_spec,
+        (P.exists_root_eq_smul_of_mem_weylGroup hw' i).choose_spec, smul_inv_smul] }
+  map_one' := by ext; simp
+  map_mul' x y := by
+    obtain ⟨x, hx⟩ := x
+    obtain ⟨y, hy⟩ := y
+    ext i
+    apply P.root.injective
+    simp only [Equiv.coe_fn_mk, Equiv.Perm.coe_mul, comp_apply]
+    rw [(P.exists_root_eq_smul_of_mem_weylGroup (mul_mem hx hy) i).choose_spec,
+      (P.exists_root_eq_smul_of_mem_weylGroup hx
+        ((P.exists_root_eq_smul_of_mem_weylGroup hy i).choose)).choose_spec,
+      (P.exists_root_eq_smul_of_mem_weylGroup hy i).choose_spec, mul_smul]
+
+@[simp]
+lemma weylGroupToPerm_apply_reflection :
+    P.weylGroupToPerm ⟨P.reflection i, P.reflection_mem_weylGroup i⟩ = P.reflection_perm i := by
+  ext j
+  apply P.root.injective
+  rw [weylGroupToPerm, MonoidHom.coe_mk, OneHom.coe_mk, Equiv.coe_fn_mk, root_reflection_perm,
+    (P.exists_root_eq_smul_of_mem_weylGroup (P.reflection_mem_weylGroup i) j).choose_spec,
+    LinearEquiv.smul_def]
+
+@[simp]
+lemma range_weylGroupToPerm :
+    P.weylGroupToPerm.range = Subgroup.closure (range P.reflection_perm) := by
+  refine (Subgroup.closure_eq_of_le _ ?_ ?_).symm
+  · rintro - ⟨i, rfl⟩
+    simpa only [← weylGroupToPerm_apply_reflection] using mem_range_self _
+  · rintro - ⟨⟨w, hw⟩, rfl⟩
+    induction hw using Subgroup.closure_induction'' with
+    | one =>
+      change P.weylGroupToPerm 1 ∈ _
+      simpa only [map_one] using Subgroup.one_mem _
+    | mem w' hw' =>
+      obtain ⟨i, rfl⟩ := hw'
+      simpa only [weylGroupToPerm_apply_reflection] using Subgroup.subset_closure (mem_range_self i)
+    | inv_mem w' hw' =>
+      obtain ⟨i, rfl⟩ := hw'
+      simpa only [reflection_inv, weylGroupToPerm_apply_reflection] using
+        Subgroup.subset_closure (mem_range_self i)
+    | mul w₁ w₂ hw₁ hw₂ h₁ h₂ =>
+      simpa only [← Submonoid.mk_mul_mk _ w₁ w₂ hw₁ hw₂, map_mul] using Subgroup.mul_mem _ h₁ h₂
+
+lemma pairing_smul_root_eq (k : ι) (hij : P.reflection_perm i = P.reflection_perm j) :
+    P.pairing k i • P.root i = P.pairing k j • P.root j := by
+  have h : P.reflection i (P.root k) = P.reflection j (P.root k) := by
+    simp only [← root_reflection_perm, hij]
+  simpa only [reflection_apply_root, sub_right_inj] using h
+
+lemma pairing_smul_coroot_eq (k : ι) (hij : P.reflection_perm i = P.reflection_perm j) :
+    P.pairing i k • P.coroot i = P.pairing j k • P.coroot j := by
+  have h : P.coreflection i (P.coroot k) = P.coreflection j (P.coroot k) := by
+    simp only [← coroot_reflection_perm, hij]
+  simpa only [coreflection_apply_coroot, sub_right_inj] using h
+
+lemma two_nsmul_reflection_eq_of_perm_eq (hij : P.reflection_perm i = P.reflection_perm j) :
+    2 • ⇑(P.reflection i) = 2 • P.reflection j := by
+  ext x
+  suffices 2 • P.toLin x (P.coroot i) • P.root i = 2 • P.toLin x (P.coroot j) • P.root j by
+    simpa [reflection_apply]
+  calc 2 • P.toLin x (P.coroot i) • P.root i
+      = P.toLin x (P.coroot i) • ((2 : R) • P.root i) := ?_
+    _ = P.toLin x (P.coroot i) • (P.pairing i j • P.root j) := ?_
+    _ = P.toLin x (P.pairing i j • P.coroot i) • (P.root j) := ?_
+    _ = P.toLin x ((2 : R) • P.coroot j) • (P.root j) := ?_
+    _ = 2 • P.toLin x (P.coroot j) • P.root j := ?_
+  · rw [smul_comm, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]
+  · rw [P.pairing_smul_root_eq j i i hij.symm, pairing_same]
+  · rw [← smul_comm, ← smul_assoc, map_smul]
+  · rw [← P.pairing_smul_coroot_eq j i j hij.symm, pairing_same]
+  · rw [map_smul, smul_assoc, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]
+
+lemma reflection_perm_eq_reflection_perm_iff_of_isSMulRegular (h2 : IsSMulRegular M 2) :
+    P.reflection_perm i = P.reflection_perm j ↔ P.reflection i = P.reflection j := by
+  refine ⟨fun h ↦ ?_, fun h ↦ Equiv.ext fun k ↦ P.root.injective <| by simp [h]⟩
+  suffices ⇑(P.reflection i) = ⇑(P.reflection j) from DFunLike.coe_injective this
+  replace h2 : IsSMulRegular (M → M) 2 := IsSMulRegular.pi fun _ ↦ h2
+  exact h2 <| P.two_nsmul_reflection_eq_of_perm_eq i j h
+
+lemma reflection_perm_eq_reflection_perm_iff_of_span :
+    P.reflection_perm i = P.reflection_perm j ↔
+    ∀ x ∈ span R (range P.root), P.reflection i x = P.reflection j x := by
+  refine ⟨fun h x hx ↦ ?_, fun h ↦ ?_⟩
+  · induction hx using Submodule.span_induction' with
+    | mem x hx =>
+      obtain ⟨k, rfl⟩ := hx
+      simp only [← root_reflection_perm, h]
+    | zero => simp
+    | add x _ y _ hx hy => simp [hx, hy]
+    | smul t x _ hx => simp [hx]
+  · ext k
+    apply P.root.injective
+    simp [h (P.root k) (Submodule.subset_span <| mem_range_self k)]
+
+lemma _root_.RootSystem.reflection_perm_eq_reflection_perm_iff (P : RootSystem ι R M N) (i j : ι) :
+    P.reflection_perm i = P.reflection_perm j ↔ P.reflection i = P.reflection j := by
+  refine ⟨fun h ↦ ?_, fun h ↦ Equiv.ext fun k ↦ P.root.injective <| by simp [h]⟩
+  ext x
+  exact (P.reflection_perm_eq_reflection_perm_iff_of_span i j).mp h x <| by simp
+
 /-- The Coxeter Weight of a pair gives the weight of an edge in a Coxeter diagram, when it is
 finite.  It is `4 cos² θ`, where `θ` describes the dihedral angle between hyperplanes. -/
 def coxeterWeight : R := pairing P i j * pairing P j i