Residue fields of schemes and their behaviour under base change

This file records how the condition (N : κ(x)) ≠ 0, that a natural number N is invertible in the residue field at a point x, carries over between schemes. It is the form in which "N is invertible on the base" enters the theory of level structures on elliptic curves.

It also provides the geometric point Spec κ(x)ᵃˡᵍ ⟶ X over a point x, through which such conditions are checked after base change to an algebraically closed field, and computes the canonical morphism Spec κ(x) ⟶ X on the opens containing x.

Main definitions

• AlgebraicGeometry.Scheme.fromSpecAlgebraicClosure X x: the morphism Spec κ(x)ᵃˡᵍ ⟶ X from the spectrum of an algebraic closure of the residue field at x, whose image is {x}.

Main results

• AlgebraicGeometry.Scheme.Hom.natCast_residueField_ne_zero: if N is invertible in the residue field at f x, then it is invertible in the residue field at x, for any morphism f.
• AlgebraicGeometry.Spec.natCast_residueField_ne_zero: if N is invertible in a field K, then it is invertible in the residue field of Spec K.
• AlgebraicGeometry.Scheme.eq_of_SpecMap_comp_fromSpecResidueField: maps out of κ(x) are determined by their spectra composed with Spec κ(x) ⟶ X, since this morphism is a monomorphism.
• AlgebraicGeometry.Scheme.fromSpecResidueField_closedPoint_mem: the closed point of Spec κ(x) lies over every open containing x.
• AlgebraicGeometry.Scheme.fromSpecResidueField_preimage_eq_top: the inverse image of an open containing x under Spec κ(x) ⟶ X is everything.
• AlgebraicGeometry.Scheme.fromSpecResidueField_appLE: on an open containing x, the morphism Spec κ(x) ⟶ X sends a function to its value at x.
• AlgebraicGeometry.Scheme.residueFieldSectionsIso: for an open V containing x, the functions on the inverse image of V in Spec κ(x) are κ(x), and Spec κ(x) ⟶ X acts on sections over V by evaluation at x (Scheme.fromSpecResidueField_app_residueFieldSectionsIso_hom).
• RingHom.isIso_SpecMap_residueFieldMap_iff: for a ring map φ : R →+* S and a prime x of S, the residue field map of Spec S ⟶ Spec R at x is an isomorphism iff the map of residue fields κ(φ⁻¹ x) → κ(x) is bijective. This translates conditions on residue fields between schemes and rings, for instance for étale neighbourhoods built from algebras.
• AlgebraicGeometry.Scheme.Hom.isIso_residueFieldMap_of_lift: a lift along f of a morphism Spec A ⟶ X from a local ring, inducing an isomorphism of residue fields, sends the closed point to a preimage of x at which f induces an isomorphism of residue fields.
• AlgebraicGeometry.Scheme.residueField_hom_ext: on a quasi-affine scheme, a ring map out of the residue field κ(x) is determined by its values on global functions evaluated at x.
• AlgebraicGeometry.Scheme.toSpecΓ_apply_asIdeal: the point of Spec Γ(X, ⊤) under x is the prime ideal of global functions vanishing at x.
• AlgebraicGeometry.Spec.map_algebraMap_residueField_closedPoint: the closed point of Spec κ(p) lies over the prime p of R.

The residue field map f.residueFieldMap x has source κ(f x). When f x is known to equal a point y only propositionally, for instance when f is an automorphism fixing x, it is composed with Scheme.residueFieldCongr to give a map κ(y) ⟶ κ(x). The lemmas Scheme.Hom.residueFieldCongr_inv_residueFieldMap_comp and its companions compute such composites without the casts that a direct rewrite of f x to y would produce.

A morphism surjective on stalks induces isomorphisms of residue fields. In a fibre product, if one of the two points has unchanged residue field over the base, the pair has a unique lift and the other projection preserves its residue field. These facts allow elementary étale neighbourhoods to be refined without splitting their distinguished points.

The pullback arguments use Mathlib's Scheme.Pullback.Triplet.tensor description of the points over a pair as the spectrum of the tensor product of their residue fields.

The two results on natural numbers only use that a ring homomorphism between fields, such as Mathlib's Scheme.Hom.residueFieldMap, preserves natural number casts and is injective.

