Base change and geometric fibres of finite étale schemes

Finite étale morphisms are stable under base change, so pulling back along f : T ⟶ S restricts Mathlib's Over.pullback f to a functor FiniteEtaleScheme.pullback f from finite étale S-schemes to finite étale T-schemes. Base change along identities and composites is identified with the identity and with composites of base changes by pullbackId and pullbackComp, whose components are those of Over.pullbackId and Over.pullbackComp. These identifications are coherent: pullbackComp x (𝟙 S) is the base change of pullbackId (pullbackComp_id_inv_app_comp_eqToHom), and the two identifications of base change along a triple composite agree (pullbackComp_comp_inv_app_comp_eqToHom), up to the equalities x ≫ 𝟙 S = x and x ≫ f ≫ g = (x ≫ f) ≫ g.

For a geometric point x : Spec Ω ⟶ S, with Ω a separably closed field, the geometric fibre functor FiniteEtaleScheme.fiber x sends a finite étale S-scheme X to the finite set attached to X ×_S Spec Ω by the classification of finite étale schemes over a separably closed field. This is the functor on finite étale covers whose automorphisms define the étale fundamental group based at x.

The fibre functor is corepresented by the geometric point itself: FiniteEtaleScheme.fiberCompInclIso identifies fiber x with the set of lifts of x to X, that is, with morphisms Over.mk x ⟶ X in Over S. Its proof combines the adjunction Over.map x ⊣ Over.pullback x with equivOfIsSepClosedFunctorCompInclIso, which identifies the finite set attached to a finite étale Spec Ω-scheme with its set of sections. Changing the geometric point along a morphism of bases is pullbackCompFiberIso, compatibly with identities and composites (pullbackCompFiberIso_id_hom_app, pullbackCompFiberIso_comp_hom_app). These compatibilities make the étale fundamental group functorial in the scheme.

References

• A. Grothendieck, SGA 1, Exposé V, §§4–7.
• H. W. Lenstra, Galois theory for schemes.
• The Stacks Project, Section 58.5 (Finite étale covers of schemes).

noncomputable def TauCeti.FiniteEtaleScheme.pullback {S T : AlgebraicGeometry.Scheme} (f : T ⟶ S) : CategoryTheory.Functor (FiniteEtaleScheme S) (FiniteEtaleScheme T)

Base change of finite étale schemes along f : T ⟶ S, sending X to X ×_S T over T. On underlying objects over the bases it is Mathlib's Over.pullback f.

@[simp]

theorem TauCeti.FiniteEtaleScheme.pullback_comp_ι {S T : AlgebraicGeometry.Scheme} (f : T ⟶ S) : (pullback f).comp (finiteEtaleSchemeProperty T).ι = (finiteEtaleSchemeProperty S).ι.comp (CategoryTheory.Over.pullback f)

Forgetting finiteness and étaleness, base change is Over.pullback.

@[simp]

theorem TauCeti.FiniteEtaleScheme.pullback_obj_obj {S T : AlgebraicGeometry.Scheme} (f : T ⟶ S) (X : FiniteEtaleScheme S) : ((pullback f).obj X).obj = (CategoryTheory.Over.pullback f).obj X.obj

The scheme over T underlying a base change is Over.pullback f of the original.

@[simp]

theorem TauCeti.FiniteEtaleScheme.pullback_map_hom {S T : AlgebraicGeometry.Scheme} (f : T ⟶ S) {X Y : FiniteEtaleScheme S} (g : X ⟶ Y) : ((pullback f).map g).hom = (CategoryTheory.Over.pullback f).map g.hom

On morphisms, base change is Over.pullback f.

noncomputable def TauCeti.FiniteEtaleScheme.pullbackId {S : AlgebraicGeometry.Scheme} : pullback (CategoryTheory.CategoryStruct.id S) ≅ CategoryTheory.Functor.id (FiniteEtaleScheme S)

Base change along the identity is the identity, with components those of Over.pullbackId.

@[simp]

theorem TauCeti.FiniteEtaleScheme.pullbackId_hom_app_hom {S : AlgebraicGeometry.Scheme} (X : FiniteEtaleScheme S) : (pullbackId.hom.app X).hom = CategoryTheory.Over.pullbackId.hom.app X.obj

The components of pullbackId.hom are those of Over.pullbackId.hom.

@[simp]

theorem TauCeti.FiniteEtaleScheme.pullbackId_inv_app_hom {S : AlgebraicGeometry.Scheme} (X : FiniteEtaleScheme S) : (pullbackId.inv.app X).hom = CategoryTheory.Over.pullbackId.inv.app X.obj

