44 Picard Schemes of Curves

Chapter 44 of the Stacks Project, Picard Schemes of Curves, Tag 0B92: the 6 sections of its 7 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 29 tags are carried by 80 declarations of the repository (all in StacksFrontier) and 2 registered declarations.

Section44.2 Hilbert scheme of points #

Section 44.2 of the Stacks Project, Tag 0B94. 8 tags here are carried by 29 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B94, the section

Tag 0B94 in the Stacks Project.

Stacks.Hilbert.hilbertSubobjects, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorClosedSubschemes.lean, line 72. The attribute's comment: “the set Hilb^d_{X/S}(T) of closed subschemes Z ⊂ X_T (closed immersions into X_T up to isomorphism over X_T) with Z → T finite locally free of degree d”.

The set Hilb^d_{X/S}(T) of closed subschemes Z ⊂ X_T, that is subobjects of X_T = X ×_S T presented by a closed immersion, such that Z → T is finite locally free of degree d.

def hilbertSubobjects (X T : Over S) (d : ℕ) :
    Set (Subobject ((Over.pullback T.hom).obj X).left)

Stacks.Hilbert.hilbertFamilyEquivHilbertSubobjects, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorClosedSubschemes.lean, line 121. The attribute's comment: “the values of Stacks.Hilbert.hilbertFunctorOfRank are the sets Hilb^d_{X/S}(T) of closed subschemes of the section: a bijection with Stacks.Hilbert.hilbertSubobjects”.

The degree-d Hilbert families in X over T, which record a closed subscheme of X_T by its ideal sheaf, are in bijection with the set Hilb^d_{X/S}(T) of closed subschemes Z ⊂ X_T with Z → T finite locally free of degree d. A family is sent to the closed subscheme it cuts out, and a closed subscheme to its ideal sheaf.

def hilbertFamilyEquivHilbertSubobjects (X T : Over S) (d : ℕ) :
    HilbertFamily X T d ≃ hilbertSubobjects X T d

Stacks.Hilbert.pullback_mem_hilbertSubobjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorClosedSubschemes.lean, line 160. The attribute's comment: “for T' ⟶ T over S and Z ∈ Hilb^d_{X/S}(T), the base change Z_{T'} ⊂ X_{T'} lies in Hilb^d_{X/S}(T')”.

For a morphism T' ⟶ T of schemes over S and a Z ∈ Hilb^d_{X/S}(T), the base change Z_{T'} ⊂ X_{T'}, the pullback of Z along X_{T'} ⟶ X_T, is an element of Hilb^d_{X/S}(T').

theorem pullback_mem_hilbertSubobjects (X : Over S) {T' T : Over S} {d : ℕ} (g : T' ⟶ T)
    {Z : Subobject ((Over.pullback T.hom).obj X).left} (hZ : Z ∈ hilbertSubobjects X T d) :
    (Subobject.pullback (familyBaseChangeMap X g)).obj Z ∈ hilbertSubobjects X T' d

Stacks.Hilbert.hilbertFamilyEquivHilbertSubobjects_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorClosedSubschemes.lean, line 173. The attribute's comment: “the functor Hilb^d_{X/S} acts on morphisms T' ⟶ T by base change of the closed subscheme Z ⊂ X_T to Z_{T'} ⊂ X_{T'}”.

The functor Hilb^d_{X/S} : (Sch/S)ᵒᵖ ⥤ Sets acts on a morphism T' ⟶ T by base change of the closed subscheme: under the identification of its values with Hilb^d_{X/S}(T), the image of Z is the pullback of Z along X_{T'} ⟶ X_T.

