The type-C carrier in the pinned symplectic model

A validated type-C index of rank r is built on the explicit full-weight standard symplectic carrier TauCeti.SpStd.groupScheme at TauCeti.TypeCLieIndex.carrierRank, which is r - 1, while the reference group of the diagram is the group of algebraic-closure-valued points of the symplectic group scheme Sp_{2r} over ℤ. This file identifies those two groups, matches their Bourbaki-numbered simple-root subgroups, and shows that the identification intertwines the carrier's Steinberg endomorphism with entrywise q-power Frobenius on the pinned points, defined independently of the carrier.

The comparison goes through the standard symplectic matrix group, which both sides realize with the same underlying matrix: the carrier through TauCeti.SpStd.pointsMulEquivGLSymplecticFin, and the scheme points through TauCeti.Symplectic.schemePointsMulEquiv. Both groups are formed at carrierRank + 1, which is r by TauCeti.TypeCLieIndex.carrierRank_add_one, so that the carrier comparison is the identity on matrices. The numbering needs no adapter: the carrier numbers its generators node for node by the Bourbaki numbering of Cᵣ, the final node r - 1 carrying the long simple root 2eᵣ₋₁ and every other node i the adjacent difference root eᵢ - eᵢ₊₁.

Nothing here asserts that the fixed-point group of either Steinberg map is finite, perfect, or simple.

Main definitions

• TauCeti.TypeCLieIndex.StandardGroup: the standard symplectic matrix group.
• TauCeti.TypeCLieIndex.PinnedGroup and TauCeti.TypeCLieIndex.pinnedEquivSymplectic: the pinned scheme points and their matrix realization.
• TauCeti.TypeCLieIndex.carrierEquivSymplectic and TauCeti.TypeCLieIndex.carrierEquivPinned: the equivalences from the explicit carrier.
• TauCeti.TypeCLieIndex.symplecticRootIndex, TauCeti.TypeCLieIndex.symplecticSimpleRootSubgroup and TauCeti.TypeCLieIndex.pinnedSimpleRootSubgroup: the symplectic root and the root subgroups at a Bourbaki-numbered simple root of Cᵣ.
• TauCeti.TypeCLieIndex.symplecticFrobenius and TauCeti.TypeCLieIndex.pinnedFrobenius: the entrywise q-power Frobenius on the matrix group and on the pinned scheme points.

Main results

• TauCeti.TypeCLieIndex.carrierNode_eq_last_iff and TauCeti.TypeCLieIndex.symplecticRootIndex_of_isLongSimpleRoot: the long simple root sits at the final carrier node, where the symplectic root is the long root 2eᵣ₋₁; every other node carries a difference root, by TauCeti.TypeCLieIndex.symplecticRootIndex_of_carrierNode_ne_last.
• TauCeti.TypeCLieIndex.carrierEquivPinned_simpleRootSubgroup: the equivalence matches the numbered simple-root subgroups.
• TauCeti.TypeCLieIndex.symplecticFrobenius_symplecticSimpleRootSubgroup and TauCeti.TypeCLieIndex.pinnedFrobenius_pinnedSimpleRootSubgroup: each Frobenius raises the parameter of a numbered simple-root element to the q-th power.
• TauCeti.TypeCLieIndex.carrierEquivPinned_frobenius and TauCeti.TypeCLieIndex.carrierEquivPinned_steinberg: the equivalence intertwines the carrier Frobenius and Steinberg map with the pinned Frobenius.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 11.3.
• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate III.

The organization follows the rank-two comparison in TauCeti.GroupTheory.SpecificGroups.CFSG.TypeB.Two.Agreement and the type-A comparison in TauCeti.GroupTheory.SpecificGroups.CFSG.TypeA.Agreement.

The two realizations of the symplectic group

@[reducible, inline]

abbrev TauCeti.TypeCLieIndex.StandardGroup (d : TypeCLieIndex) : Type

The standard symplectic matrix group Sp_{2r} over the algebraic closure of the index's prime field, formed at carrierRank + 1 = r.

Equations

• d.StandardGroup = ↥(TauCeti.GLSymplecticFin (d.carrierRank + 1) (↑d).Closure)

@[reducible, inline]

noncomputable abbrev TauCeti.TypeCLieIndex.PinnedGroup (d : TypeCLieIndex) : Type

The algebraic-closure-valued points of the pinned symplectic group scheme Sp_{2r} over ℤ, formed at carrierRank + 1 = r.

Equations

• d.PinnedGroup = ((AlgebraicGeometry.Spec ↧(↑d).Closure).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (TauCeti.Symplectic.groupScheme ℤ (d.carrierRank + 1)).X)

noncomputable def TauCeti.TypeCLieIndex.pinnedEquivSymplectic (d : TypeCLieIndex) : d.PinnedGroup ≃* d.StandardGroup

