The full-weight Chevalley carrier of type A

Fix r and let sl_{r+1} act on the standard module Fin (r+1) → ℚ. This file feeds that representation, its coordinate ℤ-lattice and the Bourbaki-numbered Chevalley generators

e_i = E_{i,i+1},    f_i = E_{i+1,i},    h_i = E_{i,i} - E_{i+1,i+1}

into the Kostant toral-closure construction, and so produces an explicit affine group scheme over ℤ for every rank: TauCeti.SlStd.groupScheme, the smallest closed subgroup scheme of GL_{r+1} containing the divided-power exponential root subgroups of those generators together with the weight torus of the standard lattice.

What distinguishes the standard module from the adjoint one is its weights. The Cartan generator h_i acts on the coordinate vector at k by δ_{k,i} - δ_{k,i+1}, so the weights are the ε_k, and TauCeti.SlStd.span_range_weight_eq_top says they generate the whole character lattice Fin r → ℤ of the rank-r split torus, whose cocharacter lattice is spanned by the simple coroots. That character lattice is the weight lattice P of type A_r, whereas the weights of the adjoint module generate only the root lattice Q, of index r + 1 in it. Consequently the split torus of rank r is a closed subgroup of the carrier built here (TauCeti.SlStd.isClosedImmersion_weightTorus), which is the property the pinned simply connected Chevalley--Demazure group of type A_r is asked for and which the adjoint carrier does not have.

The whole ambient Lie algebra used is Mathlib's LieAlgebra.SpecialLinear.sl, and the Kostant form depends only on the numbered generators above, so every carrier below traces back to explicit matrices; no existence or classification theorem is invoked anywhere.

Three things are deliberately not asserted. The carrier is not proved reductive, its torus is not proved maximal, and it is not identified with the special linear group scheme; each needs the generation and root-datum statements that Layer 9 of the reductive-groups roadmap still owes. Nor is any group here claimed to be finite or simple.

Main definitions

• TauCeti.SlStd.rootGenerator and TauCeti.SlStd.cartanGenerator: the Bourbaki-numbered Chevalley generators of sl_{r+1}, as elements of LieAlgebra.SpecialLinear.sl.
• TauCeti.SlStd.rep: the standard representation, extended to the universal enveloping algebra.
• TauCeti.SlStd.weight and TauCeti.SlStd.rootGeneratorWeight: the integral weights of the coordinate vectors and the roots of the numbered generators.
• TauCeti.SlStd.lattice and TauCeti.SlStd.latticeBasis: the standard admissible lattice and its coordinate basis.
• TauCeti.SlStd.definingIdeal and TauCeti.SlStd.definingIdeal_def: the Hopf ideal cutting the carrier out of the coordinate Hopf algebra of GL_{r+1}, in terms of which TauCeti.SlStd.points_def presents its points, together with its characterization as the generic Kostant toral defining ideal.
• TauCeti.SlStd.groupScheme, TauCeti.SlStd.carrierι, TauCeti.SlStd.rootSubgroup, TauCeti.SlStd.weightTorus, TauCeti.SlStd.points, TauCeti.SlStd.rootSubgroupPoints, and TauCeti.SlStd.weightTorusPoints: the carrier, its closed immersion into GL_{r+1}, its pinned generating morphisms, its matrix points, and the parametrized root subgroups and split torus inside those points.

Main results

• TauCeti.SlStd.lie_cartanGenerator_rootGenerator: the numbered Cartan generators act on the numbered root generators through the type A_r Cartan matrix.
• TauCeti.SlStd.isSl2Triple_rootGenerator: the numbered generators at a Bourbaki node form an sl₂ triple, from the identification of them with matrix units of sl_{r+1}.
• TauCeti.SlStd.rep_kostantForm_mem_lattice: the Kostant ℤ-form preserves the standard lattice, so the lattice is admissible.
• TauCeti.SlStd.span_range_weight_eq_top: the weights of the standard module generate the full character lattice.
• TauCeti.SlStd.isClosedImmersion_rootSubgroup and TauCeti.SlStd.isClosedImmersion_weightTorus: the root subgroups and the split torus are closed subgroups of the carrier.
• TauCeti.SlStd.torusPoints_conj_rootSubgroupParam and TauCeti.SlStd.weightTorus_conj_rootSubgroup: the pinning equation t(s) x_k(u) t(s)⁻¹ = x_k(α_k(s) u), on matrix points and on A-valued scheme points after corestriction to the carrier.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §27, and Linear Algebraic Groups, §§26--27, for admissible lattices and the weights that distinguish the simply connected form from the adjoint one.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate I, for the numbering of the type A diagram and the index r + 1 of the root lattice in the weight lattice.

