108 Moduli Stacks

Chapter 108 of the Stacks Project, Moduli Stacks, Tag 0DLT: the 9 sections of its 12 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 53 tags are carried by 122 declarations of the repository (all in StacksFrontier) and 1 registered declaration.

Section108.4 Properties of the stack of coherent sheaves#

Section 108.4 of the Stacks Project, Tag 0DLX. 10 tags here are carried by 27 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DLY, a lemma

Tag 0DLY in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation.coherentRelativeDiagonal_affine_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackDiagonalAffineFinitePresentation.lean, line 175.

The diagonal of Coh_{X/B} over B is affine and of finite presentation (Stacks 0DLY). The relative diagonal of the projection Coh_{X/B} ⟶ 𝒮_B is representable by algebraic spaces, and every algebraic space representing one of its base changes along a scheme-valued point over U is affine and of finite presentation over U: that base change is the isomorphism sheaf of two objects over one point of B (exists_isAlgebraicSpace_isomPresheaf_affineFinitePresentation).

theorem coherentRelativeDiagonal_affine_finitePresentation :
    ∃ _hrep : Stack.IsRepresentableByAlgebraicSpaces B S hS
        (Stack.relativeDiagonalBasedFunctor B S hS (coherentCFG D) (baseCFG D.Y)
          (coherentToBase D.categoryData)),
      ∀ (U : BigFppfOver B S hS)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤
          (Stack.twoFibreProduct B S hS (baseCFG D.Y) (coherentCFG D) (coherentCFG D)
            (coherentToBase D.categoryData) (coherentToBase D.categoryData)).val.obj)
        (_hy : y ⋙ (Stack.twoFibreProduct B S hS (baseCFG D.Y) (coherentCFG D) (coherentCFG D)
            (coherentToBase D.categoryData) (coherentToBase D.categoryData)).val.p =
          Over.map U.hom)
        (F : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hF : IsAlgebraicSpace B U.left.1 U.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) (coherentCFG D).val.p
            (Stack.twoFibreProduct B S hS (baseCFG D.Y) (coherentCFG D) (coherentCFG D)
              (coherentToBase D.categoryData) (coherentToBase D.categoryData)).val.p y
            (Stack.relativeDiagonalBasedFunctor B S hS (coherentCFG D) (baseCFG D.Y)
              (coherentToBase D.categoryData)).toFunctor)
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        IsAffineHom B S hS (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom ∧
          IsFinitePresentation B S hS (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom

Tag 0DLZ, a lemma

Tag 0DLZ in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation.isFiberedQuasiSeparated_and_isLocallyOfFinitePresentation_toBaseCFG, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackQuasiSeparatedFinitePresentation.lean, line 86. The attribute's comment: “quasi-separated as Stacks 04YW for a 1-morphism of categories fibred in groupoids; locally of finite presentation as Stacks 06Q2 (1) for the small models, Coh_{X/B} having its hom types one universe above the site”.

Let f : X ⟶ B be a morphism of algebraic spaces of finite presentation. Then the morphism Coh_{X/B} ⟶ B is quasi-separated and locally of finite presentation.

Quasi-separatedness is AlgebraicGeometry.Stack.IsFiberedQuasiSeparated, Stacks 04YW for a 1-morphism of categories fibred in groupoids; local finite presentation is part (1) of Stacks 06Q2 for the induced 1-morphism of small models (AlgebraicGeometry.Stack.smallHomsModelMap), the hom types of Coh_{X/B} lying one universe above those of the site. See the implementation notes of the file.

theorem isFiberedQuasiSeparated_and_isLocallyOfFinitePresentation_toBaseCFG
    (D : CoherentSituation B S hS) :
    Stack.IsFiberedQuasiSeparated.{u, u + 1, u + 1} B S hS D.toBaseCFG ∧
      letI := locallySmall_coherentCFG D
      letI := locallySmall_baseCFG D.Y
      Stack.HasPropertyOnEverySmoothDiagram B S hS
        (fun _ _ h => Space.IsLocallyOfFinitePresentation B S hS h)
        (Stack.smallHomsModelMap D.toBaseCFG)

Tag 0DM0, a lemma

Tag 0DM0 in the Stacks Project.

StacksDraft.CoherentGenericFibre.exists_submodule_finite_flat_isLocalizedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackValuativeChart.lean, line 246. The attribute's comment: “the affine-chart case: over a valuation ring a module of finite type on the chart of the generic fibre is the generic fibre of a module of finite type on the chart which is flat over the valuation ring, its flatness being Stacks 0539 and its generic fibre being identified by a localization; the base-change reduction of the first step, the gluing of the chart-wise extensions over Stacks 0829, the proper support, the finite presentation of Stacks 0DLR, and hence the statement for the 1-morphism Cohstack_{X/B} -> B in the sense of Stacks 0CLK are not covered”.

Stacks 0DM0, on an affine chart over a valuation ring. Let R be a valuation ring, A an R-algebra and A_K the localization of A at the nonzero elements of R, that is, the chart of the generic fibre. Let N be an A_K-module of finite type, the coherent module on the generic fibre. Then there is an A-submodule M of N which is of finite type over A, flat over R, and whose generic fibre is N, in that N is the localization of M at the nonzero elements of R.

This is the chart-wise content of the source's proof: M is generated over A by a finite A_K-generating family of N, it is flat over R because it is torsion free and R is a valuation ring (Stacks 0539), and its generic fibre is all of N because denominators can be cleared.

theorem exists_submodule_finite_flat_isLocalizedModule [IsDomain R] [ValuationRing R]
    [Module.Finite AK N] :
    ∃ M : Submodule A N, Module.Finite A M ∧ Module.Flat R M ∧
      IsLocalizedModule R⁰ (LinearMap.restrictScalars R M.subtype)

AlgebraicGeometry.Space.CoherentSituation.fiberedValuativeExistence_toBaseCFG, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackValuativeCriterion.lean, line 100.

Let f : X ⟶ B be a morphism of algebraic spaces which is proper and of finite presentation. Then Coh_{X/B} ⟶ B satisfies the existence part of the valuative criterion (Stacks 0CLK): every 2-commutative square with left edge Spec K ⟶ Spec R, for a valuation ring R with fraction field K, admits a dotted arrow after an extension K'/K and passage to a valuation ring R' ⊂ K' dominating R — here already with K' = K and R' = R.

The criterion is AlgebraicGeometry.Stack.FiberedValuativeExistence, the data of Stacks 0CLK for a 1-morphism of categories fibred in groupoids; it agrees with AlgebraicGeometry.Stack.ValuativeCriterion.Existence on 1-morphisms of algebraic stacks by AlgebraicGeometry.Stack.valuativeCriterionExistence_iff_fiberedValuativeExistence.

theorem CoherentSituation.fiberedValuativeExistence_toBaseCFG (D : CoherentSituation B S hS)
    (hp : IsProper B S hS D.f.hom) :
    Stack.FiberedValuativeExistence.{u, u + 1, u + 1} B S hS D.toBaseCFG

Tag 0DN9, a lemma

Tag 0DN9 in the Stacks Project.

AlgebraicGeometry.Space.CoherentPushforwardSituation.cohPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackPushforwardQuasiFinite.lean, line 301.

Let B be an algebraic space and let π : X ⟶ Y be a quasi-finite morphism of algebraic spaces which are separated and of finite presentation over B. Then π_* induces a morphism Coh_{X/B} ⟶ Coh_{Y/B}: the 1-morphism of categories over the big fppf site sending an object (T, ℱ) to (T, π_{T,*}ℱ) and a morphism (h, φ), with φ : X_h^*ℱ' ⟶ ℱ, to (h, θ_h ≫ π_{T,*}φ), where θ_h : Y_h^*π_{T',*}ℱ' ⟶ π_{T,*}X_h^*ℱ' is the base change map.

def cohPushforward :
    coherentBasedCategory D.source.categoryData ⥤ᵇ coherentBasedCategory D.target.categoryData

AlgebraicGeometry.Space.isFinite_of_comp_isProper_of_isSeparated_of_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackPushforwardReduction.lean, line 56. The attribute's comment: “the reduction of the proof to the finite case: a locally quasi-finite morphism whose source is proper and whose target is separated over the base is finite”.

Let π : X ⟶ Y and pY : Y ⟶ Z be morphisms of algebraic spaces over S. If the composite X ⟶ Z is proper, pY is separated and π is locally quasi-finite, then π is finite.

theorem isFinite_of_comp_isProper_of_isSeparated_of_isLocallyQuasiFinite
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (π : X ⟶ Y) (pY : Y ⟶ Z)
    (hXZ : IsProper B S hS (π ≫ pY)) (hpY : IsSeparated B S hS pY)
    (hπ : IsLocallyQuasiFinite B S hS π) :
    IsFinite B S hS π

AlgebraicGeometry.Space.isFinitePresentation_of_comp_isProper_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackPushforwardReduction.lean, line 69. The attribute's comment: “the finite presentation of π in the reduction to the finite case”.

Let π : X ⟶ Y and pY : Y ⟶ Z be morphisms of algebraic spaces over S. If the composite X ⟶ Z is locally of finite presentation and proper and pY is locally of finite type and separated, then π is of finite presentation.

theorem isFinitePresentation_of_comp_isProper_of_isSeparated
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (π : X ⟶ Y) (pY : Y ⟶ Z)
    (hXZfp : IsLocallyOfFinitePresentation B S hS (π ≫ pY))
    (hXZ : IsProper B S hS (π ≫ pY)) (hpYft : IsLocallyOfFiniteType B S hS pY)
    (hpY : IsSeparated B S hS pY) :
    IsFinitePresentation B S hS π

AlgebraicGeometry.Space.isFinite_comp_of_isLocallyQuasiFinite_of_comp_isProper_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackPushforwardReduction.lean, line 85. The attribute's comment: “the finiteness of the composite Z ⟶ X_T ⟶ Y_T in the first paragraph of the proof, the composite being locally quasi-finite”.

Let i : W ⟶ X, π : X ⟶ Y and pY : Y ⟶ Z be morphisms of algebraic spaces over S. If i and π are locally quasi-finite, the composite W ⟶ Z is proper and pY is separated, then i ≫ π is finite.

theorem isFinite_comp_of_isLocallyQuasiFinite_of_comp_isProper_of_isSeparated
    {W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hW : IsAlgebraicSpace B S hS W)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (i : W ⟶ X) (π : X ⟶ Y) (pY : Y ⟶ Z)
    (hi : IsLocallyQuasiFinite B S hS i) (hπ : IsLocallyQuasiFinite B S hS π)
    (hWZ : IsProper B S hS (i ≫ π ≫ pY)) (hpY : IsSeparated B S hS pY) :
    IsFinite B S hS (i ≫ π)

Tag 0DNA, a lemma

Tag 0DNA in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation.isOpenSubspace_supportFactorizationLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackOpenImmersion.lean, line 176. The attribute's comment: “an ingredient only: the open locus of the source's hint, namely the locus in T above which Supp(F) lands in X_T. The conclusion itself is not stated, the 1-morphism Coh_{X/B} ⟶ Coh_{Y/B} of 0DN9 not being constructed in this development”.

For an object (T, g, F) of Coh_{Y/B} the locus in T above which Supp(F) lands in the open subspace X_T ⊆ Y_T is an open subspace of T.

theorem isOpenSubspace_supportFactorizationLocus (hπ : π ≫ D.f = bX)
    (hopen : IsOpenImmersion B S hS π.hom) (obj : CoherentObject D)
    (hU : IsClosed (D.support obj.T obj.F)) :
    IsOpenSubspace B S hS (supportFactorizationLocus D hπ obj hU)

AlgebraicGeometry.Space.CoherentSituation.factorsThrough_supportFactorizationLocus_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackOpenImmersion.lean, line 190. The attribute's comment: “an ingredient only: the universal property of that locus, a test object factoring through it exactly when the base change of Supp(F) lands in X_T. The residues are the 1-morphism of 0DN9 and the algebraicity of Coh of 09DS”.

A morphism T' ⟶ T from an algebraic space factors through the locus exactly when the base change of Supp(F) to T' lands in X_T.

theorem factorsThrough_supportFactorizationLocus_iff (hπ : π ≫ D.f = bX)
    (hopen : IsOpenImmersion B S hS π.hom) (obj : CoherentObject D)
    (hU : IsClosed (D.support obj.T obj.F))
    {T' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hT' : IsAlgebraicSpace B S hS T')
    (g : T' ⟶ ((schemeSpaceFunctor B S hS).obj obj.T.left).1) :
    (∃ l : T' ⟶ (supportFactorizationLocus D hπ obj hU).toFunctor,
        l ≫ (supportFactorizationLocus D hπ obj hU).ι = g) ↔
      ∃ l : pullback ((supportSubspace D obj hU).ι ≫ (D.projection obj.T).hom) g ⟶
          (baseChangeSpace bX obj.T).1,
        l ≫ (baseChangeOfMap D hπ obj.T).hom =
          pullback.fst ((supportSubspace D obj hU).ι ≫ (D.projection obj.T).hom) g ≫
            (supportSubspace D obj hU).ι

AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_and_isOpenImmersion_cohPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackPushforwardOpenImmersion.lean, line 668. The attribute's comment: “the whole statement: for an open immersion π : X → Y of algebraic spaces separated and of finite presentation over B, the morphism Cohstack_{X/B} → Cohstack_{Y/B} of Tag 0DN9 is representable by algebraic spaces and an open immersion in the sense of Tag 04XB, which together are representability by open immersions (Tag 04YL (1))”.

Stacks 0DNA. Let B be an algebraic space and let π : X ⟶ Y be an open immersion of algebraic spaces which are separated and of finite presentation over B, the structure morphism of X being π ≫ f for the structure morphism f : Y ⟶ B. Then the morphism Coh_{X/B} ⟶ Coh_{Y/B} of Stacks 0DN9, AlgebraicGeometry.Space.CoherentPushforwardSituation.cohPushforward, is an open immersion: it is representable by algebraic spaces, and every algebraic space representing its base change along a scheme-valued point of Coh_{Y/B} is an open subspace of that scheme (Stacks 04XB at open immersions), which together are Stacks 04YL (1).

The morphism is fully faithful because π_{T,*} is, π_T being an open immersion; its essential image over a test scheme T is the objects (T, G) with Supp(G) ⊆ |X_T|; and over every scheme-valued point (T₀, G) of Coh_{Y/B} that condition is cut out by the open subscheme on {t ∈ |T₀| : Supp(G) ∩ |Y_t| ⊆ |X_t|}, the locus of the source's hint.

theorem isRepresentableByAlgebraicSpaces_and_isOpenImmersion_cohPushforward
    {A X Y : AlgebraicSpaces B S hS} (π : X ⟶ Y) (f : Y ⟶ A)
    (hopen : IsOpenImmersion B S hS π.hom)
    (hsepX : IsSeparated B S hS (π ≫ f).hom) (hfpX : IsFinitePresentation B S hS (π ≫ f).hom)
    (hsepY : IsSeparated B S hS f.hom) (hfpY : IsFinitePresentation B S hS f.hom) :
    let D := CoherentPushforwardSituation.ofIsOpenImmersion π f hopen hsepX hfpX hsepY hfpY
    Stack.IsRepresentableByAlgebraicSpaces B S hS
        (Bicategory.InducedBicategory.mkHom D.cohPushforward :
          coherentCFG D.source ⟶ coherentCFG D.target).hom ∧
      Stack.IsOpenImmersion B S hS
        (Bicategory.InducedBicategory.mkHom D.cohPushforward :
          coherentCFG D.source ⟶ coherentCFG D.target)

Tag 0DNB, a lemma

Tag 0DNB in the Stacks Project.

AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_and_isClosedImmersion_cohPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackPushforwardClosedImmersion.lean, line 460. The attribute's comment: “the whole statement: for a closed immersion π : X → Y of algebraic spaces separated and of finite presentation over B, the morphism Cohstack_{X/B} → Cohstack_{Y/B} of Tag 0DN9 is representable by algebraic spaces and a closed immersion in the sense of Tag 04XB, which together are representability by closed immersions (Tag 04YL (2))”.

Stacks 0DNB. Let B be an algebraic space and let π : X ⟶ Y be a closed immersion of algebraic spaces which are separated and of finite presentation over B, the structure morphism of X being π ≫ f for the structure morphism f : Y ⟶ B. Then the morphism Coh_{X/B} ⟶ Coh_{Y/B} of Stacks 0DN9, AlgebraicGeometry.Space.CoherentPushforwardSituation.cohPushforward, is a closed immersion: it is representable by algebraic spaces, and every algebraic space representing its base change along a scheme-valued point of Coh_{Y/B} is a closed subspace of that scheme (Stacks 04XB at closed immersions), which together are Stacks 04YL (2).

The proof is the source's. The morphism is fully faithful because π_{T,*} is, π_T being a closed immersion (Stacks 04CJ); its essential image over a test scheme T is the objects (T, G) with G a direct image along π_T, which is the vanishing of the inclusion ker(G ⟶ π_{T,*}π_T^*G) ⟶ G, and that vanishing after base change is cut out by a closed subspace of T by Stacks 083M.

theorem isRepresentableByAlgebraicSpaces_and_isClosedImmersion_cohPushforward
    {A X Y : AlgebraicSpaces B S hS} (π : X ⟶ Y) (f : Y ⟶ A)
    (hclosed : IsClosedImmersion B S hS π.hom)
    (hsepX : IsSeparated B S hS (π ≫ f).hom) (hfpX : IsFinitePresentation B S hS (π ≫ f).hom)
    (hsepY : IsSeparated B S hS f.hom) (hfpY : IsFinitePresentation B S hS f.hom) :
    let D := CoherentPushforwardSituation.ofIsClosedImmersion π f hclosed hsepX hfpX hsepY hfpY
    Stack.IsRepresentableByAlgebraicSpaces B S hS
        (Bicategory.InducedBicategory.mkHom D.cohPushforward :
          coherentCFG D.source ⟶ coherentCFG D.target).hom ∧
      Stack.IsClosedImmersion B S hS
        (Bicategory.InducedBicategory.mkHom D.cohPushforward :
          coherentCFG D.source ⟶ coherentCFG D.target)

Tag 0DNC, a situation

Tag 0DNC in the Stacks Project.

AlgebraicGeometry.Space.NumericalSituation.numericalDirectImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalDirectImage.lean, line 116. The attribute's comment: “the object K_i = Rf_{T,*}(E_{i,T} ⊗^𝐋 𝓕) of D(𝒪_T)”.

For an object (T, 𝓕) of Coh_{X/B} and i ∈ I, the object K_i = Rf_{T,*}(E_{i,T} ⊗^𝐋_{𝒪_{X_T}} 𝓕) of D(𝒪_T), where f_T : X_T ⟶ T is the projection of the base change and E_{i,T} the derived pullback of E_i to X_T.

def numericalDirectImage (i : N.I) :
    DerivedCategory (Modules.{u, u} B S hS (testSpace A).1 (testSpace A).2)

AlgebraicGeometry.Space.NumericalSituation.numericalEuler, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalDirectImage.lean, line 124. The attribute's comment: “the function χ_i : |T| → ℤ, t ↦ χ(K_i ⊗^𝐋 κ(t))”.

The function χ_i : |T| → ℤ whose value at a point t of T is the Euler characteristic χ(K_i ⊗^𝐋 κ(t)) = ∑ (-1)^n dim H^n(K_i ⊗^𝐋 κ(t)) of the derived fibre of K_i at t.

def numericalEuler (i : N.I) : points B S hS (testSpace A).1 → ℤ

AlgebraicGeometry.Space.NumericalSituation.numericalSubstack, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalDirectImage.lean, line 135. The attribute's comment: “the substack Coh^P_{X/B} ⊆ Coh_{X/B} cut out by χ_i(t) = P(i)”.

The substack Coh^P_{X/B} ⊆ Coh_{X/B}: the full subcategory of Coh_{X/B} on the objects (T, 𝓕) with χ_i(t) = P(i) for all i ∈ I and all t ∈ |T|.

abbrev numericalSubstack : Type (u + 1)

AlgebraicGeometry.Space.NumericalSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalInvariants.lean, line 100. The attribute's comment: “the standing data: separatedness of the relative space, the index set, the family of perfect objects of D(𝒪_X), and the prescribed numerical invariants”.

Stacks 0DNC, the standing data. Over a morphism f : X ⟶ Y of algebraic spaces of finite presentation: separatedness of f, a set I, a perfect object of D(𝒪_X) for each i ∈ I, and the prescribed numerical invariants P : I → ℤ.

structure NumericalSituation

Tag 0DND, a lemma

Tag 0DND in the Stacks Project.

AlgebraicGeometry.Space.NumericalSituation.isAlgebraicStack_and_numericalSubstackι_isFlatClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalSubstackAlgebraicFlatClosed.lean, line 62. The attribute's comment: “Coh^P_{X/B} is algebraic and Coh^P_{X/B} -> Coh_{X/B} is a flat closed immersion”.

In Situation 0DNC the substack Coh^P_{X/B} of Coh_{X/B} cut out by χ_i = P(i) is an algebraic stack, and its inclusion into Coh_{X/B} is a flat closed immersion: representable by algebraic spaces, a closed immersion and flat (Properties of Stacks, Section 04XB).

theorem isAlgebraicStack_and_numericalSubstackι_isFlatClosedImmersion :
    Stack.IsAlgebraicStack.{u, w} B S hS
        (D.conditionCFG N.HasNumericalInvariants N.hasNumericalInvariants_inherited).val ∧
      Stack.IsRepresentableByAlgebraicSpaces B S hS
        (D.conditionι N.HasNumericalInvariants N.hasNumericalInvariants_inherited).hom ∧
      Stack.IsClosedImmersion B S hS
        (D.conditionι N.HasNumericalInvariants N.hasNumericalInvariants_inherited) ∧
      Stack.IsFlat B S hS
        (D.conditionι N.HasNumericalInvariants N.hasNumericalInvariants_inherited)

AlgebraicGeometry.Space.NumericalSituation.numericalSubstackι_isOpenAndClosedImmersion_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalSubstackOpenClosedImmersion.lean, line 80. The attribute's comment: “the case I finite: Coh^P_{X/B} is an open and closed substack of Coh_{X/B}”.

If I is finite, Coh^P_{X/B} is an open and closed substack of Coh_{X/B}: its inclusion is representable by algebraic spaces, an open immersion and a closed immersion.

theorem numericalSubstackι_isOpenAndClosedImmersion_of_finite [Finite N.I] :
    Stack.IsRepresentableByAlgebraicSpaces B S hS
        (D.conditionι N.HasNumericalInvariants N.hasNumericalInvariants_inherited).hom ∧
      Stack.IsOpenImmersion B S hS
        (D.conditionι N.HasNumericalInvariants N.hasNumericalInvariants_inherited) ∧
      Stack.IsClosedImmersion B S hS
        (D.conditionι N.HasNumericalInvariants N.hasNumericalInvariants_inherited)

AlgebraicGeometry.Space.NumericalSituation.numericalSubstackι_isOpenAndClosedImmersion_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalSubstackOpenClosedImmersion.lean, line 96. The attribute's comment: “the case B locally Noetherian: Coh^P_{X/B} is an open and closed substack of Coh_{X/B}”.

If B is locally Noetherian (hB) and I is arbitrary, Coh^P_{X/B} is an open and closed substack of Coh_{X/B}: its inclusion is representable by algebraic spaces, an open immersion and a closed immersion.

theorem numericalSubstackι_isOpenAndClosedImmersion_of_isLocallyNoetherian
    (hB : IsLocallyNoetherian B S hS D.Y.1) :
    Stack.IsRepresentableByAlgebraicSpaces B S hS
        (D.conditionι N.HasNumericalInvariants N.hasNumericalInvariants_inherited).hom ∧
      Stack.IsOpenImmersion B S hS
        (D.conditionι N.HasNumericalInvariants N.hasNumericalInvariants_inherited) ∧
      Stack.IsClosedImmersion B S hS
        (D.conditionι N.HasNumericalInvariants N.hasNumericalInvariants_inherited)

Tag 0DNE, a lemma

Tag 0DNE in the Stacks Project.

AlgebraicGeometry.Space.NumericalSituation.isClopen_setOf_chi_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalSubstack.lean, line 131. The attribute's comment: “the open-and-closed clause only, at the level of the locus in |T| cut out by the condition chi_i = P i; Coh_{X/B} is no category here, so no substack claim is made”.

Stacks 0DNE, the open-and-closed clause, at the level of the locus in |T|. For an object (T, 𝓕) of Coh_{X/B} and an index i, the subset of |T| on which the numerical invariant χ_i takes the prescribed value P i is open and closed: χ_i is locally constant by Stacks 0D1Z (AlgebraicGeometry.Space.isLocallyConstant_of_isEtaleLocallyDerivedFibreChi), and the fibres of a locally constant function are open and closed.

theorem isClopen_setOf_chi_eq (c : ChiData B S hS D N) (A : CoherentObject D) (i : N.I) :
    IsClopen {t : testPoints B S hS D A | c.chi A i t = N.P i}

AlgebraicGeometry.Space.NumericalSituation.isOpenAndClosedCondition_ofDerivedTensorPowerProducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalTensorPowerProductsOpenClosed.lean, line 63.

Let f : X ⟶ B be a separated morphism of finite presentation of algebraic spaces, E_1, …, E_r perfect objects of D(𝒪_X) and P : ℤ^{⊕ r} ⟶ ℤ. Then the subcategory Coh^P_{X/B} ⊆ Coh_{X/B} of the objects (T, 𝓕) with χ(X_t, (E_1^{⊗ n_1} ⊗ ⋯ ⊗ E_r^{⊗ n_r})_t ⊗^𝐋 𝓕_t) = P(n) for all n ∈ ℤ^{⊕ r} and all t ∈ T is an open and closed substack.

theorem isOpenAndClosedCondition_ofDerivedTensorPowerProducts (hf : IsSeparated B S hS D.f.hom)
    {r : ℕ}
    (E : Fin r → @DerivedCategory (Modules.{u, u} B S hS D.X.1 D.X.2) _ _
      (HasDerivedCategory.standard _))
    (hE : ∀ j, letI := HasDerivedCategory.standard (Modules.{u, u} B S hS D.X.1 D.X.2)
      (smallEtaleRingedSite B S hS D.X.1 D.X.2).IsPerfect (E j))
    (P : (Fin r → ℤ) → ℤ) :
    IsOpenAndClosedCondition D (ofDerivedTensorPowerProducts hf E hE P).HasNumericalInvariants

Tag 0DNF, an example

Tag 0DNF in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation.exists_hilbertPolynomialι_obj_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertPolynomialSubstack.lean, line 104. The attribute's comment: “an object (T ⟶ B, 𝓕) of Coh_{X/B} lies in Coh^P_{X/B} iff P(n) = χ(X_t, 𝓕_t ⊗ L_t^{⊗ n}) for all n ∈ ℤ and t ∈ T”.

An object (T ⟶ B, 𝓕) of Coh_{X/B} lies in Coh^P_{X/B} = Coh^{P, L}_{X/B} (is the image of an object of it) exactly when P(n) = χ(X_t, 𝓕_t ⊗_{𝒪_{X_t}} L_t^{⊗ n}) for every n ∈ ℤ and every t ∈ T.

theorem exists_hilbertPolynomialι_obj_eq_iff (A : CoherentObject D) :
    (∃ X, (CatFiberedInGroupoids.homFunctor (D.hilbertPolynomialι L P)).obj X = A) ↔
      ∀ (n : ℤ) (t : A.testScheme), P n = CoherentObject.twistedEuler L A t n

AlgebraicGeometry.Space.CoherentSituation.hilbertPolynomialι_isOpenAndClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertPolynomialSubstack.lean, line 119. The attribute's comment: “Coh^P_{X/B} = Coh^{P,L}_{X/B} ⊂ Coh_{X/B} is an open and closed substack”.

Coh^P_{X/B} ⊆ Coh_{X/B} is an open and closed substack: the inclusion Coh^{P, L}_{X/B} ⟶ Coh_{X/B} is representable by algebraic spaces, an open immersion and a closed immersion (Stacks 0DNE for I = ℤ and E_n = L^{⊗ n}).

theorem hilbertPolynomialι_isOpenAndClosedImmersion :
    Stack.IsRepresentableByAlgebraicSpaces B S hS (D.hilbertPolynomialι L P).hom ∧
      Stack.IsOpenImmersion B S hS (D.hilbertPolynomialι L P) ∧
      Stack.IsClosedImmersion B S hS (D.hilbertPolynomialι L P)

AlgebraicGeometry.Space.CoherentSituation.isAlgebraicStack_hilbertPolynomialCFG, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertPolynomialSubstack.lean, line 141. The attribute's comment: “for f : X ⟶ B separated and of finite presentation, Coh^P_{X/B} is an algebraic stack”.

For a separated morphism f : X ⟶ B of finite presentation, Coh^{P, L}_{X/B} is an algebraic stack: Coh_{X/B} is algebraic (Stacks 09DS, with Grothendieck's existence theorem Stacks 0CXB), and the inclusion of Coh^{P, L}_{X/B} is representable by algebraic spaces (Stacks 05UM).

theorem isAlgebraicStack_hilbertPolynomialCFG (hsep : IsSeparated B S hS D.f.hom) :
    Stack.IsAlgebraicStack.{u, w} B S hS (D.hilbertPolynomialCFG L P).val

AlgebraicGeometry.Space.CoherentSituation.hilbertPolynomialLocus_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertPolynomialSubstack.lean, line 156. The attribute's comment: “Coh_{X/B} = ∐_{P numerical polynomial} Coh^P_{X/B} is a disjoint union decomposition, read on each object (T, 𝓕): the loci of the numerical polynomials are open and closed, pairwise disjoint, cover T, and the locus of P cuts out Coh^P_{X/B}”.

The disjoint union decomposition Coh_{X/B} = ∐_P Coh^P_{X/B}, read on each object A = (T, 𝓕) of Coh_{X/B}: the loci of the functions P : ℤ → ℤ (AlgebraicGeometry.Space.CoherentObject.hilbertPolynomialLocus) are open and closed in T, pairwise disjoint, and those of the numerical polynomials cover T (Stacks 0DN4); a morphism A' ⟶ A of Coh_{X/B} has its source in Coh^{P, L}_{X/B} exactly when its map of test schemes lands in the locus of P.

theorem hilbertPolynomialLocus_decomposition (A : CoherentObject D) :
    (∀ P : ℤ → ℤ, IsClopen (A.hilbertPolynomialLocus L P)) ∧
      (⋃ P : {P : ℤ → ℤ // ∃ p : Polynomial ℚ, ∀ m : ℤ, p.eval (m : ℚ) = (P m : ℚ)},
        A.hilbertPolynomialLocus L P.1) = Set.univ ∧
      Pairwise (fun P Q : ℤ → ℤ =>
        Disjoint (A.hilbertPolynomialLocus L P) (A.hilbertPolynomialLocus L Q)) ∧
      ∀ (P : ℤ → ℤ) (A' : CoherentObject D) (φ : CoherentHom A' A),
        CoherentObject.HasHilbertPolynomial L P A' ↔
          Set.range φ.baseScheme ⊆ A.hilbertPolynomialLocus L P

AlgebraicGeometry.Space.NumericalSituation.ofInvertibleTwists, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalInvariantsTwist.lean, line 186. The attribute's comment: “the substack as the specialisation of Situation 0DNC to the index set ℤ and the family n ↦ L^{⊗ n}; perfectness of those twists is a hypothesis, and openness and closedness (Lemma 0DNE) and the disjoint union decomposition are not established”.

Stacks 0DNF, the specialisation of Situation 0DNC. Over a separated morphism f : X ⟶ B of algebraic spaces of finite presentation, an invertible 𝒪_X-module L and a map P : ℤ → ℤ, the standing data of Stacks 0DNC with index set I = ℤ and with the family n ↦ L^{⊗ n} of perfect objects of D(𝒪_X). This is the datum relative to which the source's Coh^P_{X/B} = Coh^{P,L}_{X/B} is formed.

Perfectness of the twists L^{⊗ n} is the hypothesis perfect: the source takes it for granted for an invertible module, and this development has no route to it on the small étale ringed site of an algebraic space. Nothing here asserts that the resulting substack is open and closed — that is Lemma 0DNE, which is absent — nor that P is a numerical polynomial, which the source assumes but which no clause of the specialisation uses.

def NumericalSituation.ofInvertibleTwists (separated : IsSeparated B S hS D.f.hom)
    (L : Modules.{u, u} B S hS D.X.1 D.X.2)
    [hL : Stacks.SheafOfModules.IsInvertible (structurePresheaf B S hS D.X.1)
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B S hS D.X.1 D.X.2).O)).property L]
    (perfect : ∀ n : ℤ, (smallEtaleRingedSite B S hS D.X.1 D.X.2).IsPerfect
      (invertibleTwistObject B S hS D.X.1 D.X.2 L n))
    (P : ℤ → ℤ) : NumericalSituation.{u, 0, u} B S hS D

AlgebraicGeometry.Space.IsPrescribedTwistedEuler, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalInvariantsTwist.lean, line 243. The attribute's comment: “the membership condition P(n) = χ(X_t, 𝓕_t ⊗ L_t^{⊗ n}), stated for a given family of fibrewise twisted Euler characteristics, which this development cannot construct”.

Stacks 0DNF, the membership condition. An object (T ⟶ B, 𝓕) of Coh_{X/B} lies in Coh^P_{X/B} = Coh^{P,L}_{X/B} exactly when

P(n) = χ(X_t, 𝓕_t ⊗_{𝒪_{X_t}} L_t^{⊗ n})

holds for every n ∈ ℤ and every t ∈ T. Here ι is the type of points of the test scheme and χ t n is the Euler characteristic above. That family is given: the Euler characteristic of a perfect object on an algebraic space cannot be constructed in this development, for the reason recorded in the implementation notes of StacksFrontier/AlgebraicGeometry/Quot/NumericalInvariants.lean, and the same device is used by AlgebraicGeometry.Space.IsEtaleLocallyDerivedFibreChi.

def IsPrescribedTwistedEuler {ι : Type v} (P : ℤ → ℤ) (χ : ι → ℤ → ℤ) : Prop

Sources

• Section 108.4, Tag 0DLX
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.CoherentSituation.coherentRelativeDiagonal_affine_finitePresentation · AlgebraicGeometry.Space.CoherentSituation.isFiberedQuasiSeparated_and_isLocallyOfFinitePresentation_toBaseCFG · StacksDraft.CoherentGenericFibre.exists_submodule_finite_flat_isLocalizedModule · AlgebraicGeometry.Space.CoherentSituation.fiberedValuativeExistence_toBaseCFG · AlgebraicGeometry.Space.CoherentPushforwardSituation.cohPushforward · AlgebraicGeometry.Space.isFinite_of_comp_isProper_of_isSeparated_of_isLocallyQuasiFinite · AlgebraicGeometry.Space.isFinitePresentation_of_comp_isProper_of_isSeparated · AlgebraicGeometry.Space.isFinite_comp_of_isLocallyQuasiFinite_of_comp_isProper_of_isSeparated

Section108.5 Properties of Quot#

Section 108.5 of the Stacks Project, Tag 0DM1. 11 tags here are carried by 38 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DM2, a lemma

Tag 0DM2 in the Stacks Project.

AlgebraicGeometry.Space.QuotSituation.diagonal_quotSitePresheafToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorDiagonal.lean, line 425.

The diagonal of Quot_{F/X/B} ⟶ B is a closed immersion. If F is of finite type, then the diagonal is a closed immersion of finite presentation.

The diagonal is that of the Quot presheaf of Type (u + 1) over the base, and being a closed immersion (of finite presentation) is representability by closed immersions of schemes (locally of finite presentation), read through CategoryTheory.uliftYoneda.

theorem diagonal_quotSitePresheafToBase :
    IsClosedImmersionULift.{u + 1} B S hS (pullback.diagonal D.quotSitePresheafToBase) ∧
      (SheafOfModules.IsFiniteTypeOnSite D.F →
        (closedImmersionFinitePresentation (B := B) (S := S) (hS := hS)).relative
          uliftYoneda.{u + 1} (pullback.diagonal D.quotSitePresheafToBase))

Tag 0DM3, a lemma

Tag 0DM3 in the Stacks Project.

AlgebraicGeometry.Space.QuotSituation.isLocallyOfFinitePresentationULift_quotSitePresheafToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorLocallyFinitePresentationOfLimits.lean, line 103. The attribute's comment: “the finite-presentation clause: if F is of finite presentation, Quot_{F/X/B} → B is locally of finite presentation”.

If F is of finite presentation, then Quot_{F/X/B} ⟶ B is locally of finite presentation: the morphism of schemes underlying every commuting square of étale charts of the Quot presheaf over B is locally of finite presentation.

theorem isLocallyOfFinitePresentationULift_quotSitePresheafToBase
    (hF : D.F.IsFinitePresentationOnSite) :
    IsLocallyOfFinitePresentationULift.{u + 1} B S hS D.quotSitePresheafToBase

AlgebraicGeometry.Space.QuotSituation.isSeparatedULift_and_imp_isLocallyOfFinitePresentationULift_quotSitePresheafToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorLocallyFinitePresentationOfLimits.lean, line 112.

The morphism Quot_{F/X/B} ⟶ B is separated, and if F is of finite presentation it is also locally of finite presentation.

theorem isSeparatedULift_and_imp_isLocallyOfFinitePresentationULift_quotSitePresheafToBase :
    IsSeparatedULift.{u + 1} B S hS D.quotSitePresheafToBase ∧
      (D.F.IsFinitePresentationOnSite →
        IsLocallyOfFinitePresentationULift.{u + 1} B S hS D.quotSitePresheafToBase)

Declarations registered for the tag:

• AlgebraicGeometry.Space.QuotSituation.isSeparatedULift_quotSitePresheafToBase, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorDiagonal.lean, line 447 (StacksFrontier): “the separation clause: the diagonal of Quot over B is a closed immersion”.

Tag 0DM4, a lemma

Tag 0DM4 in the Stacks Project.

StacksDraft.GenericFibre.existsUnique_submodule_flat_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotValuativeAffineChart.lean, line 210. The attribute's comment: “the affine-chart case: over a valuation ring a quotient of the generic fibre of a finite module extends uniquely to a quotient flat over the valuation ring and finite over the chart, the extension being the generic-kernel quotient and its flatness Stacks 0539; the etale gluing of Stacks 03M3, the proper support, and the finite presentation of Stacks 0DLR are not covered”. References: EGA IV (2.8.1.1), “special case”.

Stacks 0DM4, on an affine chart over a valuation ring. Let R be a valuation ring, A an R-algebra, M a finite A-module and M_K the generic fibre of M, that is, its localization at the nonzero elements of R. Let P be the kernel of a prescribed quotient of M_K, an A-submodule saturated for the nonzero elements of R. Then there is exactly one A-submodule L of M such that M / L is flat over R and finite over A and the generic fibre of L is P; it is the generic kernel {x ∈ M | ι x ∈ P}.

theorem existsUnique_submodule_flat_quotient [ValuationRing R] [Module.Finite A M]
    (hP : ∀ (s : R) {y : MK}, s ≠ 0 → s • y ∈ P → y ∈ P) :
    ∃! L : Submodule A M, (Module.Flat R (M ⧸ L) ∧ Module.Finite A (M ⧸ L)) ∧
      Submodule.localized₀ R⁰ (ι.restrictScalars R) (L.restrictScalars R)
        = P.restrictScalars R

AlgebraicGeometry.Space.QuotSitePresheafModel.valuativeCriterionExistence_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotValuativeExistence.lean, line 397.

Let f : X ⟶ B be a morphism of algebraic spaces which is proper and of finite presentation, and let F be a quasi-coherent 𝒪_X-module of finite type. Then Quot_{F/X/B} ⟶ B satisfies the existence part of the valuative criterion (Stacks 03IX): for every model of the Quot presheaf, its canonical morphism to B has it. Here the Quot situation D (Stacks 09TR) records f, its finite presentation and the quasi-coherent module F.

theorem QuotSitePresheafModel.valuativeCriterionExistence_toBase (D : QuotSituation B S hS)
    (hproper : IsProper B S hS D.f.hom) (hF : SheafOfModules.IsFiniteTypeOnSite D.F)
    (N : QuotSitePresheafModel D) : ValuativeCriterion.Existence N.toBase

Tag 0DP1, a lemma

Tag 0DP1 in the Stacks Project.

AlgebraicGeometry.Space.QuotPushforwardSituation.pushforwardQuotFunctorMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorAffinePushforward.lean, line 361.

Let B be an algebraic space, let π : X ⟶ Y be an affine quasi-finite morphism of algebraic spaces which are separated and of finite presentation over B, and let F be a quasi-coherent 𝒪_X-module. Then π_* induces a morphism Quot_{F/X/B} ⟶ Quot_{π_*F/Y/B}: over a scheme T over B it sends a quotient F_T ⟶ Q to the quotient (π_*F)_T ≅ π_{T,*}F_T ⟶ π_{T,*}Q.

def pushforwardQuotFunctorMap :
    D.sourceSituation.quotFunctor ⟶ D.directImageSituation.quotFunctor

AlgebraicGeometry.Space.QuotPushforwardSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPushforward.lean, line 130. The attribute's comment: “the standing data”.

Stacks 0DP1, the standing data. An affine quasi-finite morphism π : X ⟶ Y of algebraic spaces which are separated and of finite presentation over an algebraic space B, together with a quasi-coherent 𝒪_X-module F: the data along which the direct image induces a morphism Quot_{F/X/B} ⟶ Quot_{π_*F/Y/B}.

structure QuotPushforwardSituation (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)

AlgebraicGeometry.Space.QuotPushforwardSituation.pushforwardQuotient, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPushforward.lean, line 267. The attribute's comment: “the direct image of a quotient, recorded by its kernel”.

Stacks 0DP1, the direct image of a quotient. The quotient G_T ⟶ π_{T,*}(F_T/K) of G_T obtained from a quotient F_T ⟶ F_T/K by applying π_{T,*} and reading the result through the comparison G_T ≅ π_{T,*}F_T, recorded — as the quotients themselves are — by its kernel.

def pushforwardQuotient (h : SchemeTargetAffinePushforwardQuasicoherent B S hS)
    (c : PushforwardComparison D) (T : SchemesOver D.base)
    (K : Subobject (D.sourceSituation.baseChangeModule T)) :
    Subobject ((D.targetSituation h).baseChangeModule T)

AlgebraicGeometry.Space.QuotPushforwardSituation.pushforwardQuotient_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPushforward.lean, line 325. The attribute's comment: “the direct image of a quotient of the Quot functor is one”.

Stacks 0DP1. The direct image of a quotient in Quot_{F/X/B}(T) lies in Quot_{G/Y/B}(T): the quotient of G_T by it is π_{T,*}(F_T/K), which is quasi-coherent, of finite presentation, flat over T and has support proper over T because F_T/K is, this being the morphism of stacks Coh_{X/B} ⟶ Coh_{Y/B} of Stacks 0DN9.

theorem pushforwardQuotient_mem (h : SchemeTargetAffinePushforwardQuasicoherent B S hS)
    (I : AffinePushforwardQuotInputs D h) (T : SchemesOver D.base)
    (K : Subobject (D.sourceSituation.baseChangeModule T))
    (hK : K ∈ D.sourceSituation.properlySupportedQuotients T) :
    D.pushforwardQuotient h I.comparison T K ∈
      (D.targetSituation h).properlySupportedQuotients T

AlgebraicGeometry.Space.QuotPushforwardSituation.quotFunctorMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPushforward.lean, line 344. The attribute's comment: “the induced morphism of Quot functors”.

Stacks 0DP1. The morphism of Quot functors Quot_{F/X/B} ⟶ Quot_{π_*F/Y/B} induced by the direct image: over a test scheme it sends a quotient F_T ⟶ Q to G_T ⟶ π_{T,*}Q.

Naturality is the compatibility of the direct image with pullback along a morphism of test schemes, part (b) of the proof of Stacks 0DN9.

def quotFunctorMap (h : SchemeTargetAffinePushforwardQuasicoherent B S hS)
    (I : AffinePushforwardQuotInputs D h) :
    D.sourceSituation.quotFunctor ⟶ (D.targetSituation h).quotFunctor

AlgebraicGeometry.Space.QuotPushforwardSituation.pushforwardQuotient', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPushforwardSupplement.lean, line 71. The attribute's comment: “the direct image of a quotient, recorded by its kernel”.

Stacks 0DP1, the direct image of a quotient. The quotient G_T ⟶ π_{T,*}(F_T/K) of G_T obtained from a quotient F_T ⟶ F_T/K by applying π_{T,*} and reading the result through the comparison G_T ≅ π_{T,*}F_T, recorded — as the quotients themselves are — by its kernel.

def pushforwardQuotient' (c : PushforwardComparison D) (T : SchemesOver D.base)
    (K : Subobject (D.sourceSituation.baseChangeModule T)) :
    Subobject (D.targetSituation'.baseChangeModule T)

AlgebraicGeometry.Space.QuotPushforwardSituation.pushforwardQuotient_mem', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPushforwardSupplement.lean, line 114. The attribute's comment: “the direct image of a quotient of the Quot functor is one”.

Stacks 0DP1. The direct image of a quotient in Quot_{F/X/B}(T) lies in Quot_{G/Y/B}(T): the quotient of G_T by it is π_{T,*}(F_T/K), which is quasi-coherent, of finite presentation, flat over T and has support proper over T because F_T/K is, this being the morphism of stacks Coh_{X/B} ⟶ Coh_{Y/B} of Stacks 0DN9.

theorem pushforwardQuotient_mem' (I : AffinePushforwardQuotInputs' D) (T : SchemesOver D.base)
    (K : Subobject (D.sourceSituation.baseChangeModule T))
    (hK : K ∈ D.sourceSituation.properlySupportedQuotients T) :
    D.pushforwardQuotient' I.comparison T K ∈
      D.targetSituation'.properlySupportedQuotients T

AlgebraicGeometry.Space.QuotPushforwardSituation.quotFunctorMap', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPushforwardSupplement.lean, line 132. The attribute's comment: “the induced morphism of Quot functors”.

Stacks 0DP1. The morphism of Quot functors Quot_{F/X/B} ⟶ Quot_{π_*F/Y/B} induced by the direct image: over a test scheme it sends a quotient F_T ⟶ Q to G_T ⟶ π_{T,*}Q.

Naturality is the compatibility of the direct image with pullback along a morphism of test schemes, part (b) of the proof of Stacks 0DN9.

def quotFunctorMap' (I : AffinePushforwardQuotInputs' D) :
    D.sourceSituation.quotFunctor ⟶ D.targetSituation'.quotFunctor

Tag 0DP2, a lemma

Tag 0DP2 in the Stacks Project.

AlgebraicGeometry.Space.QuotPushforwardSituation.isOpenImmersion_pushforwardQuotModelMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorAffineOpenImmersionDirectImage.lean, line 171.

Let B be an algebraic space, let π : X ⟶ Y be an affine open immersion of algebraic spaces which are separated and of finite presentation over B, and let F be a quasi-coherent 𝒪_X-module. Then the morphism Quot_{F/X/B} ⟶ Quot_{π_*F/Y/B} of Stacks 0DP1 is an open immersion.

The morphism is AlgebraicGeometry.Space.QuotPushforwardSituation.pushforwardQuotFunctorMap, read on the Quot presheaves of the site (AlgebraicGeometry.Space.QuotPushforwardSituation.pushforwardQuotSitePresheafMap_app) and then in their canonical models in the universe of the site, where being an open immersion of algebraic spaces is defined (Stacks 02YU).

theorem isOpenImmersion_pushforwardQuotModelMap (base X Y : AlgebraicSpaces B S hS)
    (π : X ⟶ Y) (structureX : X ⟶ base) (structureY : Y ⟶ base)
    (comp : π ≫ structureY = structureX) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) (hπ : IsOpenImmersion B S hS π.hom)
    (haff : IsAffineHom B S hS π.hom) (hsepX : IsSeparated B S hS structureX.hom)
    (hsepY : IsSeparated B S hS structureY.hom)
    (hfpX : IsFinitePresentation B S hS structureX.hom)
    (hfpY : IsFinitePresentation B S hS structureY.hom) :
    IsOpenImmersion B S hS (ofAffineOpenImmersion base X Y π structureX structureY comp F hF hπ
      haff hsepX hsepY hfpX hfpY).pushforwardQuotModelMap