The canonical matrix realization of the pinned symplectic scheme points.

Equations

• d.pinnedEquivSymplectic = TauCeti.Symplectic.schemePointsMulEquiv (d.carrierRank + 1) (↑d).Closure

noncomputable def TauCeti.TypeCLieIndex.carrierEquivSymplectic (d : TypeCLieIndex) : d.AmbientGroup ≃* d.StandardGroup

The explicit type-C carrier is the standard symplectic matrix group. The equivalence preserves the underlying matrix.

Equations

• d.carrierEquivSymplectic = TauCeti.SpStd.pointsMulEquivGLSymplecticFin d.carrierRank (↑d).Closure

noncomputable def TauCeti.TypeCLieIndex.carrierEquivPinned (d : TypeCLieIndex) : d.AmbientGroup ≃* d.PinnedGroup

The explicit type-C carrier is equivalent to the points of the pinned Sp_{2r}/ℤ group scheme.

Equations

• d.carrierEquivPinned = d.carrierEquivSymplectic.trans d.pinnedEquivSymplectic.symm

The numbered simple root subgroups on the symplectic side

theorem TauCeti.TypeCLieIndex.carrierNode_eq_last_iff (d : TypeCLieIndex) (i : Fin (↑d).rank) : d.carrierNode i = Fin.last d.carrierRank ↔ (↑d).dynkinType.IsLongSimpleRoot i

The long simple root sits at the final carrier node. In the Bourbaki numbering of Cᵣ the long simple root is the last node r - 1, and carrierNode moves no node value.

noncomputable def TauCeti.TypeCLieIndex.symplecticRootIndex (d : TypeCLieIndex) (i : Fin (↑d).rank) : GLSymplecticFin.RootSubgroupIndex (d.carrierRank + 1)

The symplectic root at the Bourbaki-numbered simple root i of Cᵣ: the positive long root 2eᵣ₋₁ at the final node, and the adjacent difference root eᵢ - eᵢ₊₁ at every other node.

Equations

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

theorem TauCeti.TypeCLieIndex.symplecticRootIndex_of_carrierNode_eq_last (d : TypeCLieIndex) {i : Fin (↑d).rank} (hi : d.carrierNode i = Fin.last d.carrierRank) : d.symplecticRootIndex i = GLSymplecticFin.RootSubgroupIndex.positiveLong (Fin.last d.carrierRank)

The symplectic root at the final carrier node is the positive long root 2eᵣ₋₁.

theorem TauCeti.TypeCLieIndex.symplecticRootIndex_of_carrierNode_ne_last (d : TypeCLieIndex) {i : Fin (↑d).rank} (hi : d.carrierNode i ≠ Fin.last d.carrierRank) : d.symplecticRootIndex i = GLSymplecticFin.RootSubgroupIndex.difference (d.carrierNode i) (Order.succ (d.carrierNode i)) ⋯

The symplectic root at a nonfinal carrier node is the adjacent difference root.

theorem TauCeti.TypeCLieIndex.symplecticRootIndex_of_isLongSimpleRoot (d : TypeCLieIndex) {i : Fin (↑d).rank} (hi : (↑d).dynkinType.IsLongSimpleRoot i) : d.symplecticRootIndex i = GLSymplecticFin.RootSubgroupIndex.positiveLong (Fin.last d.carrierRank)

At a long simple root the symplectic root is the positive long root 2eᵣ₋₁.

noncomputable def TauCeti.TypeCLieIndex.symplecticSimpleRootSubgroup (d : TypeCLieIndex) (i : Fin (↑d).rank) : Multiplicative (↑d).Closure →* d.StandardGroup

The positive simple-root subgroup of the standard symplectic matrix group at the Bourbaki-numbered node i of Cᵣ.

Equations

• d.symplecticSimpleRootSubgroup i = (d.symplecticRootIndex i).hom

noncomputable def TauCeti.TypeCLieIndex.pinnedSimpleRootSubgroup (d : TypeCLieIndex) (i : Fin (↑d).rank) : Multiplicative (↑d).Closure →* d.PinnedGroup

The positive simple-root subgroup of the pinned symplectic group scheme at the Bourbaki-numbered node i of Cᵣ.

Equations

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

The Frobenius maps on the symplectic side

noncomputable def TauCeti.TypeCLieIndex.symplecticFrobenius (d : TypeCLieIndex) : d.StandardGroup →* d.StandardGroup

Entrywise q-power Frobenius on the standard symplectic matrix group, for q the field order the index records.

Equations

• d.symplecticFrobenius = TauCeti.GLSymplecticFin.map (d.carrierRank + 1) (↑d).Closure (iterateFrobenius (↑d).Closure (↑d).characteristic (↑d).fieldExponent)

