Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.GeckLattice.FixedPoints

The Frobenius-fixed points of the pinned Geck carrier are its points over the fixed subring #

TauCeti.DynkinType.geckFrobenius is the p ^ k-power Frobenius endomorphism of the points of the pinned Geck carrier over a value ring A of exponential characteristic p. Which points it fixes is settled in general: the carrier is a closed subgroup scheme of GLโ‚™ presented by a Hopf ideal, and TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsMulEquiv identifies the Frobenius-fixed matrix points of such a scheme with its points over the Frobenius-fixed subring. What is missing is that statement in the named Geck API.

This file supplies it. The isomorphism

G(๐”ฝ) โ‰ƒ* G(A)^F,        ๐”ฝ = frobeniusFixedSubring A p k,

is the general one transported by TauCeti.GeneralLinear.frobeniusFixedMulEquivOfCoeEq, which is fed TauCeti.DynkinType.geckPoints_def and TauCeti.DynkinType.coe_geckFrobenius, exactly as TauCeti.DynkinType.geckPointsMap consumes TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup and TauCeti.DynkinType.map_subtype_fixedSubgroup_geckFrobenius_eq consumes TauCeti.GeneralLinear.map_hopfIdealPointsSubgroup_frobeniusFixedSubring. Nothing is reproved: the transport changes no matrix, and the one thing it has to check is that the two Frobenius endomorphisms correspond under it, which they do because both act entrywise.

What the isomorphism adds over TauCeti.DynkinType.map_subtype_fixedSubgroup_geckFrobenius_eq, which is already available, is a map. That lemma equates two subgroups of the ambient GLโ‚™(A): the image of the fixed subgroup and the image of the points over ๐”ฝ. It names no map between G(๐”ฝ) and G(A)^F themselves, and a consumer that wants to read a property of G(A)^F off the same property of G(๐”ฝ) needs one. The isomorphism below packages that equality of embedded subgroups as an explicit MulEquiv between the two element types.

Naturality on the pinned generating families is not restated: the isomorphism is the entrywise inclusion, by TauCeti.DynkinType.coe_geckPointsMulEquivFixedSubgroupGeckFrobenius, so TauCeti.DynkinType.geckPointsMap_geckRootSubgroupPoints and TauCeti.DynkinType.geckPointsMap_geckWeightTorusPoints at the inclusion of ๐”ฝ already describe its action on the numbered root subgroups and on the weight torus.

Two limitations carry over from the file this one builds on. The Geck carrier is built from the adjoint module, so outside the types Eโ‚ˆ, Fโ‚„ and Gโ‚‚ its weights span the root lattice rather than the whole character lattice and it is not the simply connected form; and no statement here restricts to the elementary subgroup generated by the root subgroups, since the generation theorem that would identify the two is not available. Nothing below asserts that a group in sight is finite, perfect, simple, or a named finite group of Lie type.

Main definitions #

Main results #

References #

The type-A counterpart is TauCeti/Algebra/Lie/SpecialLinear/StandardCarrier/FixedPoints.lean, which identifies the Frobenius-fixed points of TauCeti.SlStd with SL_{r+1} over the fixed subfield; no such identification with a classical matrix group is available here, so the fixed group is described as the carrier's points over the fixed subring instead. The coordinate-free form of the isomorphism, for the points of a Hopf algebra rather than for matrix points, is TauCeti.Bialgebra.frobeniusFixedPointsMulEquiv.

Roadmap #

This advances the target "points over an algebraically closed field as a group, functorially in the field, so that a field endomorphism induces a group endomorphism of the points. The q-power Frobenius is the case a consumer asks for first" in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, by naming an isomorphism onto the group that endomorphism fixes, from the points over the fixed subring.

The fixed points as points over the fixed subring #

source
noncomputable def TauCeti.DynkinType.geckPointsMulEquivFixedSubgroupGeckFrobenius (t : DynkinType) (ht : t.Valid) (p k : โ„•) (A : Type v) [CommRing A] [ExpChar A p] :
โ†ฅ(t.geckPoints ht โ†ฅ(frobeniusFixedSubring A p k)) โ‰ƒ* โ†ฅ(fixedSubgroup (t.geckFrobenius ht p k A))

