The Frobenius endomorphism of the points of a Kostant toral closure

Let A be a commutative ring of exponential characteristic p and let G = kostantToralGroupScheme be the closed subgroup scheme of GLₙ over ℤ generated by a family of represented Kostant root subgroups together with a represented weight torus. Since G is cut out by a Hopf ideal over ℤ, the p ^ k-power Frobenius of TauCeti.GeneralLinear.iterateFrobeniusHopfIdealPoints restricts to a group endomorphism F of its A-valued points, acting on matrices by raising every entry to its p ^ k-th power.

This file names that endomorphism for the toral carrier and computes it on the two pinned families that generate it. Writing q = p ^ k, the root subgroups and the torus transform by

F (xᵢ(u)) = xᵢ(u ^ q),        F (t(s)) = t(s ^ q).

Neither equation is a hypothesis on the data: both are the naturality of those families in the value ring, read at the Frobenius, which is a ring endomorphism of A exactly because A has exponential characteristic p. In particular no root-system, reductivity, or finiteness input is used, and F is defined on the whole point group rather than only on the elementary subgroup the root subgroups generate.

The fixed points are then identified: read inside GLₙ(A), the points of the carrier fixed by F are the points of the same carrier valued in the Frobenius-fixed subring of A. For p prime, 0 < k, A an algebraic closure of ZMod p and q = p ^ k, that subring is the field of q elements, so this is G(𝔽_q) = G(A)^F. Nothing here asserts that either side is finite, and no algebraic closedness or field hypothesis is used.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantToralFrobenius: the p ^ k-power Frobenius as a group endomorphism of the points of the toral closure.

Main results

• TauCeti.UniversalEnvelopingAlgebra.map_iterateFrobenius_kostantRootSubgroupMatrix and TauCeti.UniversalEnvelopingAlgebra.map_iterateFrobenius_kostantTorusMatrix: the entrywise Frobenius raises a root-subgroup parameter and a torus point to their p ^ k-th powers.
• TauCeti.UniversalEnvelopingAlgebra.coe_kostantToralFrobenius: the endomorphism acts by the entrywise Frobenius.
• TauCeti.UniversalEnvelopingAlgebra.kostantToralFrobenius_kostantRootSubgroupMatrix and TauCeti.UniversalEnvelopingAlgebra.kostantToralFrobenius_kostantTorusMatrix: its action on the bundled root-subgroup and torus points.
• TauCeti.UniversalEnvelopingAlgebra.kostantToralFrobenius_zero and TauCeti.UniversalEnvelopingAlgebra.kostantToralFrobenius_add: the iteration laws.
• TauCeti.UniversalEnvelopingAlgebra.map_subtype_fixedSubgroup_kostantToralFrobenius_eq: the points fixed by the Frobenius are the points valued in the Frobenius-fixed subring.

References

• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

This supplies the q-power Frobenius half of the target "points over an algebraically closed field as a group, functorially in the field, so that a field endomorphism induces a group endomorphism of the points" in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, for the toral carrier that Layer 9's Chevalley--Demazure construction assembles. Its consumer is milestone L1 of TauCetiRoadmap/CFSGStatement/README.md, whose untwisted Steinberg map is Frob_q on the points of a pinned Chevalley--Demazure group and whose completion evidence is the simple-root-subgroup equations, together with milestone L3, which takes the fixed subgroup of that map.

The Frobenius on the generating families

theorem TauCeti.UniversalEnvelopingAlgebra.map_iterateFrobenius_kostantRootSubgroupMatrix {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (p k : ℕ) {A : Type v} [CommRing A] [ExpChar A p] (i : I) (t : Multiplicative A) : (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) ((kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) (AdditiveGroup.gaPointsMulEquiv.symm t)) = (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (Multiplicative.toAdd t ^ p ^ k)))

The Frobenius raises a root-subgroup parameter to its p ^ k-th power. This is the naturality of the represented root subgroup in the value ring, read at the ring endomorphism iterateFrobenius A p k.

