The algebraic closure for the Tits construction

This file records that the algebraic closure attached to the validated Tits index has characteristic two, and equips it with the resulting structure of an algebra over the field of two elements. These are the structures through which the index reaches the explicit type-F₄ carrier and its exceptional isogeny.

Main results

• TauCeti.TitsLieIndex.charP_closure_two: the algebraic closure attached to the Tits index has characteristic two.
• TauCeti.TitsLieIndex.algebraZModTwo: the resulting ZMod 2-algebra structure.

instance TauCeti.TitsLieIndex.charP_closure_two (d : TitsLieIndex) : CharP (↑d).Closure 2

The algebraic closure attached to the Tits index has characteristic two.

@[instance_reducible]

noncomputable instance TauCeti.TitsLieIndex.algebraZModTwo (d : TitsLieIndex) : Algebra (ZMod 2) (↑d).Closure

The algebraic closure attached to the Tits index is an algebra over the field of two elements, the base ring over which its short-root carrier is defined.

Equations

• d.algebraZModTwo = ZMod.algebra (↑d).Closure 2