The full-weight type-C carrier scheme

This file feeds the standard type-C Chevalley generators, integral lattice, and full set of weights into the Kostant toral-closure construction. It defines the carrier, its numbered root subgroups and weight torus, their bundled matrix-valued points, and the scheme-level pinning relation.

The file does not prove that the carrier is reductive, that its weight torus is maximal, or that it is the separately constructed symplectic group scheme.

Main definitions

• TauCeti.SpStd.groupScheme: the carrier, cut out of the general linear group by TauCeti.SpStd.definingIdeal, with its closed immersion TauCeti.SpStd.carrierι.
• TauCeti.SpStd.rootSubgroup and TauCeti.SpStd.weightTorus: the numbered root subgroups and the split weight torus, each a closed immersion into the carrier.
• TauCeti.SpStd.points, TauCeti.SpStd.rootSubgroupPoints and TauCeti.SpStd.weightTorusPoints: the corresponding groups of matrix-valued points.

Main results

• TauCeti.SpStd.groupScheme_hom_ext: a morphism from the carrier to the affine group scheme of a commutative Hopf algebra is determined by its restrictions to the numbered root subgroups and the weight torus.
• TauCeti.SpStd.weightTorus_conj_rootSubgroup: the pinning equation, conjugation by the weight torus rescales each numbered root subgroup by its root character.

The pinned carrier

noncomputable def TauCeti.SpStd.definingIdeal (n : ℕ) : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ (n + 1 + (n + 1)))

The Hopf ideal cutting out the full-weight type-C_(n+1) carrier inside the standard general linear group.

Equations

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

theorem TauCeti.SpStd.definingIdeal_def (n : ℕ) : definingIdeal n = UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n)

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

@[reducible, inline]

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

The full-weight Chevalley carrier of type C_(n+1), obtained as the smallest closed subgroup of the standard general linear group containing its numbered root subgroups and weight torus.

Equations

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

theorem TauCeti.SpStd.groupScheme_def (n : ℕ) : groupScheme n = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra ℤ (n + 1 + (n + 1))) (definingIdeal n)

The quotient-spectrum presentation of the full-weight type-C_(n+1) carrier.

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

The canonical inclusion of the type-C_(n+1) carrier into its ambient general linear group.

Equations

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

theorem TauCeti.SpStd.carrierι_def (n : ℕ) : carrierι n = UniversalEnvelopingAlgebra.kostantToralGroupSchemeι (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n)

The ambient inclusion is the one supplied by the generic Kostant toral-closure construction.

theorem TauCeti.SpStd.carrierι_eq_eqToHom_comp_hopfIdealInclusion (n : ℕ) : carrierι n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (GeneralLinear.hopfIdealInclusion ℤ (n + 1 + (n + 1)) (definingIdeal n))

The carrier inclusion expressed through its named Hopf-ideal quotient presentation.

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

The type-C_(n+1) carrier is a closed subgroup scheme of its ambient general linear group.