theorem AlgebraicGeometry.Scheme.Hom.natCast_residueField_ne_zero {X Y : Scheme} (f : X ⟶ Y) {x : ↥X} {N : ℕ} (hN : ↑N ≠ 0) : ↑N ≠ 0

If N is invertible in the residue field at f x, it is invertible in the residue field at x.

theorem AlgebraicGeometry.Spec.natCast_residueField_ne_zero {K : Type u} [Field K] {N : ℕ} (hN : ↑N ≠ 0) (s : ↥(Spec ↧K)) : ↑N ≠ 0

If N is invertible in a field K, it is invertible in the residue field of Spec K.

theorem AlgebraicGeometry.Scheme.Hom.residueFieldCongr_inv_residueFieldMap_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {x : ↥X} {y : ↥Y} {z : ↥Z} (hf : f x = y) (hg : g y = z) (hfg : (CategoryTheory.CategoryStruct.comp f g) x = z) : CategoryTheory.CategoryStruct.comp (residueFieldCongr hfg).inv (residueFieldMap (CategoryTheory.CategoryStruct.comp f g) x) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (residueFieldCongr hg).inv (residueFieldMap g y)) (CategoryTheory.CategoryStruct.comp (residueFieldCongr hf).inv (residueFieldMap f x))

The residue field map of a composite, with sources identified along f x = y and g y = z, is the composite of the residue field maps.

theorem AlgebraicGeometry.Scheme.Hom.residueFieldCongr_inv_residueFieldMap_congr {X Y : Scheme} {f f' : X ⟶ Y} (e : f = f') {x : ↥X} {y : ↥Y} (h : f x = y) (h' : f' x = y) : CategoryTheory.CategoryStruct.comp (residueFieldCongr h).inv (residueFieldMap f x) = CategoryTheory.CategoryStruct.comp (residueFieldCongr h').inv (residueFieldMap f' x)

Equal morphisms have equal residue field maps, with sources identified along f x = y.

theorem AlgebraicGeometry.Scheme.residueFieldCongr_inv_residueFieldMap_id {X : Scheme} {x x' : ↥X} (h : (CategoryTheory.CategoryStruct.id X) x = x') : CategoryTheory.CategoryStruct.comp (residueFieldCongr h).inv (Hom.residueFieldMap (CategoryTheory.CategoryStruct.id X) x) = (residueFieldCongr ⋯).hom

The residue field map of the identity, with source identified along x = x', is the identification κ(x') ≅ κ(x).

theorem AlgebraicGeometry.Scheme.Hom.residueFieldCongr_inv_residueFieldMap_Γevaluation {X Y : Scheme} (f : X ⟶ Y) {x : ↥X} {y : ↥Y} (h : f x = y) (a : ↑(Y.presheaf.obj (Opposite.op ⊤))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (residueFieldCongr h).inv (residueFieldMap f x))) ((CategoryTheory.ConcreteCategory.hom (Y.Γevaluation y)) a) = (CategoryTheory.ConcreteCategory.hom (X.Γevaluation x)) ((CategoryTheory.ConcreteCategory.hom (appTop f)) a)

The residue field map at x, with source identified along f x = y, sends the value at y of a global function a to the value at x of its pullback f^*(a).

theorem AlgebraicGeometry.Scheme.toSpecΓ_apply_asIdeal (X : Scheme) (x : ↥X) : (X.toSpecΓ x).asIdeal = RingHom.ker (CommRingCat.Hom.hom (X.Γevaluation x))

The point of Spec Γ(X, ⊤) under x is the prime ideal of global functions vanishing at x.

theorem AlgebraicGeometry.Spec.residueField_hom_ext {R : CommRingCat} {p : ↥(Spec R)} {K : CommRingCat} {α β : (Spec R).residueField p ⟶ K} (h : CategoryTheory.CategoryStruct.comp ((Spec R).Γevaluation p) α = CategoryTheory.CategoryStruct.comp ((Spec R).Γevaluation p) β) : α = β

A ring map out of a residue field of Spec R is determined by its values on the elements of R.

@[simp]

theorem AlgebraicGeometry.Spec.map_algebraMap_residueField_closedPoint {R : Type u} [CommRing R] (p : PrimeSpectrum R) : (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField))) (IsLocalRing.closedPoint p.asIdeal.ResidueField) = p

The closed point of Spec κ(p) lies over p in Spec R.

