The special isogeny of Sp₄ in characteristic two

Over a field of characteristic two the pinned group of type B₂ = C₂ admits an endomorphism τ that exchanges the two root lengths, raising the parameter of a short simple root subgroup to the defining characteristic and leaving that of a long one alone. It is the special isogeny, and the finite Suzuki groups are cut out by the fixed points of its odd powers. This file constructs τ on TauCeti.GLSymplecticFin 2 R for every commutative ring R of characteristic two, and proves its action on the two simple root subgroups.

The construction

Sp₄ acts on Λ² R⁴, which is free of rank six. The alternating form gives a linear functional φ on that module, and the form read as a bivector gives an invariant element ω. In characteristic two, and only there, φ ω = 2 = 0, so ω lies in the rank-five kernel W = ker φ and the quotient W ⧸ ⟨ω⟩ is free of rank four, carries the induced alternating form, and is acted on by Sp₄. Composing gives Sp₄ → Sp₄, and that composite is the special isogeny.

The four bivectors e₀∧e₁, e₀∧e₃, e₂∧e₃, e₁∧e₂ are a basis of a complement of ⟨ω⟩ in W, because they are exactly the coordinate bivectors on which the form vanishes, ω being supported on the other two. So no correction term is needed when passing to the quotient, and the matrix of the composite in that basis is simply the matrix of 2 × 2 minors of g on those four index pairs. That matrix is Matrix.symplecticSpecialIsogeny. The exterior square is the reason for the construction but is not itself used below, so no exterior power appears.

The order of the four pairs is chosen so that the induced form is again the standard one: the first pairs with the third and the second with the fourth, matching TauCeti.JFin 2 R.

Where characteristic two enters

Multiplicativity fails in odd characteristic. Expanding a minor of a product over the six index pairs, four terms assemble the product of the two minor matrices and the two carried by the pairs (0,2) and (1,3) leave 2 times a product of minors. Characteristic two is what kills that remainder, which is why the construction has no counterpart in odd characteristic. It is used again in each of the results that follow: that the isogeny commutes with the symplectic adjoint, that it carries a symplectic matrix to a symplectic one, and the square relation.

Nothing here concerns fixed points, finiteness or simplicity, and the odd powers τ ^ (2m+1) that cut out the Suzuki groups are not taken. Two properties of τ are recorded independently of each other: its action on the simple root subgroups, raising the parameter of a short one to the second power and leaving that of a long one alone, and the square relation τ ^ 2 = Frob₂. Neither is derived from the other, and nothing below shows that the action on root subgroups determines an endomorphism over an arbitrary commutative ring.

Main definitions

• Matrix.symplecticSpecialIsogeny: the matrix of 2 × 2 minors on the four form-free index pairs.
• TauCeti.specialIsogeny: the resulting endomorphism of TauCeti.GLSymplecticFin 2 R in characteristic two.

Main results

• TauCeti.pairMinor_row_add_eq_neg_jFin and TauCeti.pairMinor_column_add_eq_neg_jFin: the symplectic condition read on minors, along rows and along columns.
• Matrix.symplecticSpecialIsogeny_mul: multiplicativity on symplectic matrices in characteristic two.
• Matrix.symplecticSpecialIsogeny_mul_jFin_mul_transpose: the image of a symplectic matrix is symplectic.
• TauCeti.specialIsogeny_differenceShortRootUnit and TauCeti.specialIsogeny_positiveLongRootTransvectionUnit: the pinning equations τ (x_{e₀-e₁}(t)) = x_{2e₁}(t²) and τ (x_{2e₁}(t)) = x_{e₀-e₁}(t), which exchange the two root lengths with exponent two on the short root and one on the long root, together with TauCeti.specialIsogeny_differenceShortRootUnit_one_zero and TauCeti.specialIsogeny_negativeLongRootTransvectionUnit on the two negative simple roots.
• Matrix.symplecticSpecialIsogeny_symplecticSpecialIsogeny and TauCeti.specialIsogeny_specialIsogeny: the square relation τ ^ 2 = Frob₂, on matrices and on the group, with TauCeti.specialIsogeny_comp_specialIsogeny for the composite of the endomorphism with itself.

References

• R. W. Carter, Simple Groups of Lie Type, §12.3 and §13.4, for the exceptional isogenies and the groups their odd powers cut out.
• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
• On the cohomology of the Ree groups and kernels of exceptional isogenies, arXiv:2108.06291, for the formulation τ ² = Frob_p.

theorem TauCeti.pairMinor_row_add_eq_neg_jFin {R : Type u} [CommRing R] {g : Matrix (Fin 4) (Fin 4) R} (hg : g * JFin 2 R * g.transpose = JFin 2 R) (p : Fin 4 × Fin 4) : g.pairMinor p (0, 2) + g.pairMinor p (1, 3) = -JFin 2 R p.1 p.2