This advances "The Chevalley--Demazure construction", "Pinnings" and "Root subgroup maps" in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, which asks for an explicitly constructed split reductive group scheme over ℤ realizing a root datum, with a torus and root subgroups as data. Its consumer is milestone L0, "pinned ambient groups", of TauCetiRoadmap/CFSGStatement/README.md, whose recipe is computed in the simply connected form and therefore cannot use the adjoint Geck carrier of TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/GeckLattice/GroupScheme.lean.

def TauCeti.SlStd.rootTarget (r : ℕ) : Fin r ⊕ Fin r → Fin (r + 1)

The target coordinate of the numbered raising or lowering generator.

Equations

• TauCeti.SlStd.rootTarget r (Sum.inl i) = i.castSucc
• TauCeti.SlStd.rootTarget r (Sum.inr i) = i.succ

def TauCeti.SlStd.rootSource (r : ℕ) : Fin r ⊕ Fin r → Fin (r + 1)

The source coordinate of the numbered raising or lowering generator.

Equations

• TauCeti.SlStd.rootSource r (Sum.inl i) = i.succ
• TauCeti.SlStd.rootSource r (Sum.inr i) = i.castSucc

@[simp]

theorem TauCeti.SlStd.rootTarget_inl (r : ℕ) (i : Fin r) : rootTarget r (Sum.inl i) = i.castSucc

@[simp]

theorem TauCeti.SlStd.rootTarget_inr (r : ℕ) (i : Fin r) : rootTarget r (Sum.inr i) = i.succ

@[simp]

theorem TauCeti.SlStd.rootSource_inl (r : ℕ) (i : Fin r) : rootSource r (Sum.inl i) = i.succ

@[simp]

theorem TauCeti.SlStd.rootSource_inr (r : ℕ) (i : Fin r) : rootSource r (Sum.inr i) = i.castSucc

theorem TauCeti.SlStd.rootTarget_ne_rootSource (r : ℕ) (k : Fin r ⊕ Fin r) : rootTarget r k ≠ rootSource r k

A numbered root generator moves between two distinct coordinates.

theorem TauCeti.SlStd.odd_rootTarget_add_rootSource (r : ℕ) (k : Fin r ⊕ Fin r) : Odd (↑(rootTarget r k) + ↑(rootSource r k))

The two coordinates of a numbered root generator are adjacent, so their indices have odd sum.

The pinned Chevalley generators

def TauCeti.SlStd.rootGenerator (r : ℕ) (k : Fin r ⊕ Fin r) : ↥(LieAlgebra.SpecialLinear.sl (Fin (r + 1)) ℚ)

The Bourbaki-numbered raising and lowering generators of sl_{r+1}: the matrix unit E_{i, i+1} at Sum.inl i and E_{i+1, i} at Sum.inr i.

Equations

• TauCeti.SlStd.rootGenerator r k = (LieAlgebra.SpecialLinear.single (TauCeti.SlStd.rootTarget r k) (TauCeti.SlStd.rootSource r k) ⋯) 1

def TauCeti.SlStd.cartanGenerator (r : ℕ) (i : Fin r) : ↥(LieAlgebra.SpecialLinear.sl (Fin (r + 1)) ℚ)

The Bourbaki-numbered Cartan generators of sl_{r+1}: the diagonal matrix E_{i,i} - E_{i+1,i+1}.

Equations

• TauCeti.SlStd.cartanGenerator r i = (LieAlgebra.SpecialLinear.singleSubSingle i.castSucc i.succ) 1

@[simp]

theorem TauCeti.SlStd.val_rootGenerator (r : ℕ) (k : Fin r ⊕ Fin r) : ↑(rootGenerator r k) = Matrix.single (rootTarget r k) (rootSource r k) 1