theorem AlgebraicGeometry.Scheme.residueField_hom_ext {X : Scheme} [X.IsQuasiAffine] {x : ↥X} {K : CommRingCat} {α β : X.residueField x ⟶ K} (h : CategoryTheory.CategoryStruct.comp (X.Γevaluation x) α = CategoryTheory.CategoryStruct.comp (X.Γevaluation x) β) : α = β

On a quasi-affine scheme, a ring map out of the residue field κ(x) is determined by its values on global functions evaluated at x.

noncomputable def AlgebraicGeometry.Scheme.fromSpecAlgebraicClosure (X : Scheme) (x : ↥X) : Spec ↧(AlgebraicClosure ↑(X.residueField x)) ⟶ X

The geometric point of X over x: the morphism Spec κ(x)ᵃˡᵍ ⟶ X from the spectrum of an algebraic closure of the residue field at x, through X.fromSpecResidueField x.

theorem AlgebraicGeometry.Scheme.fromSpecAlgebraicClosure_def (X : Scheme) (x : ↥X) : X.fromSpecAlgebraicClosure x = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (algebraMap (↑(X.residueField x)) (AlgebraicClosure ↑(X.residueField x))))) (X.fromSpecResidueField x)

The geometric point over x factors through X.fromSpecResidueField x.

@[simp]

theorem AlgebraicGeometry.Scheme.fromSpecAlgebraicClosure_apply (X : Scheme) (x : ↥X) (p : ↥(Spec ↧(AlgebraicClosure ↑(X.residueField x)))) : (X.fromSpecAlgebraicClosure x) p = x

Every point of Spec κ(x)ᵃˡᵍ maps to x under the geometric point over x.

@[simp]

theorem AlgebraicGeometry.Scheme.range_fromSpecAlgebraicClosure (X : Scheme) (x : ↥X) : Set.range ⇑(X.fromSpecAlgebraicClosure x) = {x}

The geometric point over x has image exactly {x}.

theorem AlgebraicGeometry.Scheme.eq_of_SpecMap_comp_fromSpecResidueField {X : Scheme} {x : ↥X} {R : CommRingCat} {a b : X.residueField x ⟶ R} (h : CategoryTheory.CategoryStruct.comp (Spec.map a) (X.fromSpecResidueField x) = CategoryTheory.CategoryStruct.comp (Spec.map b) (X.fromSpecResidueField x)) : a = b

Two ring maps out of the residue field κ(x) agree once their spectra agree after composition with the canonical morphism Spec κ(x) ⟶ X.

instance AlgebraicGeometry.Scheme.Hom.isIso_residueFieldMap_of_surjectiveOnStalks {X Y : Scheme} (f : X ⟶ Y) [SurjectiveOnStalks f] (x : ↥X) : CategoryTheory.IsIso (residueFieldMap f x)

A morphism surjective on stalks induces isomorphisms on residue fields.

theorem AlgebraicGeometry.Scheme.Hom.isIso_residueFieldMap_of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥X) [CategoryTheory.IsIso (residueFieldMap (CategoryTheory.CategoryStruct.comp f g) x)] : CategoryTheory.IsIso (residueFieldMap g (f x))

If a composite preserves the residue field at a point, the second morphism preserves the residue field at the image point. In particular, this cancels an open immersion from a composite.

theorem AlgebraicGeometry.Scheme.Hom.isIso_residueFieldMap_of_lift {X U : Scheme} (f : U ⟶ X) {x : ↥X} {A : Type u} [CommRing A] [IsLocalRing A] (φ : X.presheaf.stalk x ⟶ ↧A) [IsLocalHom (CommRingCat.Hom.hom φ)] (hφ : Function.Bijective ⇑(IsLocalRing.ResidueField.map (CommRingCat.Hom.hom φ))) (s : Spec ↧A ⟶ U) (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.comp (Spec.map φ) (X.fromSpecStalk x)) : f (s (IsLocalRing.closedPoint A)) = x ∧ CategoryTheory.IsIso (residueFieldMap f (s (IsLocalRing.closedPoint A)))

A lift of a morphism Spec A ⟶ X inducing an isomorphism of residue fields passes through a point with unchanged residue field: if A is local, φ : 𝒪_{X,x} → A is a local homomorphism inducing an isomorphism of residue fields, and s : Spec A ⟶ U lifts the morphism Spec A ⟶ X given by φ along f, then s maps the closed point to a preimage of x at which f induces an isomorphism of residue fields.

