Type-C standard generators and full-weight lattice

For positive rank n + 1, the symplectic Lie algebra sp₂ₙ₊₂ acts on its standard module (Fin (n + 1) ⊕ Fin (n + 1)) → ℚ. This file records its Bourbaki-numbered simple Chevalley generators, their Serre relations, the standard integral lattice, and the standard weights. These data feed the Kostant toral-closure construction in TauCeti.Algebra.Lie.Symplectic.StandardCarrier.Scheme.

For a nonfinal node i, the raising generator is

E_{i,i+1} - E_{-(i+1),-i},

and the final raising generator is E_{n,-n}. The lowering generators are their transposed counterparts. All of these square to zero in the standard representation. Their divided powers therefore preserve the coordinate ℤ-lattice, while the Cartan binomial operators preserve it because the coordinate vectors have integral weights.

The weights of the upper coordinates are ε_i and those of the lower coordinates are -ε_i. In simple-coroot coordinates, the map

(x₀, ..., xₙ) ↦ (x₀ - x₁, ..., xₙ₋₁ - xₙ, xₙ)

is unimodular. Thus the standard weights generate the whole character lattice, unlike the roots of the adjoint carrier. This makes the rank-n + 1 split torus a closed subgroup of the carrier.

This file does not prove reductivity or maximality of the torus, and it does not identify this carrier with the separately constructed symplectic group scheme. Those root-datum and generation statements remain part of Layer 9 of the reductive-groups roadmap. No finite or simple group is asserted here.

Main definitions

• TauCeti.SpStd.rootGenerator and TauCeti.SpStd.cartanGenerator: the numbered type-C Chevalley generators in the symplectic Lie algebra.
• TauCeti.SpStd.rep: the standard representation, extended to the enveloping algebra.
• TauCeti.SpStd.weight and TauCeti.SpStd.rootGeneratorWeight: the integral weights of the standard coordinates and the root characters of the numbered generators.
• TauCeti.SpStd.lattice, TauCeti.SpStd.latticeBasis, and TauCeti.SpStd.basisWeight: the standard admissible lattice, its enumerated coordinate basis, and the weights of that basis.
• TauCeti.SpStd.rootSubgroupParam and TauCeti.SpStd.torusPoints: the parametrized numbered root subgroups and the split weight torus on points of a value algebra.

Main results

• TauCeti.SpStd.isSl2Triple_rootGenerator: the sl₂ triple at each numbered index, from which the higher Serre relations are read off.
• TauCeti.SpStd.isSerreSystem_rootGenerator: the characteristic Chevalley--Serre relations of the numbered generators.
• TauCeti.SpStd.lie_cartanGenerator_rootGenerator: the numbered Cartan generators act on the root generators through the rows of the type-C Cartan matrix.
• TauCeti.SpStd.isNilpotent_rep_rootGenerator and TauCeti.SpStd.nilpotencyClass_rep_rootGenerator: each numbered root generator squares to zero on the standard module, and has nilpotency class exactly two.
• TauCeti.SpStd.intCast_latticeBasis_repr: the coordinate-basis coefficients of a lattice vector are its rational coordinates.
• TauCeti.SpStd.rep_kostantForm_mem_lattice: the Kostant ℤ-form preserves the standard lattice, so the lattice is admissible.
• TauCeti.SpStd.span_range_weight_eq_top: the weights of the standard module generate the full character lattice.
• TauCeti.SpStd.torusPoints_conj_rootSubgroupParam: the pointwise pinning equation.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4, 7.1, and 11.3.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §27, and Linear Algebraic Groups, §§26--27.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate III.

The organization of the carrier API and its applications of the generic Kostant infrastructure follow the type-A standard-carrier implementation in TauCetiProject/TauCeti#4603, commits 998d5984 and f4239801; the symplectic matrices, doubled coordinate action, type-C weight calculation, and their proofs are specific to this file.

This advances the Chevalley--Demazure construction, pinning, and root-subgroup targets of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. Its consumer is milestone L0 of TauCetiRoadmap/CFSGStatement/README.md, which needs a simply connected pinned carrier for every valid Lie-type family.

def TauCeti.SpStd.positiveRootMatrix (n : ℕ) (i : Fin (n + 1)) : Matrix (Fin (n + 1) ⊕ Fin (n + 1)) (Fin (n + 1) ⊕ Fin (n + 1)) ℚ

