The simply connected root datum of type G2

This file constructs the pinned integral root datum of type G2 on the character and cocharacter lattices Fin 2 -> Z. The character lattice is written in the fundamental-weight basis and the cocharacter lattice in the simple-coroot basis. Consequently the two simple roots are the rows (2, -1) and (-3, 2) of the Bourbaki-numbered Cartan matrix, while their coroots are the two standard basis vectors.

The twelve roots are ordered with the two simple roots first, followed by the other four positive roots and then their negatives. Their coroots use the same ordering. The displayed positive roots, in simple-root coordinates, are

alpha1, alpha2, alpha1 + alpha2, 2 alpha1 + alpha2,
3 alpha1 + alpha2, 3 alpha1 + 2 alpha2.

Here alpha1 is short and alpha2 is long. The corresponding positive coroot coordinates are (1,0), (0,1), (1,3), (2,3), (1,1), (1,2). These tables make the carrier explicit and also make the reflection-stability axioms of RootPairing decidable finite calculations.

Main definitions and results

• TauCeti.DynkinType.g2SimplyConnectedRootDatum is the pinned twelve-root datum, with g2Root and g2Coroot its coordinate tables, g2Root_apply and g2Coroot_apply their entries, and g2SimplyConnectedRootDatum_root, g2SimplyConnectedRootDatum_coroot, g2SimplyConnectedRootDatum_toLinearMap and g2SimplyConnectedRootDatum_pairing the lemmas that expose them.
• Its RootPairing.IsRootSystem instance records that the roots and the coroots span their lattices; coroot spanning is the simply connected condition.
• Its RootPairing.IsReduced instance rules out nontrivial scalar multiples among the roots.
• TauCeti.DynkinType.g2Coeff is the simple-root coordinate table of the twelve roots; TauCeti.DynkinType.g2Root_eq_smul_add_smul expands each root along it, and TauCeti.DynkinType.eq_g2Coeff_of_root_eq records the uniqueness of that expansion.
• TauCeti.DynkinType.linearIndepOn_g2Root_zero_one records that the two simple roots are linearly independent, which is what makes that expansion unique.
• TauCeti.DynkinType.g2SimplyConnectedBase is its Bourbaki-numbered base.
• TauCeti.DynkinType.g2SimplyConnectedRootDatum_pairing_eq_cartanMatrix_G2 pins that numbering entrywise: on the two base indices the Cartan integers are the Bourbaki matrix !![2, -1; -3, 2].
• TauCeti.DynkinType.hasCartanType_g2SimplyConnectedRootDatum identifies its Cartan type as G2.
• TauCeti.DynkinType.ncard_posRoots_g2SimplyConnectedRootDatum counts its positive roots: there are six of them, for any base.

References

The coordinates and numbering follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IX. This is the G2 branch of Layer 6 in TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, following the target signatures in TauCetiRoadmap/RepresentationTheory/RootSystems/Suggested.lean. The positive-root count is the corresponding clause of the G₂ worked example in the "Worked examples (acceptance criteria)" section of that README; it agrees with the count in Bourbaki, Plate IX.

def TauCeti.DynkinType.g2Root : Fin 12 ↪ Fin 2 → ℤ

The roots of G2 in the fundamental-weight basis, with simple roots first.

Equations

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

theorem TauCeti.DynkinType.g2Root_apply (i : Fin 12) : g2Root i = ![![2, -1], ![-3, 2], ![-1, 1], ![1, 0], ![3, -1], ![0, 1], ![-2, 1], ![3, -2], ![1, -1], ![-1, 0], ![-3, 1], ![0, -1]] i

The explicit entries of the root coordinate table.

def TauCeti.DynkinType.g2Coroot : Fin 12 ↪ Fin 2 → ℤ

The coroots of G2 in the simple-coroot basis, ordered compatibly with g2Root.

Equations

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

theorem TauCeti.DynkinType.g2Coroot_apply (i : Fin 12) : g2Coroot i = ![![1, 0], ![0, 1], ![1, 3], ![2, 3], ![1, 1], ![1, 2], ![-1, 0], ![0, -1], ![-1, -3], ![-2, -3], ![-1, -1], ![-1, -2]] i

