Flatness of the integral type-E6 minuscule carrier

The full-weight type-E₆ minuscule carrier has scalar-torsion-free coordinate algebra and is consequently flat over ℤ. This is a property of the integral carrier itself, before specializing to any field. It does not assert smoothness of its fibers or identify it with the pinned simply connected group scheme of type E₆.

The result applies the flatness criterion for integral Kostant toral closures to TauCeti.E6Minuscule.definingIdeal.

References

• J. E. Humphreys, Linear Algebraic Groups, §26.
• The Stacks Project, Tag 0AUW, for flatness of torsion-free modules over Dedekind domains.

instance TauCeti.E6Minuscule.isTorsionFree_integralCoordinateHopfAlgebra : Module.IsTorsionFree ℤ ↑(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 27) definingIdeal)

The integral full-weight type-E₆ minuscule carrier has no scalar torsion in its coordinate algebra. In particular its coordinate algebra is flat over ℤ.