The components of pullbackId.inv are those of Over.pullbackId.inv.

noncomputable def TauCeti.FiniteEtaleScheme.pullbackComp {S T U : AlgebraicGeometry.Scheme} (f : T ⟶ S) (g : S ⟶ U) : pullback (CategoryTheory.CategoryStruct.comp f g) ≅ (pullback g).comp (pullback f)

Base change along a composite is the composite of the base changes, with components those of Over.pullbackComp.

@[simp]

theorem TauCeti.FiniteEtaleScheme.pullbackComp_hom_app_hom {S T U : AlgebraicGeometry.Scheme} (f : T ⟶ S) (g : S ⟶ U) (X : FiniteEtaleScheme U) : ((pullbackComp f g).hom.app X).hom = (CategoryTheory.Over.pullbackComp f g).hom.app X.obj

The components of (pullbackComp f g).hom are those of Over.pullbackComp.

@[simp]

theorem TauCeti.FiniteEtaleScheme.pullbackComp_inv_app_hom {S T U : AlgebraicGeometry.Scheme} (f : T ⟶ S) (g : S ⟶ U) (X : FiniteEtaleScheme U) : ((pullbackComp f g).inv.app X).hom = (CategoryTheory.Over.pullbackComp f g).inv.app X.obj

The components of (pullbackComp f g).inv are those of Over.pullbackComp.

theorem TauCeti.FiniteEtaleScheme.pullbackComp_id_inv_app_comp_eqToHom {S T : AlgebraicGeometry.Scheme} (x : T ⟶ S) (X : FiniteEtaleScheme S) : CategoryTheory.CategoryStruct.comp ((pullbackComp x (CategoryTheory.CategoryStruct.id S)).inv.app X) (CategoryTheory.eqToHom ⋯) = (pullback x).map (pullbackId.hom.app X)

Base change along x : T ⟶ S of the identification pullbackId of base change along the identity is the composition isomorphism pullbackComp x (𝟙 S), up to the equality x ≫ 𝟙 S = x.

theorem TauCeti.FiniteEtaleScheme.pullbackComp_id_inv_app_comp_eqToHom_assoc {S T : AlgebraicGeometry.Scheme} (x : T ⟶ S) (X : FiniteEtaleScheme S) {Z : FiniteEtaleScheme T} (h : (pullback x).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((pullbackComp x (CategoryTheory.CategoryStruct.id S)).inv.app X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp ((pullback x).map (pullbackId.hom.app X)) h

Base change along x : T ⟶ S of the identification pullbackId of base change along the identity is the composition isomorphism pullbackComp x (𝟙 S), up to the equality x ≫ 𝟙 S = x.

theorem TauCeti.FiniteEtaleScheme.pullbackComp_comp_inv_app_comp_eqToHom {S T U V : AlgebraicGeometry.Scheme} (x : V ⟶ T) (f : T ⟶ S) (g : S ⟶ U) (X : FiniteEtaleScheme U) : CategoryTheory.CategoryStruct.comp ((pullbackComp x (CategoryTheory.CategoryStruct.comp f g)).inv.app X) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp ((pullback x).map ((pullbackComp f g).hom.app X)) (CategoryTheory.CategoryStruct.comp ((pullbackComp x f).inv.app ((pullback g).obj X)) ((pullbackComp (CategoryTheory.CategoryStruct.comp x f) g).inv.app X))

The two ways of identifying base change along x ≫ f ≫ g with the composite of the base changes along g, f and x agree, up to the equality x ≫ f ≫ g = (x ≫ f) ≫ g.

theorem TauCeti.FiniteEtaleScheme.pullbackComp_comp_inv_app_comp_eqToHom_assoc {S T U V : AlgebraicGeometry.Scheme} (x : V ⟶ T) (f : T ⟶ S) (g : S ⟶ U) (X : FiniteEtaleScheme U) {Z : FiniteEtaleScheme V} (h : (pullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp x f) g)).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((pullbackComp x (CategoryTheory.CategoryStruct.comp f g)).inv.app X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp ((pullback x).map ((pullbackComp f g).hom.app X)) (CategoryTheory.CategoryStruct.comp ((pullbackComp x f).inv.app ((pullback g).obj X)) (CategoryTheory.CategoryStruct.comp ((pullbackComp (CategoryTheory.CategoryStruct.comp x f) g).inv.app X) h))

The two ways of identifying base change along x ≫ f ≫ g with the composite of the base changes along g, f and x agree, up to the equality x ≫ f ≫ g = (x ≫ f) ≫ g.

noncomputable def TauCeti.FiniteEtaleScheme.fiber {S : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (x : AlgebraicGeometry.Spec ↧Ω ⟶ S) : CategoryTheory.Functor (FiniteEtaleScheme S) FintypeCat

The geometric fibre functor at a geometric point x : Spec Ω ⟶ S, for Ω separably closed: a finite étale S-scheme X goes to the finite set classifying X ×_S Spec Ω.

theorem TauCeti.FiniteEtaleScheme.fiber_def {S : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (x : AlgebraicGeometry.Spec ↧Ω ⟶ S) : fiber x = (pullback x).comp (equivOfIsSepClosed Ω).functor

The geometric fibre functor is base change to the geometric point followed by the classification of finite étale schemes over a separably closed field.

noncomputable def TauCeti.FiniteEtaleScheme.fiberCompInclIso {S : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (x : AlgebraicGeometry.Spec ↧Ω ⟶ S) : (fiber x).comp FintypeCat.incl ≅ (finiteEtaleSchemeProperty S).ι.comp (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Over.mk x)))

The geometric fibre functor at x is corepresented by x: the fibre of X is naturally the set of lifts of x to X, that is, of morphisms Over.mk x ⟶ X over S.

theorem TauCeti.FiniteEtaleScheme.fiberCompInclIso_inv_app_apply {S : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (x : AlgebraicGeometry.Spec ↧Ω ⟶ S) (X : FiniteEtaleScheme S) (g : CategoryTheory.Over.mk x ⟶ X.obj) : (CategoryTheory.ConcreteCategory.hom ((fiberCompInclIso x).inv.app X)) g = (CategoryTheory.ConcreteCategory.hom ((equivOfIsSepClosedFunctorCompInclIso Ω).inv.app ((pullback x).obj X))) (((CategoryTheory.Over.mapPullbackAdj x).homEquiv (Opposite.unop (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧Ω))))) ((finiteEtaleSchemeProperty S).ι.obj X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.homMk (CategoryTheory.CategoryStruct.id ((CategoryTheory.Over.map x).obj (Opposite.unop (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧Ω)))))).left) ⋯) g))