Tag 0DP3, a lemma

Tag 0DP3 in the Stacks Project.

AlgebraicGeometry.Space.QuotOpenImmersionSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorOpenImmersionDirectImage.lean, line 101. The attribute's comment: “the standing data”.

Stacks 0DP3, the standing data. An open immersion j : X ⟶ Y of algebraic spaces which are separated and of finite presentation over an algebraic space B, together with a quasi-coherent 𝒪_Y-module G: the data along which the direct image induces a morphism Quot_{j^*G/X/B} ⟶ Quot_{G/Y/B}.

structure QuotOpenImmersionSituation (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S)

AlgebraicGeometry.Space.QuotOpenImmersionSituation.directImageQuotient, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorOpenImmersionDirectImage.lean, line 254. The attribute's comment: “the direct image of a quotient, recorded by its kernel”.

Stacks 0DP3, the direct image of a quotient. The quotient G_T ⟶ j_{T,*}(F_T/K) of G_T, recorded — as the quotients themselves are — by its kernel.

def directImageQuotient (ν : DirectImageInputs D) (T : SchemesOver D.base)
    (K : Subobject (D.sourceSituation.baseChangeModule T)) :
    Subobject (D.targetSituation.baseChangeModule T)

AlgebraicGeometry.Space.QuotOpenImmersionSituation.directImageQuotient_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorOpenImmersionDirectImage.lean, line 302. The attribute's comment: “the direct image of a quotient of the Quot functor is one”.

