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.IsAnisotropic: We say a finite root pairing is anisotropic if there are no roots / coroots which have length zero wrt the root / coroot forms.RootPairing.rootForm_pos_of_nonzero:RootFormis 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.RootPairing.rootForm_restrict_nondegenerate_of_ordered: The root form is non-degenerate if the coefficients are ordered.RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic: the root form is non-degenerate if the coefficients are a field and the pairing is crystallographic.
References: #
- N. Bourbaki, Lie groups and Lie algebras. Chapters 4--6
- M. Demazure, SGA III, Exposé XXI, Données Radicielles
Todo #
- Weyl-invariance of
RootFormandCorootForm - 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.
class
RootPairing.IsAnisotropic
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[CommRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
:
We say a finite root pairing is anisotropic if there are no roots / coroots which have length zero wrt the root / coroot forms.
Examples include crystallographic pairings in characteristic zero
RootPairing.instIsAnisotropicOfIsCrystallographic and pairings over ordered scalars.
RootPairing.instIsAnisotropicOfLinearOrderedCommRing.
- rootForm_root_ne_zero (i : ι) : (P.RootForm (P.root i)) (P.root i) ≠ 0
- corootForm_coroot_ne_zero (i : ι) : (P.CorootForm (P.coroot i)) (P.coroot i) ≠ 0
Instances
instance
RootPairing.instIsAnisotropicFlip
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[CommRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[P.IsAnisotropic]
:
P.flip.IsAnisotropic
instance
RootPairing.instIsAnisotropicOfIsCrystallographic
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[CommRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[CharZero R]
[P.IsCrystallographic]
:
P.IsAnisotropic
@[simp]
theorem
RootPairing.finrank_rootSpan_map_polarization_eq_finrank_corootSpan
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[CommRing R]
[IsDomain R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[P.IsAnisotropic]
:
Module.finrank R ↥(Submodule.map P.Polarization P.rootSpan) = Module.finrank R ↥P.corootSpan
theorem
RootPairing.finrank_corootSpan_eq
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[CommRing R]
[IsDomain R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[P.IsAnisotropic]
:
Module.finrank R ↥P.corootSpan = Module.finrank R ↥P.rootSpan
theorem
RootPairing.disjoint_rootSpan_ker_rootForm
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[CommRing R]
[IsDomain R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[P.IsAnisotropic]
:
Disjoint P.rootSpan (LinearMap.ker P.RootForm)
theorem
RootPairing.disjoint_corootSpan_ker_corootForm
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[CommRing R]
[IsDomain R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[P.IsAnisotropic]
:
Disjoint P.corootSpan (LinearMap.ker P.CorootForm)
theorem
RootPairing.isCompl_rootSpan_ker_rootForm
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[Field R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[P.IsAnisotropic]
:
IsCompl P.rootSpan (LinearMap.ker P.RootForm)
theorem
RootPairing.isCompl_corootSpan_ker_corootForm
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[Field R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[P.IsAnisotropic]
:
IsCompl P.corootSpan (LinearMap.ker P.CorootForm)
theorem
RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[Field R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[P.IsAnisotropic]
:
LinearMap.Nondegenerate (P.RootForm.restrict P.rootSpan)
See also RootPairing.rootForm_restrict_nondegenerate_of_ordered.
Note that this applies to crystallographic root systems in characteristic zero via
RootPairing.instIsAnisotropicOfIsCrystallographic.
@[simp]
theorem
RootPairing.orthogonal_rootSpan_eq
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[Field R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[P.IsAnisotropic]
:
P.RootForm.orthogonal P.rootSpan = LinearMap.ker P.RootForm
@[simp]
theorem
RootPairing.orthogonal_corootSpan_eq
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[Field R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[P.IsAnisotropic]
:
P.CorootForm.orthogonal P.corootSpan = LinearMap.ker P.CorootForm
instance
RootPairing.instIsAnisotropicOfLinearOrderedCommRing
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[LinearOrderedCommRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
:
P.IsAnisotropic
theorem
RootPairing.rootForm_restrict_nondegenerate_of_ordered
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[LinearOrderedCommRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
:
LinearMap.Nondegenerate (P.RootForm.restrict P.rootSpan)
See also RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic.
theorem
RootPairing.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[LinearOrderedCommRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
{x : M}
(hx : x ∈ P.rootSpan)
(hx' : (P.RootForm x) x = 0)
:
x = 0
theorem
RootPairing.rootForm_pos_of_ne_zero
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[LinearOrderedCommRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
{x : M}
(hx : x ∈ P.rootSpan)
(h : x ≠ 0)
:
0 < (P.RootForm x) x
theorem
RootSystem.rootForm_anisotropic
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[LinearOrderedCommRing R]
[Module R M]
[Module R N]
(P : RootSystem ι R M N)
:
(LinearMap.BilinMap.toQuadraticMap P.RootForm).Anisotropic