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") an ι-indexed subset of N ("the coroots"), and an ι-indexed set of permutations of ι such that each root-coroot pair evaluates to 2, and the permutation attached to each element of ι is compatible with the reflections on the corresponding roots and coroots.
• 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

• Put more API theorems in the Defs file.
• Introduce the Weyl Group, and its action on the indexing set.
• Base change of root pairings (may need flatness).
• Isomorphism of root pairings.
• Crystallographic root systems are isomorphic to base changes of root systems over ℤ: Take M₀ and N₀ to be the ℤ-span of roots and coroots.

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.

Furthermore, 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.

As a final point of divergence from the classical literature, we make the reflection permutation on roots and coroots explicit, rather than specifying only that reflection preserves the sets of roots and coroots. This is necessary when working with infinite root systems, where the coroots are not uniquely determined by the roots, because without it, the reflection permutations on roots and coroots may not correspond. For this purpose, we define a map from ι to permutations on ι, and require that it is compatible with reflections and coreflections.

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"), an ι-indexed subset of N ("the coroots"), and an ι-indexed set of permutations of ι, such that each root-coroot pair evaluates to 2, and the permutation attached to each element of ι is compatible with the reflections on the corresponding roots and coroots.

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

  A parametrized family of vectors, called roots.

• coroot : ι ↪ N

  A parametrized family of dual vectors, called coroots.

• root_coroot_two : ∀ (i : ι), (self.toLin (self.root i)) (self.coroot i) = 2
• reflection_perm : ι → ι ≃ ι

  A parametrized family of permutations, induced by reflection.

• reflection_perm_root : ∀ (i j : ι), self.root j - (self.toLin (self.root j)) (self.coroot i) • self.root i = self.root ((self.reflection_perm i) j)
• reflection_perm_coroot : ∀ (i j : ι), self.coroot j - (self.toLin (self.root i)) (self.coroot j) • self.coroot i = self.coroot ((self.reflection_perm i) j)

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.reflection_perm_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 : ι) (j : ι) : self.root j - (self.toLin (self.root j)) (self.coroot i) • self.root i = self.root ((self.reflection_perm i) j)

theorem RootPairing.reflection_perm_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 : ι) (j : ι) : self.coroot j - (self.toLin (self.root i)) (self.coroot j) • self.coroot i = self.coroot ((self.reflection_perm i) j)

@[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
• reflection_perm : ι → ι ≃ ι
• reflection_perm_root : ∀ (i j : ι), self.root j - (self.toLin (self.root j)) (self.coroot i) • self.root i = self.root ((self.reflection_perm i) j)
• reflection_perm_coroot : ∀ (i j : ι), self.coroot j - (self.toLin (self.root i)) (self.coroot j) • self.coroot i = self.coroot ((self.reflection_perm i) j)
• 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) = ⊤

theorem RootPairing.ne_zero {ι : 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 : ι) [CharZero R] : P.root i ≠ 0

theorem RootPairing.ne_zero' {ι : 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 : ι) [CharZero R] : P.coroot i ≠ 0

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

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

@[simp]

theorem RootPairing.flip_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) : P.flip.flip = P

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)

@[simp]

theorem RootPairing.root_coroot_eq_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 : ι) : (P.toLin (P.root i)) (P.coroot j) = P.pairing i j

theorem RootPairing.coroot_root_eq_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 : ι) : (P.toLin.flip (P.coroot i)) (P.root j) = P.pairing j i

@[simp]

theorem RootPairing.pairing_same {ι : 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 : ι) : P.pairing i i = 2

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

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 ⋯

@[simp]

theorem RootPairing.root_reflection_perm {ι : 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 : ι) : P.root ((P.reflection_perm i) j) = (P.reflection i) (P.root j)

theorem RootPairing.mapsTo_reflection_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) (i : ι) : Set.MapsTo (⇑(P.reflection i)) (Set.range ⇑P.root) (Set.range ⇑P.root)

theorem RootPairing.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) (i : ι) (x : M) : (P.reflection i) x = x - (P.toLin x) (P.coroot i) • P.root i

theorem RootPairing.reflection_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) (i : ι) (j : ι) : (P.reflection i) (P.root j) = P.root j - P.pairing j i • P.root i

@[simp]

theorem RootPairing.reflection_apply_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) (i : ι) : (P.reflection i) (P.root i) = -P.root i

@[simp]

theorem RootPairing.reflection_same {ι : 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 : ι) (x : M) : (P.reflection i) ((P.reflection i) x) = x

theorem RootPairing.bijOn_reflection_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) (i : ι) : Set.BijOn (⇑(P.reflection i)) (Set.range ⇑P.root) (Set.range ⇑P.root)

@[simp]

theorem RootPairing.reflection_image_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) (i : ι) : ⇑(P.reflection i) '' Set.range ⇑P.root = Set.range ⇑P.root

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 ⋯

@[simp]

theorem RootPairing.coroot_reflection_perm {ι : 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 : ι) : P.coroot ((P.reflection_perm i) j) = (P.coreflection i) (P.coroot j)

theorem RootPairing.mapsTo_coreflection_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) (i : ι) : Set.MapsTo (⇑(P.coreflection i)) (Set.range ⇑P.coroot) (Set.range ⇑P.coroot)

theorem RootPairing.coreflection_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) (i : ι) (f : N) : (P.coreflection i) f = f - (P.toLin (P.root i)) f • P.coroot i

theorem RootPairing.coreflection_apply_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) (i : ι) (j : ι) : (P.coreflection i) (P.coroot j) = P.coroot j - P.pairing i j • P.coroot i

@[simp]

theorem RootPairing.coreflection_apply_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) (i : ι) : (P.coreflection i) (P.coroot i) = -P.coroot i

@[simp]

theorem RootPairing.coreflection_same {ι : 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 : ι) (x : N) : (P.coreflection i) ((P.coreflection i) x) = x

theorem RootPairing.bijOn_coreflection_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) (i : ι) : Set.BijOn (⇑(P.coreflection i)) (Set.range ⇑P.coroot) (Set.range ⇑P.coroot)

@[simp]

theorem RootPairing.coreflection_image_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) (i : ι) : ⇑(P.coreflection i) '' Set.range ⇑P.coroot = Set.range ⇑P.coroot

theorem RootPairing.coreflection_eq_flip_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 : ι) : P.coreflection i = P.flip.reflection i

theorem RootPairing.reflection_dualMap_eq_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 : ι) : ↑(P.reflection i).dualMap ∘ₗ P.toLin.flip = P.toLin.flip ∘ₗ ↑(P.coreflection i)

theorem RootPairing.coroot_eq_coreflection_of_root_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) {i : ι} {j : ι} {k : ι} (hk : P.root k = (P.reflection i) (P.root j)) : P.coroot k = (P.coreflection i) (P.coroot j)

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)

theorem RootPairing.isCrystallographic_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) : P.IsCrystallographic ↔ ∀ (i j : ι), ∃ (z : ℤ), ↑z = P.pairing i j

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

theorem RootPairing.isReduced_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) : P.IsReduced ↔ ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root 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

theorem RootPairing.coxeterWeight_swap {ι : 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 : ι) : P.coxeterWeight i j = P.coxeterWeight 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)

theorem RootPairing.IsOrthogonal.symm {ι : 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 : ι) : P.IsOrthogonal i j ↔ P.IsOrthogonal j i

theorem RootPairing.isOrthogonal_comm {ι : 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 : ι) (h : P.IsOrthogonal i j) : Commute (P.reflection i) (P.reflection j)