Documentation

TauCeti.Algebra.AlgebraicGroup.HopfIdeal.CommonKernel.Flat

Flatness of subgroups generated by flat affine group schemes #

Over a Dedekind domain the common-kernel quotient of scalar-torsion-free coordinate algebras is scalar-torsion-free, hence flat. Its scalar-torsion Hopf ideal is killed by every lifted generator map and therefore lies in their common kernel, which is zero.

In particular an integral carrier generated by additive root subgroups and a split torus is flat over ℤ. No reducedness or smoothness of its special fibers follows from this alone.

References #

The maximality argument parallels TauCeti.CommHopfAlgCat.isReduced_quotient_commonKernelHopfIdeal; the Hopf ideal used here is TauCeti.HopfIdeal.scalarTorsion.

instance TauCeti.CommHopfAlgCat.isTorsionFree_quotient_commonKernelHopfIdeal {R : Type u} [CommRing R] [IsDedekindDomain R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) [∀ (i : ι), Module.IsTorsionFree R ↑(K i)] :

A subgroup scheme generated by scalar-torsion-free affine group schemes over a Dedekind domain has scalar-torsion-free coordinate algebra. Consequently it is flat over the base.