Stacks 0DP3. The direct image of a quotient in Quot_{F/X/B}(T) lies in Quot_{G/Y/B}(T): the quotient of G_T by it is j_{T,*}(F_T/K), which is quasi-coherent, of finite presentation, flat over T and has support proper over T because F_T/K is, this being the morphism of stacks Coh_{X/B} ⟶ Coh_{Y/B} of Stacks 0DN9.

theorem directImageQuotient_mem (I : QuotDirectImageInputs D) (T : SchemesOver D.base)
    (K : Subobject (D.sourceSituation.baseChangeModule T))
    (hK : K ∈ D.sourceSituation.properlySupportedQuotients T) :
    D.directImageQuotient I.projections T K ∈
      D.targetSituation.properlySupportedQuotients T

AlgebraicGeometry.Space.QuotOpenImmersionSituation.quotFunctorMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorOpenImmersionDirectImage.lean, line 322. The attribute's comment: “the morphism of Quot functors the source constructs, not its being open”.

Stacks 0DP3, the morphism of Quot functors. The morphism Quot_{F/X/B} ⟶ Quot_{G/Y/B} induced by the direct image: over a test scheme it sends a quotient F_T ⟶ Q to G_T ⟶ j_{T,*}Q. This is the morphism the source constructs; that it is an open immersion is the half of the statement whose proof the source omits, and is not proved here.

Naturality is the compatibility of the direct image with pullback along a morphism of test schemes, part (b) of the proof of Stacks 0DN9.

def quotFunctorMap (I : QuotDirectImageInputs D) :
    D.sourceSituation.quotFunctor ⟶ D.targetSituation.quotFunctor

AlgebraicGeometry.Space.QuotOpenSubspaceSituation.isOpenImmersion_quotSitePresheafModelMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorOpenSubspace.lean, line 847.

Let B be an algebraic space, let j : X ⟶ Y be an open immersion of algebraic spaces which are separated and of finite presentation over B, let G be a quasi-coherent 𝒪_Y-module and set F = j^*G. Then the morphism Quot_{F/X/B} ⟶ Quot_{G/Y/B}, sending a quotient F_T ⟶ Q to G_T ⟶ j_{T,*}Q, is an open immersion of spaces over B.

The Quot functors are read in their canonical models in the universe of the site (AlgebraicGeometry.Space.QuotSituation.quotSitePresheafModel); for arbitrary models this is AlgebraicGeometry.Space.QuotOpenSubspaceSituation.isOpenImmersion_quotModelMap.

theorem isOpenImmersion_quotSitePresheafModelMap :
    IsOpenImmersion B S hS
        (D.quotModelMap D.sourceSituation.quotSitePresheafModel
          D.targetSituation.quotSitePresheafModel) ∧
      D.quotModelMap D.sourceSituation.quotSitePresheafModel
          D.targetSituation.quotSitePresheafModel ≫ D.targetSituation.quotSitePresheafModel.toBase =
        D.sourceSituation.quotSitePresheafModel.toBase

AlgebraicGeometry.Space.QuotOpenSubspaceSituation.isOpenImmersion_quotSitePresheafModelMap_ofOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorOpenSubspace.lean, line 901.

Let B be an algebraic space, let j : X ⟶ Y be an open immersion of algebraic spaces which are separated and of finite presentation over B, let G be a quasi-coherent 𝒪_Y-module and set F = j^*G. Then the morphism Quot_{F/X/B} ⟶ Quot_{G/Y/B}, sending a quotient F_T ⟶ Q to G_T ⟶ j_{T,*}Q, is an open immersion of spaces over B.

The situation D is assembled from the hypotheses by AlgebraicGeometry.Space.QuotOpenSubspaceSituation.ofOpenImmersion. Its source Quot situation D.sourceSituation is F/X/B of Stacks 09TR with F = (modulePullback B S hS j).obj G, the inverse image j^*G (quasi-coherent by Stacks 03GA), and its target Quot situation D.targetSituation is G/Y/B. The Quot functors are read in their canonical models in the universe of the site (AlgebraicGeometry.Space.QuotSituation.quotSitePresheafModel), where being an open immersion of algebraic spaces is defined (Stacks 02YU); for arbitrary models this is AlgebraicGeometry.Space.QuotOpenSubspaceSituation.isOpenImmersion_quotModelMap. Over a test scheme the morphism takes a quotient to its direct image (AlgebraicGeometry.Space.QuotOpenSubspaceSituation.familyEquiv_quotModelMap), and the second conjunct says it is a morphism over B.

theorem isOpenImmersion_quotSitePresheafModelMap_ofOpenImmersion
    (base X Y : AlgebraicSpaces B S hS) (j : X ⟶ Y)
    (structureX : X ⟶ base) (structureY : Y ⟶ base) (comp : j ≫ structureY = structureX)
    (G : Modules.{u, u} B S hS Y.1 Y.2) (quasicoherent : G.IsQuasicoherentOnSite)
    (openImmersion : IsOpenImmersion B S hS j.hom)
    (separatedX : IsSeparated B S hS structureX.hom)
    (separatedY : IsSeparated B S hS structureY.hom)
    (finitePresentationX : IsFinitePresentation B S hS structureX.hom)
    (finitePresentationY : IsFinitePresentation B S hS structureY.hom) :
    let D := ofOpenImmersion base X Y j structureX structureY comp G quasicoherent openImmersion
      separatedX separatedY finitePresentationX finitePresentationY
    D.sourceSituation.F = (modulePullback B S hS j).obj G ∧
      IsOpenImmersion B S hS D.quotSitePresheafModelMap ∧
      D.quotSitePresheafModelMap ≫ D.targetSituation.quotSitePresheafModel.toBase =
        D.sourceSituation.quotSitePresheafModel.toBase

Tag 0DP4, a lemma

Tag 0DP4 in the Stacks Project.

AlgebraicGeometry.Space.QuotPushforwardSituation.isIso_pushforwardQuotFunctorMap_ofIsClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorClosedImmersionDirectImageIso.lean, line 103.

Let B be an algebraic space, let π : X ⟶ Y be a closed immersion of algebraic spaces which are separated and of finite presentation over B, and let F be a quasi-coherent 𝒪_X-module. Then the morphism Quot_{F/X/B} ⟶ Quot_{π_*F/Y/B} of Stacks 0DP1 is an isomorphism.

theorem isIso_pushforwardQuotFunctorMap_ofIsClosedImmersion (base X Y : AlgebraicSpaces B S hS)
    (π : X ⟶ Y) (hπ : IsClosedImmersion B S hS π.hom) (structureX : X ⟶ base)
    (structureY : Y ⟶ base) (comp : π ≫ structureY = structureX)
    (F : Modules.{u, u} B S hS X.1 X.2) (quasicoherent : F.IsQuasicoherentOnSite)
    (separatedX : IsSeparated B S hS structureX.hom)
    (separatedY : IsSeparated B S hS structureY.hom)
    (finitePresentationX : IsFinitePresentation B S hS structureX.hom)
    (finitePresentationY : IsFinitePresentation B S hS structureY.hom) :
    IsIso (ofIsClosedImmersion base X Y π hπ structureX structureY comp F quasicoherent
      separatedX separatedY finitePresentationX finitePresentationY).pushforwardQuotFunctorMap

AlgebraicGeometry.Space.QuotPushforwardSituation.isIso_quotFunctorMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorClosedImmersionPushforward.lean, line 190. The attribute's comment: “an isomorphism, granted 04CJ (3) essential image and 0DN9 reversed”.

Stacks 0DP4. The morphism of Quot functors Quot_{F/X/B} ⟶ Quot_{π_*F/Y/B} induced by the direct image along a closed immersion is an isomorphism: over every test scheme it is a bijection, injectively by full faithfulness of π_{T,*} (Stacks 04CJ) and surjectively by the two carried inputs.

theorem isIso_quotFunctorMap (h : SchemeTargetAffinePushforwardQuasicoherent B S hS)
    (I : D.AffinePushforwardQuotInputs h) (J : D.ClosedImmersionQuotInputs h)
    (hπ : IsClosedImmersion B S hS D.π.hom) :
    IsIso (D.quotFunctorMap h I)

Tag 0DP5, a lemma

Tag 0DP5 in the Stacks Project.

AlgebraicGeometry.Space.QuotSituation.relative_closedImmersionOver_quotientInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorSurjection.lean, line 380.

Let φ : F ⟶ G be a surjection of quasi-coherent 𝒪_X-modules. The canonical transformation Quot_{G/X/B} ⟶ Quot_{F/X/B} of functors on the test schemes over B, sending a quotient G_T ⟶ Q to the quotient F_T ⟶ G_T ⟶ Q, is a closed immersion: it is representable by closed immersions of test schemes.

The Quot functors take values in Type (u + 1), so representability is read through CategoryTheory.uliftYoneda.

theorem relative_closedImmersionOver_quotientInclusion :
    D.closedImmersionOver.relative uliftYoneda.{u + 1} (D.quotientInclusion (hG := hG) φ)

Tag 0DP6, a remark

Tag 0DP6 in the Stacks Project.

AlgebraicGeometry.Space.QuotSituation.numericalQuot, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotNumericalFibreProduct.lean, line 164. The attribute's comment: “the fibre product Quot^P = Quot_{F/X/B} ×_{Coh_{X/B}} Coh^P_{X/B}, as the 2-fibre product over the site of Stacks 0040 of the morphism Quot ⟶ Coh and the inclusion Coh^P ⟶ Coh”.

The fibre product Quot^P_{F/X/B} = Quot_{F/X/B} ×_{Coh_{X/B}} Coh^P_{X/B}, as a category over the big fppf site of S: an object over a scheme U is a member F_T ⟶ 𝒬 of Quot_{F/X/B} over U, an object of Coh^P_{X/B} over U and a vertical isomorphism of their images in Coh_{X/B}.

def numericalQuot : BasedCategory.{u + 1, u + 1} (BigFppfOver B S hS)

AlgebraicGeometry.Space.QuotSituation.numericalQuotSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotNumericalSubspace.lean, line 105. The attribute's comment: “Quot^P_{F/X/B} as the subfunctor of Quot_{F/X/B} of the quotients whose object of Coh_{X/B} lies in Coh^P_{X/B}; it is the fibre product numericalQuot by mem_numericalQuotSubspace_iff_exists_numericalQuot”.

Quot^P_{F/X/B}, as the subfunctor of the Quot presheaf it is: the quotients F_T ⟶ 𝒬 whose object (T, 𝒬) of Coh_{X/B} has χ(K_i ⊗^𝐋 κ(t)) = P(i) for all i ∈ I and t ∈ |T|, where K_i = Rf_{T,*}(E_{i,T} ⊗^𝐋 𝒬). It is a subfunctor because the numerical invariants are compatible with pullback (AlgebraicGeometry.Space.NumericalSituation.numericalEuler_eq_of_hom, from Stacks 0A1P).

def numericalQuotSubspace : Subfunctor D.quotSitePresheaf

AlgebraicGeometry.Space.QuotSituation.numericalQuotToQuot_fullyFaithful_and_mem_numericalQuotSubspace_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotNumericalSubspace.lean, line 123. The attribute's comment: “the fibre product Quot_{F/X/B} x_{Coh_{X/B}} Coh^P_{X/B} is the subfunctor numericalQuotSubspace: the left vertical arrow is fully faithful with that essential image”.

The fibre product Quot^P_{F/X/B} = Quot_{F/X/B} ×_{Coh_{X/B}} Coh^P_{X/B} of the remark (AlgebraicGeometry.Space.QuotSituation.numericalQuot) is the subfunctor AlgebraicGeometry.Space.QuotSituation.numericalQuotSubspace of Quot_{F/X/B}: its projection to Quot_{F/X/B} is fully faithful, and a quotient F_T ⟶ 𝒬 lifts to it exactly when it lies in the subfunctor.

theorem numericalQuotToQuot_fullyFaithful_and_mem_numericalQuotSubspace_iff :
    (D.numericalQuotToQuot N).toFunctor.Full ∧ (D.numericalQuotToQuot N).toFunctor.Faithful ∧
      ∀ {T : (BigFppfOver B S hS)ᵒᵖ} (x : D.quotSitePresheaf.obj T),
        x ∈ (D.numericalQuotSubspace N).obj T ↔
          ∃ P : D.NumericalQuotObjects N, P.x = QuotFamilyOver.toQuotObjects x