noncomputable def TauCeti.TypeCLieIndex.pinnedFrobenius (d : TypeCLieIndex) : d.PinnedGroup →* d.PinnedGroup

The q-power Frobenius on the pinned symplectic scheme points, defined through their canonical matrix realization and independently of the explicit carrier. The type-C family is untwisted, so this is also the pinned Steinberg map, matched with the carrier's by TauCeti.TypeCLieIndex.carrierEquivPinned_steinberg.

Equations

• d.pinnedFrobenius = d.pinnedEquivSymplectic.symm.toMonoidHom.comp (d.symplecticFrobenius.comp d.pinnedEquivSymplectic.toMonoidHom)

The pinned data in the standard matrix realization

@[simp]

theorem TauCeti.TypeCLieIndex.pinnedEquivSymplectic_pinnedSimpleRootSubgroup (d : TypeCLieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.pinnedEquivSymplectic ((d.pinnedSimpleRootSubgroup i) u) = (d.symplecticSimpleRootSubgroup i) u

Under the canonical matrix realization, a pinned simple-root element is its standard symplectic root matrix.

@[simp]

theorem TauCeti.TypeCLieIndex.pinnedEquivSymplectic_pinnedFrobenius (d : TypeCLieIndex) (g : d.PinnedGroup) : d.pinnedEquivSymplectic (d.pinnedFrobenius g) = d.symplecticFrobenius (d.pinnedEquivSymplectic g)

The canonical matrix realization intertwines pinned and matrix Frobenius.

The carrier in the standard matrix realization

@[simp]

theorem TauCeti.TypeCLieIndex.carrierEquivSymplectic_simpleRootSubgroup (d : TypeCLieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.carrierEquivSymplectic ((d.simpleRootSubgroup i) u) = (d.symplecticSimpleRootSubgroup i) u

The carrier equivalence identifies each numbered simple-root subgroup with its standard symplectic root one-parameter subgroup.

@[simp]

theorem TauCeti.TypeCLieIndex.carrierEquivSymplectic_frobenius (d : TypeCLieIndex) (g : d.AmbientGroup) : d.carrierEquivSymplectic (d.frobenius g) = d.symplecticFrobenius (d.carrierEquivSymplectic g)

The carrier equivalence intertwines the two entrywise q-power Frobenius maps.

@[simp]

theorem TauCeti.TypeCLieIndex.symplecticFrobenius_symplecticSimpleRootSubgroup (d : TypeCLieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.symplecticFrobenius ((d.symplecticSimpleRootSubgroup i) u) = (d.symplecticSimpleRootSubgroup i) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ (↑d).fieldOrder))

The matrix Frobenius raises the parameter of a numbered simple-root element to the q-th power, that is, Frob_q (x_i(u)) = x_i(u ^ q).

The comparison with the pinned scheme points

@[simp]

theorem TauCeti.TypeCLieIndex.pinnedEquivSymplectic_carrierEquivPinned (d : TypeCLieIndex) (g : d.AmbientGroup) : d.pinnedEquivSymplectic (d.carrierEquivPinned g) = d.carrierEquivSymplectic g

The pinned comparison, read in the standard matrix realization, is the carrier's own.

@[simp]

theorem TauCeti.TypeCLieIndex.carrierEquivPinned_simpleRootSubgroup (d : TypeCLieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.carrierEquivPinned ((d.simpleRootSubgroup i) u) = (d.pinnedSimpleRootSubgroup i) u

The carrier-to-pinned equivalence matches the numbered simple root subgroups.

@[simp]

theorem TauCeti.TypeCLieIndex.carrierEquivPinned_frobenius (d : TypeCLieIndex) (g : d.AmbientGroup) : d.carrierEquivPinned (d.frobenius g) = d.pinnedFrobenius (d.carrierEquivPinned g)

The carrier-to-pinned equivalence intertwines the two q-power Frobenius maps.

@[simp]

theorem TauCeti.TypeCLieIndex.pinnedFrobenius_pinnedSimpleRootSubgroup (d : TypeCLieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.pinnedFrobenius ((d.pinnedSimpleRootSubgroup i) u) = (d.pinnedSimpleRootSubgroup i) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ (↑d).fieldOrder))

The pinned Frobenius raises the parameter of a numbered simple-root element to the q-th power, that is, F' (x'_i(u)) = x'_i(u ^ q).

@[simp]

theorem TauCeti.TypeCLieIndex.carrierEquivPinned_steinberg (d : TypeCLieIndex) (g : d.AmbientGroup) : d.carrierEquivPinned (d.steinberg g) = d.pinnedFrobenius (d.carrierEquivPinned g)

The carrier Steinberg map agrees with the independently defined pinned q-power Frobenius, the Steinberg map of the untwisted type-C family on the pinned scheme points.