Finite limits, finite coproducts, summands and epimorphisms of finite étale schemes

The category FiniteEtaleScheme S of finite étale schemes over a scheme S has a terminal object, fibre products and finite coproducts, all computed in Over S. Every monomorphism in it is the inclusion of a direct summand: its underlying morphism of schemes is an open and closed immersion, and the open complement of its image is again finite étale over S. These are the axioms (G1) and (G3), and the finite-coproduct half of (G2), of a Galois category in the sense of Lenstra, as they appear in Mathlib's CategoryTheory.PreGaloisCategory. Quotients by finite groups, the remaining half of (G2), are not treated here.

Main results

• TauCeti.FiniteEtaleScheme.isOpenImmersion_hom_left, TauCeti.FiniteEtaleScheme.isClosedImmersion_hom_left: the underlying morphism of a monomorphism of finite étale schemes is an open and closed immersion.
• TauCeti.FiniteEtaleScheme.clopenSubscheme: an open and closed subscheme of a finite étale S-scheme, as a finite étale S-scheme, with its inclusion clopenSubschemeι.
• TauCeti.FiniteEtaleScheme.exists_isColimit_binaryCofanMk_of_mono: every monomorphism of finite étale schemes is the first inclusion of a binary coproduct.
• TauCeti.FiniteEtaleScheme.epi_iff_surjective: a morphism of finite étale schemes is an epimorphism if and only if its underlying morphism of schemes is surjective.
• The category FiniteEtaleScheme S is balanced: a morphism that is both a monomorphism and an epimorphism is an isomorphism.
• The category FiniteEtaleScheme S is finitary extensive: finite coproducts are disjoint and stable under pullback.
• The category FiniteEtaleScheme S is closed in Over S under binary products, so it inherits the cartesian monoidal structure of Over S (Mathlib's CartesianMonoidalCategory.fullSubcategory), with the fibre product over S as tensor product.

The limit and colimit instances are deduced from Mathlib's closure results for MorphismProperty.overObj and from Mathlib's description of coproducts of schemes by disjoint open covers, AlgebraicGeometry.nonempty_isColimit_binaryCofanMk_of_isCompl. Openness of monomorphisms uses AlgebraicGeometry.IsOpenImmersion.of_flat_of_mono. Surjective morphisms are epimorphisms because they are faithfully flat (AlgebraicGeometry.Flat.epi_of_flat_of_surjective); conversely the image of an epimorphism is a direct summand whose complement must be empty.

References

• H. W. Lenstra, Galois theory for schemes, Definition 3.1 and Section 5.
• The Stacks Project, Section 58.5 (tag 0BL8), Finite étale covers of schemes.

instance TauCeti.FiniteEtaleScheme.instIsClosedUnderLimitsOfShapeOverSchemeFiniteEtaleSchemePropertyDiscretePEmpty {S : AlgebraicGeometry.Scheme} : (finiteEtaleSchemeProperty S).IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})

instance TauCeti.FiniteEtaleScheme.instIsClosedUnderLimitsOfShapeOverSchemeFiniteEtaleSchemePropertyWalkingCospan {S : AlgebraicGeometry.Scheme} : (finiteEtaleSchemeProperty S).IsClosedUnderLimitsOfShape CategoryTheory.Limits.WalkingCospan

instance TauCeti.FiniteEtaleScheme.instIsClosedUnderIsomorphismsOverSchemeFiniteEtaleSchemeProperty {S : AlgebraicGeometry.Scheme} : (finiteEtaleSchemeProperty S).IsClosedUnderIsomorphisms

A scheme over S isomorphic to a finite étale one is finite étale.

instance TauCeti.FiniteEtaleScheme.instIsClosedUnderLimitsOfShapeOverSchemeFiniteEtaleSchemePropertyDiscreteWalkingPair {S : AlgebraicGeometry.Scheme} : (finiteEtaleSchemeProperty S).IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)

Binary products of finite étale schemes over S are finite étale: in Over S the product is the fibre product over the terminal object S.

instance TauCeti.FiniteEtaleScheme.instHasFiniteLimits {S : AlgebraicGeometry.Scheme} : CategoryTheory.Limits.HasFiniteLimits (FiniteEtaleScheme S)

Finite étale schemes over S have all finite limits, computed in Over S: the terminal object is S itself and fibre products are fibre products of schemes.

instance TauCeti.FiniteEtaleScheme.instIsClosedUnderColimitsOfShapeOverSchemeFiniteEtaleSchemePropertyDiscretePEmpty {S : AlgebraicGeometry.Scheme} : (finiteEtaleSchemeProperty S).IsClosedUnderColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})

instance TauCeti.FiniteEtaleScheme.instIsClosedUnderColimitsOfShapeOverSchemeFiniteEtaleSchemePropertyDiscreteWalkingPair {S : AlgebraicGeometry.Scheme} : (finiteEtaleSchemeProperty S).IsClosedUnderColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)

instance TauCeti.FiniteEtaleScheme.instIsClosedUnderFiniteCoproductsOverSchemeFiniteEtaleSchemeProperty {S : AlgebraicGeometry.Scheme} : (finiteEtaleSchemeProperty S).IsClosedUnderFiniteCoproducts

Finite étale schemes over S are closed under finite coproducts in Over S: the empty scheme and disjoint unions of finite étale schemes are finite étale.

instance TauCeti.FiniteEtaleScheme.instPreservesFiniteLimitsFullSubcategoryOverSchemeFiniteEtaleSchemePropertyι {S : AlgebraicGeometry.Scheme} : CategoryTheory.Limits.PreservesFiniteLimits (finiteEtaleSchemeProperty S).ι

The inclusion of finite étale schemes over S into Over S preserves finite limits.

@[instance_reducible]

