The algebraic closure for the Ree family of type F₄

This file records that the algebraic closure attached to a validated Ree index of type F₄ has characteristic two, and equips it with the resulting structure of an algebra over the field of two elements. That is the form in which the characteristic reaches a construction on the family's carrier, whose defining equations live in characteristic two and whose base ring is ZMod 2 itself.

Main results

• TauCeti.ReeF4LieIndex.charP_closure_two: the algebraic closure attached to a Ree index of type F₄ has characteristic two.
• TauCeti.ReeF4LieIndex.algebraZModTwo: the resulting ZMod 2-algebra structure on it.

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

The algebraic closure attached to a Ree index of type F₄ has characteristic two.

@[instance_reducible]

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

The algebraic closure attached to a Ree index of type F₄ is an algebra over the field of two elements, this being the base ring over which its carrier is defined. Characteristic two forces the structure: any two ZMod 2-algebra structures on a ring agree.

Equations

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