Invariance of the G2 tensors under the root elements and torus

The four numbered simple root elements of the seven-dimensional representation preserve its cross product and its invariant dual form, over every commutative ring. The weight torus preserves the same tensors. These are the generator equations needed to place the group generated by the root subgroups and torus inside the tensor stabilizers. In characteristic three, those stabilizer conditions are the hypotheses of Matrix.g2SpecialIsogeny_mul.

The short-root elements include their integral divided-square terms; no division by two or characteristic restriction is needed. All parameters are arbitrary ring elements, so the equations also apply to the universal root parameter over a polynomial ring.

The coordinates and conventions are those of TauCeti.G2ShortRoot.crossOperator and TauCeti.G2ShortRoot.invariantDualForm. See R. W. Carter, Simple Groups of Lie Type, §§12.3, 13.4, and S. Garibaldi and R. M. Guralnick, Simple groups stabilizing polynomials, §6.

@[simp]

theorem TauCeti.G2ShortRoot.preservesG2Cross_one_add_smul_raisingMatrix_zero_add_sq_smul_single {R : Type u_1} [CommRing R] (t : R) : (1 + t • (raisingMatrix 0).map Int.cast + t ^ 2 • Matrix.single 2 4 1).PreservesG2Cross

The positive short simple root elements preserve the cross product.

@[simp]

theorem TauCeti.G2ShortRoot.preservesG2Cross_one_add_smul_raisingMatrix_one {R : Type u_1} [CommRing R] (t : R) : (1 + t • (raisingMatrix 1).map Int.cast).PreservesG2Cross

The positive long simple root elements preserve the cross product.

@[simp]

theorem TauCeti.G2ShortRoot.preservesG2Cross_one_add_smul_loweringMatrix_zero_add_sq_smul_single {R : Type u_1} [CommRing R] (t : R) : (1 + t • (loweringMatrix 0).map Int.cast + t ^ 2 • Matrix.single 4 2 1).PreservesG2Cross

The negative short simple root elements preserve the cross product.

@[simp]

theorem TauCeti.G2ShortRoot.preservesG2Cross_one_add_smul_loweringMatrix_one {R : Type u_1} [CommRing R] (t : R) : (1 + t • (loweringMatrix 1).map Int.cast).PreservesG2Cross

The negative long simple root elements preserve the cross product.

@[simp]

theorem TauCeti.G2ShortRoot.one_add_smul_raisingMatrix_zero_add_sq_smul_single_mul_invariantDualForm_mul_transpose {R : Type u_1} [CommRing R] (t : R) : have g := 1 + t • (raisingMatrix 0).map Int.cast + t ^ 2 • Matrix.single 2 4 1; g * invariantDualForm.map Int.cast * g.transpose = invariantDualForm.map Int.cast

The positive short simple root elements fix the invariant dual form by congruence.

@[simp]

theorem TauCeti.G2ShortRoot.one_add_smul_raisingMatrix_one_mul_invariantDualForm_mul_transpose {R : Type u_1} [CommRing R] (t : R) : have g := 1 + t • (raisingMatrix 1).map Int.cast; g * invariantDualForm.map Int.cast * g.transpose = invariantDualForm.map Int.cast

The positive long simple root elements fix the invariant dual form by congruence.

@[simp]

theorem TauCeti.G2ShortRoot.one_add_smul_loweringMatrix_zero_add_sq_smul_single_mul_invariantDualForm_mul_transpose {R : Type u_1} [CommRing R] (t : R) : have g := 1 + t • (loweringMatrix 0).map Int.cast + t ^ 2 • Matrix.single 4 2 1; g * invariantDualForm.map Int.cast * g.transpose = invariantDualForm.map Int.cast

The negative short simple root elements fix the invariant dual form by congruence.

@[simp]

theorem TauCeti.G2ShortRoot.one_add_smul_loweringMatrix_one_mul_invariantDualForm_mul_transpose {R : Type u_1} [CommRing R] (t : R) : have g := 1 + t • (loweringMatrix 1).map Int.cast; g * invariantDualForm.map Int.cast * g.transpose = invariantDualForm.map Int.cast

The negative long simple root elements fix the invariant dual form by congruence.

@[simp]

theorem TauCeti.G2ShortRoot.preservesG2Cross_diagonal_torusCharacter {R : Type u_1} [CommRing R] (s : Fin 2 → Rˣ) : (Matrix.diagonal fun (a : Fin 7) => ↑(torusCharacter s (weight a))).PreservesG2Cross

The weight torus preserves the cross product.

@[simp]

theorem TauCeti.G2ShortRoot.diagonal_torusCharacter_mul_invariantDualForm_mul_transpose {R : Type u_1} [CommRing R] (s : Fin 2 → Rˣ) : have g := Matrix.diagonal fun (a : Fin 7) => ↑(torusCharacter s (weight a)); g * invariantDualForm.map Int.cast * g.transpose = invariantDualForm.map Int.cast

The weight torus fixes the invariant dual form by congruence.