Étale morphisms: open immersions, and rational points of finite schemes over a field

A morphism of schemes is an open immersion exactly when it is étale and universally injective (AlgebraicGeometry.isOpenImmersion_iff_etale_and_universallyInjective): an unramified universally injective morphism is a monomorphism, and a flat monomorphism locally of finite presentation is an open immersion (Mathlib's AlgebraicGeometry.IsOpenImmersion.of_flat_of_mono). In particular an étale morphism that is universally injective and surjective, for instance an étale universal homeomorphism, is an isomorphism (AlgebraicGeometry.isIso_of_etale_of_universallyInjective_of_surjective).

Let f : X ⟶ Spec R be a morphism from an affine scheme to the spectrum of a commutative ring. Then f is étale exactly when Γ(X, ⊤) is an étale R-algebra. Its points with values in Spec R are the characters Γ(X, ⊤) →ₐ[R] R of its coordinate ring (AlgebraicGeometry.Scheme.Hom.pointsEquivAlgHom, in TauCeti.AlgebraicGeometry.RationalPoint.Affine).

Now let f : X ⟶ Spec K be a finite morphism to the spectrum of a field. A finite-dimensional K-algebra has at most as many characters as its dimension, which is the rank of f (AlgebraicGeometry.Scheme.Hom.finrank_eq_finrank_of_field). When X has at least that many points over Spec K, its coordinate ring is a finite product of copies of K (Algebra.IsFiniteSplit.of_finrank_le_card_algHom), so f is étale. Conversely, over a separably closed field a finite étale K-algebra is a finite product of copies of K, so a finite étale scheme over Spec K has exactly as many points over Spec K as its rank.

Points over Spec K are written as morphisms 𝟙_ (Over (Spec K)) ⟶ Over.mk f of the cartesian monoidal category Over (Spec K), as for the points of group schemes over Spec K.

Finally, let A be a local ring with residue field κ and B an A-algebra whose closed fibre κ ⊗[A] B is a finite étale κ-algebra. A field-valued point Spec L ⟶ Spec A of the closed point factors through κ, so the base change L ⊗[A] B is the base change of κ ⊗[A] B along κ → L; hence the base change of Spec B ⟶ Spec A to Spec L is finite étale of rank dim_κ (κ ⊗[A] B).

Main results

• AlgebraicGeometry.isOpenImmersion_iff_etale_and_universallyInjective: the open immersions are the étale universally injective morphisms.
• AlgebraicGeometry.isIso_of_etale_of_universallyInjective_of_surjective: an étale universally injective surjective morphism is an isomorphism.
• AlgebraicGeometry.Scheme.Hom.etale_iff_algebraEtale: for affine X, f : X ⟶ Spec R is étale exactly when Γ(X, ⊤) is an étale R-algebra.
• AlgebraicGeometry.Scheme.Hom.etale_of_finrank_le_natCard: a finite morphism f : X ⟶ Spec K with at least f.finrank s points of X over Spec K is étale.
• AlgebraicGeometry.Scheme.Hom.natCard_eq_finrank_of_etale: over a separably closed field K, a finite étale morphism f : X ⟶ Spec K has exactly f.finrank s points of X over Spec K.
• TauCeti.AlgebraicGeometry.etale_isFinite_finrank_of_isPullback_SpecMap: for a local ring A and an A-algebra B whose closed fibre is finite étale, the base change of Spec B ⟶ Spec A along a field-valued point of the closed point is finite étale of the same rank.

theorem AlgebraicGeometry.isOpenImmersion_iff_etale_and_universallyInjective {X Y : Scheme} (f : X ⟶ Y) : IsOpenImmersion f ↔ Etale f ∧ UniversallyInjective f

The open immersions are the étale universally injective morphisms. Stacks, Tag 025G.

theorem AlgebraicGeometry.IsOpenImmersion.of_etale_of_universallyInjective {X Y : Scheme} (f : X ⟶ Y) [Etale f] [UniversallyInjective f] : IsOpenImmersion f

An étale universally injective morphism is an open immersion.

theorem AlgebraicGeometry.isIso_of_etale_of_universallyInjective_of_surjective {X Y : Scheme} (f : X ⟶ Y) [Etale f] [UniversallyInjective f] [Surjective f] : CategoryTheory.IsIso f

An étale universally injective surjective morphism is an isomorphism.

theorem AlgebraicGeometry.Scheme.Hom.etale_iff_algebraEtale {R : Type u} [CommRing R] {X : Scheme} (f : X ⟶ Spec ↧R) [IsAffine X] [Algebra R ↑(X.presheaf.obj (Opposite.op ⊤))] (hf : algebraMap R ↑(X.presheaf.obj (Opposite.op ⊤)) = CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso ↧R).inv (appTop f))) : Etale f ↔ Algebra.Etale R ↑(X.presheaf.obj (Opposite.op ⊤))