instance AlgebraicGeometry.Scheme.Pullback.Triplet.isIso_tensorInl {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : Triplet f g) [CategoryTheory.IsIso (Hom.residueFieldMap g T.y)] : CategoryTheory.IsIso T.tensorInl

Tensoring with an unchanged residue field leaves the other residue field unchanged.

theorem AlgebraicGeometry.Scheme.Pullback.eq_of_fst_eq_snd_eq_of_isIso {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} {z z' : ↥(CategoryTheory.Limits.pullback f g)} (hx : (CategoryTheory.Limits.pullback.fst f g) z = (CategoryTheory.Limits.pullback.fst f g) z') (hy : (CategoryTheory.Limits.pullback.snd f g) z = (CategoryTheory.Limits.pullback.snd f g) z') [CategoryTheory.IsIso (Hom.residueFieldMap g ((CategoryTheory.Limits.pullback.snd f g) z'))] : z = z'

If the residue field of y is unchanged over the base, a pair (x, y) has at most one lift to the fibre product.

theorem AlgebraicGeometry.Scheme.Pullback.isIso_residueFieldMap_fst {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} (z : ↥(CategoryTheory.Limits.pullback f g)) [CategoryTheory.IsIso (Hom.residueFieldMap g ((CategoryTheory.Limits.pullback.snd f g) z))] : CategoryTheory.IsIso (Hom.residueFieldMap (CategoryTheory.Limits.pullback.fst f g) z)

Base change by a point with unchanged residue field preserves the residue field at every point above it. No finiteness or étaleness hypothesis is needed.

theorem AlgebraicGeometry.Scheme.fromSpecResidueField_closedPoint_mem {X : Scheme} (x : ↥X) {V : X.Opens} (hx : x ∈ V) : (X.fromSpecResidueField x) (IsLocalRing.closedPoint ↑(X.residueField x)) ∈ V

The closed point of Spec κ(x) maps to x, so it lies over every open containing x.

theorem AlgebraicGeometry.Scheme.fromSpecResidueField_preimage_eq_top {X : Scheme} (x : ↥X) {V : X.Opens} (hx : x ∈ V) : (TopologicalSpace.Opens.map (X.fromSpecResidueField x).base).obj V = ⊤

The inverse image of an open containing x under Spec κ(x) ⟶ X is everything.

theorem AlgebraicGeometry.Scheme.fromSpecResidueField_appLE {X : Scheme} (x : ↥X) {V : X.Opens} (hx : x ∈ V) (h : ⊤ ≤ (TopologicalSpace.Opens.map (X.fromSpecResidueField x).base).obj V) : Hom.appLE (X.fromSpecResidueField x) V ⊤ h = CategoryTheory.CategoryStruct.comp (X.evaluation V x hx) (ΓSpecIso (X.residueField x)).inv

On an open V containing x, the morphism Spec κ(x) ⟶ X sends a function to its value at x, as a global function on Spec κ(x).

noncomputable def AlgebraicGeometry.Scheme.residueFieldSectionsIso {X : Scheme} (x : ↥X) {V : X.Opens} (hx : x ∈ V) : (Spec (X.residueField x)).presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (X.fromSpecResidueField x).base).obj V)) ≅ X.residueField x

For an open V containing x, the functions on ι⁻¹ V = Spec κ(x) are κ(x), where ι : Spec κ(x) ⟶ X.

theorem AlgebraicGeometry.Scheme.residueFieldSectionsIso_inv {X : Scheme} (x : ↥X) {V : X.Opens} (hx : x ∈ V) : (residueFieldSectionsIso x hx).inv = CategoryTheory.CategoryStruct.comp (ΓSpecIso (X.residueField x)).inv ((Spec (X.residueField x)).presheaf.map (CategoryTheory.homOfLE ⋯).op)

The inverse of Scheme.residueFieldSectionsIso is restriction from ⊤ to ι⁻¹ V.

@[simp]