AlgebraicGeometry.Space.QuotSituation.relative_closedImmersion_flat_numericalQuotSubspace_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotNumericalSubspace.lean, line 137. The attribute's comment: “the left vertical arrow Quot^P -> Quot is a flat closed immersion”.

Quot^P_{F/X/B} ⟶ Quot_{F/X/B} is a flat closed immersion: its base change to every scheme of the site is a flat closed immersion. It is the base change of the flat closed immersion Coh^P_{X/B} ⟶ Coh_{X/B} of Lemma 0DND, the functions χ_i being compatible with pullback and locally constant (Stacks 0A1P, 0D1Z).

theorem relative_closedImmersion_flat_numericalQuotSubspace_ι :
    (MorphismProperty.inverseImage
      (@_root_.AlgebraicGeometry.IsClosedImmersion.{u} ⊓ @Flat.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative uliftYoneda.{u + 1}
        (D.numericalQuotSubspace N).ι

AlgebraicGeometry.Space.QuotSituation.relative_openImmersion_closedImmersion_numericalQuotSubspace_ι_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotNumericalSubspace.lean, line 149. The attribute's comment: “the left vertical arrow is an open and closed immersion if I is finite”.

For a finite index set, Quot^P_{F/X/B} ⟶ Quot_{F/X/B} is an open and closed immersion.

theorem relative_openImmersion_closedImmersion_numericalQuotSubspace_ι_of_finite [Finite N.I] :
    (MorphismProperty.inverseImage
      (@_root_.AlgebraicGeometry.IsOpenImmersion.{u} ⊓
        @_root_.AlgebraicGeometry.IsClosedImmersion.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative uliftYoneda.{u + 1}
        (D.numericalQuotSubspace N).ι

AlgebraicGeometry.Space.QuotSituation.relative_openImmersion_closedImmersion_numericalQuotSubspace_ι_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotNumericalSubspace.lean, line 164. The attribute's comment: “the left vertical arrow is an open and closed immersion if B is locally Noetherian”.

For B locally Noetherian, Quot^P_{F/X/B} ⟶ Quot_{F/X/B} is an open and closed immersion, however large the index set: every object of Coh_{X/B} is étale locally pulled back from one over a Noetherian test scheme, on which the locus where every χ_i takes its prescribed value is an intersection of unions of connected components, hence open.

theorem relative_openImmersion_closedImmersion_numericalQuotSubspace_ι_of_isLocallyNoetherian
    (hB : IsLocallyNoetherian B S hS D.Y.1) :
    (MorphismProperty.inverseImage
      (@_root_.AlgebraicGeometry.IsOpenImmersion.{u} ⊓
        @_root_.AlgebraicGeometry.IsClosedImmersion.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative uliftYoneda.{u + 1}
        (D.numericalQuotSubspace N).ι

AlgebraicGeometry.Space.QuotSituation.isAlgebraicSpace_subfunctorModel_numericalQuotSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotNumericalSubspace.lean, line 183. The attribute's comment: “Quot^P_{F/X/B} is an algebraic space, for F etale-locally generated by fewer than mu sections with mu below the cutoff of the site (every F of finite type)”.

Quot^P_{F/X/B} is an algebraic space, for F étale-locally generated by fewer than μ sections with μ below the cutoff of the site (for instance F of finite type): every model of Quot^P_{F/X/B} in the universe of the site is an algebraic space. It maps to a model of Quot_{F/X/B}, an algebraic space by Stacks 09TU, by a flat closed immersion. For an arbitrary quasi-coherent F the assertion fails on the size-bounded site.

theorem isAlgebraicSpace_subfunctorModel_numericalQuotSubspace
    (hF : ∃ μ < B.cutoff, IsEtaleLocallyGeneratedBelow B S hS μ D.F)
    (F : D.SubfunctorModel (D.numericalQuotSubspace N)) : IsAlgebraicSpace B S hS F.presheaf

AlgebraicGeometry.Space.QuotSituation.relative_openImmersion_closedImmersion_hilbertPolynomialQuot_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotNumericalSubspace.lean, line 206. The attribute's comment: “the left vertical arrow is an open and closed immersion if I = Z and E_i = L^{(x) i} for an invertible L; this is Quot^{P,L}, cut out by P(n) = chi(X_t, Q_t (x) L_t^n)”.

For I = ℤ and E_i = 𝓛^{⊗ i}, Quot^{P, 𝓛}_{F/X/B} ⟶ Quot_{F/X/B} is an open and closed immersion. For an invertible 𝒪_X-module 𝓛 and P : ℤ → ℤ, the subfunctor Quot^{P, 𝓛}_{F/X/B} of the quotients F_T ⟶ 𝒬 with P(n) = χ(X_t, 𝒬_t ⊗ 𝓛_t^{⊗ n}) for all n ∈ ℤ and t ∈ |T| (AlgebraicGeometry.Space.QuotSituation.hilbertPolynomialQuot, the condition of Example 0DNF) is an open and closed subfunctor: it is the base change of the open and closed substack Coh^{P, 𝓛}_{X/B}.

theorem relative_openImmersion_closedImmersion_hilbertPolynomialQuot_ι (P : ℤ → ℤ) :
    (MorphismProperty.inverseImage
      (@_root_.AlgebraicGeometry.IsOpenImmersion.{u} ⊓
        @_root_.AlgebraicGeometry.IsClosedImmersion.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative uliftYoneda.{u + 1}
        (D.hilbertPolynomialQuot L P).ι

AlgebraicGeometry.Space.QuotSituation.cohObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotToCoherentStack.lean, line 289. The attribute's comment: “the object part of the morphism Quot_{F/X/B} ⟶ Coh_{X/B}: a quotient F_T ⟶ Q in Quot_{F/X/B}(T) goes to the object Q of Coh_{X/B} over T. The action on morphisms of test schemes is AlgebraicGeometry.Space.QuotSituation.cohHom. The functor laws hold for the OBJECT part (cohObject_quotientPullback_id, cohObject_quotientPullback_comp) but are NOT established for the module comparisons, Coh_{X/B} not being a category in this development; and the fibre product Quot^P = Quot ×_{Coh} Coh^P of the remark is NOT formed: Coh^P_{X/B} is not constructed anywhere in this development, only the standing data of Situation 0DNC. See the module docstring for the full accounting”.

Stacks 0DP6, the object part of the morphism Quot_{F/X/B} ⟶ Coh_{X/B}. A T-point F_T ⟶ 𝒬 of the Quot functor, recorded by its kernel K, goes to the object (T, F_T/K) of Coh_{X/B}: the four conditions an object of Coh_{X/B} over T satisfies — quasi-coherence, finite presentation, flatness over T and proper support over T — are the four conditions cutting Quot_{F/X/B}(T) out of the subobjects of F_T.

def cohObject (T : SchemesOver D.Y) (K : Subobject (D.baseChangeModule T))
    (hK : K ∈ D.properlySupportedQuotients T) : CoherentObject D.toCoherentSituation

AlgebraicGeometry.Space.QuotSituation.cohHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotToCoherentStack.lean, line 313. The attribute's comment: “the action of the morphism Quot_{F/X/B} ⟶ Coh_{X/B} on morphisms of test schemes, whose object part is AlgebraicGeometry.Space.QuotSituation.cohObject: the base map is h itself, so the morphism lies over the identity of the schemes over B, and the module comparison is the one of Tag 03LU identifying the inverse image of F_T/K with the quotient of F_{T'} by the pulled-back kernel. No hypothesis is carried: the preservation under inverse image of finite presentation (Properties of Spaces, Section 05VR) is the theorem AlgebraicGeometry.Space.QuotientSituation.pullbackPreservesFinitePresentation. The functor laws for the module comparisons are NOT established and the fibre product Quot^P of the remark is NOT formed; see the module docstring”.

Stacks 0DP6, the action of the morphism Quot_{F/X/B} ⟶ Coh_{X/B} on morphisms of test schemes. A morphism h : T' ⟶ T of test schemes over B and a member K of Quot_{F/X/B}(T) give a morphism of Coh_{X/B} from the object attached to the inverse image of K to the object attached to K: its base map is h itself, and its module comparison is the identification of the inverse image of F_T/K with the quotient of F_{T'} by the pulled-back kernel.

def cohHom {T' T : SchemesOver D.Y}
    (h : T' ⟶ T)
    {K : Subobject (D.baseChangeModule T)} (hK : K ∈ D.properlySupportedQuotients T) :
    CoherentHom
      (D.cohObject T' (D.quotientPullback h K)
        (D.quotientPullback_mem_properlySupportedQuotients h K hK))
      (D.cohObject T K hK)

AlgebraicGeometry.Space.QuotSituation.quotToCoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotToCoherentStackFunctor.lean, line 308. The attribute's comment: “the morphism Quot_{F/X/B} ⟶ Coh_{X/B} sending F_T ⟶ Q to the object Q over T, as a 1-morphism of categories over the big fppf site (functor laws included)”.

Stacks 0DP6, the morphism Quot_{F/X/B} ⟶ Coh_{X/B}. The rule sending an element F_T ⟶ 𝒬 of Quot_{F/X/B}(T) to the object 𝒬 of Coh_{X/B} over T, and a morphism of test schemes along which one quotient pulls back to another to the morphism of Coh_{X/B} with that base map identifying the inverse image of the one quotient with the other, is a 1-morphism of categories over the big fppf site: it respects identities and composition, by the coherences of the comparisons of inverse images of Stacks 03LU, and it does not change the underlying test scheme.

def quotToCoherent :
    D.quotBasedCategory ⥤ᵇ coherentBasedCategory D.toCoherentSituation.categoryData

Tag 0DP7, a lemma

Tag 0DP7 in the Stacks Project.

AlgebraicGeometry.Space.isPrescribedTwistedEuler_iff_shift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalInvariantsTwist.lean, line 289. The attribute's comment: “the final statement at the level of membership conditions: the condition for P and 𝓕 is the condition for P'(t) = P(t + 1) and 𝓕 ⊗ L. The isomorphism Quot_{𝓕/X/B} ⟶ Quot_{𝓕 ⊗ L/X/B} itself is not constructed”.

Stacks 0DP7, the final statement, at the level of membership conditions. Tensoring with an invertible module L replaces the twisted Euler characteristics n ↦ χ(X_t, 𝓕_t ⊗ L_t^{⊗ n}) of 𝓕 by their shift n ↦ χ(X_t, 𝓕_t ⊗ L_t^{⊗ (n + 1)}), which is the hypothesis twist. The condition cutting out Quot^P_{𝓕/X/B} is then the condition cutting out Quot^{P'}_{𝓕 ⊗ L/X/B} for P'(t) = P(t + 1).

The isomorphism Quot_{𝓕/X/B} ⟶ Quot_{𝓕 ⊗ L/X/B} of the first statement of the source is not constructed here, and neither are the two open and closed substacks it is claimed to restrict to.

theorem isPrescribedTwistedEuler_iff_shift {ι : Type v} {P : ℤ → ℤ} {χ χ' : ι → ℤ → ℤ}
    (twist : ∀ (t : ι) (m : ℤ), χ' t m = χ t (m + 1)) :
    IsPrescribedTwistedEuler P χ ↔ IsPrescribedTwistedEuler (fun m => P (m + 1)) χ'

AlgebraicGeometry.Space.QuotSituation.quotSitePresheafTensorInvertibleIso_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorTensorInvertible.lean, line 553. The attribute's comment: “the isomorphism Quot_{F/X/B} ≅ Quot_{F ⊗ L/X/B} given by tensoring with L, and its restriction to Quot^P ≅ Quot^{P'} for P'(t) = P(t + 1), membership read on the actual twisted Euler characteristics χ(X_t, Q_t ⊗ L_t^{⊗ n})”.

Stacks 0DP7. Let f : X ⟶ B be a morphism of algebraic spaces of finite presentation, F a quasi-coherent 𝒪_X-module and L an invertible 𝒪_X-module. Tensoring with L is an isomorphism of Quot functors AlgebraicGeometry.Space.QuotSituation.quotSitePresheafTensorInvertibleIso : Quot\_\{F/X/B} ≅ Quot\_\{F ⊗ L/X/B}; precisely:

• it lies over B;
• it sends a quotient F_T ⟶ Q over T to a quotient of (F ⊗ L)_T with quotient module Q ⊗ L_T;
• for every P : ℤ → ℤ it carries Quot^P_{F/X/B} onto Quot^{P'}_{F ⊗ L/X/B}, where P'(n) = P(n + 1): a quotient lies in Quot^P_{F/X/B} exactly when its image lies in Quot^{P'}_{F ⊗ L/X/B}, membership being that the object of Coh_{X/B} the quotient gives has Hilbert polynomial P, respectively P', with respect to L (Stacks 0DNF).

theorem quotSitePresheafTensorInvertibleIso_spec :
    (D.quotSitePresheafTensorInvertibleIso L).hom ≫
        (D.tensorInvertible L).quotSitePresheafToBase = D.quotSitePresheafToBase ∧
      (∀ {T : (BigFppfOver B S hS)ᵒᵖ} (x : D.quotSitePresheaf.obj T),
        Nonempty ((D.tensorInvertible L).quotientModule _
            ((D.quotSitePresheafTensorInvertibleIso L).hom.app T x).subobject ≅
          moduleTensor B S hS (D.space _) (D.quotientModule _ x.subobject)
            (D.baseChangeInvertible L _))) ∧
      ∀ (P : ℤ → ℤ) {T : (BigFppfOver B S hS)ᵒᵖ} (x : D.quotSitePresheaf.obj T),
        letI : Stacks.SheafOfModules.IsInvertible
            (structurePresheaf B S hS (D.tensorInvertible L).toCoherentSituation.X.1)
            ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS
              (D.tensorInvertible L).toCoherentSituation.X.1
              (D.tensorInvertible L).toCoherentSituation.X.2).O)).property L := hL
        letI : Stacks.SheafOfModules.IsInvertible
            (structurePresheaf B S hS D.toCoherentSituation.X.1)
            ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS
              D.toCoherentSituation.X.1 D.toCoherentSituation.X.2).O)).property L := hL
        (((D.quotSitePresheafTensorInvertibleIso L).hom.app T x).cohObject.HasHilbertPolynomial L
            (fun n ↦ P (n + 1)) ↔
          x.cohObject.HasHilbertPolynomial L P)

Tag 0DP8, a lemma

Tag 0DP8 in the Stacks Project.

AlgebraicGeometry.Space.isPrescribedTwistedEuler_iff_reindexMul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalInvariantsTwist.lean, line 307. The attribute's comment: “the equality Quot^{P,L} = Quot^{P',L^{⊗ n}} with P'(t) = P(n t), read on the two membership conditions, for n ≠ 0 and numerical-polynomial invariants; the substacks themselves are not constructed in this development”.

Stacks 0DP8, at the level of membership conditions. Replacing L by L^{⊗ n} replaces the twisted Euler characteristics m ↦ χ(X_t, 𝓕_t ⊗ L_t^{⊗ m}) by m ↦ χ(X_t, 𝓕_t ⊗ L_t^{⊗ n m}), which is the hypothesis twist. For n ≠ 0 the condition cutting out Quot^{P,L}_{𝓕/X/B} is then the condition cutting out Quot^{P',L^{⊗ n}}_{𝓕/X/B} for P'(t) = P(n t): this is the source's equality of the two substacks, read on their defining conditions.

The hypotheses hP and hχ say that P and each χ t are numerical polynomials, represented by the rational polynomials p and q t. They are not removable: for a general P the right-hand condition constrains only the values of P at the multiples of n.

theorem isPrescribedTwistedEuler_iff_reindexMul {ι : Type v} {P : ℤ → ℤ} {χ χ' : ι → ℤ → ℤ}
    {p : Polynomial ℚ} {q : ι → Polynomial ℚ}
    (hP : ∀ m : ℤ, p.eval (m : ℚ) = (P m : ℚ))
    (hχ : ∀ (t : ι) (m : ℤ), (q t).eval (m : ℚ) = (χ t m : ℚ))
    {n : ℤ} (hn : n ≠ 0) (twist : ∀ (t : ι) (m : ℤ), χ' t m = χ t (n * m)) :
    IsPrescribedTwistedEuler P χ ↔ IsPrescribedTwistedEuler (fun m => P (n * m)) χ'

AlgebraicGeometry.Space.QuotSituation.setOf_hasHilbertPolynomial_invertibleTensorPower_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorTensorPowerReindex.lean, line 106. The attribute's comment: “the equality Quot^{P,L} = Quot^{P',L^{⊗ n}} with P'(t) = P(n t), for n ≠ 0 and P a numerical polynomial, compared on the sections over every scheme of the site, membership read on the actual twisted Euler characteristics χ(X_t, Q_t ⊗ L_t^{⊗ m})”.

Let f : X ⟶ B be a morphism of algebraic spaces of finite presentation, F a quasi-coherent 𝒪_X-module, L an invertible 𝒪_X-module, P : ℤ → ℤ a numerical polynomial (at every integer, the value of a rational polynomial) and n a nonzero integer. Then

Quot^{P, L}_{F/X/B} = Quot^{P', L^{⊗ n}}_{F/X/B}, where P'(t) = P(n t):

over every scheme T of the site, a quotient F_T ⟶ Q in Quot_{F/X/B}(T) satisfies P(m) = χ(X_t, Q_t ⊗ L_t^{⊗ m}) for all t ∈ T and m ∈ ℤ exactly when it satisfies P(n m) = χ(X_t, Q_t ⊗ (L^{⊗ n})_t^{⊗ m}) for all t ∈ T and m ∈ ℤ, these being the twisted Euler characteristics AlgebraicGeometry.Space.CoherentObject.twistedEuler of the object of Coh_{X/B} the quotient gives.

theorem setOf_hasHilbertPolynomial_invertibleTensorPower_eq {P : ℤ → ℤ}
    (hP : ∃ p : Polynomial ℚ, ∀ m : ℤ, p.eval (m : ℚ) = (P m : ℚ)) {n : ℤ} (hn : n ≠ 0)
    (T : (BigFppfOver B S hS)ᵒᵖ) :
    letI : Stacks.SheafOfModules.IsInvertible
        (structurePresheaf B S hS D.toCoherentSituation.X.1)
        ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS
          D.toCoherentSituation.X.1 D.toCoherentSituation.X.2).O)).property L := hL
    letI := isInvertible_invertibleTensorPower B S hS D.toCoherentSituation.X.1
      D.toCoherentSituation.X.2 L n
    {x : D.quotSitePresheaf.obj T | x.cohObject.HasHilbertPolynomial L P} =
      {x : D.quotSitePresheaf.obj T | x.cohObject.HasHilbertPolynomial
        (invertibleTensorPower B S hS D.toCoherentSituation.X.1 D.toCoherentSituation.X.2 L n)
        (fun m => P (n * m))}

Sources

• Section 108.5, Tag 0DM1
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.QuotSituation.diagonal_quotSitePresheafToBase · AlgebraicGeometry.Space.QuotSituation.isLocallyOfFinitePresentationULift_quotSitePresheafToBase · AlgebraicGeometry.Space.QuotSituation.isSeparatedULift_and_imp_isLocallyOfFinitePresentationULift_quotSitePresheafToBase · AlgebraicGeometry.Space.QuotSituation.isSeparatedULift_quotSitePresheafToBase · StacksDraft.GenericFibre.existsUnique_submodule_flat_quotient · AlgebraicGeometry.Space.QuotSitePresheafModel.valuativeCriterionExistence_toBase · AlgebraicGeometry.Space.QuotPushforwardSituation.pushforwardQuotFunctorMap · AlgebraicGeometry.Space.QuotPushforwardSituation

Section108.6 Boundedness for Quot#

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

Tag 0DPA, a lemma

Tag 0DPA in the Stacks Project.

AlgebraicGeometry.ProjectiveQuot.isProperAlgebraicSpaceOver_hilbertSubfunctor_quotSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ProjectiveQuot/SiteQuotProper.lean, line 140.

Let n ≥ 0, r ≥ 1 and P ∈ ℚ[t]. The algebraic space Quot^P_{𝒪^{⊕ r}_{ℙⁿ_ℤ}/ℙⁿ_ℤ/ℤ} parametrizing quotients of 𝒪^{⊕ r}_{ℙⁿ_ℤ} with Hilbert polynomial P is proper over Spec ℤ: the subfunctor of the Quot presheaf (Stacks 09TR) of 𝒪^{⊕ r}/ℙⁿ_ℤ/ℤ of the quotients which, read on ℙⁿ_T, have Hilbert polynomial P on every fibre is an algebraic space proper over Spec ℤ.

theorem isProperAlgebraicSpaceOver_hilbertSubfunctor_quotSituation (hr : 1 ≤ r)
    (P : Polynomial ℚ) :
    (quotSituation B n r).IsProperAlgebraicSpaceOver
      (hilbertSubfunctor (quotSituationFrame B n r) P)

Tag 0DPB, a lemma

Tag 0DPB in the Stacks Project.

AlgebraicGeometry.ProjectiveQuotOverSpace.isProperAlgebraicSpaceOver_hilbertPolynomialQuot_productSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ProjectiveQuotOverSpace/QuotProper.lean, line 45.

Let Y be an algebraic space, X = Y × ℙⁿ_ℤ, 𝓛 the pullback of 𝒪_{ℙⁿ}(1) to X and F an 𝒪_X-module of finite presentation. For a numerical polynomial P : ℤ → ℤ (the function of a rational polynomial p), the algebraic space Quot^P_{F/X/Y} parametrizing quotients of F having Hilbert polynomial P with respect to 𝓛 is proper over Y.

theorem isProperAlgebraicSpaceOver_hilbertPolynomialQuot_productSpace
    (Y : AlgebraicSpaces B integerBase B.contains_integerBase)
    (F : Space.Modules.{u, u} B integerBase B.contains_integerBase (productSpace n Y).1
      (productSpace n Y).2) (hF : SheafOfModules.IsFinitePresentationOnSite F)
    {P : ℤ → ℤ} {p : Polynomial ℚ} (hP : ∀ m : ℤ, p.eval (m : ℚ) = (P m : ℚ)) :
    (situation n Y F (@SheafOfModules.isQuasicoherentOnSite_of_isFinitePresentationOnSite
        _ _ _ _ F hF)).IsProperAlgebraicSpaceOver
      ((situation n Y F (@SheafOfModules.isQuasicoherentOnSite_of_isFinitePresentationOnSite
          _ _ _ _ F hF)).hilbertPolynomialQuot
        (twistingModule (situationFrame n Y F
          (@SheafOfModules.isQuasicoherentOnSite_of_isFinitePresentationOnSite _ _ _ _ F hF)))
        (hL := isInvertible_twistingModule (situationFrame n Y F
          (@SheafOfModules.isQuasicoherentOnSite_of_isFinitePresentationOnSite _ _ _ _ F hF))) P)

Tag 0DPC, a lemma

Tag 0DPC in the Stacks Project.

AlgebraicGeometry.Space.QuotSituation.isProperAlgebraicSpaceOver_hilbertPolynomialQuot_of_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotHilbertPolynomialRelativelyAmpleProper.lean, line 59.

Stacks 0DPC. Let f : X ⟶ B be a proper morphism of finite presentation of algebraic spaces (over Spec ℤ), F a finitely presented 𝒪_X-module, L an invertible 𝒪_X-module ample on X/B (Stacks 0D31) and P a numerical polynomial. Then the algebraic space Quot^P_{F/X/B} parametrizing quotients of F having Hilbert polynomial P with respect to L is proper over B.

theorem isProperAlgebraicSpaceOver_hilbertPolynomialQuot_of_isRelativelyAmple
    (D : QuotSituation B integerBase B.contains_integerBase)
    (hf : IsProper B integerBase B.contains_integerBase D.f.hom)
    (hF : SheafOfModules.IsFinitePresentationOnSite D.F)
    (L : Modules.{u, u} B integerBase B.contains_integerBase D.X.1 D.X.2)
    [hL : Stacks.SheafOfModules.IsInvertible (structurePresheaf B integerBase
      B.contains_integerBase D.X.1)
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B integerBase B.contains_integerBase D.X.1 D.X.2).O)).property L]
    (hamp : IsRelativelyAmple B integerBase B.contains_integerBase D.f L)
    {P : ℤ → ℤ} {p : Polynomial ℚ} (hP : ∀ m : ℤ, p.eval (m : ℚ) = (P m : ℚ)) :
    D.IsProperAlgebraicSpaceOver (D.hilbertPolynomialQuot L P)

Tag 0DPD, a lemma

Tag 0DPD in the Stacks Project.

AlgebraicGeometry.Space.QuotSituation.exists_model_isSeparated_isFinitePresentation_hilbertPolynomialQuot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotHilbertPolynomialSeparatedFinitePresentation.lean, line 51.

Let F/X/B be a Quot situation over Spec ℤ (Stacks 09TR): f : X ⟶ B a morphism of finite presentation of algebraic spaces and F a quasi-coherent 𝒪_X-module. If f is separated, F is of finite presentation, L is an invertible 𝒪_X-module ample on X/B (Stacks 0D31) and P is a numerical polynomial, then Quot^P_{F/X/B} (the quotients of F having Hilbert polynomial P with respect to L) has a model M in the universe of the site, identified with it over B, which is an algebraic space whose morphism to B is separated and of finite presentation.

theorem exists_model_isSeparated_isFinitePresentation_hilbertPolynomialQuot
    (D : QuotSituation B integerBase B.contains_integerBase)
    (hsep : IsSeparated B integerBase B.contains_integerBase D.f.hom)
    (hF : SheafOfModules.IsFinitePresentationOnSite D.F)
    (L : Modules.{u, u} B integerBase B.contains_integerBase D.X.1 D.X.2)
    [hL : Stacks.SheafOfModules.IsInvertible
      (structurePresheaf B integerBase B.contains_integerBase D.X.1)
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B integerBase B.contains_integerBase D.X.1 D.X.2).O)).property L]
    (hamp : IsRelativelyAmple B integerBase B.contains_integerBase D.f L)
    {P : ℤ → ℤ} {p : Polynomial ℚ} (hP : ∀ m : ℤ, p.eval (m : ℚ) = (P m : ℚ)) :
    ∃ M : D.SubfunctorModel (D.hilbertPolynomialQuot L P),
      IsAlgebraicSpace B integerBase B.contains_integerBase M.presheaf ∧
        IsSeparated B integerBase B.contains_integerBase M.toBase ∧
        IsFinitePresentation B integerBase B.contains_integerBase M.toBase