The explicit entries of the coroot coordinate table.

@[simp]

theorem TauCeti.DynkinType.g2Root_castAdd (i : Fin 2) : g2Root (Fin.castAdd 10 i) = CartanMatrix.G₂.transpose i

The simple roots of G2 sit at the first two indices, where they are the rows of its Bourbaki-numbered Cartan matrix.

@[simp]

theorem TauCeti.DynkinType.g2Coroot_castAdd (i : Fin 2) : g2Coroot (Fin.castAdd 10 i) = Pi.single i 1

The simple coroots of G2 sit at the first two indices, where they are the standard basis of the cocharacter lattice.

def TauCeti.DynkinType.g2Coeff : Fin 12 → Fin 2 → ℤ

The simple-root coordinates of the twelve roots of the pinned G2 datum, in the index order of g2Root: the positive roots are alpha1, alpha2, alpha1 + alpha2, 2 alpha1 + alpha2, 3 alpha1 + alpha2, 3 alpha1 + 2 alpha2, and index k + 6 is the negative of index k.

Equations

• TauCeti.DynkinType.g2Coeff = ![![1, 0], ![0, 1], ![1, 1], ![2, 1], ![3, 1], ![3, 2], ![-1, 0], ![0, -1], ![-1, -1], ![-2, -1], ![-3, -1], ![-3, -2]]

theorem TauCeti.DynkinType.g2Coeff_apply (i : Fin 12) : g2Coeff i = ![![1, 0], ![0, 1], ![1, 1], ![2, 1], ![3, 1], ![3, 2], ![-1, 0], ![0, -1], ![-1, -1], ![-2, -1], ![-3, -1], ![-3, -2]] i

The explicit entries of the simple-root coefficient table.

theorem TauCeti.DynkinType.g2Root_eq_smul_add_smul (k : Fin 12) : g2Root k = g2Coeff k 0 • g2Root 0 + g2Coeff k 1 • g2Root 1

Each tabulated root is the tabulated combination of the two simple roots.

theorem TauCeti.DynkinType.linearIndepOn_g2Root_zero_one : LinearIndepOn ℤ ⇑g2Root {0, 1}

The two simple roots of G2 are linearly independent.

theorem TauCeti.DynkinType.eq_g2Coeff_of_root_eq {k : Fin 12} {c : Fin 2 → ℤ} (h : g2Root k = c 0 • g2Root 0 + c 1 • g2Root 1) : c = g2Coeff k

The two simple roots are linearly independent, so the expansion TauCeti.DynkinType.g2Root_eq_smul_add_smul determines the coefficients.

theorem TauCeti.DynkinType.g2Coeff_nonneg (k : Fin 12) (hk : ↑k < 6) (i : Fin 2) : 0 ≤ g2Coeff k i

The six positive roots come first: their simple-root coordinates are nonnegative.

theorem TauCeti.DynkinType.g2Coeff_nonpos (k : Fin 12) (hk : 6 ≤ ↑k) (i : Fin 2) : g2Coeff k i ≤ 0

The six negative roots come last: their simple-root coordinates are nonpositive.

@[simp]

theorem TauCeti.DynkinType.g2Coeff_add_six (k : Fin 12) : g2Coeff (k + 6) = -g2Coeff k

The last six roots are the negatives of the first six, in simple-root coordinates.

def TauCeti.DynkinType.g2SimplyConnectedRootDatum : RootDatum (Fin 12) (Fin 2 → ℤ) (Fin 2 → ℤ)

The pinned simply connected root datum of type G2.

Both lattices use Fin 2 -> Z: fundamental weights on the root side and simple coroots on the coroot side. Root indices 0 and 1 are the short and long simple roots respectively, as pinned by g2SimplyConnectedRootDatum_pairing_eq_cartanMatrix_G2.

Equations

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

@[simp]

theorem TauCeti.DynkinType.g2SimplyConnectedRootDatum_root : g2SimplyConnectedRootDatum.root = g2Root