The symplectic condition, read on minors. The two minors supported by the form on a fixed row pair sum to the corresponding entry of the form.

theorem TauCeti.pairMinor_column_add_eq_neg_jFin {R : Type u} [CommRing R] {g : Matrix (Fin 4) (Fin 4) R} (hg : g * JFin 2 R * g.transpose = JFin 2 R) (q : Fin 4 × Fin 4) : g.pairMinor (0, 2) q + g.pairMinor (1, 3) q = -JFin 2 R q.1 q.2

The symplectic condition, read on minors along columns. The two minors supported by the form on a fixed column pair sum to the corresponding entry of the form.

The special isogeny on matrices

def TauCeti.specialIsogenyPair : Fin 4 → Fin 4 × Fin 4

The four coordinate pairs whose 2 × 2 minors carry the special isogeny.

Equations

• TauCeti.specialIsogenyPair = ![(0, 1), (0, 3), (2, 3), (1, 2)]

@[simp]

theorem TauCeti.specialIsogenyPair_zero : specialIsogenyPair 0 = (0, 1)

@[simp]

theorem TauCeti.specialIsogenyPair_one : specialIsogenyPair 1 = (0, 3)

@[simp]

theorem TauCeti.specialIsogenyPair_two : specialIsogenyPair 2 = (2, 3)

@[simp]

theorem TauCeti.specialIsogenyPair_three : specialIsogenyPair 3 = (1, 2)

@[simp]

theorem TauCeti.jFin_specialIsogenyPair_eq_zero {R : Type u} [CommRing R] (i : Fin 4) : JFin 2 R (specialIsogenyPair i).1 (specialIsogenyPair i).2 = 0

The J-supported pairs are exactly the two omitted ones.

def Matrix.symplecticSpecialIsogeny {R : Type u} [CommRing R] (g : Matrix (Fin 4) (Fin 4) R) : Matrix (Fin 4) (Fin 4) R

The matrix of 2 × 2 minors on the four pairs.

Equations

• g.symplecticSpecialIsogeny = Matrix.of fun (i j : Fin 4) => g.pairMinor (TauCeti.specialIsogenyPair i) (TauCeti.specialIsogenyPair j)

@[simp]

theorem Matrix.symplecticSpecialIsogeny_apply {R : Type u} [CommRing R] (g : Matrix (Fin 4) (Fin 4) R) (i j : Fin 4) : g.symplecticSpecialIsogeny i j = g.pairMinor (TauCeti.specialIsogenyPair i) (TauCeti.specialIsogenyPair j)

theorem Matrix.symplecticSpecialIsogeny_mul {R : Type u} [CommRing R] [CharP R 2] {g h : Matrix (Fin 4) (Fin 4) R} (hg : g * TauCeti.JFin 2 R * g.transpose = TauCeti.JFin 2 R) (hh : h * TauCeti.JFin 2 R * h.transpose = TauCeti.JFin 2 R) : (g * h).symplecticSpecialIsogeny = g.symplecticSpecialIsogeny * h.symplecticSpecialIsogeny

The special isogeny is multiplicative on symplectic matrices in characteristic two.

Compatibility with inversion

@[simp]

theorem Matrix.symplecticSpecialIsogeny_one {R : Type u} [CommRing R] : symplecticSpecialIsogeny 1 = 1

The special isogeny fixes the identity.

theorem Matrix.symplecticSpecialIsogeny_neg_jFin_mul_transpose_mul_jFin {R : Type u} [CommRing R] [CharP R 2] (g : Matrix (Fin 4) (Fin 4) R) : (-(TauCeti.JFin 2 R * g.transpose * TauCeti.JFin 2 R)).symplecticSpecialIsogeny = -(TauCeti.JFin 2 R * g.symplecticSpecialIsogeny.transpose * TauCeti.JFin 2 R)

In characteristic two the special isogeny commutes with the symplectic adjoint.

theorem Matrix.symplecticSpecialIsogeny_mul_jFin_mul_transpose {R : Type u} [CommRing R] {g : Matrix (Fin 4) (Fin 4) R} [CharP R 2] (hg : g * TauCeti.JFin 2 R * g.transpose = TauCeti.JFin 2 R) : g.symplecticSpecialIsogeny * TauCeti.JFin 2 R * g.symplecticSpecialIsogeny.transpose = TauCeti.JFin 2 R

The special isogeny of a symplectic matrix is symplectic.

@[simp]

theorem Matrix.symplecticSpecialIsogeny_map {R : Type u} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : Matrix (Fin 4) (Fin 4) R) : (g.map ⇑f).symplecticSpecialIsogeny = g.symplecticSpecialIsogeny.map ⇑f