The matrix of the raising generator attached to a simple root of type C_(n+1).

Equations

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

def TauCeti.SpStd.negativeRootMatrix (n : ℕ) (i : Fin (n + 1)) : Matrix (Fin (n + 1) ⊕ Fin (n + 1)) (Fin (n + 1) ⊕ Fin (n + 1)) ℚ

The matrix of the lowering generator attached to a simple root of type C_(n+1).

Equations

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

theorem TauCeti.SpStd.positiveRootMatrix_mem_sp (n : ℕ) (i : Fin (n + 1)) : positiveRootMatrix n i ∈ LieAlgebra.Symplectic.sp (Fin (n + 1)) ℚ

theorem TauCeti.SpStd.negativeRootMatrix_mem_sp (n : ℕ) (i : Fin (n + 1)) : negativeRootMatrix n i ∈ LieAlgebra.Symplectic.sp (Fin (n + 1)) ℚ

Weights and Cartan generators

def TauCeti.SpStd.weight (n : ℕ) (a : Fin (n + 1) ⊕ Fin (n + 1)) : Fin (n + 1) → ℤ

The integral weight of a standard coordinate vector. Upper coordinates have weight ε_a and lower coordinates have weight -ε_a.

Equations

• TauCeti.SpStd.weight n a = TauCeti.DynkinType.TypeC.signedWeight (((Equiv.boolProdEquivSum (Fin (n + 1))).symm a).2, ((Equiv.boolProdEquivSum (Fin (n + 1))).symm a).1)

@[simp]

theorem TauCeti.SpStd.weight_inl (n : ℕ) (a i : Fin (n + 1)) : weight n (Sum.inl a) i = DynkinType.TypeC.weight (n + 1) (↑a) i

@[simp]

theorem TauCeti.SpStd.weight_inr (n : ℕ) (a i : Fin (n + 1)) : weight n (Sum.inr a) i = -DynkinType.TypeC.weight (n + 1) (↑a) i

def TauCeti.SpStd.cartanGeneratorMatrix (n : ℕ) (i : Fin (n + 1)) : Matrix (Fin (n + 1) ⊕ Fin (n + 1)) (Fin (n + 1) ⊕ Fin (n + 1)) ℚ

The diagonal matrix of the i-th simple coroot in the standard symplectic representation.

Equations

• TauCeti.SpStd.cartanGeneratorMatrix n i = Matrix.diagonal fun (k : Fin (n + 1) ⊕ Fin (n + 1)) => ↑(TauCeti.SpStd.weight n k i)

@[simp]

theorem TauCeti.SpStd.cartanGeneratorMatrix_apply (n : ℕ) (i : Fin (n + 1)) (a b : Fin (n + 1) ⊕ Fin (n + 1)) : cartanGeneratorMatrix n i a b = if a = b then ↑(weight n a i) else 0

The entries of the diagonal matrix of a Cartan generator are the coordinate weights.

theorem TauCeti.SpStd.cartanGeneratorMatrix_mem_sp (n : ℕ) (i : Fin (n + 1)) : cartanGeneratorMatrix n i ∈ LieAlgebra.Symplectic.sp (Fin (n + 1)) ℚ

def TauCeti.SpStd.rootGenerator (n : ℕ) : Fin (n + 1) ⊕ Fin (n + 1) → ↥(LieAlgebra.Symplectic.sp (Fin (n + 1)) ℚ)

The Bourbaki-numbered raising and lowering generators of sp₂ₙ₊₂.

Equations

• TauCeti.SpStd.rootGenerator n (Sum.inl i) = ⟨TauCeti.SpStd.positiveRootMatrix n i, ⋯⟩
• TauCeti.SpStd.rootGenerator n (Sum.inr i) = ⟨TauCeti.SpStd.negativeRootMatrix n i, ⋯⟩

def TauCeti.SpStd.cartanGenerator (n : ℕ) (i : Fin (n + 1)) : ↥(LieAlgebra.Symplectic.sp (Fin (n + 1)) ℚ)

The Bourbaki-numbered Cartan generators in the standard symplectic representation.

Equations

