Documentation

Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

The canonical bilinear form on a finite root pairing #

Given a finite root pairing, we define a canonical map from weight space to coweight space, and the corresponding bilinear form. This form is symmetric and Weyl-invariant, and if the base ring is linearly ordered, then the form is root-positive, positive-semidefinite on the weight space, 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 crystallographic root pairing are restricted to a small finite set of possibilities. Another application is to the faithfulness of the Weyl group action on roots, and finiteness of the Weyl group.

Main definitions: #

Polarization: A distinguished linear map from the weight space to the coweight space.
RootForm : The bilinear form on weight space corresponding to Polarization.

Main results: #

polarization_self_sum_of_squares : The inner product of any weight vector is a sum of squares.
rootForm_reflection_reflection_apply : RootForm is invariant with respect to reflections.
rootForm_self_smul_coroot: The inner product of a root with itself times the corresponding coroot is equal to two times Polarization applied to the root.
rootForm_self_non_neg: RootForm is positive semidefinite.

References: #

[N. Bourbaki, Lie groups and Lie algebras. Chapters 4--6][bourbaki1968]
[M. Demazure, SGA III, Exposé XXI, Données Radicielles][demazure1970]

TODO (possibly in other files) #

Weyl-invariance
Faithfulness of Weyl group action, and finiteness of Weyl group, for finite root systems.
Relation to Coxeter weight. In particular, positivity constraints for finite root pairings mean we restrict to weights between 0 and 4.

instance RootPairing.instFiniteSubtypeMemSubmoduleRootSpan {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

Module.Finite R ↥P.rootSpan

instance RootPairing.instFiniteSubtypeMemSubmoduleCorootSpan {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

Module.Finite R ↥P.corootSpan

def RootPairing.Polarization {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

An invariant linear map from weight space to coweight space.

Equations

P.Polarization = ∑ i : ι, LinearMap.toSpanSingleton R N (P.coroot i) ∘ₗ P.coroot' i

Instances For

@[simp]

theorem RootPairing.Polarization_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (x : M) :

P.Polarization x = ∑ i : ι, (P.coroot' i) x • P.coroot i

def RootPairing.CoPolarization {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

An invariant linear map from coweight space to weight space.

Equations

P.CoPolarization = ∑ i : ι, LinearMap.toSpanSingleton R M (P.root i) ∘ₗ P.root' i

Instances For

@[simp]

theorem RootPairing.CoPolarization_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (x : N) :

P.CoPolarization x = ∑ i : ι, (P.root' i) x • P.root i

theorem RootPairing.CoPolarization_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

P.CoPolarization = P.flip.Polarization

def RootPairing.RootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

LinearMap.BilinForm R M

An invariant inner product on the weight space.

Equations

P.RootForm = ∑ i : ι, LinearMap.smulRight (P.coroot' i) (P.coroot' i)

Instances For

def RootPairing.CorootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

LinearMap.BilinForm R N

An invariant inner product on the coweight space.

Equations

P.CorootForm = ∑ i : ι, LinearMap.smulRight (P.root' i) (P.root' i)

Instances For

theorem RootPairing.rootForm_apply_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (x y : M) :

(P.RootForm x) y = ∑ i : ι, (P.coroot' i) x * (P.coroot' i) y

theorem RootPairing.corootForm_apply_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (x y : N) :

(P.CorootForm x) y = ∑ i : ι, (P.root' i) x * (P.root' i) y

theorem RootPairing.toPerfectPairing_apply_apply_Polarization {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (x y : M) :

(P.toPerfectPairing y) (P.Polarization x) = (P.RootForm x) y

theorem RootPairing.toPerfectPairing_apply_CoPolarization {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (x : N) :

P.toPerfectPairing (P.CoPolarization x) = P.CorootForm x

theorem RootPairing.flip_comp_polarization_eq_rootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

P.flip.toLin ∘ₗ P.Polarization = P.RootForm

theorem RootPairing.self_comp_coPolarization_eq_corootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

P.toLin ∘ₗ P.CoPolarization = P.CorootForm

theorem RootPairing.polarization_apply_eq_zero_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (m : M) :

P.Polarization m = 0 ↔ P.RootForm m = 0

theorem RootPairing.coPolarization_apply_eq_zero_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (n : N) :

P.CoPolarization n = 0 ↔ P.CorootForm n = 0

theorem RootPairing.ker_polarization_eq_ker_rootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

LinearMap.ker P.Polarization = LinearMap.ker P.RootForm

theorem RootPairing.ker_copolarization_eq_ker_corootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

LinearMap.ker P.CoPolarization = LinearMap.ker P.CorootForm

theorem RootPairing.rootForm_symmetric {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

LinearMap.IsSymm P.RootForm

@[simp]

theorem RootPairing.rootForm_reflection_reflection_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i : ι) (x y : M) :

(P.RootForm ((P.reflection i) x)) ((P.reflection i) y) = (P.RootForm x) y

theorem RootPairing.rootForm_self_smul_coroot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i : ι) :

(P.RootForm (P.root i)) (P.root i) • P.coroot i = 2 • P.Polarization (P.root i)

This is SGA3 XXI Lemma 1.2.1 (10), key for proving nondegeneracy and positivity.

theorem RootPairing.four_smul_rootForm_sq_eq_coxeterWeight_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i j : ι) :

4 • (P.RootForm (P.root i)) (P.root j) ^ 2 = P.coxeterWeight i j • ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))

theorem RootPairing.corootForm_self_smul_root {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i : ι) :

(P.CorootForm (P.coroot i)) (P.coroot i) • P.root i = 2 • P.CoPolarization (P.coroot i)

theorem RootPairing.rootForm_self_sum_of_squares {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (x : M) :

IsSumSq ((P.RootForm x) x)

theorem RootPairing.rootForm_root_self {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (j : ι) :

(P.RootForm (P.root j)) (P.root j) = ∑ i : ι, P.pairing j i * P.pairing j i

theorem RootPairing.range_polarization_domRestrict_le_span_coroot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

LinearMap.range (P.Polarization.domRestrict P.rootSpan) ≤ P.corootSpan

theorem RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

Submodule.map P.toDualLeft.symm P.corootSpan.dualAnnihilator ≤ LinearMap.ker P.RootForm

theorem RootPairing.rootSpan_dualAnnihilator_le_ker_rootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

Submodule.map P.toDualRight.symm P.rootSpan.dualAnnihilator ≤ LinearMap.ker P.CorootForm

theorem RootPairing.prod_rootForm_smul_coroot_mem_range_domRestrict {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i : ι) :

(∏ a : ι, (P.RootForm (P.root a)) (P.root a)) • P.coroot i ∈ LinearMap.range (P.Polarization.domRestrict P.rootSpan)

theorem RootPairing.rootForm_self_non_neg {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (x : M) :

0 ≤ (P.RootForm x) x

theorem RootPairing.rootForm_self_eq_zero_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) {x : M} :

(P.RootForm x) x = 0 ↔ x ∈ LinearMap.ker P.RootForm

theorem RootPairing.rootForm_root_self_pos {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i : ι) :

0 < (P.RootForm (P.root i)) (P.root i)

theorem RootPairing.coxeterWeight_le_four {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i j : ι) :

P.coxeterWeight i j ≤ 4

SGA3 XXI Prop. 2.3.1

instance RootPairing.instIsRootPositiveRootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

P.IsRootPositive P.RootForm

theorem RootPairing.coxeterWeight_mem_set_of_isCrystallographic {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i j : ι) [P.IsCrystallographic] :

P.coxeterWeight i j ∈ {0, 1, 2, 3, 4}