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: #

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

Main results: #

RootPairing.rootForm_self_sum_of_squares : The inner product of any weight vector is a sum of squares.
RootPairing.rootForm_reflection_reflection_apply : RootForm is invariant with respect to reflections.
RootPairing.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.
RootPairing.exists_ge_zero_eq_rootForm: RootForm is positive semidefinite.
RootPairing.coxeterWeight_mem_set_of_isCrystallographic: the Coxeter weights belongs to the set {0, 1, 2, 3, 4}.

References: #

TODO (possibly in other files) #

Weyl-invariance
Faithfulness of Weyl group action, and finiteness of Weyl group, for finite root systems.

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

Module.Finite R ↥P.rootSpan

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

Module.Finite R ↥P.corootSpan

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

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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

P.CoPolarization = P.flip.Polarization

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

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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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.corootForm_self_smul_root {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (i : ι) :

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

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

(4 • P.CoPolarization ∘ₗ P.Polarization) (P.root i) = ((P.RootForm (P.root i)) (P.root i) * (P.CorootForm (P.coroot i)) (P.coroot i)) • P.root i

theorem RootPairing.four_smul_rootForm_sq_eq_coxeterWeight_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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.rootForm_self_sum_of_squares {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (i : ι) :

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

def RootPairing.posRootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [LinearOrderedCommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] [Fintype ι] :

RootPositiveForm S P

The bilinear form of a finite root pairing taking values in a linearly-ordered ring, as a root-positive form.

Equations

P.posRootForm S = { form := P.RootForm, symm := ⋯, isOrthogonal_reflection := ⋯, exists_eq := ⋯, exists_pos_eq := ⋯ }

Instances For

theorem RootPairing.exists_ge_zero_eq_rootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [LinearOrderedCommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] [Fintype ι] (x : M) (hx : x ∈ Submodule.span S (Set.range ⇑P.root)) :

∃ s ≥ 0, (algebraMap S R) s = (P.RootForm x) x

theorem RootPairing.coxeterWeightIn_le_four {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [LinearOrderedCommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] [Finite ι] (i j : ι) :

P.coxeterWeightIn S i j ≤ 4

SGA3 XXI Prop. 2.3.1

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

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

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

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