A Kostant root subgroup is a closed copy of the additive group

Let a Kostant integral form act on a rational representation, preserving an integral lattice M with finite basis b. A nilpotent root vector eᵢ then gives the scheme morphism xᵢ : 𝔾ₐ → GLₙ of RootSubgroup.Scheme.Basic. A pinning of a Chevalley--Demazure group needs more than this morphism: the root subgroup has to be a closed subgroup scheme, and it has to be a faithful copy of 𝔾ₐ, so that xᵢ(t) determines t.

Both follow from one extra hypothesis on ρ, M and b, a root step: a pair of basis indices r, s together with a scalar c : ℤ such that

ρ(eᵢ) (b s) = c • b r    and    ρ(eᵢ) (ρ(eᵢ) (b s)) = 0,

with c a unit. The coordinate expansion below is unconditional; the faithfulness and closed-immersion results carry these three assumptions as hypotheses. These assumptions are not derived here from the Kostant form, from the representation, or from the lattice.

The second equation truncates the divided-power exponential in that matrix column, so the (r, s) entry of xᵢ(t) is exactly c t rather than a polynomial of higher degree. Consequently the coordinate Hopf-algebra morphism O(GLₙ) → O(𝔾ₐ) hits the polynomial generator, hence is surjective, and xᵢ is a closed immersion.

A root step is not a normalization that could be arranged by rescaling the basis: it says that the column of eᵢ at b s is a single basis vector with unit coefficient. For the adjoint representation on a Chevalley lattice of a simply laced type the intended witness is s the index of a root vector e_β with β + αᵢ a root and β + 2αᵢ not a root; supplying such a witness is left to the caller in the general construction.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootGeneratorIntMatrix: the represented generator in an integral lattice basis, shared with the matrix construction of TauCeti.Algebra.Lie.Symplectic.StandardCarrier.AlternatingForm.
• TauCeti.UniversalEnvelopingAlgebra.repr_kostantRootSubgroupPoints_baseChange: the coordinates of a root-subgroup point on a base-changed basis vector.
• TauCeti.UniversalEnvelopingAlgebra.repr_kostantRootSubgroupPoints_of_isRootStep: a root step makes one coordinate equal to the parameter, scaled by the unit c.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_apply_of_isRootStep: the same statement read as a matrix entry.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_apply_baseChange_basis_of_action: the class-two exponential formula for an operator with one nonzero basis column.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_eq_transvectionUnit_of_action: a class-two root operator with one nonzero basis column exponentiates to a transvection.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_eq_sum: a nilpotent root operator exponentiates to the finite sum of its integral divided-power matrices.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_eq_one_add_smul and, in the same namespace, map_genericMatrix_kostantRootSubgroupCoordinateMap_eq_one_add_smul: without the single-column hypothesis a square-zero root operator still exponentiates to 1 + t X, on a point and on the generic matrix respectively.
• TauCeti.UniversalEnvelopingAlgebra.map_genericMatrix_eq_kostantRootSubgroupMatrix: the universal additive-group point identifies the image of the generic matrix with the represented root-subgroup matrix.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_injective: the root subgroup is faithfully parametrized by 𝔾ₐ.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap_surjective: the coordinate Hopf-algebra morphism of the root subgroup is surjective.
• TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantRootSubgroup: the root subgroup 𝔾ₐ → GLₙ is a closed immersion.
• TauCeti.UniversalEnvelopingAlgebra.mono_kostantRootSubgroup: it is a monomorphism.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupClosedSubgroup: the resulting closed subgroup scheme of GLₙ.
• TauCeti.UniversalEnvelopingAlgebra.coe_kostantRootSubgroupClosedSubgroup: that closed subgroup is the subobject represented by the root-subgroup morphism.

References

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

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootGeneratorIntMatrix {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) {η : Type u_2} (i : ι) (b : Module.Basis η ℤ ↥M) : Matrix η η ℤ

The integral matrix of a represented root generator in an invariant lattice basis.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootGeneratorIntMatrix e h ρ M hM i b = b.toMatrix fun (s : η) => ⟨(ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s), ⋯⟩

theorem TauCeti.UniversalEnvelopingAlgebra.rep_rootGenerator_basis_eq_sum {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) {η : Type u_2} [Fintype η] (i : ι) (b : Module.Basis η ℤ ↥M) (s : η) : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = ∑ r : η, kostantRootGeneratorIntMatrix e h ρ M hM i b r s • ↑(b r)

A represented root generator acts on each lattice basis vector by its integral matrix column.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootGeneratorIntMatrix_apply_of_eq {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) {η : Type u_2} [DecidableEq η] (i : ι) (b : Module.Basis η ℤ ↥M) {a a' : η} {c : ℤ} (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b a) = c • ↑(b a')) (r : η) : kostantRootGeneratorIntMatrix e h ρ M hM i b r a = if r = a' then c else 0

If a root generator takes the lattice basis vector b a to c • b a', then the a-th column of its integral matrix is supported at a', with entry c there.