@[simp]

theorem TauCeti.SlStd.val_cartanGenerator (r : ℕ) (i : Fin r) : ↑(cartanGenerator r i) = Matrix.single i.castSucc i.castSucc 1 - Matrix.single i.succ i.succ 1

theorem TauCeti.SlStd.isSl2Triple_rootGenerator (r : ℕ) (i : Fin r) : IsSl2Triple (cartanGenerator r i) (rootGenerator r (Sum.inl i)) (rootGenerator r (Sum.inr i))

The numbered Chevalley generators at a Bourbaki node form an sl₂ triple in sl_{r+1}: they are the matrix units E_{i, i+1}, E_{i+1, i} and the diagonal difference E_{i,i} - E_{i+1,i+1}.

The standard representation

noncomputable def TauCeti.SlStd.rep (r : ℕ) : UniversalEnvelopingAlgebra ℚ ↥(LieAlgebra.SpecialLinear.sl (Fin (r + 1)) ℚ) →ₐ[ℚ] Module.End ℚ (Fin (r + 1) → ℚ)

The standard representation of sl_{r+1} on coordinate vectors, extended to the universal enveloping algebra.

Equations

• TauCeti.SlStd.rep r = (LieAlgebra.SpecialLinear.sl (Fin (r + 1)) ℚ).matrixRepresentation

theorem TauCeti.SlStd.rep_ι_apply (r : ℕ) (x : ↥(LieAlgebra.SpecialLinear.sl (Fin (r + 1)) ℚ)) (v : Fin (r + 1) → ℚ) : ((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) x)) v = (↑x).mulVec v

theorem TauCeti.SlStd.rep_rootGenerator_apply (r : ℕ) (k : Fin r ⊕ Fin r) (v : Fin (r + 1) → ℚ) : ((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator r k))) v = v (rootSource r k) • Pi.single (rootTarget r k) 1

A numbered root generator reads off one coordinate and writes it into another.

theorem TauCeti.SlStd.rep_rootGenerator_single_source (r : ℕ) (k : Fin r ⊕ Fin r) : ((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator r k))) (Pi.single (rootSource r k) 1) = Pi.single (rootTarget r k) 1

A numbered root generator sends the coordinate vector at its source to the one at its target.

theorem TauCeti.SlStd.rep_rootGenerator_rep_rootGenerator_eq_zero (r : ℕ) (k : Fin r ⊕ Fin r) (v : Fin (r + 1) → ℚ) : ((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator r k))) (((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator r k))) v) = 0

Applying a numbered root generator twice to a vector gives zero: it writes into a coordinate it does not read from.

theorem TauCeti.SlStd.pow_two_rep_rootGenerator_eq_zero (r : ℕ) (k : Fin r ⊕ Fin r) : (rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator r k)) ^ 2 = 0

Every numbered root generator squares to zero in the standard representation.

theorem TauCeti.SlStd.isNilpotent_rep_rootGenerator (r : ℕ) (k : Fin r ⊕ Fin r) : IsNilpotent ((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator r k)))

Every numbered root generator acts nilpotently.

theorem TauCeti.SlStd.nilpotencyClass_rep_rootGenerator (r : ℕ) (k : Fin r ⊕ Fin r) : nilpotencyClass ((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator r k))) = 2

Every numbered root generator has nilpotency class exactly two in the standard representation.

Weights and roots

def TauCeti.SlStd.weight (r : ℕ) (k : Fin (r + 1)) (i : Fin r) : ℤ

The integral weight of the k-th standard coordinate vector on the numbered Cartan generators. These are the weights ε₀, …, ε_r of the standard module, written in the basis of fundamental weights.

Equations

• TauCeti.SlStd.weight r k i = (if k = i.castSucc then 1 else 0) - if k = i.succ then 1 else 0

@[simp]

theorem TauCeti.SlStd.weight_def (r : ℕ) (k : Fin (r + 1)) (i : Fin r) : weight r k i = (if k = i.castSucc then 1 else 0) - if k = i.succ then 1 else 0

The standard-module weight in Kronecker-delta form.

