Central isogenies of group schemes

For group schemes over the spectrum of a commutative ring, an isogeny is a homomorphism whose underlying scheme morphism is finite, flat, and surjective. It is central when its scheme-theoretic kernel is central. We express the latter condition intrinsically through the functor of points: for every test scheme over the base, every point killed by the homomorphism commutes with every other point of the source.

Quantifying over all test schemes is essential. Centrality only on base-ring-valued points would miss infinitesimal points and need not describe a central subgroup scheme. The functorial definition below is equivalent, by Yoneda, to factorization of the kernel through the scheme-theoretic centre once that closed subgroup has been constructed.

The API records the equivalent pointwise statement that the kernel of every induced group homomorphism is contained in the ordinary group centre. It also shows that isomorphisms have central kernel and that every isogeny out of a commutative group scheme is central.

Main declarations

• TauCeti.GroupScheme.pointMap: the homomorphism induced on points over a test scheme.
• TauCeti.GroupScheme.pointMap_injective_of_mono: a morphism monic in Over X induces an injective map on points over every test scheme.
• TauCeti.GroupScheme.HasCentralKernel: every functor-of-points kernel is central.
• TauCeti.GroupScheme.hasCentralKernel: the corresponding morphism property.
• TauCeti.GroupScheme.isogenies: the finite, flat, surjective morphism property on group schemes.
• TauCeti.GroupScheme.IsIsogeny: the corresponding predicate on a group-scheme morphism.
• TauCeti.GroupScheme.centralIsogenies: the central-isogeny morphism property.
• TauCeti.GroupScheme.IsCentralIsogeny: an isogeny with central kernel.
• TauCeti.GroupScheme.isCentralIsogeny_iff_isIsogeny_and_hasCentralKernel: the predicate-level bridge to the two constituent properties.

References

• J. S. Milne, Algebraic Groups (2017), §18.a.

The property-level isogeny API is adapted from TauCeti.AlgebraicGeometry.AbelianVariety.Isogeny.

This supplies the central-isogeny interface required by Layer 6 of the ReductiveGroups roadmap.

