From 80283e82493b544a6a60aa1e61bb206268ee11f5 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Fri, 17 Jan 2025 18:44:04 +0000 Subject: [PATCH] feat: define bases of root pairings (#20667) --- Mathlib.lean | 1 + Mathlib/LinearAlgebra/RootSystem/Base.lean | 214 +++++++++++++++++++++ Mathlib/LinearAlgebra/RootSystem/Defs.lean | 47 +++++ 3 files changed, 262 insertions(+) create mode 100644 Mathlib/LinearAlgebra/RootSystem/Base.lean diff --git a/Mathlib.lean b/Mathlib.lean index 4a69dea48edc2..4ac20c6ec4516 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3573,6 +3573,7 @@ import Mathlib.LinearAlgebra.Quotient.Defs import Mathlib.LinearAlgebra.Quotient.Pi import Mathlib.LinearAlgebra.Ray import Mathlib.LinearAlgebra.Reflection +import Mathlib.LinearAlgebra.RootSystem.Base import Mathlib.LinearAlgebra.RootSystem.Basic import Mathlib.LinearAlgebra.RootSystem.Defs import Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear diff --git a/Mathlib/LinearAlgebra/RootSystem/Base.lean b/Mathlib/LinearAlgebra/RootSystem/Base.lean new file mode 100644 index 0000000000000..e21237212ee01 --- /dev/null +++ b/Mathlib/LinearAlgebra/RootSystem/Base.lean @@ -0,0 +1,214 @@ +/- +Copyright (c) 2025 Oliver Nash. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Oliver Nash +-/ +import Mathlib.LinearAlgebra.RootSystem.Defs + +/-! +# Bases for root pairings / systems + +This file contains a theory of bases for root pairings / systems. + +## Implementation details + +For reduced root pairings `RootSystem.Base` is equivalent to the usual definition appearing in the +informal literature (e.g., it follows from [serre1965](Ch. V, §8, Proposition 7) that +`RootSystem.Base` is equivalent to both [serre1965](Ch. V, §8, Definition 5) and +[bourbaki1968](Ch. VI, §1.5) for reduced pairings). However for non-reduced root pairings, it is +more restrictive because it includes axioms on coroots as well as on roots. For example by +`RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem` it is clear that the 1-dimensional +root system `{-2, -1, 0, 1, 2} ⊆ ℝ` has no base in the sense of `RootSystem.Base`. + +It is also worth remembering that it is only for reduced root systems that one has the simply +transitive action of the Weyl group on the set of bases, and that the Weyl group of a non-reduced +root system is the same as that of the reduced root system obtained by passing to the indivisible +roots. + +For infinite root systems, `RootSystem.Base` is usually not the right notion: linear independence +is too strong. + +## Main definitions / results: + * `RootSystem.Base`: a base of a root pairing. + +## TODO + + * Develop a theory of base / separation / positive roots for infinite systems which specialises to + the concept here for finite systems. + +-/ + +noncomputable section + +open Function Set Submodule + +variable {ι R M N : Type*} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] + +namespace RootPairing + +/-- A base of a root pairing. + +For reduced root pairings this definition is equivalent to the usual definition appearing in the +informal literature but not for non-reduced root pairings it is more restrictive. See the module +doc string for further remarks. -/ +structure Base (P : RootPairing ι R M N) where + /-- The set of roots / coroots belonging to the base. -/ + support : Set ι + linInd_root : LinearIndependent R fun i : support ↦ P.root i + linInd_coroot : LinearIndependent R fun i : support ↦ P.coroot i + root_mem_or_neg_mem (i : ι) : P.root i ∈ AddSubmonoid.closure (P.root '' support) ∨ + - P.root i ∈ AddSubmonoid.closure (P.root '' support) + coroot_mem_or_neg_mem (i : ι) : P.coroot i ∈ AddSubmonoid.closure (P.coroot '' support) ∨ + - P.coroot i ∈ AddSubmonoid.closure (P.coroot '' support) + +namespace Base + +section RootPairing + +variable {P : RootPairing ι R M N} (b : P.Base) + +/-- Interchanging roots and coroots, one still has a base of a root pairing. -/ +@[simps] protected def flip : + P.flip.Base where + support := b.support + linInd_root := b.linInd_coroot + linInd_coroot := b.linInd_root + root_mem_or_neg_mem := b.coroot_mem_or_neg_mem + coroot_mem_or_neg_mem := b.root_mem_or_neg_mem + +lemma root_mem_span_int (i : ι) : + P.root i ∈ span ℤ (P.root '' b.support) := by + have := b.root_mem_or_neg_mem i + simp only [← span_nat_eq_addSubmonoid_closure, mem_toAddSubmonoid] at this + rw [← span_span_of_tower (R := ℕ)] + rcases this with hi | hi + · exact subset_span hi + · rw [← neg_mem_iff] + exact subset_span hi + +lemma coroot_mem_span_int (i : ι) : + P.coroot i ∈ span ℤ (P.coroot '' b.support) := + b.flip.root_mem_span_int i + +@[simp] +lemma span_int_root_support : + span ℤ (P.root '' b.support) = span ℤ (range P.root) := by + refine le_antisymm (span_mono <| image_subset_range _ _) (span_le.mpr ?_) + rintro - ⟨i, rfl⟩ + exact b.root_mem_span_int i + +@[simp] +lemma span_int_coroot_support : + span ℤ (P.coroot '' b.support) = span ℤ (range P.coroot) := + b.flip.span_int_root_support + +@[simp] +lemma span_root_support : + span R (P.root '' b.support) = P.rootSpan := by + rw [← span_span_of_tower (R := ℤ), span_int_root_support, span_span_of_tower] + +@[simp] +lemma span_coroot_support : + span R (P.coroot '' b.support) = P.corootSpan := + b.flip.span_root_support + +open Finsupp in +lemma eq_one_or_neg_one_of_mem_support_of_smul_mem_aux [Finite ι] + [NoZeroSMulDivisors ℤ M] [NoZeroSMulDivisors ℤ N] + (i : ι) (h : i ∈ b.support) (t : R) (ht : t • P.root i ∈ range P.root) : + ∃ z : ℤ, z * t = 1 := by + classical + have : Fintype ι := Fintype.ofFinite ι + obtain ⟨j, hj⟩ := ht + obtain ⟨f, hf⟩ : ∃ f : b.support → ℤ, P.coroot i = ∑ i, (t * f i) • P.coroot i := by + have : P.coroot j ∈ span ℤ (P.coroot '' b.support) := b.coroot_mem_span_int j + rw [image_eq_range, mem_span_range_iff_exists_fun] at this + refine this.imp fun f hf ↦ ?_ + simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf, + coroot_eq_smul_coroot_iff.mpr hj] + use f ⟨i, h⟩ + replace hf : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k) + (t • (linearEquivFunOnFinite R _ _).symm (fun x ↦ (f x : R))) := by + rw [map_smul, linearCombination_eq_fintype_linearCombination_apply R R, + Fintype.linearCombination_apply, hf] + simp_rw [mul_smul, ← Finset.smul_sum] + let g : b.support →₀ R := single ⟨i, h⟩ 1 + have hg : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k) g := by simp [g] + rw [hg] at hf + have : Injective (linearCombination R fun k : b.support ↦ P.coroot k) := b.linInd_coroot + simpa [g, linearEquivFunOnFinite, mul_comm t] using (DFunLike.congr_fun (this hf) ⟨i, h⟩).symm + +lemma eq_one_or_neg_one_of_mem_support_of_smul_mem [Finite ι] [CharZero R] + [NoZeroSMulDivisors ℤ M] [NoZeroSMulDivisors ℤ N] + (i : ι) (h : i ∈ b.support) (t : R) (ht : t • P.root i ∈ range P.root) : + t = 1 ∨ t = - 1 := by + obtain ⟨z, hz⟩ := b.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux i h t ht + obtain ⟨s, hs⟩ := IsUnit.exists_left_inv <| isUnit_of_mul_eq_one_right _ t hz + replace ht : s • P.coroot i ∈ range P.coroot := by + obtain ⟨j, hj⟩ := ht + simpa only [coroot_eq_smul_coroot_iff.mpr hj, smul_smul, hs, one_smul] using mem_range_self j + obtain ⟨w, hw⟩ := b.flip.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux i h s ht + have : (z : R) * w = 1 := by + simpa [mul_mul_mul_comm _ t _ s, mul_comm t s, hs] using congr_arg₂ (· * ·) hz hw + suffices z = 1 ∨ z = - 1 by + rcases this with rfl | rfl + · left; simpa using hz + · right; simpa [neg_eq_iff_eq_neg] using hz + norm_cast at this + rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at this + tauto + +end RootPairing + +section RootSystem + +variable {P : RootSystem ι R M N} (b : P.Base) + +/-- A base of a root system yields a basis of the root space. -/ +@[simps!] def toWeightBasis : + Basis b.support R M := + Basis.mk b.linInd_root <| by + change ⊤ ≤ span R (range <| P.root ∘ ((↑) : b.support → ι)) + rw [top_le_iff, range_comp, Subtype.range_coe_subtype, setOf_mem_eq, b.span_root_support] + exact P.span_root_eq_top + +/-- A base of a root system yields a basis of the coroot space. -/ +def toCoweightBasis : + Basis b.support R N := + Base.toWeightBasis (P := P.flip) b.flip + +include b +variable [Fintype ι] + +lemma exists_root_eq_sum_nat_or_neg (i : ι) : + ∃ f : ι → ℕ, P.root i = ∑ j, f j • P.root j ∨ P.root i = - ∑ j, f j • P.root j := by + classical + simp_rw [← neg_eq_iff_eq_neg] + suffices ∀ m ∈ AddSubmonoid.closure (P.root '' b.support), ∃ f : ι → ℕ, m = ∑ j, f j • P.root j by + rcases b.root_mem_or_neg_mem i with hi | hi + · obtain ⟨f, hf⟩ := this _ hi + exact ⟨f, Or.inl hf⟩ + · obtain ⟨f, hf⟩ := this _ hi + exact ⟨f, Or.inr hf⟩ + intro m hm + refine AddSubmonoid.closure_induction ?_ ⟨0, by simp⟩ ?_ hm + · rintro - ⟨j, hj, rfl⟩ + exact ⟨Pi.single j 1, by simp [Pi.single_apply]⟩ + · intro _ _ _ _ ⟨f, hf⟩ ⟨g, hg⟩ + exact ⟨f + g, by simp [hf, hg, add_smul, Finset.sum_add_distrib]⟩ + +lemma exists_root_eq_sum_int (i : ι) : + ∃ f : ι → ℤ, (0 ≤ f ∨ f ≤ 0) ∧ P.root i = ∑ j, f j • P.root j := by + obtain ⟨f, hf | hf⟩ := b.exists_root_eq_sum_nat_or_neg i + · exact ⟨ Nat.cast ∘ f, Or.inl fun _ ↦ by simp, by simp [hf]⟩ + · exact ⟨- Nat.cast ∘ f, Or.inr fun _ ↦ by simp, by simp [hf]⟩ + +lemma exists_coroot_eq_sum_int (i : ι) : + ∃ f : ι → ℤ, (0 ≤ f ∨ f ≤ 0) ∧ P.coroot i = ∑ j, f j • P.coroot j := + b.flip.exists_root_eq_sum_int i (P := P.flip) + +end RootSystem + +end Base + +end RootPairing diff --git a/Mathlib/LinearAlgebra/RootSystem/Defs.lean b/Mathlib/LinearAlgebra/RootSystem/Defs.lean index eaaf04a6c7bfd..8b01626b5d947 100644 --- a/Mathlib/LinearAlgebra/RootSystem/Defs.lean +++ b/Mathlib/LinearAlgebra/RootSystem/Defs.lean @@ -150,6 +150,33 @@ protected def flip : RootPairing ι R N M := lemma flip_flip : P.flip.flip = P := rfl +variable (ι R M N) in +/-- `RootPairing.flip` as an equivalence. -/ +@[simps] def flipEquiv : RootPairing ι R N M ≃ RootPairing ι R M N where + toFun P := P.flip + invFun P := P.flip + left_inv _ := rfl + right_inv _ := rfl + +/-- If we interchange the roles of `M` and `N`, we still have a root system. -/ +protected def _root_.RootSystem.flip (P : RootSystem ι R M N) : RootSystem ι R N M := + { toRootPairing := P.toRootPairing.flip + span_root_eq_top := P.span_coroot_eq_top + span_coroot_eq_top := P.span_root_eq_top } + +@[simp] +protected lemma _root_.RootSystem.flip_flip (P : RootSystem ι R M N) : + P.flip.flip = P := + rfl + +variable (ι R M N) in +/-- `RootSystem.flip` as an equivalence. -/ +@[simps] def _root_.RootSystem.flipEquiv : RootSystem ι R N M ≃ RootSystem ι R M N where + toFun P := P.flip + invFun P := P.flip + left_inv _ := rfl + right_inv _ := rfl + /-- Roots written as functionals on the coweight space. -/ abbrev root' (i : ι) : Dual R N := P.toPerfectPairing (P.root i) @@ -385,6 +412,26 @@ lemma isReduced_iff : P.IsReduced ↔ ∀ i j : ι, i ≠ j → · exact Or.inl (congrArg P.root h') · exact Or.inr (h i j h' hLin) +variable {P} in +lemma smul_coroot_eq_of_root_eq_smul [Finite ι] [NoZeroSMulDivisors ℤ N] (i j : ι) (t : R) + (h : P.root j = t • P.root i) : + t • P.coroot j = P.coroot i := by + have hij : t * P.pairing i j = 2 := by simpa using ((P.coroot' j).congr_arg h).symm + refine Module.eq_of_mapsTo_reflection_of_mem (f := P.root' i) (g := P.root' i) + (finite_range P.coroot) (by simp [hij]) (by simp) (by simp [hij]) (by simp) ?_ + (P.mapsTo_coreflection_coroot i) (mem_range_self i) + convert P.mapsTo_coreflection_coroot j + ext x + replace h : P.root' j = t • P.root' i := by ext; simp [h, root'] + simp [Module.preReflection_apply, coreflection_apply, h, smul_comm _ t, mul_smul] + +variable {P} in +@[simp] lemma coroot_eq_smul_coroot_iff [Finite ι] [NoZeroSMulDivisors ℤ M] [NoZeroSMulDivisors ℤ N] + {i j : ι} {t : R} : + P.coroot i = t • P.coroot j ↔ P.root j = t • P.root i := + ⟨fun h ↦ (P.flip.smul_coroot_eq_of_root_eq_smul j i t h).symm, + fun h ↦ (P.smul_coroot_eq_of_root_eq_smul i j t h).symm⟩ + /-- The linear span of roots. -/ abbrev rootSpan := span R (range P.root)