Sources

• Section 108.6, Tag 0DP9
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.ProjectiveQuot.isProperAlgebraicSpaceOver_hilbertSubfunctor_quotSituation · AlgebraicGeometry.ProjectiveQuotOverSpace.isProperAlgebraicSpaceOver_hilbertPolynomialQuot_productSpace · AlgebraicGeometry.Space.QuotSituation.isProperAlgebraicSpaceOver_hilbertPolynomialQuot_of_isRelativelyAmple · AlgebraicGeometry.Space.QuotSituation.exists_model_isSeparated_isFinitePresentation_hilbertPolynomialQuot

Section108.7 Properties of the Hilbert functor#

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

Tag 0DM6, a lemma

Tag 0DM6 in the Stacks Project.

AlgebraicGeometry.Space.diagonal_hilbertPresheafToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorDiagonal.lean, line 83.

Stacks 0DM6. The diagonal of Hilb_{X/Y} ⟶ Y is a closed immersion of finite presentation, for f : X ⟶ Y of finite presentation.

The Hilbert presheaf takes values in Type (u + 1), closed subspaces being recorded as subfunctors, so its diagonal is read through CategoryTheory.uliftYoneda: it is representable by closed immersions of schemes locally of finite presentation.

theorem diagonal_hilbertPresheafToBase (f : X ⟶ Y) (hf : IsFinitePresentation B S hS f.hom) :
    (closedImmersionFinitePresentation (B := B) (S := S) (hS := hS)).relative uliftYoneda.{u + 1}
      (pullback.diagonal (hilbertPresheafToBase f))

Tag 0DM7, a lemma

Tag 0DM7 in the Stacks Project.

AlgebraicGeometry.Space.HilbertPresheafModel.isSeparated_and_isLocallyOfFinitePresentation_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorSeparatedLocallyFinitePresentation.lean, line 48.

For a morphism f : X ⟶ Y of algebraic spaces over S which is separated and of finite presentation, the morphism Hilb_{X/Y} ⟶ Y from the Hilbert functor of Stacks 0CZY to the base — read on the canonical model of the Hilbert presheaf in the universe of the site — is separated and locally of finite presentation.

theorem HilbertPresheafModel.isSeparated_and_isLocallyOfFinitePresentation_toBase
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hsep : IsSeparated B S hS f.hom)
    (hfp : IsFinitePresentation B S hS f.hom) :
    IsSeparated B S hS (HilbertPresheafModel.canonical f).toBase ∧
      IsLocallyOfFinitePresentation B S hS (HilbertPresheafModel.canonical f).toBase

Tag 0DM8, a lemma

Tag 0DM8 in the Stacks Project.

AlgebraicGeometry.Space.valuativeCriterionExistence_hilbertPresheafModel_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertValuativeExistence.lean, line 213. The attribute's comment: “the existence part of the valuative criterion for Hilb_{X/B} ⟶ B, for any model of the Hilbert presheaf. WARNING, stated plainly: given the carried e, he (Lemma 0D00) the carried hex (Lemma 0DM4 for Quot_{F/X/B} ⟶ B) is INTER-DERIVABLE with the conclusion, the identification making the transport run both ways, so this statement's content is the transport and the model-independence, not the criterion. The unconditional results are the ones to cite”.

Stacks 0DM8. For a morphism f : X ⟶ B of algebraic spaces over S which is proper as well as of finite presentation, Hilb_{X/B} ⟶ B satisfies the existence part of the valuative criterion of Morphisms of Spaces, Definition 03IX: every model of the Hilbert presheaf has it for its canonical morphism to B.

This is the source's deduction from Quot, Lemma 0D00 and Lemma 0DM4, both of which are carried as hypotheses because neither is in the library. Lemma 0DM4 is N together with hex: a model of the Quot presheaf of a situation on f whose morphism to B satisfies the existence part. Lemma 0D00 is e together with he: an isomorphism of the Hilbert presheaf with that Quot presheaf, compatible with the two canonical morphisms to B. The source's hypotheses that f be proper and of finite presentation are recorded as _hproper and _hfp; the deduction itself does not consume them, since they enter through Lemma 0DM4, which is carried. The content delivered is the transport: the Quot model is a model of the Hilbert presheaf through e with the same morphism to B, and the existence part is independent of the model.

theorem valuativeCriterionExistence_hilbertPresheafModel_toBase {X : AlgebraicSpaces B S hS}
    (D : QuotSituation B S hS) (f : X ⟶ D.Y)
    (_hproper : IsProper B S hS f.hom) (_hfp : IsFinitePresentation B S hS f.hom)
    (N : QuotSitePresheafModel D) (hex : ValuativeCriterion.Existence N.toBase)
    (e : hilbertPresheaf f ≅ D.quotSitePresheaf)
    (he : e.hom ≫ D.quotSitePresheafToBase = hilbertPresheafToBase f)
    (M : HilbertPresheafModel f) :
    ValuativeCriterion.Existence M.toBase

StacksDraft.GenericFibre.existsUnique_submodule_structureSheaf_flat_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertValuativeExistence.lean, line 261. The attribute's comment: “the affine-chart case over a valuation ring: a closed subscheme of the generic fibre of an affine chart extends uniquely to one flat over the valuation ring, the extension being the generic-kernel ideal; the etale gluing, the proper support and the finite presentation of the glued extension, and hence the valuative criterion itself, are not covered here”. References: EGA IV (2.8.1), “special case”.

Stacks 0DM8 on an affine chart over a valuation ring. Let R be a valuation ring, A an R-algebra — the ring of an affine chart of X — and A_K the generic fibre of A, that is, its localization at the nonzero elements of R. Let P be an ideal of A_K saturated for the nonzero elements of R, that is, the ideal of a closed subscheme of the generic fibre. Then there is exactly one ideal L of A such that A / L is flat over R and the generic fibre of L is P: the closed subscheme of the generic fibre extends uniquely to a closed subscheme of the chart flat over the valuation ring, and the extension is cut out by the generic kernel {x ∈ A | ι x ∈ P}.

This is the case F = 𝒪_X of the chart-wise construction of Lemma 0DM4 — the case Stacks 0DM8 uses, via the identification Hilb_{X/B} = Quot_{𝒪_X/X/B} of Quot, Lemma 0D00, under which a family classified by Hilb_{X/B} is the quotient of the structure sheaf by the ideal of a closed subspace. It is stated with no finiteness condition on the quotient, which for an ideal of A is automatic, so its uniqueness clause is stronger than that of StacksDraft.GenericFibre.existsUnique_submodule_flat_quotient; flatness over R comes from torsion freeness, which is Stacks 0539.

The gluing of these chart-wise extensions, the properness of the support of the glued extension and its finite presentation are not proved — see the implementation notes of StacksFrontier/AlgebraicGeometry/Quot/QuotValuativeAffineChart.lean — so this does not discharge the hypothesis hex of AlgebraicGeometry.Space.valuativeCriterionExistence_hilbertPresheafModel_toBase.

theorem existsUnique_submodule_structureSheaf_flat_quotient
    (hP : ∀ (s : R) {y : AK}, s ≠ 0 → s • y ∈ P → y ∈ P) :
    ∃! L : Submodule A A, Module.Flat R (A ⧸ L) ∧
      Submodule.localized₀ R⁰ (ι.restrictScalars R) (L.restrictScalars R)
        = P.restrictScalars R

AlgebraicGeometry.Space.HilbertPresheafModel.valuativeCriterionExistence_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertValuativeExistenceProper.lean, line 110.

Let f : X ⟶ Y be a morphism of algebraic spaces over S which is proper as well as of finite presentation. Then Hilb_{X/Y} ⟶ Y satisfies the existence part of the valuative criterion (Stacks 03IX): for every model of the Hilbert presheaf of f, its canonical morphism to Y has it.

theorem HilbertPresheafModel.valuativeCriterionExistence_toBase {f : X ⟶ Y}
    (hproper : IsProper B S hS f.hom) (hf : IsFinitePresentation B S hS f.hom)
    (M : HilbertPresheafModel f) : ValuativeCriterion.Existence M.toBase

Tag 0DPE, a lemma

Tag 0DPE in the Stacks Project.

AlgebraicGeometry.Space.hilbertPresheafMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorOpenImmersion.lean, line 431. The attribute's comment: “the induced morphism of Hilbert functors”.

An open immersion π : X ⟶ Y of algebraic spaces over A induces a morphism of Hilbert functors Hilb_{X/A} ⟶ Hilb_{Y/A}, sending a family of closed subspaces of X_T to its image in Y_T.

def hilbertPresheafMap : hilbertPresheaf bX ⟶ hilbertPresheaf bY

AlgebraicGeometry.Space.isOpenImmersion_hilbertModelMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorOpenImmersion.lean, line 552. The attribute's comment: “the induced morphism is an open immersion”.

The morphism of Hilbert functors induced by an open immersion π : X ⟶ Y of algebraic spaces over A, with Y separated over A, is an open immersion, read in any models of the two Hilbert functors.

theorem isOpenImmersion_hilbertModelMap (MX : HilbertPresheafModel bX)
    (MY : HilbertPresheafModel bY) :
    IsOpenImmersion B S hS (hilbertModelMap hπ hopen hsep MX MY)

AlgebraicGeometry.Space.isOpenImmersion_hilbertModelMap_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorOpenImmersionCanonical.lean, line 57. The attribute's comment: “the induced morphism of the canonical Hilbert functors is an open immersion”.

Stacks 0DPE. Let π : X ⟶ Y be an open immersion of algebraic spaces over an algebraic space A, with Y separated over A. Then π induces an open immersion Hilb_{X/A} ⟶ Hilb_{Y/A} of Hilbert functors: the morphism AlgebraicGeometry.Space.hilbertPresheafMap, sending a family Z ⊆ X_T to its image in Y_T, read in the canonical models AlgebraicGeometry.Space.HilbertPresheafModel.canonical of the two Hilbert functors, is an open immersion. Nothing is assumed about the models: they exist for every morphism of algebraic spaces.

theorem isOpenImmersion_hilbertModelMap_canonical (hπ : π ≫ bY = bX)
    (hopen : IsOpenImmersion B S hS π.hom) (hsep : IsSeparated B S hS bY.hom) :
    IsOpenImmersion B S hS (hilbertModelMap hπ hopen hsep (HilbertPresheafModel.canonical bX)
      (HilbertPresheafModel.canonical bY))

Tag 0DPF, a lemma

Tag 0DPF in the Stacks Project.

AlgebraicGeometry.Space.hilbertPresheafMapOfClosed, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorClosedImmersion.lean, line 343. The attribute's comment: “the induced morphism of Hilbert functors”.

A closed immersion π : X ⟶ Y of algebraic spaces over A induces a morphism of Hilbert functors Hilb_{X/A} ⟶ Hilb_{Y/A}, sending a family of closed subspaces of X_T to its image in Y_T.

def hilbertPresheafMapOfClosed : hilbertPresheaf bX ⟶ hilbertPresheaf bY

AlgebraicGeometry.Space.mono_hilbertModelMapOfClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorClosedImmersion.lean, line 413. The attribute's comment: “the induced morphism is a monomorphism”.

The morphism of Hilbert functors induced by a closed immersion over the base is a monomorphism.

theorem mono_hilbertModelMapOfClosed (MX : HilbertPresheafModel bX)
    (MY : HilbertPresheafModel bY) :
    Mono (hilbertModelMapOfClosed hπ hclosed MX MY)

AlgebraicGeometry.Space.isClosedImmersion_hilbertModelMapOfClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorClosedImmersionLocus.lean, line 217. The attribute's comment: “the induced morphism is a closed immersion”.

Let π : X ⟶ Y be a closed immersion of algebraic spaces over an algebraic space A, with Y of finite presentation over A. Then the morphism of Hilbert functors Hilb_{X/A} ⟶ Hilb_{Y/A} that π induces is a closed immersion, read in any models of the two Hilbert functors.

theorem isClosedImmersion_hilbertModelMapOfClosed (hfp : IsFinitePresentation B S hS bY.hom)
    (MX : HilbertPresheafModel bX) (MY : HilbertPresheafModel bY) :
    IsClosedImmersion B S hS (hilbertModelMapOfClosed hπ hclosed MX MY)

AlgebraicGeometry.Space.isClosedImmersion_hilbertModelMapOfClosed_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorClosedImmersionLocus.lean, line 244. The attribute's comment: “the induced morphism of the canonical Hilbert functors is a closed immersion”.

Let π : X ⟶ Y be a closed immersion of algebraic spaces over an algebraic space A, with Y of finite presentation over A. Then π induces a closed immersion Hilb_{X/A} ⟶ Hilb_{Y/A} of Hilbert functors: the morphism AlgebraicGeometry.Space.hilbertPresheafMapOfClosed, sending a family Z ⊆ X_T to its image in Y_T, read in the canonical models AlgebraicGeometry.Space.HilbertPresheafModel.canonical of the two Hilbert functors, is a closed immersion.

theorem isClosedImmersion_hilbertModelMapOfClosed_canonical
    (hfp : IsFinitePresentation B S hS bY.hom) :
    IsClosedImmersion B S hS (hilbertModelMapOfClosed hπ hclosed
      (HilbertPresheafModel.canonical bX) (HilbertPresheafModel.canonical bY))

Tag 0DPG, a remark

Tag 0DPG in the Stacks Project.

AlgebraicGeometry.Space.HilbertEulerData.numericalHilbertFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorNumerical.lean, line 172. The attribute's comment: “the definition of Hilb^P_{X/Y}, as the subfunctor of Hilb_{X/Y} of families whose fibrewise invariants are the prescribed ones; the fibre product Quot_{𝒪_X/X/Y} ×_{Coh_{X/Y}} Coh^P_{X/Y} of Remark 0DP6 and the identification Hilb_{X/Y} = Quot_{𝒪_X/X/Y} of Lemma 0D00 are not available in this development”.

Stacks 0DPG. The functor Hilb^P_{X/Y}: it sends a test scheme T over Y to the set of families classified by Hilb_{X/Y} over T whose fibrewise invariants are the prescribed P, and a morphism of test schemes to base change of those families, which is well defined by AlgebraicGeometry.Space.HilbertEulerData.isPrescribed_baseChange.

This is the source's Hilb^P_{X/Y} = Quot^P_{𝒪_X/X/Y}, formed directly as the subfunctor of the Hilbert functor that the fibre product of Remark 0DP6 computes; that fibre product itself is not available here, since Coh^P_{X/Y} is not constructed in this development.

def numericalHilbertFunctor : (SchemesOverPresheaf B S hS Y)ᵒᵖ ⥤ Type (u + 1)

AlgebraicGeometry.Space.HilbertEulerData.numericalHilbertInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorNumerical.lean, line 194. The attribute's comment: “the morphism Hilb^P_{X/Y} ⟶ Hilb_{X/Y}, proved to be a monomorphism; that it is a flat closed immersion, and an open and closed immersion for I finite, Y locally Noetherian, or I = ℤ with E i = L^{⊗ i}, rests on Lemmas 0DND and 0DNE and is not proved”.