theorem TauCeti.SlStd.weight_eq_ite_single_sub_ite_single (r : ℕ) (k : Fin (r + 1)) : weight r k = (if hk : ↑k < r then Pi.single ⟨↑k, hk⟩ 1 else 0) - if hk : 0 < ↑k then Pi.single ⟨↑k - 1, ⋯⟩ 1 else 0

A standard-module weight as the difference of its possible adjacent basis characters.

theorem TauCeti.SlStd.weight_injective (r : ℕ) : Function.Injective (weight r)

The weights of the standard representation of sl_{r+1} are pairwise distinct.

theorem TauCeti.SlStd.sum_weight_eq_zero (r : ℕ) : ∑ k : Fin (r + 1), weight r k = 0

The weights of the standard representation sum to zero.

def TauCeti.SlStd.rootGeneratorWeight (r : ℕ) : Fin r ⊕ Fin r → Fin r → ℤ

The root of a numbered raising or lowering generator, as an integral character of the numbered Cartan generators: the i-th row of the type A Cartan matrix on a raising generator and its negative on a lowering one.

Equations

• TauCeti.SlStd.rootGeneratorWeight r (Sum.inl i) = fun (j : Fin r) => CartanMatrix.A r i j
• TauCeti.SlStd.rootGeneratorWeight r (Sum.inr i) = fun (j : Fin r) => -CartanMatrix.A r i j

@[simp]

theorem TauCeti.SlStd.rootGeneratorWeight_inl (r : ℕ) (i j : Fin r) : rootGeneratorWeight r (Sum.inl i) j = CartanMatrix.A r i j

@[simp]

theorem TauCeti.SlStd.rootGeneratorWeight_inr (r : ℕ) (i j : Fin r) : rootGeneratorWeight r (Sum.inr i) j = -CartanMatrix.A r i j

theorem TauCeti.SlStd.isCartanWeightVector_single (r : ℕ) (k : Fin (r + 1)) : UniversalEnvelopingAlgebra.IsCartanWeightVector (cartanGenerator r) (rep r) (weight r k) (Pi.single k 1)

Every standard coordinate vector is a Cartan weight vector, of the weight recorded by TauCeti.SlStd.weight.

theorem TauCeti.SlStd.lie_cartanGenerator_rootGenerator (r : ℕ) (k : Fin r ⊕ Fin r) (j : Fin r) : ⁅cartanGenerator r j, rootGenerator r k⁆ = ↑(rootGeneratorWeight r k j) • rootGenerator r k

The numbered Cartan generators act on the numbered root generators through the type A Cartan matrix. This is the relation that makes the split torus of the carrier below act on the root subgroup at k through the character TauCeti.SlStd.rootGeneratorWeight r k.

The standard admissible lattice

def TauCeti.SlStd.lattice (r : ℕ) : Submodule ℤ (Fin (r + 1) → ℚ)

The standard ℤ-lattice of the standard sl_{r+1}-module, spanned by the coordinate vectors.

Equations

• TauCeti.SlStd.lattice r = TauCeti.coordinateLattice (Fin (r + 1))

@[simp]

theorem TauCeti.SlStd.mem_lattice_iff (r : ℕ) {v : Fin (r + 1) → ℚ} : v ∈ lattice r ↔ ∀ (i : Fin (r + 1)), ∃ (z : ℤ), ↑z = v i

A vector lies in the standard lattice exactly when all of its coordinates are integers.

theorem TauCeti.SlStd.single_mem_lattice (r : ℕ) (i : Fin (r + 1)) : Pi.single i 1 ∈ lattice r

noncomputable def TauCeti.SlStd.latticeBasis (r : ℕ) : Module.Basis (Fin (r + 1)) ℤ ↥(lattice r).toAddSubgroup

The coordinate basis of the standard lattice.

The carrier subtype and ℤ-module structure of a submodule are definitionally equal to those of its underlying additive subgroup, so the restricted-scalars basis has the displayed target type.

Equations

• TauCeti.SlStd.latticeBasis r = TauCeti.coordinateLatticeBasis (Fin (r + 1))

@[simp]

theorem TauCeti.SlStd.coe_latticeBasis (r : ℕ) (i : Fin (r + 1)) : ↑((latticeBasis r) i) = Pi.single i 1

