Central isogenies and isomorphisms

An isogeny with monic underlying scheme morphism is an isomorphism. Central isogenies are also unchanged by replacing their source or target by an isomorphic group scheme. This file proves the corresponding MorphismProperty.RespectsIso instance and records the underlying fact that the all-test-schemes central-kernel condition is invariant under pre- and postcomposition with an isomorphism.

The proofs stay at the functor-of-points level used by GroupScheme.HasCentralKernel. A morphism monic in Over X induces an injective map on points over every test scheme. On the source this reflects commutativity, while on the target it shows that postcomposition does not change the pointwise kernel.

Main declarations

• TauCeti.GroupScheme.HasCentralKernel.precomp_of_mono: central kernels are preserved by precomposition with a morphism monic in Over X.
• TauCeti.GroupScheme.HasCentralKernel.postcomp_of_mono: central kernels are preserved by postcomposition with a morphism monic in Over X.
• TauCeti.GroupScheme.hasCentralKernel_comp_iff_of_mono: postcomposition by a morphism monic in Over X preserves and reflects central kernels.
• TauCeti.GroupScheme.hasCentralKernel_respectsIso: having central kernel respects isomorphisms of arrows.
• TauCeti.GroupScheme.IsIsogeny.isIso_of_mono: an isogeny whose underlying scheme morphism is monic is an isomorphism.
• TauCeti.GroupScheme.centralIsogenies_respectsIso: central isogenies respect isomorphisms of arrows.

References

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

This supplies the isomorphism-invariance needed by the central-isogeny, simply-connected and adjoint-form targets in Layer 6 of the ReductiveGroups roadmap.

theorem TauCeti.GroupScheme.HasCentralKernel.precomp_of_mono {X : AlgebraicGeometry.Scheme} {F G H : CategoryTheory.Grp (CategoryTheory.Over X)} (e : F ⟶ G) [CategoryTheory.Mono e.hom.hom] (f : G ⟶ H) (hf : HasCentralKernel f) : HasCentralKernel (CategoryTheory.CategoryStruct.comp e f)

Precomposing with a morphism monic in Over X preserves the central-kernel condition.

theorem TauCeti.GroupScheme.HasCentralKernel.postcomp_of_mono {X : AlgebraicGeometry.Scheme} {G H K : CategoryTheory.Grp (CategoryTheory.Over X)} (f : G ⟶ H) (e : H ⟶ K) [CategoryTheory.Mono e.hom.hom] (hf : HasCentralKernel f) : HasCentralKernel (CategoryTheory.CategoryStruct.comp f e)

Postcomposing with a morphism monic in Over X preserves the central-kernel condition.

theorem TauCeti.GroupScheme.hasCentralKernel_comp_iff_of_mono {X : AlgebraicGeometry.Scheme} {G H K : CategoryTheory.Grp (CategoryTheory.Over X)} (f : G ⟶ H) (e : H ⟶ K) [CategoryTheory.Mono e.hom.hom] : HasCentralKernel (CategoryTheory.CategoryStruct.comp f e) ↔ HasCentralKernel f

Postcomposition by a morphism monic in Over X preserves and reflects the central-kernel condition.

instance TauCeti.GroupScheme.hasCentralKernel_respectsIso {X : AlgebraicGeometry.Scheme} : (hasCentralKernel X).RespectsIso

Having central kernel is invariant under isomorphisms of arrows.

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

A group-scheme isogeny whose underlying scheme morphism is monic is an isomorphism.

instance TauCeti.GroupScheme.centralIsogenies_respectsIso {k : Type u} [CommRing k] : (centralIsogenies k).RespectsIso

Central isogenies are invariant under pre- and postcomposition with isomorphisms.