The elementary group generated by Kostant root subgroups

Let U_ℤ = kostantForm e h be a Kostant integral form acting on a rational representation V and preserving an additive subgroup M ≤ V, and suppose every distinguished root vector eᵢ acts nilpotently. Over a commutative ring A the divided-power exponentials of the eᵢ are automorphisms of A ⊗[ℤ] M, and the subgroup they generate,

E(A) = ⟨xᵢ(t) : i, t ∈ A⟩ ≤ Aut_A(A ⊗[ℤ] M),

is the subgroup generated by the Kostant root subgroups. When e and M arise from a Chevalley system and a finite free admissible lattice, this is the elementary Chevalley group constructed in Carter, Simple Groups of Lie Type, §4.4. A later identification theorem, under its additional hypotheses (including an algebraically closed value field), may identify it with all points of the Chevalley--Demazure group scheme; no such identification is claimed here.

The results here are the functoriality of E in the value ring and the endomorphism a ring endomorphism induces on it. Naturality of the divided-power exponential upgrades to the statement that the bundled scalar extension of automorphisms carries xᵢ(t) to xᵢ(φ t), so E is a subfunctor of GeneralLinear.scalarExtensionAutomorphismsFunctor. Specializing to the p ^ n-power Frobenius of a value ring of exponential characteristic p gives the endomorphism a Steinberg map is built from; it is injective as soon as the value ring is reduced.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam: the root subgroup map x_α with its parameter read in the value ring itself.
• TauCeti.UniversalEnvelopingAlgebra.kostantElementarySubgroup: the elementary group E(A).
• TauCeti.UniversalEnvelopingAlgebra.kostantElementaryMap: the group homomorphism induced by a morphism of value rings.
• TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFunctor: the resulting group-valued functor.
• TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFrobenius: the p ^ n-power Frobenius endomorphism, with kostantElementaryFrobenius_injective on a reduced value ring, kostantElementaryFrobenius_eq_kostantElementaryMap exhibiting it as a base change, kostantElementaryFrobenius_mul computing its powers, and kostantElementaryMap_kostantElementaryFrobenius its naturality in the value ring.

References

• R. W. Carter, Simple Groups of Lie Type, §4.4.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §27.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (A : CommAlgCat ℤ) : Multiplicative ↑A →* LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥M)

The root subgroup map x_α with its parameter read in the value ring.

This is kostantRootSubgroupPoints reindexed along the identification 𝔾ₐ(A) ≃ A⁺ of AdditiveGroup.gaPointsMulEquiv. The two forms carry the same information; this one states the Chevalley relations in the shape downstream work uses, xᵢ(t) xᵢ(u) = xᵢ(t + u).

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam_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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (A : CommAlgCat ℤ) (t : Multiplicative ↑A) : (kostantRootSubgroupParam e h ρ M hM i hnil A) t = (kostantRootSubgroupPoints e h ρ M hM i hnil) (AdditiveGroup.gaPointsMulEquiv.symm t)

The parametrized root subgroup map is the root subgroup on 𝔾ₐ-points, read through the identification of those points with the value ring.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam_val_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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (A : CommAlgCat ℤ) (t : Multiplicative ↑A) (z : TensorProduct ℤ ↑A ↥M) : ↑((kostantRootSubgroupParam e h ρ M hM i hnil A) t) z = (baseChangeExp (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M ⋯ (Multiplicative.toAdd t)) z

The parametrized root-subgroup element acts through the corresponding base-changed divided-power exponential.

theorem TauCeti.UniversalEnvelopingAlgebra.mapScalarExtensionAutomorphisms_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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A B : CommAlgCat ℤ} (φ : A ⟶ B) (t : Multiplicative ↑A) : (CategoryTheory.ConcreteCategory.hom (GeneralLinear.mapScalarExtensionAutomorphisms φ)) ((kostantRootSubgroupParam e h ρ M hM i hnil A) t) = (kostantRootSubgroupParam e h ρ M hM i hnil B) (Multiplicative.ofAdd ((CommAlgCat.Hom.hom φ) (Multiplicative.toAdd t)))

Scalar extension of automorphisms along a morphism of value rings carries the root-subgroup element with parameter t to the one with parameter φ t.

This is the bundled form of the naturality statement map_kostantRootSubgroupPoints_algHom: the elementwise intertwining relation characterizes the extended automorphism.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantElementarySubgroup {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)))) (A : CommAlgCat ℤ) : Subgroup (LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥M))

The elementary group of the Kostant-stable lattice M over a value ring A: the subgroup of Aut_A(A ⊗[ℤ] M) generated by all root-subgroup elements.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam_mem_kostantElementarySubgroup {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)))) (A : CommAlgCat ℤ) (i : I) (t : Multiplicative ↑A) : (kostantRootSubgroupParam e h ρ M hM i ⋯ A) t ∈ kostantElementarySubgroup e h ρ M hM hnil A

