[Merged by Bors] - feat (LinearAlgebra/RootSystem/Finite): nondegeneracy of canonical bilinear form restricted to root span

Mathlib.lean

@@ -3342,6 +3342,7 @@ import Mathlib.LinearAlgebra.Reflection
 import Mathlib.LinearAlgebra.RootSystem.Basic
 import Mathlib.LinearAlgebra.RootSystem.Defs
 import Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
+import Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
 import Mathlib.LinearAlgebra.RootSystem.Hom
 import Mathlib.LinearAlgebra.RootSystem.OfBilinear
 import Mathlib.LinearAlgebra.RootSystem.RootPairingCat

Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

@@ -95,7 +95,6 @@ lemma sum_sq_le_sq_sum_of_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) :
   · exact hf i hi
   · exact single_le_sum hf hi
 
-
 end OrderedSemiring
 
 section OrderedCommSemiring
@@ -142,6 +141,19 @@ lemma sum_mul_sq_le_sq_mul_sq (s : Finset ι) (f g : ι → R) :
         sum_le_sum fun i _ ↦ two_mul_le_add_sq (f i * ∑ j ∈ s, g j ^ 2) (g i * ∑ j ∈ s, f j * g j)
     _ = _ := by simp_rw [sum_add_distrib, mul_pow, ← sum_mul]; ring
 
+theorem sum_mul_self_eq_zero_iff (s : Finset ι) (f : ι → R) :
+    ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0 := by
+  induction s using Finset.cons_induction with
+  | empty => simp
+  | cons i s his ih =>
+    simp only [Finset.sum_cons, Finset.mem_cons, forall_eq_or_imp]
+    refine ⟨fun hc => ?_, fun h => by simpa [h.1] using ih.mpr h.2⟩
+    have hi : f i * f i ≤ 0 := by
+      rw [← hc, le_add_iff_nonneg_right]
+      exact Finset.sum_nonneg fun i _ ↦ mul_self_nonneg (f i)
+    have h : f i * f i = 0 := (eq_of_le_of_le (mul_self_nonneg (f i)) hi).symm
+    exact ⟨zero_eq_mul_self.mp h.symm, ih.mp (by rw [← hc, h, zero_add])⟩
+
 end LinearOrderedCommSemiring
 
 lemma abs_prod [LinearOrderedCommRing R] (s : Finset ι) (f : ι → R) :

Mathlib/LinearAlgebra/Dimension/Basic.lean

@@ -353,6 +353,13 @@ theorem rank_subsingleton [Subsingleton R] : Module.rank R M = 1 := by
     subsingleton
   · exact hw.trans_eq (Cardinal.mk_singleton _).symm
 