A morphism f : X ⟶ Spec R from an affine scheme is étale exactly when its coordinate ring Γ(X, ⊤) is an étale R-algebra, for the R-algebra structure given by the map of global sections of f.

theorem AlgebraicGeometry.Scheme.Hom.etale_of_finrank_le_natCard {X : Scheme} {K : Type u} [Field K] (f : X ⟶ Spec ↧K) [IsFinite f] (s : ↥(Spec ↧K)) (h : finrank f s ≤ Nat.card (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (Spec ↧K)) ⟶ CategoryTheory.Over.mk f)) : Etale f

A finite scheme over a field with as many rational points as its degree is étale. Let f : X ⟶ Spec K be finite. If X has at least f.finrank s points over Spec K, then f is étale: the coordinate ring of X is a finite product of copies of K.

theorem AlgebraicGeometry.Scheme.Hom.natCard_eq_finrank_of_etale {X : Scheme} {K : Type u} [Field K] [IsSepClosed K] (f : X ⟶ Spec ↧K) [IsFinite f] [Etale f] (s : ↥(Spec ↧K)) : Nat.card (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (Spec ↧K)) ⟶ CategoryTheory.Over.mk f) = finrank f s

A finite étale scheme over a separably closed field has as many rational points as its degree. Let K be separably closed and f : X ⟶ Spec K finite étale. Then X has exactly f.finrank s points over Spec K: its coordinate ring is a finite product of copies of K.

instance TauCeti.AlgebraicGeometry.etale_isStableUnderComposition : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.Etale

Étale morphisms are stable under composition.

instance TauCeti.AlgebraicGeometry.etale_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.Etale

Being étale is invariant under isomorphisms of source and target.

instance TauCeti.AlgebraicGeometry.etale_hasPullbacksAlong {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.MorphismProperty.HasPullbacksAlong (@AlgebraicGeometry.Etale) f

Étale schemes over Y can be pulled back along any f : X ⟶ Y.

instance TauCeti.AlgebraicGeometry.etale_isStableUnderBaseChangeAlong {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlong (@AlgebraicGeometry.Etale) f

Étale morphisms are stable under base change along any f : X ⟶ Y.

theorem TauCeti.AlgebraicGeometry.etale_isFinite_finrank_of_isPullback_SpecMap {A L B : Type u} [CommRing A] [IsLocalRing A] [Field L] [Algebra A L] [IsLocalHom (algebraMap A L)] [CommRing B] [Algebra A B] [Algebra.Etale (IsLocalRing.ResidueField A) (TensorProduct A (IsLocalRing.ResidueField A) B)] [Module.Finite (IsLocalRing.ResidueField A) (TensorProduct A (IsLocalRing.ResidueField A) B)] {P : AlgebraicGeometry.Scheme} {fst : P ⟶ AlgebraicGeometry.Spec ↧B} {snd : P ⟶ AlgebraicGeometry.Spec ↧L} (h : CategoryTheory.IsPullback fst snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap A B))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap A L)))) : AlgebraicGeometry.Etale snd ∧ AlgebraicGeometry.IsFinite snd ∧ ∀ (y : ↥(AlgebraicGeometry.Spec ↧L)), AlgebraicGeometry.Scheme.Hom.finrank snd y = Module.finrank (IsLocalRing.ResidueField A) (TensorProduct A (IsLocalRing.ResidueField A) B)

If the closed fibre κ ⊗[A] B of A → B is a finite étale κ-algebra, then the base change of Spec B ⟶ Spec A along a field-valued point of the closed point of Spec A is finite étale, of the same rank.