Steinberg endomorphisms of a Kostant elementary group

Let E(A) = ⟨xᵢ(t)⟩ be the elementary group generated by the Kostant root subgroups over a value ring A of exponential characteristic p. Two endomorphisms of it are already available: the q-power Frobenius Frob_q for q = p ^ n, which raises every root-subgroup parameter to its q-th power, and the automorphism γ attached to a symmetry (σ, θ) of the numbered Kostant data, which moves the root subgroup at i to the one at σ i without touching its parameter. This file forms their composite

steinberg = γ ∘ Frob_q,

the abstract shape of a Steinberg endomorphism outside the Suzuki--Ree families. The Kostant data (e, h, ρ, M) and the value ring A stay arbitrary here, so the fixed points of the composite are only an abstract subgroup: identifying them with a finite group of Lie type needs the pinned ambient data of the later milestone L0 together with an identification theorem, neither of which is available yet, and no finiteness is proved below. Its defining equation on the root subgroups is

steinberg (xᵢ(t)) = x_{σ i}(t ^ q).

The two factors commute, so iterating the composite separates them: the k-th iterate is γ ^ k ∘ Frob_{q ^ k}. When γ ^ d = 1, the d-th iterate is therefore the plain Frobenius Frob_{q ^ d}, and a steinberg-fixed point is fixed by it. Once the data is pinned and the fixed subgroups are identified, that containment becomes the standard statement that a graph-twisted group of Lie type sits inside the untwisted group over the degree-d extension of the field of definition, with d = 2 for ²A, ²D and ²E₆ and d = 3 for ³D₄; what is proved below is the containment of abstract fixed subgroups it specializes to. Conversely a point fixed by both Frob_q and γ is fixed by the composite, though in general not every fixed point of the composite arises this way.

A trivial symmetry automorphism, γ = 1, collapses steinberg to Frob_q itself, so the nine untwisted families are the same construction rather than a separate one.

Nothing here asserts that steinberg is the unique endomorphism with the displayed action on the root subgroups, that its fixed subgroup is finite, or that the derived central quotient of that fixed subgroup is simple. The symmetry (σ, θ) is data supplied by the caller, exactly as in TauCeti/Algebra/Lie/UniversalEnveloping/Kostant/RootSubgroup/NumberedSymmetry.lean, and no claim is made that σ comes from a symmetry of a Dynkin diagram.

Main definitions

• TauCeti.UniversalEnvelopingAlgebra.kostantElementarySteinberg: the endomorphism γ ∘ Frob_q of the elementary group.

Main results

• TauCeti.UniversalEnvelopingAlgebra.kostantElementarySteinberg_kostantRootSubgroupParam: the defining equation steinberg (xᵢ(t)) = x_{σ i}(t ^ q).
• TauCeti.UniversalEnvelopingAlgebra.kostantElementarySteinberg_iterate: the iterates separate as γ ^ k ∘ Frob_{q ^ k}; the corresponding _of_numberedSymmetryAut_pow_eq_one theorem handles a symmetry automorphism whose k-th power is the identity.
• kostantElementarySteinberg_eq_kostantElementaryFrobenius_of_numberedSymmetryAut_eq_one: a trivial symmetry automorphism gives back the Frobenius endomorphism.
• fixedSubgroup_kostantElementarySteinberg_le_fixedSubgroup_kostantElementaryFrobenius: the fixed subgroup of a Steinberg endomorphism whose symmetry automorphism has d-th power equal to the identity lies in the fixed subgroup of Frob_{q ^ d}.
• fixedSubgroup_inf_fixedSubgroup_le_fixedSubgroup_kostantElementarySteinberg: a point fixed by both Frob_q and γ is fixed by the composite.
• TauCeti.UniversalEnvelopingAlgebra.kostantElementarySteinberg_injective: injectivity over a reduced value ring.
• TauCeti.UniversalEnvelopingAlgebra.kostantElementaryMap_kostantElementarySteinberg: compatibility with base change of the value ring, and map_fixedSubgroup_kostantElementarySteinberg_le for the fixed points it carries along.

Roadmap

This supplies an abstract prerequisite for milestone L1 of TauCetiRoadmap/CFSGStatement/README.md, "ordinary and graph Steinberg maps": the composite γ ∘ Frob_q that its graph-twisted branches require. Its factors and their commutation are already available over a general Kostant datum, so they can be composed without the pinned ambient group owned by L0.

