Existence of bases for crystallographic root systems #
Main results: #
RootPairing.Base.mk': an alternate constructor forRootPairing.Basewhich demands the axioms for roots but not for coroots.RootPairing.nonempty_base: base existence proof for reduced 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.
This is [serre1965](Ch. V, §9, Lemma 3).
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.
This is really just an auxiliary result en route to RootPairing.Base.mk'.
An alternate constructor for RootPairing.Base which demands the axioms for roots but not for
coroots.
Equations
- RootPairing.Base.mk' P s hli hsp = { support := ⋯.toFinset, linearIndepOn_root := ⋯, linearIndepOn_coroot := ⋯, root_mem_or_neg_mem := ⋯, coroot_mem_or_neg_mem := ⋯ }