The roots of the pinned G2 datum are the coordinate table g2Root.

@[simp]

theorem TauCeti.DynkinType.g2SimplyConnectedRootDatum_coroot : g2SimplyConnectedRootDatum.coroot = g2Coroot

The coroots of the pinned G2 datum are the coordinate table g2Coroot.

@[simp]

theorem TauCeti.DynkinType.g2SimplyConnectedRootDatum_toLinearMap (x y : Fin 2 → ℤ) : (g2SimplyConnectedRootDatum.toLinearMap x) y = x ⬝ᵥ y

The perfect pairing of the pinned G2 datum is the dot product of coordinate vectors, the fundamental-weight and simple-coroot bases being dual to one another.

@[simp]

theorem TauCeti.DynkinType.g2SimplyConnectedRootDatum_pairing (i j : Fin 12) : RootPairing.pairing g2SimplyConnectedRootDatum i j = g2Root i ⬝ᵥ g2Coroot j

The Cartan integer of the pinned G2 datum at a pair of root indices is the dot product of the tabulated root and coroot coordinates.

instance TauCeti.DynkinType.instIsReducedG2SimplyConnectedRootDatum : RootPairing.IsReduced g2SimplyConnectedRootDatum

The pinned simply connected root datum of type G₂ is reduced.

theorem TauCeti.DynkinType.span_root_g2SimplyConnectedRootDatum_eq_top : Submodule.span ℤ (Set.range ⇑g2SimplyConnectedRootDatum.root) = ⊤

The roots of the pinned type G₂ datum span the character lattice.

instance TauCeti.DynkinType.instIsRootSystemFinOfNatNatIntForallG2SimplyConnectedRootDatum : RootPairing.IsRootSystem g2SimplyConnectedRootDatum

The pinned G2 datum is a root system: its roots and coroots span their two lattices. Coroot spanning is the simply connected lattice condition required by the pinned Chevalley--Demazure construction.

def TauCeti.DynkinType.g2SimplyConnectedBase : RootPairing.Base g2SimplyConnectedRootDatum

The Bourbaki-numbered base of the pinned simply connected G2 root datum. Its support is the first two root indices, short root first and long root second; see g2SimplyConnectedRootDatum_pairing_eq_cartanMatrix_G2.

Equations

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

@[simp]

theorem TauCeti.DynkinType.g2SimplyConnectedBase_support : g2SimplyConnectedBase.support = {0, 1}

theorem TauCeti.DynkinType.g2SimplyConnectedRootDatum_pairing_eq_cartanMatrix_G2 (i j : Fin 2) : RootPairing.pairing g2SimplyConnectedRootDatum (Fin.castLE g2SimplyConnectedRootDatum_pairing_eq_cartanMatrix_G2._proof_2 i) (Fin.castLE g2SimplyConnectedRootDatum_pairing_eq_cartanMatrix_G2._proof_2 j) = !![2, -1; -3, 2] i j

The Cartan integers of the pinned G2 datum at the two base indices form the Bourbaki matrix !![2, -1; -3, 2] in the pinned index order: index 0 is the short simple root and index 1 the long one. This is what pins the numbering; hasCartanType_g2SimplyConnectedRootDatum cannot, since the relabelling in HasCartanType is existential and at rank two it may transpose the two off-diagonal entries.

theorem TauCeti.DynkinType.hasCartanType_g2SimplyConnectedRootDatum : HasCartanType g2SimplyConnectedRootDatum g2SimplyConnectedBase G2

The pinned simply connected G2 datum has Cartan type G2. The relabelling supplied by HasCartanType is existential, so the Bourbaki node numbering itself is pinned separately by g2SimplyConnectedRootDatum_pairing_eq_cartanMatrix_G2.

@[simp]

theorem TauCeti.DynkinType.ncard_posRoots_g2SimplyConnectedRootDatum (b : RootPairing.Base g2SimplyConnectedRootDatum) : (posRoots g2SimplyConnectedRootDatum b).ncard = 6

The pinned root datum of type G₂ has six positive roots. Exactly half of its twelve roots are positive, for any base.