Stacks 0DPG. The morphism Hilb^P_{X/Y} ⟶ Hilb_{X/Y}: a family with the prescribed invariants is in particular a family. The source asserts that this morphism is a flat closed immersion, and an open and closed immersion in three listed cases; neither assertion is proved here, both resting on Lemmas 0DND and 0DNE, which are absent. What is proved is that it is a monomorphism, AlgebraicGeometry.Space.HilbertEulerData.mono_numericalHilbertInclusion.

def numericalHilbertInclusion : χd.numericalHilbertFunctor P ⟶ hilbertFunctor f

AlgebraicGeometry.Space.numericalHilbertSubfunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertNumericalSubfunctor.lean, line 108. The attribute's comment: “the definition of Hilb^P_{X/B} as the subfunctor of Hilb_{X/B} corresponding to Quot^P_{𝒪_X/X/B} = Quot_{𝒪_X/X/B} ×_{Coh_{X/B}} Coh^P_{X/B}, for the actual invariants χ(K_i ⊗^𝐋 κ(t)) of Situation 0DNC”.

Hilb^P_{X/B} = Quot^P_{𝒪_X/X/B}: the subfunctor of the Hilbert presheaf of the families Z ⊆ X_T whose object (T, 𝒪_Z) of Coh_{X/B} lies in Coh^P_{X/B}: for every i ∈ I and every point t of T, χ(K_i ⊗^𝐋 κ(t)) = P(i) with K_i = Rf_{T,*}(E_{i,T} ⊗^𝐋 𝒪_Z). It is the subfunctor that the fibre product Quot_{𝒪_X/X/B} ×_{Coh_{X/B}} Coh^P_{X/B} of Stacks 0DP6 cuts out of Hilb_{X/B} through Stacks 0D00 (AlgebraicGeometry.Space.mem_numericalHilbertSubfunctor_iff_exists_numericalQuot), and a subfunctor because the χ_i are compatible with pullback (Stacks 0A1P).

def numericalHilbertSubfunctor : Subfunctor (hilbertPresheaf f)

AlgebraicGeometry.Space.mem_numericalHilbertSubfunctor_iff_exists_numericalQuot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertNumericalSubfunctor.lean, line 127. The attribute's comment: “Hilb^P_{X/B} = Quot^P_{𝒪_X/X/B}: a family lies in Hilb^P_{X/B} exactly when its quotient, through Hilb_{X/B} = Quot_{𝒪_X/X/B} (0D00), lifts to the 2-fibre product Quot_{𝒪_X/X/B} ×_{Coh_{X/B}} Coh^P_{X/B} of 0DP6”.

A family Z ⊆ X_T lies in Hilb^P_{X/B} exactly when its quotient 𝒪_{X_T} ⟶ 𝒪_Z, the section of Quot_{𝒪_X/X/B} over T it corresponds to under Hilb_{X/B} = Quot_{𝒪_X/X/B} (Stacks 0D00), lifts to the 2-fibre product Quot^P_{𝒪_X/X/B} = Quot_{𝒪_X/X/B} ×_{Coh_{X/B}} Coh^P_{X/B} of Stacks 0DP6 (AlgebraicGeometry.Space.QuotSituation.numericalQuot).

theorem mem_numericalHilbertSubfunctor_iff_exists_numericalQuot {T : (BigFppfOver B S hS)ᵒᵖ}
    (x : (hilbertPresheaf f).obj T) :
    x ∈ (numericalHilbertSubfunctor f hf N).obj T ↔
      ∃ P : (structureSheafQuotSituation f hf).NumericalQuotObjects N,
        P.x = ((hilbertPresheafIsoQuotSitePresheaf f hf).hom.app T x).toQuotObjects

AlgebraicGeometry.Space.relative_closedImmersion_flat_numericalHilbertSubfunctor_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertNumericalSubfunctor.lean, line 139. The attribute's comment: “Hilb^P_{X/B} ⟶ Hilb_{X/B} is a flat closed immersion”.

Hilb^P_{X/B} ⟶ Hilb_{X/B} is a flat closed immersion: its inclusion is representable by morphisms of schemes which are flat closed immersions. This is the base change of Coh^P_{X/B} ⟶ Coh_{X/B}, a flat closed immersion by Stacks 0DND.