theorem TauCeti.UniversalEnvelopingAlgebra.map_iterateFrobenius_kostantTorusMatrix {κ V : Type} [AddCommGroup V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (p k : ℕ) {A : Type v} [CommRing A] [ExpChar A p] [Fintype κ] (s : κ → Aˣ) : (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) ((kostantTorusMatrix M b wt) s) = (kostantTorusMatrix M b wt) (s ^ p ^ k)

The Frobenius raises a torus point to its p ^ k-th power. In a weight basis the torus point is the diagonal matrix of its weight characters, and the Frobenius raises each of them to the p ^ k-th power.

The Frobenius endomorphism of the points

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralFrobenius {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (p k : ℕ) [Finite κ] (A : Type v) [CommRing A] [ExpChar A p] : ↥(kostantToralPointsSubgroup e h ρ M hM hnil b wt A) →* ↥(kostantToralPointsSubgroup e h ρ M hM hnil b wt A)

The p ^ k-power Frobenius endomorphism of the points of a Kostant toral closure.

For p prime, 0 < k, A an algebraic closure of ZMod p and pinned Chevalley data, this is the untwisted Steinberg endomorphism of the carrier; for k = 0, or in characteristic zero, it is the identity.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantToralFrobenius {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (p k : ℕ) [Finite κ] (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(kostantToralPointsSubgroup e h ρ M hM hnil b wt A)) : ↑((kostantToralFrobenius e h ρ M hM hnil b wt p k A) g) = (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) ↑g

The Frobenius endomorphism of the points of a toral closure acts by the entrywise Frobenius.

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantToralFrobenius_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (p k : ℕ) [Finite κ] (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(kostantToralPointsSubgroup e h ρ M hM hnil b wt A)) (r c : Fin n) : ↑↑((kostantToralFrobenius e h ρ M hM hnil b wt p k A) g) r c = ↑↑g r c ^ p ^ k

Entrywise, the Frobenius endomorphism of the points of a toral closure raises each entry to the p ^ k-th power.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralFrobenius_kostantRootSubgroupMatrix {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (p k : ℕ) [Finite κ] (A : Type v) [CommRing A] [ExpChar A p] (i : I) (t : Multiplicative A) : (kostantToralFrobenius e h ρ M hM hnil b wt p k A) ⟨(kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) (AdditiveGroup.gaPointsMulEquiv.symm t), ⋯⟩ = ⟨(kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (Multiplicative.toAdd t ^ p ^ k))), ⋯⟩

The Frobenius raises a bundled root-subgroup parameter to its p ^ k-th power.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralFrobenius_kostantTorusMatrix {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (p k : ℕ) [Finite κ] (A : Type v) [CommRing A] [ExpChar A p] [Fintype κ] (s : κ → Aˣ) : (kostantToralFrobenius e h ρ M hM hnil b wt p k A) ⟨diagGL fun (i : Fin n) => torusCharacter s (wt i), ⋯⟩ = ⟨(kostantTorusMatrix M b wt) (s ^ p ^ k), ⋯⟩

The Frobenius raises a bundled point of the represented weight torus to its p ^ k-th power.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralFrobenius_zero {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (p : ℕ) [Finite κ] (A : Type v) [CommRing A] [ExpChar A p] : kostantToralFrobenius e h ρ M hM hnil b wt p 0 A = MonoidHom.id ↥(kostantToralPointsSubgroup e h ρ M hM hnil b wt A)

The zeroth Frobenius iterate is the identity on the points of a toral closure.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralFrobenius_add {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (p k : ℕ) [Finite κ] (A : Type v) [CommRing A] [ExpChar A p] (m : ℕ) : kostantToralFrobenius e h ρ M hM hnil b wt p (k + m) A = (kostantToralFrobenius e h ρ M hM hnil b wt p k A).comp (kostantToralFrobenius e h ρ M hM hnil b wt p m A)

Frobenius iterates add under composition on the points of a toral closure.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralFrobenius_eq_self_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (p k : ℕ) [Finite κ] (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(kostantToralPointsSubgroup e h ρ M hM hnil b wt A)) : (kostantToralFrobenius e h ρ M hM hnil b wt p k A) g = g ↔ ∀ (r c : Fin n), ↑↑g r c ∈ frobeniusFixedSubring A p k

A point of a toral closure is fixed by the Frobenius endomorphism exactly when every one of its entries lies in the Frobenius-fixed subring.

theorem TauCeti.UniversalEnvelopingAlgebra.map_subtype_fixedSubgroup_kostantToralFrobenius {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (p k : ℕ) [Finite κ] (A : Type v) [CommRing A] [ExpChar A p] : Subgroup.map (kostantToralPointsSubgroup e h ρ M hM hnil b wt A).subtype (fixedSubgroup (kostantToralFrobenius e h ρ M hM hnil b wt p k A)) = kostantToralPointsSubgroup e h ρ M hM hnil b wt A ⊓ fixedSubgroup (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k))

The points of a toral closure fixed by its Frobenius endomorphism, read inside GLₙ(A).

theorem TauCeti.UniversalEnvelopingAlgebra.map_subtype_fixedSubgroup_kostantToralFrobenius_eq {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (p k : ℕ) [Finite κ] (A : Type v) [CommRing A] [ExpChar A p] : Subgroup.map (kostantToralPointsSubgroup e h ρ M hM hnil b wt A).subtype (fixedSubgroup (kostantToralFrobenius e h ρ M hM hnil b wt p k A)) = Subgroup.map (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) (kostantToralPointsSubgroup e h ρ M hM hnil b wt ↥(frobeniusFixedSubring A p k))

The points of a toral closure over the Frobenius-fixed subring are its Frobenius-fixed points. For p prime, 0 < k, A an algebraic closure of ZMod p and q = p ^ k this is G(𝔽_q) = G(A)^F for the carrier the Chevalley--Demazure construction assembles.