The special isogeny of the rank-two type-C carrier

The rank-two member of the explicit full-weight type-C Chevalley carrier is the ambient group of the two classification-list families on the B₂ diagram, the untwisted B₂(q) and the Suzuki family ²B₂(2^(2m+1)). Over a field of characteristic two its points carry the special isogeny, the endomorphism exchanging the two root lengths whose odd powers cut out the Suzuki groups. This file transports that endomorphism from the symplectic group to the carrier.

The transport is possible because the two point groups coincide: TauCeti.SpStd.points_eq_GLSymplecticFin identifies the carrier's points with the symplectic matrices over any field, so the special isogeny of Sp₄ restricts to an endomorphism of the carrier rather than merely mapping it into a larger group. The four pinning equations and the square relation below are the symplectic-group statements read through that identification.

Main definitions

• TauCeti.SpStd.pointsMulEquivGLSymplecticFin: the all-rank identification of the carrier's points with the symplectic group, specialized here to rank two.
• TauCeti.SpStd.specialIsogeny: the special isogeny of the carrier in characteristic two.

Main results

• TauCeti.SpStd.specialIsogeny_rootSubgroupPoints_inl_zero and its three siblings: the pinning equations on the four numbered simple root subgroups. The short root at the nonfinal node goes to the long root at the final one with the parameter squared, and the long root goes back to the short one with the parameter unchanged, which is the exponent convention 1 on a long simple root and the defining characteristic on a short one.
• TauCeti.SpStd.specialIsogeny_specialIsogeny: the square relation, that the isogeny composed with itself is the Frobenius TauCeti.SpStd.frobenius 1 2 1, transported from the symplectic group along the identification, with TauCeti.SpStd.specialIsogeny_comp_specialIsogeny stating it for the composite endomorphism itself.

What is not here

No fixed-point subgroup is formed, no odd power τ ^ (2m+1) is taken, and nothing is claimed to be finite or simple. The isogeny is built on the carrier alone, with no Lie-type index in sight.

References

• R. W. Carter, Simple Groups of Lie Type, §§12.3 and 13.4.
• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.

noncomputable def TauCeti.SpStd.specialIsogeny (K : Type v) [Field K] [CharP K 2] : ↥(points 1 K) →* ↥(points 1 K)

The special isogeny of the rank-two type-C carrier in characteristic two.

Equations

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

@[simp]

theorem TauCeti.SpStd.coe_specialIsogeny (K : Type v) [Field K] [CharP K 2] (g : ↥(points 1 K)) : ↑↑((specialIsogeny K) g) = (↑↑g).symplecticSpecialIsogeny

The matrix of the carrier's special isogeny is the matrix of 2 × 2 minors.

theorem TauCeti.SpStd.coe_specialIsogeny_gl (K : Type v) [Field K] [CharP K 2] (g : ↥(points 1 K)) : ↑((specialIsogeny K) g) = ↑(TauCeti.specialIsogeny ((pointsMulEquivGLSymplecticFin 1 K) g))

The special isogeny of the carrier, read in the symplectic group.

@[simp]

theorem TauCeti.SpStd.pointsMulEquivGLSymplecticFin_specialIsogeny (K : Type v) [Field K] [CharP K 2] (g : ↥(points 1 K)) : (pointsMulEquivGLSymplecticFin 1 K) ((specialIsogeny K) g) = TauCeti.specialIsogeny ((pointsMulEquivGLSymplecticFin 1 K) g)

The identification intertwines the two special isogenies.

@[simp]

theorem TauCeti.SpStd.specialIsogeny_specialIsogeny (K : Type v) [Field K] [CharP K 2] (g : ↥(points 1 K)) : (specialIsogeny K) ((specialIsogeny K) g) = (frobenius 1 2 1 K) g

The square of the carrier's special isogeny is the Frobenius.

@[simp]

theorem TauCeti.SpStd.specialIsogeny_comp_specialIsogeny (K : Type v) [Field K] [CharP K 2] : (specialIsogeny K).comp (specialIsogeny K) = frobenius 1 2 1 K

The square of the carrier's special isogeny is the Frobenius, as an identity of monoid homomorphisms, so a consumer taking odd powers can rewrite the composite itself.

@[simp]

theorem TauCeti.SpStd.specialIsogeny_rootSubgroupPoints_inl_zero (K : Type v) [Field K] [CharP K 2] (t : K) : (specialIsogeny K) ((rootSubgroupPoints 1 (Sum.inl 0) K) (Multiplicative.ofAdd t)) = (rootSubgroupPoints 1 (Sum.inl (Fin.last 1)) K) (Multiplicative.ofAdd (t ^ 2))

The isogeny carries the short simple root subgroup to the long one, squaring the parameter.

@[simp]

theorem TauCeti.SpStd.specialIsogeny_rootSubgroupPoints_inl_last (K : Type v) [Field K] [CharP K 2] (t : K) : (specialIsogeny K) ((rootSubgroupPoints 1 (Sum.inl (Fin.last 1)) K) (Multiplicative.ofAdd t)) = (rootSubgroupPoints 1 (Sum.inl 0) K) (Multiplicative.ofAdd t)

The isogeny carries the long simple root subgroup to the short one, keeping the parameter.

@[simp]

theorem TauCeti.SpStd.specialIsogeny_rootSubgroupPoints_inr_zero (K : Type v) [Field K] [CharP K 2] (t : K) : (specialIsogeny K) ((rootSubgroupPoints 1 (Sum.inr 0) K) (Multiplicative.ofAdd t)) = (rootSubgroupPoints 1 (Sum.inr (Fin.last 1)) K) (Multiplicative.ofAdd (t ^ 2))

The isogeny on the negative short simple root subgroup.

@[simp]

theorem TauCeti.SpStd.specialIsogeny_rootSubgroupPoints_inr_last (K : Type v) [Field K] [CharP K 2] (t : K) : (specialIsogeny K) ((rootSubgroupPoints 1 (Sum.inr (Fin.last 1)) K) (Multiplicative.ofAdd t)) = (rootSubgroupPoints 1 (Sum.inr 0) K) (Multiplicative.ofAdd t)

The isogeny on the negative long simple root subgroup.