Rank of finite flat affine group schemes

The rank of the structural morphism of a finite flat affine group scheme equals the local rank of its coordinate Hopf algebra. Neither commutativity of the group nor local finite presentation is needed. The comparison uses the Hopf-spectrum anti-equivalence and TauCeti.finrank_hopfSpec.

@[simp]

theorem TauCeti.AffineGroupSchemeCat.finrank_eq_rankAtStalk_coordinateHopfAlgebra (R : Type u) [CommRing R] (G : AffineGroupSchemeCat ↧R) [AlgebraicGeometry.IsFinite G.obj.X.hom] [AlgebraicGeometry.Flat G.obj.X.hom] (x : PrimeSpectrum R) : AlgebraicGeometry.Scheme.Hom.finrank G.obj.X.hom x = Module.rankAtStalk (↑(Opposite.unop ((commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).inverse.obj G))) x

The scheme-theoretic rank of a finite flat affine group scheme is the local rank of its coordinate Hopf algebra.