A lift g : Over.mk x ⟶ X of the geometric point x gives the point of the fibre corresponding, under equivOfIsSepClosedFunctorCompInclIso, to the section of X ×_S Spec Ω adjoint to g under Over.map x ⊣ Over.pullback x.

theorem TauCeti.FiniteEtaleScheme.fiberCompInclIso_hom_app_apply {S : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (x : AlgebraicGeometry.Spec ↧Ω ⟶ S) (X : FiniteEtaleScheme S) (y : ((fiber x).obj X).obj) : (CategoryTheory.ConcreteCategory.hom ((fiberCompInclIso x).hom.app X)) y = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.homMk (CategoryTheory.CategoryStruct.id ((CategoryTheory.Over.map x).obj (Opposite.unop (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧Ω)))))).left) ⋯) (((CategoryTheory.Over.mapPullbackAdj x).homEquiv (Opposite.unop (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧Ω))))) ((finiteEtaleSchemeProperty S).ι.obj X)).symm ((CategoryTheory.ConcreteCategory.hom ((equivOfIsSepClosedFunctorCompInclIso Ω).hom.app ((pullback x).obj X))) y))

A point y of the fibre gives the lift of x adjoint, under Over.map x ⊣ Over.pullback x, to the section of X ×_S Spec Ω corresponding to y under equivOfIsSepClosedFunctorCompInclIso.

noncomputable def TauCeti.FiniteEtaleScheme.fiberIdIso (Ω : Type u) [Field Ω] [IsSepClosed Ω] : fiber (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧Ω)) ≅ (equivOfIsSepClosed Ω).functor

The geometric fibre functor of Spec Ω at its identity point is the classification of finite étale schemes over the separably closed field Ω by finite sets.

@[simp]

theorem TauCeti.FiniteEtaleScheme.fiberIdIso_hom_app (Ω : Type u) [Field Ω] [IsSepClosed Ω] (X : FiniteEtaleScheme (AlgebraicGeometry.Spec ↧Ω)) : (fiberIdIso Ω).hom.app X = (equivOfIsSepClosed Ω).functor.map (pullbackId.hom.app X)

The components of fiberIdIso are the images of those of pullbackId.

@[simp]

theorem TauCeti.FiniteEtaleScheme.fiberIdIso_inv_app (Ω : Type u) [Field Ω] [IsSepClosed Ω] (X : FiniteEtaleScheme (AlgebraicGeometry.Spec ↧Ω)) : (fiberIdIso Ω).inv.app X = (equivOfIsSepClosed Ω).functor.map (pullbackId.inv.app X)

The components of (fiberIdIso Ω).inv are the images of those of pullbackId.inv.