• TauCeti.SpStd.cartanGenerator n i = ⟨TauCeti.SpStd.cartanGeneratorMatrix n i, ⋯⟩

@[simp]

theorem TauCeti.SpStd.val_rootGenerator_inl (n : ℕ) (i : Fin (n + 1)) : ↑(rootGenerator n (Sum.inl i)) = positiveRootMatrix n i

@[simp]

theorem TauCeti.SpStd.val_rootGenerator_inr (n : ℕ) (i : Fin (n + 1)) : ↑(rootGenerator n (Sum.inr i)) = negativeRootMatrix n i

@[simp]

theorem TauCeti.SpStd.val_cartanGenerator (n : ℕ) (i : Fin (n + 1)) : ↑(cartanGenerator n i) = cartanGeneratorMatrix n i

noncomputable def TauCeti.SpStd.rep (n : ℕ) : UniversalEnvelopingAlgebra ℚ ↥(LieAlgebra.Symplectic.sp (Fin (n + 1)) ℚ) →ₐ[ℚ] Module.End ℚ (Fin (n + 1) ⊕ Fin (n + 1) → ℚ)

The standard representation of the symplectic Lie algebra, extended to its enveloping algebra.

Equations

• TauCeti.SpStd.rep n = (LieAlgebra.Symplectic.sp (Fin (n + 1)) ℚ).matrixRepresentation

theorem TauCeti.SpStd.rep_ι_apply (n : ℕ) (x : ↥(LieAlgebra.Symplectic.sp (Fin (n + 1)) ℚ)) (v : Fin (n + 1) ⊕ Fin (n + 1) → ℚ) : ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) x)) v = (↑x).mulVec v

theorem TauCeti.SpStd.rep_cartanGenerator_apply_apply (n : ℕ) (i : Fin (n + 1)) (v : Fin (n + 1) ⊕ Fin (n + 1) → ℚ) (a : Fin (n + 1) ⊕ Fin (n + 1)) : ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (cartanGenerator n i))) v a = ↑(weight n a i) * v a

A Cartan generator acts diagonally on every standard-module vector with the recorded coordinate weight.

def TauCeti.SpStd.rootSource (n : ℕ) : Fin (n + 1) ⊕ Fin (n + 1) → Fin (n + 1) ⊕ Fin (n + 1)

The source coordinate of a numbered root generator: the coordinate on whose basis vector the generator is nonzero with coefficient one.

Equations

• TauCeti.SpStd.rootSource n (Sum.inl i) = if i = Fin.last n then Sum.inr i else Sum.inl (Order.succ i)
• TauCeti.SpStd.rootSource n (Sum.inr i) = Sum.inl i

def TauCeti.SpStd.rootTarget (n : ℕ) : Fin (n + 1) ⊕ Fin (n + 1) → Fin (n + 1) ⊕ Fin (n + 1)

The target coordinate of a numbered root generator: the coordinate carrying the image of the basis vector at rootSource.

Equations

• TauCeti.SpStd.rootTarget n (Sum.inl i) = Sum.inl i
• TauCeti.SpStd.rootTarget n (Sum.inr i) = if i = Fin.last n then Sum.inr i else Sum.inl (Order.succ i)

@[simp]

theorem TauCeti.SpStd.rootSource_inl_last (n : ℕ) : rootSource n (Sum.inl (Fin.last n)) = Sum.inr (Fin.last n)

@[simp]

theorem TauCeti.SpStd.rootSource_inl_of_ne_last (n : ℕ) (i : Fin (n + 1)) (hi : i ≠ Fin.last n) : rootSource n (Sum.inl i) = Sum.inl (Order.succ i)

@[simp]

theorem TauCeti.SpStd.rootSource_inr (n : ℕ) (i : Fin (n + 1)) : rootSource n (Sum.inr i) = Sum.inl i

@[simp]

theorem TauCeti.SpStd.rootTarget_inl (n : ℕ) (i : Fin (n + 1)) : rootTarget n (Sum.inl i) = Sum.inl i

@[simp]

theorem TauCeti.SpStd.rootTarget_inr_last (n : ℕ) : rootTarget n (Sum.inr (Fin.last n)) = Sum.inr (Fin.last n)

@[simp]

