Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.SpecialIsogeny

The special isogeny selected by a Suzuki--Ree index #

The Steinberg endomorphism of a Suzuki or Ree group is an odd power of the exceptional isogeny of its pinned ambient group. That isogeny exists only for B₂ and F₄ in characteristic two and for G₂ in characteristic three, and this file selects it, on root data, for every TauCeti.SuzukiReeIndex: the Suzuki family takes the special isogeny of the pinned B₂ datum, the Ree G₂ family that of G₂, and the Ree F₄ family together with the Tits index that of F₄.

The point of selecting it here rather than downstream is that the selection carries a convention, and the convention has to be checked against the one the CFSG roadmap fixes. Its exponent assignment attaches 1 to a long simple root and the defining characteristic to a short one, which is a genuine choice: the opposite assignment also squares to the prime-field Frobenius. The upstream isogenies are pinned instead by squared root lengths, and TauCeti.SuzukiReeIndex.datumSpecialIsogeny_exponent_simpleIndex and TauCeti.SuzukiReeIndex.datumSpecialIsogeny_weightMap_root_simpleIndex are the statements that the two agree. In the form the second one takes,

τ (root (σ i)) = exponent i • root i,

the character map is the pullback along the group-scheme isogeny, so the exponent is indexed by the node i whose root subgroup is being raised to a power and not by its image σ i; this is the root-datum shadow of τ (x_{α_i}(t)) = x_{α_{σ i}}(t ^ exponent i).

The permutation of nodes is checked in the same way. TauCeti.SuzukiReeIndex.isSpecialNodePerm_lengthPerm reads the length permutation the index carries as a TauCeti.DynkinType.IsSpecialNodePerm, which is the uniform root-level notion, and TauCeti.SuzukiReeIndex.datumSpecialIsogeny_indexEquiv_simpleIndex says the upstream isogeny permutes the simple-root indices by exactly that permutation. Since a special node permutation is unique when it exists (TauCeti.DynkinType.IsSpecialNodePerm.unique), no second convention can sneak in.

Nothing here is a group. The lift of these three isogenies from root data to the pinned Chevalley--Demazure group schemes, and hence the finite groups themselves, are separate work.

Main definitions #

Main results #

Roadmap and references #

This is the selection half of milestone L2 of TauCetiRoadmap/CFSGStatement/README.md, which owns "selecting τ_X for a given SuzukiReeIndex, checking that the upstream isogeny is the one this roadmap's conventions describe, and taking the odd power" and states its exponent convention against TauCeti.DynkinType.IsLongSimpleRoot. The isogeny selected here is the root-datum half of the target "Special isogenies in characteristics two and three" of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, which owns the isogeny itself. This file is to L2 what TauCeti/GroupTheory/SpecificGroups/CFSG/RootDatumAutomorphism.lean is to L1.

Transport along an equality of root pairings #

The special isogenies are constructed on the pinned data of the family modules, while a Suzuki--Ree index names its datum through TauCeti.DynkinType.simplyConnectedRootDatum. The two are equal, by the branch equations of that dispatcher, but not syntactically so; the transport below reads one as the other. None of the four pieces of data of an isogeny has a type mentioning the root pairing, so the transport moves only its three proof obligations and leaves the data alone.

The selected isogeny #

source
noncomputable def TauCeti.SuzukiReeIndex.datumSpecialIsogeny (e : SuzukiReeIndex) :
RootPairingIsogeny ((↑e).dynkinType.simplyConnectedRootDatum ⋯) ((↑e).dynkinType.simplyConnectedRootDatum ⋯)

The special isogeny of the pinned simply connected root datum selected by a Suzuki--Ree index: the exceptional isogeny of B₂ in characteristic two for the Suzuki family, of G₂ in characteristic three for the Ree G₂ family, and of F₄ in characteristic two for the Ree F₄ family and the Tits index.

The sixteen branch equations below name the selected isogeny on each family, field by field, so no consumer needs this body.

