Algebraic closures for finite groups of Lie type

This file attaches to every valid Lie-type index the algebraically closed field over which its ambient pinned algebraic group will be evaluated. The field is Mathlib's algebraic closure of the prime field in the characteristic recorded by the index. Consequently its field, algebraic-closure, and characteristic structures are the canonical Mathlib instances rather than parallel data.

Main definition

• TauCeti.ValidLieTypeIndex.Closure: the algebraic closure of the index's prime field.

Roadmap

This is the algebraic-closure part of item I0 in TauCetiRoadmap/CFSGStatement/README.md. Milestone L0 uses this carrier when it base-changes the pinned Chevalley--Demazure group scheme to the characteristic of a valid Lie-type index and takes its algebraic-closure-valued points.

@[reducible, inline]

abbrev TauCeti.ValidLieTypeIndex.Closure (d : ValidLieTypeIndex) : Type

The algebraic closure of the prime field in the characteristic attached to a valid Lie-type index.

Equations

• d.Closure = AlgebraicClosure (ZMod d.characteristic)

The instances used by the later ambient-group construction are inherited from Mathlib.