Powers of an isogeny of a root pairing with itself #
An isogeny of a root pairing with itself can be composed with itself, and the Suzuki and Ree
groups are cut out by the odd powers of a special isogeny rather than by the isogeny itself.
This file gives the isogenies of a fixed root pairing with itself their monoid structure under
composition, so that f ^ n is available with the whole Monoid API, and computes the square of
a power of a special isogeny.
The monoid is the one composition already determines: TauCeti.RootPairingIsogeny.comp is
associative with TauCeti.RootPairingIsogeny.id as a two-sided unit, and nothing new is proved to
put it together. What the monoid buys is the identity
f ^ n * f ^ n = smulId P (c ^ n) whenever f * f = smulId P c,
TauCeti.RootPairingIsogeny.pow_mul_self_eq_smulId, which is pure monoid algebra: f ^ n * f ^ n
is (f * f) ^ n. Read at c the defining characteristic and n odd, this is the root-datum form
of steinberg (m) ^ 2 = Frob_(p ^ (2 * m + 1)) for steinberg (m) = τ ^ (2 * m + 1). It is stated
for every n, since the restriction to odd exponents belongs to the finite-group construction and
not to this identity.
All three of the weight map, the coweight map and the index bijection are monoid homomorphisms out
of this monoid, the coweight map into the opposite endomorphism monoid because comp reverses on
that component. These declarations adapt the Mathlib API RootPairing.Hom.weightHom,
RootPairing.Hom.coweightHom and RootPairing.Hom.indexHom for the endomorphism monoid of a root
pairing, and the powers of all three components are map_pow.
Two further maps into the monoid are recorded because the Steinberg endomorphisms of the twisted
families are built from them: the automorphisms of the root pairing land in it multiplicatively,
TauCeti.RootPairingIsogeny.ofEquivHom, and the scalings are central in it,
TauCeti.RootPairingIsogeny.commute_smulId. Together they let a power of an automorphism times a
scaling be separated into a power of each.
The same hypothesis also splits the powers themselves: an even power is a scaling, and an odd power
is a scaling times f, so an odd power permutes the roots exactly as f does while multiplying
its exponents and its weight and coweight maps by c ^ m. The three special isogenies of B₂,
G₂ and F₄ are the instance this exists for; their power relations are in
TauCeti/LinearAlgebra/RootSystem/Isogeny/Special.lean, where they join the square relations they
come from.
Main definitions #
TauCeti.RootPairingIsogeny.instMonoid: the composition monoid of isogenies of a root pairing with itself.TauCeti.RootPairingIsogeny.weightHom,TauCeti.RootPairingIsogeny.coweightHomandTauCeti.RootPairingIsogeny.indexHom: the weight map, the coweight map and the index bijection as monoid homomorphisms, the coweight map into the opposite endomorphism monoid.TauCeti.RootPairingIsogeny.smulIdHom: the scalings, as a monoid homomorphism out ofℕ+.TauCeti.RootPairingIsogeny.ofEquivHom: the automorphisms of the root pairing, as a monoid homomorphism into the isogeny monoid.
Main results #
TauCeti.RootPairingIsogeny.ofEquiv_pow: an automorphism and the isogeny it becomes have the same powers.TauCeti.RootPairingIsogeny.commute_smulId: a scaling commutes with every endo-isogeny.TauCeti.RootPairingIsogeny.pow_mul_self_eq_smulId: a power of an isogeny whose square is a scaling squares to the corresponding power of that scaling.TauCeti.RootPairingIsogeny.pow_two_mul_eq_smulIdandTauCeti.RootPairingIsogeny.pow_two_mul_add_one_eq_smulId_mul: such an isogeny has scalings for its even powers, and a scaling times itself for its odd ones.TauCeti.RootPairingIsogeny.exponent_pow: the exponent of an iterate is the product along the corresponding orbit of indices.TauCeti.RootPairingIsogeny.indexEquiv_pow_two_mul_add_one,TauCeti.RootPairingIsogeny.exponent_pow_two_mul_add_one,TauCeti.RootPairingIsogeny.weightMap_pow_two_mul_add_oneandTauCeti.RootPairingIsogeny.coweightMap_pow_two_mul_add_one: an odd power permutes the roots as the isogeny does and multiplies its exponents and its two lattice maps byc ^ m.
References #
- Scott Carnahan,
Mathlib/LinearAlgebra/RootSystem/Hom.lean, for theRootPairing.Homendomorphism monoid API adapted here. - Schémas en groupes (SGA 3), Exposé XXI, 6.8.
- R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
The odd powers of the special isogeny are what milestone L2 of
TauCetiRoadmap/CFSGStatement/README.md asks for, "steinberg(m) = τ_X ^ (2m + 1),
steinberg(m) ^ 2 = Frob_(p ^ (2m + 1))", once the special isogeny itself has been lifted from
root data to the pinned group schemes of Layer 9 of
TauCetiRoadmap/ReductiveGroups/README.md.
The composition monoid #
The isogenies of a root pairing with itself form a monoid under composition, with the
identity isogeny as unit. Multiplication is composition in the same order as
TauCeti.RootPairingIsogeny.comp, so f * g applies g first.
Equations
- One or more equations did not get rendered due to their size.
The automorphisms of a root pairing sit inside its monoid of endo-isogenies, as a monoid
homomorphism: an automorphism is an isogeny with every exponent 1, and composition agrees on the
two sides.
Equations
- TauCeti.RootPairingIsogeny.ofEquivHom P = { toFun := TauCeti.RootPairingIsogeny.ofEquiv, map_one' := ⋯, map_mul' := ⋯ }
Instances For
An automorphism and the isogeny it becomes have the same powers, since
TauCeti.RootPairingIsogeny.ofEquiv is multiplicative.
The multiplicative components #
The weight map of an isogeny, as a monoid homomorphism into the endomorphism monoid of the weight space.
Equations
- TauCeti.RootPairingIsogeny.weightHom P = { toFun := fun (f : TauCeti.RootPairingIsogeny P P) => f.weightMap, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The weight map of a power of an isogeny is the corresponding power of its weight map.
The coweight map of an isogeny, as a monoid homomorphism into the opposite of the
endomorphism monoid of the coweight space. Composition reverses on this component, exactly as for
RootPairing.Hom.coweightHom.
Equations
- TauCeti.RootPairingIsogeny.coweightHom P = { toFun := fun (f : TauCeti.RootPairingIsogeny P P) => MulOpposite.op f.coweightMap, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The coweight map of a power of an isogeny is the corresponding power of its coweight map. The
reversal in TauCeti.RootPairingIsogeny.coweightHom is immaterial here, since the two factors of
f ^ (n + 1) are the same map.
The index bijection of an isogeny, as a monoid homomorphism into the permutation group of the index set.
Equations
- TauCeti.RootPairingIsogeny.indexHom P = { toFun := fun (f : TauCeti.RootPairingIsogeny P P) => f.indexEquiv, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The index bijection of a power of an isogeny is the corresponding power of its index bijection.
The exponent of a power of an isogeny, in terms of the exponents of the lower power.
The exponent of an iterate accumulates along the forward orbit of the index bijection. Unlike the other three fields the exponent is not multiplicative: the exponent of a composite at an index is the product of the exponents met at the successive images of that index.
The scalings #
The scalings of a root pairing, as a monoid homomorphism out of the positive integers. At a prime this picks out the root-datum shadow of the Frobenius isogeny.
Equations
- TauCeti.RootPairingIsogeny.smulIdHom P = { toFun := fun (c : ℕ+) => TauCeti.RootPairingIsogeny.smulId P c, map_one' := ⋯, map_mul' := ⋯ }
Instances For
A power of a scaling is the scaling by the corresponding power.
A scaling is central in the monoid of endo-isogenies, the monoid form of
TauCeti.RootPairingIsogeny.comp_smulId. Since a scaling at a prime power q is the root-datum
shadow of the q-power Frobenius, this is the root-datum form of the fact that a Frobenius
commutes with every endomorphism of the datum.
An even power of an isogeny whose square is a scaling is itself a scaling.
A power of an isogeny whose square is a scaling squares to the corresponding power of that
scaling. For c the defining characteristic and n = 2 * m + 1, this is the root-datum form of
the relation steinberg (m) ^ 2 = Frob_(p ^ (2 * m + 1)) satisfied by the odd powers of a special
isogeny; the identity itself holds at every exponent.
An odd power of an isogeny whose square is a scaling is a scaling times the isogeny. This
is what makes the odd powers genuinely new maps rather than scalings: the factor f survives.
An odd power of an isogeny whose square is a scaling permutes the roots exactly as the isogeny does, since a scaling fixes every index.
The rescaling exponents of an odd power are those of the isogeny times c ^ m.
Read at a special isogeny in characteristic p, so at c = p: the exponent field is indexed by
the source of the character map, and is 1 at a short simple root and p at a long one
(TauCeti.DynkinType.b2SpecialIsogeny_exponent_typeBSimpleIndex_eq_one_iff), so the odd power has
exponent p ^ m at a short simple root and p ^ (m + 1) at a long one.
The weight map of an odd power is c ^ m times that of the isogeny.
The coweight map of an odd power is c ^ m times that of the isogeny. Composition reverses
on this component, but a scaling is central, so the formula is the same as for the weight map.