theorem TauCeti.SpStd.rootTarget_inr_of_ne_last (n : ℕ) (i : Fin (n + 1)) (hi : i ≠ Fin.last n) : rootTarget n (Sum.inr i) = Sum.inl (Order.succ i)

def TauCeti.SpStd.rootGeneratorWeight (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (j : Fin (n + 1)) : ℤ

The root character of a numbered generator, calculated as target weight minus source weight.

Equations

• TauCeti.SpStd.rootGeneratorWeight n k j = TauCeti.SpStd.weight n (TauCeti.SpStd.rootTarget n k) j - TauCeti.SpStd.weight n (TauCeti.SpStd.rootSource n k) j

theorem TauCeti.SpStd.rootGeneratorWeight_inl_eq_root (n : ℕ) (i : Fin (n + 1)) : rootGeneratorWeight n (Sum.inl i) = (DynkinType.typeCSimplyConnectedRootDatum (n + 1)).root (DynkinType.typeCSimpleIndex (n + 1) i)

The weight difference across a raising generator is the corresponding simple root in the canonical simply connected type-C root datum.

@[simp]

theorem TauCeti.SpStd.rootGeneratorWeight_inl (n : ℕ) (i j : Fin (n + 1)) : rootGeneratorWeight n (Sum.inl i) j = CartanMatrix.C (n + 1) i j

The roots of the raising generators are the rows of the type-C Cartan matrix.

@[simp]

theorem TauCeti.SpStd.rootGeneratorWeight_inr (n : ℕ) (i j : Fin (n + 1)) : rootGeneratorWeight n (Sum.inr i) j = -CartanMatrix.C (n + 1) i j

The roots of the lowering generators are the negatives of the rows of the type-C Cartan matrix.

theorem TauCeti.SpStd.positiveRootMatrix_last (n : ℕ) : positiveRootMatrix n (Fin.last n) = Matrix.single (Sum.inl (Fin.last n)) (Sum.inr (Fin.last n)) 1

The final raising matrix is a single off-diagonal matrix unit.

theorem TauCeti.SpStd.positiveRootMatrix_of_ne_last (n : ℕ) (i : Fin (n + 1)) (hi : i ≠ Fin.last n) : positiveRootMatrix n i = Matrix.single (Sum.inl i) (Sum.inl (Order.succ i)) 1 - Matrix.single (Sum.inr (Order.succ i)) (Sum.inr i) 1

A nonfinal raising matrix is the difference of its upper and lower matrix units.

theorem TauCeti.SpStd.negativeRootMatrix_eq_transpose (n : ℕ) (i : Fin (n + 1)) : negativeRootMatrix n i = (positiveRootMatrix n i).transpose

Each lowering matrix is the transpose of the raising matrix at the same index.

theorem TauCeti.SpStd.negativeRootMatrix_last (n : ℕ) : negativeRootMatrix n (Fin.last n) = Matrix.single (Sum.inr (Fin.last n)) (Sum.inl (Fin.last n)) 1

The final lowering matrix is a single off-diagonal matrix unit.

theorem TauCeti.SpStd.negativeRootMatrix_of_ne_last (n : ℕ) (i : Fin (n + 1)) (hi : i ≠ Fin.last n) : negativeRootMatrix n i = Matrix.single (Sum.inl (Order.succ i)) (Sum.inl i) 1 - Matrix.single (Sum.inr i) (Sum.inr (Order.succ i)) 1

A nonfinal lowering matrix is the difference of its upper and lower matrix units.

theorem TauCeti.SpStd.lie_cartanGenerator_rootGenerator (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (j : Fin (n + 1)) : ⁅cartanGenerator n j, rootGenerator n k⁆ = ↑(rootGeneratorWeight n k j) • rootGenerator n k

The numbered Cartan generators act on the root generators through their recorded root characters, equivalently through the type-C Cartan matrix and its negatives.

The sl₂ triples of the numbered generators

theorem TauCeti.SpStd.isSl2Triple_rootGenerator (n : ℕ) (i : Fin (n + 1)) : IsSl2Triple (cartanGenerator n i) (rootGenerator n (Sum.inl i)) (rootGenerator n (Sum.inr i))

The numbered raising and lowering generators at a common index, together with the Cartan generator at that index, form an sl₂ triple.

theorem TauCeti.SpStd.isSerreSystem_rootGenerator (n : ℕ) : IsSerreSystem ℚ (CartanMatrix.C (n + 1)).transpose (cartanGenerator n) (fun (i : Fin (n + 1)) => rootGenerator n (Sum.inl i)) fun (i : Fin (n + 1)) => rootGenerator n (Sum.inr i)

The standard type-C Chevalley generators satisfy the Serre relations for the transposed Cartan matrix, in the convention used by IsSerreSystem.

def TauCeti.SpStd.rootAction (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (v : Fin (n + 1) ⊕ Fin (n + 1) → ℚ) : Fin (n + 1) ⊕ Fin (n + 1) → ℚ

The action of a numbered simple root generator on the standard module, written in coordinate vectors.

Equations

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

@[simp]

theorem TauCeti.SpStd.rootAction_inl_last (n : ℕ) (v : Fin (n + 1) ⊕ Fin (n + 1) → ℚ) : rootAction n (Sum.inl (Fin.last n)) v = v (Sum.inr (Fin.last n)) • Pi.single (Sum.inl (Fin.last n)) 1

@[simp]

theorem TauCeti.SpStd.rootAction_inl_of_ne_last (n : ℕ) (i : Fin (n + 1)) (hi : i ≠ Fin.last n) (v : Fin (n + 1) ⊕ Fin (n + 1) → ℚ) : rootAction n (Sum.inl i) v = v (Sum.inl (Order.succ i)) • Pi.single (Sum.inl i) 1 - v (Sum.inr i) • Pi.single (Sum.inr (Order.succ i)) 1

@[simp]

theorem TauCeti.SpStd.rootAction_inr_last (n : ℕ) (v : Fin (n + 1) ⊕ Fin (n + 1) → ℚ) : rootAction n (Sum.inr (Fin.last n)) v = v (Sum.inl (Fin.last n)) • Pi.single (Sum.inr (Fin.last n)) 1

@[simp]

theorem TauCeti.SpStd.rootAction_inr_of_ne_last (n : ℕ) (i : Fin (n + 1)) (hi : i ≠ Fin.last n) (v : Fin (n + 1) ⊕ Fin (n + 1) → ℚ) : rootAction n (Sum.inr i) v = v (Sum.inl i) • Pi.single (Sum.inl (Order.succ i)) 1 - v (Sum.inr (Order.succ i)) • Pi.single (Sum.inr i) 1

theorem TauCeti.SpStd.rep_rootGenerator_apply (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (v : Fin (n + 1) ⊕ Fin (n + 1) → ℚ) : ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator n k))) v = rootAction n k v

The standard action of a numbered root generator is the explicit coordinate operation rootAction.

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

Applying a numbered root generator twice in the standard representation gives zero.

theorem TauCeti.SpStd.pow_two_rep_rootGenerator_eq_zero (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : (rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator n k)) ^ 2 = 0

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

theorem TauCeti.SpStd.isNilpotent_rep_rootGenerator (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : IsNilpotent ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator n k)))