theorem TauCeti.UniversalEnvelopingAlgebra.repr_kostantRootSubgroupPoints_baseChange {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} (b : Module.Basis η ℤ ↥M) {A : Type u_3} [CommRing A] (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) (r s : η) : ((Module.Basis.baseChange A b).repr (↑((kostantRootSubgroupPoints e h ρ M hM i hnil) f) ((Module.Basis.baseChange A b) s))) r = ∑ k ∈ Finset.range (nilpotencyClass (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))), (b.repr ((integralDividedPower (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M k ⋯) (b s))) r • Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ k

The coordinates of a root-subgroup point on a base-changed basis vector: the r-th coordinate of xᵢ(t) (1 ⊗ b s) is the divided-power polynomial in t whose coefficients are the r-th coordinates of the integral divided powers of b s.

theorem TauCeti.UniversalEnvelopingAlgebra.repr_kostantRootSubgroupPoints_of_isRootStep {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} (b : Module.Basis η ℤ ↥M) {r s : η} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) {A : Type u_3} [CommRing A] (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : ((Module.Basis.baseChange A b).repr (↑((kostantRootSubgroupPoints e h ρ M hM i hnil) f) ((Module.Basis.baseChange A b) s))) r = c • Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f)

The pinning coordinate of a root subgroup. At a root step, the r-th coordinate of xᵢ(t) (1 ⊗ b s) is the parameter itself, scaled by the unit c. Every higher divided power vanishes on this basis vector, so no higher power of the parameter appears, and the zeroth one contributes b s, which has no r-th coordinate because r ≠ s.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_injective {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} (b : Module.Basis η ℤ ↥M) {r s : η} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) {A : Type u_3} [CommRing A] : Function.Injective ⇑(kostantRootSubgroupPoints e h ρ M hM i hnil)

The root subgroup is a faithful copy of 𝔾ₐ. Distinct parameters give distinct automorphisms of the base-changed lattice.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_apply_of_isRootStep {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} (b : Module.Basis η ℤ ↥M) {r s : η} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) [Fintype η] [DecidableEq η] {A : Type u_3} [CommRing A] (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : ↑((kostantRootSubgroupMatrix e h ρ M hM i hnil b) f) r s = c • Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f)

At a root step, the (r, s) entry of the root-subgroup matrix is the parameter, scaled by the unit c.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_apply_baseChange_basis_of_action {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} (b : Module.Basis η ℤ ↥M) [DecidableEq η] {A : Type u_3} [CommRing A] (source target : η) (hclass : nilpotencyClass (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) = 2) (haction : ∀ (s : η), (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = if s = source then ↑(b target) else 0) (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) (s : η) : ↑((kostantRootSubgroupPoints e h ρ M hM i hnil) f) ((Module.Basis.baseChange A b) s) = (Module.Basis.baseChange A b) s + if s = source then Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) • (Module.Basis.baseChange A b) target else 0

A class-two root operator with one nonzero basis column acts by adding the parameter times that column after base change.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_eq_transvectionUnit_of_action {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} (b : Module.Basis η ℤ ↥M) [Fintype η] [DecidableEq η] {A : Type u_3} [CommRing A] (source target : η) (hne : target ≠ source) (hclass : nilpotencyClass (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) = 2) (haction : ∀ (s : η), (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = if s = source then ↑(b target) else 0) (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : (kostantRootSubgroupMatrix e h ρ M hM i hnil b) f = transvectionUnit hne (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f))

A class-two root operator that sends one basis vector to another and kills all remaining basis vectors exponentiates to the corresponding elementary transvection.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap_X_of_isRootStep {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {r s : Fin n} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) : (CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i hnil b)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv ℤ n) ((GeneralLinear.coordinateRingMap ℤ n) (MvPolynomial.X (r, s)))) = c • (SymmetricAlgebra.ι ℤ ℤ) 1

At a root step, the coordinate morphism of the root subgroup sends the (r, s) generic matrix coordinate to the polynomial generator, scaled by the unit c.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap_surjective {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {r s : Fin n} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i hnil b))

The coordinate morphism of a root subgroup is surjective. Its image is a subalgebra of the polynomial coordinate algebra of 𝔾ₐ containing the generator, hence everything.

theorem TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantRootSubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {r s : Fin n} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantRootSubgroup e h ρ M hM i hnil b).hom.hom)

A Kostant root subgroup is a closed immersion. The one-parameter subgroup xᵢ : 𝔾ₐ → GLₙ identifies 𝔾ₐ with a closed subscheme of GLₙ over ℤ.

theorem TauCeti.UniversalEnvelopingAlgebra.mono_kostantRootSubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {r s : Fin n} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) : CategoryTheory.Mono (kostantRootSubgroup e h ρ M hM i hnil b)

A root subgroup is a monomorphism of group schemes over ℤ.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupClosedSubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {r s : Fin n} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) : ClosedSubgroupScheme (GeneralLinear.groupScheme ℤ n)

The root subgroup as a closed subgroup scheme of GLₙ. This is the subgroup U_αᵢ that a pinning carries: a closed subgroup scheme which the root-subgroup morphism identifies with 𝔾ₐ.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantRootSubgroupClosedSubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {r s : Fin n} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) : ↑(kostantRootSubgroupClosedSubgroup e h ρ M hM i hnil b hc hstep hsq) = CategoryTheory.Subobject.mk (kostantRootSubgroup e h ρ M hM i hnil b)