The Frobenius-fixed points of the pinned Geck carrier are its points over the Frobenius-fixed subring, as an isomorphism between the two element types rather than as the equality of their images in GLโ‚™(A) recorded by TauCeti.DynkinType.map_subtype_fixedSubgroup_geckFrobenius_eq. For p prime, 0 < k and A an algebraic closure of ZMod p this reads G(๐”ฝ_q) โ‰ƒ* G(A)^F with q = p ^ k.

It is TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsMulEquiv, the same isomorphism for the matrix points cut out by a Hopf ideal, transported into the named Geck API by TauCeti.GeneralLinear.frobeniusFixedMulEquivOfCoeEq, which consumes only the presentation TauCeti.DynkinType.geckPoints_def of the point group and the entrywise description TauCeti.DynkinType.coe_geckFrobenius of the carrier Frobenius; nothing is reproved. TauCeti.DynkinType.coe_geckPointsMulEquivFixedSubgroupGeckFrobenius says that the transport leaves the matrices alone, so the isomorphism is the entrywise inclusion.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.DynkinType.coe_geckPointsMulEquivFixedSubgroupGeckFrobenius (t : DynkinType) (ht : t.Valid) (p k : โ„•) (A : Type v) [CommRing A] [ExpChar A p] (g : โ†ฅ(t.geckPoints ht โ†ฅ(frobeniusFixedSubring A p k))) :
    โ†‘โ†‘((t.geckPointsMulEquivFixedSubgroupGeckFrobenius ht p k A) g) = (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) โ†‘g

    The isomorphism onto the Frobenius-fixed points includes the matrix entries of a point over the Frobenius-fixed subring into the value ring, and does nothing else.

    source
    theorem TauCeti.DynkinType.coe_geckPointsMulEquivFixedSubgroupGeckFrobenius_apply (t : DynkinType) (ht : t.Valid) (p k : โ„•) (A : Type v) [CommRing A] [ExpChar A p] (g : โ†ฅ(t.geckPoints ht โ†ฅ(frobeniusFixedSubring A p k))) (r c : Fin (t.geckDim ht)) :
    โ†‘โ†‘โ†‘((t.geckPointsMulEquivFixedSubgroupGeckFrobenius ht p k A) g) r c = โ†‘(โ†‘โ†‘g r c)

    Entrywise, the isomorphism includes each matrix entry of a point over the Frobenius-fixed subring into the value ring.

    source
    @[simp]
    theorem TauCeti.DynkinType.coe_geckPointsMulEquivFixedSubgroupGeckFrobenius_symm_apply (t : DynkinType) (ht : t.Valid) (p k : โ„•) (A : Type v) [CommRing A] [ExpChar A p] (x : โ†ฅ(fixedSubgroup (t.geckFrobenius ht p k A))) :
    (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) โ†‘((t.geckPointsMulEquivFixedSubgroupGeckFrobenius ht p k A).symm x) = โ†‘โ†‘x

    The inverse of the isomorphism reads a Frobenius-fixed point as a point over the Frobenius-fixed subring: including its matrix back into the A-valued points returns the point one started from.

    source
    @[simp]
    theorem TauCeti.DynkinType.coe_geckPointsMulEquivFixedSubgroupGeckFrobenius_symm_apply_apply (t : DynkinType) (ht : t.Valid) (p k : โ„•) (A : Type v) [CommRing A] [ExpChar A p] (x : โ†ฅ(fixedSubgroup (t.geckFrobenius ht p k A))) (r c : Fin (t.geckDim ht)) :
    โ†‘(โ†‘โ†‘((t.geckPointsMulEquivFixedSubgroupGeckFrobenius ht p k A).symm x) r c) = โ†‘โ†‘โ†‘x r c

    Entrywise, the point over the Frobenius-fixed subring produced by the inverse of the isomorphism has the entries of the Frobenius-fixed point it came from.