No carrier is introduced here. The elementary group and both of its endomorphisms are already on main, and they belong to Layer 9, "pinned Chevalley--Demazure group schemes over ℤ", of TauCetiRoadmap/ReductiveGroups/README.md, as the module documentation of the surrounding Kostant files records. That layer asks for the Chevalley--Demazure construction via a Chevalley basis and the Kostant ℤ-form of the enveloping algebra, for its root subgroup maps, for points functorial enough that a field endomorphism induces an endomorphism of the point group, with the q-power Frobenius named as the first case a consumer asks for, and for the pinned isomorphism theorem that turns a diagram automorphism into a named group automorphism. The CFSGStatement README lists Layer 9 among the two bodies of work owned by other roadmaps that L0 rests on, to be claimed in the roadmap owning them because L0 consumes rather than restates them. Layer 9 therefore runs ahead of L0 rather than behind it, and composing two of its endomorphisms uses nothing L0 supplies.

The route to that ambient point group is already explicit in the repository. The same represented root subgroups define kostantGeneratedGroupScheme, whose point group is an input to L0, and map_kostantElementarySubgroup_le_generatedPoints embeds the elementary subgroup into those points. On the scheme side, kostantGeneratedNumberedSymmetryIso is the graph automorphism required by L1, while Frobenius on the corresponding Hopf-ideal points is GeneralLinear.iterateFrobeniusHopfIdealPoints. Thus the missing generation theorem is needed to identify the elementary subgroup with all ambient points, but not to connect the construction here to the already-established point-group route.

This file does not complete L1: its displayed equation concerns Kostant root subgroups indexed by an arbitrary type I, not the numbered simple root subgroups of ValidLieTypeIndex.AmbientGroup, and the required power relation on γ is a hypothesis here. Once L0 supplies the pinned Chevalley--Demazure data, the GraphTwistedIndex branches of ValidLieTypeIndex.steinberg can instantiate this construction and discharge those hypotheses using their numbered diagram maps. The Suzuki--Ree branches of L2 are a separate construction, an odd power of an exceptional isogeny rather than a composite with a graph automorphism.

References

• R. W. Carter, Simple Groups of Lie Type, chapters 12 and 13.
• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, chapter 1.
• D. Gorenstein, R. Lyons and R. Solomon, The Classification of the Finite Simple Groups.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantElementarySteinberg {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] : ↥(kostantElementarySubgroup e h ρ M hM hnil A) →* ↥(kostantElementarySubgroup e h ρ M hM hnil A)

The Steinberg endomorphism attached to a symmetry (σ, θ) of the numbered Kostant data and to the p ^ n-power Frobenius of the value ring: the composite γ ∘ Frob_q, where q = p ^ n.

For general Kostant data and a general value ring this is just that composite, and its fixed subgroup is an abstract subgroup of the elementary group. Over an algebraic closure of 𝔽_p, with the pinned ambient data of the later milestone L0 and with θ realising a symmetry of the Dynkin diagram, it is intended to be the endomorphism whose fixed points are the untwisted or graph-twisted finite group of Lie type; that identification is a separate theorem and is not proved here. The Suzuki--Ree families are not of this form: their Steinberg maps are odd powers of an exceptional isogeny and use no diagram permutation.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementarySteinberg_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] (g : ↥(kostantElementarySubgroup e h ρ M hM hnil A)) : (kostantElementarySteinberg e h ρ M hM hnil σ θ hθM hθe hσ p n A) g = (kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ A) ((kostantElementaryFrobenius e h ρ M hM hnil p n A) g)

The Steinberg endomorphism applies the Frobenius first and the numbered symmetry second.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementarySteinberg_kostantRootSubgroupParam {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] (i : I) (t : Multiplicative ↑A) : (kostantElementarySteinberg e h ρ M hM hnil σ θ hθM hθe hσ p n A) ⟨(kostantRootSubgroupParam e h ρ M hM i ⋯ A) t, ⋯⟩ = ⟨(kostantRootSubgroupParam e h ρ M hM (σ i) ⋯ A) (Multiplicative.ofAdd (Multiplicative.toAdd t ^ p ^ n)), ⋯⟩

The defining equation of the Steinberg endomorphism on the root subgroups: it moves the root subgroup at i to the one at σ i and raises the parameter to the p ^ n-th power.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementarySteinberg_injective {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] [IsReduced ↑A] : Function.Injective ⇑(kostantElementarySteinberg e h ρ M hM hnil σ θ hθM hθe hσ p n A)

The Steinberg endomorphism is injective over a reduced value ring.

Its symmetry factor is an automorphism, and its Frobenius factor is injective because a reduced ring has injective Frobenius.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementarySteinberg_iterate {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] (k : ℕ) : (have this := kostantElementarySteinberg e h ρ M hM hnil σ θ hθM hθe hσ p n A; this) ^ k = (MulEquiv.toMonoidHom (kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ A ^ k)).comp (kostantElementaryFrobenius e h ρ M hM hnil p (n * k) A)

The iterates of a Steinberg endomorphism separate into a power of the numbered symmetry and a Frobenius: the k-th iterate of γ ∘ Frob_q is γ ^ k ∘ Frob_{q ^ k}.

