Finite étale group schemes

Group objects in FiniteEtaleScheme S are the finite étale group schemes over S: the inclusion into Over S preserves finite products, so it is a braided monoidal functor for the cartesian monoidal structures and carries group objects to group schemes over S, fully faithfully. A group scheme over S comes from FiniteEtaleScheme S exactly when its underlying scheme is finite étale over S (TauCeti.FiniteEtaleScheme.essImage_mapGrp_ι_iff).

Main results

• TauCeti.FiniteEtaleScheme.essImage_mapGrp_ι_iff: the group schemes over S coming from group objects of FiniteEtaleScheme S are those whose underlying scheme is finite étale over S.

@[instance_reducible]

noncomputable instance TauCeti.FiniteEtaleScheme.instMonoidalFullSubcategoryOverSchemeFiniteEtaleSchemePropertyι (S : AlgebraicGeometry.Scheme) : (finiteEtaleSchemeProperty S).ι.Monoidal

The inclusion of finite étale schemes over S into Over S is monoidal for the cartesian monoidal structures, as it preserves finite products.

@[instance_reducible]

noncomputable instance TauCeti.FiniteEtaleScheme.instBraidedFullSubcategoryOverSchemeFiniteEtaleSchemePropertyι (S : AlgebraicGeometry.Scheme) : (finiteEtaleSchemeProperty S).ι.Braided

The inclusion of finite étale schemes over S into Over S is braided.

theorem TauCeti.FiniteEtaleScheme.essImage_mapGrp_ι_iff {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.Grp (CategoryTheory.Over S)} : (finiteEtaleSchemeProperty S).ι.mapGrp.essImage G ↔ AlgebraicGeometry.IsFinite G.X.hom ∧ AlgebraicGeometry.Etale G.X.hom

Finite étale group schemes. A group scheme over S is, up to isomorphism, a group object of finite étale schemes over S if and only if its underlying scheme is finite and étale over S.