The full-weight type-C carrier is the symplectic group

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 together with the weight torus of the standard lattice. TauCeti.SpStd.mem_GLSymplecticFin_of_mem_points is the containment in one direction, that every point of the carrier preserves the standard alternating form. This file supplies the other: over a field the two point groups are equal.

The numbered root subgroups

Each numbered root generator squares to zero in the standard representation, so its divided-power exponential is 1 + u X for X the integral matrix TauCeti.SpStd.rootIntMatrix of the generator, which AlternatingForm.lean computes in the enumerated coordinate basis: the single unit E_{i,m+i} at the final node, the difference E_{i,i+1} - E_{m+i+1,m+i} of two units at a nonfinal one. Those are the matrices of the symplectic group's long-root transvection at the terminal coordinate and of its difference short-root element at an adjacent pair, so the carrier's four families of numbered root points are the corresponding elements of TauCeti.GLSymplecticFin, and the terminal coordinate is what makes them the Bourbaki simple roots of type C.

What is not proved

The identifications of the numbered root points hold over every commutative ring; it is the equality of the two point groups that needs a field, and it is asserted only there. Nothing below asserts that the carrier is reductive, that its weight torus is maximal, or that the two group schemes agree.

Main results

• TauCeti.SpStd.rootSubgroupPoints_inl_last_eq_positiveLongRootTransvectionUnit and its three siblings: each numbered root point is the corresponding long-root transvection or difference short-root element of the symplectic group.
• TauCeti.SpStd.points_eq_GLSymplecticFin: the carrier points are exactly the symplectic matrices, over every field.
• TauCeti.SpStd.pointsMulEquivGLSymplecticFin: the resulting multiplicative equivalence, with equations describing both directions on matrices and its action on every numbered simple-root subgroup and the weight torus.

References

The decisive input is formal rather than bibliographic: the generation theorem TauCeti.GLSymplecticFin.eq_top_of_adjacent_of_long, from TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/Symplectic/TorusGeneration.lean, is what reduces the equality of point groups to the four root identifications below.

• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 11.3.
• R. Steinberg, Lectures on Chevalley Groups, §3.

theorem TauCeti.SpStd.rootSubgroupPoints_inl_last_eq_positiveLongRootTransvectionUnit (n : ℕ) {A : Type v} [CommRing A] (u : Multiplicative A) : ↑((rootSubgroupPoints n (Sum.inl (Fin.last n)) A) u) = ↑(GLSymplecticFin.positiveLongRootTransvectionUnit (Fin.last n) (Multiplicative.toAdd u))

The final raising point of the carrier is the positive long-root transvection.

theorem TauCeti.SpStd.rootSubgroupPoints_inr_last_eq_negativeLongRootTransvectionUnit (n : ℕ) {A : Type v} [CommRing A] (u : Multiplicative A) : ↑((rootSubgroupPoints n (Sum.inr (Fin.last n)) A) u) = ↑(GLSymplecticFin.negativeLongRootTransvectionUnit (Fin.last n) (Multiplicative.toAdd u))

The final lowering point of the carrier is the negative long-root transvection.

theorem TauCeti.SpStd.rootSubgroupPoints_inl_eq_differenceShortRootUnit_of_ne_last (n : ℕ) {A : Type v} [CommRing A] (i : Fin (n + 1)) (hi : i ≠ Fin.last n) (u : Multiplicative A) : ↑((rootSubgroupPoints n (Sum.inl i) A) u) = ↑(GLSymplecticFin.differenceShortRootUnit ⋯ (Multiplicative.toAdd u))

A nonfinal raising point of the carrier is the difference short-root element.

theorem TauCeti.SpStd.rootSubgroupPoints_inr_eq_differenceShortRootUnit_of_ne_last (n : ℕ) {A : Type v} [CommRing A] (i : Fin (n + 1)) (hi : i ≠ Fin.last n) (u : Multiplicative A) : ↑((rootSubgroupPoints n (Sum.inr i) A) u) = ↑(GLSymplecticFin.differenceShortRootUnit ⋯ (Multiplicative.toAdd u))

A nonfinal lowering point of the carrier is the opposite difference short-root element.

theorem TauCeti.SpStd.points_eq_GLSymplecticFin (n : ℕ) {K : Type v} [Field K] : points n K = GLSymplecticFin (n + 1) K

The full-weight type-C carrier is the symplectic group over a field. Its points always preserve the standard alternating form, and over a field the numbered root subgroups already generate every symplectic matrix, so the containment is an equality.

The point-group equivalence