theorem hilbertFamilyEquivHilbertSubobjects_map (X : Over S) (d : ℕ) {T' T : Over S}
    (g : T' ⟶ T) (Z : (hilbertFunctorOfRank X d).obj (op T)) :
    (hilbertFamilyEquivHilbertSubobjects X T' d ((hilbertFunctorOfRank X d).map g.op Z) :
        Subobject _) =
      (Subobject.pullback (familyBaseChangeMap X g)).obj
        (hilbertFamilyEquivHilbertSubobjects X T d Z)

Stacks.Hilbert.hilbertScheme, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorClosedSubschemes.lean, line 191. The attribute's comment: “the notation \underline{Hilb}^d_{X/S} for the representing scheme”.

The scheme \underline{Hilb}^d_{X/S} over S representing the degree-d Hilbert functor, when that functor is representable by a scheme.

abbrev hilbertScheme (X : Over S) (d : ℕ) [(hilbertFunctorOfRank X d).IsRepresentable] :
    Over S

Stacks.Hilbert.baseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorFpqcSheaf.lean, line 156. The attribute's comment: “base change of families: that for a morphism T' ⟶ T over S and a Z in Hilb^d_{X/S}(T) the base change Z_{T'} ⊂ X_{T'} lies in Hilb^d_{X/S}(T'). This is the part of the section that requires an argument; the set Hilb^d_{X/S}(T) is Stacks.Hilbert.HilbertFamily and the functor is Stacks.Hilbert.hilbertFunctorOfRank”.

Stacks Project, Section 0B94. The base change of a degree-d Hilbert family along a morphism of S-schemes: the closed subscheme cut out by the pullback of its ideal sheaf.

This is the section's assertion that for a morphism T' ⟶ T over S and a Z ∈ Hilb^d_{X/S}(T) the base change Z_{T'} ⊂ X_{T'} is again an element of Hilb^d_{X/S}(T') — the type below says exactly that, and it is the one part of the section that requires an argument. That the resulting closed subscheme really is Z_{T'}, that is that its ideal sheaf is the pullback of Z's, is Stacks.Hilbert.baseChange_ideal. The set Hilb^d_{X/S}(T) is Stacks.Hilbert.HilbertFamily and the functor is Stacks.Hilbert.hilbertFunctorOfRank.

def baseChange {S : Scheme.{u}} (X : Over S) {T' T : Over S} {d : ℕ} (g : T' ⟶ T)
    (Z : HilbertFamily X T d) : HilbertFamily X T' d

Stacks.Hilbert.hilbertFunctorOfRank, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorFpqcSheaf.lean, line 211. The attribute's comment: “the functor Hilb^d_{X/S} : (Sch/S)ᵒᵖ ⥤ Sets itself, acting on morphisms by base change of families. Its values, the sets Hilb^d_{X/S}(T), are Stacks.Hilbert.HilbertFamily, which carries the other part of this section”.

Stacks Project, Section 0B94. The degree-d Hilbert functor of points of X over S. It sends an S-scheme T to the degree-d Hilbert families in X over T and a morphism to the base change of families.

This is the functor Hilb^d_{X/S} : (Sch/S)ᵒᵖ ⥤ Sets of the section, for an arbitrary morphism X ⟶ S of schemes and an arbitrary degree d. Its values are Stacks.Hilbert.HilbertFamily, which carries the other part of the section; that base change of a degree-d family is again one, which is what makes the assignment a functor, is Stacks.Hilbert.baseChange together with Stacks.Hilbert.baseChange_id and Stacks.Hilbert.baseChange_comp.

def hilbertFunctorOfRank {S : Scheme.{u}} (X : Over S) (d : ℕ) : (Over S)ᵒᵖ ⥤ Type u

Stacks.Hilbert.HilbertFamily, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorOfPoints.lean, line 94. The attribute's comment: “the set Hilb^d_{X/S}(T): the closed subschemes of X_T that are finite locally free of degree d over T. The functor these sets are the values of is Stacks.Hilbert.hilbertFunctorOfRank, which carries the other part of this section”.

Stacks Project, Section 0B94. A degree-d Hilbert family in X over T: an ideal sheaf on X ×_S T whose associated closed subscheme is finite locally free of rank d over T.

This is the value Hilb^d_{X/S}(T) of the degree-d Hilbert functor, which the section displays as the set of closed subschemes Z ⊂ X_T such that Z → T is finite locally free of degree d. The functor itself, with its action by base change, is Stacks.Hilbert.hilbertFunctorOfRank.

structure HilbertFamily {S : Scheme.{u}} (X T : Over S) (d : ℕ)

Tag 0B95, a lemma

Tag 0B95 in the Stacks Project.

Stacks.Hilbert.isSheaf_fpqcTopology_hilbertFunctorOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorFpqcGluing.lean, line 373.

Stacks Project, Tag 0B95. The degree-d Hilbert functor of points of X over S satisfies the sheaf property for the fpqc topology on the schemes over S.

theorem isSheaf_fpqcTopology_hilbertFunctorOfRank {S : Scheme.{u}} (X : Over S) (d : ℕ) :
    Presheaf.IsSheaf (Scheme.fpqcTopology.over S) (hilbertFunctorOfRank X d)

Stacks.Hilbert.isSeparated_fpqcTopology_hilbertFunctorOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorFpqcSheaf.lean, line 337. The attribute's comment: “the separatedness clause of the sheaf property”.

Stacks Project, Tag 0B95, separatedness. The degree-d Hilbert functor of points of X over S is separated for the fpqc topology on the schemes over S: a section has at most one amalgamation along any fpqc covering sieve.

theorem isSeparated_fpqcTopology_hilbertFunctorOfRank {S : Scheme.{u}} (X : Over S) (d : ℕ) :
    Presieve.IsSeparated (Scheme.fpqcTopology.over S) (hilbertFunctorOfRank X d)

Stacks.Hilbert.existsUnique_hilbertFamily_of_mem_fpqcPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorFpqcSheafProperty.lean, line 70. The attribute's comment: “the sheaf property in the shape of Tag 022G: unique amalgamation for an arbitrary fpqc covering family, with compatibility over the pairwise fibre products”.

Stacks Project, Tag 0B95, in the shape of the definition it refers to, Tag 022G. Let X be a scheme over S, let d be a natural number, and let {g i : Y i ⟶ T} be a family of morphisms of S-schemes whose underlying family of morphisms of schemes is an fpqc covering of T. Then a collection of degree-d Hilbert families Z i in X over Y i whose base changes to the fibre products Y i ×_T Y j agree is the collection of base changes of a unique degree-d Hilbert family in X over T.

theorem existsUnique_hilbertFamily_of_mem_fpqcPrecoverage {S : Scheme.{u}} (X : Over S) (d : ℕ)
    {T : Over S} {ι : Type*} {Y : ι → Over S} (g : ∀ i, Y i ⟶ T)
    (hcov : Presieve.ofArrows (fun i ↦ (Y i).left) (fun i ↦ (g i).left) ∈
      Scheme.fpqcPrecoverage T.left)
    (Z : ∀ i, HilbertFamily X (Y i) d)
    (hZ : ∀ i j, baseChange X (pullback.fst (g i) (g j)) (Z i) =
      baseChange X (pullback.snd (g i) (g j)) (Z j)) :
    ∃! V : HilbertFamily X T d, ∀ i, baseChange X (g i) V = Z i

Tag 0B96, a lemma

Tag 0B96 in the Stacks Project.

Stacks.Hilbert.isLimitPreserving_hilbertFunctorOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorLimitPreserving.lean, line 405.

Stacks Project, Tag 0B96. If X ⟶ S is of finite presentation, then the degree-d Hilbert functor of points of X over S is limit preserving: it turns every cofiltered inverse limit of affine S-schemes into a filtered colimit of sets.

theorem isLimitPreserving_hilbertFunctorOfRank (X : Over S) (d : ℕ)
    (hX : FinitePresentation X.hom) :
    Scheme.IsLimitPreserving S (hilbertFunctorOfRank X d)

Tag 0B97, a lemma

Tag 0B97 in the Stacks Project.

Stacks.Hilbert.exists_closedSubschemeRepresentingHilbertFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorClosedImmersion.lean, line 708. The attribute's comment: “if the degree-d Hilbert functor of Y is representable by a scheme, so is that of X, by a closed subscheme of it, compatibly with the universal families”.

Stacks Project, Tag 0B97. Let i : X ⟶ Y be a closed immersion of schemes over S. If the degree-d Hilbert functor of Y is represented by a scheme H_Y over S, then the degree-d Hilbert functor of X is represented by a scheme H_X over S together with a closed immersion H_X ⟶ H_Y over which the universal families correspond.

public theorem exists_closedSubschemeRepresentingHilbertFunctor {S : Scheme.{u}}
    {X Y : Over S} (i : X ⟶ Y) [IsClosedImmersion i.left] (d : ℕ)
    (H_Y : Over S) (hY : RepresentsHilbertFunctorOfRank Y H_Y d) :
    Nonempty (ClosedSubschemeRepresentingHilbertFunctor i d H_Y hY)

Tag 0B98, a lemma

Tag 0B98 in the Stacks Project.

Stacks.Hilbert.isSeparated_of_representsHilbertFunctorOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorSeparated.lean, line 330.

Stacks Project, Tag 0B98. Let X ⟶ S be separated and let d be a natural number. If the degree-d Hilbert functor of X is represented by a scheme H over S, then H ⟶ S is separated.

The separatedness of X ⟶ S which the source assumes is not used: Stacks.Hilbert.isSeparated_of_representsHilbertFunctorOfRank' is the same conclusion for an arbitrary X ⟶ S, and this is that statement specialised to the hypotheses of the source.

public theorem isSeparated_of_representsHilbertFunctorOfRank {S : Scheme.{u}}
    (X H : Over S) (d : ℕ) [IsSeparated X.hom]
    (hH : RepresentsHilbertFunctorOfRank X H d) :
    IsSeparated H.hom

Tag 0B99, a lemma

Tag 0B99 in the Stacks Project.

Stacks.Hilbert.exists_representsHilbertFunctorOfRank_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorAffineRepresentable.lean, line 133. The attribute's comment: “the reduction of the affine case to the case of an affine space, conditional on two inputs carried as hypotheses: Stacks 0B97, and representability for an affine space over an affine base. The latter is an instance of this very conclusion, since an affine space over an affine base is affine; what is proved here is therefore the source's reduction step, the closed immersion of an affine scheme into an affine space, and not the universal construction that makes the affine-space case true”.

Stacks 0B99, conditional on Stacks 0B97 and on the case of affine space, both carried as hypotheses. Let X ⟶ S be a morphism of affine schemes and let d be a natural number. Then the degree-d Hilbert functor of points of X over S is represented by a scheme over S.

Over an affine base, X is a closed subscheme of an affine space; its Hilbert functor is therefore represented by a closed subscheme of the Hilbert scheme of that affine space.

theorem exists_representsHilbertFunctorOfRank_of_isAffine {S : Scheme.{u}} [IsAffine S]
    (X : Over S) [IsAffine X.left] (d : ℕ) (h0B97 : ClosedImmersionRepresentability.{u})
    (hAffineSpace : AffineSpaceRepresentability.{u}) :
    Nonempty (Σ H : Over S, RepresentsHilbertFunctorOfRank X H d)

Stacks.Hilbert.exists_representsHilbertFunctorOfRank_of_isAffine_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorAffineRepresentableUnconditional.lean, line 57.

Let X ⟶ S be a morphism of affine schemes and let d be a natural number. Then the degree-d Hilbert functor of points of X over S is representable by a scheme over S.

theorem exists_representsHilbertFunctorOfRank_of_isAffine_of_isAffine {S : Scheme.{u}}
    [IsAffine S] (X : Over S) [IsAffine X.left] (d : ℕ) :
    Nonempty (Σ H : Over S, RepresentsHilbertFunctorOfRank X H d)

Tag 0B9A, a proposition

Tag 0B9A in the Stacks Project.

Stacks.Hilbert.exists_representsHilbertFunctorOfRank_of_affineFibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorAffineFibresRepresentable.lean, line 148. The attribute's comment: “for separated X ⟶ S. Separatedness is added to the source's statement, which is false without it: for the affine line with a doubled origin over the affine line and d = 1 the hypothesis holds but the Hilbert functor is not representable. Every case of Stacks 0B9B is separated”.

Stacks Project, Tag 0B9A. Let X ⟶ S be a separated morphism of schemes and let d be a natural number such that for every s ∈ S and all points x₁, …, x_d of the fibre X_s there is an affine open of X containing them. Then the degree-d Hilbert functor of X over S is representable by a scheme.

The subfunctors of families over bases mapping into an affine open V ⊆ S are open, cover the field-valued points, and are represented by the Hilbert scheme of X ×_S V over V, which exists by the affine case since the hypothesis passes to X ×_S V ⟶ V.

Separatedness of X ⟶ S is not in the source's statement, which is false without it. Let X be the affine line with a doubled origin over 𝔸¹ and d = 1; the hypothesis holds. Over each Spec k[t]/(t^n) the inclusion into one copy of 𝔸¹ is a point of the Hilbert functor, these are compatible, and compatible maps from all Spec k[t]/(t^n) to a scheme come from a map from Spec k[[t]]; but the only candidate section of X_{k[[t]]} ⟶ Spec k[[t]] has non-closed image, so the functor is not representable. The source's footnote, which proves F_U = Hilb^d_U without separatedness, uses an affine open containing d + 1 points of a fibre: the d points of Z_t and one more point of the closure of Z.

theorem exists_representsHilbertFunctorOfRank_of_affineFibres (X : Over S) [IsSeparated X.hom]
    (d : ℕ)
    (hX : ∀ (s : S) (x : Fin d → X.left), (∀ i, X.hom (x i) = s) →
      ∃ U : X.left.Opens, IsAffineOpen U ∧ ∀ i, x i ∈ U) :
    Nonempty (Σ H : Over S, RepresentsHilbertFunctorOfRank X H d)

Stacks.Hilbert.exists_representsHilbertFunctorOfRank_of_affineFibres_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorAffineFibresRepresentable.lean, line 174. The attribute's comment: “without separatedness, for X ⟶ S such that any d + 1 points of a fibre lie in an affine open: one point more than the source's hypothesis, which is what the footnote to the source's proof uses. With d points the source's statement is false, by the affine line with a doubled origin over the affine line and d = 1”.

Stacks Project, Tag 0B9A, in the form of the footnote to its proof. Let X ⟶ S be a morphism of schemes and let d be a natural number such that for every s ∈ S and all points x₀, …, x_d of the fibre X_s there is an affine open of X containing them. Then the degree-d Hilbert functor of X over S is representable by a scheme.

No separatedness is assumed; the price is one more point than in the source's hypothesis, which is what the source's footnote uses to show that a family in an open U ⊆ X is closed in X_T (Stacks.Hilbert.isClosed_range_of_affineFibres_succ). With d points instead of d + 1 the statement is false, by the affine line with a doubled origin over 𝔸¹ and d = 1, as recorded on Stacks.Hilbert.exists_representsHilbertFunctorOfRank_of_affineFibres.

theorem exists_representsHilbertFunctorOfRank_of_affineFibres_succ (X : Over S) (d : ℕ)
    (hX : ∀ (s : S) (x : Fin (d + 1) → X.left), (∀ i, X.hom (x i) = s) →
      ∃ U : X.left.Opens, IsAffineOpen U ∧ ∀ i, x i ∈ U) :
    Nonempty (Σ H : Over S, RepresentsHilbertFunctorOfRank X H d)

Stacks.Hilbert.nonempty_representsHilbertFunctorOfRank_of_exists_isAffineOpen_forall_mem_of_ne_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorRepresentableAmbient.lean, line 284. The attribute's comment: “the source's own hypothesis, an affine open around every d-tuple of points of one fibre, for every d ≠ 1; at d = 1 that hypothesis is vacuous and the tag's conclusion fails, refuted by Stacks.Hilbert.not_nonempty_representsHilbertFunctorOfRank_one”.

Stacks Project, Tag 0B9A, for every d ≠ 1. Let X ⟶ S be a morphism of schemes and let d ≥ 0 with d ≠ 1. Assume that for every s ∈ S and every tuple of points x₁, …, x_d of the fibre X_s there is an affine open U ⊆ X with x₁, …, x_d ∈ U. Then the degree-d Hilbert functor of points Hilb^d_{X/S} is representable by a scheme over S.

The hypothesis is the source's own, point for point, and the conclusion is the source's. The one value of d left out is the one at which the proposition is false: at d = 1 the d-tuple hypothesis holds for every morphism of schemes (Stacks.Hilbert.exists_isAffineOpen_forall_mem_of_le_one), while no scheme represents the degree-1 Hilbert functor of the affine line with the origin doubled over affine 1-space (Stacks.Hilbert.not_nonempty_representsHilbertFunctorOfRank_one).

For 2 ≤ d this is Stacks.Hilbert.nonempty_representsHilbertFunctorOfRank_of_exists_isAffineOpen_forall_mem_of_two_le; for d = 0 the base S itself represents Hilb^0_{X/S}, with no hypothesis needed (Stacks.Hilbert.representsHilbertFunctorOfRankZero).

theorem nonempty_representsHilbertFunctorOfRank_of_exists_isAffineOpen_forall_mem_of_ne_one
    (X : Over S) {d : ℕ} (hd : d ≠ 1)
    (hX : ∀ (s : S) (x : Fin d → X.left), (∀ i, X.hom.base (x i) = s) →
      ∃ U : X.left.Opens, IsAffineOpen U ∧ ∀ i, x i ∈ U) :
    Nonempty (Σ H : Over S, RepresentsHilbertFunctorOfRank X H d)

Stacks.Hilbert.HilbertFamily.baseChange_supportedIn_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorSupportedInOpen.lean, line 329. The attribute's comment: “condition (2)(b) of the gluing criterion used in the proof, in set-theoretic form: the subset of the base over which a degree-d Hilbert family is supported in a given open of the ambient scheme is open, and a base change lands in the subfunctor of families supported in that open exactly when the image of the base-change morphism is contained in that subset. Recasting this as representability of the inclusion by open immersions, which is the form the gluing criterion consumes, is not done here. Condition (2)(c) is proved separately in this file; conditions (1) and (2)(a) are not, and representability of the Hilbert functor is not asserted anywhere in this file. See the module docstring for what the proof of Tag 0B9A still needs”.

Stacks Project, Tag 0B9A, condition (2)(b) of the gluing criterion. A base change of a degree-d Hilbert family is supported in an open U ⊆ X exactly when the base change misses the non-support locus of the original family — a closed subset of T by Stacks.Hilbert.HilbertFamily.isClosed_notSupportedLocus.

theorem HilbertFamily.baseChange_supportedIn_iff {S : Scheme.{u}} {X : Over S} {T' T : Over S}
    {d : ℕ} (g : T' ⟶ T) (Z : HilbertFamily X T d) (U : X.left.Opens) :
    (baseChange X g Z).SupportedIn U ↔ ∀ t : T'.left, g.left t ∉ Z.notSupportedLocus U

Stacks.Hilbert.exists_isAffineOpen_supportedIn_of_specField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFunctorSupportedInOpen.lean, line 537. The attribute's comment: “condition (2)(c) of the gluing criterion used in the proof: the subfunctors of families supported in an affine open contain every field-valued point of the Hilbert functor. Conditions (1) and (2)(a), the reduction to an affine base of Stacks 01LG, and the criterion of Stacks 01JJ itself are not proved in this development, so representability is not asserted anywhere in this file”.

Stacks Project, Tag 0B9A, condition (2)(c) of the gluing criterion. Let X ⟶ S be a morphism of schemes and let d be a natural number such that any d points of X lying in a single fibre of X ⟶ S are contained in an affine open of X. Then every degree-d Hilbert family in X over the spectrum of a field is supported in an affine open of X.

The closed subscheme cut out by the family is finite locally free of rank d over the field, so it has at most d points; all of their images in X lie in one fibre, because the spectrum of a field has one point; so the hypothesis produces an affine open containing them all.

theorem exists_isAffineOpen_supportedIn_of_specField {S : Scheme.{u}} (X : Over S) (d : ℕ)
    (hX : ∀ (s : S) (x : Fin d → X.left), (∀ i, X.hom (x i) = s) →
      ∃ U : X.left.Opens, IsAffineOpen U ∧ ∀ i, x i ∈ U)
    (k : Type u) [Field k] (g : Spec (CommRingCat.of k) ⟶ S)
    (Z : HilbertFamily X (Over.mk g) d) :
    ∃ U : X.left.Opens, IsAffineOpen U ∧ Z.SupportedIn U

Tag 0B9B, a remark

Tag 0B9B in the Stacks Project.

Stacks.HilbertFibreAffineOpen.hasAffineFinitePointsInFibres_of_isQuasiAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HilbertFibreAffineOpen/Basic.lean, line 141. The attribute's comment: “case (1), the source is quasi-affine”.

If X is quasi-affine then every finite subset of a fibre of any f : X ⟶ S lies in an affine open of X.

theorem hasAffineFinitePointsInFibres_of_isQuasiAffine [Scheme.IsQuasiAffine X] (f : X ⟶ S) :
    HasAffineFinitePointsInFibres f

Stacks.HilbertFibreAffineOpen.hasAffineFinitePointsInFibres_of_isLocallyProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HilbertFibreAffineOpen/Basic.lean, line 149. The attribute's comment: “case (4), the morphism is locally projective”.

A locally projective morphism satisfies the fibrewise affineness condition.

theorem hasAffineFinitePointsInFibres_of_isLocallyProjective {f : X ⟶ S}
    (hf : IsLocallyProjective f) : HasAffineFinitePointsInFibres f

Stacks.HilbertFibreAffineOpen.hasAffineFinitePointsInFibres_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HilbertFibreAffineOpen/Basic.lean, line 160. The attribute's comment: “case (5), an ample invertible sheaf on the source”.

If X carries an ample invertible sheaf then every finite subset of a fibre of any f : X ⟶ S lies in an affine open of X.

theorem hasAffineFinitePointsInFibres_of_isAmple (f : X ⟶ S) (L : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L] (hL : Stacks.Ample.IsAmple X L) :
    HasAffineFinitePointsInFibres f

Stacks.HilbertFibreAffineOpen.hasAffineFinitePointsInFibres_of_modulesIsAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HilbertFibreAffineOpen/Basic.lean, line 170. The attribute's comment: “case (5), an ample invertible sheaf on the source, at Scheme.Modules.IsAmple”.

If X carries an invertible sheaf that is ample in the sense of AlgebraicGeometry.Scheme.Modules.IsAmple, then every finite subset of a fibre of any f : X ⟶ S lies in an affine open of X.

theorem hasAffineFinitePointsInFibres_of_modulesIsAmple (f : X ⟶ S) (L : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L]
    (hL : AlgebraicGeometry.Scheme.Modules.IsAmple X L) :
    HasAffineFinitePointsInFibres f

Stacks.HilbertFibreAffineOpen.hasAffineFinitePointsInFibres_of_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HilbertFibreAffineOpen/Basic.lean, line 182. The attribute's comment: “case (6), an f-ample invertible sheaf, at Stacks.RelativeAmple.IsRelativelyAmple”.

A morphism admitting a relatively ample invertible sheaf satisfies the fibrewise affineness condition.

theorem hasAffineFinitePointsInFibres_of_isRelativelyAmple {f : X ⟶ S} (L : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L]
    (hL : Stacks.RelativeAmple.IsRelativelyAmple f L) :
    HasAffineFinitePointsInFibres f

Stacks.HilbertFibreAffineOpen.hasAffineFinitePointsInFibres_of_modulesIsRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HilbertFibreAffineOpen/Basic.lean, line 195. The attribute's comment: “case (6), an f-ample invertible sheaf, at Stacks.RelativeAmple.IsRelativelyAmple”.

A morphism admitting a relatively ample sheaf L, invertible in the sense of AlgebraicGeometry.SheafOfModules.IsInvertible, satisfies the fibrewise affineness condition.

theorem hasAffineFinitePointsInFibres_of_modulesIsRelativelyAmple {f : X ⟶ S} (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
    (hL : Stacks.RelativeAmple.IsRelativelyAmple f L) :
    HasAffineFinitePointsInFibres f

Stacks.HilbertFibreAffineOpen.hasAffineFinitePointsInFibres_of_isRelativelyVeryAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HilbertFibreAffineOpen/Basic.lean, line 207. The attribute's comment: “case (7), an f-very ample invertible sheaf”.

A morphism admitting an invertible sheaf that is relatively very ample in the sense of Stacks.Tag01VMRelativeVeryAmple.IsRelativelyVeryAmple satisfies the fibrewise affineness condition.

theorem hasAffineFinitePointsInFibres_of_isRelativelyVeryAmple {f : X ⟶ S} (L : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L]
    (hL : Stacks.Tag01VMRelativeVeryAmple.IsRelativelyVeryAmple f L) :
    HasAffineFinitePointsInFibres f

Stacks.HilbertFibreAffineOpen.hasAffineFinitePointsInFibres_of_isRelativelyVeryAmpleTwistOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HilbertFibreAffineOpen/Basic.lean, line 220. The attribute's comment: “case (7), an f-very ample invertible sheaf, at the Tag 01VM predicate”.

A morphism admitting an invertible sheaf that is relatively very ample in the sense of Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple, with twist 𝒪_{𝐏(E)}(1), satisfies the fibrewise affineness condition.

theorem hasAffineFinitePointsInFibres_of_isRelativelyVeryAmpleTwistOne {f : X ⟶ S} (L : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L]
    (hL : Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple f L) :
    HasAffineFinitePointsInFibres f

Declarations registered for the tag:

AlgebraicGeometry.hasAffineFinitePointsInFibres_of_isQuasiAffineHom, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/HilbertFibreAffineOpen/Basic.lean, line 67 (StacksFrontier): “case (2), the morphism is quasi-affine”.
AlgebraicGeometry.hasAffineFinitePointsInFibres_of_isQuasiProjective, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/HilbertFibreAffineOpen/Basic.lean, line 69 (StacksFrontier): “case (3), the morphism is quasi-projective”.

Sources

LeanStacks.Hilbert.hilbertSubobjects · Stacks.Hilbert.hilbertFamilyEquivHilbertSubobjects · Stacks.Hilbert.pullback_mem_hilbertSubobjects · Stacks.Hilbert.hilbertFamilyEquivHilbertSubobjects_map · Stacks.Hilbert.hilbertScheme · Stacks.Hilbert.baseChange · Stacks.Hilbert.hilbertFunctorOfRank · Stacks.Hilbert.HilbertFamily

Section44.3 Moduli of divisors on smooth curves #

Section 44.3 of the Stacks Project, Tag 0B9C. 8 tags here are carried by 22 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B9C, the section

Tag 0B9C in the Stacks Project.

Stacks.Hilbert.HilbertFamily.isRelativeEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFamilyDivisor.lean, line 80. The attribute's comment: “the forward inclusion of the section's identification: a degree-d Hilbert family on a smooth relative curve is a relative effective Cartier divisor. The identification itself, as a natural isomorphism of functors, is Stacks.Hilbert.hilbertFunctorOfRankIsoRelativeEffectiveCartierDivisorFunctorOfRank”.

Stacks Project, Section 0B9C, forward inclusion. On a scheme smooth of relative dimension one over S, a degree-d Hilbert family in X over T is a relative effective Cartier divisor on X ×_S T over T.

Smoothness of relative dimension one is stable under base change, so X ×_S T ⟶ T is again smooth of relative dimension one; the family is finite locally free of degree d over T, hence finite locally free, and a finite locally free closed subscheme of a smooth relative curve is a relative effective Cartier divisor.

theorem HilbertFamily.isRelativeEffectiveCartierDivisor {S : Scheme.{u}} {X T : Over S}
    [SmoothOfRelativeDimension 1 X.hom] {d : ℕ} (Z : HilbertFamily X T d) :
    Stacks.Divisors.IsRelativeEffectiveCartierDivisor
      ((Over.pullback T.hom).obj X).hom Z.ideal

Stacks.Hilbert.hilbertFunctorOfRankIsoRelativeEffectiveCartierDivisorFunctorOfRank, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertFamilyDivisor.lean, line 187. The attribute's comment: “the section's assertion that Hilb^d_{X/S} parametrizes relative effective Cartier divisors, read as a natural isomorphism of functors on schemes over S between Hilb^d_{X/S} and the functor sending T to the relative effective Cartier divisors D ⊂ X_T over T which are finite locally free of degree d over T. This is the form in which the rest of the section uses it: 0B9E, 0B9F and the addition morphism on Hilb^d treat points of Hilb^d as divisors”.

Stacks Project, Section 0B9C. For X ⟶ S smooth of relative dimension one, the degree-d Hilbert functor Hilb^d_{X/S} is the functor of degree-d relative effective Cartier divisors: for every S-scheme T, the closed subschemes of X ×_S T finite locally free of degree d over T are exactly the relative effective Cartier divisors on X ×_S T over T which are finite locally free of degree d over T, compatibly with base change in T.

Both directions send an ideal sheaf to itself. A Hilbert family is a relative effective Cartier divisor by Stacks.Hilbert.HilbertFamily.isRelativeEffectiveCartierDivisor (Tag 0B9D, (1) implies (2), on X ×_S T ⟶ T), and a divisor of degree d is in particular a Hilbert family.

def hilbertFunctorOfRankIsoRelativeEffectiveCartierDivisorFunctorOfRank {S : Scheme.{u}}
    (X : Over S) [SmoothOfRelativeDimension 1 X.hom] (d : ℕ) :
    hilbertFunctorOfRank X d ≅ relativeEffectiveCartierDivisorFunctorOfRank X d

Tag 0B9D, a lemma

Tag 0B9D in the Stacks Project.

AlgebraicGeometry.isRelativeEffectiveCartierDivisor_iff_locallyQuasiFinite_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/DivisorsOnSmoothCurves.lean, line 288. The attribute's comment: “(2) iff (3)”.

Stacks Project, Tag 0B9D (2) iff (3). On a scheme smooth of relative dimension one over a base, the relative effective Cartier divisors are exactly the closed subschemes that are locally quasi-finite, flat and locally of finite presentation over the base.

Both directions are checked on the fibres, which are smooth curves over a field and hence regular of dimension one at every point. An effective Cartier divisor drops the local dimension, so its fibres are zero-dimensional, hence discrete, which is quasi-finiteness; conversely a discrete closed subscheme of a smooth curve meets each local ring, a discrete valuation ring, in a nonzero ideal, which is therefore generated by a nonzerodivisor.

theorem isRelativeEffectiveCartierDivisor_iff_locallyQuasiFinite_flat
    {X S : Scheme.{u}} (f : X ⟶ S) [SmoothOfRelativeDimension 1 f] (I : X.IdealSheafData) :
    IsRelativeEffectiveCartierDivisor f I ↔
      LocallyOfFiniteType (I.subschemeι ≫ f) ∧ LocallyQuasiFinite (I.subschemeι ≫ f) ∧
        Flat (I.subschemeι ≫ f) ∧ LocallyOfFinitePresentation (I.subschemeι ≫ f)

AlgebraicGeometry.isRelativeEffectiveCartierDivisor_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/DivisorsOnSmoothCurves.lean, line 301. The attribute's comment: “(1) implies (2)”.

Stacks Project, Tag 0B9D (1) implies (2). A closed subscheme of a scheme smooth of relative dimension one over a base that is finite locally free over the base is a relative effective Cartier divisor: a finite locally free morphism is finite, flat and locally of finite presentation, hence in particular locally quasi-finite.

theorem isRelativeEffectiveCartierDivisor_of_isFiniteLocallyFree {X S : Scheme.{u}} (f : X ⟶ S)
    [SmoothOfRelativeDimension 1 f] (I : X.IdealSheafData)
    [Stacks.Morphisms.IsFiniteLocallyFree (I.subschemeι ≫ f)] :
    IsRelativeEffectiveCartierDivisor f I

AlgebraicGeometry.locallyQuasiFinite_flat_of_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/DivisorsOnSmoothCurves.lean, line 316. The attribute's comment: “(3) implies (4)”.

Stacks Project, Tag 0B9D (3) implies (4). Dropping the local finite presentation conjunct from the third condition gives the fourth.

theorem locallyQuasiFinite_flat_of_locallyOfFinitePresentation {D S : Scheme.{u}} (g : D ⟶ S)
    (h : LocallyOfFiniteType g ∧ LocallyQuasiFinite g ∧ Flat g ∧
      LocallyOfFinitePresentation g) :
    LocallyOfFiniteType g ∧ LocallyQuasiFinite g ∧ Flat g

AlgebraicGeometry.isFiniteLocallyFree_iff_isRelativeEffectiveCartierDivisor_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/DivisorsOnSmoothCurves.lean, line 328. The attribute's comment: “(1) iff (2) when X over S is proper”. References: SGA 4 XVIII (1.5.10.3), “special case”.

Stacks Project, Tag 0B9D (1) iff (2) for a proper morphism. On a proper scheme smooth of relative dimension one over a base, the relative effective Cartier divisors are exactly the closed subschemes that are finite locally free over the base. Such a divisor is quasi-finite over the base, and proper since it is a closed subscheme of a proper scheme, hence finite; being also flat and locally of finite presentation it is finite locally free.

theorem isFiniteLocallyFree_iff_isRelativeEffectiveCartierDivisor_of_isProper {X S : Scheme.{u}}
    (f : X ⟶ S) [SmoothOfRelativeDimension 1 f] [IsProper f] (I : X.IdealSheafData) :
    Stacks.Morphisms.IsFiniteLocallyFree (I.subschemeι ≫ f) ↔
      IsRelativeEffectiveCartierDivisor f I

AlgebraicGeometry.locallyQuasiFinite_flat_locallyOfFinitePresentation_iff_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/SmoothCurveLocalDimension.lean, line 336. The attribute's comment: “(3) iff (4) when S is locally Noetherian”.

Stacks Project, Tag 0B9D (3) iff (4). Over a locally Noetherian base, a morphism locally of finite type is automatically locally of finite presentation, so the finite presentation conjunct may be dropped from the characterization of relative effective Cartier divisors.

theorem locallyQuasiFinite_flat_locallyOfFinitePresentation_iff_of_isLocallyNoetherian
    {D S : Scheme.{u}} (g : D ⟶ S) [IsLocallyNoetherian S] :
    (LocallyOfFiniteType g ∧ LocallyQuasiFinite g ∧ Flat g ∧
      LocallyOfFinitePresentation g) ↔
    (LocallyOfFiniteType g ∧ LocallyQuasiFinite g ∧ Flat g)

Tag 0B9E, a lemma

Tag 0B9E in the Stacks Project.

AlgebraicGeometry.isFiniteLocallyFreeOfRank_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/DivisorDegreeSum.lean, line 655.

Stacks Project, Tag 0B9E. Let f : X ⟶ S be smooth of relative dimension one and let I and J be quasi-coherent sheaves of ideals on X whose closed subschemes are finite locally free over S of degrees d₁ and d₂. The sum of the two divisors, cut out by the product I * J, is finite locally free over S of degree d₁ + d₂.

theorem isFiniteLocallyFreeOfRank_mul
    {X S : Scheme.{u}} (f : X ⟶ S) [SmoothOfRelativeDimension 1 f]
    (I J : X.IdealSheafData) (d₁ d₂ : ℕ)
    [Stacks.Morphisms.IsFiniteLocallyFreeOfRank (I.subschemeι ≫ f) d₁]
    [Stacks.Morphisms.IsFiniteLocallyFreeOfRank (J.subschemeι ≫ f) d₂] :
    Stacks.Morphisms.IsFiniteLocallyFreeOfRank ((I * J).subschemeι ≫ f) (d₁ + d₂)

Tag 0B9F, a lemma

Tag 0B9F in the Stacks Project.

AlgebraicGeometry.exists_isFiniteLocallyFreeOfRank_sub_mul_eq_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/DivisorDegreeDifference.lean, line 112.

Stacks Project, Tag 0B9F. Let f : X ⟶ S be smooth of relative dimension one and let D₁ and D₂ be quasi-coherent sheaves of ideals on X whose closed subschemes are finite locally free over S of degrees d₁ and d₂. If the closed subscheme of D₁ is contained in that of D₂, that is D₂ ≤ D₁, then there is a quasi-coherent sheaf of ideals D with D₂ = D₁ * D, the sum of the two divisors, whose closed subscheme is finite locally free over S of degree d₂ - d₁.

theorem exists_isFiniteLocallyFreeOfRank_sub_mul_eq_of_le
    {X S : Scheme.{u}} (f : X ⟶ S) [SmoothOfRelativeDimension 1 f]
    (D₁ D₂ : X.IdealSheafData) (d₁ d₂ : ℕ)
    [Stacks.Morphisms.IsFiniteLocallyFreeOfRank (D₁.subschemeι ≫ f) d₁]
    [Stacks.Morphisms.IsFiniteLocallyFreeOfRank (D₂.subschemeι ≫ f) d₂]
    (hle : D₂ ≤ D₁) :
    ∃ D : X.IdealSheafData, D₂ = D₁ * D ∧
      Stacks.Morphisms.IsFiniteLocallyFreeOfRank (D.subschemeι ≫ f) (d₂ - d₁)

Tag 0B9G, a lemma

Tag 0B9G in the Stacks Project.

Stacks.Hilbert.IsPointAddition.isFiniteLocallyFreeOfRank_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertPointAddition.lean, line 565.

Stacks Project, Tag 0B9G. Let X ⟶ S be smooth of relative dimension one and suppose the Hilbert functors Hilb^d_{X/S} are representable, say by H in degree d and by H' in degree d + 1. The point-addition morphism H ×_S X ⟶ H' is finite locally free of degree d + 1.

It factors as the incidence isomorphism H ×_S X ≅ D_univ onto the universal degree-(d+1) family followed by the structure morphism of D_univ, which is finite locally free of degree d + 1 because D_univ is a degree-(d+1) family. The incidence morphism is an isomorphism because it is bijective on points: surjectivity is the subtraction of a point from a family (Stacks Tag 0B9F) and injectivity is the cancellation of the graph of the point from the sum.

theorem isFiniteLocallyFreeOfRank_left (hf : IsPointAddition hH hH' f) :
    Stacks.Morphisms.IsFiniteLocallyFreeOfRank f.left (d + 1)

Tag 0B9H, a lemma

Tag 0B9H in the Stacks Project.

Stacks.Hilbert.smoothOfRelativeDimension_of_represents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertSchemeSmoothness.lean, line 425. The attribute's comment: “corrected statement: adds the hypothesis that X -> S is separated, which the printed statement omits and needs (the source uses it through Hilb^1 = X and Tag 0B9G; without it the statement is false, see Stacks.Hilbert.NonSeparated.not_smooth_hilbertScheme_doubledLine); representability is the tag's own hypothesis”.

Stacks Project, Tag 0B9H. Let X ⟶ S be a smooth morphism of schemes of relative dimension one such that the functors Hilb^d_{X/S} are representable, say by H d over S. Then the schemes H d are smooth over S of relative dimension d.

Representability is the tag's own hypothesis, carried here as the family hH. Separatedness of X ⟶ S is what makes the point-addition morphism of Tag 0B9G available, and by Stacks.Hilbert.isSeparated_of_isPointAddition_zero it is equivalent to the existence of that morphism in degree 0, so the induction cannot be started without it. The form of the result which takes those morphisms as data instead is Stacks.Hilbert.smoothOfRelativeDimension_of_isPointAddition.

Correction. The printed statement has no separatedness hypothesis and is false without one: Stacks.Hilbert.NonSeparated.not_smooth_hilbertScheme_doubledLine is a smooth non-separated relative curve all of whose Hilbert functors are representable, with no Hilb^d of positive degree smooth. Apart from [IsSeparated X.hom] the binders are exactly the tag's: X ⟶ S smooth of relative dimension one, and a representing scheme H d of Hilb^d_{X/S} for every d.

theorem smoothOfRelativeDimension_of_represents [IsSeparated X.hom] (H : ℕ → Over S)
    (hH : ∀ d : ℕ, RepresentsHilbertFunctorOfRank X (H d) d) (d : ℕ) :
    SmoothOfRelativeDimension d (H d).hom

Stacks.Hilbert.NonSeparated.not_forall_smoothOfRelativeDimension_of_represents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertSchemeSmoothnessCounterexample.lean, line 232. The attribute's comment: “the statement as printed is false: without separatedness of X → S it fails (this is the negation of the printed statement); the separated case is Stacks.Hilbert.smoothOfRelativeDimension_of_represents”.

Stacks Project, Tag 0B9H, as printed, is false. The statement "for a smooth morphism of schemes X ⟶ S of relative dimension 1 such that the functors Hilb^d_{X/S} are representable, the schemes Hilb^d_{X/S} are smooth over S of relative dimension d" fails without a separation hypothesis on X ⟶ S: for S = Spec ∏_{n ∈ ℕ} 𝔽₂ and X two copies of 𝔸¹_S glued along the inverse image of the dense open ⋃ₙ D(eₙ), every Hilb^d_{X/S} is representable and none with d ≥ 1 is smooth. The tag holds for a separated X ⟶ S: Stacks.Hilbert.smoothOfRelativeDimension_of_represents.

theorem not_forall_smoothOfRelativeDimension_of_represents :
    ¬ ∀ (S : Scheme.{u}) (X : Over S) [SmoothOfRelativeDimension 1 X.hom] (H : ℕ → Over S),
      (∀ d, RepresentsHilbertFunctorOfRank X (H d) d) →
        ∀ d, SmoothOfRelativeDimension d (H d).hom

Stacks.Hilbert.NonSeparated.not_smooth_hilbertScheme_doubledLine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertSchemeSmoothnessCounterexample.lean, line 288. The attribute's comment: “the statement as printed is false: this is an explicit counterexample, a smooth non-separated relative curve over Spec of a product of copies of F_2 with every Hilb^d representable and no Hilb^d with d >= 1 smooth. The source needs X -> S separated (it uses Hilb^1 = X and Tag 0B9G); the corrected statement is Stacks.Hilbert.smoothOfRelativeDimension_of_represents”.

Stacks Project, Tag 0B9H, as printed, is false: the concrete counterexample.

The tag reads: "Let X → S be a smooth morphism of schemes of relative dimension 1 such that the functors Hilb^d_{X/S} are representable. The schemes Hilb^d_{X/S} are smooth over S of relative dimension d." This theorem exhibits S, X and the failure, with every degree d ≥ 1 failing.

S = Spec A with A = ∏_{n ∈ ℕ} 𝔽₂ (the ring ULift ℕ → ZMod 2).

S' = ⋃ₙ D(eₙ) ⊆ S, where eₙ = Pi.single n 1 is the n-th coordinate idempotent; S' is a dense open whose complement V((eₙ)ₙ) is nonempty.

X = Stacks.Hilbert.DoubledLine.doubledLine S': two copies of 𝔸¹_S glued along 𝔸¹_{S'}, that is, the total space of Stacks.Examples.doubleSectionCover 𝔸¹_S 𝔸¹_{S'}, covered by two open charts 𝔸¹_S ⟶ X which agree exactly over S', with structure map to S given on each chart by the projection 𝔸¹_S ⟶ S.

The conclusion records, in this order: X ⟶ S is smooth of relative dimension 1 (the tag's hypothesis); X ⟶ S is not separated (the hypothesis the source uses implicitly, through Hilb^1_{X/S} = X and Tag 0B9G); for every d the functor Hilb^d_{X/S} is representable (the tag's other hypothesis); and for every d ≥ 1, every scheme representing Hilb^d_{X/S} fails to be smooth over S, so in particular is not smooth of relative dimension d.

The definitions the statement relies on:

Stacks.Hilbert.HilbertFamily X T d (Stacks Section 0B94, the value Hilb^d_{X/S}(T)): an ideal sheaf ideal on X ×_S T together with the proof that ideal.subschemeι ≫ (X ×_S T ⟶ T) is Stacks.Morphisms.IsFiniteLocallyFreeOfRank _ d, i.e. affine with direct image of the structure sheaf finite locally free of rank d (Stacks Tag 02KA). A closed subscheme is recorded by its ideal sheaf, so two families are equal iff their ideals are.

Stacks.Hilbert.RepresentsHilbertFunctorOfRank X H d (H represents Hilb^d_{X/S}): a bijection family : (T ⟶ H) ≃ HilbertFamily X T d for every S-scheme T, natural in T: (family (g ≫ f)).ideal = (family f).ideal.comap (X ×_S T' ⟶ X ×_S T), where comap is the ideal of the scheme-theoretic inverse image (Mathlib Scheme.IdealSheafData.comap), i.e. the base change of the closed subscheme.

AlgebraicGeometry.SmoothOfRelativeDimension, AlgebraicGeometry.Smooth, AlgebraicGeometry.IsSeparated: Mathlib's.

Why it fails: a family of positive degree splits any base T into the open and closed parts over S' and over S ∖ S', and over the latter T ⟶ S factors through Z = V((eₙ)ₙ); so Hilb^d_{X/S} ≅ 𝔸^d_{S'} ⊔ ∐_{a + b = d} (𝔸^a × 𝔸^b)_Z. The pieces over Z are open and map into S ∖ S', which has empty interior, whereas a smooth morphism is open.

The corrected statement, with X ⟶ S separated, is Stacks.Hilbert.smoothOfRelativeDimension_of_represents; the bare negation of the printed statement is Stacks.Hilbert.NonSeparated.not_forall_smoothOfRelativeDimension_of_represents.

theorem not_smooth_hilbertScheme_doubledLine :
    let S : Scheme.{u} := Spec (CommRingCat.of (ULift.{u} ℕ → ZMod 2))
    let S' : S.Opens :=
      ⨆ n : ULift.{u} ℕ, PrimeSpectrum.basicOpen (Pi.single n 1 : ULift.{u} ℕ → ZMod 2)
    let X : Over S := DoubledLine.doubledLine S'
    SmoothOfRelativeDimension 1 X.hom ∧ ¬ IsSeparated X.hom ∧
      (∀ d : ℕ, ∃ H : Over S, Nonempty (RepresentsHilbertFunctorOfRank X H d)) ∧
      ∀ d : ℕ, 0 < d → ∀ H : Over S, RepresentsHilbertFunctorOfRank X H d → ¬ Smooth H.hom

Tag 0B9I, a proposition

Tag 0B9I in the Stacks Project.

Stacks.Hilbert.smoothOfRelativeDimension_and_isProper_of_isCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertSchemeCurve.lean, line 134. The attribute's comment: “(1), ingredient: every representing scheme is smooth of relative dimension d and proper. The whole of (1), with representability, is Stacks.Hilbert.exists_representsHilbertFunctorOfRank_isVariety_of_isCurve”.

Stacks Project, Tag 0B9I, (1), smoothness and properness. Let X be a smooth proper curve over a field k. Every scheme representing the degree-d Hilbert functor of X is smooth of relative dimension d and proper over k.

Smoothness is Tag 0B9H; properness follows by induction on d from the point-addition morphisms H^d ×_k X ⟶ H^{d+1} of Tag 0B9G, which are finite locally free of degree d + 1, hence surjective, so that H^{d+1} is universally closed over k (Tag 03GN), and separated by Tag 0B98.

theorem smoothOfRelativeDimension_and_isProper_of_isCurve [IsProper f] [IsCurve k f] [Smooth f]
    (d : ℕ) (H : Over (Spec (.of k))) (hH : RepresentsHilbertFunctorOfRank (Over.mk f) H d) :
    SmoothOfRelativeDimension d H.hom ∧ IsProper H.hom

Stacks.Hilbert.isVariety_and_topologicalKrullDim_of_isCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertSchemeCurve.lean, line 189. The attribute's comment: “(1), ingredient: every representing scheme is a variety of dimension d. The whole of (1), with representability, is Stacks.Hilbert.exists_representsHilbertFunctorOfRank_isVariety_of_isCurve”.

Stacks Project, Tag 0B9I, (1), the varieties. Let X be a geometrically irreducible smooth proper curve over a field k. Every scheme representing the degree-d Hilbert functor of X is a variety of dimension d over k.

By induction on d: H^0 is a point, and H^{d+1} is the image of the irreducible scheme H^d ×_k X (Tag 038F) under the surjective point-addition morphism of Tag 0B9G; smooth and connected over a field it is integral, and its dimension is its relative dimension d.

theorem isVariety_and_topologicalKrullDim_of_isCurve [IsProper f] [IsCurve k f] [Smooth f]
    [GeometricallyIrreducible f] (d : ℕ) (H : Over (Spec (.of k)))
    (hH : RepresentsHilbertFunctorOfRank (Over.mk f) H d) :
    IsVariety k H.hom ∧ topologicalKrullDim H.left = d

Stacks.Hilbert.rationalPointsEquivEffectiveCartierDivisors, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertSchemeCurve.lean, line 232. The attribute's comment: “(2)”.

Stacks Project, Tag 0B9I, (2). Let X be a smooth proper curve over a field k and H a scheme representing the degree-d Hilbert functor of X. For a field extension k'/k, the k'-rational points of H correspond bijectively to the effective Cartier divisors of degree d on X_{k'}: the closed subschemes of X_{k'} which are effective Cartier divisors, finite locally free of rank d over k'.

The correspondence is representability; every degree-d family over k' is an effective Cartier divisor by Tag 0B9D.

def rationalPointsEquivEffectiveCartierDivisors [IsProper f] [IsCurve k f] [Smooth f] (d : ℕ)
    (H : Over (Spec (.of k))) (hH : RepresentsHilbertFunctorOfRank (Over.mk f) H d)
    (k' : Type u) [Field k'] [Algebra k k'] :
    (fieldExtOver k k' ⟶ H) ≃
      {I : ((Over.pullback (fieldExtOver k k').hom).obj (Over.mk f)).left.IdealSheafData //
        Stacks.Divisors.IsEffectiveCartierDivisor I ∧
          Stacks.Morphisms.IsFiniteLocallyFreeOfRank
            (I.subschemeι ≫ ((Over.pullback (fieldExtOver k k').hom).obj (Over.mk f)).hom) d}

Stacks.Hilbert.Curve.hilbertScheme_geometry, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertSchemeCurveGeometry.lean, line 125. The attribute's comment: “(1)”. References: SGA 4 XVII (6.3.8), “special case”.

Stacks Project, Tag 0B9I, part (1). Let X be a geometrically irreducible smooth proper curve over a field k and d ≥ 0. The degree-d Hilbert functor of points of X is representable, and every scheme representing it is a smooth proper variety of dimension d over k.

theorem hilbertScheme_geometry [IsCurve k f] [GeometricallyIrreducible f] [Smooth f] [IsProper f]
    (d : ℕ) :
    Nonempty (Σ H : Over (Spec (.of k)), RepresentsHilbertFunctorOfRank (Over.mk f) H d) ∧
    ∀ (H : Over (Spec (.of k))), RepresentsHilbertFunctorOfRank (Over.mk f) H d →
      Smooth H.hom ∧ IsProper H.hom ∧ IsVariety k H.hom ∧
        topologicalKrullDim H.left = (d : WithBot ℕ∞)

Stacks.Hilbert.Curve.rationalPointsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertSchemeCurveGeometry.lean, line 156. The attribute's comment: “(2)”.

Stacks Project, Tag 0B9I, part (2). Let X be a geometrically irreducible smooth proper curve over a field k, let H represent its degree-d Hilbert functor and let k'/k be a field extension. The k'-rational points of H are in bijection with the effective Cartier divisors of degree d on X_{k'}: the closed subschemes of X_{k'} which are effective Cartier divisors and finite locally free of degree d over k'.

def rationalPointsEquiv {k' : Type u} [Field k'] [Algebra k k'] [IsCurve k f]
    [GeometricallyIrreducible f] [Smooth f] [IsProper f] (d : ℕ) (H : Over (Spec (.of k)))
    (hH : RepresentsHilbertFunctorOfRank (Over.mk f) H d) :
    (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap k k'))) ⟶ H) ≃
    {I : ((Over.pullback (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap k k')))).hom).obj
          (Over.mk f)).left.IdealSheafData //
      Stacks.Divisors.IsEffectiveCartierDivisor I ∧
        Stacks.Morphisms.IsFiniteLocallyFreeOfRank (I.subschemeι ≫
          ((Over.pullback (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap k k')))).hom).obj
            (Over.mk f)).hom) d}

Stacks.Hilbert.exists_representsHilbertFunctorOfRank_isVariety_of_isCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertSchemeProperCurve.lean, line 70. The attribute's comment: “(1)”.

Stacks Project, Tag 0B9I (1). Let X be a geometrically irreducible smooth proper curve over a field k. For every d the degree-d Hilbert functor of X is representable by a smooth proper variety of dimension d over k.

theorem exists_representsHilbertFunctorOfRank_isVariety_of_isCurve [IsProper f] [IsCurve k f]
    [Smooth f] [GeometricallyIrreducible f] (d : ℕ) :
    ∃ (H : Over (Spec (.of k))) (_ : RepresentsHilbertFunctorOfRank (Over.mk f) H d),
      IsVariety k H.hom ∧ SmoothOfRelativeDimension d H.hom ∧ IsProper H.hom ∧
        topologicalKrullDim H.left = d

Stacks.Hilbert.isFiniteLocallyFreeOfRank_addDivisors_of_isCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertSchemeProperCurve.lean, line 84. The attribute's comment: “(3), for every choice of representing schemes; geometric irreducibility of X is not needed”.

Stacks Project, Tag 0B9I (3). Let X be a smooth proper curve over a field k, and let H₁, H₂ and H be any schemes representing the Hilbert functors of X of degrees d₁, d₂ and d₁ + d₂. The addition morphism H₁ ×_k H₂ ⟶ H, (D₁, D₂) ↦ D₁ + D₂, classifies the sum of the two families, and is finite locally free of degree (d₁ + d₂).choose d₁.

theorem isFiniteLocallyFreeOfRank_addDivisors_of_isCurve [IsProper f] [IsCurve k f] [Smooth f]
    {d₁ d₂ : ℕ} {H₁ H₂ H : Over (Spec (.of k))}
    (h₁ : RepresentsHilbertFunctorOfRank (Over.mk f) H₁ d₁)
    (h₂ : RepresentsHilbertFunctorOfRank (Over.mk f) H₂ d₂)
    (h : RepresentsHilbertFunctorOfRank (Over.mk f) H (d₁ + d₂)) :
    haveI : SmoothOfRelativeDimension 1 (Over.mk f).hom :=
      smoothOfRelativeDimension_one_of_isCurve k f
    (∀ {T : Over (Spec (.of k))} (g : T ⟶ H₁ ⨯ H₂),
        h.family (g ≫ addDivisors h₁ h₂ h) =
          (h₁.family (g ≫ prod.fst)).add (h₂.family (g ≫ prod.snd))) ∧
      Morphisms.IsFiniteLocallyFreeOfRank (addDivisors h₁ h₂ h).left ((d₁ + d₂).choose d₁)

Stacks.Hilbert.exists_hilbertSchemes_of_isCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertSchemeProperCurve.lean, line 111.

Stacks Project, Tag 0B9I. Let X be a geometrically irreducible smooth proper curve over a field k. There are schemes H d representing the Hilbert functors Hilb^d_{X/k} such that

each H d is a smooth proper variety of dimension d over k;

for every field extension k'/k, the k'-rational points of H d are in bijection with the effective Cartier divisors of degree d on X_{k'}, i.e. the closed subschemes of X_{k'} which are effective Cartier divisors finite locally free of rank d over k';

for d₁, d₂ ≥ 0 the addition morphism H d₁ ×_k H d₂ ⟶ H (d₁ + d₂), (D₁, D₂) ↦ D₁ + D₂, is finite locally free of degree (d₁ + d₂).choose d₁.

theorem exists_hilbertSchemes_of_isCurve [IsProper f] [IsCurve k f] [Smooth f]
    [GeometricallyIrreducible f] :
    haveI : SmoothOfRelativeDimension 1 (Over.mk f).hom :=
      smoothOfRelativeDimension_one_of_isCurve k f
    ∃ (H : ℕ → Over (Spec (.of k)))
      (hH : ∀ d, RepresentsHilbertFunctorOfRank (Over.mk f) (H d) d),
      (∀ d, IsVariety k (H d).hom ∧ SmoothOfRelativeDimension d (H d).hom ∧
          IsProper (H d).hom ∧ topologicalKrullDim (H d).left = d) ∧
      (∀ (d : ℕ) (k' : Type u) [Field k'] [Algebra k k'],
        Nonempty ((fieldExtOver k k' ⟶ H d) ≃
          {I : ((Over.pullback (fieldExtOver k k').hom).obj (Over.mk f)).left.IdealSheafData //
            Stacks.Divisors.IsEffectiveCartierDivisor I ∧
              Stacks.Morphisms.IsFiniteLocallyFreeOfRank
                (I.subschemeι ≫ ((Over.pullback (fieldExtOver k k').hom).obj (Over.mk f)).hom)
                d})) ∧
      (∀ d₁ d₂ : ℕ,
        (∀ {T : Over (Spec (.of k))} (g : T ⟶ H d₁ ⨯ H d₂),
          (hH (d₁ + d₂)).family (g ≫ addDivisors (hH d₁) (hH d₂) (hH (d₁ + d₂))) =
            ((hH d₁).family (g ≫ prod.fst)).add ((hH d₂).family (g ≫ prod.snd))) ∧
        Morphisms.IsFiniteLocallyFreeOfRank
          (addDivisors (hH d₁) (hH d₂) (hH (d₁ + d₂))).left ((d₁ + d₂).choose d₁))

Tag 0B9J, a remark

Tag 0B9J in the Stacks Project.

Stacks.Hilbert.isRelativeEffectiveCartierDivisor_univ_iso_prod_and_restrict_picardClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/HilbertSchemeCurve.lean, line 303.

Stacks Project, Tag 0B9J. Let X be a smooth proper curve over a field k, let d ≥ 0, and let H and H' be schemes representing the Hilbert functors Hilb^d_{X/k} and Hilb^{d+1}_{X/k} (they exist by Tag 0B9I). Write D_univ ⊆ X ×_k H' for the universal closed subscheme. Then

D_univ is a relative effective Cartier divisor over H' (Tag 0B9D);

D_univ is isomorphic as a scheme to H ×_k X, by an isomorphism under which the inclusion D_univ ⊆ X ×_k H' becomes (D, x) ↦ (x, D + x), the point and point addition Stacks.Hilbert.addPoint of Tag 0B9G (see the proof of Tag 0B9G);

in particular D_univ is an effective Cartier divisor on X ×_k H' and its sheaf 𝒪(D_univ) is invertible;

for a k-rational point [D] of H', classifying the effective Cartier divisor D of degree d + 1 on the fibre [D] × X = X ×_k k, the restriction of 𝒪(D_univ) to that fibre is 𝒪_X(D), as classes in the Picard group of the fibre.

The source assumes X geometrically irreducible, as in Tag 0B9I; that hypothesis is not used, and is dropped.

theorem isRelativeEffectiveCartierDivisor_univ_iso_prod_and_restrict_picardClass [IsProper f]
    [IsCurve k f] [Smooth f] (d : ℕ) (H H' : Over (Spec (.of k)))
    (hH : RepresentsHilbertFunctorOfRank (Over.mk f) H d)
    (hH' : RepresentsHilbertFunctorOfRank (Over.mk f) H' (d + 1)) :
    haveI : SmoothOfRelativeDimension 1 (Over.mk f).hom :=
      smoothOfRelativeDimension_one_of_isCurve k f
    haveI : IsSeparated (Over.mk f).hom := inferInstanceAs (IsSeparated f)
    Stacks.Divisors.IsRelativeEffectiveCartierDivisor ((Over.pullback H'.hom).obj (Over.mk f)).hom
        (hH'.family (𝟙 H')).ideal ∧
      (∃ e : (H ⨯ Over.mk f).left ≅ (hH'.family (𝟙 H')).ideal.subscheme,
        e.hom ≫ (hH'.family (𝟙 H')).ideal.subschemeι ≫ pullback.fst f H'.hom =
            (prod.snd : H ⨯ Over.mk f ⟶ Over.mk f).left ∧
          e.hom ≫ (hH'.family (𝟙 H')).ideal.subschemeι ≫ pullback.snd f H'.hom =
            (addPoint hH hH').left) ∧
      Stacks.Divisors.IsEffectiveCartierDivisor (hH'.family (𝟙 H')).ideal ∧
      AlgebraicGeometry.SheafOfModules.IsInvertible _
        (_root_.structureSheafRing
          ((Over.pullback H'.hom).obj (Over.mk f)).left.toRingedSpace).property
        (Stacks.Divisors.invertibleSheaf' (hH'.family (𝟙 H')).ideal) ∧
      ∀ x : Over.mk (𝟙 (Spec (.of k))) ⟶ H',
        Stacks.Picard.schemePullbackClass (familyBaseChangeMap (Over.mk f) x)
          (hH'.family (𝟙 H')).picardClass = (hH'.family x).picardClass

Sources

LeanStacks.Hilbert.HilbertFamily.isRelativeEffectiveCartierDivisor · Stacks.Hilbert.hilbertFunctorOfRankIsoRelativeEffectiveCartierDivisorFunctorOfRank · AlgebraicGeometry.isRelativeEffectiveCartierDivisor_iff_locallyQuasiFinite_flat · AlgebraicGeometry.isRelativeEffectiveCartierDivisor_of_isFiniteLocallyFree · AlgebraicGeometry.locallyQuasiFinite_flat_of_locallyOfFinitePresentation · AlgebraicGeometry.isFiniteLocallyFree_iff_isRelativeEffectiveCartierDivisor_of_isProper · AlgebraicGeometry.locallyQuasiFinite_flat_locallyOfFinitePresentation_iff_of_isLocallyNoetherian · AlgebraicGeometry.isFiniteLocallyFreeOfRank_mul

Section44.4 The Picard functor #

Section 44.4 of the Stacks Project, Tag 0B9K. 3 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B9L, a definition

Tag 0B9L in the Stacks Project.

Stacks.PicardFunctor.picardPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/PicardFunctor.lean, line 154. The attribute's comment: “the presheaf of Picard groups of the base changes”.

Stacks Project, Tag 0B9L. The presheaf T ↦ Pic(X_T) on the S-schemes of the site, whose fppf sheafification is the Picard functor. Its action on a morphism of test schemes is pullback of Picard classes.

def picardPresheaf : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (u + 1)

Stacks.PicardFunctor.picardFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/PicardFunctor.lean, line 176. The attribute's comment: “the Picard functor”. References: SGA 6 X (2.4), “definition of Pic_{X/S}”; SGA 6 XIII (3.1).

Stacks Project, Tag 0B9L. The Picard functor Pic_{X/S} : (Sch/S)_{fppf} ⥤ Sets of a morphism f : X ⟶ S of a big fppf site: the fppf sheafification of the presheaf T ↦ Pic(X_T) of isomorphism classes of invertible modules on the base changes of X.

def picardFunctor : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (u + 1)

Tag 0B9M, a lemma

Tag 0B9M in the Stacks Project.

Stacks.PicardFunctor.injective_schemePullbackClass_baseChangeProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/PicardSequenceLeftExactness.lean, line 155. The attribute's comment: “left exactness”.

Stacks Project, Tag 0B9M. If the comparison map 𝒪_T ⟶ f_{T,*}𝒪_{X_T} is an isomorphism for every S-scheme T of the site, then pullback along X_T ⟶ T is injective on Picard groups; this is exactness at Pic(T) of 0 ⟶ Pic(T) ⟶ Pic(X_T) ⟶ Pic_{X/S}(T).

theorem injective_schemePullbackClass_baseChangeProj
    (hO : ∀ T : BigFppfOver B S hS,
      IsIso (baseChangeProj B hX hS f T).toLRSHom.toHom.c)
    (T : BigFppfOver B S hS) :
    Function.Injective (Stacks.Picard.schemePullbackClass (baseChangeProj B hX hS f T))

Stacks.PicardFunctor.exact_schemePullbackClass_baseChangeProj_toPicardFunctorHom_of_isIso_c, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/PicardSequenceMiddleExactness.lean, line 627. The attribute's comment: “exactness at Pic(X_T)”.

If the comparison map 𝒪_T ⟶ f_{T,*}𝒪_{X_T} is an isomorphism for every S-scheme T of the site, then a Picard class of X_T dies in Pic_{X/S}(T) exactly when it is pulled back along the projection X_T ⟶ T; this is exactness at Pic(X_T) of 0 ⟶ Pic(T) ⟶ Pic(X_T) ⟶ Pic_{X/S}(T).

theorem exact_schemePullbackClass_baseChangeProj_toPicardFunctorHom_of_isIso_c
    (hOiso : ∀ U : BigFppfOver B S hS, IsIso (baseChangeProj B hX hS f U).toLRSHom.toHom.c)
    (T : BigFppfOver B S hS) :
    Function.Exact (Stacks.Picard.schemePullbackClass (baseChangeProj B hX hS f T))
      (toPicardFunctorHom B hX hS f T)

Tag 0B9N, a lemma

Tag 0B9N in the Stacks Project.

Stacks.PicardFunctor.schemePullbackClass_baseChangeSection_baseChangeProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/PicardSequenceSplitExact/SplittingExactness.lean, line 66. The attribute's comment: “the splitting”.

Stacks Project, Tag 0B9N. Pullback of Picard classes along the induced section σ_T : T ⟶ X_T is a left inverse of pullback along the projection X_T ⟶ T: the sequence 0 ⟶ Pic(T) ⟶ Pic(X_T) ⟶ Pic_{X/S}(T) ⟶ 0 is split by σ_T^*.

theorem schemePullbackClass_baseChangeSection_baseChangeProj (T : BigFppfOver B S hS) :
    Function.LeftInverse
      (Stacks.Picard.schemePullbackClass (baseChangeSection B hX hS f σ hσ T))
      (Stacks.Picard.schemePullbackClass (baseChangeProj B hX hS f T))

Stacks.PicardFunctor.injective_schemePullbackClass_baseChangeProj_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/PicardSequenceSplitExact/SplittingExactness.lean, line 79. The attribute's comment: “injectivity”.

Stacks Project, Tag 0B9N. Pullback of Picard classes along the projection X_T ⟶ T is injective, the induced section providing a left inverse; this is exactness at Pic(T) of 0 ⟶ Pic(T) ⟶ Pic(X_T) ⟶ Pic_{X/S}(T) ⟶ 0.

theorem injective_schemePullbackClass_baseChangeProj_of_section (T : BigFppfOver B S hS) :
    Function.Injective (Stacks.Picard.schemePullbackClass (baseChangeProj B hX hS f T))

Stacks.PicardFunctor.exact_schemePullbackClass_baseChangeProj_toPicardFunctorHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/PicardSequenceSplitExact/SplittingExactness.lean, line 591. The attribute's comment: “exactness in the middle”.

Stacks Project, Tag 0B9N. The image of pullback from Pic(T) is exactly the kernel of the map to the Picard functor: a Picard class of X_T dies in Pic_{X/S}(T) if and only if it is pulled back along the projection X_T ⟶ T. This is exactness in the middle of 0 ⟶ Pic(T) ⟶ Pic(X_T) ⟶ Pic_{X/S}(T) ⟶ 0.

theorem exact_schemePullbackClass_baseChangeProj_toPicardFunctorHom
    (hOiso : ∀ U : BigFppfOver B S hS,
      IsIso (baseChangeProj B hX hS f U).toLRSHom.toHom.c)
    (T : BigFppfOver B S hS) :
    Function.Exact (Stacks.Picard.schemePullbackClass (baseChangeProj B hX hS f T))
      (toPicardFunctorHom B hX hS f T)

Stacks.PicardFunctor.surjective_toPicardFunctorHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/PicardSequenceSplitExact/Surjectivity.lean, line 386. The attribute's comment: “surjectivity”.

Stacks Project, Tag 0B9N. Every section of the Picard functor over a test scheme T is the class of an invertible module on X_T: pullback Pic(X_T) ⟶ Pic_{X/S}(T) is surjective. This is exactness at Pic_{X/S}(T) of 0 ⟶ Pic(T) ⟶ Pic(X_T) ⟶ Pic_{X/S}(T) ⟶ 0.

A section is locally the class of an invertible module; normalising those local classes by the induced sections makes them agree on the overlaps of the covering family, so they form a quasi-coherent descent datum for the base-changed family, which is an fpqc covering of X_T. Effectivity of fpqc descent produces a module on X_T, invertible because its pullbacks are, and its class restricts to the given section on the covering family.

theorem surjective_toPicardFunctorHom
    (hOiso : ∀ U : BigFppfOver B S hS,
      IsIso (baseChangeProj B hX hS f U).toLRSHom.toHom.c)
    (T : BigFppfOver B S hS) :
    Function.Surjective (toPicardFunctorHom B hX hS f T)

Sources

LeanStacks.PicardFunctor.picardPresheaf · Stacks.PicardFunctor.picardFunctor · Stacks.PicardFunctor.injective_schemePullbackClass_baseChangeProj · Stacks.PicardFunctor.exact_schemePullbackClass_baseChangeProj_toPicardFunctorHom_of_isIso_c · Stacks.PicardFunctor.schemePullbackClass_baseChangeSection_baseChangeProj · Stacks.PicardFunctor.injective_schemePullbackClass_baseChangeProj_of_section · Stacks.PicardFunctor.exact_schemePullbackClass_baseChangeProj_toPicardFunctorHom · Stacks.PicardFunctor.surjective_toPicardFunctorHom

Section44.5 A representability criterion #

Section 44.5 of the Stacks Project, Tag 0B9P. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B9Q, a lemma

Tag 0B9Q in the Stacks Project.

AlgebraicGeometry.exists_grp_iso_of_representable_openSubfunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/Representability/GroupSchemeCriterion.lean, line 829.

A Zariski sheaf of groups with a representable open subfunctor meeting every field-valued point after translation by a rational point is a group scheme.

theorem exists_grp_iso_of_representable_openSubfunctor (k : Type u) [Field k]
    (G : (Over (Spec (.of k)))ᵒᵖ ⥤ GrpCat.{u})
    (hG : Presheaf.IsSheaf (Scheme.zariskiTopology.over (Spec (.of k)))
      (G ⋙ forget GrpCat))
    (F : Subfunctor (G ⋙ forget GrpCat))
    (hF : F.toFunctor.IsRepresentable)
    (hopen : (IsOpenImmersion.over (X := Spec (.of k))).presheaf F.ι)
    (hfield : ∀ (K : Type u) [Field K] [Algebra k K]
      (g : G.obj (op (fieldExtensionPoint k K))),
      ∃ g' : G.obj (op (Over.mk (𝟙 (Spec (.of k))))),
        (G.map (Over.homMk (fieldExtensionPoint k K).hom).op).hom g' * g ∈
          F.obj (op (fieldExtensionPoint k K))) :
    ∃ X : Grp (Over (Spec (.of k))), Nonempty (yonedaGrp.obj X ≅ G)

Sources

LeanAlgebraicGeometry.exists_grp_iso_of_representable_openSubfunctor

Section44.6 The Picard scheme of a curve #

Section 44.6 of the Stacks Project, Tag 0B9R. 7 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B9U, a lemma

Tag 0B9U in the Stacks Project.

AlgebraicGeometry.isIso_c_baseChange_of_isCurve_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/PicardSchemeCurve/PointedCurveStructureSheaf.lean, line 216.

Let k be a field and let X be a smooth projective curve over k with a k-rational point, given as a section σ of its structure morphism f. Then 𝒪_T ⟶ f_{T,*}𝒪_{X_T} is an isomorphism for every k-scheme T.

theorem isIso_c_baseChange_of_isCurve_of_section {k : Type u} [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsCurve k f] [IsProjectiveVariety k f] [Smooth f]
    (σ : Spec (.of k) ⟶ X) (hσ : σ ≫ f = 𝟙 _)
    {T : Scheme.{u}} (g : T ⟶ Spec (.of k)) :
    IsIso (pullback.snd f g).toLRSHom.toHom.c

Tag 0B9V, a lemma

Tag 0B9V in the Stacks Project.

Stacks.RigidifiedPicard.cohomologyLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/Jacobian/CohomologyLocus.lean, line 53. The attribute's comment: “F is a subfunctor, for f flat, proper and locally of finite presentation with a section (the source's smooth projective curve over a field with a rational point is a special case)”.

The rigidified classes ℒ ∈ Pic_{X/S,σ}(T) with Rf_{T,*}ℒ isomorphic to an invertible 𝒪_T-module placed in degree 0, as a subfunctor of Pic_{X/S,σ}.

def cohomologyLocus : Subfunctor (functor f σ hσ ⋙ forget GrpCat)

Stacks.RigidifiedPicard.isOpenSubfunctor_cohomologyLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/Jacobian/CohomologyLocus.lean, line 74. The attribute's comment: “the inclusion is representable by open immersions, for f flat, proper and locally of finite presentation with a section”.

The inclusion F ⊆ Pic_{X/S,σ} is representable by open immersions, in the elementwise form of [Stacks, Tag 01JI]: for every S-scheme T and every ℒ ∈ Pic_{X/S,σ}(T) there is an open U ⊆ T such that for every g : T' ⟶ T over S, the restriction of ℒ to T' lies in F(T') exactly when g maps T' into U.

theorem isOpenSubfunctor_cohomologyLocus : IsOpenSubfunctor (cohomologyLocus f σ hσ)

Tag 0B9W, a definition

Tag 0B9W in the Stacks Project.

AlgebraicGeometry.genus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusCurve/Basic.lean, line 59. The attribute's comment: “smooth projective geometrically irreducible curve over a field”.

The genus of a scheme X over a field k, namely dim_k H¹(X, 𝒪_X).

noncomputable def genus {k : Type u} [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) : ℕ

Tag 0B9X, a lemma

Tag 0B9X in the Stacks Project.

Stacks.RigidifiedPicard.exists_representableBy_cohomologyLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/Jacobian/PicardOfCurve.lean, line 282.

[Stacks, Tag 0B9X]. Let k be a field and X a smooth projective curve of genus g over k with a rational point σ. The open subfunctor F ⊆ Pic_{X/k,σ} of [Stacks, Tag 0B9V] is representable by an open subscheme of Hilb^g_{X/k}.

theorem exists_representableBy_cohomologyLocus (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsCurve k f] [Smooth f] (hproj : IsProjectiveMorphism f)
    (σ : Spec (.of k) ⟶ X) (hσ : σ ≫ f = 𝟙 _) :
    haveI : IsProper f := isProper_of_isProjectiveMorphism f hproj
    haveI : GeometricallyIrreducible f := geometricallyIrreducible_of_isCurve_of_section k f σ hσ
    haveI : SmoothOfRelativeDimension 1 f := smoothOfRelativeDimension_one_of_isCurve k f
    ∀ (H : Over (Spec (.of k)))
      (_ : Stacks.Hilbert.RepresentsHilbertFunctorOfRank (Over.mk f) H (genus f)),
      ∃ W : H.left.Opens, Nonempty ((cohomologyLocus f σ hσ).toFunctor.RepresentableBy
        (Over.mk (W.ι ≫ H.hom)))

Tag 0B9Y, a lemma

Tag 0B9Y in the Stacks Project.

AlgebraicGeometry.exists_invertible_baseChangeTwist_finrank_eq_one_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/BaseChangeTwistLowCohomology.lean, line 438. The attribute's comment: “for X_K given as any pullback square of X ⟶ Spec k along Spec K ⟶ Spec k, with L ⊗ L₀|_{X_K} the twist baseChangeTwist p L L₀ = L ⊗ p^*L₀”.

Stacks Project, Tag 0B9Y. Let k be a separably closed field, X a smooth projective curve over k, K/k a field extension and X' = X_K the base change, given as any pullback square with X ⟶ Spec k ⟵ Spec K. For every invertible sheaf L on X' there is an invertible sheaf L₀ on X with

dim_K H⁰(X', L ⊗ p^*L₀) = 1 and dim_K H¹(X', L ⊗ p^*L₀) = 0.

The proof is the source's: the start of the descending induction is AlgebraicGeometry.ampleTwistStart, its step is AlgebraicGeometry.pointIdealTwistStep, and the induction joining them is AlgebraicGeometry.exists_hasPrescribedLowCohomology_one, whose cohomology is Tag 0B8Z's step lemma. The genus g of the source occurs in neither the assertion nor the proof and is not a parameter. This form, for an arbitrary pullback square, is the one Stacks.PicardFunctor.TwistToNormalized quantifies over.

theorem exists_invertible_baseChangeTwist_finrank_eq_one_of_isSepClosed
    (k K : Type u) [Field k] [IsSepClosed k] [Field K] [Algebra k K]
    {X X' : Scheme.{u}} (f : X ⟶ Spec (.of k)) (f' : X' ⟶ Spec (.of K)) (p : X' ⟶ X)
    (hp : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap k K))))
    [IsCurve k f] [Smooth f] (hproj : IsProjective f)
    (L : X'.Modules) [Stacks.Ample.IsInvertibleModule X' L] :
    ∃ L₀ : X.Modules, Stacks.Ample.IsInvertibleModule X L₀ ∧
      Module.finrank K (cohomologyOverField K f' (baseChangeTwist p L L₀) 0) = 1 ∧
      Module.finrank K (cohomologyOverField K f' (baseChangeTwist p L L₀) 1) = 0

AlgebraicGeometry.exists_finrank_cohomologyOverField_add_schemePullbackClass_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PrescribedLowCohomologyFieldExtension.lean, line 501. The attribute's comment: “on Picard classes: the class c of the invertible sheaf L on X_K and the class c₀ of L₀ on X, with c + p^*c₀ the class of L ⊗ L₀|_{X_K}; H¹ = 0 is stated as vanishing, which gives dim_K H¹ = 0. Properness of X is used in place of projectivity”.

Let k be a separably closed field, X a smooth proper curve over k, K/k a field extension and p : X_K ⟶ X the projection of the base change. For every Picard class c on X_K (the class of an invertible 𝓛) there is a Picard class c₀ on X (the class of an invertible 𝓛₀) such that the class c + p^*c₀ (that of 𝓛 ⊗ 𝓛₀|_{X_K}) has

dim_K H⁰(X_K, c + p^*c₀) = 1 and H¹(X_K, c + p^*c₀) = 0.

theorem exists_finrank_cohomologyOverField_add_schemePullbackClass_eq_one
    [IsSepClosed k] [IsProper f] [IsCurve k f] [Smooth f] (c : Stacks.Picard.ofScheme 𝔛) :
    ∃ c₀ : Stacks.Picard.ofScheme X,
      Module.finrank K (cohomologyOverField K 𝔣
        (Stacks.Picard.picardRepresentative (𝔛).toRingedSpace
          (c + Stacks.Picard.schemePullbackClass 𝔭 c₀)).obj 0) = 1 ∧
      IsZero (cohomologyOverField K 𝔣
        (Stacks.Picard.picardRepresentative (𝔛).toRingedSpace
          (c + Stacks.Picard.schemePullbackClass 𝔭 c₀)).obj 1)

AlgebraicGeometry.exists_invertible_baseChangeTwist_finrank_cohomologyOverField_eq_one_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PrescribedLowCohomologyFieldExtension.lean, line 522. The attribute's comment: “the source's statement on sheaves, with L ⊗ L₀|_{X_K} the twist baseChangeTwist p L L₀ = L ⊗ p^*L₀; properness of X is used in place of projectivity”.

Let k be a separably closed field, X a smooth proper curve over k, K/k a field extension and p : X_K ⟶ X the projection of the base change. For every invertible 𝒪_{X_K}-module 𝓛 there is an invertible 𝒪_X-module 𝓛₀ with

dim_K H⁰(X_K, 𝓛 ⊗ p^*𝓛₀) = 1 and dim_K H¹(X_K, 𝓛 ⊗ p^*𝓛₀) = 0.

theorem exists_invertible_baseChangeTwist_finrank_cohomologyOverField_eq_one_of_isSepClosed
    [IsSepClosed k] [IsProper f] [IsCurve k f] [Smooth f]
    (L : (𝔛).Modules) [hL : Stacks.Ample.IsInvertibleModule 𝔛 L] :
    ∃ L₀ : X.Modules, Stacks.Ample.IsInvertibleModule X L₀ ∧
      Module.finrank K (cohomologyOverField K 𝔣 (baseChangeTwist 𝔭 L L₀) 0) = 1 ∧
      Module.finrank K (cohomologyOverField K 𝔣 (baseChangeTwist 𝔭 L L₀) 1) = 0

Tag 0B9Z, a proposition

Tag 0B9Z in the Stacks Project.

Stacks.PicardFunctor.isRepresentable_picardFunctor_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/CurvePicard/PicardCurveRepresentable.lean, line 53.

Stacks Project, Tag 0B9Z. Let k be a separably closed field and X a smooth projective curve over k. The Picard functor Pic_{X/k} is representable.

theorem isRepresentable_picardFunctor_of_isSepClosed [IsSepClosed k]
    [IsCurve k (B.inclusion.map f)] [Smooth (B.inclusion.map f)]
    [IsProjectiveVariety k (B.inclusion.map f)] :
    (picardFunctor B hX hk f).IsRepresentable

Stacks.RigidifiedPicard.isRepresentable_picardFunctor_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/Jacobian/PicardFunctorRepresentable.lean, line 211.

[Stacks, Tag 0B9Z]. Let k be a separably closed field and X a smooth projective curve over k. The Picard functor Pic_{X/k} is representable.

theorem isRepresentable_picardFunctor_of_isSepClosed (k : Type u) [Field k] [IsSepClosed k]
    (B : BigFppfSite.{u}) {X : Scheme.{u}} (hX : B.Contains X) (hk : B.Contains (Spec (.of k)))
    (f : B.obj hX ⟶ B.obj hk) [IsCurve k (B.inclusion.map f)] [Smooth (B.inclusion.map f)]
    (hproj : IsProjectiveMorphism (B.inclusion.map f)) :
    (Stacks.PicardFunctor.picardFunctor B hX hk f).IsRepresentable

Stacks.RigidifiedPicard.exists_grp_iso_functor_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/Jacobian/PicardOfCurve.lean, line 301. The attribute's comment: “as the rigidified functor Pic_{X/k,σ} at a rational point σ, which the source's proof identifies with Pic_{X/k}”.

[Stacks, Tag 0B9Z]. The Picard functor of a smooth projective curve X over a separably closed field k is representable: for a rational point σ, the rigidified Picard functor Pic_{X/k,σ} ≅ Pic_{X/k} is represented by a group scheme over k.

theorem exists_grp_iso_functor_of_isSepClosed (k : Type u) [Field k] [IsSepClosed k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsCurve k f] [Smooth f]
    (hproj : IsProjectiveMorphism f) :
    haveI : IsProper f := isProper_of_isProjectiveMorphism f hproj
    ∃ (σ : Spec (.of k) ⟶ X) (hσ : σ ≫ f = 𝟙 _) (P : Grp (Over (Spec (.of k)))),
      Nonempty (yonedaGrp.obj P ≅ functor f σ hσ)

Tag 0BA0, a lemma

Tag 0BA0 in the Stacks Project.

Stacks.AbelMap.picardScheme_clause_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/PicardSchemeCurve.lean, line 83. The attribute's comment: “(1)”.

Stacks Project, Tag 0BA0, clause (1).

theorem picardScheme_clause_one :
    haveI := geometricallyIrreducible_of_isSepClosed B hX hk f
    haveI := isProjectiveVariety_of_isProjective B hX hk f hproj
    haveI := isRepresentable_picardFunctor_of_isSepClosed B hX hk f
    Nonempty (IsColimit (Cofan.mk (picardScheme B hX hk f)
        fun d => (picardDegreeLocus B hX hk f (curveSection B hX hk f)
          (curveSection_comp B hX hk f) d).ι)) ∧
      ∀ d : ℤ, SmoothOfRelativeDimension (genus (B.inclusion.map f))
          (picardDegreeComponentHom B hX hk f (curveSection B hX hk f)
            (curveSection_comp B hX hk f) d) ∧
        IsProper (picardDegreeComponentHom B hX hk f (curveSection B hX hk f)
            (curveSection_comp B hX hk f) d) ∧
        IsVariety k (picardDegreeComponentHom B hX hk f (curveSection B hX hk f)
            (curveSection_comp B hX hk f) d) ∧
        topologicalKrullDim (B.inclusion.obj (picardSchemeDegreeComponent B hX hk f
            (curveSection B hX hk f) (curveSection_comp B hX hk f) d).left) =
          (genus (B.inclusion.map f) : WithBot ℕ∞)

Stacks.AbelMap.picardScheme_clause_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/PicardSchemeCurve.lean, line 105. The attribute's comment: “(2)”.

Stacks Project, Tag 0BA0, clause (2).

theorem picardScheme_clause_two (d : ℤ) :
    haveI := geometricallyIrreducible_of_isSepClosed B hX hk f
    haveI := isProjectiveVariety_of_isProjective B hX hk f hproj
    haveI := isRepresentable_picardFunctor_of_isSepClosed B hX hk f
    Nonempty ((baseOver B hk ⟶ picardSchemeDegreeComponent B hX hk f (curveSection B hX hk f)
        (curveSection_comp B hX hk f) d) ≃
      {x : Stacks.Picard.ofScheme X //
        @invertibleCurveDegree k _ X (B.inclusion.map f) _
          (IsCurve.topologicalKrullDim_eq_one (k := k) (f := B.inclusion.map f)).le (rep x)
          (Stacks.Picard.picardRepresentative X.toRingedSpace x).property = d})

Stacks.AbelMap.picardScheme_clause_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/PicardSchemeCurve.lean, line 120. The attribute's comment: “(3)”.

Stacks Project, Tag 0BA0, clause (3).

theorem picardScheme_clause_three :
    haveI := geometricallyIrreducible_of_isSepClosed B hX hk f
    haveI := isProjectiveVariety_of_isProjective B hX hk f hproj
    haveI := isRepresentable_picardFunctor_of_isSepClosed B hX hk f
    ∃ H : AlgebraicGeometry.OpenSubgroupScheme (picardGrp B hX hk f),
      IsClosedImmersion H.ι.hom.hom.left ∧
        Set.range H.ι.hom.hom.left.base = (picardDegreeLocus B hX hk f (curveSection B hX hk f)
          (curveSection_comp B hX hk f) 0 : Set (picardScheme B hX hk f))

Stacks.AbelMap.picardScheme_clauses_four_five_six, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/PicardSchemeCurve.lean, line 154. The attribute's comment: “(4), (5) and (6)”.

Stacks Project, Tag 0BA0, clauses (4), (5) and (6). For every d ≥ 0 the degree-d Hilbert scheme Hilb^d_{X/k} exists in the site ([Stacks, Tag 0B9I]), and for every scheme H representing it there is a unique morphism γ_d : H ⟶ Pic^d_{X/k} classifying the invertible module 𝒪(D_univ) of the universal divisor (clause (4)); it is surjective for d ≥ g and smooth for d ≥ 2g - 1 (clause (5)), and birational for d = g (clause (6)).

theorem picardScheme_clauses_four_five_six (d : ℕ) :
    haveI := geometricallyIrreducible_of_isSepClosed B hX hk f
    haveI := isProjectiveVariety_of_isProjective B hX hk f hproj
    haveI := isRepresentable_picardFunctor_of_isSepClosed B hX hk f
    (∃ H : BigFppfOver B (Spec (.of k)) hk,
      Nonempty (Stacks.Hilbert.RepresentsHilbertFunctorOfRank (Over.mk (B.inclusion.map f))
        (Over.mk (B.inclusion.map H.hom)) d)) ∧
    ∀ (H : BigFppfOver B (Spec (.of k)) hk)
      (hH : Stacks.Hilbert.RepresentsHilbertFunctorOfRank (Over.mk (B.inclusion.map f))
        (Over.mk (B.inclusion.map H.hom)) d),
    ∃! γ : H ⟶ picardSchemeDegreeComponent B hX hk f (curveSection B hX hk f)
        (curveSection_comp B hX hk f) d,
      (∀ {T : BigFppfOver B (Spec (.of k)) hk} (t : T ⟶ H),
        picardHomEquiv B hX hk f (t ≫ γ ≫ picardSchemeDegreeComponentι B hX hk f
            (curveSection B hX hk f) (curveSection_comp B hX hk f) d) =
          (toPicardFunctor B hX hk f).app (op T) (hH.family (testMap B hk t)).picardClass) ∧
      (genus (B.inclusion.map f) ≤ d → Surjective (B.inclusion.map γ.left)) ∧
      (2 * (genus (B.inclusion.map f) : ℤ) - 1 ≤ d →
        AlgebraicGeometry.Smooth (B.inclusion.map γ.left)) ∧
      (d = genus (B.inclusion.map f) → IsBirational (B.inclusion.map γ.left))

Stacks.RigidifiedPicard.exists_picardScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardScheme/Jacobian/PicardOfCurveRegistered.lean, line 37.

[Stacks, Tag 0BA0]. Let k be a separably closed field and X a smooth projective curve of genus g over k. Choosing a rational point σ, the Picard functor is represented by a group scheme P (Pic_{X/k} ≅ Pic_{X/k,σ}, [Stacks, Tag 0B9Z]), and: 1. P is the disjoint union of the open and closed P^d, g-dimensional smooth proper varieties; 2. the k-points of P^d are the invertible 𝒪_X-modules of degree d; 3. P^0 is an open and closed subgroup scheme; 4. for d ≥ 0 there is the canonical Abel morphism γ_d : Hilb^d_{X/k} ⟶ P^d, classifying the rigidified class of 𝒪(D_univ); 5. γ_d is surjective for d ≥ g and smooth for d ≥ 2g - 1; 6. γ_g is birational.

theorem exists_picardScheme (k : Type u) [Field k] [IsSepClosed k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsCurve k f] [Smooth f] (hproj : IsProjectiveMorphism f) :
    haveI : IsProper f := isProper_of_isProjectiveMorphism f hproj
    haveI : GeometricallyIrreducible f := geometricallyIrreducible_of_isCurve_of_isSepClosed k f
    haveI : SmoothOfRelativeDimension 1 f := smoothOfRelativeDimension_one_of_isCurve k f
    ∃ (σ : Spec (.of k) ⟶ X) (hσ : σ ≫ f = 𝟙 _) (P : Grp (Over (Spec (.of k))))
      (e : yonedaGrp.obj P ≅ functor f σ hσ),
      -- (1)
      (∀ d d' : ℤ, d ≠ d' → Disjoint
        (degreeLocus f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e d : Set P.X.left)
        (degreeLocus f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e d')) ∧
      (⨆ d, degreeLocus f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e d = ⊤) ∧
      (∀ d : ℤ,
        IsClopen (degreeLocus f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e d :
          Set P.X.left) ∧
        IsProperVariety k
          ((degreeLocus f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e d).ι ≫
            P.X.hom) ∧
        SmoothOfRelativeDimension (genus f)
          ((degreeLocus f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e d).ι ≫
            P.X.hom) ∧
        topologicalKrullDim
          (degreeLocus f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e d) =
            (genus f : WithBot ℕ∞)) ∧
      -- (2)
      (∀ d : ℤ, Set.BijOn (pointClassOf f σ hσ P e)
        {r | Set.range r.left ⊆
          (degreeLocus f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e d :
            Set P.X.left)}
        {c | invertibleCurveDegreeHom k f (IsCurve.topologicalKrullDim_eq_one (k := k) (f := f)).le
          c = d}) ∧
      -- (3)
      (∃ K : OpenSubgroupScheme P, ∃ i : degreeLocusOver f
          (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e 0 ≅ K.carrier.X,
        degreeLocusι f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e 0 =
          i.hom ≫ K.ι.hom.hom) ∧
      ∀ (H : ℕ → Over (Spec (.of k)))
        (hH : ∀ d, Stacks.Hilbert.RepresentsHilbertFunctorOfRank (Over.mk f) (H d) d),
        -- (4)
        (∀ d : ℕ,
          abelMorphismDegree f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e
              (hH d) ≫
            (degreeLocus f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e d).ι =
              (abelMorphismFull f σ hσ (hH d) P e).left ∧
          ∀ {T : Over (Spec (.of k))} (m : T ⟶ H d),
            (e.hom.app (op T)).hom (m ≫ abelMorphismFull f σ hσ (hH d) P e) =
              abelElementFull f σ hσ (hH d) m) ∧
        -- (5), surjectivity
        (∀ d : ℕ, genus f ≤ d → Surjective
          (abelMorphismDegree f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e
            (hH d))) ∧
        -- (5), smoothness
        (∀ d : ℕ, 2 * (genus f : ℤ) - 1 ≤ d → Smooth
          (abelMorphismDegree f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ P e
            (hH d))) ∧
        -- (6)
        IsBirational (abelMorphismDegree f (topologicalKrullDim_fiber_le_one_of_isCurve k f) σ hσ
          P e (hH (genus f)))

Sources

LeanAlgebraicGeometry.isIso_c_baseChange_of_isCurve_of_section · Stacks.RigidifiedPicard.cohomologyLocus · Stacks.RigidifiedPicard.isOpenSubfunctor_cohomologyLocus · AlgebraicGeometry.genus · Stacks.RigidifiedPicard.exists_representableBy_cohomologyLocus · AlgebraicGeometry.exists_invertible_baseChangeTwist_finrank_eq_one_of_isSepClosed · AlgebraicGeometry.exists_finrank_cohomologyOverField_add_schemePullbackClass_eq_one · AlgebraicGeometry.exists_invertible_baseChangeTwist_finrank_cohomologyOverField_eq_one_of_isSepClosed

Section44.7 Some remarks on Picard groups #

Section 44.7 of the Stacks Project, Tag 0CDS. 2 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CDT, a lemma

Tag 0CDT in the Stacks Project.

Stacks.Picard.continuousSMul_galoisPicardAction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/GaloisDescent/FiniteStageContinuity.lean, line 274. The attribute's comment: “continuity of the action of Gal(k'/k) on Pic(X_{k'}), proved from Tag 0B8W (2) through exists_finiteSubextension_schemePullbackClass_eq”.

The continuity clause of Stacks Tag 0CDT. Let k be a field, let X be a quasi-compact, quasi-separated scheme over k, and let K/k be a Galois extension. The action of Gal(K/k) on Pic(X_K) by pullback along the twists id_X × Spec(σ) is continuous for the Krull topology on the Galois group and the discrete topology on the Picard group: every class descends to a finite subextension E (Tag 0B8W (2)), hence is fixed by the open subgroup Gal(K/E).

theorem continuousSMul_galoisPicardAction (X : Over (Spec (.of k)))
    [CompactSpace X.left] [QuasiSeparatedSpace X.left]
    [TopologicalSpace (ofScheme (SchemeOver.baseChange k K X))]
    [DiscreteTopology (ofScheme (SchemeOver.baseChange k K X))] :
    letI := galoisPicardAction k K X
    ContinuousSMul (K ≃ₐ[k] K) (ofScheme (SchemeOver.baseChange k K X))

Stacks.Picard.injective_schemePullbackClass_of_globalSectionsIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/GaloisDescent/Injectivity.lean, line 68. The attribute's comment: “injectivity of Pic(X) → Pic(X_{k'}), proved from Tag 0CC5; the full identification is bijOn_schemePullbackClass_galoisFixedClasses”.

The injectivity half of Stacks Tag 0CDT. Let X be a quasi-compact, quasi-separated scheme over a field k with H⁰(X, 𝒪_X) = k, and let k'/k be a field extension. Then the pullback map Pic(X) → Pic(X_{k'}) is injective: H⁰(X, 𝒪_X) is then a field, hence semi-local, and Tag 0CC5 applies.

theorem injective_schemePullbackClass_of_globalSectionsIso {k k' : Type u} [Field k] [Field k']
    (φ : k →+* k') {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [CompactSpace X] [QuasiSeparatedSpace X]
    (hf : IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop)) :
    Function.Injective (schemePullbackClass (pullback.fst f (Spec.map (CommRingCat.ofHom φ))))

Stacks.Picard.bijOn_schemePullbackClass_galoisFixedClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/GaloisDescent/PicardGaloisInvariants.lean, line 178. The attribute's comment: “the identification Pic(X) = Pic(X_{k'})^{Gal(k'/k)}. The continuity clause of the tag is Stacks.Picard.continuousSMul_galoisPicardAction”.

Stacks Project, Tag 0CDT. Let k be a field, let X be a quasi-compact, quasi-separated scheme over k with H⁰(X, 𝒪_X) = k admitting a k-rational point, and let k'/k be a Galois extension. Then pullback along X_{k'} ⟶ X is a bijection of Pic(X) onto the classes of Pic(X_{k'}) fixed by Gal(k'/k).

theorem bijOn_schemePullbackClass_galoisFixedClasses (k k' : Type u) [Field k] [Field k']
    [Algebra k k'] [IsGalois k k'] (X : Over (Spec (.of k)))
    [CompactSpace X.left] [QuasiSeparatedSpace X.left]
    (hΓ : IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop))
    (pt : Spec (.of k) ⟶ X.left) (hpt : pt ≫ X.hom = 𝟙 (Spec (.of k))) :
    Set.BijOn (schemePullbackClass (pullback.fst X.hom
        (Spec.map (CommRingCat.ofHom (algebraMap k k'))))) Set.univ
      (galoisFixedClasses k k' X)

Tag 0CD5, a lemma

Tag 0CD5 in the Stacks Project.

Stacks.Picard.bijOn_schemePullbackClass_zsmulTorsion_of_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/TorsionBaseChange.lean, line 125.

Stacks Project, Tag 0CD5. Let k be a field of characteristic p > 0, let X be a quasi-compact and quasi-separated scheme over k with H⁰(X, 𝒪_X) = k, and let n be an integer prime to p. Then for every purely inseparable extension k'/k, pullback along X_{k'} ⟶ X is a bijection Pic(X)[n] → Pic(X_{k'})[n].

Injectivity is Tag 0CC5. For surjectivity, a class of Pic(X_{k'})[n] is pulled back from a class of Pic(X_E) for a finite subextension E/k (Tag 0B8W), which is again n-torsion because pullback from X_E is injective (Tag 0CC5 at the stage), and the finite purely inseparable case is Stacks.Picard.bijOn_schemePullbackClass_zsmulTorsion_of_hasExponent, proved through the absolute Frobenius.

theorem bijOn_schemePullbackClass_zsmulTorsion_of_isPurelyInseparable
    {k k' : Type u} [Field k] [Field k'] [Algebra k k'] [IsPurelyInseparable k k']
    (p : ℕ) [CharP k p] (hp : 0 < p) {n : ℤ} (hn : n.natAbs.Coprime p)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [CompactSpace X] [QuasiSeparatedSpace X]
    (hΓ : IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop)) :
    Set.BijOn
      (schemePullbackClass (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k k')))))
      (zsmulTorsion (ofScheme X) n)
      (zsmulTorsion
        (ofScheme (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k k'))))) n)

Sources

LeanStacks.Picard.continuousSMul_galoisPicardAction · Stacks.Picard.injective_schemePullbackClass_of_globalSectionsIso · Stacks.Picard.bijOn_schemePullbackClass_galoisFixedClasses · Stacks.Picard.bijOn_schemePullbackClass_zsmulTorsion_of_isPurelyInseparable

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

44 Picard Schemes of Curves

Section44.2 Hilbert scheme of points#

Tag 0B94, the section

Tag 0B95, a lemma

Tag 0B96, a lemma

Tag 0B97, a lemma

Tag 0B98, a lemma

Tag 0B99, a lemma

Tag 0B9A, a proposition

Tag 0B9B, a remark

Sources

Section44.3 Moduli of divisors on smooth curves#

Tag 0B9C, the section

Tag 0B9D, a lemma

Tag 0B9E, a lemma

Tag 0B9F, a lemma

Tag 0B9G, a lemma

Tag 0B9H, a lemma

Tag 0B9I, a proposition

Tag 0B9J, a remark

Sources

Section44.4 The Picard functor#

Tag 0B9L, a definition

Tag 0B9M, a lemma

Tag 0B9N, a lemma

Sources

Section44.5 A representability criterion#

Tag 0B9Q, a lemma

Sources

Section44.6 The Picard scheme of a curve#

Tag 0B9U, a lemma

Tag 0B9V, a lemma

Tag 0B9W, a definition

Tag 0B9X, a lemma

Tag 0B9Y, a lemma

Tag 0B9Z, a proposition

Tag 0BA0, a lemma

Sources

Section44.7 Some remarks on Picard groups#

Tag 0CDT, a lemma

Tag 0CD5, a lemma

Sources

Section44.2 Hilbert scheme of points #

Section44.3 Moduli of divisors on smooth curves #

Section44.4 The Picard functor #

Section44.5 A representability criterion #

Section44.6 The Picard scheme of a curve #

Section44.7 Some remarks on Picard groups #