Every numbered root generator acts nilpotently on the standard module.

Weight vectors and the standard admissible lattice

theorem TauCeti.SpStd.isCartanWeightVector_single (n : ℕ) (a : Fin (n + 1) ⊕ Fin (n + 1)) : UniversalEnvelopingAlgebra.IsCartanWeightVector (cartanGenerator n) (rep n) (weight n a) (Pi.single a 1)

Every standard coordinate vector is a weight vector for the numbered Cartan generators.

def TauCeti.SpStd.lattice (n : ℕ) : Submodule ℤ (Fin (n + 1) ⊕ Fin (n + 1) → ℚ)

The standard coordinate ℤ-lattice in the symplectic module.

Equations

• TauCeti.SpStd.lattice n = TauCeti.coordinateLattice (Fin (n + 1) ⊕ Fin (n + 1))

@[simp]

theorem TauCeti.SpStd.mem_lattice_iff (n : ℕ) {v : Fin (n + 1) ⊕ Fin (n + 1) → ℚ} : v ∈ lattice n ↔ ∀ (a : Fin (n + 1) ⊕ Fin (n + 1)), ∃ (z : ℤ), ↑z = v a

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

theorem TauCeti.SpStd.single_mem_lattice (n : ℕ) (a : Fin (n + 1) ⊕ Fin (n + 1)) : Pi.single a 1 ∈ lattice n

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

