The skyscraper sheaf of a residue field

For a point x of a scheme X, the skyscraper sheaf κ(x)ₓ has sections κ(x) over the open subsets containing x and 0 over the others, a regular function r acting through its value r(x) ∈ κ(x). This file realizes it as the pushforward of the structure sheaf along the canonical morphism Spec κ(x) ⟶ X, which makes the sheaf condition and the 𝒪_X-module structure automatic. Its restriction maps are surjective, so the sheaf is flasque. This is the residue-field analogue of Scheme.rationalFunctions, with x and κ(x) in place of the generic point and the function field.

On a Noetherian integral scheme whose codimension-one local rings are discrete valuation rings, the skyscraper sheaf at a closed codimension-one point x is the cokernel of the inclusion 𝒪_X(D) ⟶ 𝒪_X(D + x). This describes how adding a point to a divisor changes its divisor sheaf.

Main declarations

• Scheme.skyscraperResidueField x, the skyscraper sheaf κ(x)ₓ as an 𝒪_X-module;
• Scheme.skyscraperResidueFieldEquiv, the identification of its sections over an open subset containing x with κ(x), under which a regular function acts by multiplication with its value at x (Scheme.skyscraperResidueFieldEquiv_smul), and which commutes with restriction (Scheme.skyscraperResidueFieldEquiv_map);
• Scheme.subsingleton_skyscraperResidueField: the sections over an open subset not containing x vanish;
• Scheme.isFlasque_skyscraperResidueField: the skyscraper sheaf is flasque.

References

• R. Hartshorne, Algebraic Geometry, II, Exercise 1.17 (skyscraper sheaves) and IV, Theorem 1.3 (their role in the proof of Riemann–Roch).

noncomputable def AlgebraicGeometry.Scheme.skyscraperResidueField {X : Scheme} (x : ↥X) : X.Modules

The skyscraper sheaf κ(x)ₓ of the residue field at a point x, as an 𝒪_X-module: the pushforward of the structure sheaf of Spec κ(x) along Scheme.fromSpecResidueField. Its sections are κ(x) over the open subsets containing x (skyscraperResidueFieldEquiv) and 0 over the others (subsingleton_skyscraperResidueField).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.skyscraperResidueFieldEquiv {X : Scheme} (x : ↥X) {U : X.Opens} (hx : x ∈ U) : ↑((skyscraperResidueField x).presheaf.obj (Opposite.op U)) ≃+ ↑(X.residueField x)

The sections of the skyscraper sheaf κ(x)ₓ over an open subset containing x are the residue field κ(x).

Equations

• AlgebraicGeometry.Scheme.skyscraperResidueFieldEquiv x hx = (TauCeti.AlgebraicGeometry.residueFieldSectionsIso✝ x hx).commRingCatIsoToRingEquiv.toAddEquiv

@[simp]

theorem AlgebraicGeometry.Scheme.skyscraperResidueFieldEquiv_smul {X : Scheme} (x : ↥X) {U : X.Opens} (hx : x ∈ U) (r : ↑(X.presheaf.obj (Opposite.op U))) (s : ↑((skyscraperResidueField x).presheaf.obj (Opposite.op U))) : (skyscraperResidueFieldEquiv x hx) (r • s) = (CategoryTheory.ConcreteCategory.hom (X.evaluation U x hx)) r * (skyscraperResidueFieldEquiv x hx) s

A regular function acts on the sections of κ(x)ₓ by multiplication with its value at x.

@[simp]

theorem AlgebraicGeometry.Scheme.skyscraperResidueFieldEquiv_map {X : Scheme} (x : ↥X) {U V : X.Opens} (i : U ⟶ V) (hx : x ∈ U) (s : ↑((skyscraperResidueField x).presheaf.obj (Opposite.op V))) : (skyscraperResidueFieldEquiv x hx) ((CategoryTheory.ConcreteCategory.hom ((skyscraperResidueField x).presheaf.map i.op)) s) = (skyscraperResidueFieldEquiv x ⋯) s

The identifications of the sections of κ(x)ₓ with κ(x) commute with restriction.

theorem AlgebraicGeometry.Scheme.subsingleton_skyscraperResidueField {X : Scheme} (x : ↥X) {U : X.Opens} (hx : x ∉ U) : Subsingleton ↑((skyscraperResidueField x).presheaf.obj (Opposite.op U))

The skyscraper sheaf κ(x)ₓ has no nonzero sections over an open subset not containing x.

theorem AlgebraicGeometry.Scheme.skyscraperResidueField_map_bijective {X : Scheme} (x : ↥X) {U V : X.Opens} (i : U ⟶ V) (hx : x ∈ U) : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((skyscraperResidueField x).presheaf.map i.op))

The restriction maps of κ(x)ₓ between open subsets containing x are bijective.

instance AlgebraicGeometry.Scheme.isFlasque_skyscraperResidueField {X : Scheme} (x : ↥X) : (skyscraperResidueField x).presheaf.IsFlasque

The skyscraper sheaf κ(x)ₓ is flasque: its restriction maps are bijective between open subsets containing x, and land in the zero group otherwise.