Finiteness of the exceptional G2 endomorphism

The exceptional 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 cubic Frobenius-square identity and do not assert faithful flatness.

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

theorem TauCeti.G2ShortRoot.PrimeField.finite_specialIsogenyCoordinateMap : (↑(CommHopfAlgCat.Hom.hom specialIsogenyCoordinateMap)).Finite

The exceptional G2 coordinate endomorphism is finite.

instance TauCeti.G2ShortRoot.PrimeField.moduleFinite_quotient_kernel_specialIsogenyCoordinateMap : Module.Finite (ZMod 3) (↑carrierAlgebra ⧸ (CommHopfAlgCat.kernelHopfIdeal specialIsogenyCoordinateMap).toIdeal)

The scheme-theoretic kernel of the exceptional G2 endomorphism is finite over 𝔽₃.

theorem TauCeti.G2ShortRoot.PrimeField.comap_specialIsogenyCoordinateMap_involutive : Function.Involutive (PrimeSpectrum.comap (↑(CommHopfAlgCat.Hom.hom specialIsogenyCoordinateMap)).toRingHom)

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