Connected finite diagonalizable groups and kernels

Over a field of characteristic p, a finite diagonalizable group is geometrically connected exactly when its character group is a p-group. In particular, the finite kernel of D(N) → D(M) is geometrically connected exactly when the character cokernel N / range f is a p-group. Ordinary connectedness gives the same criterion over any connected commutative base ring of prime characteristic p.

These statements detect infinitesimal finite kernels without assuming smoothness of either ambient group. They complement the prime-to-characteristic criterion for étale diagonalizable kernels.

References

• J. S. Milne, Algebraic Groups (2017), §12.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.

theorem TauCeti.DiagonalizableGroup.geometricallyConnected_of_isPGroup (k : Type u) [Field k] (p : ℕ) [ExpChar k p] {G : Type v} [CommGroup G] (hG : IsPGroup p G) : geometricallyConnectedCommHopfAlgProperty k ↧(MonoidAlgebra k G)

The diagonalizable group of an abelian p-group is geometrically connected in exponential characteristic p, even when the character group is infinite.

theorem TauCeti.DiagonalizableGroup.geometricallyConnected_iff_isPGroup (k : Type u) [Field k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (G : Type v) [CommGroup G] [Finite G] : geometricallyConnectedCommHopfAlgProperty k ↧(MonoidAlgebra k G) ↔ IsPGroup p G

A finite diagonalizable group in characteristic p is geometrically connected if and only if its character group is a p-group.

Use rw [geometricallyConnected_iff_isPGroup k p G] to supply the characteristic explicitly when rewriting a geometric connectedness goal.

theorem TauCeti.DiagonalizableGroup.connectedSpace_kernelCoordinate_iff_isPGroup {M N : Type v} [CommGroup M] [CommGroup N] (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (f : M →* N) [Finite (N ⧸ f.range)] : ConnectedSpace (PrimeSpectrum ↑(CommHopfAlgCat.quotient (↧(MonoidAlgebra R N)) (CommHopfAlgCat.kernelHopfIdeal (CommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom R f))))) ↔ IsPGroup p (N ⧸ f.range)

A finite diagonalizable-group kernel over a connected commutative ring of prime characteristic p is connected if and only if the character cokernel is a p-group.

Use rw [connectedSpace_kernelCoordinate_iff_isPGroup R p f] to supply the characteristic explicitly when rewriting a connectedness goal.

theorem TauCeti.DiagonalizableGroup.geometricallyConnected_kernelCoordinate_iff_isPGroup (k : Type u) [Field k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] {M N : Type v} [CommGroup M] [CommGroup N] (f : M →* N) [Finite (N ⧸ f.range)] : geometricallyConnectedCommHopfAlgProperty k (CommHopfAlgCat.quotient (↧(MonoidAlgebra k N)) (CommHopfAlgCat.kernelHopfIdeal (CommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom k f)))) ↔ IsPGroup p (N ⧸ f.range)

A finite diagonalizable-group kernel in characteristic p is geometrically connected if and only if the character cokernel is a p-group.

Use rw [geometricallyConnected_kernelCoordinate_iff_isPGroup k p f] to supply the characteristic explicitly when rewriting a geometric connectedness goal.