Root data and root systems

This file contains basic results for root systems and root data.

Main definitions / results:

• RootPairing.ext: In characteristic zero if there is no torsion, the correspondence between roots and coroots is unique.
• RootSystem.ext: In characteristic zero if there is no torsion, a root system is determined entirely by its roots.
• RootPairing.mk': In characteristic zero if there is no torsion, to check that two finite familes of of roots and coroots form a root pairing, it is sufficient to check that they are stable under reflections.
• RootSystem.mk': In characteristic zero if there is no torsion, to check that a finite family of roots form a root system, we do not need to check that the coroots are stable under reflections since this follows from the corresponding property for the roots.

Todo

• Derived properties of pairs, e.g., (ultra)parallel linearly independent pairs generate infinite dihedral groups.
• Properties of Weyl group (faithful action on roots, finiteness for finite ι)
• Conditions for existence of Weyl-invariant form (e.g., finiteness).

@[simp]

theorem RootPairing.equiv_of_mapsTo_symm_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 : PerfectPairing R M N) (root : ι ↪ M) (coroot : ι ↪ N) (i : ι) (h : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) (hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2) (j : ι) : (RootPairing.equiv_of_mapsTo p root coroot i h hp).symm j = ⋯.choose

@[simp]

theorem RootPairing.equiv_of_mapsTo_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 : PerfectPairing R M N) (root : ι ↪ M) (coroot : ι ↪ N) (i : ι) (h : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) (hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2) (j : ι) : (RootPairing.equiv_of_mapsTo p root coroot i h hp) j = ⋯.choose

def RootPairing.equiv_of_mapsTo {ι : 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 : PerfectPairing R M N) (root : ι ↪ M) (coroot : ι ↪ N) (i : ι) (h : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) (hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2) : ι ≃ ι

The bijection on the indexing set induced by reflection.

Equations

• RootPairing.equiv_of_mapsTo p root coroot i h hp = { toFun := fun (j : ι) => ⋯.choose, invFun := fun (j : ι) => ⋯.choose, left_inv := ⋯, right_inv := ⋯ }

theorem RootPairing.injOn_dualMap_subtype_span_root_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] [Finite ι] (P : RootPairing ι R M N) [NoZeroSMulDivisors ℤ M] : Set.InjOn (⇑((Submodule.span R (Set.range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip)) (Set.range ⇑P.coroot)

Even though the roots may not span, coroots are distinguished by their pairing with the roots. The proof depends crucially on the fact that there are finitely-many roots.

Modulo trivial generalisations, this statement is exactly Lemma 1.1.4 on page 87 of SGA 3 XXI.

theorem RootPairing.ext {ι : 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] [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] {P₁ : RootPairing ι R M N} {P₂ : RootPairing ι R M N} (he : P₁.toLin = P₂.toLin) (hr : P₁.root = P₂.root) (hc : Set.range ⇑P₁.coroot = Set.range ⇑P₂.coroot) : P₁ = P₂

In characteristic zero if there is no torsion, the correspondence between roots and coroots is unique.

Formally, the point is that the hypothesis hc depends only on the range of the coroot mappings.

def RootPairing.mk' {ι : 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] [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] (p : PerfectPairing R M N) (root : ι ↪ M) (coroot : ι ↪ N) (hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2) (hr : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) (hc : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (coroot i) (p.toLin (root i)))) (Set.range ⇑coroot) (Set.range ⇑coroot)) : RootPairing ι R M N

In characteristic zero if there is no torsion, to check that two finite familes of of roots and coroots form a root pairing, it is sufficient to check that they are stable under reflections.

Equations

• One or more equations did not get rendered due to their size.

theorem RootSystem.ext {ι : 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] [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] {P₁ : RootSystem ι R M N} {P₂ : RootSystem ι R M N} (he : P₁.toLin = P₂.toLin) (hr : P₁.root = P₂.root) : P₁ = P₂

In characteristic zero if there is no torsion, a finite root system is determined entirely by its roots.

def RootSystem.mk' {ι : 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] [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] (p : PerfectPairing R M N) (root : ι ↪ M) (coroot : ι ↪ N) (hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2) (hs : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) (hsp : Submodule.span R (Set.range ⇑root) = ⊤) : RootSystem ι R M N

In characteristic zero if there is no torsion, to check that a finite family of roots form a root system, we do not need to check that the coroots are stable under reflections since this follows from the corresponding property for the roots.

Equations

• RootSystem.mk' p root coroot hp hs hsp = { toRootPairing := RootPairing.mk' p root coroot hp hs ⋯, span_eq_top := hsp }