theorem relative_closedImmersion_flat_numericalHilbertSubfunctor_ι :
    (MorphismProperty.inverseImage
      (@_root_.AlgebraicGeometry.IsClosedImmersion.{u} ⊓ @Flat.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative uliftYoneda.{u + 1}
        (numericalHilbertSubfunctor f hf N).ι

AlgebraicGeometry.Space.relative_openImmersion_closedImmersion_numericalHilbertSubfunctor_ι_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertNumericalSubfunctor.lean, line 150. The attribute's comment: “for I finite, Hilb^P_{X/B} ⟶ Hilb_{X/B} is an open and closed immersion”.

If I is finite, then Hilb^P_{X/B} ⟶ Hilb_{X/B} is an open and closed immersion.

theorem relative_openImmersion_closedImmersion_numericalHilbertSubfunctor_ι_of_finite
    [Finite N.I] :
    (MorphismProperty.inverseImage
      (@_root_.AlgebraicGeometry.IsOpenImmersion.{u} ⊓
        @_root_.AlgebraicGeometry.IsClosedImmersion.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative uliftYoneda.{u + 1}
        (numericalHilbertSubfunctor f hf N).ι

AlgebraicGeometry.Space.relative_openImmersion_closedImmersion_numericalHilbertSubfunctor_ι_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertNumericalSubfunctor.lean, line 165. The attribute's comment: “for B locally Noetherian, Hilb^P_{X/B} ⟶ Hilb_{X/B} is an open and closed immersion”.

If every scheme étale over B is locally Noetherian (Stacks 03E2), then Hilb^P_{X/B} ⟶ Hilb_{X/B} is an open and closed immersion, whatever the index set.

theorem relative_openImmersion_closedImmersion_numericalHilbertSubfunctor_ι_of_isLocallyNoetherian
    (hY : IsLocallyNoetherian B S hS Y.1) :
    (MorphismProperty.inverseImage
      (@_root_.AlgebraicGeometry.IsOpenImmersion.{u} ⊓
        @_root_.AlgebraicGeometry.IsClosedImmersion.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative uliftYoneda.{u + 1}
        (numericalHilbertSubfunctor f hf N).ι

AlgebraicGeometry.Space.hilbertPolynomialHilbertSubfunctor, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertNumericalSubfunctor.lean, line 193. The attribute's comment: “the notation Hilb^{P, L}_{X/B} for the case I = ℤ, E_n = L^{⊗ n}: the families Z ⊆ X_T with P(n) = χ(X_t, 𝒪_{Z_t} ⊗ L_t^{⊗ n}) for all n and t, the inverse image of Quot^{P, L}_{𝒪_X/X/B} under Hilb_{X/B} = Quot_{𝒪_X/X/B}”.

Hilb^{P, 𝓛}_{X/B}: the case I = ℤ, E_n = 𝓛^{⊗ n} for an invertible 𝒪_X-module 𝓛, the subfunctor of the Hilbert presheaf of the families Z ⊆ X_T whose object (T, 𝒪_Z) lies in Coh^{P, 𝓛}_{X/B} of Stacks 0DNF: P(n) = χ(X_t, 𝒪_{Z_t} ⊗ 𝓛_t^{⊗ n}) for every n ∈ ℤ and every point t of T. It is the inverse image of Quot^{P, 𝓛}_{𝒪_X/X/B} under Hilb_{X/B} = Quot_{𝒪_X/X/B} (Stacks 0D00).

alias hilbertPolynomialHilbertSubfunctor

AlgebraicGeometry.Space.relative_openImmersion_closedImmersion_hilbertPolynomialHilbertSubfunctor_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertNumericalSubfunctor.lean, line 210. The attribute's comment: “for I = ℤ and E_n = L^{⊗ n}, Hilb^{P, L}_{X/B} ⟶ Hilb_{X/B} is an open and closed immersion”.

In the case I = ℤ, E_n = 𝓛^{⊗ n}, Hilb^{P, 𝓛}_{X/B} ⟶ Hilb_{X/B} is an open and closed immersion, the base change of the open and closed substack Coh^{P, 𝓛}_{X/B} ⊆ Coh_{X/B} of Stacks 0DNF.

theorem relative_openImmersion_closedImmersion_hilbertPolynomialHilbertSubfunctor_ι :
    (MorphismProperty.inverseImage
      (@_root_.AlgebraicGeometry.IsOpenImmersion.{u} ⊓
        @_root_.AlgebraicGeometry.IsClosedImmersion.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative uliftYoneda.{u + 1}
        (hilbertPolynomialHilbertSubfunctor f hf L P).ι

Tag 0DPH, a lemma

Tag 0DPH in the Stacks Project.

AlgebraicGeometry.Space.exists_hilbertPolynomialHilbert_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertPolynomialHilbertProper.lean, line 88.

Let f : X ⟶ Y be a proper morphism of finite presentation of algebraic spaces (over Spec ℤ), L an invertible 𝒪_X-module ample on X/Y (Stacks 0D31) and P a numerical polynomial. Then the algebraic space Hilb^P_{X/Y} parametrizing closed subschemes having Hilbert polynomial P with respect to L is proper over Y: the subfunctor Hilb^{P, L}_{X/Y} of the Hilbert presheaf has a model M in the universe of the site, identified with it over Y, which is an algebraic space whose morphism to Y is proper.

theorem exists_hilbertPolynomialHilbert_isProper
    {X Y : AlgebraicSpaces B integerBase B.contains_integerBase} (f : X ⟶ Y)
    (hprop : IsProper B integerBase B.contains_integerBase f.hom)
    (hf : IsFinitePresentation B integerBase B.contains_integerBase f.hom)
    (L : Modules.{u, u} B integerBase B.contains_integerBase X.1 X.2)
    [hL : Stacks.SheafOfModules.IsInvertible
      (structurePresheaf B integerBase B.contains_integerBase X.1)
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B integerBase B.contains_integerBase X.1 X.2).O)).property L]
    (hamp : IsRelativelyAmple B integerBase B.contains_integerBase f L)
    {P : ℤ → ℤ} {p : Polynomial ℚ} (hP : ∀ m : ℤ, p.eval (m : ℚ) = (P m : ℚ)) :
    ∃ (M : (BigFppfOver B integerBase B.contains_integerBase)ᵒᵖ ⥤ Type u)
      (e : M ⋙ uliftFunctor.{u + 1, u} ≅ (hilbertPolynomialHilbert f hf L P).toFunctor)
      (q : M ⟶ Y.obj),
      Functor.whiskerRight q uliftFunctor.{u + 1, u} =
          e.hom ≫ (hilbertPolynomialHilbert f hf L P).ι ≫ hilbertPresheafToBase f ∧
        IsAlgebraicSpace B integerBase B.contains_integerBase M ∧
        IsProper B integerBase B.contains_integerBase q

Tag 0DPI, a lemma

Tag 0DPI in the Stacks Project.

AlgebraicGeometry.Space.exists_hilbertPolynomialHilbert_isSeparated_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertPolynomialHilbertSeparatedFinitePresentation.lean, line 65.

Let f : X ⟶ Y be a separated morphism of finite presentation of algebraic spaces (over Spec ℤ), L an invertible 𝒪_X-module ample on X/Y (Stacks 0D31) and P a numerical polynomial. Then the algebraic space Hilb^P_{X/Y} parametrizing closed subschemes having Hilbert polynomial P with respect to L is separated and of finite presentation over Y: the subfunctor Hilb^{P, L}_{X/Y} of the Hilbert presheaf has a model M in the universe of the site, identified with it over Y, which is an algebraic space whose morphism to Y is separated and of finite presentation.

theorem exists_hilbertPolynomialHilbert_isSeparated_isFinitePresentation
    {X Y : AlgebraicSpaces B integerBase B.contains_integerBase} (f : X ⟶ Y)
    (hsep : IsSeparated B integerBase B.contains_integerBase f.hom)
    (hf : IsFinitePresentation B integerBase B.contains_integerBase f.hom)
    (L : Modules.{u, u} B integerBase B.contains_integerBase X.1 X.2)
    [hL : Stacks.SheafOfModules.IsInvertible
      (structurePresheaf B integerBase B.contains_integerBase X.1)
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B integerBase B.contains_integerBase X.1 X.2).O)).property L]
    (hamp : IsRelativelyAmple B integerBase B.contains_integerBase f L)
    {P : ℤ → ℤ} {p : Polynomial ℚ} (hP : ∀ m : ℤ, p.eval (m : ℚ) = (P m : ℚ)) :
    ∃ (M : (BigFppfOver B integerBase B.contains_integerBase)ᵒᵖ ⥤ Type u)
      (e : M ⋙ uliftFunctor.{u + 1, u} ≅ (hilbertPolynomialHilbert f hf L P).toFunctor)
      (q : M ⟶ Y.obj),
      Functor.whiskerRight q uliftFunctor.{u + 1, u} =
          e.hom ≫ (hilbertPolynomialHilbert f hf L P).ι ≫ hilbertPresheafToBase f ∧
        IsAlgebraicSpace B integerBase B.contains_integerBase M ∧
        IsSeparated B integerBase B.contains_integerBase q ∧
        IsFinitePresentation B integerBase B.contains_integerBase q

Sources

• Section 108.7, Tag 0DM5
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.diagonal_hilbertPresheafToBase · AlgebraicGeometry.Space.HilbertPresheafModel.isSeparated_and_isLocallyOfFinitePresentation_toBase · AlgebraicGeometry.Space.valuativeCriterionExistence_hilbertPresheafModel_toBase · StacksDraft.GenericFibre.existsUnique_submodule_structureSheaf_flat_quotient · AlgebraicGeometry.Space.HilbertPresheafModel.valuativeCriterionExistence_toBase · AlgebraicGeometry.Space.hilbertPresheafMap · AlgebraicGeometry.Space.isOpenImmersion_hilbertModelMap · AlgebraicGeometry.Space.isOpenImmersion_hilbertModelMap_canonical

Section108.8 Properties of the Picard stack#

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

Tag 0DMA, a lemma

Tag 0DMA in the Stacks Project.

AlgebraicGeometry.Space.picardRelativeDiagonal_affine_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackDiagonal.lean, line 167.

Let f : X ⟶ B be a morphism of algebraic spaces over S which is flat, proper and of finite presentation (finite presentation is part of the standing data D). The diagonal of Picardstack_{X/B} over B is affine and of finite presentation: the relative diagonal of the structure morphism Picardstack_{X/B} ⟶ 𝒮_B is representable by algebraic spaces (Stacks 02ZW), and every algebraic space representing one of its base changes along a scheme-valued point over U is affine and of finite presentation over U (Properties of Stacks, Section 04XB).

theorem picardRelativeDiagonal_affine_finitePresentation
    (D : CoherentSituation B S hS) (hflat : IsFlat B S hS D.f.hom)
    (hproper : IsProper B S hS D.f.hom) :
    letI π := picardToBase (modulePushforwardCoherence B S hS) D.toPicardSituation
    ∃ _hrep : Stack.IsRepresentableByAlgebraicSpaces B S hS
        (Stack.relativeDiagonal.{u, u + 1, u + 1} B S hS _ _ π).hom,
      ∀ (U : BigFppfOver B S hS)
        (z : BigFppfOver B U.left.1 U.left.2 ⥤
          (Stack.twoFibreProduct B S hS (baseCFG D.Y) _ _ π.hom π.hom).val.obj)
        (_hz : z ⋙ (Stack.twoFibreProduct B S hS (baseCFG D.Y) _ _ π.hom π.hom).val.p =
          Over.map U.hom)
        (F : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hF : IsAlgebraicSpace B U.left.1 U.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom)
            (picardCFG (modulePushforwardCoherence B S hS) D.toPicardSituation).val.p
            (Stack.twoFibreProduct B S hS (baseCFG D.Y) _ _ π.hom π.hom).val.p z
            (CatFiberedInGroupoids.homFunctor
              (Stack.relativeDiagonal.{u, u + 1, u + 1} B S hS _ _ π)))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        IsAffineHom B S hS (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom ∧
          IsFinitePresentation B S hS (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom

Tag 0DMB, a lemma

Tag 0DMB in the Stacks Project.

AlgebraicGeometry.Space.PicardOverBase.quasiSeparated_limitPreservingOnObjects_picardToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackQuasiSeparatedLimitPreserving.lean, line 63. The attribute's comment: “quasi-separated: the relative diagonal is representable by algebraic spaces, quasi-compact and quasi-separated; locally of finite presentation: limit preserving on objects”.

Let f : X ⟶ B be a morphism of algebraic spaces over S which is flat, proper and of finite presentation. Then the structure morphism Picardstack_{X/B} ⟶ 𝒮_B is quasi-separated, i.e. its relative diagonal is representable by algebraic spaces, quasi-compact and quasi-separated (Stacks 04YW, 04XB), and locally of finite presentation in the sense of categories fibred in groupoids, i.e. limit preserving on objects (Stacks 06CU; for a 1-morphism of algebraic stacks this is local finite presentation, Stacks 0CMY).

theorem quasiSeparated_limitPreservingOnObjects_picardToBase
    (s : PicardSituation B S hS) (hfp : IsFinitePresentation B S hS s.f.hom)
    (hflat : IsFlat B S hS s.f.hom) (hproper : IsProper B S hS s.f.hom) :
    (∃ _ : Stack.IsRepresentableByAlgebraicSpaces B S hS
        (Stack.relativeDiagonal.{u, u + 1, u + 1} B S hS _ _
          (picardToBase (modulePushforwardCoherence B S hS) s)).hom,
      Stack.IsQuasiCompact B S hS
          (Stack.relativeDiagonal.{u, u + 1, u + 1} B S hS _ _
            (picardToBase (modulePushforwardCoherence B S hS) s)) ∧
        Stack.IsQuasiSeparated B S hS
          (Stack.relativeDiagonal.{u, u + 1, u + 1} B S hS _ _
            (picardToBase (modulePushforwardCoherence B S hS) s))) ∧
      BigFppfOver.IsLimitPreservingOnObjects.{u, u, u} B S hS _ _
        (picardToBase (modulePushforwardCoherence B S hS) s)

Tag 0DNG, a lemma

Tag 0DNG in the Stacks Project.

AlgebraicGeometry.Space.liftedValuativeCriterionExistence_picardToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackValuativeExistence.lean, line 70.

Let f : X ⟶ B be a morphism of algebraic spaces over S which is proper, of finite presentation and smooth. Then the structure morphism Picardstack_{X/B} ⟶ B satisfies the existence part of the valuative criterion (Stacks 0CLK).

theorem liftedValuativeCriterionExistence_picardToBase (s : PicardSituation B S hS)
    (hfp : IsFinitePresentation B S hS s.f.hom) (hproper : IsProper B S hS s.f.hom)
    (hsmooth : IsSmooth B S hS s.f.hom) :
    Stack.LiftedValuativeCriterion.Existence.{u, u + 1} B S hS
      (picardToBase (modulePushforwardCoherence B S hS) s)

Tag 0DNH, a lemma

Tag 0DNH in the Stacks Project.

AlgebraicGeometry.Space.picardInertiaEquivalenceOverMultiplicativeGroupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackInertia.lean, line 828. The attribute's comment: “the inertia stack of the Picard stack is 𝐆_{m,S} ×_S Picardstack_{X/B}, as categories over the big fppf site, when 𝒪_T ⟶ f_{T,*}𝒪_{X_T} is an isomorphism for every scheme T over the base”.

Let f : X ⟶ B be a morphism of algebraic spaces over S, and assume that for every scheme T over B the structure map 𝒪_T ⟶ f_{T, *}𝒪_{X_T} of the base change f_T : X_T ⟶ T is an isomorphism. Then the inertia stack of the Picard stack Picardstack_{X/B} of Section 0372 is equal to 𝐆_{m, S} ×_S Picardstack_{X/B}: this is an equivalence of the two over (Sch/S)_fppf, which is the identity on the Picardstack_{X/B}-factor and sends a point (L, α) of the inertia over T to the point of 𝐆_{m, S}(T) = H^0(T, 𝒪_T^*) that the automorphism α of L is multiplication by.

The hypothesis h reads the source's f_{T, *}𝒪_{X_T} ≅ 𝒪_T, as in Stacks 0375, as the canonical map 𝒪_T ⟶ f_{T, *}𝒪_{X_T} being an isomorphism for every test scheme over the base. The category Picardstack_{X/B} is AlgebraicGeometry.Space.picardCategoryData, with the comparisons of inverse images of Stacks 03LU given by AlgebraicGeometry.Space.modulePushforwardCoherence. The standing assumptions of the section that f be flat, proper and of finite presentation are not needed.

"Equal" is read as an equivalence over the site (CategoryTheory.StacksRepresentableCFG.EquivalenceOver), and the product is the 2-fibre product CategoryTheory.inertiaPresheafProduct of the category of elements of 𝐆_{m, S} with Picardstack_{X/B} over the site.

def picardInertiaEquivalenceOverMultiplicativeGroupProduct (s : PicardSituation B S hS)
    (h : s.StructureSheafMapIso) :
    letI : Category.{u + 1} (PicardObject s) :=
      (picardCategoryData (modulePushforwardCoherence B S hS) s).category
    StacksRepresentableCFG.EquivalenceOver
      (relativeInertiaStruct
        (picardCategoryData (modulePushforwardCoherence B S hS) s).siteProjection
        (picardCategoryData (modulePushforwardCoherence B S hS) s).siteProjection)
      (inertiaPresheafProductStruct
        (picardCategoryData (modulePushforwardCoherence B S hS) s).siteProjection
        (multiplicativeGroupPresheaf B S hS))

Tag 0DPJ, a lemma

Tag 0DPJ in the Stacks Project.

AlgebraicGeometry.Space.isSmooth_picardStructureMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackSmoothRegistered.lean, line 46. The attribute's comment: “the full statement: f flat (hflat), proper (hproper), of finite presentation (the field of D) and of relative dimension ≤ 1 (hd); Picardstack_{X/B} → B is smooth; the algebraicity of Picardstack_{X/B} is Stacks 0D04, proved, not assumed”.

Stacks 0DPJ: the Picard stack is smooth in relative dimension ≤ 1. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is flat, proper, of finite presentation (a field of the standing datum D) and of relative dimension ≤ 1. Then the structure morphism Picardstack_{X/Y} ⟶ Y is smooth, as a 1-morphism of algebraic stacks; the Picard stack is algebraic by Stacks 0D04.

theorem isSmooth_picardStructureMorphism (D : CoherentSituation B S hS)
    (hflat : IsFlat B S hS D.f.hom) (hproper : IsProper B S hS D.f.hom)
    (hd : HasRelativeDimensionLE 1 B S hS D.f.hom) :
    Stack.AlgebraicStacks.IsSmooth B S hS
      (picardStructureMorphism D (isAlgebraicStack_picardCFG.{u, w} D hflat hproper))

Sources

• Section 108.8, Tag 0DM9
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.picardRelativeDiagonal_affine_finitePresentation · AlgebraicGeometry.Space.PicardOverBase.quasiSeparated_limitPreservingOnObjects_picardToBase · AlgebraicGeometry.Space.liftedValuativeCriterionExistence_picardToBase · AlgebraicGeometry.Space.picardInertiaEquivalenceOverMultiplicativeGroupProduct · AlgebraicGeometry.Space.isSmooth_picardStructureMorphism

Section108.9 Properties of the Picard functor#

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

Tag 0DME, a lemma

Tag 0DME in the Stacks Project.

AlgebraicGeometry.Space.PicardSituation.isGerbeOver_toPicardFunctorBased, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackGerbe.lean, line 270.

In Situation 0D25 — a morphism f : X ⟶ B of algebraic spaces over S — the morphism Picardstack_{X/B} ⟶ Pic_{X/B}, sending an object (U, b, L) to the element of Pic_{X/B}(U, b) named by the class of L, turns the Picard stack into a gerbe over the Picard functor: it satisfies the two conditions of Stacks 06P2 (conditions (2)(a) and (2)(b) of Stacks 06P1) over the big fppf site of S, which is the condition of Stacks 06QC.

The section's assumptions on f (flat, proper, of finite presentation, with 𝒪_T ≅ f_{T,*}𝒪_{X_T} for every T) are not assumed.

theorem isGerbeOver_toPicardFunctorBased :
    IsGerbeOver (BigFppfOver.topology B S hS) s.picardFunctorBasedCategory.p
      s.toPicardFunctorBased.toFunctor

Tag 0DMF, a lemma

Tag 0DMF in the Stacks Project.

AlgebraicGeometry.Space.PicardSituation.isImmersion_and_isQuasiCompact_diagonal_of_iso_picardFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardFunctorDiagonalQuasiCompactImmersion.lean, line 59.

Let f : X ⟶ B be a morphism of algebraic spaces over S which is flat, proper and of finite presentation, such that 𝒪_T ⟶ f_{T,*}𝒪_{X_T} is an isomorphism for every scheme T over B, and let p : H ⟶ B be an algebraic space over B whose functor of points over B is identified (c) with the relative Picard functor Pic_{X/B} (such an H exists by Stacks 0D2C, AlgebraicGeometry.Space.isAlgebraicSpaceOver_picardFunctor). Then the diagonal H ⟶ H ×_B H of Pic_{X/B} over B is a quasi-compact immersion.

theorem isImmersion_and_isQuasiCompact_diagonal_of_iso_picardFunctor
    {s : PicardSituation B S hS} (hflat : IsFlat B S hS s.f.hom)
    (hfp : IsFinitePresentation B S hS s.f.hom) (hproper : IsProper B S hS s.f.hom)
    (h : s.StructureSheafMapIso) {H : AlgebraicSpaces B S hS} {p : H ⟶ s.base}
    (c : spacePointsOver p ⋙ uliftFunctor.{u + 1, u} ≅ s.picardFunctor) :
    IsImmersion B S hS (pullback.diagonal p.hom) ∧
      IsQuasiCompact B S hS (pullback.diagonal p.hom)

Tag 0DNI, a lemma

Tag 0DNI in the Stacks Project.

AlgebraicGeometry.Space.PicardSituation.isQuasiSeparated_and_isLocallyOfFinitePresentation_of_represents_picardFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardFunctorRepresentingSpace.lean, line 62. The attribute's comment: “Stated for every algebraic space representing Pic_{X/B}, i.e. with an identification c of its points over B with Pic_{X/B}, since Section 0DMD presupposes that Pic_{X/B} is an algebraic space (Stacks 0D2C); with Pic_{X/B} itself as that space this is the lemma as printed. The cohomological-flatness condition O_T -> f_{T,*}O_{X_T} iso of the section is dropped: f flat, proper and of finite presentation suffices.”.

Let f : X ⟶ B be a flat, proper morphism of finite presentation of algebraic spaces, and let p : H ⟶ B be an algebraic space over B whose functor of points over B is identified (c) with the relative Picard functor Pic_{X/B}. Then p is quasi-separated and locally of finite presentation.

theorem isQuasiSeparated_and_isLocallyOfFinitePresentation_of_represents_picardFunctor
    (c : spacePointsOver p ⋙ uliftFunctor.{u + 1, u} ≅ s.picardFunctor)
    (hflat : IsFlat B S hS s.f.hom) (hfp : IsFinitePresentation B S hS s.f.hom)
    (hproper : IsProper B S hS s.f.hom) :
    IsQuasiSeparated B S hS p.hom ∧ Space.IsLocallyOfFinitePresentation B S hS p.hom

Tag 0DNJ, a lemma

Tag 0DNJ in the Stacks Project.

AlgebraicGeometry.Space.PicardSituation.isSeparated_of_represents_picardFunctor_of_hasIntegralGeometricFibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardFunctorRepresentingSpace.lean, line 78. The attribute's comment: “Stated for every algebraic space representing Pic_{X/B}, i.e. with an identification c of its points over B with Pic_{X/B}, since Section 0DMD presupposes that Pic_{X/B} is an algebraic space (Stacks 0D2C); with Pic_{X/B} itself as that space this is the lemma as printed.”.

Let f : X ⟶ B be a flat, proper morphism of finite presentation of algebraic spaces with 𝒪_T ≅ f_{T,*}𝒪_{X_T} for every scheme T over B, whose geometric fibres are integral, and let p : H ⟶ B be an algebraic space over B whose functor of points over B is identified (c) with the relative Picard functor Pic_{X/B}. Then p is separated.

theorem isSeparated_of_represents_picardFunctor_of_hasIntegralGeometricFibres
    (c : spacePointsOver p ⋙ uliftFunctor.{u + 1, u} ≅ s.picardFunctor)
    (hflat : IsFlat B S hS s.f.hom) (hfp : IsFinitePresentation B S hS s.f.hom)
    (hproper : IsProper B S hS s.f.hom) (hstein : s.StructureSheafMapIso)
    (hgeom : HasIntegralGeometricFibres B S hS s.f.hom) :
    IsSeparated B S hS p.hom

Tag 0DPK, a lemma

Tag 0DPK in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpaceOver_and_isSmooth_picardFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardFunctorSmooth.lean, line 208. The attribute's comment: “the full statement, in the setting of Section 0DMD: f flat (hflat), of finite presentation (hfp), proper (hproper), O_T -> f_{T,*}O_{X_T} an isomorphism for every T (hstr), of relative dimension ≤ 1 (hd); the conclusion contains that Pic_{X/B} is an algebraic space over B (Stacks 0D2C) and that its morphism to B is smooth, for every algebraic space representing it”.

The Picard functor is smooth in relative dimension ≤ 1. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is flat, of finite presentation and proper, with 𝒪_T ⟶ f_{T,*}𝒪_{X_T} an isomorphism for every scheme T over Y (the standing assumptions of Section 0DMD), and of relative dimension ≤ 1. Then Pic_{X/Y} is an algebraic space over Y (Stacks 0D2C) and Pic_{X/Y} ⟶ Y is smooth: every algebraic space H with a morphism p : H ⟶ Y whose functor of points over Y is identified with Pic_{X/Y} has p smooth.

theorem isAlgebraicSpaceOver_and_isSmooth_picardFunctor {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hflat : IsFlat B S hS f.hom) (hfp : IsFinitePresentation B S hS f.hom)
    (hproper : IsProper B S hS f.hom)
    (hstr : (PicardSituation.mk X Y f).StructureSheafMapIso)
    (hd : HasRelativeDimensionLE 1 B S hS f.hom) :
    IsAlgebraicSpaceOver (PicardSituation.mk X Y f).picardFunctor ∧
      ∀ (H : AlgebraicSpaces B S hS) (p : H ⟶ Y),
        Nonempty (spacePointsOver p ⋙ uliftFunctor.{u + 1, u} ≅
          (PicardSituation.mk X Y f).picardFunctor) →
        IsSmooth B S hS p.hom

Sources

• Section 108.9, Tag 0DMD
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.PicardSituation.isGerbeOver_toPicardFunctorBased · AlgebraicGeometry.Space.PicardSituation.isImmersion_and_isQuasiCompact_diagonal_of_iso_picardFunctor · AlgebraicGeometry.Space.PicardSituation.isQuasiSeparated_and_isLocallyOfFinitePresentation_of_represents_picardFunctor · AlgebraicGeometry.Space.PicardSituation.isSeparated_of_represents_picardFunctor_of_hasIntegralGeometricFibres · AlgebraicGeometry.Space.isAlgebraicSpaceOver_and_isSmooth_picardFunctor

Section108.10 Properties of relative morphisms#

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

Tag 0DPM, a lemma

Tag 0DPM in the Stacks Project.

AlgebraicGeometry.Space.diagonal_relativeHomProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeMorphismDiagonal.lean, line 94.

Stacks 0DPM. The diagonal of Mor_B(Y, X) ⟶ B is a closed immersion of finite presentation, for Y ⟶ B flat, proper and of finite presentation and X ⟶ B separated and of finite presentation: it is representable by closed immersions of schemes locally of finite presentation.

theorem diagonal_relativeHomProjection (hsep : IsSeparated B S hS x)
    (hxfp : IsFinitePresentation B S hS x) (hfp : IsFinitePresentation B S hS z)
    (hflat : IsFlat B S hS z) (hproper : IsProper B S hS z) :
    (closedImmersionFinitePresentation (B := B) (S := S) (hS := hS)).presheaf
      (pullback.diagonal (relativeHomProjection B S hS Z X Q z x hZ hX hQ))

Tag 0DPN, a lemma

Tag 0DPN in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_and_isLocallyOfFinitePresentation_relativeHomProjection_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeMorphismSeparatedFinitePresentationUnconditional.lean, line 56.

Stacks 0DPN. Let Q be an algebraic space, z : Z ⟶ Q flat, proper and of finite presentation and x : X ⟶ Q separated and of finite presentation, all algebraic spaces over S. Then the projection Mor_Q(Z, X) ⟶ Q of the relative morphism functor is separated (its diagonal is a closed immersion, Stacks 0DPM) and locally of finite presentation.

theorem isSeparated_and_isLocallyOfFinitePresentation_relativeHomProjection_unconditional
    (hsep : IsSeparated B S hS x) (hxfp : IsFinitePresentation B S hS x)
    (hfp : IsFinitePresentation B S hS z) (hflat : IsFlat B S hS z)
    (hproper : IsProper B S hS z) :
    IsSeparated B S hS (relativeHomProjection B S hS Z X Q z x hZ hX hQ) ∧
      IsLocallyOfFinitePresentation B S hS (relativeHomProjection B S hS Z X Q z x hZ hX hQ)

Tag 0DPP, a lemma

Tag 0DPP in the Stacks Project.

AlgebraicGeometry.Space.isomSubfunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/IsomorphismLocusInRelativeMorphisms.lean, line 290. The attribute's comment: “the subfunctor Isom_B(Y, X) of Mor_B(Y, X) of isomorphisms”.

Stacks 0DPP, the subfunctor Isom_Q(Z, X) ⊆ Mor_Q(Z, X) of relative isomorphisms: its sections over a scheme T are the pairs (a, b) of Stacks 05Y1 at T whose morphism of base changes Z_T ⟶ X_T is an isomorphism.

This is a subfunctor because the restriction maps of Mor_Q(Z, X) are restriction of pairs (AlgebraicGeometry.Space.relativeHomSections_map) and a restriction of a relative isomorphism is a relative isomorphism.

def isomSubfunctor : Subfunctor (relativeHom B S hS Z X Q z x hZ hX hQ)

AlgebraicGeometry.Space.isOpenSubspace_isomSubfunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/IsomorphismLocusInRelativeMorphisms.lean, line 322. The attribute's comment: “openness of the subfunctor of isomorphisms”.

Stacks 0DPP. With Z ⟶ Q flat, proper and of finite presentation and X ⟶ Q proper, the subfunctor Isom_Q(Z, X) ⊆ Mor_Q(Z, X) of relative isomorphisms is an open subspace.

This is the isomorphism locus of Stacks 05XD applied to the universal relative morphism, the pair corresponding to the identity of Mor_Q(Z, X) under the bijection of Stacks 05Y3: the source of that morphism is flat, locally of finite presentation and universally closed over Mor_Q(Z, X) and its target is separated, locally of finite type and closed over Mor_Q(Z, X), both being base changes. A morphism from a scheme T factors through the locus exactly when the base change of the universal morphism along it is an isomorphism, which is the condition cutting out Isom_Q(Z, X), so the locus is Isom_Q(Z, X).

The algebraicity hM of Mor_Q(Z, X) is an explicit hypothesis: it is Stacks 0D1C, the standing fact of the source's section, and the conclusion cannot do without it, because an open subspace is in particular an algebraic space and the finite presentation and separatedness hypotheses on x of the source's section enter the statement only through it.

theorem isOpenSubspace_isomSubfunctor (hzfp : IsFinitePresentation B S hS z)
    (hzflat : IsFlat B S hS z) (hzproper : IsProper B S hS z) (hxproper : IsProper B S hS x)
    (hM : IsAlgebraicSpace B S hS (relativeHom B S hS Z X Q z x hZ hX hQ)) :
    IsOpenSubspace B S hS (isomSubfunctor B S hS Z X Q z x hZ hX hQ)

AlgebraicGeometry.Space.isOpenSubspace_isomSubfunctor_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/IsomorphismLocusUnconditional.lean, line 59. The attribute's comment: “the subfunctor Isom_B(Y, X) of Mor_B(Y, X) of isomorphisms is an open subspace, for Y ⟶ B flat, proper and of finite presentation and X ⟶ B proper and of finite presentation”.

Let Q be an algebraic space and z : Z ⟶ Q, x : X ⟶ Q morphisms of algebraic spaces over S with z flat, proper and of finite presentation and x proper and of finite presentation (in particular separated, as in the standing data of Stacks 0DPL). Then the subfunctor Isom_Q(Z, X) ⊆ Mor_Q(Z, X) of isomorphisms is an open subspace.

theorem isOpenSubspace_isomSubfunctor_of_isFinitePresentation
    (hx_fp : IsFinitePresentation B S hS x) (hx_proper : IsProper B S hS x)
    (hz_fp : IsFinitePresentation B S hS z) (hz_flat : IsFlat B S hS z)
    (hz_proper : IsProper B S hS z) :
    IsOpenSubspace B S hS (isomSubfunctor B S hS Z X Q z x hZ hX hQ)

Tag 0DPQ, a remark

Tag 0DPQ in the Stacks Project.

AlgebraicGeometry.Space.numericalRelativeHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalRelativeMorphisms.lean, line 320. The attribute's comment: “the definition of Mor^P_B(Y, X) as the subfunctor of Mor_B(Y, X) of relative morphisms whose graph has the prescribed invariants, with the open subspace of a test scheme that tests the source's open immersion for a finite index set; that Mor^P_B(Y, X) ⟶ Mor_B(Y, X) is a flat closed immersion rests on Lemmas 0DND and 0DNE, which are assertions about a morphism of algebraic stacks and are unavailable in this development, and is not stated”.

Stacks 0DPQ, the subfunctor Mor^P_Q(Z, X) ⊆ Mor_Q(Z, X): its sections over a scheme T are the pairs (a, b) of Stacks 05Y1 at T whose graph, a point of Hilb_{Z ×_Q X / Q} over T by Stacks 0D1A, has the prescribed invariants. Since the graph transformation is the inclusion Mor_Q(Z, X) ⊆ Hilb_{Z ×_Q X / Q} of Stacks 0D1B, this is the intersection Mor_Q(Z, X) ∩ Hilb^P_{Z ×_Q X / Q} of the source, formed as an inverse image.

This is a subfunctor because the restriction maps of Mor_Q(Z, X) go to base change of graphs and the condition on the invariants is stable under base change.

def numericalRelativeHom : Subfunctor (relativeHom B S hS Z X Q z x hZ hX hQ)

AlgebraicGeometry.Space.numericalSituationRelativeHom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalRelativeMorphismsClopen.lean, line 173. The attribute's comment: “the definition Mor^P_B(Y, X) = Mor_B(Y, X) ∩ Hilb^P_{Y ×_B X/B}, for the numerical invariants χ(K_i ⊗^𝐋 κ(t)) of Situation 0DNC on Y ×_B X ⟶ B”.

The subfunctor Mor^P_Q(Z, X) = Mor_Q(Z, X) ∩ Hilb^P_{Z ×_Q X / Q}. For the standing data N of Situation 0DNC on Z ×_Q X ⟶ Q (a set I, perfect objects E_i of D(𝒪_{Z ×_Q X}) and P : I → ℤ), the subfunctor of Mor_Q(Z, X) of the relative morphisms over T whose graph W, a point of Hilb_{Z ×_Q X / Q} by Stacks 0D1A and 0D1B, lies in Hilb^P_{Z ×_Q X / Q} of Stacks 0DPG: χ(K_i ⊗^𝐋 κ(t)) = P(i) for K_i = Rf_{T,*}(E_{i,T} ⊗^𝐋 𝒪_W), every i ∈ I and every point t of T.

abbrev numericalSituationRelativeHom : Subfunctor (relativeHom B S hS Z X Q z x hZ hX hQ)

AlgebraicGeometry.Space.isFlat_and_isClosedImmersion_numericalSituationRelativeHom_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalRelativeMorphismsClopen.lean, line 222. The attribute's comment: “Mor^P_B(Y, X) ⟶ Mor_B(Y, X) is a flat closed immersion”.

The morphism Mor^P_Q(Z, X) ⟶ Mor_Q(Z, X) is a flat closed immersion.

theorem isFlat_and_isClosedImmersion_numericalSituationRelativeHom_ι :
    IsFlat B S hS (numericalSituationRelativeHom B S hS hsep hx_fp hfp hflat hproper N).ι ∧
      IsClosedImmersion B S hS
        (numericalSituationRelativeHom B S hS hsep hx_fp hfp hflat hproper N).ι

AlgebraicGeometry.Space.isOpenImmersion_and_isClosedImmersion_numericalSituationRelativeHom_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalRelativeMorphismsClopen.lean, line 232. The attribute's comment: “for I finite, Mor^P_B(Y, X) ⟶ Mor_B(Y, X) is an open and closed immersion”.

For I finite the morphism Mor^P_Q(Z, X) ⟶ Mor_Q(Z, X) is an open and closed immersion.

theorem isOpenImmersion_and_isClosedImmersion_numericalSituationRelativeHom_ι [Finite N.I] :
    IsOpenImmersion B S hS (numericalSituationRelativeHom B S hS hsep hx_fp hfp hflat hproper N).ι ∧
      IsClosedImmersion B S hS
        (numericalSituationRelativeHom B S hS hsep hx_fp hfp hflat hproper N).ι

AlgebraicGeometry.Space.isOpenImmersion_and_isClosedImmersion_numericalSituationRelativeHom_ι_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalRelativeMorphismsClopen.lean, line 244. The attribute's comment: “for B locally Noetherian, Mor^P_B(Y, X) ⟶ Mor_B(Y, X) is an open and closed immersion, for an arbitrary index set I”.

If Q is locally Noetherian, then for any index set I the morphism Mor^P_Q(Z, X) ⟶ Mor_Q(Z, X) is an open and closed immersion.

theorem isOpenImmersion_and_isClosedImmersion_numericalSituationRelativeHom_ι_of_isLocallyNoetherian
    (hQN : IsLocallyNoetherian B S hS Q) :
    IsOpenImmersion B S hS (numericalSituationRelativeHom B S hS hsep hx_fp hfp hflat hproper N).ι ∧
      IsClosedImmersion B S hS
        (numericalSituationRelativeHom B S hS hsep hx_fp hfp hflat hproper N).ι

AlgebraicGeometry.Space.hilbertPolynomialSituationRelativeHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalRelativeMorphismsClopen.lean, line 301. The attribute's comment: “the notation Mor^{P, L}_B(Y, X): Mor^P_B(Y, X) for I = ℤ and E_i = L^{⊗ i}, the relative morphisms whose graph W has χ((Y ×_B X)_t, 𝒪_{W_t} ⊗ L_t^{⊗ i}) = P(i) for all i and t”.

The subfunctor Mor^{P, L}_Q(Z, X): Mor^P_Q(Z, X) for I = ℤ and E_n = L^{⊗ n}, an invertible 𝒪_{Z ×_Q X}-module L. Its sections over T are the relative morphisms whose graph W ⊆ (Z ×_Q X)_T has χ((Z ×_Q X)_t, 𝒪_{W_t} ⊗ L_t^{⊗ n}) = P(n) for every n ∈ ℤ and every point t of T, the invariants χ(X_t, E_{n,t} ⊗^𝐋 𝒪_{W_t}) of Situation 0DNC for E_n = L^{⊗ n}: the pull-back along the graph transformation of the subfunctor of Hilb_{Z ×_Q X / Q} corresponding to Coh^{P, L}_{Z ×_Q X / Q} (Stacks 0DNF).

def hilbertPolynomialSituationRelativeHom : Subfunctor (relativeHom B S hS Z X Q z x hZ hX hQ)

AlgebraicGeometry.Space.isOpenImmersion_and_isClosedImmersion_hilbertPolynomialSituationRelativeHom_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalRelativeMorphismsClopen.lean, line 323. The attribute's comment: “for I = ℤ and E_i = L^{⊗ i} with L an invertible module on Y ×_B X, Mor^{P, L}_B(Y, X) ⟶ Mor_B(Y, X) is an open and closed immersion”.

For an invertible 𝒪_{Z ×_Q X}-module L and any P : ℤ → ℤ, the morphism Mor^{P, L}_Q(Z, X) ⟶ Mor_Q(Z, X) is an open and closed immersion.

theorem isOpenImmersion_and_isClosedImmersion_hilbertPolynomialSituationRelativeHom_ι :
    IsOpenImmersion B S hS
        (hilbertPolynomialSituationRelativeHom B S hS hsep hx_fp hfp hflat hproper L P).ι ∧
      IsClosedImmersion B S hS
        (hilbertPolynomialSituationRelativeHom B S hS hsep hx_fp hfp hflat hproper L P).ι

AlgebraicGeometry.Space.isFlat_and_isClosedImmersion_numericalRelativeHomInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalRelativeMorphismsImmersion.lean, line 244. The attribute's comment: “Mor^P_B(Y, X) ⟶ Mor_B(Y, X) is a flat closed immersion”.

Stacks 0DPQ. The morphism Mor^P_Q(Z, X) ⟶ Mor_Q(Z, X) is a flat closed immersion.

theorem isFlat_and_isClosedImmersion_numericalRelativeHomInclusion :
    IsFlat B S hS
        (numericalRelativeHomInclusion B S hS Z X Q z x hZ hX hQ χd P hsep hfp hflat hproper) ∧
      IsClosedImmersion B S hS
        (numericalRelativeHomInclusion B S hS Z X Q z x hZ hX hQ χd P hsep hfp hflat hproper)

AlgebraicGeometry.Space.isOpenImmersion_and_isClosedImmersion_numericalRelativeHomInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NumericalRelativeMorphismsImmersion.lean, line 256. The attribute's comment: “for I finite, Mor^P_B(Y, X) ⟶ Mor_B(Y, X) is an open and closed immersion”.

Stacks 0DPQ, the case of a finite index set. For I finite the morphism Mor^P_Q(Z, X) ⟶ Mor_Q(Z, X) is an open and closed immersion.

theorem isOpenImmersion_and_isClosedImmersion_numericalRelativeHomInclusion [Finite I] :
    IsOpenImmersion B S hS
        (numericalRelativeHomInclusion B S hS Z X Q z x hZ hX hQ χd P hsep hfp hflat hproper) ∧
      IsClosedImmersion B S hS
        (numericalRelativeHomInclusion B S hS Z X Q z x hZ hX hQ χd P hsep hfp hflat hproper)

Tag 0DPR, a lemma

Tag 0DPR in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_and_isFinitePresentation_relativeHomHilbertPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeMorphismsHilbertPolynomialFinitePresentation.lean, line 59.

Let Q be an algebraic space over Spec ℤ, z : Z ⟶ Q flat, proper and of finite presentation, x : X ⟶ Q separated and of finite presentation, N an invertible module ample on Z/Q and L an invertible module ample on X/Q (Stacks 0D31), and P a numerical polynomial. Then for ℳ = pr₁^*N ⊗ pr₂^*L on Z ×_Q X (AlgebraicGeometry.Space.graphAmbientTensor), Mor^{P, ℳ}_Q(Z, X) (AlgebraicGeometry.Space.relativeHomHilbertPolynomial) is an algebraic space and its morphism to Q is separated and of finite presentation.

theorem isSeparated_and_isFinitePresentation_relativeHomHilbertPolynomial
    {Z X Q : (BigFppfOver B integerBase ℤS)ᵒᵖ ⥤ Type u} {z : Z ⟶ Q} {x : X ⟶ Q}
    (hZ : IsAlgebraicSpace B integerBase ℤS Z) (hX : IsAlgebraicSpace B integerBase ℤS X)
    (hQ : IsAlgebraicSpace B integerBase ℤS Q)
    (hsep : IsSeparated B integerBase ℤS x) (hxfp : IsFinitePresentation B integerBase ℤS x)
    (hfp : IsFinitePresentation B integerBase ℤS z) (hflat : IsFlat B integerBase ℤS z)
    (hproper : IsProper B integerBase ℤS z)
    (N : Modules.{u, u} B integerBase ℤS Z hZ)
    [hNi : Stacks.SheafOfModules.IsInvertible (structurePresheaf B integerBase ℤS Z)
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B integerBase ℤS Z hZ).O)).property N]
    (L : Modules.{u, u} B integerBase ℤS X hX)
    [hLi : Stacks.SheafOfModules.IsInvertible (structurePresheaf B integerBase ℤS X)
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B integerBase ℤS X hX).O)).property L]
    (hN : IsRelativelyAmple B integerBase ℤS
      (ObjectProperty.homMk z : (⟨Z, hZ⟩ : AlgebraicSpaces B integerBase ℤS) ⟶ ⟨Q, hQ⟩) N)
    (hL : IsRelativelyAmple B integerBase ℤS
      (ObjectProperty.homMk x : (⟨X, hX⟩ : AlgebraicSpaces B integerBase ℤS) ⟶ ⟨Q, hQ⟩) L)
    {P : ℤ → ℤ} {p : Polynomial ℚ} (hP : ∀ m : ℤ, p.eval (m : ℚ) = (P m : ℚ)) :
    IsAlgebraicSpace B integerBase ℤS (relativeHomHilbertPolynomial hZ hX hQ hsep hxfp hfp hflat
        hproper (graphAmbientTensor z x hZ hX hQ N L) P).toFunctor ∧
      IsSeparated B integerBase ℤS ((relativeHomHilbertPolynomial hZ hX hQ hsep hxfp hfp hflat
        hproper (graphAmbientTensor z x hZ hX hQ N L) P).ι ≫
          relativeHomProjection B integerBase ℤS Z X Q z x hZ hX hQ) ∧
      IsFinitePresentation B integerBase ℤS ((relativeHomHilbertPolynomial hZ hX hQ hsep hxfp hfp
        hflat hproper (graphAmbientTensor z x hZ hX hQ N L) P).ι ≫
          relativeHomProjection B integerBase ℤS Z X Q z x hZ hX hQ)