Stability of the lattice under the Kostant form

theorem TauCeti.SlStd.rep_rootGenerator_mem_lattice (r : ℕ) (k : Fin r ⊕ Fin r) {v : Fin (r + 1) → ℚ} (hv : v ∈ lattice r) : ((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator r k))) v ∈ lattice r

A numbered root generator carries the standard lattice into itself.

theorem TauCeti.SlStd.rep_kostantForm_mem_lattice (r : ℕ) {u : UniversalEnvelopingAlgebra ℚ ↥(LieAlgebra.SpecialLinear.sl (Fin (r + 1)) ℚ)} (hu : u ∈ UniversalEnvelopingAlgebra.kostantForm (rootGenerator r) (cartanGenerator r)) {v : Fin (r + 1) → ℚ} (hv : v ∈ lattice r) : ((rep r) u) v ∈ lattice r

The standard lattice is an admissible lattice: the Kostant ℤ-form presented by the numbered Chevalley generators preserves it. The root generators square to zero on the standard module and preserve the lattice, and the coordinate vectors are weight vectors with integer weights.

The weights generate the full character lattice

theorem TauCeti.SlStd.span_range_weight_eq_top (r : ℕ) : Submodule.span ℤ (Set.range (weight r)) = ⊤

The weights of the standard module generate the full character lattice. This is the property that separates the standard module from the adjoint one, whose weights are the roots and generate the root lattice, of index r + 1. It is what makes the rank-r split torus a closed subgroup of the carrier assembled below.

The pinned carrier of type A_r

theorem TauCeti.SlStd.isCartanWeightVector_latticeBasis (r : ℕ) (k : Fin (r + 1)) : UniversalEnvelopingAlgebra.IsCartanWeightVector (cartanGenerator r) (rep r) (weight r k) ↑((latticeBasis r) k)

Every coordinate basis vector of the standard lattice is a Cartan weight vector.

@[reducible, inline]

noncomputable abbrev TauCeti.SlStd.definingIdeal (r : ℕ) : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ (r + 1))

The Hopf ideal cutting the type A_r carrier out of the coordinate Hopf algebra of GL_{r+1} over ℤ.

Like TauCeti.SlStd.groupScheme below, and like the generic TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme it is cut out of, this is an abbrev: the descent arguments of TauCeti/Algebra/Lie/SpecialLinear/StandardCarrier/GraphAutomorphism.lean feed it straight into the generic Kostant comap lemmas and the generic toral coordinate maps, which are stated for the ideal it names. Consumers that only need to know which ideal this is should rewrite with TauCeti.SlStd.definingIdeal_def rather than unfold it.

Equations

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

theorem TauCeti.SlStd.definingIdeal_def (r : ℕ) : definingIdeal r = UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r)

The defining ideal is the one supplied by the generic Kostant toral-closure construction.

@[reducible, inline]

noncomputable abbrev TauCeti.SlStd.groupScheme (r : ℕ) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))

The full-weight Chevalley carrier of type A_r: the smallest closed subgroup scheme of GL_{r+1} over ℤ containing the divided-power exponential root subgroups of the numbered Chevalley generators of sl_{r+1} and the weight torus of the standard lattice.

Equations

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

noncomputable def TauCeti.SlStd.carrierι (r : ℕ) : groupScheme r ⟶ GeneralLinear.groupScheme ℤ (r + 1)

The canonical closed immersion of the type A_r carrier into GL_{r+1}: the carrier is by construction a closed subgroup scheme of the general linear group scheme of the standard lattice.

Equations

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

theorem TauCeti.SlStd.carrierι_def (r : ℕ) : carrierι r = UniversalEnvelopingAlgebra.kostantToralGroupSchemeι (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r)

The ambient inclusion of the type A_r carrier is the inclusion supplied by the generic Kostant toral-closure construction.

instance TauCeti.SlStd.isClosedImmersion_carrierι (r : ℕ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (carrierι r).hom.hom)

The type A_r carrier is a closed subgroup scheme of GL_{r+1}.

noncomputable def TauCeti.SlStd.rootSubgroup (r : ℕ) (k : Fin r ⊕ Fin r) : AdditiveGroup.groupScheme ℤ ⟶ groupScheme r

