Root data and root systems

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

Main definitions:

• RootPairing: Given two perfectly-paired R-modules M and N (over some commutative ring R) a root pairing with indexing set ι is the data of an ι-indexed subset of M ("the roots") and an ι-indexed subset of N ("the coroots") satisfying the axioms familiar from the traditional theory of root systems / data.
• RootDatum: A root datum is a root pairing for which the roots and coroots take values in finitely-generated free Abelian groups.
• RootSystem: A root system is a root pairing for which the roots span their ambient module.
• RootPairing.IsCrystallographic: A root pairing is said to be crystallographic if the pairing between a root and coroot is always an integer.
• RootPairing.IsReduced: A root pairing is said to be reduced if it never contains the double of a root.

Todo

• Introduce the Weyl Group
• Base change of root pairings.
• Isomorphism of root pairings.
• Crystallographic root systems are isomorphic to base changes of root systems over ℤ?

Implementation details

A root datum is sometimes defined as two subsets: roots and coroots, together with a bijection between them, subject to hypotheses. However the hypotheses ensure that the bijection is unique and so the question arises of whether this bijection should be part of the data of a root datum or whether one should merely assert its existence. For root systems, things are even more extreme: the coroots are uniquely determined by the roots. Furthermore a root system induces a canonical non-degenerate bilinear form on the ambient space and many informal accounts even include this form as part of the data.

We have opted for a design in which some of the uniquely-determined data is included: the bijection between roots and coroots is (implicitly) included and the coroots are included for root systems. Empirically this seems to be by far the most convenient design and by providing extensionality lemmas expressing the uniqueness we expect to get the best of both worlds.

A final point is that we require roots and coroots to be injections from a base indexing type ι rather than subsets of their codomains. This design was chosen to avoid the bijection between roots and coroots being a dependently-typed object. A third option would be to have the roots and coroots be subsets but to avoid having a dependently-typed bijection by defining it globally with junk value 0 outside of the roots and coroots. This would work but lacks the convenient symmetry that the chosen design enjoys: by introducing the indexing type ι, one does not have to pick a direction (roots → coroots or coroots → roots) for the forward direction of the bijection. Besides, providing the user with the additional definitional power to specify an indexing type ι is a benefit and the junk-value pattern is a cost.

structure RootPairing (ι : 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] extends PerfectPairing : Type (max (max (max u_1 u_2) u_3) u_4)

Given two perfectly-paired R-modules M and N, a root pairing with indexing set ι is the data of an ι-indexed subset of M ("the roots") and an ι-indexed subset of N ("the coroots") satisfying the axioms familiar from the traditional theory of root systems / data.

It exists to allow for a convenient unification of the theories of root systems and root data.

• toLin : M →ₗ[R] N →ₗ[R] R
• bijectiveLeft : Function.Bijective ⇑self.toLin
• bijectiveRight : Function.Bijective ⇑self.toLin.flip
• root : ι ↪ M
• coroot : ι ↪ N
• root_coroot_two : ∀ (i : ι), (self.toLin (self.root i)) (self.coroot i) = 2
• mapsTo_preReflection_root : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (self.root i) (self.toLin.flip (self.coroot i)))) (Set.range ⇑self.root) (Set.range ⇑self.root)
• mapsTo_preReflection_coroot : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (self.coroot i) (self.toLin (self.root i)))) (Set.range ⇑self.coroot) (Set.range ⇑self.coroot)

theorem RootPairing.root_coroot_two {ι : 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] (self : RootPairing ι R M N) (i : ι) : (self.toLin (self.root i)) (self.coroot i) = 2

theorem RootPairing.mapsTo_preReflection_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] (self : RootPairing ι R M N) (i : ι) : Set.MapsTo (⇑(Module.preReflection (self.root i) (self.toLin.flip (self.coroot i)))) (Set.range ⇑self.root) (Set.range ⇑self.root)

theorem RootPairing.mapsTo_preReflection_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] (self : RootPairing ι R M N) (i : ι) : Set.MapsTo (⇑(Module.preReflection (self.coroot i) (self.toLin (self.root i)))) (Set.range ⇑self.coroot) (Set.range ⇑self.coroot)

