Finite étale schemes and their coordinate algebras

Finite étale schemes over an affine base are anti-equivalent to finite étale algebras over its coordinate ring. In particular, over a separably closed field they are equivalent to finite sets. These comparisons allow finite étale geometry to be expressed in terms of coordinate algebras without replacing a scheme by a chosen affine presentation.

The construction restricts Mathlib's fully faithful AlgebraicGeometry.algSpec; essential surjectivity uses affineness of finite morphisms. The inverse is naturally identified with AlgebraicGeometry.algΓ using AlgebraicGeometry.algΓAlgSpecAdjunction. The classification over a separably closed field uses CommAlgCat.FiniteEtale.equivOfIsSepClosed, and equivOfIsSepClosedFunctorCompInclIso identifies the finite set it attaches to a finite étale scheme with the set of sections of that scheme.

References

• The Stacks Project, Étale morphisms, Sections 29.36 and 58.2.

def TauCeti.finiteEtaleSchemeProperty (S : AlgebraicGeometry.Scheme) : CategoryTheory.ObjectProperty (CategoryTheory.Over S)

The property of a scheme over S being finite and étale over S.

@[simp]

theorem TauCeti.finiteEtaleSchemeProperty_iff {S : AlgebraicGeometry.Scheme} (X : CategoryTheory.Over S) : finiteEtaleSchemeProperty S X ↔ AlgebraicGeometry.IsFinite X.hom ∧ AlgebraicGeometry.Etale X.hom

A scheme over S is finite étale exactly when its structure morphism is finite and étale.

theorem TauCeti.finiteEtaleSchemeProperty_eq_overObj (S : AlgebraicGeometry.Scheme) : finiteEtaleSchemeProperty S = (@AlgebraicGeometry.IsFinite ⊓ @AlgebraicGeometry.Etale).overObj

The finite étale property of schemes over S is the object property of Over S induced by the morphism property IsFinite ⊓ Etale. Use it to apply Mathlib's closure results for MorphismProperty.overObj.

instance TauCeti.instHasOfPostcompPropertySchemeMinMorphismPropertyIsFiniteEtale_tauCeti : (@AlgebraicGeometry.IsFinite ⊓ @AlgebraicGeometry.Etale).HasOfPostcompProperty (@AlgebraicGeometry.IsFinite ⊓ @AlgebraicGeometry.Etale)

If f ≫ g and g are finite étale, then so is f.

@[reducible, inline]

abbrev TauCeti.FiniteEtaleScheme (S : AlgebraicGeometry.Scheme) : Type (u + 1)

Finite étale schemes over S, with all morphisms over S.

instance TauCeti.FiniteEtaleScheme.instIsFiniteHomSchemeObjOverFiniteEtaleSchemeProperty {S : AlgebraicGeometry.Scheme} (X : FiniteEtaleScheme S) : AlgebraicGeometry.IsFinite X.obj.hom

instance TauCeti.FiniteEtaleScheme.instEtaleHomSchemeObjOverFiniteEtaleSchemeProperty {S : AlgebraicGeometry.Scheme} (X : FiniteEtaleScheme S) : AlgebraicGeometry.Etale X.obj.hom

instance TauCeti.FiniteEtaleScheme.isFinite_hom_left {S : AlgebraicGeometry.Scheme} {X Y : FiniteEtaleScheme S} (f : X ⟶ Y) : AlgebraicGeometry.IsFinite (CategoryTheory.Over.Hom.left f.hom)

A morphism of finite étale schemes over S is finite.

instance TauCeti.FiniteEtaleScheme.etale_hom_left {S : AlgebraicGeometry.Scheme} {X Y : FiniteEtaleScheme S} (f : X ⟶ Y) : AlgebraicGeometry.Etale (CategoryTheory.Over.Hom.left f.hom)

A morphism of finite étale schemes over S is étale.

def TauCeti.FiniteEtaleScheme.ofHom {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsFinite f] [AlgebraicGeometry.Etale f] : FiniteEtaleScheme S

Bundle a scheme with a finite étale structure morphism.

@[simp]

theorem TauCeti.FiniteEtaleScheme.ofHom_obj {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsFinite f] [AlgebraicGeometry.Etale f] : (ofHom f).obj = CategoryTheory.Over.mk f