noncomputable def TauCeti.SpStd.pointsMulEquivGLSymplecticFin (n : ℕ) (K : Type v) [Field K] : ↥(points n K) ≃* ↥(GLSymplecticFin (n + 1) K)

The full-weight type-C_(n+1) carrier's points are the symplectic group, as a multiplicative equivalence. This packages TauCeti.SpStd.points_eq_GLSymplecticFin in the form needed to transport endomorphisms and subgroups while leaving the underlying matrices unchanged.

Equations

• TauCeti.SpStd.pointsMulEquivGLSymplecticFin n K = MulEquiv.subgroupCongr ⋯

@[simp]

theorem TauCeti.SpStd.coe_pointsMulEquivGLSymplecticFin_apply (n : ℕ) {K : Type v} [Field K] (g : ↥(points n K)) : ↑((pointsMulEquivGLSymplecticFin n K) g) = ↑g

The symplectic element underlying a point of the carrier is that point. This is MulEquiv.subgroupCongr_apply stated for the named equivalence, so that consumers need not unfold TauCeti.SpStd.pointsMulEquivGLSymplecticFin.

@[simp]

theorem TauCeti.SpStd.coe_pointsMulEquivGLSymplecticFin_symm_apply (n : ℕ) {K : Type v} [Field K] (g : ↥(GLSymplecticFin (n + 1) K)) : ↑((pointsMulEquivGLSymplecticFin n K).symm g) = ↑g

The point of the carrier underlying a symplectic element is that element. This is MulEquiv.subgroupCongr_symm_apply stated for the named equivalence.

@[simp]

theorem TauCeti.SpStd.pointsMulEquivGLSymplecticFin_rootSubgroupPoints_inl_last (n : ℕ) {K : Type v} [Field K] (u : Multiplicative K) : (pointsMulEquivGLSymplecticFin n K) ((rootSubgroupPoints n (Sum.inl (Fin.last n)) K) u) = GLSymplecticFin.positiveLongRootTransvectionUnit (Fin.last n) (Multiplicative.toAdd u)

Under the point-group equivalence, the final positive simple-root subgroup is the positive long-root transvection subgroup of the symplectic group.

@[simp]

theorem TauCeti.SpStd.pointsMulEquivGLSymplecticFin_rootSubgroupPoints_inr_last (n : ℕ) {K : Type v} [Field K] (u : Multiplicative K) : (pointsMulEquivGLSymplecticFin n K) ((rootSubgroupPoints n (Sum.inr (Fin.last n)) K) u) = GLSymplecticFin.negativeLongRootTransvectionUnit (Fin.last n) (Multiplicative.toAdd u)

Under the point-group equivalence, the final negative simple-root subgroup is the negative long-root transvection subgroup of the symplectic group.

@[simp]

theorem TauCeti.SpStd.pointsMulEquivGLSymplecticFin_rootSubgroupPoints_inl_of_ne_last (n : ℕ) {K : Type v} [Field K] (i : Fin (n + 1)) (hi : i ≠ Fin.last n) (u : Multiplicative K) : (pointsMulEquivGLSymplecticFin n K) ((rootSubgroupPoints n (Sum.inl i) K) u) = GLSymplecticFin.differenceShortRootUnit ⋯ (Multiplicative.toAdd u)

Under the point-group equivalence, a nonfinal positive simple-root subgroup is the adjacent difference-root subgroup of the symplectic group.

@[simp]

theorem TauCeti.SpStd.pointsMulEquivGLSymplecticFin_rootSubgroupPoints_inr_of_ne_last (n : ℕ) {K : Type v} [Field K] (i : Fin (n + 1)) (hi : i ≠ Fin.last n) (u : Multiplicative K) : (pointsMulEquivGLSymplecticFin n K) ((rootSubgroupPoints n (Sum.inr i) K) u) = GLSymplecticFin.differenceShortRootUnit ⋯ (Multiplicative.toAdd u)

Under the point-group equivalence, a nonfinal negative simple-root subgroup is the opposite adjacent difference-root subgroup of the symplectic group.

@[simp]

theorem TauCeti.SpStd.pointsMulEquivGLSymplecticFin_weightTorusPoints (n : ℕ) {K : Type v} [Field K] (s : Fin (n + 1) → Kˣ) : (pointsMulEquivGLSymplecticFin n K) ((weightTorusPoints n K) s) = GLSymplecticFin.diagonal fun (i : Fin (n + 1)) => torusCharacter s (DynkinType.TypeC.weight (n + 1) ↑i)

Under the point-group equivalence, the carrier's weight torus is the standard paired diagonal torus. Its first-block coordinate at i is the character of the classical type-C weight ε_i; the second block is its inverse.