Finiteness of the exceptional F4 endomorphism

The represented-quotient endomorphism of the short-root carrier over 𝔽₂ is finite, has a finite scheme-theoretic kernel, and induces an involution on the prime spectrum of its coordinate ring. In particular its map on the underlying scheme points is bijective. These facts follow from the existing quadratic Frobenius-square identity; faithful flatness is a separate question.

The coordinate map and its square identity are constructed in TauCeti.Algebra.Lie.F4.ShortRoot.PrimeField.QuotientSpecialIsogeny.

theorem TauCeti.F4ShortRoot.PrimeField.finite_quotientIsogeny : (↑(CommHopfAlgCat.Hom.hom quotientIsogeny)).Finite

The exceptional F4 coordinate endomorphism is finite.

instance TauCeti.F4ShortRoot.PrimeField.moduleFinite_quotient_kernel_quotientIsogeny : Module.Finite (ZMod 2) (↑(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) (CommHopfAlgCat.commonKernelHopfIdeal generator)) ⧸ (CommHopfAlgCat.kernelHopfIdeal quotientIsogeny).toIdeal)

The scheme-theoretic kernel of the exceptional F4 endomorphism is finite over 𝔽₂.

theorem TauCeti.F4ShortRoot.PrimeField.comap_quotientIsogeny_involutive : Function.Involutive (PrimeSpectrum.comap (↑(CommHopfAlgCat.Hom.hom quotientIsogeny)).toRingHom)

The exceptional F4 endomorphism induces an involution on the underlying prime spectrum. It is therefore bijective there, even though the coordinate endomorphism need not be invertible.