Existence of bases for crystallographic root systems

Implementation details

The proof needs a set of ordered coefficients, even though the ultimate existence statement does not. There are at least two ways to deal with this: (a) Using the fact that a crystallographic root system induces a ℚ-structure, pass to the root system over ℚ defined by RootPairing.restrictScalarsRat, and develop a theory of base change for root system bases. (b) Introduce a second set of ordered coefficients (ultimately taken to be ℚ) and develop a theory with two sets of coefficients simultaneously in play.

It is not really clear which is the better approach but here we opt for approach (b) as it seems to yield slightly more general results.

TODO

1. Prove that for crystallographic reduced root systems, the axiom coroot_mem_or_neg_mem appearing in RootPairing.Base follows from the others, and combine this with RootPairing.linearIndepOn_coroot_iff to thus provide an alternate constructor for RootPairing.Base which demands only the hypotheses on the roots.
2. [Easy given 1 above] Prove that every reduced crystallographic root system has a base by combining the constructor in 1 above with RootPairing.linearIndepOn_root_baseOf, IsAddIndecomposable.mem_or_neg_mem_closure_baseOf, Module.exists_dual_forall_apply_ne_zero.

theorem RootPairing.baseOf_pairwise_pairing_le_zero {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (P : RootPairing ι R M N) {S : Type u_5} [LinearOrder S] [AddCommGroup S] [IsOrderedAddMonoid S] (f : M →+ S) [CharZero R] [IsDomain R] [P.IsCrystallographic] (hf : ∀ (i : ι), f (P.root i) ≠ 0) : (IsAddIndecomposable.baseOf (⇑P.root) f).Pairwise fun (i j : ι) => P.pairingIn ℤ i j ≤ 0

This is [Ser87](Ch. V, §9, Lemma 3).

theorem RootPairing.linearIndepOn_root_baseOf' {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (P : RootPairing ι R M N) [IsDomain R] {S : Type u_6} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [Module S N] [IsScalarTower S R N] [P.IsValuedIn S] [P.IsCrystallographic] (f : Module.Dual S M) (hf : ∀ (i : ι), f (P.root i) ≠ 0) : LinearIndepOn S (⇑P.root) (IsAddIndecomposable.baseOf ⇑P.root ↑f)

This lemma is usually established for root systems with coefficients R equal to ℚ or ℝ, in which case one may take S = R. However our statement allows for more general coefficients such as R = ℂ and S = ℚ.

This lemma is mostly a stepping stone en route to RootPairing.linearIndepOn_root_baseOf (where linear independence is established over R rather than just S) except that this version does not make the field assumption and so covers the case S = R = ℤ which the latter does not.

theorem RootPairing.linearIndepOn_root_baseOf {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [AddCommGroup M] [AddCommGroup N] [Field R] [CharZero R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsRootSystem] [P.IsCrystallographic] [Module ℚ M] [Module ℚ N] (f : Module.Dual ℚ M) (hf : ∀ (i : ι), f (P.root i) ≠ 0) : LinearIndepOn R (⇑P.root) (IsAddIndecomposable.baseOf ⇑P.root ↑f)

noncomputable def RootPairing.basisOfBase {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [Field R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsRootSystem] (s : Set ι) (hli : LinearIndepOn R (⇑P.root) s) (hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)) : Module.Basis (↑s) R M

A set of linearly independent roots whose cone span over ℕ contains all the roots is a basis for the ambient space.

Equations

• P.basisOfBase s hli hsp = Module.Basis.mk hli ⋯

theorem RootPairing.exists_dual_baseOf_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [AddCommGroup M] [AddCommGroup N] [Field R] [CharZero R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsRootSystem] [P.IsCrystallographic] [Module ℚ M] [Module ℚ N] (s : Set ι) (hli : LinearIndepOn R (⇑P.root) s) (hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)) : ∃ (f : Module.Dual ℚ M), IsAddIndecomposable.baseOf ⇑P.root ↑f = s ∧ ∀ i ∈ s, f (P.root i) = 1