Every root-subgroup element belongs to the elementary group.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementarySubgroup_eq_closure {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)))) (A : CommAlgCat ℤ) : kostantElementarySubgroup e h ρ M hM hnil A = Subgroup.closure (⋃ (i : I), Set.range ⇑(kostantRootSubgroupParam e h ρ M hM i ⋯ A))

The elementary group is generated by the root-subgroup elements.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantElementarySubgroup_le_of_map_param {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)))) {A B : CommAlgCat ℤ} (f : LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥M) →* LinearMap.GeneralLinearGroup (↑B) (TensorProduct ℤ ↑B ↥M)) (σ : I → I) (τ : Multiplicative ↑A → Multiplicative ↑B) (hf : ∀ (i : I) (t : Multiplicative ↑A), f ((kostantRootSubgroupParam e h ρ M hM i ⋯ A) t) = (kostantRootSubgroupParam e h ρ M hM (σ i) ⋯ B) (τ t)) : Subgroup.map f (kostantElementarySubgroup e h ρ M hM hnil A) ≤ kostantElementarySubgroup e h ρ M hM hnil B

A homomorphism carrying every parametrized root-subgroup element to another such element carries the generated elementary group into the target elementary group.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantElementarySubgroup_eq_of_map_param_of_surjective {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)))) {A B : CommAlgCat ℤ} (f : LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥M) →* LinearMap.GeneralLinearGroup (↑B) (TensorProduct ℤ ↑B ↥M)) (σ : I → I) (τ : Multiplicative ↑A → Multiplicative ↑B) (hf : ∀ (i : I) (t : Multiplicative ↑A), f ((kostantRootSubgroupParam e h ρ M hM i ⋯ A) t) = (kostantRootSubgroupParam e h ρ M hM (σ i) ⋯ B) (τ t)) (hσ : Function.Surjective σ) (hτ : Function.Surjective τ) : Subgroup.map f (kostantElementarySubgroup e h ρ M hM hnil A) = kostantElementarySubgroup e h ρ M hM hnil B

If the index and parameter maps are surjective, a homomorphism with the specified action on root-subgroup elements carries the elementary group onto the target elementary group.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantElementarySubgroup_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)))) {A B : CommAlgCat ℤ} (φ : A ⟶ B) : Subgroup.map (GrpCat.Hom.hom (GeneralLinear.mapScalarExtensionAutomorphisms φ)) (kostantElementarySubgroup e h ρ M hM hnil A) ≤ kostantElementarySubgroup e h ρ M hM hnil B

Scalar extension along a morphism of value rings carries the elementary group into the elementary group.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantElementarySubgroup_of_surjective {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)))) {A B : CommAlgCat ℤ} (φ : A ⟶ B) (hφ : Function.Surjective ⇑(CommAlgCat.Hom.hom φ)) : Subgroup.map (GrpCat.Hom.hom (GeneralLinear.mapScalarExtensionAutomorphisms φ)) (kostantElementarySubgroup e h ρ M hM hnil A) = kostantElementarySubgroup e h ρ M hM hnil B

A surjective morphism of value rings carries the elementary group onto the elementary group: every generator of the target is the image of a generator.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantElementaryMap {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)))) {A B : CommAlgCat ℤ} (φ : A ⟶ B) : ↥(kostantElementarySubgroup e h ρ M hM hnil A) →* ↥(kostantElementarySubgroup e h ρ M hM hnil B)

The group homomorphism between elementary groups induced by a morphism of value rings.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.val_kostantElementaryMap {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)))) {A B : CommAlgCat ℤ} (φ : A ⟶ B) (g : ↥(kostantElementarySubgroup e h ρ M hM hnil A)) : ↑((kostantElementaryMap e h ρ M hM hnil φ) g) = (CategoryTheory.ConcreteCategory.hom (GeneralLinear.mapScalarExtensionAutomorphisms φ)) ↑g

The induced homomorphism acts by scalar extension of automorphisms.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryMap_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)))) {A B : CommAlgCat ℤ} (φ : A ⟶ B) (i : I) (t : Multiplicative ↑A) : ↑((kostantElementaryMap e h ρ M hM hnil φ) ⟨(kostantRootSubgroupParam e h ρ M hM i ⋯ A) t, ⋯⟩) = (kostantRootSubgroupParam e h ρ M hM i ⋯ B) (Multiplicative.ofAdd ((CommAlgCat.Hom.hom φ) (Multiplicative.toAdd t)))

The induced homomorphism sends a root-subgroup element to the root-subgroup element with the transported parameter.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryMap_id {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)))) (A : CommAlgCat ℤ) : kostantElementaryMap e h ρ M hM hnil (CategoryTheory.CategoryStruct.id A) = MonoidHom.id ↥(kostantElementarySubgroup e h ρ M hM hnil A)

The identity morphism of value rings induces the identity of elementary groups.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryMap_comp {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)))) {A B C : CommAlgCat ℤ} (φ : A ⟶ B) (ψ : B ⟶ C) : kostantElementaryMap e h ρ M hM hnil (CategoryTheory.CategoryStruct.comp φ ψ) = (kostantElementaryMap e h ρ M hM hnil ψ).comp (kostantElementaryMap e h ρ M hM hnil φ)