noncomputable def TauCeti.SpStd.rootSubgroup (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : AdditiveGroup.groupScheme ℤ ⟶ groupScheme n

A numbered root subgroup of the type C_(n+1) carrier.

Equations

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

theorem TauCeti.SpStd.rootSubgroup_def (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : rootSubgroup n k = UniversalEnvelopingAlgebra.kostantRootSubgroupToToral (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) k

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

noncomputable def TauCeti.SpStd.weightTorus (n : ℕ) : SplitTorus.groupScheme ℤ (Fin (n + 1)) ⟶ groupScheme n

The rank-n+1 split weight torus in the type C_(n+1) 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.SpStd.weightTorus_def (n : ℕ) : weightTorus n = UniversalEnvelopingAlgebra.kostantWeightTorusToToral (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n)

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

@[simp]

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

Including a numbered root subgroup into the ambient general linear group recovers its represented Kostant root subgroup.

@[simp]

theorem TauCeti.SpStd.weightTorus_comp_carrierι (n : ℕ) : CategoryTheory.CategoryStruct.comp (weightTorus n) (carrierι n) = GeneralLinear.weightTorus (basisWeight n)

Including the split weight torus into the ambient general linear group recovers the torus of the standard-module weights.

theorem TauCeti.SpStd.groupScheme_hom_ext (n : ℕ) {Y : CommHopfAlgCat ℤ} (φ ψ : groupScheme n ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (k : Fin (n + 1) ⊕ Fin (n + 1)), CategoryTheory.CategoryStruct.comp (rootSubgroup n k) φ = CategoryTheory.CategoryStruct.comp (rootSubgroup n k) ψ) (htorus : CategoryTheory.CategoryStruct.comp (weightTorus n) φ = CategoryTheory.CategoryStruct.comp (weightTorus n) ψ) : φ = ψ

Two morphisms from the type-C_(n+1) carrier to the affine group scheme of a commutative Hopf ℤ-algebra Y agree when they agree on every numbered root subgroup and on the split weight torus.

theorem TauCeti.SpStd.groupScheme_hom_ext_iff {n : ℕ} {Y : CommHopfAlgCat ℤ} {φ ψ : groupScheme n ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)} : φ = ψ ↔ (∀ (k : Fin (n + 1) ⊕ Fin (n + 1)), CategoryTheory.CategoryStruct.comp (rootSubgroup n k) φ = CategoryTheory.CategoryStruct.comp (rootSubgroup n k) ψ) ∧ CategoryTheory.CategoryStruct.comp (weightTorus n) φ = CategoryTheory.CategoryStruct.comp (weightTorus n) ψ

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

The matrix-valued points of the type C_(n+1) carrier.

Equations

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

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

The points of the type-C_(n+1) carrier are cut out by its defining Hopf ideal.

@[simp]

theorem TauCeti.SpStd.mem_points_iff (n : ℕ) (A : Type v) [CommRing A] (g : GL (Fin (n + 1 + (n + 1))) A) : g ∈ points n A ↔ ∀ x ∈ definingIdeal n, ((GeneralLinear.pointsMulEquiv (n + 1 + (n + 1))).symm g).ofConv x = 0

A matrix is a point of the type-C_(n+1) carrier exactly when its associated convolution point kills the carrier's defining Hopf ideal.

noncomputable def TauCeti.SpStd.rootSubgroupPoints (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (A : Type v) [CommRing A] : Multiplicative A →* ↥(points n A)

The parametrized numbered root subgroup inside the type-C_(n+1) 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.SpStd.coe_rootSubgroupPoints (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑((rootSubgroupPoints n k A) u) = (UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ k ⋯ (latticeBasis n)) (AdditiveGroup.gaPointsMulEquiv.symm u)

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

noncomputable def TauCeti.SpStd.weightTorusPoints (n : ℕ) (A : Type v) [CommRing A] : (Fin (n + 1) → Aˣ) →* ↥(points n A)

The split weight torus inside the type-C_(n+1) carrier points.

Equations

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

@[simp]

theorem TauCeti.SpStd.coe_weightTorusPoints (n : ℕ) (A : Type v) [CommRing A] (s : Fin (n + 1) → Aˣ) : ↑((weightTorusPoints n A) s) = (UniversalEnvelopingAlgebra.kostantTorusMatrix (lattice n).toAddSubgroup (latticeBasis n) (basisWeight n)) s

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

theorem TauCeti.SpStd.rootSubgroupCoordinateMap_surjective (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) k))

The root-subgroup coordinate map remains surjective after adjoining the weight torus.

instance TauCeti.SpStd.isClosedImmersion_rootSubgroup (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (rootSubgroup n k).hom.hom)

Every numbered root subgroup is a closed copy of the additive group.

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

The full-weight torus is a closed immersion into the type C_(n+1) carrier.

@[simp]

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

The scheme-level pinning equation: conjugation by the weight torus acts on each numbered root subgroup through the corresponding row of the type-C Cartan matrix, with negative rows on lowering generators.