noncomputable instance TauCeti.FiniteEtaleScheme.instBraidedCategory {S : AlgebraicGeometry.Scheme} : CategoryTheory.BraidedCategory (FiniteEtaleScheme S)

The braiding of the cartesian monoidal structure on finite étale schemes over S, whose tensor product is the fibre product over S.

instance TauCeti.FiniteEtaleScheme.instPreservesFiniteCoproductsFullSubcategoryOverSchemeFiniteEtaleSchemePropertyι {S : AlgebraicGeometry.Scheme} : CategoryTheory.Limits.PreservesFiniteCoproducts (finiteEtaleSchemeProperty S).ι

The inclusion of finite étale schemes over S into Over S preserves finite coproducts.

instance TauCeti.FiniteEtaleScheme.instFinitaryExtensive {S : AlgebraicGeometry.Scheme} : CategoryTheory.FinitaryExtensive (FiniteEtaleScheme S)

The category of finite étale schemes over S is finitary extensive: finite coproducts are disjoint and stable under pullback, since both are computed in the extensive category of schemes.

instance TauCeti.FiniteEtaleScheme.mono_hom_left {S : AlgebraicGeometry.Scheme} {X Y : FiniteEtaleScheme S} (i : X ⟶ Y) [CategoryTheory.Mono i] : CategoryTheory.Mono (CategoryTheory.Over.Hom.left i.hom)

The underlying morphism of schemes of a monomorphism of finite étale schemes is a monomorphism.

instance TauCeti.FiniteEtaleScheme.isOpenImmersion_hom_left {S : AlgebraicGeometry.Scheme} {X Y : FiniteEtaleScheme S} (i : X ⟶ Y) [CategoryTheory.Mono i] : AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Over.Hom.left i.hom)

The underlying morphism of schemes of a monomorphism of finite étale schemes is an open immersion.

instance TauCeti.FiniteEtaleScheme.isClosedImmersion_hom_left {S : AlgebraicGeometry.Scheme} {X Y : FiniteEtaleScheme S} (i : X ⟶ Y) [CategoryTheory.Mono i] : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i.hom)

The underlying morphism of schemes of a monomorphism of finite étale schemes is a closed immersion.

noncomputable def TauCeti.FiniteEtaleScheme.clopenSubscheme {S : AlgebraicGeometry.Scheme} {Y : FiniteEtaleScheme S} (U : Y.obj.left.Opens) (hU : IsClosed ↑U) : FiniteEtaleScheme S

An open subscheme U of a finite étale S-scheme Y that is also closed in Y is finite étale over S: its inclusion is an open and closed immersion.

noncomputable def TauCeti.FiniteEtaleScheme.clopenSubschemeι {S : AlgebraicGeometry.Scheme} {Y : FiniteEtaleScheme S} (U : Y.obj.left.Opens) (hU : IsClosed ↑U) : clopenSubscheme U hU ⟶ Y

The inclusion of an open and closed subscheme of a finite étale S-scheme Y into Y.

instance TauCeti.FiniteEtaleScheme.instMonoClopenSubschemeι {S : AlgebraicGeometry.Scheme} {Y : FiniteEtaleScheme S} (U : Y.obj.left.Opens) (hU : IsClosed ↑U) : CategoryTheory.Mono (clopenSubschemeι U hU)

The inclusion of an open and closed subscheme is a monomorphism.

@[simp]

theorem TauCeti.FiniteEtaleScheme.range_clopenSubschemeι_hom_left {S : AlgebraicGeometry.Scheme} {Y : FiniteEtaleScheme S} (U : Y.obj.left.Opens) (hU : IsClosed ↑U) : Set.range ⇑(CategoryTheory.Over.Hom.left (clopenSubschemeι U hU).hom) = ↑U

The image of the inclusion of an open and closed subscheme U is U.

theorem TauCeti.FiniteEtaleScheme.exists_isColimit_binaryCofanMk_of_mono {S : AlgebraicGeometry.Scheme} {X Y : FiniteEtaleScheme S} (i : X ⟶ Y) [CategoryTheory.Mono i] : ∃ (Z : FiniteEtaleScheme S) (u : Z ⟶ Y), Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk i u))

Every monomorphism i : X ⟶ Y of finite étale schemes over S is the inclusion of a direct summand: there is a finite étale Z over S with a morphism u : Z ⟶ Y exhibiting Y as the coproduct of X and Z. Here Z is the open complement of the image of i.

theorem TauCeti.FiniteEtaleScheme.epi_of_surjective {S : AlgebraicGeometry.Scheme} {X Y : FiniteEtaleScheme S} (g : X ⟶ Y) [AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left g.hom)] : CategoryTheory.Epi g

A morphism of finite étale schemes whose underlying morphism of schemes is surjective is an epimorphism.

instance TauCeti.FiniteEtaleScheme.surjective_hom_left {S : AlgebraicGeometry.Scheme} {X Y : FiniteEtaleScheme S} (g : X ⟶ Y) [CategoryTheory.Epi g] : AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left g.hom)

The underlying morphism of schemes of an epimorphism of finite étale schemes is surjective.

theorem TauCeti.FiniteEtaleScheme.epi_iff_surjective {S : AlgebraicGeometry.Scheme} {X Y : FiniteEtaleScheme S} (g : X ⟶ Y) : CategoryTheory.Epi g ↔ AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left g.hom)

A morphism of finite étale schemes is an epimorphism if and only if its underlying morphism of schemes is surjective.

instance TauCeti.FiniteEtaleScheme.instBalanced {S : AlgebraicGeometry.Scheme} : CategoryTheory.Balanced (FiniteEtaleScheme S)

The category of finite étale schemes over S is balanced: the underlying morphism of a monomorphism that is also an epimorphism is a surjective open immersion, hence an isomorphism.