Coordinate criterion for central kernels

A morphism f : H ⟶ K of commutative Hopf algebras induces contravariantly a morphism Spec K ⟶ Spec H of affine group schemes. This file identifies the two existing notions of a central kernel for that morphism:

• GroupScheme.HasCentralKernel tests the kernel on points valued in every scheme over the base;
• HopfIdeal.IsCentral says that the represented kernel Hopf ideal is central.

The bridge must account for nonaffine test schemes in HasCentralKernel. It uses the relative Γ-Spec multiplicative equivalence from CommHopfAlgCat.SchemePoints, so the group law on all scheme-valued points is convolution on global sections. Naturality in H then identifies the kernel of the scheme-valued point map with the points cut out by kernelHopfIdeal f.

Main declarations

• TauCeti.GroupScheme.hasCentralKernel_hopfSpec_map_iff: the induced affine group-scheme morphism has central kernel exactly when its kernel Hopf ideal is central.
• TauCeti.GroupScheme.isCentralIsogeny_hopfSpec_map_iff: the resulting coordinate criterion for a central isogeny.

References

• J. S. Milne, Algebraic Groups (2017), §§1.k, 2, and 18.a.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapters 2 and 10.

The relative global-sections comparison uses Mathlib's algΓAlgSpecAdjunction and AlgebraicGeometry.Spec.mapMulEquiv. This synchronizes the Hopf-algebra and group-scheme formulations of central isogenies required in Layer 6 of the ReductiveGroups roadmap.

theorem TauCeti.GroupScheme.hasCentralKernel_hopfSpec_map_of_isCentral_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : (CommHopfAlgCat.kernelHopfIdeal f).IsCentral) : HasCentralKernel ((AlgebraicGeometry.hopfSpec ↧R).map f.op)

If the represented kernel Hopf ideal is central, then the induced affine group-scheme morphism has central kernel on points valued in every scheme over the base.

theorem TauCeti.GroupScheme.isCentral_kernelHopfIdeal_of_hasCentralKernel_hopfSpec_map {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : HasCentralKernel ((AlgebraicGeometry.hopfSpec ↧R).map f.op)) : (CommHopfAlgCat.kernelHopfIdeal f).IsCentral

If the induced affine group-scheme morphism has central kernel on all scheme-valued points, then its represented kernel Hopf ideal is central.

theorem TauCeti.GroupScheme.hasCentralKernel_hopfSpec_map_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) : HasCentralKernel ((AlgebraicGeometry.hopfSpec ↧R).map f.op) ↔ (CommHopfAlgCat.kernelHopfIdeal f).IsCentral

Coordinate criterion for a central kernel. The affine group-scheme morphism induced by f : H ⟶ K has central kernel exactly when its represented kernel Hopf ideal is central.

theorem TauCeti.GroupScheme.isCentralIsogeny_hopfSpec_map_iff {k : Type u} [CommRing k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : IsCentralIsogeny ((AlgebraicGeometry.hopfSpec ↧k).map f.op) ↔ IsIsogeny ((AlgebraicGeometry.hopfSpec ↧k).map f.op) ∧ (CommHopfAlgCat.kernelHopfIdeal f).IsCentral

Coordinate criterion for a central isogeny. A Hopf-spectrum morphism is a central isogeny exactly when it is an isogeny and its represented kernel Hopf ideal is central.