The numbered root subgroup x_k : 𝔾ₐ → G of the type A_r carrier.

Equations

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

theorem TauCeti.SlStd.rootSubgroup_def (r : ℕ) (k : Fin r ⊕ Fin r) : rootSubgroup r k = UniversalEnvelopingAlgebra.kostantRootSubgroupToToral (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r) k

The root subgroup is the one supplied by the generic Kostant toral-closure construction.

noncomputable def TauCeti.SlStd.weightTorus (r : ℕ) : SplitTorus.groupScheme ℤ (Fin r) ⟶ groupScheme r

The rank-r split weight torus T → G of the type A_r carrier. Maximality is not asserted here; see the scope disclaimer in the module documentation.

Equations

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

theorem TauCeti.SlStd.weightTorus_def (r : ℕ) : weightTorus r = UniversalEnvelopingAlgebra.kostantWeightTorusToToral (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r)

The weight torus is the one supplied by the generic Kostant toral-closure construction.

@[simp]

theorem TauCeti.SlStd.rootSubgroup_comp_carrierι (r : ℕ) (k : Fin r ⊕ Fin r) : CategoryTheory.CategoryStruct.comp (rootSubgroup r k) (carrierι r) = UniversalEnvelopingAlgebra.kostantRootSubgroup (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ k ⋯ (latticeBasis r)

Including a numbered root subgroup of the type A_r carrier into GL_{r+1} recovers the Kostant root subgroup of the numbered generator.

@[simp]

theorem TauCeti.SlStd.weightTorus_comp_carrierι (r : ℕ) : CategoryTheory.CategoryStruct.comp (weightTorus r) (carrierι r) = GeneralLinear.weightTorus (weight r)

Including the split torus of the type A_r carrier into GL_{r+1} recovers the weight torus of the weights of the standard module.

noncomputable def TauCeti.SlStd.points (r : ℕ) (A : Type v) [CommRing A] : Subgroup (GL (Fin (r + 1)) A)

The A-valued points of the type A_r carrier, as matrices.

Equations

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

theorem TauCeti.SlStd.points_def (r : ℕ) (A : Type v) [CommRing A] : points r A = GeneralLinear.hopfIdealPointsSubgroup (r + 1) (definingIdeal r) A

The points of the type A_r carrier are the invertible matrices cut out by its defining Hopf ideal. This is the presentation the functoriality of the points is read off.

noncomputable def TauCeti.SlStd.rootSubgroupPoints (r : ℕ) (i : Fin r ⊕ Fin r) (A : Type v) [CommRing A] : Multiplicative A →* ↥(points r A)

The parametrized numbered root subgroup inside the type-A_r carrier points. The parameter is read through the canonical multiplicative copy of the additive group of A.

Equations

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

@[simp]

theorem TauCeti.SlStd.coe_rootSubgroupPoints (r : ℕ) (i : Fin r ⊕ Fin r) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑((rootSubgroupPoints r i A) u) = (UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ i ⋯ (latticeBasis r)) (AdditiveGroup.gaPointsMulEquiv.symm u)

The numbered root subgroup point is the corresponding divided-power exponential matrix.

noncomputable def TauCeti.SlStd.weightTorusPoints (r : ℕ) (A : Type v) [CommRing A] : (Fin r → Aˣ) →* ↥(points r A)

The split weight torus inside the type-A_r carrier points.

Equations

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

@[simp]

theorem TauCeti.SlStd.coe_weightTorusPoints (r : ℕ) (A : Type v) [CommRing A] (s : Fin r → Aˣ) : ↑((weightTorusPoints r A) s) = (UniversalEnvelopingAlgebra.kostantTorusMatrix (lattice r).toAddSubgroup (latticeBasis r) (weight r)) s

A split-torus point is the diagonal matrix whose entries are its values on the standard-module weights.

@[simp]

theorem TauCeti.SlStd.mem_points_iff (r : ℕ) (A : Type v) [CommRing A] (g : GL (Fin (r + 1)) A) : g ∈ points r A ↔ ∀ x ∈ UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r), ((GeneralLinear.pointsMulEquiv (r + 1)).symm g).ofConv x = 0