noncomputable def TauCeti.GroupScheme.pointMap {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (f : G ⟶ H) (T : CategoryTheory.Over X) : (T ⟶ G.X) →* (T ⟶ H.X)

The homomorphism induced by a group-scheme morphism on points valued in a test scheme over the base.

Equations

• TauCeti.GroupScheme.pointMap f T = GrpCat.Hom.hom ((CategoryTheory.yonedaGrp.map f).app (Opposite.op T))

@[simp]

theorem TauCeti.GroupScheme.pointMap_apply {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (f : G ⟶ H) (T : CategoryTheory.Over X) (g : T ⟶ G.X) : (pointMap f T) g = CategoryTheory.CategoryStruct.comp g f.hom.hom

The map on points is postcomposition with the underlying morphism of group objects.

@[simp]

theorem TauCeti.GroupScheme.pointMap_id {X : AlgebraicGeometry.Scheme} (G : CategoryTheory.Grp (CategoryTheory.Over X)) (T : CategoryTheory.Over X) : pointMap (CategoryTheory.CategoryStruct.id G) T = MonoidHom.id (T ⟶ G.X)

The map on points induced by an identity morphism is the identity homomorphism.

@[simp]

theorem TauCeti.GroupScheme.pointMap_comp {X : AlgebraicGeometry.Scheme} {G H K : CategoryTheory.Grp (CategoryTheory.Over X)} (f : G ⟶ H) (g : H ⟶ K) (T : CategoryTheory.Over X) : pointMap (CategoryTheory.CategoryStruct.comp f g) T = (pointMap g T).comp (pointMap f T)

The map on points induced by a composite is the composite of the maps on points.

theorem TauCeti.GroupScheme.pointMap_injective_of_mono {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (e : G ⟶ H) [CategoryTheory.Mono e.hom.hom] (T : CategoryTheory.Over X) : Function.Injective ⇑(pointMap e T)

A group-scheme morphism monic in Over X induces an injective map on points over every test scheme.

def TauCeti.GroupScheme.hasCentralKernel (X : AlgebraicGeometry.Scheme) : CategoryTheory.MorphismProperty (CategoryTheory.Grp (CategoryTheory.Over X))

The morphism property of having central kernel: over every test scheme, each point in the kernel commutes with every point of the source.

This all-test-schemes condition is the functor-of-points formulation of the scheme-theoretic kernel being contained in the centre.

Equations

• TauCeti.GroupScheme.hasCentralKernel X f = ∀ (T : CategoryTheory.Over X) (g : T ⟶ G.X), CategoryTheory.CategoryStruct.comp g f.hom.hom = 1 → ∀ (h : T ⟶ G.X), Commute g h

@[reducible, inline]

abbrev TauCeti.GroupScheme.HasCentralKernel {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (f : G ⟶ H) : Prop

A group-scheme morphism has central kernel when it belongs to hasCentralKernel X.

Equations

• TauCeti.GroupScheme.HasCentralKernel f = TauCeti.GroupScheme.hasCentralKernel X f

theorem TauCeti.GroupScheme.hasCentralKernel_iff_pointMap_ker_le_center {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (f : G ⟶ H) : HasCentralKernel f ↔ ∀ (T : CategoryTheory.Over X), (pointMap f T).ker ≤ Subgroup.center (T ⟶ G.X)

A group-scheme morphism has central kernel exactly when the kernel of its map on points over every test scheme is contained in the ordinary group centre.

theorem TauCeti.GroupScheme.hasCentralKernel_of_mono {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (f : G ⟶ H) [CategoryTheory.Mono f.hom.hom] : HasCentralKernel f

A group-scheme morphism with monic underlying morphism has central kernel: every point in its kernel is the identity.

theorem TauCeti.GroupScheme.hasCentralKernel_of_isCommMonObj {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (f : G ⟶ H) [CategoryTheory.IsCommMonObj G.X] : HasCentralKernel f

Every morphism from a commutative group scheme has central kernel.

def TauCeti.GroupScheme.isogenies (R : Type u) [CommRing R] : CategoryTheory.MorphismProperty (CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R)))

The morphism property of being an isogeny of group schemes over a commutative ring: the underlying scheme morphism is finite, flat, and surjective.

Equations

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

@[reducible, inline]

abbrev TauCeti.GroupScheme.IsIsogeny {R : Type u} [CommRing R] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (f : G ⟶ H) : Prop

A homomorphism of group schemes is an isogeny when its underlying scheme morphism is finite, flat, and surjective.

Equations

• TauCeti.GroupScheme.IsIsogeny f = TauCeti.GroupScheme.isogenies R f

theorem TauCeti.GroupScheme.isIsogeny_iff {R : Type u} [CommRing R] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (f : G ⟶ H) : IsIsogeny f ↔ AlgebraicGeometry.IsFinite (CategoryTheory.Over.Hom.left f.hom.hom) ∧ AlgebraicGeometry.Flat (CategoryTheory.Over.Hom.left f.hom.hom) ∧ AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left f.hom.hom)

A group-scheme morphism is an isogeny exactly when its underlying scheme morphism is finite, flat, and surjective.

instance TauCeti.GroupScheme.instIsMultiplicativeGrpOverSchemeSpecOfIsogenies {R : Type u} [CommRing R] : (isogenies R).IsMultiplicative

Group-scheme isogenies contain identities and are closed under composition.

instance TauCeti.GroupScheme.instRespectsIsoGrpOverSchemeSpecOfIsogenies {R : Type u} [CommRing R] : (isogenies R).RespectsIso

Being a group-scheme isogeny is invariant under isomorphisms of arrows.

@[simp]

theorem TauCeti.GroupScheme.isIsogeny_id {R : Type u} [CommRing R] (G : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))) : IsIsogeny (CategoryTheory.CategoryStruct.id G)

The identity of a group scheme is an isogeny.

theorem TauCeti.GroupScheme.isIsogeny_of_isIso {R : Type u} [CommRing R] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (f : G ⟶ H) [CategoryTheory.IsIso f] : IsIsogeny f

Every isomorphism of group schemes is an isogeny.

theorem TauCeti.GroupScheme.IsIsogeny.isFinite {R : Type u} [CommRing R] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} {f : G ⟶ H} (hf : IsIsogeny f) : AlgebraicGeometry.IsFinite (CategoryTheory.Over.Hom.left f.hom.hom)

The underlying scheme morphism of a group-scheme isogeny is finite.

theorem TauCeti.GroupScheme.IsIsogeny.flat {R : Type u} [CommRing R] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} {f : G ⟶ H} (hf : IsIsogeny f) : AlgebraicGeometry.Flat (CategoryTheory.Over.Hom.left f.hom.hom)

The underlying scheme morphism of a group-scheme isogeny is flat.

theorem TauCeti.GroupScheme.IsIsogeny.surjective {R : Type u} [CommRing R] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} {f : G ⟶ H} (hf : IsIsogeny f) : AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left f.hom.hom)

The underlying scheme morphism of a group-scheme isogeny is surjective.

theorem TauCeti.GroupScheme.IsIsogeny.comp {R : Type u} [CommRing R] {G H K : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} {f : G ⟶ H} {g : H ⟶ K} (hf : IsIsogeny f) (hg : IsIsogeny g) : IsIsogeny (CategoryTheory.CategoryStruct.comp f g)

A composite of group-scheme isogenies is an isogeny.

def TauCeti.GroupScheme.centralIsogenies (k : Type u) [CommRing k] : CategoryTheory.MorphismProperty (CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)))

