Theorems · Inductive type · nonassociative algebras

RootPairing

Type u_1 →
  (R : Type u_2) →
    (M : Type u_3) →
      (N : Type u_4) →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [Module R M] → [inst_3 : AddCommGroup N] → [Module R N] → 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.

Defined in

Mathlib.LinearAlgebra.RootSystem.Defs

Cited by

710 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 39 definitions · uses no axioms

Assumes

CommRingAddCommGroupModuleAddCommGroupModule