Sources

• Section 108.10, Tag 0DPL
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.diagonal_relativeHomProjection · AlgebraicGeometry.Space.isSeparated_and_isLocallyOfFinitePresentation_relativeHomProjection_unconditional · AlgebraicGeometry.Space.isomSubfunctor · AlgebraicGeometry.Space.isOpenSubspace_isomSubfunctor · AlgebraicGeometry.Space.isOpenSubspace_isomSubfunctor_of_isFinitePresentation · AlgebraicGeometry.Space.numericalRelativeHom · AlgebraicGeometry.Space.numericalSituationRelativeHom · AlgebraicGeometry.Space.isFlat_and_isClosedImmersion_numericalSituationRelativeHom_ι

Section108.11 Properties of the stack of polarized proper schemes#

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

Tag 0DPT, a lemma

Tag 0DPT in the Stacks Project.

AlgebraicGeometry.diagonal_polarizedStackUnconditional_isSeparated_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedDiagonalUnconditional.lean, line 281.

Stacks 0DPT. The diagonal Δ : 𝒫olarized ⟶ 𝒫olarized × 𝒫olarized of the stack of polarized proper flat families of finite presentation, over the big fppf site of a terminal base scheme, is separated and of finite presentation, both read as in Properties of Stacks, Section 04XB: Δ is representable by algebraic spaces (Stacks 0D42), and every algebraic space representing its base change along a scheme-valued point over a scheme U is separated (Stacks 03HL) and of finite presentation (Stacks 03XP, part (3)) over U, read over the base (Stacks 04SG).

theorem diagonal_polarizedStackUnconditional_isSeparated_isFinitePresentation :
    Stack.HasRepresentableDiagonal B S hS (polarizedStackUnconditional B hS hT) ∧
      Stack.IsSeparated B S hS
        (Stack.diagonal.{u, u, u + 1} B S hS (polarizedStackUnconditional B hS hT)) ∧
      ∀ (U : BigFppfOver B S hS)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤
          (CatFiberedInGroupoids.product (polarizedStackUnconditional B hS hT)
            (polarizedStackUnconditional B hS hT)).val.obj)
        (_hy : y ⋙ (CatFiberedInGroupoids.product (polarizedStackUnconditional B hS hT)
            (polarizedStackUnconditional B hS hT)).val.p = Over.map U.hom)
        (F : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hF : IsAlgebraicSpace B U.left.1 U.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) (polarizedStackUnconditional B hS hT).val.p
            (CatFiberedInGroupoids.product (polarizedStackUnconditional B hS hT)
              (polarizedStackUnconditional B hS hT)).val.p y
            (CatFiberedInGroupoids.homFunctor
              (Stack.diagonal.{u, u, u + 1} B S hS (polarizedStackUnconditional B hS hT))))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Space.IsFinitePresentation B S hS
          (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom

Tag 0DPU, a lemma

Tag 0DPU in the Stacks Project.

AlgebraicGeometry.isQuasiSeparated_and_isLocallyOfFinitePresentation_polarizedAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedQuasiSeparatedLocallyFinitePresentation.lean, line 94. The attribute's comment: “the morphism Polarized → Spec(Z) is quasi-separated and locally of finite presentation”.

The morphism 𝒫olarized → Spec(ℤ) is quasi-separated (Stacks 04YW) and locally of finite presentation (Stacks 06Q2).

theorem isQuasiSeparated_and_isLocallyOfFinitePresentation_polarizedAlgebraicStack :
    Stack.AlgebraicStacks.IsQuasiSeparated B _ hZ
        (Stack.structureMorphism B _ hZ (polarizedAlgebraicStack B hZ)) ∧
      Stack.AlgebraicStacks.IsLocallyOfFinitePresentation B _ hZ
        (Stack.structureMorphism B _ hZ (polarizedAlgebraicStack B hZ))

Tag 0E96, a lemma

Tag 0E96 in the Stacks Project.

AlgebraicGeometry.noetherianSpace_of_isHilbertPolarizedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedHilbertBoundedUnconditional.lean, line 254.

Let n ∈ ℕ, let P ∈ ℚ[t] and let T ⊆ |𝒫olarized| be a set of points each represented over a field by a polarized proper scheme (X, ℒ) satisfying conditions (1) and (2) (AlgebraicGeometry.IsHilbertPolarizedOver): the Hilbert polynomial of ℒ on X is P, and there is a closed immersion i : X ⟶ ℙⁿ over the base with i^*𝒪(1) ≅ ℒ. Then T is a Noetherian topological space, in particular quasi-compact. The source's hypotheses n ≥ 1 and that P is numerical are not needed.

theorem noetherianSpace_of_isHilbertPolarizedPoint (hT : IsTerminal (B.obj hS)) (n : ℕ)
    (P : Polynomial ℚ)
    (T : Set (Stack.points B S hS (polarizedStackUnconditional B hS hT).val
      (polarizedStackUnconditional B hS hT).property))
    (hTP : ∀ ξ ∈ T, ∃ p, Stack.pointClass B S hS _ _ p = ξ ∧
      IsHilbertPolarizedPoint B hS hT n P p) :
    letI := Stack.pointTopology B S hS (polarizedStackUnconditional B hS hT)
    NoetherianSpace T

Sources

• Section 108.11, Tag 0DPS
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.diagonal_polarizedStackUnconditional_isSeparated_isFinitePresentation · AlgebraicGeometry.isQuasiSeparated_and_isLocallyOfFinitePresentation_polarizedAlgebraicStack · AlgebraicGeometry.noetherianSpace_of_isHilbertPolarizedPoint

Section108.12 Properties of moduli of complexes on a proper morphism#

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

Tag 0DPW, a lemma

Tag 0DPW in the Stacks Project.

AlgebraicGeometry.Space.ComplexesSituation.complexesIsom_finitePresentation_and_affine_overNegativeExtLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesDiagonalProved.lean, line 326. The attribute's comment: “Corrected statement (Stacks erratum): the source asserts that the diagonal of Complexes_{X/B} over B is affine and of finite presentation; the 'affine' part is false (counterexample: X = P^1 over A^2_k with complexes E and E' = E ⊗ O(2), for which Isom(E, E') is empty over the origin and not affine over A^2). Formalized: the diagonal over B is representable by algebraic spaces and of finite presentation, and for (T, E), (T, E') the functor Isom(E, E') factors through the open W(E, E') ∩ W(E', E) of 0DLC and is affine and of finite presentation over it.”.

Let f : X ⟶ B be proper, flat and of finite presentation (Situation 0DLE), and let x = (T, E), y = (T, E') be objects of Complexes_{X/B} over the same scheme T and the same morphism T ⟶ B, so that E, E' are B-perfect objects of D(𝒪_{X_T}) with vanishing negative self-Exts on the fibres; the base change of the diagonal of Complexes_{X/B} over B along the T-point (x, y) of Complexes_{X/B} ×_B Complexes_{X/B} is Isom(x, y). Then:

1. the presheaf Isom(x, y) on (Sch/T) is the relative derived Isom functor T' ↦ Isom(E_{T'}, E'_{T'}) of X_T ⟶ T;
2. it is an algebraic space of finite presentation over T: the diagonal of Complexes_{X/B} over B is representable by algebraic spaces and of finite presentation;
3. the opens W(E, E') and W(E', E) of T of Stacks 0DLC, part (1), exist;
4. for these opens (W(E, E'): the field points y of T with Ext^i(E_y, E'_y) = 0 for i < 0, and symmetrically), Isom(x, y) factors through W(E, E') ∩ W(E', E) and is affine and of finite presentation over it.

This is the corrected form of Stacks 0DPW, not the statement as written. The source asserts that the diagonal is affine and of finite presentation; the "affine" part is false (its proof applies Stacks 0DLC, part (3), as if W(E, E') were all of T): for X = P¹ over A²_k there are complexes E, E' = E ⊗ O(2) for which Isom(E, E') is empty over the origin and not affine over A².

theorem complexesIsom_finitePresentation_and_affine_overNegativeExtLocus :
    Nonempty ((complexesFunctor D).isomPresheaf ⟨A, rfl⟩ ⟨sameTest A E' h₁ h₂, rfl⟩ ≅
      (overSchemeTest A.T.left).op ⋙ relativeDerivedIsomFunctor (D.projection A.T) A.E E') ∧
    IsFinitePresentationAlgebraicSpaceOver ((schemeSpaceFunctor B S hS).obj A.T.left)
      (relativeDerivedIsomFunctor (D.projection A.T) A.E E') ∧
    (∃ W₁ : OpenSubspaces B S hS ((schemeSpaceFunctor B S hS).obj A.T.left).1,
      IsNegativeExtLocus (D.projection A.T) A.E E' W₁) ∧
    (∃ W₂ : OpenSubspaces B S hS ((schemeSpaceFunctor B S hS).obj A.T.left).1,
      IsNegativeExtLocus (D.projection A.T) E' A.E W₂) ∧
    ∀ (W₁ W₂ : OpenSubspaces B S hS ((schemeSpaceFunctor B S hS).obj A.T.left).1),
      IsNegativeExtLocus (D.projection A.T) A.E E' W₁ →
      IsNegativeExtLocus (D.projection A.T) E' A.E W₂ →
      (∀ T' : SchemesOver ((schemeSpaceFunctor B S hS).obj A.T.left),
        Nonempty ((relativeDerivedIsomFunctor (D.projection A.T) A.E E').obj (op T')) →
          ∃ t : (schemeSpaceFunctor B S hS).obj T'.left ⟶
              openSubspaceAsSpace B S hS ⟨W₁.1 ⊓ W₂.1,
                isOpenSubspace_inf B S hS ((schemeSpaceFunctor B S hS).obj A.T.left).2 W₁.1 W₂.1
                  W₁.2 W₂.2⟩,
            t ≫ openSubspaceImmersion B S hS ⟨W₁.1 ⊓ W₂.1,
              isOpenSubspace_inf B S hS ((schemeSpaceFunctor B S hS).obj A.T.left).2 W₁.1 W₂.1
                W₁.2 W₂.2⟩ = T'.hom) ∧
      IsAffineFinitePresentationAlgebraicSpaceOver
        (openSubspaceAsSpace B S hS ⟨W₁.1 ⊓ W₂.1,
          isOpenSubspace_inf B S hS ((schemeSpaceFunctor B S hS).obj A.T.left).2 W₁.1 W₂.1 W₁.2
            W₂.2⟩)
        ((CostructuredArrow.map (S := schemeSpaceFunctor B S hS)
          (openSubspaceImmersion B S hS ⟨W₁.1 ⊓ W₂.1,
            isOpenSubspace_inf B S hS ((schemeSpaceFunctor B S hS).obj A.T.left).2 W₁.1 W₂.1
              W₁.2 W₂.2⟩)).op ⋙
          relativeDerivedIsomFunctor (D.projection A.T) A.E E')

Tag 0DPX, a lemma

Tag 0DPX in the Stacks Project.

AlgebraicGeometry.Space.ComplexesSituation.isQuasiSeparated_and_isLocallyOfFinitePresentation_complexesAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesQuasiSeparatedLocallyFinitePresentation.lean, line 72.

In Situation 0DLE (f : X ⟶ B proper, flat and of finite presentation), the morphism Complexes_{X/B} → B is quasi-separated and locally of finite presentation. Here Complexes_{X/B} is the algebraic stack given by isAlgebraicStack_complexes_proved, taken through its small model, and B is the algebraic stack of its category of elements.

theorem isQuasiSeparated_and_isLocallyOfFinitePresentation_complexesAlgebraicStack
    (D : ComplexesSituation B S hS) :
    Stack.AlgebraicStacks.IsQuasiSeparated B S hS
        (complexesStructureMorphism D (isAlgebraicStack_complexes_proved.{u, w} hS D)) ∧
      Stack.AlgebraicStacks.IsLocallyOfFinitePresentation B S hS
        (complexesStructureMorphism D (isAlgebraicStack_complexes_proved.{u, w} hS D))

Sources

• Section 108.12, Tag 0DPV
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.ComplexesSituation.complexesIsom_finitePresentation_and_affine_overNegativeExtLocus · AlgebraicGeometry.Space.ComplexesSituation.isQuasiSeparated_and_isLocallyOfFinitePresentation_complexesAlgebraicStack

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.