The numbered type C root subgroups sit at the named simple roots

TauCeti.SpStd.groupScheme n is the full-weight Chevalley carrier of type C_(n+1): the closed subgroup scheme of GL_(2n+2) over ℤ generated by the divided-power exponential root subgroups of the Bourbaki-numbered Chevalley generators of sp_(2n+2) together with the weight torus of the standard lattice. The root character by which its split torus rescales the parameter of the k-th numbered subgroup is TauCeti.SpStd.rootGeneratorWeight n k, so far described as a row of CartanMatrix.C (n + 1), which is a table rather than a root datum.

This file names those characters inside a root datum. It shows that the character of the i-th raising subgroup is the i-th simple root of TauCeti.DynkinType.simplyConnectedRootDatum at type C (n + 1) — the uniform pinned datum a consumer reaches holding only a Dynkin type — and that the character of the i-th lowering subgroup is its negative. Rewriting with these two equations turns the carrier's existing torus-conjugation equations, TauCeti.SpStd.torusPoints_conj_rootSubgroupParam and TauCeti.SpStd.weightTorus_conj_rootSubgroup, into equations whose exponent is a named simple root of that datum, which is the form downstream work states its conventions in.

At rank two this has to be said differently, and the last section says it. C 2 is not a valid Dynkin type, so it names no pinned datum; the rank-two root system is carried by B 2, and the identification acquires the swap of the two Bourbaki nodes.

This file constructs no pinning: it exhibits neither a Borel subgroup nor a root subgroup for every root, and packages no pinning datum. Nothing here asserts that the carrier is reductive, that the weight torus is maximal, or that the carrier equals the separately constructed symplectic group scheme. No group below is claimed to be finite or simple.

Main results

• TauCeti.SpStd.rootGeneratorWeight_inl_eq_root_simpleIndex: the root character of the i-th numbered raising subgroup is the i-th simple root of the uniform pinned type-C datum.
• TauCeti.SpStd.rootGeneratorWeight_inr_eq_neg_root_simpleIndex: the root character of the i-th numbered lowering subgroup is the negative of that simple root.
• TauCeti.SpStd.torusPoints_conj_rootSubgroupParam_root_simpleIndex and its negative-root counterpart state the pinning equations on the carrier's matrix-valued points.
• TauCeti.SpStd.weightTorus_conj_rootSubgroup_root_simpleIndex and its negative-root counterpart state the same equations on scheme points.
• TauCeti.SpStd.rootGeneratorWeight_inl_eq_root_simpleIndex_B_two and TauCeti.SpStd.rootGeneratorWeight_inr_eq_neg_root_simpleIndex_B_two: the same two identifications at rank two, where the datum available is that of TauCeti.DynkinType.B 2 and the node numbering is moved by the swap of the two Bourbaki nodes.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4, 7.1, and 11.3.
• J. E. Humphreys, Linear Algebraic Groups, §§26--27.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate III for the type-C numbering and Plate II for the B₂ numbering the rank-two statements are read in.

The statements follow the type-A identifications in TauCeti/Algebra/Lie/SpecialLinear/StandardCarrier/RootDatum.lean, added in TauCetiProject/TauCeti#5198, specialized to the type-C standard carrier.

This advances the "Pinnings" and "Root subgroup maps" targets of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. Its consumer is milestone L0 of TauCetiRoadmap/CFSGStatement/README.md, which requires each carrier to be traceable to DynkinType.simplyConnectedRootDatum through ValidLieTypeIndex.dynkinType.

The numbered root subgroups sit at the named simple roots

Neither identification below is a simp lemma, for the same reason as in the type-A file. Their left-hand sides are already simp-normal: TauCeti.SpStd.rootGeneratorWeight_inl and TauCeti.SpStd.rootGeneratorWeight_inr rewrite an applied rootGeneratorWeight to an entry of CartanMatrix.C (n + 1), and orienting these identifications towards the datum would undo that. The validity hypothesis ht, which naming the datum needs, also occurs only on the right, so simp could not produce it from a matching left-hand side anyway.

theorem TauCeti.SpStd.rootGeneratorWeight_inl_eq_root_simpleIndex (n : ℕ) (ht : (DynkinType.C (n + 1)).Valid) (i : Fin (n + 1)) : rootGeneratorWeight n (Sum.inl i) = ((DynkinType.C (n + 1)).simplyConnectedRootDatum ht).root ((DynkinType.C (n + 1)).simpleIndex ht i)

The i-th raising subgroup sits at the i-th simple root of the uniform pinned type-C datum. This is the dispatcher form consumed by the construction indexed by a Dynkin type.

theorem TauCeti.SpStd.rootGeneratorWeight_inr_eq_neg_root_simpleIndex (n : ℕ) (ht : (DynkinType.C (n + 1)).Valid) (i : Fin (n + 1)) : rootGeneratorWeight n (Sum.inr i) = -((DynkinType.C (n + 1)).simplyConnectedRootDatum ht).root ((DynkinType.C (n + 1)).simpleIndex ht i)

The i-th lowering subgroup sits at the negative of the i-th simple root of the uniform pinned type-C datum.

Pinning equations on matrix-valued points

