Documentation

TauCeti.Algebra.Lie.SpecialLinear.StandardCarrier.AllRootSubgroups.Steinberg

The type-A Steinberg maps on every root subgroup #

The Frobenius, the pinned graph automorphism, and their composite are explicitly constructed maps of the full-weight type-A_r carrier, already pinned against its 2 * r numbered simple root subgroups: on those the equations recorded so far carry the parameter across unchanged. This file records what the three maps do on the remaining root subgroups, the pair-indexed family TauCeti.SlStd.rootSubgroupPointsOfPair covering all r * (r + 1) roots ε_i - ε_j:

Frob_q (x_{ij}(c))     = x_{ij}(c ^ q),
γ (x_{ij}(c))          = x_{rev j, rev i}(ε_{ij} c),
γ ∘ Frob_q (x_{ij}(c)) = x_{rev j, rev i}(ε_{ij} c ^ q),      ε_{ij} = (-1) ^ (i + j + 1).

The Frobenius keeps each root subgroup and raises the parameter, exactly as on a simple root. The graph automorphism reverses the two matrix indices, which is the reversal of the Bourbaki numbering, and rescales the parameter by a sign: that sign is 1 whenever i + j is odd, and -1 whenever i + j is even, and the even case differs from the odd one only when (-1 : A) ≠ 1.

That sign comes from the signed conjugator that defines this γ. The sum i + j is odd on every numbered simple root, by TauCeti.SlStd.odd_rootTarget_add_rootSource, which is why the pinned equation TauCeti.SlStd.graphAutomorphismPoints_rootSubgroupPoints carries no sign; but as soon as the rank is at least two the root ε_0 - ε_2 has even index sum, and the automorphism inverts its parameter there. That inversion is a genuine departure from the sign-free equation whenever -1 ≠ 1 in the coefficient ring, which is TauCeti.SlStd.exists_graphAutomorphismPoints_rootSubgroupPointsOfPair_ne; over a ring where -1 = 1, such as ZMod 2, the sign is invisible and no such witness exists. Nothing here claims the stronger statement that no reparametrization of the root subgroups makes this particular γ sign-free on every root at once: that is a statement about compatibility with the Chevalley commutator constants, and is not proved in this file. The sign does not move the subgroup itself, only the parameter inside it, which is TauCeti.SlStd.map_graphAutomorphismPoints_range_rootSubgroupPointsOfPair.

Nothing here asserts that the carrier is the pinned simply connected Chevalley--Demazure group scheme, nor that any of the groups below is finite.

Main results #

References #

The Frobenius on an arbitrary root subgroup #

source
@[simp]
theorem TauCeti.SlStd.frobenius_rootSubgroupPointsOfPair (r p k : ℕ) {A : Type v} [CommRing A] [ExpChar A p] {i j : Fin (r + 1)} (hij : i ≠ j) (u : Multiplicative A) :
(frobenius r p k A) ((rootSubgroupPointsOfPair r hij) u) = (rootSubgroupPointsOfPair r hij) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ p ^ k))

The Frobenius raises the parameter of every root subgroup to its p ^ k-th power, and fixes the root. On a numbered simple root this is TauCeti.SlStd.frobenius_rootSubgroupPoints.

The graph automorphism on an arbitrary root subgroup #

source
@[simp]
theorem TauCeti.SlStd.graphAutomorphismPoints_rootSubgroupPointsOfPair (r : ℕ) {A : Type} [CommRing A] {i j : Fin (r + 1)} (hij : i ≠ j) (u : Multiplicative A) :
(graphAutomorphismPoints r A) ((rootSubgroupPointsOfPair r hij) u) = (rootSubgroupPointsOfPair r ⋯) (Multiplicative.ofAdd ((-1) ^ (↑i + ↑j + 1) * Multiplicative.toAdd u))

The pinned graph automorphism on an arbitrary root subgroup. It carries the root subgroup at ε_i - ε_j to the one at ε_{rev j} - ε_{rev i} and rescales the parameter by the sign (-1) ^ (i + j + 1). The reversal of the indices is the reversal of the Bourbaki numbering that TauCeti.SlStd.graphAutomorphismPoints_rootSubgroupPoints records on the simple roots; the sign is 1 on those roots and can be -1 on the others.

source
theorem TauCeti.SlStd.graphAutomorphismPoints_rootSubgroupPointsOfPair_of_odd (r : ℕ) {A : Type} [CommRing A] {i j : Fin (r + 1)} (hij : i ≠ j) (hodd : Odd (↑i + ↑j)) (u : Multiplicative A) :
(graphAutomorphismPoints r A) ((rootSubgroupPointsOfPair r hij) u) = (rootSubgroupPointsOfPair r ⋯) u

