Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.TypeE7.Basic

The exceptional family E₇(q) on the minuscule carrier #

The classification list carries a single family on the E₇ diagram, the untwisted E₇(q), cut out of the index datatype by TauCeti.TypeE7LieIndex. Tau Ceti's explicit full-weight Chevalley carrier for that diagram is TauCeti.E7Minuscule.groupScheme, the Kostant toral closure of the 56-dimensional minuscule representation V(ϖ₇) inside GL₅₆ over ℤ.

This file attaches that carrier to such an index: the group of points over the algebraic closure of the index's prime field, the simple root subgroups numbered by the Bourbaki nodes of the E₇ diagram, the explicit unipotent matrix each of them is, and the pinning equation that reads their characters as the simple roots of TauCeti.DynkinType.simplyConnectedRootDatum at E₇.

The minuscule representation rather than the adjoint one is what makes the carrier's character lattice the full weight lattice of the E₇ root datum, which contains the root lattice with index two; the adjoint carrier spans the character lattice exactly in the types E₈, F₄ and G₂, where the two lattices coincide.

The Steinberg endomorphism and candidate group of E₇(q) are formed on this carrier in TauCeti/GroupTheory/SpecificGroups/CFSG/TypeE7/Frobenius.lean. The carrier is not identified with the pinned simply connected Chevalley--Demazure group scheme of type E₇: nothing below asserts that it is reductive, that its weight torus is maximal, that it is that pinned group scheme, or that any group named is finite, perfect or simple; none of those is proved of TauCeti.E7Minuscule.groupScheme here or in the files this one imports, and constructions on the carrier transfer to the pinned group only along such an identification, once one is proved. What is proved of the carrier against the E₇ diagram is the pinning equation TauCeti.TypeE7LieIndex.weightTorusPoints_conj_simpleRootSubgroup.

Main declarations #

Main results #

References #

The ambient group and its simple root subgroups #

source
@[reducible, inline]
abbrev TauCeti.TypeE7LieIndex.AmbientGroup (d : TypeE7LieIndex) :
Type

The ambient group this file attaches to a validated E₇ index: the points of the explicit full-weight type-E₇ minuscule Chevalley carrier over the algebraic closure of its prime field. No finiteness, reductivity, pinning or maximality statement is attached to it, and it is not claimed to be the points of the pinned simply connected E₇ group scheme.

Equations
Instances For
    source
    noncomputable def TauCeti.TypeE7LieIndex.simpleRootSubgroup (d : TypeE7LieIndex) (i : Fin (↑d).rank) :
    Multiplicative (↑d).Closure →* d.AmbientGroup

    The positive simple-root subgroup at the Bourbaki-numbered node i of the E₇ diagram. It is the carrier's numbered raising subgroup at the same node, the index type Fin d.1.rank being the upstream Bourbaki index type of the index's own Dynkin type.

    Equations
    Instances For
      source
      theorem TauCeti.TypeE7LieIndex.simpleRootSubgroup_def (d : TypeE7LieIndex) (i : Fin (↑d).rank) :
      d.simpleRootSubgroup i = E7Minuscule.rootSubgroupPoints (Sum.inl ((finCongr ⋯) i)) (↑d).Closure

      The simple-root subgroup is the carrier's numbered raising subgroup at the corresponding node. This is the equation through which the upstream root-subgroup API reaches simpleRootSubgroup. It is not a simp lemma: coe_simpleRootSubgroup and weightTorusPoints_conj_simpleRootSubgroup are the normal forms the equations of this file are stated against, and unfolding to TauCeti.E7Minuscule.rootSubgroupPoints would keep them from firing.

      source
      @[simp]
      theorem TauCeti.TypeE7LieIndex.coe_simpleRootSubgroup (d : TypeE7LieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) :
      ↑↑((d.simpleRootSubgroup i) u) = 1 + Multiplicative.toAdd u • (E7Minuscule.raisingMatrix ((finCongr ⋯) i)).map Int.cast

      A simple-root point is an explicit unipotent matrix. At the Bourbaki-numbered node i and parameter u it is 1 + u Eᵢ, where Eᵢ is the integral raising matrix of the minuscule basis, read in the algebraic closure. This is the sense in which the carrier of the family is explicit data rather than a group produced by an existence theorem.

      source
      theorem TauCeti.TypeE7LieIndex.weightTorusPoints_conj_simpleRootSubgroup (d : TypeE7LieIndex) (i : Fin (↑d).rank) (s : Fin 7 → (↑d).Closureˣ) (u : Multiplicative (↑d).Closure) :
      (E7Minuscule.weightTorusPoints (↑d).Closure) s * (d.simpleRootSubgroup i) u * ((E7Minuscule.weightTorusPoints (↑d).Closure) s)⁻¹ = (d.simpleRootSubgroup i) (Multiplicative.ofAdd (↑(torusCharacter s ((DynkinType.E7.simplyConnectedRootDatum DynkinType.valid_E7).root (DynkinType.E7.simpleIndex DynkinType.valid_E7 ((finCongr ⋯) i)))) * Multiplicative.toAdd u))

      The simple-root subgroups sit at the simple roots of the E₇ root datum. A point s of the carrier's rank-seven split weight torus conjugates the subgroup at node i to itself, rescaling its parameter by the value at s of the i-th simple root of TauCeti.DynkinType.simplyConnectedRootDatum at E₇, in the same Bourbaki numbering. This is the sense in which the minuscule carrier serves the diagram that the index names; it is not a claim that the carrier is the pinned group of that diagram, no pinning being constructed for it.

      The torus is indexed by the carrier's own Fin 7, which finCongr d.rank_eq_seven identifies with the index's copy Fin d.1.rank of the Bourbaki index type.