The underlying object over S of ofHom f is Over.mk f.

noncomputable def TauCeti.FiniteEtaleScheme.isTerminalOfHomId (S : AlgebraicGeometry.Scheme) : CategoryTheory.Limits.IsTerminal (ofHom (CategoryTheory.CategoryStruct.id S))

The base itself, through its identity, is a terminal finite étale scheme.

noncomputable def TauCeti.FiniteEtaleScheme.spec (R : CommRingCat) : CategoryTheory.Functor (CommAlgCat.FiniteEtale ↑R)ᵒᵖ (FiniteEtaleScheme (AlgebraicGeometry.Spec R))

The spectrum functor on finite étale algebras, with target finite étale schemes.

@[simp]

theorem TauCeti.FiniteEtaleScheme.spec_comp_ι (R : CommRingCat) : (spec R).comp (finiteEtaleSchemeProperty (AlgebraicGeometry.Spec R)).ι = (CommAlgCat.finiteEtale ↑R).ι.op.comp (AlgebraicGeometry.algSpec R)

Forgetting the finite étale properties of spec gives Mathlib's algebraic spectrum functor, on both objects and morphisms.

@[simp]

theorem TauCeti.FiniteEtaleScheme.spec_obj_obj (R : CommRingCat) (A : (CommAlgCat.FiniteEtale ↑R)ᵒᵖ) : ((spec R).obj A).obj = (AlgebraicGeometry.algSpec R).obj (Opposite.op (Opposite.unop A).obj)

The object over the base underlying a finite étale spectrum is Mathlib's algebraic spectrum of its coordinate algebra.

instance TauCeti.FiniteEtaleScheme.essSurj_spec (R : CommRingCat) : (spec R).EssSurj

instance TauCeti.FiniteEtaleScheme.instIsEquivalenceOppositeFiniteEtaleCarrierSpecSpec (R : CommRingCat) : (spec R).IsEquivalence

noncomputable def TauCeti.FiniteEtaleScheme.finiteEtaleCommAlgCatOpEquivFiniteEtaleScheme (R : CommRingCat) : (CommAlgCat.FiniteEtale ↑R)ᵒᵖ ≌ FiniteEtaleScheme (AlgebraicGeometry.Spec R)

Finite étale algebras over a commutative ring are anti-equivalent to finite étale schemes over its spectrum. The forward functor is spec.

@[simp]

theorem TauCeti.FiniteEtaleScheme.finiteEtaleCommAlgCatOpEquivFiniteEtaleScheme_functor (R : CommRingCat) : (finiteEtaleCommAlgCatOpEquivFiniteEtaleScheme R).functor = spec R

The forward functor of the finite étale anti-equivalence is the spectrum functor.

noncomputable def TauCeti.FiniteEtaleScheme.finiteEtaleCommAlgCatOpEquivFiniteEtaleSchemeInverseCompInclusionIso (R : CommRingCat) : (finiteEtaleCommAlgCatOpEquivFiniteEtaleScheme R).inverse.comp (CommAlgCat.finiteEtale ↑R).ι.op ≅ (finiteEtaleSchemeProperty (AlgebraicGeometry.Spec R)).ι.comp (AlgebraicGeometry.algΓ R)

After forgetting finiteness and étaleness, the inverse coordinate-algebra functor is naturally isomorphic to Mathlib's global-sections functor algΓ. The components identify coordinate algebras, and .hom.naturality identifies pullback on every morphism.

noncomputable def TauCeti.FiniteEtaleScheme.equivOfIsSepClosed (K : Type u) [Field K] [IsSepClosed K] : FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K) ≌ FintypeCat

Over a separably closed field, finite étale schemes are equivalent to finite sets. The inverse constructs the spectrum of the algebra of functions on the finite set.

@[simp]

theorem TauCeti.FiniteEtaleScheme.equivOfIsSepClosed_functor (K : Type u) [Field K] [IsSepClosed K] : (equivOfIsSepClosed K).functor = (finiteEtaleCommAlgCatOpEquivFiniteEtaleScheme ↧K).inverse.comp (CommAlgCat.FiniteEtale.finiteSpec K)

The finite-set classification takes the finite prime spectrum of the coordinate algebra. Its object and map computations are those of Mathlib's finiteSpec; the coordinate algebra and its pullback are identified with global sections by finiteEtaleCommAlgCatOpEquivFiniteEtaleSchemeInverseCompInclusionIso.