The root subgroup presents its own closed subgroup. The subobject underlying kostantRootSubgroupClosedSubgroup is the one represented by kostantRootSubgroup itself, so a consumer never has to unfold the bundled definition; the inclusion arrow agrees with kostantRootSubgroup up to CategoryTheory.Subobject.underlyingIso.

theorem TauCeti.UniversalEnvelopingAlgebra.integralDividedPower_zero_basis_eq_sum {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) {η : Type u_2} [Fintype η] [DecidableEq η] (b : Module.Basis η ℤ ↥M) (s : η) : (integralDividedPower (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M 0 ⋯) (b s) = ∑ r : η, 1 r s • b r

The zeroth divided power has the identity matrix in an integral lattice basis.

theorem TauCeti.UniversalEnvelopingAlgebra.integralDividedPower_basis_eq_sum {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) {η : Type u_2} [Fintype η] (b : Module.Basis η ℤ ↥M) (k : ℕ) (X : Matrix η η ℤ) (haction : ∀ (s : η), (Associative.dividedPower k (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) ↑(b s) = ∑ r : η, X r s • ↑(b r)) (s : η) : (integralDividedPower (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M k ⋯) (b s) = ∑ r : η, X r s • b r

A divided power has the prescribed matrix in an integral lattice basis.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_eq_sum {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} [Fintype η] [DecidableEq η] (b : Module.Basis η ℤ ↥M) {A : Type u_3} [CommRing A] (d : ℕ) (X : ℕ → Matrix η η ℤ) (hclass : nilpotencyClass (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ≤ d) (haction : ∀ k < d, ∀ (s : η), (integralDividedPower (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M k ⋯) (b s) = ∑ r : η, X k r s • b r) (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : ↑((kostantRootSubgroupMatrix e h ρ M hM i hnil b) f) = ∑ k ∈ Finset.range d, Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ k • (X k).map Int.cast

A nilpotent root-subgroup matrix is the finite divided-power sum. If X k is the integral matrix of the kth divided power for every k < d, and the nilpotency class is at most d, then evaluation at t is ∑ k < d, t ^ k • X k.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_eq_one_add_smul {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} [Fintype η] [DecidableEq η] (b : Module.Basis η ℤ ↥M) {A : Type u_3} [CommRing A] (X : Matrix η η ℤ) (hclass : nilpotencyClass (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ≤ 2) (haction : ∀ (s : η), (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = ∑ r : η, X r s • ↑(b r)) (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : ↑((kostantRootSubgroupMatrix e h ρ M hM i hnil b) f) = 1 + Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) • X.map Int.cast

The matrix of a square-zero root subgroup is 1 + t X. When the root operator squares to zero its divided-power exponential stops after the linear term, so the root-subgroup matrix at parameter t is the identity plus t times the integral matrix X of the operator itself. Unlike TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_eq_transvectionUnit_of_action this does not assume the operator has a single nonzero basis column, so it also covers operators with several nonzero columns, such as the nonfinal root generators of type C.

theorem TauCeti.UniversalEnvelopingAlgebra.map_genericMatrix_eq_kostantRootSubgroupMatrix {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {N : ℕ} (bb : Module.Basis (Fin N) ℤ ↥M) : (GeneralLinear.genericMatrix ℤ N).map ⇑↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i hnil bb)) = ↑((kostantRootSubgroupMatrix e h ρ M hM i hnil bb) (WithConv.toConv (AlgHom.id ℤ ↑(AdditiveGroup.coordinateHopfAlgebra ℤ))))

The generic matrix of a root subgroup is its matrix at the universal point of 𝔾ₐ. The identity of the additive coordinate algebra is a point of 𝔾ₐ over that algebra, and the root-subgroup matrix there is the image of the generic matrix of GL N under the root-subgroup coordinate morphism. A matrix formula proved at every algebra-valued point is read on the coordinate morphism through this equation, which is the only place the universal point is handled.

theorem TauCeti.UniversalEnvelopingAlgebra.map_genericMatrix_kostantRootSubgroupCoordinateMap_eq_one_add_smul {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {N : ℕ} (bb : Module.Basis (Fin N) ℤ ↥M) (X : Matrix (Fin N) (Fin N) ℤ) (hclass : nilpotencyClass (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ≤ 2) (haction : ∀ (s : Fin N), (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(bb s) = ∑ r : Fin N, X r s • ↑(bb r)) : (GeneralLinear.genericMatrix ℤ N).map ⇑↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i hnil bb)) = 1 + (SymmetricAlgebra.ι ℤ ℤ) 1 • X.map Int.cast

The generic matrix of a square-zero root subgroup is 1 + t X. This is TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_eq_one_add_smul read on the coordinate morphism rather than on a point: the entries of the generic matrix of GL N are carried to those of 1 + t X for the parameter t of the universal point of 𝔾ₐ. A consumer that has to check a matrix equation on every algebra-valued point at once evaluates it here instead.