Documentation

TauCeti.AlgebraicGeometry.RationalPoint.IdealSheaf

The ideal sheaf of a rational point #

On an integral regular curve, the ideal sheaf of a closed field-valued point is canonically isomorphic to the divisor sheaf 𝒪_X(-x). The comparison identifies both inclusions into the sheaf of rational functions. It therefore connects points presented as closed immersions with points presented as Weil divisors, without choosing a local parameter.

For a rational point on a proper curve, the ideal line bundle has Euler-characteristic degree -1. Its dual is the degree-one line bundle used by the Abel map. The sheaf comparison needs only a closed immersion from a field spectrum and dimension at most one; the degree calculation additionally uses a section of the structure morphism and finite-dimensional H¹(X, 𝒪_X).

References #

source
noncomputable def AlgebraicGeometry.Scheme.Hom.kerSheafIsoNegPoint {k : Type u} [Field k] {X : Scheme} (s : Spec ↧k ⟶ X) [IsClosedImmersion s] [IsIntegral X] [IsLocallyNoetherian X] [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] {x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X} (hx : ↑x = s (IsLocalRing.closedPoint k)) (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) :
(ker s).sheaf ≅ TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sheaf (-TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint x)

The ideal sheaf of a closed field-valued point on a regular integral curve is 𝒪_X(-x). The comparison respects the embeddings into rational functions (kerSheafIsoNegPoint_hom_ι). The dimension bound is only needed to recover regular functions from rational sections.

Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.kerSheafIsoNegPoint_hom_ι {k : Type u} [Field k] {X : Scheme} (s : Spec ↧k ⟶ X) [IsClosedImmersion s] [IsIntegral X] [IsLocallyNoetherian X] [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] {x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X} (hx : ↑x = s (IsLocalRing.closedPoint k)) (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) :
    CategoryTheory.CategoryStruct.comp (kerSheafIsoNegPoint s hx hX).hom (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sheafι (-TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint x)) = CategoryTheory.CategoryStruct.comp (ker s).sheafι (TauCeti.AlgebraicGeometry.Scheme.toRationalFunctions X)

    The comparison from the ideal sheaf of a point to 𝒪_X(-x) sends a regular function to the same rational function.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.kerSheafIsoNegPoint_hom_ι_assoc {k : Type u} [Field k] {X : Scheme} (s : Spec ↧k ⟶ X) [IsClosedImmersion s] [IsIntegral X] [IsLocallyNoetherian X] [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] {x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X} (hx : ↑x = s (IsLocalRing.closedPoint k)) (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) {Z : X.Modules} (h : TauCeti.AlgebraicGeometry.Scheme.rationalFunctions X ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (kerSheafIsoNegPoint s hx hX).hom (CategoryTheory.CategoryStruct.comp (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sheafι (-TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint x)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (ker s).sheafι (TauCeti.AlgebraicGeometry.Scheme.toRationalFunctions X)) h

    The comparison from the ideal sheaf of a point to 𝒪_X(-x) sends a regular function to the same rational function.

    source
    theorem AlgebraicGeometry.Scheme.Hom.eulerDegree_ker {k : Type u} [Field k] {X : Scheme} (s : Spec ↧k ⟶ X) [IsClosedImmersion s] [IsIntegral X] [IsLocallyNoetherian X] [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] {x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X} (hx : ↑x = s (IsLocalRing.closedPoint k)) (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) [X.Over (Spec ↧k)] [IsProper (X ↘ Spec ↧k)] [FiniteDimensional k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X).obj 1)] (hs : CategoryTheory.CategoryStruct.comp s (X ↘ Spec ↧k) = CategoryTheory.CategoryStruct.id (Spec ↧k)) (hI : (ker s).IsEffectiveCartier) :
    TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerDegree k hI.toInvertibleSheaf = -1

    The ideal line bundle of a rational point on a proper regular integral curve has Euler-characteristic degree -1.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.eulerDegree_ker_of_smooth {k : Type u} [Field k] {X : Scheme} [X.Over (Spec ↧k)] [IsProper (X ↘ Spec ↧k)] [SmoothOfRelativeDimension 1 (X ↘ Spec ↧k)] [ConnectedSpace ↥X] (s : Spec ↧k ⟶ X) (hs : CategoryTheory.CategoryStruct.comp s (X ↘ Spec ↧k) = CategoryTheory.CategoryStruct.id (Spec ↧k)) :
    have hI := ⋯; TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerDegree k hI.toInvertibleSheaf = -1

    On a connected smooth proper curve, the ideal line bundle of a rational point has degree -1. The geometric hypotheses supply discrete valuation stalks and finite-dimensional cohomology, without a perfect-field assumption.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.eulerDegree_dual_ker_of_smooth {k : Type u} [Field k] {X : Scheme} [X.Over (Spec ↧k)] [IsProper (X ↘ Spec ↧k)] [SmoothOfRelativeDimension 1 (X ↘ Spec ↧k)] [ConnectedSpace ↥X] (s : Spec ↧k ⟶ X) (hs : CategoryTheory.CategoryStruct.comp s (X ↘ Spec ↧k) = CategoryTheory.CategoryStruct.id (Spec ↧k)) :
    have hI := ⋯; TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerDegree k hI.toInvertibleSheaf.dual = 1

    The dual of the ideal line bundle of a rational point has degree one on a connected smooth proper curve. This is the class 𝒪_X(x) used by the Abel map.