theorem AlgebraicGeometry.Scheme.residueFieldSectionsIso_map {X : Scheme} (x : ↥X) {U V : X.Opens} (hU : x ∈ U) (hV : x ∈ V) (j : (TopologicalSpace.Opens.map (X.fromSpecResidueField x).base).obj U ⟶ (TopologicalSpace.Opens.map (X.fromSpecResidueField x).base).obj V) : CategoryTheory.CategoryStruct.comp ((Spec (X.residueField x)).presheaf.map j.op) (residueFieldSectionsIso x hU).hom = (residueFieldSectionsIso x hV).hom

The identifications Scheme.residueFieldSectionsIso commute with restriction.

@[simp]

theorem AlgebraicGeometry.Scheme.residueFieldSectionsIso_map_assoc {X : Scheme} (x : ↥X) {U V : X.Opens} (hU : x ∈ U) (hV : x ∈ V) (j : (TopologicalSpace.Opens.map (X.fromSpecResidueField x).base).obj U ⟶ (TopologicalSpace.Opens.map (X.fromSpecResidueField x).base).obj V) {Z : CommRingCat} (h : X.residueField x ⟶ Z) : CategoryTheory.CategoryStruct.comp ((Spec (X.residueField x)).presheaf.map j.op) (CategoryTheory.CategoryStruct.comp (residueFieldSectionsIso x hU).hom h) = CategoryTheory.CategoryStruct.comp (residueFieldSectionsIso x hV).hom h

The identifications Scheme.residueFieldSectionsIso commute with restriction.

@[simp]

theorem AlgebraicGeometry.Scheme.fromSpecResidueField_app_residueFieldSectionsIso_hom {X : Scheme} (x : ↥X) {V : X.Opens} (hx : x ∈ V) : CategoryTheory.CategoryStruct.comp (Hom.app (X.fromSpecResidueField x) V) (residueFieldSectionsIso x hx).hom = X.evaluation V x hx

On an open V containing x, the morphism ι : Spec κ(x) ⟶ X acts on sections by evaluation at x.

@[simp]

theorem AlgebraicGeometry.Scheme.fromSpecResidueField_app_residueFieldSectionsIso_hom_assoc {X : Scheme} (x : ↥X) {V : X.Opens} (hx : x ∈ V) {Z : CommRingCat} (h : X.residueField x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.app (X.fromSpecResidueField x) V) (CategoryTheory.CategoryStruct.comp (residueFieldSectionsIso x hx).hom h) = CategoryTheory.CategoryStruct.comp (X.evaluation V x hx) h

On an open V containing x, the morphism ι : Spec κ(x) ⟶ X acts on sections by evaluation at x.

theorem RingHom.isIso_SpecMap_residueFieldMap_iff {R S : Type u} [CommRing R] [CommRing S] (φ : R →+* S) (x : ↥(AlgebraicGeometry.Spec ↧S)) (p : Ideal R) [p.IsPrime] (hp : p = Ideal.comap φ x.asIdeal) : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.residueFieldMap (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ)) x) ↔ Function.Bijective ⇑(Ideal.ResidueField.map p x.asIdeal φ hp)

For a ring map φ : R →+* S and a point x of Spec S, the residue field map of Spec.map φ at x is an isomorphism iff the induced map κ(p) → κ(x) is bijective, where p = φ⁻¹ x is the image point.

theorem AlgebraicGeometry.IsAffineOpen.isIso_residueFieldMap_spec_algebraMap_comp_fromSpec {S : Scheme} {U : S.Opens} (hU : IsAffineOpen U) {s : ↥S} (hs : s ∈ U) (R : Type u) [CommRing R] [Algebra (↑(S.presheaf.obj (Opposite.op U))) R] (u : ↥(Spec ↧R)) [u.asIdeal.LiesOver (hU.primeIdealOf ⟨s, hs⟩).asIdeal] (hres : Function.Bijective ⇑(Ideal.ResidueField.mapₐ (hU.primeIdealOf ⟨s, hs⟩).asIdeal u.asIdeal (Algebra.ofId ↑(S.presheaf.obj (Opposite.op U)) ↑↧R) ⋯)) : CategoryTheory.IsIso (Scheme.Hom.residueFieldMap (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (algebraMap (↑(S.presheaf.obj (Opposite.op U))) R))) hU.fromSpec) u)

The map Spec R ⟶ U ⊆ S induced by the structure map of a Γ(S, U)-algebra R on an affine open U induces an isomorphism of residue fields at a point u over the prime s of Γ(S, U) as soon as κ(s) ≅ κ(u).