The morphism property of being a central isogeny of group schemes over a commutative ring.

Equations

• TauCeti.GroupScheme.centralIsogenies k = TauCeti.GroupScheme.isogenies k ⊓ TauCeti.GroupScheme.hasCentralKernel (AlgebraicGeometry.Spec ↧k)

@[reducible, inline]

abbrev TauCeti.GroupScheme.IsCentralIsogeny {k : Type u} [CommRing k] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} (f : G ⟶ H) : Prop

A central isogeny is an isogeny whose scheme-theoretic kernel is central, expressed on the functor of points over every test scheme.

Equations

• TauCeti.GroupScheme.IsCentralIsogeny f = TauCeti.GroupScheme.centralIsogenies k f

theorem TauCeti.GroupScheme.isCentralIsogeny_iff_isIsogeny_and_hasCentralKernel {k : Type u} [CommRing k] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} (f : G ⟶ H) : IsCentralIsogeny f ↔ IsIsogeny f ∧ HasCentralKernel f

A central isogeny is precisely an isogeny with central kernel.

theorem TauCeti.GroupScheme.centralIsogenies_eq {k : Type u} [CommRing k] : centralIsogenies k = isogenies k ⊓ hasCentralKernel (AlgebraicGeometry.Spec ↧k)

Central isogenies are the intersection of isogenies and morphisms with central kernel.

theorem TauCeti.GroupScheme.isCentralIsogeny_iff {k : Type u} [CommRing k] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} (f : G ⟶ H) : IsCentralIsogeny f ↔ AlgebraicGeometry.IsFinite (CategoryTheory.Over.Hom.left f.hom.hom) ∧ AlgebraicGeometry.Flat (CategoryTheory.Over.Hom.left f.hom.hom) ∧ AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left f.hom.hom) ∧ HasCentralKernel f

A morphism is a central isogeny exactly when its underlying scheme morphism is finite, flat, and surjective and its kernel is central on all scheme-valued points.

theorem TauCeti.GroupScheme.isCentralIsogeny_iff_pointMap_ker_le_center {k : Type u} [CommRing k] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} (f : G ⟶ H) : IsCentralIsogeny f ↔ AlgebraicGeometry.IsFinite (CategoryTheory.Over.Hom.left f.hom.hom) ∧ AlgebraicGeometry.Flat (CategoryTheory.Over.Hom.left f.hom.hom) ∧ AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left f.hom.hom) ∧ ∀ (T : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)), (pointMap f T).ker ≤ Subgroup.center (T ⟶ G.X)

A group-scheme morphism is a central isogeny exactly when it is finite, flat, and surjective and, on points over every test scheme, its kernel is contained in the ordinary group centre.

theorem TauCeti.GroupScheme.IsCentralIsogeny.isIsogeny {k : Type u} [CommRing k] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} {f : G ⟶ H} (hf : IsCentralIsogeny f) : IsIsogeny f

The isogeny underlying a central isogeny.

theorem TauCeti.GroupScheme.IsCentralIsogeny.isFinite {k : Type u} [CommRing k] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} {f : G ⟶ H} (hf : IsCentralIsogeny f) : AlgebraicGeometry.IsFinite (CategoryTheory.Over.Hom.left f.hom.hom)

The underlying scheme morphism of a central isogeny is finite.

theorem TauCeti.GroupScheme.IsCentralIsogeny.flat {k : Type u} [CommRing k] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} {f : G ⟶ H} (hf : IsCentralIsogeny f) : AlgebraicGeometry.Flat (CategoryTheory.Over.Hom.left f.hom.hom)

The underlying scheme morphism of a central isogeny is flat.

theorem TauCeti.GroupScheme.IsCentralIsogeny.surjective {k : Type u} [CommRing k] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} {f : G ⟶ H} (hf : IsCentralIsogeny f) : AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left f.hom.hom)

The underlying scheme morphism of a central isogeny is surjective.

theorem TauCeti.GroupScheme.IsCentralIsogeny.hasCentralKernel {k : Type u} [CommRing k] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} {f : G ⟶ H} (hf : IsCentralIsogeny f) : HasCentralKernel f

The central-kernel property underlying a central isogeny.

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

Every isogeny from a commutative group scheme is central.

@[simp]

theorem TauCeti.GroupScheme.isCentralIsogeny_id {k : Type u} [CommRing k] (G : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))) : IsCentralIsogeny (CategoryTheory.CategoryStruct.id G)

The identity of a group scheme is a central isogeny.

theorem TauCeti.GroupScheme.isCentralIsogeny_of_isIso {k : Type u} [CommRing k] {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} (f : G ⟶ H) [CategoryTheory.IsIso f] : IsCentralIsogeny f

Every isomorphism of group schemes is a central isogeny.