The minor formula commutes with entrywise application of a ring morphism.

The square of the special isogeny

@[simp]

theorem Matrix.symplecticSpecialIsogeny_symplecticSpecialIsogeny {R : Type u} [CommRing R] {g : Matrix (Fin 4) (Fin 4) R} [CharP R 2] (hg : g * TauCeti.JFin 2 R * g.transpose = TauCeti.JFin 2 R) : g.symplecticSpecialIsogeny.symplecticSpecialIsogeny = g.map fun (x : R) => x ^ 2

The square of the special isogeny is the Frobenius.

The special isogeny as an endomorphism of Sp₄

def TauCeti.specialIsogeny {R : Type u} [CommRing R] [CharP R 2] : ↥(GLSymplecticFin 2 R) →* ↥(GLSymplecticFin 2 R)

The special isogeny of Sp₄ in characteristic two.

Equations

• TauCeti.specialIsogeny = TauCeti.specialIsogenyToMatrix✝.toHomUnits.codRestrict (TauCeti.GLSymplecticFin 2 R) ⋯

@[simp]

theorem TauCeti.coe_specialIsogeny {R : Type u} [CommRing R] [CharP R 2] (M : ↥(GLSymplecticFin 2 R)) : ↑↑(specialIsogeny M) = (↑↑M).symplecticSpecialIsogeny

The matrix underlying the special isogeny is the matrix of 2 × 2 minors.

@[simp]

theorem TauCeti.map_specialIsogeny {R : Type u} [CommRing R] [CharP R 2] {S : Type u_1} [CommRing S] [CharP S 2] (f : R →+* S) (M : ↥(GLSymplecticFin 2 R)) : (GLSymplecticFin.map 2 R f) (specialIsogeny M) = specialIsogeny ((GLSymplecticFin.map 2 R f) M)

The special isogeny is natural in the value ring, so a consumer can transport it along a morphism of characteristic-two rings without unfolding the minor construction.

The action on the simple root subgroups

@[simp]

theorem TauCeti.specialIsogeny_differenceShortRootUnit {R : Type u} [CommRing R] [CharP R 2] (t : R) : specialIsogeny (GLSymplecticFin.differenceShortRootUnit ⋯ t) = GLSymplecticFin.positiveLongRootTransvectionUnit 1 (t ^ 2)

The special isogeny carries the short simple root subgroup to the long one and squares the parameter: τ (x_{e₀-e₁}(t)) = x_{2e₁}(t²).

@[simp]

theorem TauCeti.specialIsogeny_positiveLongRootTransvectionUnit {R : Type u} [CommRing R] [CharP R 2] (t : R) : specialIsogeny (GLSymplecticFin.positiveLongRootTransvectionUnit 1 t) = GLSymplecticFin.differenceShortRootUnit ⋯ t

The special isogeny carries the long simple root subgroup to the short one and keeps the parameter: τ (x_{2e₁}(t)) = x_{e₀-e₁}(t).

@[simp]

theorem TauCeti.specialIsogeny_differenceShortRootUnit_one_zero {R : Type u} [CommRing R] [CharP R 2] (t : R) : specialIsogeny (GLSymplecticFin.differenceShortRootUnit ⋯ t) = GLSymplecticFin.negativeLongRootTransvectionUnit 1 (t ^ 2)

The special isogeny on the negative short simple root subgroup: τ (x_{e₁-e₀}(t)) = x_{-2e₁}(t²).

@[simp]

theorem TauCeti.specialIsogeny_negativeLongRootTransvectionUnit {R : Type u} [CommRing R] [CharP R 2] (t : R) : specialIsogeny (GLSymplecticFin.negativeLongRootTransvectionUnit 1 t) = GLSymplecticFin.differenceShortRootUnit ⋯ t

The special isogeny on the negative long simple root subgroup: τ (x_{-2e₁}(t)) = x_{e₁-e₀}(t).

@[simp]

theorem TauCeti.specialIsogeny_specialIsogeny {R : Type u} [CommRing R] [CharP R 2] (M : ↥(GLSymplecticFin 2 R)) : specialIsogeny (specialIsogeny M) = (GLSymplecticFin.map 2 R (frobenius R 2)) M

The square of the special isogeny is the Frobenius, on the symplectic group.

@[simp]

theorem TauCeti.specialIsogeny_comp_specialIsogeny {R : Type u} [CommRing R] [CharP R 2] : specialIsogeny.comp specialIsogeny = GLSymplecticFin.map 2 R (frobenius R 2)

The square of the special isogeny is the Frobenius, as an identity of monoid homomorphisms, so a consumer can rewrite the composite itself rather than each of its values.