17.1. First examples🔗

A root system is a finite collection of non-zero vectors in Euclidean space that is invariant under reflection in the hyperplane perpendicular to any of the vectors. In fact, this data determines the inner product up to scale and alternative definitions exist which obviate the need to supply the inner product as part of the data. Mathlib omits the inner product, partly because it allows a unified treatment of root systems and root data.

The following adds a root system to the Lean environment

variable {ι R M N : Type*} [Finite ι] [CommRing R]
  [AddCommGroup M] [Module R M]
  [AddCommGroup N] [Module R N]
  (P : RootPairing ι R M N) [P.IsRootSystem]

Similarly, the following adds a root datum to the Lean environment

variable {ι M N : Type*} [Finite ι]
  [AddCommGroup M] [Module.Finite ℤ M]
  [AddCommGroup N] [Module.Finite ℤ N]
  (P : RootDatum ι M N)

Note that we do not need to add the assumption that M and N are free since P includes the data of a perfect pairing between M and N and, together with finiteness, this ensures freeness. Indeed we can witness this as follows:

open Module in
example : Free ℤ M :=
  have : IsReflexive ℤ M := .of_isPerfPair P.toLinearMap
  free_of_finite_type_torsion_free'