Equations
Instances For

    Branch equations #

    The four pieces of data of an isogeny are recorded one family at a time. Together they determine the selected isogeny, since TauCeti.RootPairingIsogeny is extensional in exactly these four fields.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_weightMap_suzuki (m : ℕ) (hv : (LieTypeIndex.suzuki m).Valid) :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.suzuki m, hv⟩, ⋯⟩).weightMap = DynkinType.b2SpecialIsogeny.weightMap

    The character map of the isogeny selected by a Suzuki index is that of the B₂ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_coweightMap_suzuki (m : ℕ) (hv : (LieTypeIndex.suzuki m).Valid) :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.suzuki m, hv⟩, ⋯⟩).coweightMap = DynkinType.b2SpecialIsogeny.coweightMap

    The cocharacter map of the isogeny selected by a Suzuki index is that of the B₂ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_indexEquiv_suzuki (m : ℕ) (hv : (LieTypeIndex.suzuki m).Valid) :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.suzuki m, hv⟩, ⋯⟩).indexEquiv = DynkinType.b2SpecialIsogeny.indexEquiv

    The root permutation of the isogeny selected by a Suzuki index is that of the B₂ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_exponent_suzuki (m : ℕ) (hv : (LieTypeIndex.suzuki m).Valid) :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.suzuki m, hv⟩, ⋯⟩).exponent = DynkinType.b2SpecialIsogeny.exponent

    The rescaling exponents of the isogeny selected by a Suzuki index are those of the B₂ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_weightMap_reeG2 (m : ℕ) (hv : (LieTypeIndex.reeG2 m).Valid) :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.reeG2 m, hv⟩, ⋯⟩).weightMap = DynkinType.g2SpecialIsogeny.weightMap

    The character map of the isogeny selected by a Ree G₂ index is that of the G₂ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_coweightMap_reeG2 (m : ℕ) (hv : (LieTypeIndex.reeG2 m).Valid) :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.reeG2 m, hv⟩, ⋯⟩).coweightMap = DynkinType.g2SpecialIsogeny.coweightMap

    The cocharacter map of the isogeny selected by a Ree G₂ index is that of the G₂ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_indexEquiv_reeG2 (m : ℕ) (hv : (LieTypeIndex.reeG2 m).Valid) :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.reeG2 m, hv⟩, ⋯⟩).indexEquiv = DynkinType.g2SpecialIsogeny.indexEquiv

    The root permutation of the isogeny selected by a Ree G₂ index is that of the G₂ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_exponent_reeG2 (m : ℕ) (hv : (LieTypeIndex.reeG2 m).Valid) :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.reeG2 m, hv⟩, ⋯⟩).exponent = DynkinType.g2SpecialIsogeny.exponent

    The rescaling exponents of the isogeny selected by a Ree G₂ index are those of the G₂ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_weightMap_reeF4 (m : ℕ) (hv : (LieTypeIndex.reeF4 m).Valid) :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.reeF4 m, hv⟩, ⋯⟩).weightMap = DynkinType.f4SpecialIsogeny.weightMap

    The character map of the isogeny selected by a Ree F₄ index is that of the F₄ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_coweightMap_reeF4 (m : ℕ) (hv : (LieTypeIndex.reeF4 m).Valid) :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.reeF4 m, hv⟩, ⋯⟩).coweightMap = DynkinType.f4SpecialIsogeny.coweightMap

    The cocharacter map of the isogeny selected by a Ree F₄ index is that of the F₄ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_indexEquiv_reeF4 (m : ℕ) (hv : (LieTypeIndex.reeF4 m).Valid) :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.reeF4 m, hv⟩, ⋯⟩).indexEquiv = DynkinType.f4SpecialIsogeny.indexEquiv

    The root permutation of the isogeny selected by a Ree F₄ index is that of the F₄ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_exponent_reeF4 (m : ℕ) (hv : (LieTypeIndex.reeF4 m).Valid) :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.reeF4 m, hv⟩, ⋯⟩).exponent = DynkinType.f4SpecialIsogeny.exponent

    The rescaling exponents of the isogeny selected by a Ree F₄ index are those of the F₄ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_weightMap_tits :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.tits, datumSpecialIsogeny_weightMap_tits._proof_1⟩, datumSpecialIsogeny_weightMap_tits._proof_2⟩).weightMap = DynkinType.f4SpecialIsogeny.weightMap

    The character map of the isogeny selected by the Tits index is that of the F₄ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_coweightMap_tits :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.tits, datumSpecialIsogeny_weightMap_tits._proof_1⟩, datumSpecialIsogeny_weightMap_tits._proof_2⟩).coweightMap = DynkinType.f4SpecialIsogeny.coweightMap

    The cocharacter map of the isogeny selected by the Tits index is that of the F₄ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_indexEquiv_tits :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.tits, datumSpecialIsogeny_weightMap_tits._proof_1⟩, datumSpecialIsogeny_weightMap_tits._proof_2⟩).indexEquiv = DynkinType.f4SpecialIsogeny.indexEquiv

    The root permutation of the isogeny selected by the Tits index is that of the F₄ special isogeny.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_exponent_tits :
    (datumSpecialIsogeny ⟨⟨LieTypeIndex.tits, datumSpecialIsogeny_weightMap_tits._proof_1⟩, datumSpecialIsogeny_weightMap_tits._proof_2⟩).exponent = DynkinType.f4SpecialIsogeny.exponent

    The rescaling exponents of the isogeny selected by the Tits index are those of the F₄ special isogeny.

    The length permutation and the root-length convention #

    source
    theorem TauCeti.SuzukiReeIndex.isSpecialNodePerm_lengthPerm (e : SuzukiReeIndex) :
    (↑e).dynkinType.IsSpecialNodePerm e.lengthPerm

    The pinned length permutation of a Suzuki--Ree index is the special node permutation of its Dynkin type. Both defining conditions are already proved of it: it exchanges long and short simple roots and transposes the Cartan matrix. Since a special node permutation is unique (TauCeti.DynkinType.IsSpecialNodePerm.unique), this leaves no room for a competing length-exchanging convention.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.rootLength_eq_characteristic_of_isLongSimpleRoot (e : SuzukiReeIndex) (i : Fin (↑e).rank) (hi : (↑e).dynkinType.IsLongSimpleRoot i) :
    (↑e).dynkinType.rootLength i = ↑(↑e).characteristic

    A long simple root of a Suzuki--Ree index has squared length the defining characteristic: two for B₂ and F₄, three for G₂.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.rootLength_eq_one_of_not_isLongSimpleRoot (e : SuzukiReeIndex) (i : Fin (↑e).rank) (hi : ¬(↑e).dynkinType.IsLongSimpleRoot i) :
    (↑e).dynkinType.rootLength i = 1

    A short simple root of a Suzuki--Ree index has squared length one: the normalisation of TauCeti.DynkinType.rootLength makes the shorter of the two lengths 1.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.rootLength_lengthPerm (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
    (↑e).dynkinType.rootLength (e.lengthPerm i) = ↑(e.exponent i)

    The exponent convention of the CFSG roadmap is the root-length convention of the root-systems roadmap. The squared length of the node paired with i by the length permutation is the exponent the exceptional isogeny attaches to the root subgroup of i: it is 1 when i is long, because the paired node is then short, and the defining characteristic when i is short.

    The selected isogeny on the simple roots #

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_indexEquiv_simpleIndex (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
    e.datumSpecialIsogeny.indexEquiv ((↑e).dynkinType.simpleIndex ⋯ i) = (↑e).dynkinType.simpleIndex ⋯ (e.lengthPerm i)

    The selected isogeny permutes the simple-root indices by the pinned length permutation. This is the check that the node convention of the upstream isogeny is the one TauCeti.SuzukiReeIndex.lengthPerm fixes.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_exponent_simpleIndex (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
    e.datumSpecialIsogeny.exponent ((↑e).dynkinType.simpleIndex ⋯ i) = (↑e).dynkinType.rootLength i

    The exponent of the selected isogeny at a simple-root index is the squared length of that node. The isogeny's exponent field is indexed by the source of its character map, which is the image node of the group-scheme isogeny; combined with TauCeti.SuzukiReeIndex.rootLength_lengthPerm this is the roadmap's assignment of 1 to a long simple root and the characteristic to a short one.

    source
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_weightMap_root_simpleIndex (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
    e.datumSpecialIsogeny.weightMap (((↑e).dynkinType.simplyConnectedRootDatum ⋯).root ((↑e).dynkinType.simpleIndex ⋯ (e.lengthPerm i))) = ↑(e.exponent i) • ((↑e).dynkinType.simplyConnectedRootDatum ⋯).root ((↑e).dynkinType.simpleIndex ⋯ i)

    The defining relation of the exceptional isogeny on the simple roots, in the exponent convention of the CFSG roadmap. The character map carries the simple root at the length-exchanged node to the simple root at i, rescaled by TauCeti.SuzukiReeIndex.exponent i, which is 1 at a long node and the defining characteristic at a short one.

    The character map is the pullback along the group-scheme isogeny, so this is the root-datum shadow of τ (x_{α_i}(t)) = x_{α_{σ i}}(t ^ exponent i), with the exponent indexed by i rather than by its image.

    source
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_coweightMap_coroot_simpleIndex (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
    e.datumSpecialIsogeny.coweightMap (((↑e).dynkinType.simplyConnectedRootDatum ⋯).coroot ((↑e).dynkinType.simpleIndex ⋯ i)) = ↑(e.exponent i) • ((↑e).dynkinType.simplyConnectedRootDatum ⋯).coroot ((↑e).dynkinType.simpleIndex ⋯ (e.lengthPerm i))

    The defining relation of the exceptional isogeny on the simple coroots. Dually to TauCeti.SuzukiReeIndex.datumSpecialIsogeny_weightMap_root_simpleIndex, the cocharacter map runs the other way, so it carries the simple coroot at i to the one at the length-exchanged node, rescaled by the same TauCeti.SuzukiReeIndex.exponent i.

    The square relation #

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.datumSpecialIsogeny_mul_self (e : SuzukiReeIndex) :
    e.datumSpecialIsogeny * e.datumSpecialIsogeny = RootPairingIsogeny.smulId ((↑e).dynkinType.simplyConnectedRootDatum ⋯) ⟨(↑e).characteristic, ⋯⟩

    The square of the selected isogeny is scaling by the defining characteristic. This is the root-datum form of τ ^ 2 = Frob_p, uniformly over the four half-Frobenius families; the odd powers of τ that cut out the Suzuki, Ree and Tits groups are read off it.