Isogenies of group schemes

For group schemes over a scheme, an isogeny is a homomorphism whose underlying scheme morphism is finite, flat, and surjective. This file defines the corresponding morphism property and predicate, and shows that isogenies contain the isomorphisms and are closed under composition.

Main declarations

• TauCeti.GroupScheme.isogenies: the finite, flat, surjective morphism property on group schemes.
• TauCeti.GroupScheme.IsIsogeny: the corresponding predicate on a group-scheme morphism.

References

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

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

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

@[reducible, inline]

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

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

theorem TauCeti.GroupScheme.isIsogeny_iff {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (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.instIsMultiplicativeGrpOverSchemeIsogenies {X : AlgebraicGeometry.Scheme} : (isogenies X).IsMultiplicative

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

instance TauCeti.GroupScheme.instRespectsIsoGrpOverSchemeIsogenies {X : AlgebraicGeometry.Scheme} : (isogenies X).RespectsIso

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

@[simp]

theorem TauCeti.GroupScheme.isIsogeny_id {X : AlgebraicGeometry.Scheme} (G : CategoryTheory.Grp (CategoryTheory.Over X)) : IsIsogeny (CategoryTheory.CategoryStruct.id G)

The identity of a group scheme is an isogeny.

theorem TauCeti.GroupScheme.isIsogeny_of_isIso {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (f : G ⟶ H) [CategoryTheory.IsIso f] : IsIsogeny f

Every isomorphism of group schemes is an isogeny.

theorem TauCeti.GroupScheme.IsIsogeny.isFinite {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} {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 {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} {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 {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} {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 {X : AlgebraicGeometry.Scheme} {G H K : CategoryTheory.Grp (CategoryTheory.Over X)} {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.