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 w.r.t. 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][bourbaki1968]
- [M. Demazure, SGA III, Exposé XXI, Données Radicielles][demazure1970]
Todo #
- Weyl-invariance of
RootFormandCorootForm - Faithfulness of Weyl group perm action, and finiteness of Weyl group, over ordered rings.
- Relation to Coxeter weight.
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 w.r.t. the root / coroot forms.
Examples include crystallographic pairings in characteristic zero
RootPairing.instIsAnisotropicOfIsCrystallographic and pairings over ordered scalars.
RootPairing.instIsAnisotropicOfLinearOrderedCommRing.
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]
:
theorem
RootPairing.isAnisotropic_of_isValuedIn
{ι : 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)
(S : Type u_5)
[CommRing S]
[LinearOrder S]
[IsStrictOrderedRing S]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
:
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]
:
def
RootPairing.toInvariantForm
{ι : 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]
:
The root form of an anisotropic pairing as an invariant form.
Equations
Instances For
@[simp]
theorem
RootPairing.toInvariantForm_form
{ι : 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]
:
theorem
RootPairing.smul_coroot_eq_of_root_add_root_eq
{ι : 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]
[IsDomain R]
[Module.IsTorsionFree R N]
{i j k : ι}
{m n : R}
(hk : m • P.root i + n • P.root j = P.root k)
:
theorem
RootPairing.finrank_range_polarization_eq_finrank_span_coroot
{ι : 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)
(S : Type u_5)
[CommRing S]
[IsDomain R]
[IsDomain S]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
[Module S M]
[IsScalarTower S R M]
[Module S N]
[IsScalarTower S R N]
[P.IsAnisotropic]
:
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]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
(S : Type u_5)
[CommRing S]
[IsDomain R]
[IsDomain S]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
[Module S M]
[IsScalarTower S R M]
[Module S N]
[IsScalarTower S R N]
[P.IsAnisotropic]
:
theorem
RootPairing.polarizationIn_Injective
{ι : 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)
(S : Type u_5)
[CommRing S]
[IsDomain R]
[IsDomain S]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
[Module S M]
[IsScalarTower S R M]
[Module S N]
[IsScalarTower S R N]
[P.IsAnisotropic]
:
Function.Injective ⇑(P.PolarizationIn S)
theorem
RootPairing.exists_coroot_ne
{ι : 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)
(S : Type u_5)
[CommRing S]
[IsDomain R]
[IsDomain S]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
[Module S M]
[IsScalarTower S R M]
[Module S N]
[IsScalarTower S R N]
[P.IsAnisotropic]
{x : ↥(P.rootSpan S)}
(hx : x ≠ 0)
:
theorem
RootPairing.posRootForm_posForm_pos_of_ne_zero
{ι : 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)
(S : Type u_5)
[CommRing S]
[LinearOrder S]
[IsStrictOrderedRing S]
[IsDomain R]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
[Module S M]
[IsScalarTower S R M]
[Module S N]
[IsScalarTower S R N]
{x : ↥(P.rootSpan S)}
(hx : x ≠ 0)
:
theorem
RootPairing.posRootForm_rootFormIn_posDef
{ι : 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)
(S : Type u_5)
[CommRing S]
[LinearOrder S]
[IsStrictOrderedRing S]
[IsDomain R]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
[Module S M]
[IsScalarTower S R M]
[Module S N]
[IsScalarTower S R N]
:
theorem
RootPairing.posRootForm_posForm_anisotropic
{ι : 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)
(S : Type u_5)
[CommRing S]
[LinearOrder S]
[IsStrictOrderedRing S]
[IsDomain R]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
[Module S M]
[IsScalarTower S R M]
[Module S N]
[IsScalarTower S R N]
:
theorem
RootPairing.posRootForm_posForm_nondegenerate
{ι : 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)
(S : Type u_5)
[CommRing S]
[LinearOrder S]
[IsStrictOrderedRing S]
[IsDomain R]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
[Module S M]
[IsScalarTower S R M]
[Module S N]
[IsScalarTower S R N]
:
(P.posRootForm S).posForm.Nondegenerate
@[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 R)) = Module.finrank R ↥(P.corootSpan R)
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]
:
Equality of finranks when the base is a domain.
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 R) (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 R) (LinearMap.ker P.CorootForm)
theorem
RootPairing.rootForm_nondegenerate
{ι : 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]
[P.IsRootSystem]
:
@[deprecated RootPairing.rootForm_nondegenerate (since := "2025-12-14")]
theorem
RootSystem.rootForm_nondegenerate
{ι : 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]
[P.IsRootSystem]
:
Alias of RootPairing.rootForm_nondegenerate.
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 R) (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 R) (LinearMap.ker P.CorootForm)
theorem
RootPairing.ker_rootForm_eq_dualAnnihilator
{ι : 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]
:
theorem
RootPairing.ker_corootForm_eq_dualAnnihilator
{ι : 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]
:
instance
RootPairing.instIsBalanced
{ι : 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]
:
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 R))
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]
:
@[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]
:
theorem
RootPairing.rootSpan_eq_top_iff
{ι : 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]
:
def
RootPairing.PolarizationEquiv
{ι : 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.IsRootSystem]
:
The polarization map from weight space to coweight space as an equivalence.
Equations
Instances For
@[simp]
theorem
RootPairing.polarizationEquiv_toLinearMap
{ι : 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.IsRootSystem]
:
theorem
RootPairing.polarizationEquiv_apply
{ι : 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.IsRootSystem]
(m : M)
:
theorem
RootPairing.coroot_eq_polarizationEquiv_apply_root
{ι : 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.IsRootSystem]
(i : ι)
:
theorem
RootPairing.polarizationEquiv_symm_apply_coroot
{ι : 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.IsRootSystem]
{i : ι}
:
@[simp]
theorem
RootPairing.linearIndepOn_coroot_iff
{ι : 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.IsRootSystem]
[NeZero 2]
{s : Set ι}
:
instance
RootPairing.instIsAnisotropicOfLinearOrderedCommRing
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[CommRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
:
theorem
RootPairing.zero_le_rootForm
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[CommRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
(x : M)
:
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]
[CommRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
:
LinearMap.Nondegenerate (P.RootForm.restrict (P.rootSpan R))
See also RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic.
theorem
RootPairing.rootForm_self_eq_zero_iff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[CommRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
{x : M}
:
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]
[CommRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
{x : M}
(hx : x ∈ P.rootSpan R)
(hx' : (P.RootForm x) 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]
[CommRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
{x : M}
(hx : x ∈ P.rootSpan R)
(h : x ≠ 0)
:
theorem
RootPairing.rootForm_anisotropic
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[CommRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[P.IsRootSystem]
:
@[deprecated RootPairing.rootForm_anisotropic (since := "2025-12-14")]
theorem
RootSystem.rootForm_anisotropic
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[AddCommGroup M]
[AddCommGroup N]
[CommRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[Module R M]
[Module R N]
(P : RootPairing ι R M N)
[P.IsRootSystem]
:
Alias of RootPairing.rootForm_anisotropic.