noncomputable def TauCeti.FiniteEtaleScheme.pullbackCompFiberIso {S T : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (f : T ⟶ S) (x : AlgebraicGeometry.Spec ↧Ω ⟶ T) : (pullback f).comp (fiber x) ≅ fiber (CategoryTheory.CategoryStruct.comp x f)

Base change along f : T ⟶ S followed by the geometric fibre at x : Spec Ω ⟶ T is the geometric fibre at the composite geometric point x ≫ f.

@[simp]

theorem TauCeti.FiniteEtaleScheme.pullbackCompFiberIso_hom_app {S T : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (f : T ⟶ S) (x : AlgebraicGeometry.Spec ↧Ω ⟶ T) (X : FiniteEtaleScheme S) : (pullbackCompFiberIso f x).hom.app X = (equivOfIsSepClosed Ω).functor.map ((pullbackComp x f).inv.app X)

The components of pullbackCompFiberIso are the images of those of pullbackComp.

@[simp]

theorem TauCeti.FiniteEtaleScheme.pullbackCompFiberIso_inv_app {S T : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (f : T ⟶ S) (x : AlgebraicGeometry.Spec ↧Ω ⟶ T) (X : FiniteEtaleScheme S) : (pullbackCompFiberIso f x).inv.app X = (equivOfIsSepClosed Ω).functor.map ((pullbackComp x f).hom.app X)

The components of (pullbackCompFiberIso f x).inv are the images of those of pullbackComp.

theorem TauCeti.FiniteEtaleScheme.pullbackCompFiberIso_id_hom_app {S : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (x : AlgebraicGeometry.Spec ↧Ω ⟶ S) (X : FiniteEtaleScheme S) : CategoryTheory.CategoryStruct.comp ((pullbackCompFiberIso (CategoryTheory.CategoryStruct.id S) x).hom.app X) (CategoryTheory.eqToHom ⋯) = (fiber x).map (pullbackId.hom.app X)

Changing the geometric point along the identity: pullbackCompFiberIso (𝟙 S) x is the geometric fibre of pullbackId, up to the equality x ≫ 𝟙 S = x.

theorem TauCeti.FiniteEtaleScheme.pullbackCompFiberIso_id_hom_app_assoc {S : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (x : AlgebraicGeometry.Spec ↧Ω ⟶ S) (X : FiniteEtaleScheme S) {Z : FintypeCat} (h : (fiber x).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((pullbackCompFiberIso (CategoryTheory.CategoryStruct.id S) x).hom.app X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp ((fiber x).map (pullbackId.hom.app X)) h

Changing the geometric point along the identity: pullbackCompFiberIso (𝟙 S) x is the geometric fibre of pullbackId, up to the equality x ≫ 𝟙 S = x.

theorem TauCeti.FiniteEtaleScheme.pullbackCompFiberIso_comp_hom_app {S T U : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (f : T ⟶ S) (g : S ⟶ U) (x : AlgebraicGeometry.Spec ↧Ω ⟶ T) (X : FiniteEtaleScheme U) : CategoryTheory.CategoryStruct.comp ((pullbackCompFiberIso (CategoryTheory.CategoryStruct.comp f g) x).hom.app X) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp ((fiber x).map ((pullbackComp f g).hom.app X)) (CategoryTheory.CategoryStruct.comp ((pullbackCompFiberIso f x).hom.app ((pullback g).obj X)) ((pullbackCompFiberIso g (CategoryTheory.CategoryStruct.comp x f)).hom.app X))

Changing the geometric point along a composite f ≫ g is changing it along f and then along g, up to the equality x ≫ f ≫ g = (x ≫ f) ≫ g.

theorem TauCeti.FiniteEtaleScheme.pullbackCompFiberIso_comp_hom_app_assoc {S T U : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (f : T ⟶ S) (g : S ⟶ U) (x : AlgebraicGeometry.Spec ↧Ω ⟶ T) (X : FiniteEtaleScheme U) {Z : FintypeCat} (h : (fiber (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp x f) g)).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((pullbackCompFiberIso (CategoryTheory.CategoryStruct.comp f g) x).hom.app X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp ((fiber x).map ((pullbackComp f g).hom.app X)) (CategoryTheory.CategoryStruct.comp ((pullbackCompFiberIso f x).hom.app ((pullback g).obj X)) (CategoryTheory.CategoryStruct.comp ((pullbackCompFiberIso g (CategoryTheory.CategoryStruct.comp x f)).hom.app X) h))

Changing the geometric point along a composite f ≫ g is changing it along f and then along g, up to the equality x ≫ f ≫ g = (x ≫ f) ≫ g.