@[reducible, inline]

abbrev RootDatum (ι : Type u_1) (X₁ : Type u_5) (X₂ : Type u_6) [AddCommGroup X₁] [AddCommGroup X₂] : Type (max (max u_1 u_5) u_6)

A root datum is a root pairing with coefficients in the integers and for which the root and coroot spaces are finitely-generated free Abelian groups.

Note that the latter assumptions [Free ℤ X₁] [Finite ℤ X₁] [Free ℤ X₂] [Finite ℤ X₂] should be supplied as mixins.

Equations

• RootDatum ι X₁ X₂ = RootPairing ι ℤ X₁ X₂

structure RootSystem (ι : 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] extends RootPairing : Type (max (max (max u_1 u_2) u_3) u_4)

A root system is a root pairing for which the roots span their ambient module.

Note that this is slightly more general than the usual definition in the sense that N is not required to be the dual of M.

• toLin : M →ₗ[R] N →ₗ[R] R
• bijectiveLeft : Function.Bijective ⇑self.toLin
• bijectiveRight : Function.Bijective ⇑self.toLin.flip
• root : ι ↪ M
• coroot : ι ↪ N
• root_coroot_two : ∀ (i : ι), (self.toLin (self.root i)) (self.coroot i) = 2
• mapsTo_preReflection_root : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (self.root i) (self.toLin.flip (self.coroot i)))) (Set.range ⇑self.root) (Set.range ⇑self.root)
• mapsTo_preReflection_coroot : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (self.coroot i) (self.toLin (self.root i)))) (Set.range ⇑self.coroot) (Set.range ⇑self.coroot)
• span_eq_top : Submodule.span R (Set.range ⇑self.root) = ⊤

theorem RootSystem.span_eq_top {ι : 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] (self : RootSystem ι R M N) : Submodule.span R (Set.range ⇑self.root) = ⊤

def RootPairing.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) : Prop

A root pairing is said to be crystallographic if the pairing between a root and coroot is always an integer.

Equations

• P.IsCrystallographic = ∀ (i : ι), Set.MapsTo (⇑(P.toLin (P.root i))) (Set.range ⇑P.coroot) ↑(AddSubgroup.zmultiples 1)

def RootPairing.IsReduced {ι : 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) : Prop

A root pairing is said to be reduced if any linearly dependent pair of roots is related by a sign.

Equations

• P.IsReduced = ∀ (i j : ι), ¬LinearIndependent R ![P.root i, P.root j] → P.root i = P.root j ∨ P.root i = -P.root j

def RootPairing.flip {ι : 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) : RootPairing ι R N M

If we interchange the roles of M and N, we still have a root pairing.

Equations

• P.flip = let __src := P.flip; { toPerfectPairing := __src, root := P.coroot, coroot := P.root, root_coroot_two := ⋯, mapsTo_preReflection_root := ⋯, mapsTo_preReflection_coroot := ⋯ }

def RootPairing.reflection {ι : 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) (i : ι) : M ≃ₗ[R] M

The reflection associated to a root.

Equations

• P.reflection i = Module.reflection ⋯

def RootPairing.coreflection {ι : 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) (i : ι) : N ≃ₗ[R] N

The reflection associated to a coroot.

Equations

• P.coreflection i = Module.reflection ⋯

def RootPairing.pairing {ι : 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) (i : ι) (j : ι) : R

This is the pairing between roots and coroots.

Equations

• P.pairing i j = (P.toLin (P.root i)) (P.coroot j)

def RootPairing.coxeterWeight {ι : 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) (i : ι) (j : ι) : R

The Coxeter Weight of a pair gives the weight of an edge in a Coxeter diagram, when it is finite. It is 4 cos² θ, where θ describes the dihedral angle between hyperplanes.

Equations

• P.coxeterWeight i j = P.pairing i j * P.pairing j i

def RootPairing.IsOrthogonal {ι : 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) (i : ι) (j : ι) : Prop

Two roots are orthogonal when they are fixed by each others' reflections.

Equations

• P.IsOrthogonal i j = (P.pairing i j = 0 ∧ P.pairing j i = 0)