The separation is exactly the commutation of the two factors; without it an iterate would only be an alternating word in them.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementarySteinberg_iterate_eq_kostantElementaryFrobenius_of_numberedSymmetryAut_pow_eq_one {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] {k : ℕ} (hk : kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ A ^ k = 1) : (have this := kostantElementarySteinberg e h ρ M hM hnil σ θ hθM hθe hσ p n A; this) ^ k = kostantElementaryFrobenius e h ρ M hM hnil p (n * k) A

If the k-th power of a symmetry automorphism is the identity, then the k-th power of its Steinberg endomorphism is the plain Frobenius Frob_{q ^ k}.

For the graph-twisted families this is k = 2 on ²A, ²D and ²E₆ and k = 3 on ³D₄. The power relation is taken on γ rather than on θ, since that is all the proof uses; a caller holding θ ^ k = 1 on the nose gets it from kostantElementaryNumberedSymmetryAut_pow_eq_one.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementarySteinberg_eq_kostantElementaryFrobenius_of_numberedSymmetryAut_eq_one {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] (hγ : kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ A = 1) : kostantElementarySteinberg e h ρ M hM hnil σ θ hθM hθe hσ p n A = kostantElementaryFrobenius e h ρ M hM hnil p n A

A trivial symmetry automorphism produces the plain Frobenius endomorphism.

The nine untwisted families of the classification are therefore the case γ = 1 of the same construction, and not a second one; it is the first iterate of the previous theorem.

theorem TauCeti.UniversalEnvelopingAlgebra.fixedSubgroup_kostantElementarySteinberg_le_fixedSubgroup_kostantElementaryFrobenius {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] {d : ℕ} (hd : kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ A ^ d = 1) : fixedSubgroup (kostantElementarySteinberg e h ρ M hM hnil σ θ hθM hθe hσ p n A) ≤ fixedSubgroup (kostantElementaryFrobenius e h ρ M hM hnil p (n * d) A)

A point fixed by a Steinberg endomorphism whose symmetry automorphism has d-th power equal to the identity is fixed by the Frobenius Frob_{q ^ d}.

Once the data is pinned and the fixed subgroups are identified, this specializes to the containment of a graph-twisted group of Lie type in the untwisted group over the degree-d extension of its field of definition; here it is a containment of abstract fixed subgroups. The reverse containment is not claimed and fails in general, the twisted group being a proper subgroup once the symmetry is nontrivial.

theorem TauCeti.UniversalEnvelopingAlgebra.fixedSubgroup_inf_fixedSubgroup_le_fixedSubgroup_kostantElementarySteinberg {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] : fixedSubgroup (kostantElementaryFrobenius e h ρ M hM hnil p n A) ⊓ fixedSubgroup (MulEquiv.toMonoidHom (kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ A)) ≤ fixedSubgroup (kostantElementarySteinberg e h ρ M hM hnil σ θ hθM hθe hσ p n A)

A point fixed by both the Frobenius and the numbered symmetry is fixed by their composite.

This is fixedSubgroup_inf_fixedSubgroup_le_fixedSubgroup_comp at the two factors. The converse fails in general: a Steinberg-fixed point need not be fixed by either factor, which is why a graph-twisted group is not the fixed points of a Frobenius.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryMap_kostantElementarySteinberg {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (p n : ℕ) {A B : CommAlgCat ℤ} [ExpChar (↑A) p] [ExpChar (↑B) p] (φ : A ⟶ B) (g : ↥(kostantElementarySubgroup e h ρ M hM hnil A)) : (kostantElementaryMap e h ρ M hM hnil φ) ((kostantElementarySteinberg e h ρ M hM hnil σ θ hθM hθe hσ p n A) g) = (kostantElementarySteinberg e h ρ M hM hnil σ θ hθM hθe hσ p n B) ((kostantElementaryMap e h ρ M hM hnil φ) g)

The Steinberg endomorphism commutes with base change of the value ring.

Both of its factors do, so the elementary groups over the value rings of a fixed exponential characteristic carry a Steinberg endomorphism naturally.

theorem TauCeti.UniversalEnvelopingAlgebra.map_fixedSubgroup_kostantElementarySteinberg_le {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (p n : ℕ) {A B : CommAlgCat ℤ} [ExpChar (↑A) p] [ExpChar (↑B) p] (φ : A ⟶ B) : Subgroup.map (kostantElementaryMap e h ρ M hM hnil φ) (fixedSubgroup (kostantElementarySteinberg e h ρ M hM hnil σ θ hθM hθe hσ p n A)) ≤ fixedSubgroup (kostantElementarySteinberg e h ρ M hM hnil σ θ hθM hθe hσ p n B)

Base change of the value ring carries Steinberg-fixed points to Steinberg-fixed points.

Both sides are abstract fixed subgroups of the elementary groups; nothing here identifies either one with a finite group of Lie type, asserts that either is finite, or asserts that the map between them is injective.