On a root whose two matrix indices have odd sum, the graph automorphism carries the parameter across unchanged. Every numbered simple root is of this kind, by TauCeti.SlStd.odd_rootTarget_add_rootSource.

source
theorem TauCeti.SlStd.graphAutomorphismPoints_rootSubgroupPointsOfPair_of_even (r : ℕ) {A : Type} [CommRing A] {i j : Fin (r + 1)} (hij : i ≠ j) (heven : Even (↑i + ↑j)) (u : Multiplicative A) :
(graphAutomorphismPoints r A) ((rootSubgroupPointsOfPair r hij) u) = (rootSubgroupPointsOfPair r ⋯) u⁻¹

On a root whose two matrix indices have even sum, the graph automorphism inverts the parameter.

source
theorem TauCeti.SlStd.exists_graphAutomorphismPoints_rootSubgroupPointsOfPair_eq_inv (r : ℕ) {A : Type} [CommRing A] (hr : 2 ≤ r) :
∃ (i : Fin (r + 1)) (j : Fin (r + 1)) (hij : i ≠ j), ∀ (u : Multiplicative A), (graphAutomorphismPoints r A) ((rootSubgroupPointsOfPair r hij) u) = (rootSubgroupPointsOfPair r ⋯) u⁻¹

The graph automorphism inverts the parameter of some root subgroup. As soon as the rank is at least two the root ε_0 - ε_2 has even index sum, so the sign (-1) ^ (i + j + 1) there is -1. This is an equation, not an inequality: whether the two sides differ depends on the coefficient ring, and TauCeti.SlStd.exists_graphAutomorphismPoints_rootSubgroupPointsOfPair_ne supplies the separation under (-1 : A) ≠ 1.

source
theorem TauCeti.SlStd.exists_graphAutomorphismPoints_rootSubgroupPointsOfPair_ne (r : ℕ) {A : Type} [CommRing A] (hr : 2 ≤ r) (hA : -1 ≠ 1) :
∃ (i : Fin (r + 1)) (j : Fin (r + 1)) (hij : i ≠ j) (u : Multiplicative A), (graphAutomorphismPoints r A) ((rootSubgroupPointsOfPair r hij) u) ≠ (rootSubgroupPointsOfPair r ⋯) u

The sign-free simple-root equation does not extend to every root. From rank two on, and whenever -1 and 1 are distinct in the coefficient ring, there is a root subgroup and a point of it whose image under the graph automorphism is not the point with the same parameter in the reversed root subgroup. Together with TauCeti.SlStd.odd_rootTarget_add_rootSource, which puts every numbered simple root in the sign-free case, this says that the sign-free equation holding on the numbered simple roots does not hold on every root. The hypothesis on A is needed: over ZMod 2 the sign -1 equals 1 and the equation of TauCeti.SlStd.graphAutomorphismPoints_rootSubgroupPointsOfPair is sign-free on every root.

source
theorem TauCeti.SlStd.map_graphAutomorphismPoints_range_rootSubgroupPointsOfPair (r : ℕ) {A : Type} [CommRing A] {i j : Fin (r + 1)} (hij : i ≠ j) :
Subgroup.map (graphAutomorphismPoints r A).toMonoidHom (rootSubgroupPointsOfPair r hij).range = (rootSubgroupPointsOfPair r ⋯).range

The graph automorphism permutes the root subgroups. The sign it introduces rescales the parameter by a unit and so does not move the subgroup: the image of the root subgroup at ε_i - ε_j is the root subgroup at ε_{rev j} - ε_{rev i}.

The twisted Frobenius on an arbitrary root subgroup #

source
@[simp]
theorem TauCeti.SlStd.twistedFrobenius_rootSubgroupPointsOfPair (r p k : ℕ) {A : Type} [CommRing A] [ExpChar A p] {i j : Fin (r + 1)} (hij : i ≠ j) (u : Multiplicative A) :
(twistedFrobenius r p k A) ((rootSubgroupPointsOfPair r hij) u) = (rootSubgroupPointsOfPair r ⋯) (Multiplicative.ofAdd ((-1) ^ (↑i + ↑j + 1) * Multiplicative.toAdd u ^ p ^ k))

The graph-twisted Frobenius on an arbitrary root subgroup. It reverses the two matrix indices, raises the parameter to the p ^ k-th power, and rescales it by the sign (-1) ^ (i + j + 1). This is the general-root form of the Steinberg map of the twisted family ²A_r(q), whose simple-root form is TauCeti.SlStd.twistedFrobenius_rootSubgroupPoints.