The full-weight type-C carrier preserves the standard alternating form

TauCeti.SpStd.groupScheme n is the explicit full-weight Chevalley carrier of type C_(n+1): the smallest closed subgroup scheme of GL_(2n+2) containing the divided-power exponentials of the Bourbaki-numbered Chevalley generators of sp_(2n+2) together with the weight torus of the standard lattice. This file proves that it sits inside the symplectic group scheme TauCeti.Symplectic.groupScheme, the subgroup scheme of GL_(2n+2) cut out by X J Xᵀ = J.

The proof is the two generator computations the toral-closure construction reduces to. A root generator squares to zero in the standard representation, so its divided-power exponential is 1 + t X for X the integral matrix TauCeti.SpStd.rootIntMatrix of the generator itself; that matrix is skew-adjoint for J because the generator lies in Mathlib's LieAlgebra.Symplectic.sp, and (1 + t X) J (1 + t X)ᵀ = J follows from skew-adjointness together with X ^ 2 = 0. The weight torus contributes a diagonal matrix whose entries at a coordinate and at its symplectic partner are inverse characters, because the standard weights come in the pairs ε_a and -ε_a, and a diagonal matrix preserves J exactly when each such pair multiplies to one.

Only the group-scheme containment is proved here. On points over a field, the reverse inclusion is TauCeti.SpStd.points_eq_GLSymplecticFin in Generation.lean, which uses the symplectic generation theorem. Nothing below claims that the carrier is reductive, that its weight torus is maximal, or that the two group schemes agree; nor does it claim that any group in sight is finite or simple.

Main definitions

• TauCeti.SpStd.rootIntMatrix: the integral matrix of a numbered root generator in the enumerated coordinate basis of the standard lattice.
• TauCeti.SpStd.toSymplectic: the canonical closed immersion from the carrier to Sp_(2n+2).

Main results

• TauCeti.SpStd.rep_rootGenerator_latticeBasis_eq_sum and TauCeti.SpStd.map_rootIntMatrix: that matrix is the matrix of the root generator, on the lattice and after extending scalars to ℚ.
• TauCeti.SpStd.rootIntMatrix_map_mul_JFin_add_eq_zero and TauCeti.SpStd.rootIntMatrix_map_mul_self_eq_zero: it is skew-adjoint for the transported alternating form, and squares to zero, over every value ring.
• TauCeti.SpStd.symplecticDefiningHopfIdeal_le_definingIdeal: the symplectic relations belong to the defining Hopf ideal of the carrier.
• TauCeti.SpStd.mem_GLSymplecticFin_of_mem_points: every matrix point of the carrier preserves the standard alternating form.
• TauCeti.SpStd.toSymplectic_comp_inclusion: composing with Sp_(2n+2) → GL_(2n+2) recovers the carrier inclusion.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 11.3.
• J. E. Humphreys, Linear Algebraic Groups, §§26--27.
• R. Steinberg, Lectures on Chevalley Groups, §3.

The file follows the type-A counterpart TauCeti/Algebra/Lie/SpecialLinear/StandardCarrier/DeterminantOne.lean, which proves the same containment for the special linear group; the class-two exponential computation and the symplectic matrix identities are specific to this file.

This advances Layer 9, "The Chevalley--Demazure construction", of TauCetiRoadmap/ReductiveGroups/README.md: the full-weight type C carrier is now proved to lie in the expected pinned ambient group. Its consumer is milestone L0 of TauCetiRoadmap/CFSGStatement/README.md, which needs a simply connected pinned carrier for the C_n(q) family.

noncomputable def TauCeti.SpStd.rootIntMatrix (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : Matrix (Fin (n + 1 + (n + 1))) (Fin (n + 1 + (n + 1))) ℤ

The integral matrix of a numbered root generator in the enumerated coordinate basis of the standard lattice. Its columns are the coefficients of the images of the basis vectors, which are integral because the generator preserves the lattice.

Equations

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

theorem TauCeti.SpStd.rep_rootGenerator_latticeBasis_eq_sum (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (s : Fin (n + 1 + (n + 1))) : ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator n k))) ↑((latticeBasis n) s) = ∑ r : Fin (n + 1 + (n + 1)), rootIntMatrix n k r s • ↑((latticeBasis n) r)