theorem TauCeti.SpStd.torusPoints_conj_rootSubgroupParam_root_simpleIndex (n : ℕ) (ht : (DynkinType.C (n + 1)).Valid) (i : Fin (n + 1)) (A : CommAlgCat ℤ) (s : Fin (n + 1) → (↑A)ˣ) (u : Multiplicative ↑A) : (torusPoints n A) s * (rootSubgroupParam n (Sum.inl i) A) u * ((torusPoints n A) s)⁻¹ = (rootSubgroupParam n (Sum.inl i) A) (Multiplicative.ofAdd (↑(torusCharacter s (((DynkinType.C (n + 1)).simplyConnectedRootDatum ht).root ((DynkinType.C (n + 1)).simpleIndex ht i))) * Multiplicative.toAdd u))

Conjugation by the full-weight torus rescales the i-th raising root subgroup through the i-th simple root of the pinned type-C_(n+1) datum.

theorem TauCeti.SpStd.torusPoints_conj_rootSubgroupParam_neg_root_simpleIndex (n : ℕ) (ht : (DynkinType.C (n + 1)).Valid) (i : Fin (n + 1)) (A : CommAlgCat ℤ) (s : Fin (n + 1) → (↑A)ˣ) (u : Multiplicative ↑A) : (torusPoints n A) s * (rootSubgroupParam n (Sum.inr i) A) u * ((torusPoints n A) s)⁻¹ = (rootSubgroupParam n (Sum.inr i) A) (Multiplicative.ofAdd (↑(torusCharacter s (-((DynkinType.C (n + 1)).simplyConnectedRootDatum ht).root ((DynkinType.C (n + 1)).simpleIndex ht i))) * Multiplicative.toAdd u))

Conjugation by the full-weight torus rescales the i-th lowering root subgroup through the negative of the i-th simple root of the pinned type-C_(n+1) datum.

Pinning equations on scheme points

theorem TauCeti.SpStd.weightTorus_conj_rootSubgroup_root_simpleIndex (n : ℕ) (ht : (DynkinType.C (n + 1)).Valid) (i : 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 (Sum.inl i)).hom.hom * (CategoryTheory.CategoryStruct.comp s (weightTorus n).hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) (((DynkinType.C (n + 1)).simplyConnectedRootDatum ht).root ((DynkinType.C (n + 1)).simpleIndex ht i))) * u))) (rootSubgroup n (Sum.inl i)).hom.hom

On scheme points, conjugation by the full-weight torus rescales the i-th raising root subgroup through the i-th simple root of the pinned type-C_(n+1) datum.

theorem TauCeti.SpStd.weightTorus_conj_rootSubgroup_neg_root_simpleIndex (n : ℕ) (ht : (DynkinType.C (n + 1)).Valid) (i : 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 (Sum.inr i)).hom.hom * (CategoryTheory.CategoryStruct.comp s (weightTorus n).hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) (-((DynkinType.C (n + 1)).simplyConnectedRootDatum ht).root ((DynkinType.C (n + 1)).simpleIndex ht i))) * u))) (rootSubgroup n (Sum.inr i)).hom.hom

On scheme points, conjugation by the full-weight torus rescales the i-th lowering root subgroup through the negative of the i-th simple root of the pinned type-C_(n+1) datum.

The rank-two carrier and the B₂ datum

TauCeti.SpStd.groupScheme 1 is the rank-two member of the family, and there the two theorems above are unavailable: TauCeti.DynkinType.C 2 is not a valid Dynkin type, so it has no simplyConnectedRootDatum. The rank-two root system these two constructor names share is carried by TauCeti.DynkinType.B 2, and the numbering that matches the two is the swap of the Bourbaki nodes, TauCeti.DynkinType.cartanMatrix_C_two_apply_eq_cartanMatrix_B_two. The two theorems below are therefore the rank-two counterparts of the two above, stated against the B 2 datum and with each node index moved by that swap.

They are not simp lemmas, for the same reasons as their higher-rank counterparts.

theorem TauCeti.SpStd.rootGeneratorWeight_inl_eq_root_simpleIndex_B_two (ht : (DynkinType.B 2).Valid) (i j : Fin 2) : rootGeneratorWeight 1 (Sum.inl i) j = ((DynkinType.B 2).simplyConnectedRootDatum ht).root ((DynkinType.B 2).simpleIndex ht ((Equiv.swap 0 1) i)) ((Equiv.swap 0 1) j)

The i-th raising subgroup of the rank-two carrier sits at the simple root of the pinned B₂ datum numbered by the swapped node. This is the exceptional isomorphism B₂ ≅ C₂ read on the pinned root characters: the character by which the split torus rescales the parameter of the i-th numbered raising subgroup is the simple root of TauCeti.DynkinType.B 2 at the other node.

theorem TauCeti.SpStd.rootGeneratorWeight_inr_eq_neg_root_simpleIndex_B_two (ht : (DynkinType.B 2).Valid) (i j : Fin 2) : rootGeneratorWeight 1 (Sum.inr i) j = -((DynkinType.B 2).simplyConnectedRootDatum ht).root ((DynkinType.B 2).simpleIndex ht ((Equiv.swap 0 1) i)) ((Equiv.swap 0 1) j)

The i-th lowering subgroup of the rank-two carrier sits at the negative of that simple root.