feat(LinearAlgebra/RootSystem/Defs): Properties of pairs of roots (#10666)

Given a pair of roots, we can describe the "angle" between them using the pairing between root `i` and coroot `j` together with the reverse pairing.  This PR adds language for describing the various cases.



Co-authored-by: Oliver Nash <github@olivernash.org>

Author: ScottCarnahan

Mathlib/LinearAlgebra/RootSystem/Basic.lean

@@ -41,24 +41,43 @@ variable {ι R M N : Type*}
 
 namespace RootPairing
 
-variable (P : RootPairing ι R M N) (i : ι)
+variable (P : RootPairing ι R M N) (i j : ι)
+
+lemma root_ne (h: i ≠ j) : P.root i ≠ P.root j := by
+  simp_all only [ne_eq, EmbeddingLike.apply_eq_iff_eq, not_false_eq_true]
 
 lemma ne_zero [CharZero R] : (P.root i : M) ≠ 0 :=
   fun h ↦ by simpa [h] using P.root_coroot_two i
 
 lemma ne_zero' [CharZero R] : (P.coroot i : N) ≠ 0 :=
   fun h ↦ by simpa [h] using P.root_coroot_two i
 
+@[simp]
+lemma root_coroot_eq_pairing :
+    P.toLin (P.root i) (P.coroot j) = P.pairing i j :=
+  rfl
+
+lemma coroot_root_eq_pairing :
+    P.toLin.flip (P.coroot i) (P.root j) = P.pairing j i := by
+  simp
+
+@[simp]
+lemma pairing_same : P.pairing i i = 2 := P.root_coroot_two i
+
 lemma coroot_root_two :
-    (P.toLin.flip (P.coroot i)) (P.root i) = 2 := by
-  rw [LinearMap.flip_apply, P.root_coroot_two i]
+    P.toLin.flip (P.coroot i) (P.root i) = 2 := by
+  simp
 
 @[simp] lemma flip_flip : P.flip.flip = P := rfl
 
 lemma reflection_apply (x : M) :
     P.reflection i x = x - (P.toLin x (P.coroot i)) • P.root i :=
   rfl
 
+lemma reflection_apply_root :
+    P.reflection i (P.root j) = P.root j - (P.pairing j i) • P.root i :=
+  rfl
+
 @[simp]
 lemma reflection_apply_self :
     P.reflection i (P.root i) = - P.root i :=
@@ -113,23 +132,57 @@ lemma reflection_dualMap_eq_coreflection :
   ext n m
   simp [coreflection_apply, reflection_apply, mul_comm (P.toLin m (P.coroot i))]
 
-variable [Finite ι]
+lemma reflection_mul (x : M) :
+    (P.reflection i * P.reflection j) x = P.reflection i (P.reflection j x) := rfl
+
+lemma isCrystallographic_iff :
+    P.IsCrystallographic ↔ ∀ i j, ∃ z : ℤ, z = P.pairing i j := by
+  rw [IsCrystallographic]
+  refine ⟨fun h i j ↦ ?_, fun h i _ ⟨j, hj⟩ ↦ ?_⟩
+  · simpa [AddSubgroup.mem_zmultiples_iff] using h i (mem_range_self j)
+  · simpa [← hj, AddSubgroup.mem_zmultiples_iff] using h i j
+
+lemma isReduced_iff : P.IsReduced ↔ ∀ (i j : ι), i ≠ j →
+    ¬ LinearIndependent R ![P.root i, P.root j] → P.root i = - P.root j := by
+  rw [IsReduced]
+  refine ⟨fun h i j hij hLin ↦ ?_, fun h i j hLin  ↦ ?_⟩
+  · specialize h i j hLin
+    simp_all only [ne_eq, EmbeddingLike.apply_eq_iff_eq, false_or]
+  · by_cases h' : i = j
+    · exact Or.inl (congrArg (⇑P.root) h')
+    · exact Or.inr (h i j h' hLin)
+
+section pairs
+
+lemma coxeterWeight_swap : coxeterWeight P i j = coxeterWeight P j i := by
+  simp only [coxeterWeight, mul_comm]
+
+lemma IsOrthogonal.symm : IsOrthogonal P i j ↔ IsOrthogonal P j i := by
+  simp only [IsOrthogonal, and_comm]
+
+lemma IsOrthogonal_comm (h : IsOrthogonal P i j) : Commute (P.reflection i) (P.reflection j) := by
+  rw [Commute, SemiconjBy]
+  ext v
+  simp_all only [IsOrthogonal, reflection_mul, reflection_apply, smul_sub]
+  simp_all only [map_sub, map_smul, LinearMap.sub_apply, LinearMap.smul_apply,
+    root_coroot_eq_pairing, smul_eq_mul, mul_zero, sub_zero]
+  exact sub_right_comm v ((P.toLin v) (P.coroot j) • P.root j)
+      ((P.toLin v) (P.coroot i) • P.root i)
+
+end pairs
 
-/-- Even though the roots may not span, coroots are distinguished by their pairing with the
-roots. The proof depends crucially on the fact that there are finitely-many roots.
+variable [Finite ι]
 
-Modulo trivial generalisations, this statement is exactly Lemma 1.1.4 on page 87 of SGA 3 XXI.
-See also `RootPairing.injOn_dualMap_subtype_span_root_coroot` for a more useful restatement. -/
-lemma eq_of_forall_coroot_root_eq [NoZeroSMulDivisors ℤ M] (i j : ι)
-    (h : ∀ k, P.toLin (P.root k) (P.coroot i) = P.toLin (P.root k) (P.coroot j)) :
+lemma eq_of_pairing_pairing_eq_two [NoZeroSMulDivisors ℤ M] (i j : ι)
+    (hij : P.pairing i j = 2) (hji : P.pairing j i = 2) :
     i = j := by
   set α := P.root i
   set β := P.root j
   set sα : M ≃ₗ[R] M := P.reflection i
   set sβ : M ≃ₗ[R] M := P.reflection j
   set sαβ : M ≃ₗ[R] M := sβ.trans sα
-  have hα : sα β = β - (2 : R) • α := by rw [P.reflection_apply, h j, P.root_coroot_two j]
-  have hβ : sβ α = α - (2 : R) • β := by rw [P.reflection_apply, ← h i, P.root_coroot_two i]
+  have hα : sα β = β - (2 : R) • α := by rw [P.reflection_apply_root, hji]
+  have hβ : sβ α = α - (2 : R) • β := by rw [P.reflection_apply_root, hij]
   have hb : BijOn sαβ (range P.root) (range P.root) :=
     (P.bijOn_reflection_root i).comp (P.bijOn_reflection_root j)
   set f : ℕ → M := fun n ↦ β + (2 * n : ℤ) • (α - β)
@@ -149,11 +202,17 @@ lemma eq_of_forall_coroot_root_eq [NoZeroSMulDivisors ℤ M] (i j : ι)
     sub_eq_zero] at hnm
   linarith [hnm.resolve_right (P.root.injective.ne this)]
 
+/-- Even though the roots may not span, coroots are distinguished by their pairing with the
+roots. The proof depends crucially on the fact that there are finitely-many roots.
+
+Modulo trivial generalisations, this statement is exactly Lemma 1.1.4 on page 87 of SGA 3 XXI. -/
 lemma injOn_dualMap_subtype_span_root_coroot [NoZeroSMulDivisors ℤ M] :
     InjOn ((span R (range P.root)).subtype.dualMap ∘ₗ P.toLin.flip) (range P.coroot) := by
   rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩ hij
   congr
-  refine P.eq_of_forall_coroot_root_eq i j fun k ↦ ?_
+  suffices ∀ k, P.pairing k i = P.pairing k j from
+    P.eq_of_pairing_pairing_eq_two i j (by simp [← this i]) (by simp [this j])
+  intro k
   simpa using LinearMap.congr_fun hij ⟨P.root k, Submodule.subset_span (mem_range_self k)⟩
 
 /-- In characteristic zero if there is no torsion, the correspondence between roots and coroots is

Mathlib/LinearAlgebra/RootSystem/Defs.lean

@@ -28,9 +28,9 @@ This file contains basic definitions for root systems and root data.
 ## Todo
 
 * Introduce the Weyl Group
-* Coxeter weights of pairs
-* Properties of pairs of roots, e.g., parallel, ultraparallel, definite, orthogonal, imaginary,
-non-symmetrizable
+* Base change of root pairings.
+* Isomorphism of root pairings.
+* Crystallographic root systems are isomorphic to base changes of root systems over ℤ?
 
 ## Implementation details
 
@@ -110,9 +110,10 @@ always an integer.-/
 def IsCrystallographic : Prop :=
   ∀ i, MapsTo (P.toLin (P.root i)) (range P.coroot) (zmultiples (1 : R))
 
-/-- A root pairing is said to be reduced if it never contains the double of a root.-/
+/-- A root pairing is said to be reduced if any linearly dependent pair of roots is related by a
+sign. -/
 def IsReduced : Prop :=
-  ∀ i, 2 • P.root i ∉ range P.root
+  ∀ i j, ¬ LinearIndependent R ![P.root i, P.root j] → (P.root i = P.root j ∨ P.root i = - P.root j)
 
 /-- If we interchange the roles of `M` and `N`, we still have a root pairing. -/
 protected def flip : RootPairing ι R N M :=
@@ -130,3 +131,17 @@ def reflection : M ≃ₗ[R] M :=
 /-- The reflection associated to a coroot. -/
 def coreflection : N ≃ₗ[R] N :=
   Module.reflection (P.root_coroot_two i)
+
+section pairs
+
+variable (j : ι)
+
+/-- This is the pairing between roots and coroots. -/
+def pairing : R := P.toLin (P.root i) (P.coroot j)
+
+/-- 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
+
+/-- Two roots are orthogonal when they are fixed by each others' reflections. -/
+def IsOrthogonal : Prop := pairing P i j = 0 ∧ pairing P j i = 0