+lemma rank_le_of_smul_regular {S : Type*} [CommSemiring S] [Algebra S R] [Module S M]
+    [IsScalarTower S R M] (L L' : Submodule R M) {s : S} (hr : IsSMulRegular M s)
+    (h : ∀ x ∈ L, s • x ∈ L') :
+    Module.rank R L ≤ Module.rank R L' :=
+  ((Algebra.lsmul S R M s).restrict h).rank_le_of_injective <|
+    fun _ _ h ↦ by simpa using hr (Subtype.ext_iff.mp h)
+
 end
 
 end Module

Mathlib/LinearAlgebra/Dimension/RankNullity.lean

@@ -203,13 +203,23 @@ lemma Submodule.finrank_quotient_add_finrank [Module.Finite R M] (N : Submodule
     Submodule.finrank_eq_rank]
   exact HasRankNullity.rank_quotient_add_rank _
 
-
 /-- Rank-nullity theorem using `finrank` and subtraction. -/
 lemma Submodule.finrank_quotient [Module.Finite R M] {S : Type*} [Ring S] [SMul R S] [Module S M]
     [IsScalarTower R S M] (N : Submodule S M) : finrank R (M ⧸ N) = finrank R M - finrank R N := by
   rw [← (N.restrictScalars R).finrank_quotient_add_finrank]
   exact Nat.eq_sub_of_add_eq rfl
 
+lemma Submodule.disjoint_of_finrank_eq [NoZeroSMulDivisors R M] {N : Type*} [AddCommGroup N]
+    [Module R N] {L : Submodule R M} [Module.Finite R L] (f : M →ₗ[R] N)
+    (h : finrank R (L.map f) = finrank R L) :
+    Disjoint L (LinearMap.ker f) := by
+  refine disjoint_iff.mpr <| LinearMap.injective_domRestrict_iff.mp <| LinearMap.ker_eq_bot.mp <|
+    Submodule.rank_eq_zero.mp ?_
+  rw [← Submodule.finrank_eq_rank, Nat.cast_eq_zero]
+  rw [← LinearMap.range_domRestrict] at h
+  have := (LinearMap.ker (f.domRestrict L)).finrank_quotient_add_finrank
+  rwa [LinearEquiv.finrank_eq (f.domRestrict L).quotKerEquivRange, h, Nat.add_eq_left] at this
+
 end Finrank
 
 section

Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

@@ -465,4 +465,12 @@ theorem LinearMap.finrank_range_le [Module.Finite R M] (f : M →ₗ[R] M') :
     finrank R (LinearMap.range f) ≤ finrank R M :=
   finrank_le_finrank_of_rank_le_rank (lift_rank_range_le f) (rank_lt_aleph0 _ _)
 
+theorem LinearMap.finrank_le_of_smul_regular {S : Type*} [CommSemiring S] [Algebra S R] [Module S M]
+    [IsScalarTower S R M] (L L' : Submodule R M) [Module.Finite R L'] {s : S}
+    (hr : IsSMulRegular M s) (h : ∀ x ∈ L, s • x ∈ L') :
+    Module.finrank R L ≤ Module.finrank R L' := by
+  refine finrank_le_finrank_of_rank_le_rank (lift_le.mpr <| rank_le_of_smul_regular L L' hr h) ?_
+  rw [← Module.finrank_eq_rank R L']
+  exact nat_lt_aleph0 (finrank R ↥L')
+
 end StrongRankCondition

Mathlib/LinearAlgebra/Dual.lean

@@ -714,6 +714,17 @@ instance instFiniteDimensionalOfIsReflexive (K V : Type*)
     rw [lift_id']
   exact lt_trans h₁ h₂
 
+instance [IsDomain R] : NoZeroSMulDivisors R M := by
+  refine (noZeroSMulDivisors_iff R M).mpr ?_
+  intro r m hrm
+  by_cases hr : r = 0; · exact Or.inl hr
+  right
+  suffices Dual.eval R M m = Dual.eval R M 0 by exact (bijective_dual_eval R M).injective this
+  ext n
+  simp only [Dual.eval_apply, map_zero, LinearMap.zero_apply]
+  suffices r • n m = 0 by exact eq_zero_of_ne_zero_of_mul_left_eq_zero hr this
+  rw [← LinearMap.map_smul_of_tower, hrm, LinearMap.map_zero]
+
 end IsReflexive
 
 end Module

Mathlib/LinearAlgebra/RootSystem/Defs.lean

@@ -374,6 +374,12 @@ 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 linear span of roots. -/
+abbrev rootSpan := span R (range P.root)
+
+/-- The linear span of coroots. -/
+abbrev corootSpan := span R (range P.coroot)
+
 /-- 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) :=

Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

@@ -3,8 +3,9 @@ Copyright (c) 2024 Scott Carnahan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Carnahan
 -/
-import Mathlib.LinearAlgebra.RootSystem.Defs
+import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.Algebra.Ring.SumsOfSquares
+import Mathlib.LinearAlgebra.RootSystem.Defs
 
 /-!
 # The canonical bilinear form on a finite root pairing
@@ -22,16 +23,17 @@ Weyl group.
  * `Polarization`: A distinguished linear map from the weight space to the coweight space.
  * `RootForm` : The bilinear form on weight space corresponding to `Polarization`.
 
-## References:
- * SGAIII Exp. XXI
- * Bourbaki, Lie groups and Lie algebras
-
 ## 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
    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.
+
+## References:
+ * SGAIII Exp. XXI
+ * Bourbaki, Lie groups and Lie algebras
 
 ## TODO (possibly in other files)
  * Positivity and nondegeneracy
@@ -41,8 +43,9 @@ Weyl group.
   we restrict to weights between 0 and 4.
 -/
 
-open Function
+open Set Function
 open Module hiding reflection
+open Submodule (span)
 
 noncomputable section
 
@@ -132,6 +135,54 @@ lemma rootForm_root_self (j : ι) :
     P.RootForm (P.root j) (P.root j) = ∑ (i : ι), (P.pairing j i) * (P.pairing j i) := by
   simp [rootForm_apply_apply]
 
+theorem range_polarization_domRestrict_le_span_coroot :
+    LinearMap.range (P.Polarization.domRestrict P.rootSpan) ≤ P.corootSpan := by
+  intro y hy
+  obtain ⟨x, hx⟩ := hy
+  rw [← hx, LinearMap.domRestrict_apply, Polarization_apply]
+  refine (mem_span_range_iff_exists_fun R).mpr ?_
+  use fun i => (P.toPerfectPairing x) (P.coroot i)
+  simp
+
 end CommRing
 
+section LinearOrderedCommRing
+
+variable [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N]
+  [Module R N] (P : RootPairing ι R M N)
+
+theorem rootForm_self_non_neg (x : M) : 0 ≤ P.RootForm x x :=
+  IsSumSq.nonneg (P.rootForm_self_sum_of_squares x)
+
+theorem rootForm_self_zero_iff (x : M) :
+    P.RootForm x x = 0 ↔ ∀ i, P.coroot' i x = 0 := by
+  simp only [rootForm_apply_apply, PerfectPairing.toLin_apply, LinearMap.coe_comp, comp_apply,
+    Polarization_apply, map_sum, map_smul, smul_eq_mul]
+  convert Finset.sum_mul_self_eq_zero_iff Finset.univ fun i => P.coroot' i x
+  simp
+
+lemma rootForm_root_self_pos (j : ι) :
+    0 < P.RootForm (P.root j) (P.root j) := by
+  simp only [LinearMap.coe_mk, AddHom.coe_mk, LinearMap.coe_comp, comp_apply,
+    rootForm_apply_apply, toLin_toPerfectPairing]
+  refine Finset.sum_pos' (fun i _ => (sq (P.pairing j i)) ▸ sq_nonneg (P.pairing j i)) ?_
+  use j
+  simp
+
+lemma prod_rootForm_root_self_pos :
+    0 < ∏ i, P.RootForm (P.root i) (P.root i) :=
+  Finset.prod_pos fun i _ => rootForm_root_self_pos P i
+
+lemma prod_rootForm_smul_coroot_mem_range_domRestrict (i : ι) :
+    (∏ a : ι, P.RootForm (P.root a) (P.root a)) • P.coroot i ∈
+      LinearMap.range (P.Polarization.domRestrict (P.rootSpan)) := by
+  obtain ⟨c, hc⟩ := Finset.dvd_prod_of_mem (fun a ↦ P.RootForm (P.root a) (P.root a))
+    (Finset.mem_univ i)
+  rw [hc, mul_comm, mul_smul, rootForm_self_smul_coroot]
+  refine LinearMap.mem_range.mpr ?_
+  use ⟨(c • 2 • P.root i), by aesop⟩
+  simp
+
+end LinearOrderedCommRing
+
 end RootPairing

Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2024 Scott Carnahan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Carnahan
+-/
+import Mathlib.LinearAlgebra.BilinearForm.Basic
+import Mathlib.LinearAlgebra.Dimension.Localization
+import Mathlib.LinearAlgebra.QuadraticForm.Basic
+import Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
+import Mathlib.LinearAlgebra.RootSystem.RootPositive
+
+/-!
+# Nondegeneracy of the polarization on a finite root pairing
+We show that if the base ring of a finite root pairing is linearly ordered, then the canonical
+bilinear form is root-positive and positive-definite on the span of roots.
+From these facts, it is easy to show that Coxeter weights in a finite root pairing are bounded
+above by 4.  Thus, the pairings of roots and coroots in a root pairing are restricted to the
+interval `[-4, 4]`.  Furthermore, a linearly independent pair of roots cannot have Coxeter weight 4.
+For the case of crystallographic root pairings, we are thus reduced to a finite set of possible
+options for each pair.
+Another application is to the faithfulness of the Weyl group action on roots, and finiteness of the
+Weyl group.
+
+## Main results:
+ * `RootPairing.rootForm_rootPositive`: `RootForm` is root-positive.
+ * `RootPairing.polarization_domRestrict_injective`: The polarization restricted to the span of
+   roots is injective.
+ * `RootPairing.rootForm_pos_of_nonzero`: `RootForm` is strictly positive on non-zero linear
+  combinations of roots. This gives us a convenient way to eliminate certain Dynkin diagrams from
+  the classification, since it suffices to produce a nonzero linear combination of simple roots with
+  non-positive norm.
+
+## References:
+ * SGAIII Exp. XXI
+ * Bourbaki, Lie groups and Lie algebras
+
+## 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.
+-/
+
+noncomputable section
+
+open Set Function
+open Module hiding reflection
+open Submodule (span)
+
+namespace RootPairing
+
+variable {ι R M N : Type*}
+
+variable [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N]
+[Module R N] (P : RootPairing ι R M N)
+
+lemma rootForm_rootPositive : 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
+
+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
+
+@[simp]
+lemma finrank_rootSpan_map_polarization_eq_finrank_corootSpan :
+    finrank R (P.rootSpan.map P.Polarization) = finrank R P.corootSpan := by
+  rw [← LinearMap.range_domRestrict]
+  refine eq_of_le_of_le (Submodule.finrank_mono P.range_polarization_domRestrict_le_span_coroot) ?_
+  have : IsReflexive R N := PerfectPairing.reflexive_right P.toPerfectPairing
+  refine LinearMap.finrank_le_of_smul_regular P.corootSpan
+    (LinearMap.range (P.Polarization.domRestrict P.rootSpan))
+    (smul_right_injective N (Ne.symm (ne_of_lt P.prod_rootForm_root_self_pos)))
+    fun _ hx => ?_
+  obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun R).mp hx
+  rw [← hc, Finset.smul_sum]
+  simp_rw [smul_smul, mul_comm, ← smul_smul]
+  exact Submodule.sum_smul_mem (LinearMap.range (P.Polarization.domRestrict P.rootSpan)) c
+    (fun c _ ↦ prod_rootForm_smul_coroot_mem_range_domRestrict P c)
+
+/-- An auxiliary lemma en route to `RootPairing.finrank_corootSpan_eq`. -/
+private lemma finrank_corootSpan_le :
+    finrank R P.corootSpan ≤ finrank R P.rootSpan := by
+  rw [← finrank_rootSpan_map_polarization_eq_finrank_corootSpan]
+  exact Submodule.finrank_map_le P.Polarization P.rootSpan
+
+lemma finrank_corootSpan_eq :
+    finrank R P.corootSpan = finrank R P.rootSpan :=
+  le_antisymm P.finrank_corootSpan_le P.flip.finrank_corootSpan_le
+
+lemma disjoint_rootSpan_ker_polarization :
+    Disjoint P.rootSpan (LinearMap.ker P.Polarization) := by
+  have : IsReflexive R M := PerfectPairing.reflexive_left P.toPerfectPairing
+  refine Submodule.disjoint_of_finrank_eq (L := P.rootSpan) P.Polarization ?_
+  rw [finrank_rootSpan_map_polarization_eq_finrank_corootSpan, finrank_corootSpan_eq]
+
+lemma mem_ker_polarization_of_rootForm_self_eq_zero {x : M} (hx : P.RootForm x x = 0) :
+    x ∈ LinearMap.ker P.Polarization := by
+  rw [LinearMap.mem_ker, Polarization_apply]
+  rw [rootForm_self_zero_iff] at hx
+  exact Fintype.sum_eq_zero _ fun i ↦ by simp [hx i]
+
+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
+  rw [← Submodule.mem_bot (R := R), ← P.disjoint_rootSpan_ker_polarization.eq_bot]
+  exact ⟨hx, P.mem_ker_polarization_of_rootForm_self_eq_zero hx'⟩
+
+lemma _root_.RootSystem.rootFormAnisotropic (P : RootSystem ι R M N) :
+    P.RootForm.toQuadraticMap.Anisotropic := by
+  refine fun x ↦ P.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero ?_
+  rw [rootSpan, P.span_eq_top]
+  exact Submodule.mem_top
+
+lemma rootForm_pos_of_nonzero {x : M} (hx : x ∈ P.rootSpan) (h : x ≠ 0) :
+    0 < P.RootForm x x := by
+  refine lt_of_le_of_ne (P.rootForm_self_non_neg x) ?_
+  contrapose! h
+  exact eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero P hx h.symm
+
+lemma rootForm_restrict_nondegenerate :
+    (P.RootForm.restrict P.rootSpan).Nondegenerate :=
+  LinearMap.IsRefl.nondegenerate_of_separatingLeft (LinearMap.IsSymm.isRefl fun x y => by
+    simp [rootForm_apply_apply, mul_comm]) fun x h => SetLike.coe_eq_coe.mp
+    (P.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero (Submodule.coe_mem x) (h x))
+
+end RootPairing