Base change of group-scheme isogenies

This file proves that central kernels of group-scheme morphisms remain central after arbitrary base change, by identifying the point groups before and after base change through the pullback adjunction. Consequently, isogenies over a commutative ring remain so after base change along a morphism between affine bases, and central isogenies remain so after such a base change. For a commutative source, the base-changed isogeny is central without any centrality hypothesis. The group-scheme base change is the pullback functor on the over category, lifted to group objects.

Main declarations

• TauCeti.GroupScheme.baseChangePointMulEquiv: the multiplicative point-group identification furnished by the pullback adjunction.
• TauCeti.GroupScheme.HasCentralKernel.baseChange: central kernels remain central after arbitrary base change.
• TauCeti.GroupScheme.IsIsogeny.baseChange: isogenies remain isogenies after base change.
• TauCeti.GroupScheme.IsCentralIsogeny.baseChange: central isogenies remain central after base change.
• TauCeti.GroupScheme.IsIsogeny.baseChange_isCentral_of_isCommMonObj: the base change of an isogeny from a commutative source is a central isogeny.

References

• J. S. Milne, Algebraic Groups (2017), §18.a.
• Mathlib's Over.mapPullbackAdj and the cartesian-monoidal structure on Over.pullback provide the point identification and its compatibility with multiplication.

The base-change argument follows TauCeti.AlgebraicGeometry.AbelianVariety.IsIsogeny.baseChange.

This is the base-change stability needed for the central-isogeny interface in Layer 6 of the ReductiveGroups roadmap.

theorem TauCeti.GroupScheme.IsIsogeny.baseChange {R S : Type u} [CommRing R] [CommRing S] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (s : AlgebraicGeometry.Spec ↧S ⟶ AlgebraicGeometry.Spec ↧R) {f : G ⟶ H} (hf : IsIsogeny f) : IsIsogeny ((CategoryTheory.Over.pullback s).mapGrp.map f)

Base change along a morphism between spectra of commutative rings preserves group-scheme isogenies.

noncomputable def TauCeti.GroupScheme.baseChangePointMulEquiv {X Y : AlgebraicGeometry.Scheme} (s : Y ⟶ X) (G : CategoryTheory.Grp (CategoryTheory.Over X)) (T : CategoryTheory.Over Y) : (T ⟶ ((CategoryTheory.Over.pullback s).mapGrp.obj G).X) ≃* ((CategoryTheory.Over.map s).obj T ⟶ G.X)

The adjunction between postcomposition and pullback identifies points of a base-changed group scheme with points of the original group scheme over the same test scheme viewed over the old base. This identification is multiplicative.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GroupScheme.baseChangePointMulEquiv_apply {X Y : AlgebraicGeometry.Scheme} (s : Y ⟶ X) (G : CategoryTheory.Grp (CategoryTheory.Over X)) (T : CategoryTheory.Over Y) (p : T ⟶ ((CategoryTheory.Over.pullback s).mapGrp.obj G).X) : (baseChangePointMulEquiv s G T) p = ((CategoryTheory.Over.mapPullbackAdj s).homEquiv T G.X).symm p

The point-group equivalence is the underlying pullback-adjunction equivalence.

@[simp]

theorem TauCeti.GroupScheme.baseChangePointMulEquiv_symm_apply {X Y : AlgebraicGeometry.Scheme} (s : Y ⟶ X) (G : CategoryTheory.Grp (CategoryTheory.Over X)) (T : CategoryTheory.Over Y) (p : (CategoryTheory.Over.map s).obj T ⟶ G.X) : (baseChangePointMulEquiv s G T).symm p = ((CategoryTheory.Over.mapPullbackAdj s).homEquiv T G.X) p

The inverse point-group equivalence is the forward pullback-adjunction equivalence.

theorem TauCeti.GroupScheme.baseChangePointMulEquiv_pointMap {X Y : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (s : Y ⟶ X) (f : G ⟶ H) (T : CategoryTheory.Over Y) (p : T ⟶ ((CategoryTheory.Over.pullback s).mapGrp.obj G).X) : (baseChangePointMulEquiv s H T) ((pointMap ((CategoryTheory.Over.pullback s).mapGrp.map f) T) p) = (pointMap f ((CategoryTheory.Over.map s).obj T)) ((baseChangePointMulEquiv s G T) p)

The point-group identification intertwines a base-changed morphism with the original morphism.

theorem TauCeti.GroupScheme.HasCentralKernel.baseChange {X Y : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (s : Y ⟶ X) {f : G ⟶ H} (hf : HasCentralKernel f) : HasCentralKernel ((CategoryTheory.Over.pullback s).mapGrp.map f)

Arbitrary base change preserves central kernels of group-scheme morphisms.

theorem TauCeti.GroupScheme.IsCentralIsogeny.baseChange {k L : Type u} [CommRing k] [CommRing L] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} (s : AlgebraicGeometry.Spec ↧L ⟶ AlgebraicGeometry.Spec ↧k) {f : G ⟶ H} (hf : IsCentralIsogeny f) : IsCentralIsogeny ((CategoryTheory.Over.pullback s).mapGrp.map f)

Base change along a morphism between spectra of commutative rings preserves central isogenies.

theorem TauCeti.GroupScheme.IsIsogeny.baseChange_isCentral_of_isCommMonObj {k L : Type u} [CommRing k] [CommRing L] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} (s : AlgebraicGeometry.Spec ↧L ⟶ AlgebraicGeometry.Spec ↧k) {f : G ⟶ H} (hf : IsIsogeny f) [CategoryTheory.IsCommMonObj G.X] : IsCentralIsogeny ((CategoryTheory.Over.pullback s).mapGrp.map f)

The base change of an isogeny from a commutative group scheme is a central isogeny.