feat: drop ordering assumption in RootPairing.coxeterWeight_mem_set_of_isCrystallographic (#21122)

Some of the required changes also allow us to unify (and generalise) the `RootPairing.IsAnisotropic` instances.

The means of obtaining these generalisations is to work with a root pairing with coefficients in `R` taking values in an ordered subring `S` (in the sense of `RootPairing.IsValuedIn`). This allows us to avoid assuming `R` is ordered, and includes the important case of a crystallographic pairing in characteristic zero.

The cost of this is that various definitions and lemmas need to be generalised to allow room for the subring `S` (implemented using an injective `algebra S R` structure). In particular the definition `RootPairing.IsRootPositive` becomes `RootPairing.RootPositiveForm` and has its API substantially reworked.

An alternative approach  to the headline result (taken in the informal literature) is to invoke `RootPairing.restrictScalarsRat` but this only works with field coefficients and does not provide the same unifications.

We also repair some doc strings (which did not have fully-qualified names, or had names which had drifted from the code).

Author: ocfnash

Mathlib/LinearAlgebra/BilinearMap.lean

@@ -429,6 +429,11 @@ noncomputable def restrictScalarsRange :
     k (restrictScalarsRange i j k hk B hB m n) = B (i m) (j n) := by
   simp [restrictScalarsRange]
 
+@[simp]
+lemma eq_restrictScalarsRange_iff (m : M') (n : N') (p : P') :
+    p = restrictScalarsRange i j k hk B hB m n ↔ k p = B (i m) (j n) := by
+  rw [← restrictScalarsRange_apply i j k hk B hB m n, hk.eq_iff]
+
 @[simp]
 lemma restrictScalarsRange_apply_eq_zero_iff (m : M') (n : N') :
     restrictScalarsRange i j k hk B hB m n = 0 ↔ B (i m) (j n) = 0 := by

Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

@@ -43,7 +43,7 @@ lemma cartanMatrixIn_def (i j : b.support) :
     b.cartanMatrixIn S i j = P.pairingIn S i j :=
   rfl
 
-variable [Nontrivial R] [NoZeroSMulDivisors S R]
+variable [FaithfulSMul S R]
 
 @[simp]
 lemma cartanMatrixIn_apply_same (i : b.support) :

Mathlib/LinearAlgebra/RootSystem/Defs.lean

@@ -406,9 +406,6 @@ lemma isValuedIn_iff_mem_range :
     P.IsValuedIn S ↔ ∀ i j, P.pairing i j ∈ range (algebraMap S R) := by
   simp only [isValuedIn_iff, mem_range]
 
-instance : P.IsValuedIn R where
-  exists_value := by simp
-
 instance [P.IsValuedIn S] : P.flip.IsValuedIn S := by
   rw [isValuedIn_iff, forall_comm]
   exact P.exists_value
@@ -417,7 +414,7 @@ instance [P.IsValuedIn S] : P.flip.IsValuedIn S := by
 coefficients.
 
 Note that it is uniquely-defined only when the map `S → R` is injective, i.e., when we have
-`[NoZeroSMulDivisors S R]`. -/
+`[FaithfulSMul S R]`. -/
 def pairingIn [P.IsValuedIn S] (i j : ι) : S :=
   (P.exists_value i j).choose
 
@@ -426,13 +423,35 @@ lemma algebraMap_pairingIn [P.IsValuedIn S] (i j : ι) :
     algebraMap S R (P.pairingIn S i j) = P.pairing i j :=
   (P.exists_value i j).choose_spec
 
+@[simp]
+lemma pairingIn_same [FaithfulSMul S R] [P.IsValuedIn S] (i : ι) :
+    P.pairingIn S i i = 2 :=
+  FaithfulSMul.algebraMap_injective S R <| by simp [map_ofNat]
+
 lemma IsValuedIn.trans (T : Type*) [CommRing T] [Algebra T S] [Algebra T R] [IsScalarTower T S R]
     [P.IsValuedIn T] :
     P.IsValuedIn S where
   exists_value i j := by
     use algebraMap T S (P.pairingIn T i j)
     simp [← RingHom.comp_apply, ← IsScalarTower.algebraMap_eq T S R]
 
+lemma coroot'_apply_apply_mem_of_mem_span [Module S M] [IsScalarTower S R M] [P.IsValuedIn S]
+    {x : M} (hx : x ∈ span S (range P.root)) (i : ι) :
+    P.coroot' i x ∈ range (algebraMap S R) := by
+  rw [show range (algebraMap S R) = LinearMap.range (Algebra.linearMap S R) from rfl]
+  induction hx using Submodule.span_induction with
+  | mem x hx =>
+    obtain ⟨k, rfl⟩ := hx
+    simpa using RootPairing.exists_value k i
+  | zero => simp
+  | add x y _ _ hx hy => simpa only [map_add] using add_mem hx hy
+  | smul t x _ hx => simpa only [LinearMap.map_smul_of_tower] using Submodule.smul_mem _ t hx
+
+lemma root'_apply_apply_mem_of_mem_span [Module S N] [IsScalarTower S R N] [P.IsValuedIn S]
+    {x : N} (hx : x ∈ span S (range P.coroot)) (i : ι) :
+    P.root' i x ∈ LinearMap.range (Algebra.linearMap S R) :=
+  P.flip.coroot'_apply_apply_mem_of_mem_span S hx i
+
 end IsValuedIn
 
 /-- A root pairing is said to be reduced if any linearly dependent pair of roots is related by a
@@ -582,7 +601,7 @@ lemma coxeterWeight_swap : coxeterWeight P i j = coxeterWeight P j i := by
 coefficients.
 
 Note that it is uniquely-defined only when the map `S → R` is injective, i.e., when we have
-`[NoZeroSMulDivisors S R]`. -/
+`[FaithfulSMul S R]`. -/
 def coxeterWeightIn (S : Type*) [CommRing S] [Algebra S R] [P.IsValuedIn S] (i j : ι) : S :=
   P.pairingIn S i j * P.pairingIn S j i
 

Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

@@ -19,16 +19,20 @@ Another application is to the faithfulness of the Weyl group action on roots, an
 Weyl group.
 
 ## Main definitions:
- * `Polarization`: A distinguished linear map from the weight space to the coweight space.
- * `RootForm` : The bilinear form on weight space corresponding to `Polarization`.
+ * `RootPairing.Polarization`: A distinguished linear map from the weight space to the coweight
+   space.
+ * `RootPairing.RootForm` : The bilinear form on weight space corresponding to `Polarization`.
 
 ## Main results:
- * `polarization_self_sum_of_squares` : The inner product of any weight vector is a sum of squares.
- * `rootForm_reflection_reflection_apply` : `RootForm` is invariant with respect
+ * `RootPairing.rootForm_self_sum_of_squares` : The inner product of any
+   weight vector is a sum of squares.
+ * `RootPairing.rootForm_reflection_reflection_apply` : `RootForm` is invariant with respect
    to reflections.
- * `rootForm_self_smul_coroot`: The inner product of a root with itself times the
-   corresponding coroot is equal to two times Polarization applied to the root.
- * `rootForm_self_non_neg`: `RootForm` is positive semidefinite.
+ * `RootPairing.rootForm_self_smul_coroot`: The inner product of a root with itself
+   times the corresponding coroot is equal to two times Polarization applied to the root.
+ * `RootPairing.exists_ge_zero_eq_rootForm`: `RootForm` is positive semidefinite.
+ * `RootPairing.coxeterWeight_mem_set_of_isCrystallographic`: the Coxeter weights belongs to the
+   set `{0, 1, 2, 3, 4}`.
 
 ## References:
  * [N. Bourbaki, *Lie groups and Lie algebras. Chapters 4--6*][bourbaki1968]
@@ -37,8 +41,6 @@ Weyl group.
 ## TODO (possibly in other files)
  * Weyl-invariance
  * Faithfulness of Weyl group action, and finiteness of Weyl group, for finite root systems.
- * Relation to Coxeter weight.  In particular, positivity constraints for finite root pairings mean
-  we restrict to weights between 0 and 4.
 -/
 
 open Set Function
@@ -51,11 +53,13 @@ variable {ι R M N : Type*}
 
 namespace RootPairing
 
-section CommRing
-
-variable [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
+variable [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
   (P : RootPairing ι R M N)
 
+section Fintype
+
+variable [Fintype ι]
+
 instance : Module.Finite R P.rootSpan := Finite.span_of_finite R <| finite_range P.root
 
 instance : Module.Finite R P.corootSpan := Finite.span_of_finite R <| finite_range P.coroot
@@ -166,6 +170,16 @@ lemma rootForm_self_smul_coroot (i : ι) :
   rw [Finset.sum_smul, add_neg_eq_zero.mpr rfl]
   exact sub_eq_zero_of_eq rfl
 
+lemma corootForm_self_smul_root (i : ι) :
+    (P.CorootForm (P.coroot i) (P.coroot i)) • P.root i = 2 • P.CoPolarization (P.coroot i) :=
+  rootForm_self_smul_coroot (P.flip) i
+
+lemma four_nsmul_coPolarization_compl_polarization_apply_root (i : ι) :
+    (4 • P.CoPolarization ∘ₗ P.Polarization) (P.root i) =
+    (P.RootForm (P.root i) (P.root i) * P.CorootForm (P.coroot i) (P.coroot i)) • P.root i := by
+  rw [LinearMap.smul_apply, LinearMap.comp_apply, show 4 = 2 * 2 from rfl, mul_smul, ← map_nsmul,
+    ← rootForm_self_smul_coroot, map_smul, smul_comm, ← corootForm_self_smul_root, smul_smul]
+
 lemma four_smul_rootForm_sq_eq_coxeterWeight_smul (i j : ι) :
     4 • (P.RootForm (P.root i) (P.root j)) ^ 2 = P.coxeterWeight i j •
       (P.RootForm (P.root i) (P.root i) * P.RootForm (P.root j) (P.root j)) := by
@@ -183,10 +197,6 @@ lemma four_smul_rootForm_sq_eq_coxeterWeight_smul (i j : ι) :
     map_smul, ← pairing, smul_eq_mul, smul_eq_mul, smul_eq_mul, coxeterWeight]
   ring
 
-lemma corootForm_self_smul_root (i : ι) :
-    (P.CorootForm (P.coroot i) (P.coroot i)) • P.root i = 2 • P.CoPolarization (P.coroot i) :=
-  rootForm_self_smul_coroot (P.flip) i
-
 lemma rootForm_self_sum_of_squares (x : M) :
     IsSumSq (P.RootForm x x) :=
   P.rootForm_apply_apply x x ▸ IsSumSq.sum_mul_self Finset.univ _
@@ -226,57 +236,86 @@ lemma prod_rootForm_smul_coroot_mem_range_domRestrict (i : ι) :
   use ⟨(c • 2 • P.root i), by aesop⟩
   simp
 
-end CommRing
-
-section LinearOrderedCommRing
+end Fintype
 
-variable [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N]
-  [Module R N] (P : RootPairing ι R M N)
+section IsValuedInOrdered
 
-theorem rootForm_self_non_neg (x : M) : 0 ≤ P.RootForm x x :=
-  IsSumSq.nonneg (P.rootForm_self_sum_of_squares x)
+variable (S : Type*) [LinearOrderedCommRing S] [Algebra S R] [FaithfulSMul S R]
+  [Module S M] [IsScalarTower S R M] [P.IsValuedIn S]
 
-lemma rootForm_self_eq_zero_iff {x : M} :
-    P.RootForm x x = 0 ↔ x ∈ LinearMap.ker P.RootForm :=
-  P.RootForm.apply_apply_same_eq_zero_iff P.rootForm_self_non_neg P.rootForm_symmetric
-
-lemma rootForm_root_self_pos (i : ι) :
-    0 < P.RootForm (P.root i) (P.root i) := by
-  simp only [rootForm_apply_apply]
-  exact Finset.sum_pos' (fun j _ ↦ mul_self_nonneg _) ⟨i, by simp⟩
+/-- The bilinear form of a finite root pairing taking values in a linearly-ordered ring, as a
+root-positive form. -/
+def posRootForm [Fintype ι] : P.RootPositiveForm S where
+  form := P.RootForm
+  symm := P.rootForm_symmetric
+  isOrthogonal_reflection := P.rootForm_reflection_reflection_apply
+  exists_eq i j := ⟨∑ k, P.pairingIn S i k * P.pairingIn S j k, by simp [rootForm_apply_apply]⟩
+  exists_pos_eq i := by
+    refine ⟨∑ k, P.pairingIn S i k ^ 2, ?_, by simp [sq, rootForm_apply_apply]⟩
+    exact Finset.sum_pos' (fun j _ ↦ sq_nonneg _) ⟨i, by simp⟩
+
+theorem exists_ge_zero_eq_rootForm [Fintype ι] (x : M) (hx : x ∈ span S (range P.root)) :
+    ∃ s ≥ 0, algebraMap S R s = P.RootForm x x := by
+  refine ⟨(P.posRootForm S).posForm ⟨x, hx⟩ ⟨x, hx⟩, IsSumSq.nonneg ?_, by simp [posRootForm]⟩
+  choose s hs using P.coroot'_apply_apply_mem_of_mem_span S hx
+  suffices (P.posRootForm S).posForm ⟨x, hx⟩ ⟨x, hx⟩ = ∑ i, s i * s i from
+    this ▸ IsSumSq.sum_mul_self Finset.univ s
+  apply FaithfulSMul.algebraMap_injective S R
+  simp only [posRootForm, RootPositiveForm.algebraMap_posForm, map_sum, map_mul]
+  simp [← Algebra.linearMap_apply, hs, rootForm_apply_apply]
 
 /-- SGA3 XXI Prop. 2.3.1 -/
-lemma coxeterWeight_le_four (i j : ι) : P.coxeterWeight i j ≤ 4 := by
-  set li := P.RootForm (P.root i) (P.root i)
-  set lj := P.RootForm (P.root j) (P.root j)
-  set lij := P.RootForm (P.root i) (P.root j)
-  have hi := P.rootForm_root_self_pos i
-  have hj := P.rootForm_root_self_pos j
+lemma coxeterWeightIn_le_four [Finite ι] (i j : ι) :
+    P.coxeterWeightIn S i j ≤ 4 := by
+  have : Fintype ι := Fintype.ofFinite ι
+  let ri : span S (range P.root) := ⟨P.root i, Submodule.subset_span (mem_range_self _)⟩
+  let rj : span S (range P.root) := ⟨P.root j, Submodule.subset_span (mem_range_self _)⟩
+  set li := (P.posRootForm S).posForm ri ri
+  set lj := (P.posRootForm S).posForm rj rj
+  set lij := (P.posRootForm S).posForm ri rj
+  obtain ⟨si, hsi, hsi'⟩ := (P.posRootForm S).exists_pos_eq i
+  obtain ⟨sj, hsj, hsj'⟩ := (P.posRootForm S).exists_pos_eq j
+  replace hsi' : si = li := FaithfulSMul.algebraMap_injective S R <| by simpa [li] using hsi'
+  replace hsj' : sj = lj := FaithfulSMul.algebraMap_injective S R <| by simpa [lj] using hsj'
+  rw [hsi'] at hsi
+  rw [hsj'] at hsj
   have cs : 4 * lij ^ 2 ≤ 4 * (li * lj) := by
     rw [mul_le_mul_left four_pos]
-    exact LinearMap.BilinForm.apply_sq_le_of_symm P.RootForm P.rootForm_self_non_neg
-      P.rootForm_symmetric (P.root i) (P.root j)
-  have key : 4 • lij ^ 2 = _ • (li * lj) := P.four_smul_rootForm_sq_eq_coxeterWeight_smul i j
+    refine (P.posRootForm S).posForm.apply_sq_le_of_symm ?_ (P.posRootForm S).isSymm_posForm ri rj
+    intro x
+    obtain ⟨s, hs, hs'⟩ := P.exists_ge_zero_eq_rootForm S x x.property
+    change _ = (P.posRootForm S).form x x at hs'
+    rw [(P.posRootForm S).algebraMap_apply_eq_form_iff] at hs'
+    rwa [← hs']
+  have key : 4 • lij ^ 2 = P.coxeterWeightIn S i j • (li * lj) := by
+    apply FaithfulSMul.algebraMap_injective S R
+    simpa [map_ofNat, lij, posRootForm, ri, rj, li, lj] using
+       P.four_smul_rootForm_sq_eq_coxeterWeight_smul i j
   simp only [nsmul_eq_mul, smul_eq_mul, Nat.cast_ofNat] at key
   rwa [key, mul_le_mul_right (by positivity)] at cs
 
-instance instIsRootPositiveRootForm : IsRootPositive P P.RootForm where
-  zero_lt_apply_root i := P.rootForm_root_self_pos i
-  symm := P.rootForm_symmetric
-  apply_reflection_eq := P.rootForm_reflection_reflection_apply
+variable [Finite ι] [P.IsCrystallographic] [CharZero R] (i j : ι)
 
-lemma coxeterWeight_mem_set_of_isCrystallographic (i j : ι) [P.IsCrystallographic] :
-    P.coxeterWeight i j ∈ ({0, 1, 2, 3, 4} : Set R) := by
-  obtain ⟨n, hcn⟩ : ∃ n : ℕ, P.coxeterWeight i j = n := by
+lemma coxeterWeightIn_mem_set_of_isCrystallographic :
+    P.coxeterWeightIn ℤ i j ∈ ({0, 1, 2, 3, 4} : Set ℤ) := by
+  have : Fintype ι := Fintype.ofFinite ι
+  obtain ⟨n, hcn⟩ : ∃ n : ℕ, P.coxeterWeightIn ℤ i j = n := by
     have : 0 ≤ P.coxeterWeightIn ℤ i j := by
-      simpa [← P.algebraMap_coxeterWeightIn ℤ] using P.coxeterWeight_non_neg P.RootForm i j
+      simpa only [P.algebraMap_coxeterWeightIn] using P.coxeterWeight_nonneg (P.posRootForm ℤ) i j
     obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le this
     exact ⟨n, by simp [← P.algebraMap_coxeterWeightIn ℤ, hn]⟩
-  have : P.coxeterWeight i j ≤ 4 := P.coxeterWeight_le_four i j
+  have : P.coxeterWeightIn ℤ i j ≤ 4 := P.coxeterWeightIn_le_four ℤ i j
   simp only [hcn, mem_insert_iff, mem_singleton_iff] at this ⊢
   norm_cast at this ⊢
   omega
 
-end LinearOrderedCommRing
+lemma coxeterWeight_mem_set_of_isCrystallographic :
+    P.coxeterWeight i j ∈ ({0, 1, 2, 3, 4} : Set R) := by
+  have := (FaithfulSMul.algebraMap_injective ℤ R).mem_set_image.mpr <|
+    P.coxeterWeightIn_mem_set_of_isCrystallographic i j
+  rw [algebraMap_coxeterWeightIn] at this
+  simpa [eq_comm] using this
+
+end IsValuedInOrdered
 
 end RootPairing

Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

@@ -42,8 +42,7 @@ Weyl group.
 ## Todo
  * Weyl-invariance of `RootForm` and `CorootForm`
  * Faithfulness of Weyl group perm action, and finiteness of Weyl group, over ordered rings.
- * Relation to Coxeter weight.  In particular, positivity constraints for finite root pairings mean
-  we restrict to weights between 0 and 4.
+ * Relation to Coxeter weight.
 -/
 
 noncomputable section
@@ -74,24 +73,15 @@ instance [P.IsAnisotropic] : P.flip.IsAnisotropic where
   rootForm_root_ne_zero := IsAnisotropic.corootForm_coroot_ne_zero
   corootForm_coroot_ne_zero := IsAnisotropic.rootForm_root_ne_zero
 
-/-- An auxiliary lemma en route to `RootPairing.instIsAnisotropicOfIsCrystallographic`. -/
-private lemma rootForm_root_ne_zero_aux [CharZero R] [P.IsCrystallographic] (i : ι) :
-    P.RootForm (P.root i) (P.root i) ≠ 0 := by
-  choose z hz using P.exists_value (S := ℤ) i
-  simp_rw [algebraMap_int_eq, Int.coe_castRingHom] at hz
-  simp only [rootForm_apply_apply, PerfectPairing.flip_apply_apply, root_coroot_eq_pairing, ← hz]
-  suffices 0 < ∑ i, z i * z i by norm_cast; exact this.ne'
-  refine Finset.sum_pos' (fun i _ ↦ mul_self_nonneg (z i)) ⟨i, Finset.mem_univ i, ?_⟩
-  have hzi : z i = 2 := by
-    specialize hz i
-    rw [pairing_same] at hz
-    norm_cast at hz
-  simp [hzi]
+lemma isAnisotropic_of_isValuedIn (S : Type*)
+    [LinearOrderedCommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] :
+    IsAnisotropic P where
+  rootForm_root_ne_zero i := (P.posRootForm S).form_apply_root_ne_zero i
+  corootForm_coroot_ne_zero i := (P.flip.posRootForm S).form_apply_root_ne_zero i
 
 instance instIsAnisotropicOfIsCrystallographic [CharZero R] [P.IsCrystallographic] :
-    IsAnisotropic P where
-  rootForm_root_ne_zero := P.rootForm_root_ne_zero_aux
-  corootForm_coroot_ne_zero := P.flip.rootForm_root_ne_zero_aux
+    IsAnisotropic P :=
+  P.isAnisotropic_of_isValuedIn ℤ
 
 end CommRing
 
@@ -224,16 +214,23 @@ section LinearOrderedCommRing
 
 variable [LinearOrderedCommRing R] [Module R M] [Module R N] (P : RootPairing ι R M N)
 
-instance instIsAnisotropicOfLinearOrderedCommRing : IsAnisotropic P where
-  rootForm_root_ne_zero i := (P.rootForm_root_self_pos i).ne'
-  corootForm_coroot_ne_zero i := (P.flip.rootForm_root_self_pos i).ne'
+instance instIsAnisotropicOfLinearOrderedCommRing : IsAnisotropic P :=
+  P.isAnisotropic_of_isValuedIn R
+
+lemma zero_le_rootForm (x : M) :
+    0 ≤ P.RootForm x x :=
+  (P.rootForm_self_sum_of_squares x).nonneg
 
 /-- See also `RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic`. -/
 lemma rootForm_restrict_nondegenerate_of_ordered :
     LinearMap.Nondegenerate (P.RootForm.restrict P.rootSpan) :=
-  (P.RootForm.nondegenerate_restrict_iff_disjoint_ker (rootForm_self_non_neg P)
+  (P.RootForm.nondegenerate_restrict_iff_disjoint_ker P.zero_le_rootForm
     P.rootForm_symmetric).mpr P.disjoint_rootSpan_ker_rootForm
 
+lemma rootForm_self_eq_zero_iff {x : M} :
+    P.RootForm x x = 0 ↔ x ∈ LinearMap.ker P.RootForm :=
+  P.RootForm.apply_apply_same_eq_zero_iff P.zero_le_rootForm P.rootForm_symmetric
+
 lemma eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero {x : M}
     (hx : x ∈ P.rootSpan) (hx' : P.RootForm x x = 0) :
     x = 0 := by
@@ -242,7 +239,7 @@ lemma eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero {x : M}
 
 lemma rootForm_pos_of_ne_zero {x : M} (hx : x ∈ P.rootSpan) (h : x ≠ 0) :
     0 < P.RootForm x x := by
-  apply (P.rootForm_self_non_neg x).lt_of_ne
+  apply (P.zero_le_rootForm x).lt_of_ne
   contrapose! h
   exact P.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero hx h.symm