A numbered root generator acts on a coordinate basis vector by the corresponding column of TauCeti.SpStd.rootIntMatrix.

theorem TauCeti.SpStd.intCast_rootIntMatrix (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (r s : Fin (n + 1 + (n + 1))) : ↑(rootIntMatrix n k r s) = ↑(rootGenerator n k) (finSumFinEquiv.symm r) (finSumFinEquiv.symm s)

Extending an entry of TauCeti.SpStd.rootIntMatrix to ℚ recovers the corresponding entry of the rational matrix of the root generator, at the standard indices enumerated by the coordinate basis.

theorem TauCeti.SpStd.map_rootIntMatrix (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : (rootIntMatrix n k).map Int.cast = (↑(rootGenerator n k)).submatrix ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

TauCeti.SpStd.rootIntMatrix is the reindexed rational matrix of the root generator.

Skew-adjointness and squaring to zero, over ℤ

The two generator matrices preserve the form

theorem TauCeti.SpStd.rootIntMatrix_map_mul_JFin_add_eq_zero (n : ℕ) {A : Type u_1} [CommRing A] (k : Fin (n + 1) ⊕ Fin (n + 1)) : (rootIntMatrix n k).map Int.cast * JFin (n + 1) A + JFin (n + 1) A * ((rootIntMatrix n k).map Int.cast).transpose = 0

A numbered root generator is skew-adjoint for the transported alternating form, over every value ring: X J + J Xᵀ = 0.

theorem TauCeti.SpStd.rootIntMatrix_map_mul_self_eq_zero (n : ℕ) {A : Type u_1} [CommRing A] (k : Fin (n + 1) ⊕ Fin (n + 1)) : (rootIntMatrix n k).map Int.cast * (rootIntMatrix n k).map Int.cast = 0

A numbered root generator squares to zero on the enumerated coordinate basis, over every value ring.

The weight torus preserves the form

The carrier lies in the symplectic group scheme

theorem TauCeti.SpStd.symplecticDefiningHopfIdeal_le_definingIdeal (n : ℕ) : Symplectic.definingHopfIdeal ℤ (n + 1) ≤ definingIdeal n

The symplectic relations belong to the defining Hopf ideal of the full-weight type C_(n+1) carrier. Equivalently, every represented root subgroup and the represented weight torus factor through Sp_(2n+2).

theorem TauCeti.SpStd.mem_GLSymplecticFin_of_mem_points (n : ℕ) {A : Type v} [CommRing A] {g : GL (Fin (n + 1 + (n + 1))) A} (hg : g ∈ points n A) : g ∈ GLSymplecticFin (n + 1) A

Every matrix-valued point of the full-weight type C_(n+1) carrier preserves the standard alternating form.

noncomputable def TauCeti.SpStd.toSymplectic (n : ℕ) : groupScheme n ⟶ Symplectic.groupScheme ℤ (n + 1)

The canonical morphism from the full-weight type C_(n+1) carrier to Sp_(2n+2), induced by the containment of defining Hopf ideals.

Equations

• TauCeti.SpStd.toSymplectic n = TauCeti.CommHopfAlgCat.quotientSpecMapOfLe (TauCeti.GeneralLinear.coordinateHopfAlgebra ℤ (n + 1 + (n + 1))) ⋯

instance TauCeti.SpStd.isClosedImmersion_toSymplectic (n : ℕ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (toSymplectic n).hom.hom)

The canonical morphism from the type C_(n+1) carrier to Sp_(2n+2) is a closed immersion.

@[simp]

theorem TauCeti.SpStd.toSymplectic_comp_inclusion (n : ℕ) : CategoryTheory.CategoryStruct.comp (toSymplectic n) (Symplectic.inclusion ℤ (n + 1)) = carrierι n

Including the type C_(n+1) carrier into Sp_(2n+2) and then into GL_(2n+2) recovers its original ambient closed immersion.