Documentation

TauCeti.Algebra.Lie.E6.DoubledMinuscule.Frobenius

The Frobenius of the doubled type-E6 minuscule carrier #

TauCeti.E6DoubledMinuscule.groupScheme is the explicit full-weight type-E₆ carrier over ℤ built from V(ϖ₁) ⊕ V(ϖ₆), and TauCeti.E6DoubledMinuscule.points A realizes its A-valued points as a subgroup of GL₅₄(A). Over a commutative ring A of exponential characteristic p, entrywise p ^ k-th powers are a homomorphism of value rings, so the carrier's functoriality turns them into a group endomorphism of its points.

This file names that endomorphism TauCeti.E6DoubledMinuscule.frobenius and records its characteristic equations:

F (g)ᵢⱼ = gᵢⱼ ^ (p ^ k),
F (xᵢ(u)) = xᵢ(u ^ (p ^ k)),
F (t(s)) = t(s ^ (p ^ k)).

The zeroth iterate is the identity, exponents add under composition and multiply under taking powers in the endomorphism monoid, and the fixed points are the points of the same carrier over the Frobenius-fixed subring.

The 27-dimensional carrier already carries a Frobenius, TauCeti.E6Minuscule.frobenius, and it is the one the untwisted family E₆(q) is built from. What the doubled carrier adds is the index set on which the E₆ diagram symmetry acts, by TauCeti.DynkinType.e6DoubledMinusculeWeight_e6DoubledMinusculeGraphPerm, whereas that symmetry moves every minuscule weight off the twenty-seven-element table by TauCeti.DynkinType.e6MinusculeWeight_comp_graphPermE6_notMem_range. A Steinberg map composing a graph automorphism with a field Frobenius therefore needs the Frobenius of this carrier, which is what is built here. The graph automorphism is built in a separate module, and no declaration below mentions the diagram symmetry.

Nothing here asserts reductivity, maximality of the weight torus, an identification of the carrier's root datum, or any finiteness or simplicity statement.

Main declarations #

References #

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", whose "the q-power Frobenius is the case a consumer asks for first", in Layer 9, "pinned Chevalley--Demazure group schemes over ℤ", of TauCetiRoadmap/ReductiveGroups/README.md. Its consumer is milestone L1, "ordinary and graph Steinberg maps", of TauCetiRoadmap/CFSGStatement/README.md, whose Steinberg map for the twisted family ²E₆(q) is γ₂ ∘ Frob_q on the points of a carrier for the E₆ diagram over an algebraic closure of ZMod p; the identification of this carrier with the pinned simply connected Chevalley--Demazure group that milestone requires remains pending.

source
noncomputable def TauCeti.E6DoubledMinuscule.frobenius (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] :
↥(points A) →* ↥(points A)

The p ^ k-power Frobenius endomorphism of the full-weight doubled type-E₆ minuscule carrier, the functorial map on points induced by the iterated Frobenius endomorphism of the value ring.

For p prime, 0 < k, and A an algebraic closure of ZMod p, this is the Frobenius factor of the Steinberg map that a future construction of the twisted family ²E₆(p ^ k) composes with the E₆ graph automorphism.

Equations
Instances For
    source
    theorem TauCeti.E6DoubledMinuscule.coe_frobenius (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points A)) :
    ↑((frobenius p k A) g) = (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) ↑g

    The Frobenius endomorphism of the doubled minuscule carrier acts by entrywise Frobenius.

    This is not a simp lemma because coe_frobenius_apply is the canonical coefficient-level normal form.

    source
    theorem TauCeti.E6DoubledMinuscule.frobenius_eq_map (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] :
    frobenius p k A = (pointsPresentation A).map (pointsPresentation A) (iterateFrobenius A p k)

    The carrier Frobenius is the functorial map on points induced by the iterated Frobenius endomorphism of the value ring.

    source
    @[simp]
    theorem TauCeti.E6DoubledMinuscule.coe_frobenius_apply (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points A)) (i j : Fin 54) :
    ↑↑((frobenius p k A) g) i j = ↑↑g i j ^ p ^ k

    Entrywise, the Frobenius endomorphism raises each matrix coefficient to its p ^ k-th power.

    source
    @[simp]
    theorem TauCeti.E6DoubledMinuscule.frobenius_rootSubgroupPoints (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (i : Fin 6 ⊕ Fin 6) (u : Multiplicative A) :
    (frobenius p k A) ((rootSubgroupPoints i A) u) = (rootSubgroupPoints i A) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ p ^ k))

    Frobenius raises the parameter of every numbered doubled type-E₆ simple-root subgroup to its p ^ k-th power.

    source
    @[simp]
    theorem TauCeti.E6DoubledMinuscule.frobenius_weightTorusPoints (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (s : Fin 6 → Aˣ) :
    (frobenius p k A) ((weightTorusPoints A) s) = (weightTorusPoints A) (s ^ p ^ k)

    Frobenius raises every coordinate of the pinned split weight torus to its p ^ k-th power.

    source
    @[simp]
    theorem TauCeti.E6DoubledMinuscule.frobenius_zero (p : ℕ) (A : Type v) [CommRing A] [ExpChar A p] :
    frobenius p 0 A = MonoidHom.id ↥(points A)

    The zeroth Frobenius iterate is the identity on the doubled minuscule carrier's point group.

    source
    theorem TauCeti.E6DoubledMinuscule.frobenius_add (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (m : ℕ) :
    frobenius p (k + m) A = (frobenius p k A).comp (frobenius p m A)

    Frobenius iterates add under composition on the doubled minuscule carrier's point group.

    source
    theorem TauCeti.E6DoubledMinuscule.frobenius_pow (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (m : ℕ) :
    (have this := frobenius p k A; this) ^ m = frobenius p (k * m) A

    Frobenius exponents multiply under taking powers: the m-th power of the p ^ k-power Frobenius of the doubled minuscule carrier, in the endomorphism monoid of its points, is its p ^ (k * m)-power Frobenius.

    source
    @[simp]
    theorem TauCeti.E6DoubledMinuscule.frobenius_eq_self_iff (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points A)) :
    (frobenius p k A) g = g ↔ ∀ (i j : Fin 54), ↑↑g i j ∈ frobeniusFixedSubring A p k

    A doubled minuscule carrier point is fixed by Frobenius exactly when all of its matrix entries lie in the Frobenius-fixed subring.

    source
    theorem TauCeti.E6DoubledMinuscule.map_subtype_fixedSubgroup_frobenius_eq (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] :
    Subgroup.map (points A).subtype (fixedSubgroup (frobenius p k A)) = Subgroup.map (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) (points ↥(frobeniusFixedSubring A p k))

    The Frobenius-fixed points of the full-weight doubled minuscule carrier are its points over the Frobenius-fixed subring.