A matrix is a point of the type A_r carrier exactly when the associated convolution point kills its toral defining Hopf ideal.

The pinning

theorem TauCeti.SlStd.rep_rootGenerator_latticeBasis_apply (r : ℕ) (k : Fin r ⊕ Fin r) (s : Fin (r + 1)) : ((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator r k))) ↑((latticeBasis r) s) = if s = rootSource r k then ↑((latticeBasis r) (rootTarget r k)) else 0

A numbered root generator sends its source lattice vector to its target lattice vector and annihilates every other lattice basis vector.

theorem TauCeti.SlStd.rep_rootGenerator_latticeBasis (r : ℕ) (k : Fin r ⊕ Fin r) : ((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator r k))) ↑((latticeBasis r) (rootSource r k)) = 1 • ↑((latticeBasis r) (rootTarget r k))

A numbered root generator carries the coordinate basis vector at its source to the one at its target. This is the root step that makes the root subgroup a closed copy of 𝔾ₐ.

theorem TauCeti.SlStd.rootSubgroupCoordinateMap_surjective (r : ℕ) (k : Fin r ⊕ Fin r) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r) k))

The coordinate morphism of every numbered root subgroup of the type A_r carrier is surjective.

instance TauCeti.SlStd.isClosedImmersion_rootSubgroup (r : ℕ) (k : Fin r ⊕ Fin r) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (rootSubgroup r k).hom.hom)

Every numbered root subgroup of the type A_r carrier is a closed immersion.

instance TauCeti.SlStd.isClosedImmersion_weightTorus (r : ℕ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (weightTorus r).hom.hom)

The split torus of the type A_r carrier is a closed immersion. This is exactly where the full-weight property is used: the weights of the standard module generate the whole character lattice, so the rank-r split torus embeds rather than mapping onto a proper quotient.

noncomputable def TauCeti.SlStd.rootSubgroupParam (r : ℕ) (k : Fin r ⊕ Fin r) (A : CommAlgCat ℤ) : Multiplicative ↑A →* LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥(lattice r).toAddSubgroup)

The parametrized numbered root subgroup on points of a value algebra.

Equations

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

noncomputable def TauCeti.SlStd.torusPoints (r : ℕ) (A : CommAlgCat ℤ) : (Fin r → (↑A)ˣ) →* LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥(lattice r).toAddSubgroup)

The split weight torus on points of a value algebra.

Equations

• TauCeti.SlStd.torusPoints r A = TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints (TauCeti.SlStd.lattice r).toAddSubgroup (TauCeti.SlStd.latticeBasis r) (TauCeti.SlStd.weight r) ↑A

theorem TauCeti.SlStd.torusPoints_conj_rootSubgroupParam (r : ℕ) (k : Fin r ⊕ Fin r) (A : CommAlgCat ℤ) (s : Fin r → (↑A)ˣ) (u : Multiplicative ↑A) : (torusPoints r A) s * (rootSubgroupParam r k A) u * ((torusPoints r A) s)⁻¹ = (rootSubgroupParam r k A) (Multiplicative.ofAdd (↑(torusCharacter s (rootGeneratorWeight r k)) * Multiplicative.toAdd u))

The pinning equation of the type A_r carrier. A torus point s conjugates the root-subgroup element of parameter u into the one of parameter α_k(s) u, where α_k is the k-th row of the type A_r Cartan matrix on a raising generator and its negative on a lowering one.

theorem TauCeti.SlStd.weightTorus_conj_rootSubgroup (r : ℕ) (k : Fin r ⊕ Fin r) (A : Type) [CommRing A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ (Fin r)).X) (u : A) : CategoryTheory.CategoryStruct.comp s (weightTorus r).hom.hom * CategoryTheory.CategoryStruct.comp ((AdditiveGroup.groupSchemePointMulEquiv A) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd u))) (rootSubgroup r k).hom.hom * (CategoryTheory.CategoryStruct.comp s (weightTorus r).hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) (rootGeneratorWeight r k)) * u))) (rootSubgroup r k).hom.hom

The pinning equation on A-valued scheme points of the type A_r carrier. After corestriction to the carrier, conjugation by a split-torus point rescales the parameter of a numbered root subgroup by the corresponding root character.