The coordinate basis of the standard lattice, enumerated by a finite interval as required by the matrix carrier construction.

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

Equations

• TauCeti.SpStd.latticeBasis n = (TauCeti.coordinateLatticeBasis (Fin (n + 1) ⊕ Fin (n + 1))).reindex finSumFinEquiv

@[simp]

theorem TauCeti.SpStd.coe_latticeBasis (n : ℕ) (a : Fin (n + 1 + (n + 1))) : ↑((latticeBasis n) a) = Pi.single (finSumFinEquiv.symm a) 1

@[simp]

theorem TauCeti.SpStd.intCast_latticeBasis_repr (n : ℕ) (v : ↥(lattice n).toAddSubgroup) (a : Fin (n + 1 + (n + 1))) : ↑(((latticeBasis n).repr v) a) = ↑v (finSumFinEquiv.symm a)

The coordinate-basis coefficients of a lattice vector are its rational coordinates: extending the a-th coefficient to ℚ recovers the coordinate at the standard index enumerated by a.

def TauCeti.SpStd.basisWeight (n : ℕ) (a : Fin (n + 1 + (n + 1))) : Fin (n + 1) → ℤ

The weight attached to the enumerated coordinate basis.

Equations

• TauCeti.SpStd.basisWeight n a = TauCeti.SpStd.weight n (finSumFinEquiv.symm a)

@[simp]

theorem TauCeti.SpStd.basisWeight_apply (n : ℕ) (a : Fin (n + 1 + (n + 1))) : basisWeight n a = weight n (finSumFinEquiv.symm a)

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

A numbered root generator preserves the standard lattice.

theorem TauCeti.SpStd.rep_kostantForm_mem_lattice (n : ℕ) {u : UniversalEnvelopingAlgebra ℚ ↥(LieAlgebra.Symplectic.sp (Fin (n + 1)) ℚ)} (hu : u ∈ UniversalEnvelopingAlgebra.kostantForm (rootGenerator n) (cartanGenerator n)) {v : Fin (n + 1) ⊕ Fin (n + 1) → ℚ} (hv : v ∈ lattice n) : ((rep n) u) v ∈ lattice n

The standard coordinate lattice is stable under the Kostant integral form: the root generators square to zero and preserve it, and the coordinate vectors have integral weights.

The full weight lattice

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

The weights of the standard symplectic module span the full character lattice.

theorem TauCeti.SpStd.span_range_basisWeight_eq_top (n : ℕ) : Submodule.span ℤ (Set.range (basisWeight n)) = ⊤

Enumerating the coordinate basis does not change the span of its weights.

theorem TauCeti.SpStd.rep_rootGenerator_latticeBasis (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator n k))) ↑((latticeBasis n) (finSumFinEquiv (rootSource n k))) = 1 • ↑((latticeBasis n) (finSumFinEquiv (rootTarget n k)))

A root generator sends its designated coordinate basis vector to the designated target with coefficient one.

theorem TauCeti.SpStd.nilpotencyClass_rep_rootGenerator (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : nilpotencyClass ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator n k))) = 2

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

theorem TauCeti.SpStd.isCartanWeightVector_latticeBasis (n : ℕ) (a : Fin (n + 1 + (n + 1))) : UniversalEnvelopingAlgebra.IsCartanWeightVector (cartanGenerator n) (rep n) (basisWeight n a) ↑((latticeBasis n) a)

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

noncomputable def TauCeti.SpStd.rootSubgroupParam (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (A : CommAlgCat ℤ) : Multiplicative ↑A →* LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥(lattice n).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.SpStd.torusPoints (n : ℕ) (A : CommAlgCat ℤ) : (Fin (n + 1) → (↑A)ˣ) →* LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥(lattice n).toAddSubgroup)

The split weight torus on points of a value algebra.

Equations

• TauCeti.SpStd.torusPoints n A = TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints (TauCeti.SpStd.lattice n).toAddSubgroup (TauCeti.SpStd.latticeBasis n) (TauCeti.SpStd.basisWeight n) ↑A

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

The pointwise pinning equation of the type C_(n+1) 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-C Cartan matrix on a raising generator and its negative on a lowering one.