@[simp]

theorem TauCeti.FiniteEtaleScheme.equivOfIsSepClosed_inverse (K : Type u) [Field K] [IsSepClosed K] : (equivOfIsSepClosed K).inverse = (CommAlgCat.FiniteEtale.equivOfIsSepClosed K).inverse.comp (spec ↧K)

The inverse finite-set classification forms the function algebra and then takes its spectrum. Mathlib's inverse object and map lemmas compute the function-algebra functor.

noncomputable def TauCeti.FiniteEtaleScheme.equivOfIsSepClosedFunctorIsoFiber (K : Type u) [Field K] [IsSepClosed K] : (equivOfIsSepClosed K).functor ≅ (finiteEtaleCommAlgCatOpEquivFiniteEtaleScheme ↧K).inverse.comp (CommAlgCat.FiniteEtale.fiber K K)

The finite-set classification is naturally isomorphic to the geometric fibre of the coordinate algebra: algebra homomorphisms to the separably closed base field, with precomposition as the action on morphisms.

@[instance_reducible]

noncomputable instance TauCeti.FiniteEtaleScheme.uniqueEquivOfIsSepClosedFunctorObjOfHomId (K : Type u) [Field K] [IsSepClosed K] : Unique ((equivOfIsSepClosed K).functor.obj (ofHom (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧K)))).obj

Over a separably closed field K, the finite set that equivOfIsSepClosed attaches to the terminal finite étale scheme Spec K is a single point, since the equivalence preserves terminal objects.

noncomputable def TauCeti.FiniteEtaleScheme.equivOfIsSepClosedFunctorCompInclIso (K : Type u) [Field K] [IsSepClosed K] : (equivOfIsSepClosed K).functor.comp FintypeCat.incl ≅ (finiteEtaleSchemeProperty (AlgebraicGeometry.Spec ↧K)).ι.comp (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧K)))))

Over a separably closed field K, the finite set attached to a finite étale scheme by equivOfIsSepClosed is naturally its set of sections, that is, of its K-rational points.

theorem TauCeti.FiniteEtaleScheme.equivOfIsSepClosedFunctorCompInclIso_inv_app_apply (K : Type u) [Field K] [IsSepClosed K] (Y : FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K)) (g : CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧K)) ⟶ Y.obj) (a : ((equivOfIsSepClosed K).functor.obj (ofHom (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧K)))).obj) : (CategoryTheory.ConcreteCategory.hom ((equivOfIsSepClosedFunctorCompInclIso K).inv.app Y)) g = (CategoryTheory.ConcreteCategory.hom ((equivOfIsSepClosed K).functor.map (CategoryTheory.ObjectProperty.homMk (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g)))) a

A section g of a finite étale scheme Y over a separably closed field K corresponds to the image under (equivOfIsSepClosed K).functor of g of the unique point attached to Spec K. The point a is arbitrary, since that finite set has exactly one element.

theorem TauCeti.FiniteEtaleScheme.equivOfIsSepClosedFunctorCompInclIso_hom_app_apply (K : Type u) [Field K] [IsSepClosed K] (Y : FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K)) (y : ((equivOfIsSepClosed K).functor.obj Y).obj) : (CategoryTheory.ConcreteCategory.hom ((equivOfIsSepClosedFunctorCompInclIso K).hom.app Y)) y = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((equivOfIsSepClosed K).functor.preimage (FintypeCat.homMk fun (x : ((equivOfIsSepClosed K).functor.obj (ofHom (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧K)))).obj) => y)).hom

A point y of the finite set attached to a finite étale scheme Y over a separably closed field K corresponds to the section preimage of the map from the one-point set picking y.

theorem AlgebraicGeometry.Scheme.Hom.exists_finiteEtale_algebra {R : CommRingCat} {X : Scheme} (f : X ⟶ Spec R) [IsFinite f] [Etale f] : ∃ (B : CommAlgCat.FiniteEtale ↑R), Nonempty (CategoryTheory.Over.mk (Spec.algebraMap ↑R ↑B.obj) ≅ CategoryTheory.Over.mk f)

Every finite étale scheme over an affine base admits a finite étale coordinate algebra, with an isomorphism respecting the structure morphism.