Induced homomorphisms of elementary groups compose.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFunctor {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)))) : CategoryTheory.Functor (CommAlgCat ℤ) GrpCat

The elementary group as a group-valued functor on commutative rings.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFunctor_obj {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)))) (A : CommAlgCat ℤ) : (kostantElementaryFunctor e h ρ M hM hnil).obj A = ↧↥(kostantElementarySubgroup e h ρ M hM hnil A)

The object part of the elementary-group functor is the subgroup generated by the Kostant root subgroups.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFunctor_map {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)))) {A B : CommAlgCat ℤ} (φ : A ⟶ B) : (kostantElementaryFunctor e h ρ M hM hnil).map φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (GrpCat.ofHom (kostantElementaryMap e h ρ M hM hnil φ)) (CategoryTheory.eqToHom ⋯))

The map part of the elementary-group functor is scalar extension restricted to the generated subgroups.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFunctorInclusion {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)))) : kostantElementaryFunctor e h ρ M hM hnil ⟶ GeneralLinear.scalarExtensionAutomorphismsFunctor

The elementary group is a subfunctor of the automorphisms of scalar extensions of M.

Equations

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

noncomputable def TauCeti.UniversalEnvelopingAlgebra.iterateFrobeniusValueHom (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] : A ⟶ A

The p ^ n-power Frobenius as an endomorphism of the value ring.

Equations

• TauCeti.UniversalEnvelopingAlgebra.iterateFrobeniusValueHom p n A = CommAlgCat.ofHom (let __src := iterateFrobenius (↑A) p n; { toRingHom := __src, commutes' := ⋯ })

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.iterateFrobeniusValueHom_apply (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] (x : ↑A) : (CommAlgCat.Hom.hom (iterateFrobeniusValueHom p n A)) x = x ^ p ^ n

The Frobenius endomorphism of the value ring raises elements to their p ^ n-th powers.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.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)))) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] : ↥(kostantElementarySubgroup e h ρ M hM hnil A) →* ↥(kostantElementarySubgroup e h ρ M hM hnil A)

The p ^ n-power Frobenius endomorphism of the elementary group of a value ring of exponential characteristic p.

This is the endomorphism of the group of points from which a Steinberg endomorphism is built: over an algebraic closure of 𝔽_p and with p ^ n = q, it is the standard q-power Frobenius.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFrobenius_eq_kostantElementaryMap {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)))) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] : kostantElementaryFrobenius e h ρ M hM hnil p n A = kostantElementaryMap e h ρ M hM hnil (iterateFrobeniusValueHom p n A)

The Frobenius endomorphism of the elementary group is induced by the Frobenius endomorphism of the value ring.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFrobenius_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)))) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] (i : I) (t : Multiplicative ↑A) : ↑((kostantElementaryFrobenius e h ρ M hM hnil 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 Frobenius endomorphism raises the parameter of a root-subgroup element to the p ^ n-th power.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFrobenius_zero {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)))) (p : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] : kostantElementaryFrobenius e h ρ M hM hnil p 0 A = MonoidHom.id ↥(kostantElementarySubgroup e h ρ M hM hnil A)

The zeroth Frobenius iterate is the identity.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFrobenius_add {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)))) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] (m : ℕ) : kostantElementaryFrobenius e h ρ M hM hnil p (n + m) A = (kostantElementaryFrobenius e h ρ M hM hnil p n A).comp (kostantElementaryFrobenius e h ρ M hM hnil p m A)

Frobenius iterates add under composition.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFrobenius_mul {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)))) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] (k : ℕ) : (have this := kostantElementaryFrobenius e h ρ M hM hnil p n A; this) ^ k = kostantElementaryFrobenius e h ρ M hM hnil p (n * k) A

Iterating the p ^ n-power Frobenius k times gives the p ^ (n * k)-power Frobenius.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryMap_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)))) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] {B : CommAlgCat ℤ} [ExpChar (↑B) p] (φ : A ⟶ B) (g : ↥(kostantElementarySubgroup e h ρ M hM hnil A)) : (kostantElementaryMap e h ρ M hM hnil φ) ((kostantElementaryFrobenius e h ρ M hM hnil p n A) g) = (kostantElementaryFrobenius e h ρ M hM hnil p n B) ((kostantElementaryMap e h ρ M hM hnil φ) g)

The Frobenius endomorphism of the elementary group commutes with base change of the value ring, because a ring homomorphism preserves p ^ n-th powers.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFrobenius_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)))) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] [IsReduced ↑A] : Function.Injective ⇑(kostantElementaryFrobenius e h ρ M hM hnil p n A)

The Frobenius endomorphism of the elementary group is injective over a reduced value ring.

The lattice M sits inside a rational vector space, hence is flat over ℤ, so an injective endomorphism of the value ring stays injective after tensoring with M; an automorphism of a scalar extension is determined by its values on the canonical copy of M.