99.3 The Hom functor to 99.12 Relative morphisms

Section99.3 The Hom functor #

Section 99.3 of the Stacks Project, Tag 08JS. 10 tags here are carried by 31 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08JT, a situation

Tag 08JT in the Stacks Project.

AlgebraicGeometry.Space.HomSituation.homFunctor_eq_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Hom/HomFunctorEtaleDescent.lean, line 200. The attribute's comment: “the Hom functor on the test schemes over the base is the restriction of the Hom functor indexed by the algebraic spaces over the base”.

The relative Hom functor of Stacks 08JT on the test schemes over the base is the restriction of the one indexed by the algebraic spaces over the base. The functor Hom(F, G) : (Sch/base)^{opp} ⥤ Sets of Stacks 08JT is AlgebraicGeometry.Space.HomSituation.homOverSpaceFunctor composed with the inclusion AlgebraicGeometry.Space.schemesOverToOver of the test schemes over the base into the algebraic spaces over the base.

The two sides are the same functor on the nose: base change along a test scheme is base change along the algebraic space it names, and the coherence datum the left-hand side carries is used only in the two functor laws, which are propositions.

theorem homFunctor_eq_restriction (hc : ModulePushforwardCoherence B S hS) :
    s.homFunctor hc = (schemesOverToOver s.base).op ⋙ s.homOverSpaceFunctor

AlgebraicGeometry.Space.HomSituation.homOverSpaceFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Hom/HomFunctorMorphisms.lean, line 306. The attribute's comment: “the Hom functor indexed by the algebraic spaces over the base”.

The relative Hom functor of Stacks 08JT, indexed by the algebraic spaces over the base. Its value at T ⟶ base is Hom_{𝒪_{X_T}}(F_T, G_T) and its action is pullback of homomorphisms. The relative Hom functor on the test schemes over the base is this one restricted along the inclusion of those into the algebraic spaces over the base.

The pseudofunctoriality of the direct images of Stacks 03LU, which makes pullback of homomorphisms functorial, is supplied by AlgebraicGeometry.Space.modulePushforwardCoherence and so is not a hypothesis.

def homOverSpaceFunctor : (Over s.base)ᵒᵖ ⥤ Type (u + 1)

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

Stacks 08JT. The standing data of the relative Hom functor: a morphism f : X ⟶ base of algebraic spaces over S and two quasi-coherent 𝒪_X-modules.

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

AlgebraicGeometry.Space.HomSituation.homFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHom.lean, line 594. The attribute's comment: “the Hom functor, conditional on the pseudofunctoriality of the direct images of Stacks 03LU”.

Stacks 08JT. The relative Hom functor Hom(F, G) : (Sch/base)ᵒᵖ ⥤ Sets, whose value at a test scheme T over the base is Hom_{𝒪_{X_T}}(F_T, G_T) and whose action on a morphism of test schemes is pullback of homomorphisms.

The hypothesis is the pseudofunctoriality of the direct images of Stacks 03LU; the two functor laws are exactly its associativity coherence and its unit law.

def homFunctor (hc : ModulePushforwardCoherence B S hS) :
    (s.SchemesOver)ᵒᵖ ⥤ Type (u + 1)

AlgebraicGeometry.Space.HomSituation.homFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHom.lean, line 602. The attribute's comment: “the value of the functor, conditional on the pseudofunctoriality of the direct images of Stacks 03LU”.

Stacks 08JT. The value of the relative Hom functor at a test scheme over the base is the set of 𝒪_{X_T}-module homomorphisms F_T ⟶ G_T.

theorem homFunctor_obj (hc : ModulePushforwardCoherence B S hS) (T : s.SchemesOver) :
    (s.homFunctor hc).obj (Opposite.op T) = s.homAt T

AlgebraicGeometry.Space.HomSituation.homFunctor_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHom.lean, line 610. The attribute's comment: “the action of the functor, conditional on the pseudofunctoriality of the direct images of Stacks 03LU”.

Stacks 08JT. The action of the relative Hom functor on a morphism of test schemes is pullback of homomorphisms.

theorem homFunctor_map (hc : ModulePushforwardCoherence B S hS) {U T : s.SchemesOver}
    (g : U ⟶ T) :
    (s.homFunctor hc).map (Opposite.op g) = TypeCat.ofHom (s.homMap g)

Tag 08JV, a lemma

Tag 08JV in the Stacks Project.

AlgebraicGeometry.Space.HomSituation.existsUnique_homMap_of_restrictionsAgree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomFpqcDescent.lean, line 493. The attribute's comment: “the sheaf property elementwise, for an fpqc covering of test schemes; the same property as CategoryTheory.Presieve.IsSheafFor is isSheafFor_homFunctor”.

Stacks 08JV. In the standing data of Stacks 08JT the relative Hom functor Hom(F, G) satisfies the sheaf property for the fpqc topology: for an fpqc covering {U i ⟶ T} of test schemes over the base, a family of homomorphisms F_{U i} ⟶ G_{U i} whose restrictions agree on the overlaps X_{U i} ×_{X_T} X_{U j} comes from a unique homomorphism F_T ⟶ G_T.

This is the proof of the source. The base changes {X_{U i} ⟶ X_T} form an fpqc covering of X_T by Stacks 03MR, part (3), in the form of AlgebraicGeometry.Space.isFpqcCovering_baseChangeMap, and a compatible family of homomorphisms of the inverse images of two quasi-coherent modules along an fpqc covering glues uniquely, which is the gluing half of Stacks 04W8, AlgebraicGeometry.Space.existsUnique_restrictPullbackHom_eq_of_isFpqcCovering. The base-changed modules F_T, G_T are quasi-coherent by Stacks 03GA, AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePullback_of_isQuasicoherentOnSite.

theorem existsUnique_homMap_of_restrictionsAgree
    {I : Type v} {T : s.SchemesOver} {U : I → s.SchemesOver} (g : ∀ i, U i ⟶ T)
    (hg : IsFpqcCovering B S hS fun i ↦ ((schemeSpaceFunctor B S hS).map (g i).left).hom)
    (α : ∀ i, s.homAt (U i))
    (hα : RestrictionsAgree (s.projection T) (fun i ↦ baseChangeMap s.f (g i))
      (fun i ↦ s.projection (U i)) (fun i ↦ baseChangeMap_comp_projection s.f (g i))
      (fun i ↦ s.toModuleHom (α i))) :
    ∃! β : s.homAt T, ∀ i, s.homMap (g i) β = α i

AlgebraicGeometry.Space.HomSituation.isSheafFor_homFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomFpqcDescent.lean, line 670. The attribute's comment: “the sheaf property for the presieve of an fpqc covering of test schemes”.

Stacks 08JV, as the sheaf condition for a presieve. In the standing data of Stacks 08JT the relative Hom functor Hom(F, G) is a sheaf for the presieve generated by an fpqc covering {U i ⟶ T} of test schemes over the base: every compatible family of sections has a unique amalgamation.

This is AlgebraicGeometry.Space.HomSituation.existsUnique_homMap_of_restrictionsAgree with the compatibility of the family transported to the overlaps X_{U i} ×_{X_T} X_{U j} of the base changes. That transport is the content added here: the overlap U i ×_T U j of two test schemes is again a test scheme, so a compatible family restricts compatibly to it, and the fibre product of the two base changes maps to the base change of that overlap by AlgebraicGeometry.Space.HomSituation.overlapTestComparison, which carries the two projections of the fibre product to the base changes of the two projections of the overlap.

This is the form of the sheaf property that Stacks 08K8 consumes, as the hypothesis hHom of AlgebraicGeometry.Space.HomSituation.isSheafFor_isomFunctor.

theorem isSheafFor_homFunctor (hc : ModulePushforwardCoherence B S hS)
    {I : Type v} {T : s.SchemesOver} {U : I → s.SchemesOver} (g : ∀ i, U i ⟶ T)
    (hg : IsFpqcCovering B S hS fun i ↦ ((schemeSpaceFunctor B S hS).map (g i).left).hom) :
    Presieve.IsSheafFor (s.homFunctor hc) (Presieve.ofArrows U g)

AlgebraicGeometry.Space.HomSituation.isSheaf_homFunctor_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomFpqcSheaf.lean, line 52.

Stacks 08JV. In Situation 08JT the relative Hom functor Hom(F, G), sending a scheme T over the base to Hom_{𝒪_{X_T}}(F_T, G_T), satisfies the sheaf property for the fpqc topology on the schemes over the base.

Its functoriality is the pseudofunctoriality of Stacks 03LU, which is AlgebraicGeometry.Space.modulePushforwardCoherence, proved with no hypothesis.

theorem isSheaf_homFunctor_fpqc :
    Presheaf.IsSheaf (fpqcTopology s.base) (s.homFunctor (modulePushforwardCoherence B S hS))

Tag 0D3S, a lemma

Tag 0D3S in the Stacks Project.

AlgebraicGeometry.Space.HomSituation.bijective_morOfSpaceHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Hom/HomFunctorEtaleDescent.lean, line 165. The attribute's comment: “Mor(T, Hom(F, G)) = {(h, u)}: the construction (h, u) ↦ (a ↦ (h ∘ a, a^*u)) is a bijection from the pairs onto the morphisms T ⟶ Hom(F, G), for every algebraic space T”.

For an algebraic space T over S, the morphisms of sheaves T ⟶ Hom(F, G) are the pairs (h, u) of a morphism h : T ⟶ base and a homomorphism u : F_T ⟶ G_T of the two modules pulled back to X ×_{base, h} T: the construction (h, u) ↦ (a ↦ (h ∘ a, a^*u)), which is AlgebraicGeometry.Space.HomSituation.morOfSpaceHom, is a bijection.

theorem bijective_morOfSpaceHom (T : AlgebraicSpaces B S hS) :
    Function.Bijective (s.morOfSpaceHom (modulePushforwardCoherence B S hS) (T := T))

AlgebraicGeometry.Space.HomSituation.baseOfMor_morOfSpaceHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Hom/HomFunctorMorphisms.lean, line 779. The attribute's comment: “the first component of the pair is recovered from the morphism of sheaves, conditional on the pseudofunctoriality of the direct images of Stacks 03LU”.

The morphism to the base is recovered from the morphism of presheaves: for a pair (h, u) the morphism underlying morOfSpaceHom (h, u) is h. This is the half of Stacks 0D3S that needs no descent.

theorem baseOfMor_morOfSpaceHom (hc : ModulePushforwardCoherence B S hS)
    {T : AlgebraicSpaces B S hS} (p : s.SpaceHomPair T) :
    s.baseOfMor hc (s.morOfSpaceHom hc p) = p.toBase

AlgebraicGeometry.Space.HomSituation.bijective_morOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Hom/HomFunctorMorphisms.lean, line 977. The attribute's comment: “the identification is a bijection on the fibres over a fixed morphism to the base; carries two hypotheses: hc, the pseudofunctoriality of the direct images of Stacks 03LU, and hd, the fullness clause of Stacks 04W8 for a one-member etale covering (the faithfulness clause of Stacks 04W8 is proved here and not assumed)”.

Stacks 0D3S, the fibres of the identification. For a fixed morphism h : T ⟶ base of algebraic spaces over S, the assignment u ↦ morOfSpaceHom (h, u) is a bijection from the homomorphisms u : F_T ⟶ G_T of the two modules pulled back to X ×_{base, h} T onto the morphisms of presheaves T ⟶ Hom(F, G) lying over h.

Together with AlgebraicGeometry.Space.HomSituation.baseOfMor_morOfSpaceHom, which recovers the first component, this is the identification Mor(T, Hom(F, G)) = {(h, u) | h : T ⟶ base, u : F_T ⟶ G_T} of Stacks 0D3S.

Injectivity is faithfulness of descent of homomorphisms of modules along the étale covering X_U ⟶ X_T cut out by a scheme atlas U ⟶ T of Stacks 0262, and is unconditional here. Surjectivity is fullness of that descent, carried by the hypothesis hd.

theorem bijective_morOver (hc : ModulePushforwardCoherence B S hS) (hd : s.EtaleHomDescent)
    {T : AlgebraicSpaces B S hS} (h : T ⟶ s.base) : Function.Bijective (s.morOver hc h)

Tag 08JW, a remark

Tag 08JW in the Stacks Project.

AlgebraicGeometry.Space.HomSituation.baseChangedSituation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHom.lean, line 654. The attribute's comment: “the base-changed situation”.

Stacks 08JW. The relative Hom situation obtained by changing the base algebraic space along p : base' ⟶ base: its source is X' = X ×_base base', its morphism the second projection, and its two modules the pullbacks of F and G along the first projection.

def baseChangedSituation : HomSituation B S hS

AlgebraicGeometry.Space.HomSituation.homFunctorBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHom.lean, line 729. The attribute's comment: “the identification Hom(F',G')(T) = Hom(F,G)(T), natural in T”.

Stacks 08JW. For a test scheme T over base' the two relative Hom sets agree: Hom(F', G')(T) = Hom(F, G)(T), where on the right T is read as a scheme over base through T ⟶ base' ⟶ base. The identification is natural in T, so it is an isomorphism of the two relative Hom functors.

It has no hypotheses. The coherence data for the direct images, which the Hom functor of either situation is formed from, is AlgebraicGeometry.Space.modulePushforwardCoherence, and the quasi-coherence of the two pullbacks, which forming the base-changed situation needs, is AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePullback_of_isQuasicoherentOnSite.

def homFunctorBaseChange :
    (s.baseChangedSituation p).homFunctor (modulePushforwardCoherence B S hS) ≅
      (CostructuredArrow.map p).op ⋙ s.homFunctor (modulePushforwardCoherence B S hS)

Tag 08K3, a lemma

Tag 08K3 in the Stacks Project.

AlgebraicGeometry.Space.HomSituation.tripleRestrictionsAgree_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomFpqcDescent.lean, line 1033. The attribute's comment: “the two parallel arrows agree on the image of the first arrow”.

Stacks 08K3, the first half of the exactness. The restrictions of a global homomorphism F_T ⟶ G_T to the base changes X_{i, T} of the members of a covering of the source satisfy the overlap condition: the two parallel arrows of the diagram agree on the image of the first arrow.

Both restrictions are the restriction of the global homomorphism along the projection X_{ijk, T} ⟶ X_T, because both parallel arrows are morphisms over X_T.

theorem tripleRestrictionsAgree_restrict (β : s.homAt T) :
    s.TripleRestrictionsAgree a T b
      (fun i ↦ restrictPullbackHom (s.memberInclusion a T i) (s.memberInclusion_comp a T i)
        (s.toModuleHom β))

AlgebraicGeometry.Space.HomSituation.existsUnique_sourceHom_of_tripleRestrictionsAgree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomFpqcDescent.lean, line 1072. The attribute's comment: “the first arrow is injective with image the equalizer of the other two”.

Stacks 08K3, the second half of the exactness. In the standing data of Stacks 08JT let {X_i ⟶ X} be an fppf covering and for all i, j let {X_{ijk} ⟶ X_i ×_X X_j} be an fppf covering. For every test scheme T over the base, a family of homomorphisms F_i ⟶ G_i over the base changes X_{i, T} whose restrictions agree on the X_{ijk, T} comes from a unique homomorphism F_T ⟶ G_T.

Together with AlgebraicGeometry.Space.HomSituation.tripleRestrictionsAgree_restrict this is the exactness of the diagram displayed by the source: the first arrow lands in the equalizer of the other two, is injective, and hits every element of that equalizer.

This is the proof of the source. The base change of an fppf covering is an fppf covering, so {X_{i, T} ⟶ X_T} and {X_{ijk, T} ⟶ X_{i, T} ×_{X_T} X_{j, T}} are fppf, hence fpqc, coverings — Stacks 03Y9 and Stacks 03MR, part (3). Applying Stacks 04W8 to the second reduces the overlap condition to the overlaps themselves, and applying it to the first, in the form AlgebraicGeometry.Space.existsUnique_restrictPullbackHom_eq_of_isFpqcCovering, produces the unique global homomorphism. The base-changed modules F_T, G_T are quasi-coherent by Stacks 03GA, AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePullback_of_isQuasicoherentOnSite.

theorem existsUnique_sourceHom_of_tripleRestrictionsAgree
    (hrepr : QuasiCoherentDescent.ReprFpqcHomInjective.{u, v} B S hS)
    (ha : IsFppfCovering B S hS (fun i ↦ (Xi i).1) fun i ↦ (a i).hom)
    (hb : ∀ i j, IsFppfCovering B S hS (fun k ↦ (Xijk i j k).1) fun k ↦ (b i j k).hom)
    (α : ∀ i, (modulePullback B S hS (s.memberToSource a T i)).obj s.F ⟶
      (modulePullback B S hS (s.memberToSource a T i)).obj s.G)
    (hα : s.TripleRestrictionsAgree a T b α) :
    ∃! β : s.homAt T, ∀ i, restrictPullbackHom (s.memberInclusion a T i)
      (s.memberInclusion_comp a T i) (s.toModuleHom β) = α i

AlgebraicGeometry.Space.HomSituation.tripleRestrictionsAgree_iff_existsUnique_sourceHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomFpqcGluing.lean, line 86.

Stacks 08K3. In Situation 08JT let {X_i ⟶ X} be an fppf covering and for all i, j let {X_{ijk} ⟶ X_i ×_X X_j} be an fppf covering, and write F_i, G_i, F_{ijk}, G_{ijk} for the pullbacks of F and G. For every scheme T over the base, the diagram Hom(F, G)(T) ⟶ ∏_i Hom(F_i, G_i)(T) ⇉ ∏_{ijk} Hom(F_{ijk}, G_{ijk})(T) presents the first arrow as the equalizer of the other two: a family (α i) of homomorphisms over the base changes X_{i, T} is taken to the same element by the two parallel arrows exactly when it is the image of a unique β : F_T ⟶ G_T.

The backward direction says that the first arrow lands in the equalizer; together with it the forward direction says that the first arrow is injective and its image is the equalizer.

This is the proof of the source. The base changes {X_{i, T} ⟶ X_T} and {X_{ijk, T} ⟶ X_{i, T} ×_{X_T} X_{j, T}} are fppf, hence fpqc, coverings (Stacks 03Y9); Stacks 04W8 applied to the second, in the form of its faithfulness half, reduces the condition to the overlaps themselves, and applied to the first, in the form AlgebraicGeometry.Space.gluesModuleHomAlongFpqcCovering, produces the unique global homomorphism. The base-changed modules F_T, G_T are quasi-coherent by Stacks 03GA.

theorem tripleRestrictionsAgree_iff_existsUnique_sourceHom
    (ha : IsFppfCovering B S hS (fun i ↦ (Xi i).1) fun i ↦ (a i).hom)
    (hb : ∀ i j, IsFppfCovering B S hS (fun k ↦ (Xijk i j k).1) fun k ↦ (b i j k).hom)
    (α : ∀ i, (modulePullback B S hS (s.memberToSource a T i)).obj s.F ⟶
      (modulePullback B S hS (s.memberToSource a T i)).obj s.G) :
    s.TripleRestrictionsAgree a T b α ↔
      ∃! β : s.homAt T, ∀ i, restrictPullbackHom (s.memberInclusion a T i)
        (s.memberInclusion_comp a T i) (s.toModuleHom β) = α i

Tag 08K4, a lemma

Tag 08K4 in the Stacks Project.

AlgebraicGeometry.Space.HomSituation.isLimitPreservingHom_of_isEqualizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomLimitPreserving.lean, line 247. The attribute's comment: “reduced to the equalizer presentation of Stacks 08K3; that presentation and the affine case, Stacks 05LI, are not proved”.

Stacks 08K4, reduced to an equalizer presentation of the relative Hom functor. The relative Hom functor of Stacks 08JT is limit preserving as soon as it is cut out, at every test scheme over the base, as the equalizer of two maps between limit-preserving presheaves.

Stacks 08K3 supplies such a presentation from an affine scheme surjective and étale over the source and an affine scheme surjective and étale over its self-overlap, which exist because the structure morphism is quasi-compact and quasi-separated (Stacks 03H6), the two presheaves being the relative Hom functors of those charts; their limit preservation is the affine case, which is Stacks 05LI. Neither the presentation nor the affine case is proved here, so both are asked for as data; accordingly the three hypotheses of Stacks 08K4 are not used.

theorem isLimitPreservingHom_of_isEqualizer (hc : ModulePushforwardCoherence B S hS)
    (s : HomSituation B S hS) {Q R : (s.SchemesOver)ᵒᵖ ⥤ Type (u + 1)}
    (a : s.homFunctor hc ⟶ Q) (b₁ b₂ : Q ⟶ R)
    (hinj : ∀ T, Function.Injective (a.app T))
    (hequalizes : ∀ (T : (s.SchemesOver)ᵒᵖ) (α : (s.homFunctor hc).obj T),
      b₁.app T (a.app T α) = b₂.app T (a.app T α))
    (hlift : ∀ (T : (s.SchemesOver)ᵒᵖ) (q : Q.obj T),
      b₁.app T q = b₂.app T q → ∃ α, a.app T α = q)
    (hQ : LimitPreserving.{u, u + 1, w, w', u + 1} s.testSchemeFunctor Q)
    (hR : LimitPreserving.{u, u + 1, w, w', u + 1} s.testSchemeFunctor R) :
    IsLimitPreservingHom.{u, w, w'} hc s

AlgebraicGeometry.Space.HomSituation.limitPreserving_homFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomLimitPreservingUnconditional.lean, line 134.

Stacks 08K4. In Situation 08JT, if F is of finite presentation and f is quasi-compact and quasi-separated, then the relative Hom functor Hom(F, G) is limit preserving: for every directed limit T = lim T_i of affine schemes over the base, Hom(F, G)(T) = colim Hom(F, G)(T_i).

theorem limitPreserving_homFunctor (s : HomSituation B S hS)
    (hF : s.F.IsFinitePresentationOnSite) (hqc : IsQuasiCompact B S hS s.f.hom)
    (hqs : IsQuasiSeparated B S hS s.f.hom) :
    LimitPreserving.{u, u + 1, u, u} s.testSchemeFunctor
      (s.homFunctor (modulePushforwardCoherence B S hS))

Tag 08K5, a lemma

Tag 08K5 in the Stacks Project.

AlgebraicGeometry.Space.homFunctorClosedImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomClosedImmersion.lean, line 560. The attribute's comment: “the identification Hom(F, i_G') = Hom(i^F, G') as functors on (Sch/B), conditional on the pseudofunctoriality of the direct images of Stacks 03LU, on the quasi-coherence of i_G' (Stacks 03M9) and of i^F (Stacks 03GA), and on the base-change clause of Stacks 07U8 for i”.

Stacks 08K5. Let i : X' ⟶ X be a closed immersion of algebraic spaces over an algebraic space Y over S, let F be a quasi-coherent 𝒪_X-module and let G' be a quasi-coherent 𝒪_{X'}-module. Then

Hom(F, i_*G') = Hom(i^*F, G')

as functors on the test schemes over Y: the relative Hom functor of Stacks 08JT of the situation (X ⟶ Y, F, i_*G') is isomorphic to the one of the situation (X' ⟶ Y, i^*F, G'). Being an isomorphism of functors, the identification includes the compatibility with every change of test scheme.

The comparison is pullback of homomorphisms along the base changes X'_T ⟶ X_T of i, read through the counit isomorphism i^*i_* ≅ 𝟭 of Stacks 04CJ, part (2).

It is conditional on three inputs this development does not have, all of them results the source quotes: the pseudofunctoriality hc of the direct images of Stacks 03LU, without which the relative Hom functor of Stacks 08JT does not exist at all; the quasi-coherence hiG of i_*G' (Stacks 03M9, resp. the quasi-coherence clause of Stacks 07U8) and hiF of i^*F (Stacks 03GA), which are fields of AlgebraicGeometry.Space.HomSituation and so are needed to form the two situations being compared; and the base-change clause hbc of Stacks 07U8, which is the one input with mathematical content here.

def homFunctorClosedImmersion (hc : ModulePushforwardCoherence B S hS) (p : X ⟶ Y)
    (i : X' ⟶ X) (hi : IsClosedImmersion B S hS i.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (G' : Modules.{u, u} B S hS X'.1 X'.2)
    (hF : F.IsQuasicoherentOnSite)
    (hiG : ((modulePushforward B S hS i).obj G').IsQuasicoherentOnSite)
    (hiF : ((modulePullback B S hS i).obj F).IsQuasicoherentOnSite)
    (hG' : G'.IsQuasicoherentOnSite)
    (hbc : TestSchemePushforwardBaseChange p i G') :
    (pushforwardHomSituation p i F G' hF hiG).homFunctor hc ≅
      (pullbackHomSituation p i F G' hiF hG').homFunctor hc

AlgebraicGeometry.Space.homFunctorClosedImmersionIso_of_isQuasicoherentOnSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomClosedImmersionUnconditional.lean, line 90.

Let i : X' ⟶ X be a closed immersion of algebraic spaces over an algebraic space Y over S, let F be a quasi-coherent 𝒪_X-module and let G' be a quasi-coherent 𝒪_{X'}-module. Then

Hom(F, i_*G') = Hom(i^*F, G')

as functors on the test schemes over Y: the relative Hom functor of Stacks 08JT of the situation (X ⟶ Y, F, i_*G') is isomorphic to the one of the situation (X' ⟶ Y, i^*F, G'), both formed with the pseudofunctoriality AlgebraicGeometry.Space.modulePushforwardCoherence of Stacks 03LU.

The two situations are formed with the quasi-coherence of i_*G' (Stacks 03M9) and of i^*F (Stacks 03GA), and the comparison is bijective by the base-change clause of Stacks 07U8 for the affine morphism i.

def homFunctorClosedImmersionIso_of_isQuasicoherentOnSite (p : X ⟶ Y) (i : X' ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    (G' : Modules.{u, u} B S hS X'.1 X'.2) (hF : F.IsQuasicoherentOnSite)
    (hG' : G'.IsQuasicoherentOnSite) :
    (pushforwardHomSituation p i F G' hF
        (isQuasicoherentOnSite_modulePushforward_of_isClosedImmersion B S hS i hi G'
          hG')).homFunctor (modulePushforwardCoherence B S hS) ≅
      (pullbackHomSituation p i F G'
        (isQuasicoherentOnSite_modulePullback_of_isClosedImmersion B S hS i hi F hF)
        hG').homFunctor (modulePushforwardCoherence B S hS)

Tag 08JX, a lemma

Tag 08JX in the Stacks Project.

AlgebraicGeometry.Space.isAffineFinitePresentationAlgebraicSpaceOver_degreeZeroSectionsFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/DegreeZeroSectionsRepresentable.lean, line 79. The attribute's comment: “part (1)”.

Stacks 08JX, part (1). Let K be a pseudo-coherent object of D(𝒪_X) on an algebraic space X such that H⁻¹(Lg^*K) = 0 for every scheme g : T → X. Then the functor (g : T → X) ↦ H⁰(T, H⁰(Lg^*K)) on the schemes over X is an algebraic space affine and of finite presentation over X.

The functor is the degree-zero sections functor of any K-flat complex P₀ with flat terms representing K; its value at g is H⁰(T, H⁰(Lg^*K)) by AlgebraicGeometry.Space.degreeZeroSectionsEquiv.

theorem isAffineFinitePresentationAlgebraicSpaceOver_degreeZeroSectionsFunctor
    (K : derivedModules B S hS X) (hK : IsPseudoCoherentObject K)
    (hvan : HasVanishingDegreeNegOneDerivedPullback (hasDerivedModulePullbacks B S hS) K)
    (P₀ : CochainComplex (toposModules B S hS X) ℤ)
    (hP₀ : IsKFlat (Y := smallEtaleRingedTopos B S hS X)
      ((HomotopyCategory.quotient _ (ComplexShape.up ℤ)).obj P₀))
    (e : DerivedCategory.Q.obj P₀ ≅ K) :
    IsAffineFinitePresentationAlgebraicSpaceOver X
      (degreeZeroSectionsFunctor (schemesOverCone X) P₀)

AlgebraicGeometry.Space.derivedPullbackSectionFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/DerivedPullbackSectionFunctor.lean, line 427. The attribute's comment: “the functor of part (2), (g : T → B) ↦ H⁰(T, Lg^*K), on the test schemes over B; its value is Hom_{D(𝒪_T)}(𝒪_T, Lg^*K) by derivedPullbackSectionFunctor_obj_equiv. The datum hc -- Stacks 0D6D and the unit law for L(-)^* -- is built with no hypothesis by AlgebraicGeometry.Space.derivedPullbackCoherence. Its representability is isAffineFinitePresentationSectionFunctor_of_hasVanishingNegativeDerivedPullback and the two conclusions about K are isPerfect_and_locally_hasTorAmplitude_of_hasVanishingNegativeDerivedPullback.”.

The degree-zero hypercohomology functor of Stacks 08JX, part (2): the functor sending a test scheme g : T → B to H⁰(T, Lg^*K), read as the derived Hom out of the pulled-back structure sheaf.

AlgebraicGeometry.Space.derivedPullbackSectionFunctor_obj_equiv identifies its value at T with Hom_{D(𝒪_T)}(𝒪_T, Lg^*K), which is that degree-zero hypercohomology group.

def derivedPullbackSectionFunctor (hc : DerivedPullbackCoherence B S hS hL)
    (K : derivedModules B S hS X) : (SchemesOver X)ᵒᵖ ⥤ Type (u + 1)

AlgebraicGeometry.Space.degreeZeroPullbackSections, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/DerivedPullbackSectionFunctor.lean, line 466. The attribute's comment: “the value at a test scheme g : T → B of the functor of part (1), the group H⁰(T, H⁰(Lg^*K)). Its restriction maps are not constructed here, for want of a comparison g^*H⁰(E) ⟶ H⁰(Lg^*E); part (1) is proved on the degree-zero sections functor of a K-flat complex representing K, which takes these values by AlgebraicGeometry.Space.degreeZeroSectionsEquiv.”.

The value at a test scheme of the functor of Stacks 08JX, part (1): the group H⁰(T, H⁰(Lg^*K)) of global sections of the degree-zero cohomology sheaf of the derived pullback of K along g : T → B.

abbrev degreeZeroPullbackSections (hL : BottomRankStratum.HasDerivedModulePullbacks B S hS)
    (K : derivedModules B S hS X) (T : SchemesOver X) : Type (u + 1)

AlgebraicGeometry.Space.HasVanishingDegreeNegOneDerivedPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/DerivedPullbackSectionFunctor.lean, line 485. The attribute's comment: “the hypothesis of part (1): H⁻¹(Lg^*K) = 0 for every test scheme g : T → B. The hypothesis of part (2) is AlgebraicGeometry.Space.HasVanishingNegativeDerivedPullback.”.

The hypothesis of Stacks 08JX, part (1): for every test scheme g : T → B the cohomology sheaf H⁻¹(Lg^*K) is zero.

def HasVanishingDegreeNegOneDerivedPullback
    (hL : BottomRankStratum.HasDerivedModulePullbacks B S hS)
    (K : derivedModules B S hS X) : Prop

AlgebraicGeometry.Space.HasVanishingNegativeDerivedPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/DerivedPullbackSectionFunctor.lean, line 495. The attribute's comment: “the hypothesis of part (2): Hⁱ(Lg^*K) = 0 for every test scheme g : T → B and every i < 0. The hypothesis of part (1) is AlgebraicGeometry.Space.HasVanishingDegreeNegOneDerivedPullback.”.

The hypothesis of Stacks 08JX, part (2): for every test scheme g : T → B the cohomology sheaves Hⁱ(Lg^*K) are zero for every i < 0.

def HasVanishingNegativeDerivedPullback
    (hL : BottomRankStratum.HasDerivedModulePullbacks B S hS)
    (K : derivedModules B S hS X) : Prop

AlgebraicGeometry.Space.isAffineFinitePresentationSectionFunctor_of_hasVanishingNegativeDerivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/DerivedSectionsFunctor.lean, line 1112. The attribute's comment: “part (2), the conclusion that (g : T → B) ↦ H⁰(T, Lg^*K) is an algebraic space affine and of finite presentation over B”.

Stacks 08JX, part (2), the functor. Let K be a pseudo-coherent object of D(𝒪_X) on an algebraic space X such that Hⁱ(Lg^*K) = 0 for every scheme g : T → X and every i < 0. Then the functor (g : T → X) ↦ H⁰(T, Lg^*K) on the schemes over X is an algebraic space affine and of finite presentation over X.

As in the source, under this hypothesis H⁰(T, Lg^*K) = H⁰(T, H⁰(Lg^*K)) (AlgebraicGeometry.Space.derivedPullbackSectionFunctorIso), so the statement is part (1).

theorem isAffineFinitePresentationSectionFunctor_of_hasVanishingNegativeDerivedPullback
    {X : AlgebraicSpaces B S hS} (K : derivedModules B S hS X) (hK : IsPseudoCoherentObject K)
    (hvan : HasVanishingNegativeDerivedPullback (hasDerivedModulePullbacks B S hS) K) :
    IsAffineFinitePresentationSectionFunctor (derivedPullbackCoherence B S hS) K

AlgebraicGeometry.Space.isPerfect_and_locally_hasTorAmplitude_of_hasVanishingNegativeDerivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PerfectOfVanishingPullbacks.lean, line 543. The attribute's comment: “part (2), the conclusions that K is perfect and locally has tor amplitude in [0, b]”.

Stacks 08JX, part (2), the first two conclusions. Let K be a pseudo-coherent object of D(𝒪_X) on an algebraic space X such that Hⁱ(Lg^*K) = 0 for every scheme g : T → X and every i < 0. Then K is perfect, and K locally has tor amplitude in [0, b]: every étale chart of X is covered by charts V over which K|_V has tor amplitude in [0, b_V] for some b_V ≥ 0, against any derived tensor product on the slices.

The proof is the source's: near every point a strictly perfect approximation of K has a free cokernel Coker(P⁻¹ → P⁰) (Stacks 068U, from the vanishing of H⁻¹ on the fibres), so its canonical truncation τ_{≥ 0} is strictly perfect, and it represents K there because K has no cohomology in negative degrees (AlgebraicGeometry.Space.exists_covering_slice_models).

theorem isPerfect_and_locally_hasTorAmplitude_of_hasVanishingNegativeDerivedPullback
    (T : ∀ U : (smallEtaleRingedSite B S hS X.1 X.2).C,
      DerivedTensorProduct.{u + 1, u, u, u + 1} ((smallEtaleRingedSite B S hS X.1 X.2).over U)) :
    (smallEtaleRingedSite B S hS X.1 X.2).IsPerfect K ∧
      ∀ U : (smallEtaleRingedSite B S hS X.1 X.2).C,
        ∃ P : Presieve U, Sieve.generate P ∈ (smallEtaleRingedSite B S hS X.1 X.2).J U ∧
          ∀ ⦃V : (smallEtaleRingedSite B S hS X.1 X.2).C⦄ (f : V ⟶ U), P f →
            ∃ b : ℤ, 0 ≤ b ∧ DerivedTensorProduct.HasTorAmplitude (T V)
              ((RingedSite.derivedRestriction.{u + 1, u, u, u + 1} _ V).obj K) 0 b

Tag 08JY, a lemma

Tag 08JY in the Stacks Project.

AlgebraicGeometry.Space.HomSituation.isAffineFinitePresentationAlgebraicSpaceOverBase_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomNoetherianRepresentable.lean, line 69.

In Situation 08JT assume that the base B is a Noetherian algebraic space, that f : X ⟶ B is locally of finite type and quasi-separated, that 𝓕 is an 𝒪_X-module of finite type, and that 𝒢 is an 𝒪_X-module of finite type, flat over B, with support proper over B. Then the functor Hom(𝓕, 𝒢) is an algebraic space affine and of finite presentation over B.

theorem isAffineFinitePresentationAlgebraicSpaceOverBase_of_isNoetherian
    (s : HomSituation B S hS) (hTop : B.Contains (⊤_ Scheme.{u}))
    (hB : IsNoetherian B S hS hTop s.base.1) (hf : IsLocallyOfFiniteType B S hS s.f.hom)
    (hfqs : IsQuasiSeparated B S hS s.f.hom) (hF : SheafOfModules.IsFiniteTypeOnSite s.F)
    (hG : SheafOfModules.IsFiniteTypeOnSite s.G) (hflat : IsFlatOver B S hS s.X.2 s.f.hom s.G)
    (hproper : HasProperSupportOver s.f s.G) :
    s.IsAffineFinitePresentationAlgebraicSpaceOverBase (modulePushforwardCoherence B S hS)

Tag 08K6, a proposition

Tag 08K6 in the Stacks Project.

AlgebraicGeometry.Space.HomSituation.isAffineFinitePresentationAlgebraicSpaceOverBase_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomSpaceAffine.lean, line 56. The attribute's comment: “second assertion: for F of finite presentation, Hom(F, G) is an algebraic space affine and of finite presentation over B”.

In Situation 08JT let f : X ⟶ B be of finite presentation and let G be an 𝒪_X-module of finite presentation, flat over B, with support proper over B. If F is of finite presentation, then Hom(F, G) is an algebraic space affine and of finite presentation over B.

theorem isAffineFinitePresentationAlgebraicSpaceOverBase_of_isFinitePresentation
    (s : HomSituation B S hS)
    (hf : IsFinitePresentation B S hS s.f.hom) (hF : s.F.IsFinitePresentationOnSite)
    (hG : s.G.IsFinitePresentationOnSite) (hflat : IsFlatOver B S hS s.X.2 s.f.hom s.G)
    (hproper : HasProperSupportOver s.f s.G) :
    s.IsAffineFinitePresentationAlgebraicSpaceOverBase (modulePushforwardCoherence B S hS)

AlgebraicGeometry.Space.HomSituation.isAffineAlgebraicSpaceOverBase_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeHomSpaceAffine.lean, line 80. The attribute's comment: “first assertion: Hom(F, G) is an algebraic space affine over B, for F étale-locally generated by fewer sections than the cutoff of the site (Stacks erratum)”.

In Situation 08JT let f : X ⟶ B be of finite presentation and let G be an 𝒪_X-module of finite presentation, flat over B, with support proper over B. Then Hom(F, G) is an algebraic space affine over B, for every quasi-coherent F étale-locally generated by fewer than μ sections for one cardinal μ below the cutoff of the site (every module of finite type is).

Without the bound on F the statement is false on a size-bounded site: for X = B = Spec k with Spec k in the site, G = 𝒪_X and F = ⊕_{i ∈ I} 𝒪_X with #I at least the cutoff, Hom(F, G) takes the value A^I at Spec A, and an affine scheme Spec R representing it has its universal element (r_i)_{i ∈ I} with pairwise distinct coordinates, so #R ≥ #I, impossible for an object of the site.

theorem isAffineAlgebraicSpaceOverBase_of_isFinitePresentation
    (s : HomSituation B S hS)
    (hf : IsFinitePresentation B S hS s.f.hom)
    (hG : s.G.IsFinitePresentationOnSite) (hflat : IsFlatOver B S hS s.X.2 s.f.hom s.G)
    (hproper : HasProperSupportOver s.f s.G)
    (hF : ∃ μ < B.cutoff, IsEtaleLocallyGeneratedBelow B S hS μ s.F) :
    s.IsAffineAlgebraicSpaceOverBase (modulePushforwardCoherence B S hS)

Sources

LeanAlgebraicGeometry.Space.HomSituation.homFunctor_eq_restriction · AlgebraicGeometry.Space.HomSituation.homOverSpaceFunctor · AlgebraicGeometry.Space.HomSituation · AlgebraicGeometry.Space.HomSituation.homFunctor · AlgebraicGeometry.Space.HomSituation.homFunctor_obj · AlgebraicGeometry.Space.HomSituation.homFunctor_map · AlgebraicGeometry.Space.HomSituation.existsUnique_homMap_of_restrictionsAgree · AlgebraicGeometry.Space.HomSituation.isSheafFor_homFunctor

Section99.4 The Isom functor #

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

Tag 08K7, the section

Tag 08K7 in the Stacks Project.

AlgebraicGeometry.Space.HomSituation.isomSubfunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeIsom.lean, line 349. The attribute's comment: “the Isom functor as a subfunctor of the Hom functor”.

Stacks 08K7. The relative Isom functor Isom(F, G) ⊆ Hom(F, G) as a subfunctor of the relative Hom functor of Stacks 08JT: its sections at a test scheme T over the base are the invertible 𝒪_{X_T}-homomorphisms F_T ⟶ G_T.

It is a subfunctor because invertibility is stable under pullback, AlgebraicGeometry.Space.HomSituation.isIsomAt_homMap. The ambient relative Hom functor is taken at the pseudofunctoriality of the direct images of Stacks 03LU, AlgebraicGeometry.Space.modulePushforwardCoherence.

def isomSubfunctor : Subfunctor (s.homFunctor (modulePushforwardCoherence B S hS))

AlgebraicGeometry.Space.HomSituation.isomFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeIsom.lean, line 367. The attribute's comment: “the Isom functor”.

Stacks 08K7. The relative Isom functor Isom(F, G) : (Sch/base)ᵒᵖ ⥤ Sets, whose value at a test scheme T over the base is the set of invertible 𝒪_{X_T}-homomorphisms F_T ⟶ G_T and whose action on a morphism of test schemes is pullback of homomorphisms. Its inclusion into the relative Hom functor is CategoryTheory.Subfunctor.ι.

def isomFunctor : (s.SchemesOver)ᵒᵖ ⥤ Type (u + 1)

Tag 08K8, a lemma

Tag 08K8 in the Stacks Project.

AlgebraicGeometry.Space.HomSituation.isSheafFor_isomFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeIsom.lean, line 416. The attribute's comment: “conditional on the sheaf property of the relative Hom functor (Stacks 08JV), on the full-faithfulness clause of the fpqc descent of quasi-coherent modules (Stacks 04W8), and on the quasi-coherence of the two base-changed modules (Stacks 03GA)”.

Stacks 08K8. In the standing data of Stacks 08JT the relative Isom functor Isom(F, G) satisfies the sheaf property for the fpqc topology: for every fpqc covering {U i ⟶ T} of test schemes over the base, every compatible family of invertible 𝒪_{X_{U i}}-homomorphisms F_{U i} ⟶ G_{U i} has a unique amalgamation, again invertible.

This is the proof of the source. The relative Hom functor already satisfies the sheaf property, so the family glues to a unique homomorphism F_T ⟶ G_T; what remains is that it is invertible, and that is AlgebraicGeometry.Space.HomSituation.isIsomAt_of_isFpqcCovering, which produces the fpqc covering {X_{U i} ⟶ X_T} of X_T by Stacks 03MR, part (3), and descends invertibility along it. The passage from the sheaf property of Hom(F, G) to that of its subfunctor is CategoryTheory.Subfunctor.isSheafFor_of_local.

theorem isSheafFor_isomFunctor
    (hdesc : ReflectsIsoAlongFpqcCovering.{u, v} B S hS)
    {I : Type v} {T : s.SchemesOver} {U : I → s.SchemesOver} (g : ∀ i, U i ⟶ T)
    (hg : IsFpqcCovering B S hS
      fun i ↦ ((schemeSpaceFunctor B S hS).map (g i).left).hom)
    (hF : (s.baseChangedModule T s.F).IsQuasicoherentOnSite)
    (hG : (s.baseChangedModule T s.G).IsQuasicoherentOnSite)
    (hHom : Presieve.IsSheafFor (s.homFunctor (modulePushforwardCoherence B S hS))
      (Presieve.ofArrows U g)) :
    Presieve.IsSheafFor s.isomFunctor (Presieve.ofArrows U g)

AlgebraicGeometry.Space.HomSituation.isSheafFor_isomFunctor_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeIsomFpqcSheaf.lean, line 141.

Stacks 08K8. In Situation 08JT the relative Isom functor Isom(F, G) satisfies the sheaf property for the fpqc topology: for every fpqc covering {U i ⟶ T} of schemes over the base, every compatible family of invertible homomorphisms F_{U i} ⟶ G_{U i} has a unique amalgamation, an invertible homomorphism F_T ⟶ G_T.

This is the proof of the source. Hom(F, G) satisfies the sheaf property, Stacks 08JV in the form of AlgebraicGeometry.Space.HomSituation.isSheafFor_homFunctor_of_isFpqcCovering, so it remains that a homomorphism F_T ⟶ G_T whose base changes to the U i are isomorphisms is an isomorphism; the base changes {X_{U i} ⟶ X_T} form an fpqc covering of X_T by Stacks 03MR, and invertibility descends along it by Stacks 04W8, AlgebraicGeometry.Space.reflectsIsoAlongFpqcCovering, the base-changed modules being quasi-coherent by Stacks 03GA.

theorem isSheafFor_isomFunctor_of_isFpqcCovering {I : Type v} {T : s.SchemesOver}
    {U : I → s.SchemesOver} (g : ∀ i, U i ⟶ T)
    (hg : IsFpqcCovering B S hS fun i ↦ ((schemeSpaceFunctor B S hS).map (g i).left).hom) :
    Presieve.IsSheafFor s.isomFunctor (Presieve.ofArrows U g)

Tag 0D3T, a lemma

Tag 0D3T in the Stacks Project.

AlgebraicGeometry.Space.HomSituation.baseOfIsomMor_isomMorOfSpaceIsom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Hom/IsomFunctorMorphisms.lean, line 586. The attribute's comment: “the first component of the pair is recovered from the morphism of sheaves into the Isom functor, conditional on the pseudofunctoriality of the direct images of Stacks 03LU”.

The morphism to the base is recovered from the morphism of presheaves into the Isom presheaf: for a pair (h, u) with u invertible the morphism underlying isomMorOfSpaceIsom (h, u) is h. This is the half of Stacks 0D3T that needs no descent, and it is inherited from the corresponding half of Stacks 0D3S, AlgebraicGeometry.Space.HomSituation.baseOfMor_morOfSpaceHom, the two left-hand sides being compared through the inclusion of the subfunctor.

theorem baseOfIsomMor_isomMorOfSpaceIsom (hc : ModulePushforwardCoherence B S hS)
    {T : AlgebraicSpaces B S hS} (h : T ⟶ s.base) (u : s.spaceHomAt (Over.mk h))
    (hu : s.IsIsomOverAt u) :
    s.baseOfIsomMor hc (s.isomMorOfSpaceIsom hc h u hu) = h

AlgebraicGeometry.Space.HomSituation.bijective_isomMorOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Hom/IsomFunctorMorphisms.lean, line 678. The attribute's comment: “the identification is a bijection on the fibres over a fixed morphism to the base; carries three hypotheses: hc, the pseudofunctoriality of the direct images of Stacks 03LU, and hd, hd', the fullness clause of Stacks 04W8 for a one-member etale covering, for the two modules of the situation and for them exchanged (the faithfulness clause of Stacks 04W8 is proved here and not assumed)”.

Stacks 0D3T, the fibres of the identification. For a fixed morphism h : T ⟶ base of algebraic spaces over S, the assignment u ↦ isomMorOfSpaceIsom (h, u) is a bijection from the isomorphisms u : F_T ⟶ G_T of the two modules pulled back to X ×_{base, h} T onto the morphisms of presheaves T ⟶ Isom(F, G) lying over h.

Together with AlgebraicGeometry.Space.HomSituation.baseOfIsomMor_isomMorOfSpaceIsom, which recovers the first component, this is the identification Mor(T, Isom(F, G)) = {(h, u) | h : T ⟶ base, u : F_T ⟶ G_T an isomorphism} of Stacks 0D3T.

This is the argument of the source: both sides are cut out of the two sides of Stacks 0D3S, and what is checked is that the subsets correspond. Injectivity is inherited from Stacks 0D3S and is unconditional beyond the coherence hc. Surjectivity needs, beyond the hypothesis hd of Stacks 0D3S, that invertibility descends along the covering of base changes cut out by a scheme atlas of T, which is the same fullness clause of Stacks 04W8 for the reversed pair of modules, carried as hd'.

theorem bijective_isomMorOver (hc : ModulePushforwardCoherence B S hS)
    (hd : s.EtaleHomDescent) (hd' : s.EtaleReverseHomDescent)
    {T : AlgebraicSpaces B S hS} (h : T ⟶ s.base) :
    Function.Bijective (s.isomMorOver hc h)

AlgebraicGeometry.Space.HomSituation.bijective_isomMorOfSpaceIsom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Hom/IsomFunctorMorphismsEquiv.lean, line 65. The attribute's comment: “the whole identification: the map (h, u) |-> the morphism T -> Isom(F, G) is a bijection from all pairs of h : T -> base and an isomorphism u : F_T -> G_T onto all morphisms from T into Isom(F, G), for any algebraic space T over S, with no hypothesis”.

Let T be an algebraic space over S. The assignment (h, u) ↦ isomMorOfSpaceIsom (h, u) is a bijection from the pairs of a morphism h : T ⟶ base and an isomorphism u : F_T ⟶ G_T of the modules pulled back to X ×_{base, h} T onto the morphisms of presheaves T ⟶ Isom(F, G) on the big fppf site of S:

Mor(T, Isom(F, G)) = {(h, u) | h : T ⟶ base, u : F_T ⟶ G_T an isomorphism}.

Here Isom(F, G) is the presheaf built from the pseudofunctoriality of direct images AlgebraicGeometry.Space.modulePushforwardCoherence.

theorem bijective_isomMorOfSpaceIsom (T : AlgebraicSpaces B S hS) :
    Function.Bijective (fun p : (Σ h : T ⟶ s.base,
        {u : s.spaceHomAt (Over.mk h) // s.IsIsomOverAt u}) =>
      s.isomMorOfSpaceIsom (modulePushforwardCoherence B S hS) p.1 p.2.1 p.2.2)

Tag 08K9, a proposition

Tag 08K9 in the Stacks Project.

AlgebraicGeometry.Space.HomSituation.isAffineFinitePresentationAlgebraicSpaceOver_isomFunctor_of_hasProperSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeIsomAffineFinitePresentation.lean, line 56. The attribute's comment: “Isom(F, G) is an algebraic space affine of finite presentation over B, for f of finite presentation and F, G of finite presentation, flat over B, with support proper over B”.

In Situation 08JT assume that f : X ⟶ B is of finite presentation and that 𝓕 and 𝒢 are finitely presented 𝒪_X-modules, flat over B, with support proper over B. Then the functor Isom(𝓕, 𝒢) is an algebraic space affine of finite presentation over B.

theorem isAffineFinitePresentationAlgebraicSpaceOver_isomFunctor_of_hasProperSupport
    (s : HomSituation B S hS) (hfp : IsFinitePresentation B S hS s.f.hom)
    (hF : s.F.IsFinitePresentationOnSite) (hG : s.G.IsFinitePresentationOnSite)
    (hFflat : IsFlatOver B S hS s.X.2 s.f.hom s.F)
    (hGflat : IsFlatOver B S hS s.X.2 s.f.hom s.G)
    (hFsupp : HasProperSupport B S hS s.X.2 s.base.2 s.f.hom
      (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation B S hS hfp.1)
      ((SheafOfModules.toSheaf _).obj s.F))
    (hGsupp : HasProperSupport B S hS s.X.2 s.base.2 s.f.hom
      (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation B S hS hfp.1)
      ((SheafOfModules.toSheaf _).obj s.G)) :
    IsAffineFinitePresentationAlgebraicSpaceOver s.base s.isomFunctor

AlgebraicGeometry.Space.HomSituation.mutualInverseFunctorIsoIsom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeIsomMutualInverse.lean, line 272. The attribute's comment: “ONLY the identification Isom(F,G) = (H' x_B H) x_{c, I x_B I', sigma} B that the proof rests on, with no hypothesis on f, F or G. The conclusion of Stacks 08K9 — that Isom(F,G) is an algebraic space affine of finite presentation over B — is NOT covered. It needs, first, the conclusion of Stacks 08K6 for the four Hom functors, which this development does not have (Stacks 08K6 in turn needs Stacks 08JY, 08JV, 07V7 and 08K2, of which only Stacks 08K2 is proved in this library, as AlgebraicGeometry.Space.MorphismDescentSituation.exists_isProperOver_supportOfSheaf_moduleAt); and second, stability of AlgebraicGeometry.Space.IsAffineHom and of AlgebraicGeometry.Space.IsFinitePresentation under base change along a morphism of algebraic spaces, which this library does not prove — only isAffineHom_comp and isLocallyOfFinitePresentation_of_comp exist — and which the fibre-product step needs. The remaining inputs of the source's proof, Stacks 03KP parts (1)-(4) and Stacks 05WT, ARE available, in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedCriteria.lean and StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FinitePresentation.lean”. References: SGA 6 XII (2.4), “partial”.

The functor of mutually inverse pairs (H' ×_B H) ×_{c, I ×_B I', σ} B is isomorphic to the relative Isom functor Isom(F, G) of Stacks 08K7.

def mutualInverseFunctorIsoIsom : s.mutualInverseFunctor ≅ s.isomFunctor

Sources

Section99.5 The stack of coherent sheaves #

Section 99.5 of the Stacks Project, Tag 08KA. 12 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08KB, a situation

Tag 08KB in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStack.lean, line 217. The attribute's comment: “the relative algebraic space”.

Stacks 08KB, the standing data. A morphism f : X ⟶ Y of algebraic spaces over S of finite presentation: the relative algebraic space whose coherent sheaves with proper support the category Coh_{X/Y} classifies.

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

AlgebraicGeometry.Space.CoherentObject, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStack.lean, line 404. The attribute's comment: “objects”.

Stacks 08KB, the objects. An object of Coh_{X/Y}: a scheme T of the site over Y together with a quasi-coherent 𝒪_{X_T}-module of finite presentation which is flat over T and whose support is proper over T.

structure CoherentObject (D : CoherentSituation B S hS)

AlgebraicGeometry.Space.CoherentHom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStack.lean, line 427. The attribute's comment: “morphisms”.

Stacks 08KB, the morphisms. A morphism of Coh_{X/Y}: a morphism h : T ⟶ T' of test schemes over Y together with an isomorphism (X_h)^*F' ⟶ F of 𝒪_{X_T}-modules.

structure CoherentHom {D : CoherentSituation B S hS} (A A' : CoherentObject D)

AlgebraicGeometry.Space.CoherentSituation.categoryData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackCategory.lean, line 227. The attribute's comment: “the category structure on Coh_{X/Y}: the identity and associativity laws, which Stacks 08KB asserts by designation and this library had left unverified”.

Coh_{X/Y} is a category, for the canonical pseudofunctoriality datum AlgebraicGeometry.Space.modulePushforwardCoherence of the direct images of Stacks 03LU.

def categoryData : CoherentCategoryData (modulePushforwardCoherence B S hS) D

Tag 08W5, a lemma

Tag 08W5 in the Stacks Project.

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

In the situation of Stacks 08KB the projection p : Coh_{X/Y} ⟶ (Sch/S)_fppf, which sends an object (T, g, F) to its test scheme T, is fibred in groupoids.

theorem projection_isFiberedInGroupoids :
    letI : Category.{u + 1} (CoherentObject D) := D.categoryData.category
    Functor.IsFiberedInGroupoids
      (D.categoryData.projection ⋙ CostructuredArrow.proj (schemeSpaceFunctor B S hS) D.Y)

AlgebraicGeometry.Space.coherentProjection_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackFibered.lean, line 475. The attribute's comment: “conditional on the three cited base-change stability results 05VW, 0CZJ and 03DO(7)”.

Stacks 08W5. In the situation of Stacks 08KB the projection p : Coh_{X/Y} ⟶ (Sch/S)_fppf, which sends an object (T, g, F) to its test scheme T, is fibred in groupoids.

The projection of Coh_{X/Y} to the test schemes over Y is fibred in groupoids by AlgebraicGeometry.Space.coherentProjection_isFiberedInGroupoids_schemesOver, the projection of the test schemes over Y to the schemes of the site is fibred in groupoids by CategoryTheory.Functor.IsFiberedInGroupoids.costructuredArrow_proj, and Stacks 09WW composes the two.

This carrier is conditional, and so asserts less than the tag. Stacks 08W5 is unconditional; the hst : ModulePullbackStability B S hS hypothesis stands in for three cited results that the library does not yet carry — 05VW (flatness under base change), 0CZJ (proper support under base change) and clause (7) of 03DO (finite presentation of a pullback) — each stated in that structure at the generality of its own source page. The attribute is qualified accordingly, and no unqualified 08W5 claim is made here. Discharging those three fields turns this into the tag itself with no change to the statement below.

theorem coherentProjection_isFiberedInGroupoids
    (hc : ModulePushforwardCoherence B S hS) (hst : ModulePullbackStability B S hS)
    {D : CoherentSituation B S hS} (cd : CoherentCategoryData hc D) :
    letI : Category.{u + 1} (CoherentObject D) := cd.category
    Functor.IsFiberedInGroupoids
      (cd.projection ⋙ CostructuredArrow.proj (schemeSpaceFunctor B S hS) D.Y)

AlgebraicGeometry.Space.coherentProjection_isFiberedInGroupoids', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackFiberedUnconditional.lean, line 178. The attribute's comment: “for a given category structure on the objects”.

Stacks 08W5. In the situation of Stacks 08KB the projection p : Coh_{X/Y} ⟶ (Sch/S)_fppf, which sends an object (T, g, F) to its test scheme T, is fibred in groupoids.

theorem coherentProjection_isFiberedInGroupoids'
    (hc : ModulePushforwardCoherence B S hS) {D : CoherentSituation B S hS}
    (cd : CoherentCategoryData hc D) :
    letI : Category.{u + 1} (CoherentObject D) := cd.category
    Functor.IsFiberedInGroupoids
      (cd.projection ⋙ CostructuredArrow.proj (schemeSpaceFunctor B S hS) D.Y)

Tag 08W6, a lemma

Tag 08W6 in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation.coherentCFG_diagonal_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/CoherentStackDiagonalRepresentable.lean, line 65.

Stacks 08W6. In Situation 08KB, with 𝒳 = Coh_{X/Y} the stack of coherent sheaves with proper support of a morphism f : X ⟶ Y of finite presentation of algebraic spaces over S, the diagonal Δ : 𝒳 ⟶ 𝒳 × 𝒳 is representable by algebraic spaces.

theorem coherentCFG_diagonal_isRepresentableByAlgebraicSpaces (D : CoherentSituation B S hS) :
    Stack.IsRepresentableByAlgebraicSpaces B S hS
      (Stack.diagonalBasedFunctor B S hS D.coherentCFG)

Tag 08KC, a lemma

Tag 08KC in the Stacks Project.

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

Stacks 08KC. In Situation 08KB the projection Coh_{X/Y} ⟶ (Sch/S)_fppf, (T, g, F) ↦ T, makes the category Coh_{X/Y} of Stacks 08KB a stack in groupoids over the big fppf site of S.

theorem isStackInGroupoids :
    (coherentBasedCategory D.categoryData).p.IsStackInGroupoids.{w}
      (BigFppfOver.topology B S hS)

Tag 08LP, a remark

Tag 08LP in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation.canonicalBaseChangeSquare_isTwoFibreProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackCanonical.lean, line 98. The attribute's comment: “the base-change square is 2-cartesian”.

The square Coh_{X'/Y'} ⟶ Coh_{X/Y}, 𝒮_{Y'} ⟶ 𝒮_Y is 2-cartesian: Coh_{X'/Y'}, with the base-change functor and the projection forgetting the module, is a 2-fibre product of the projection Coh_{X/Y} ⟶ 𝒮_Y with the morphism 𝒮_{Y'} ⟶ 𝒮_Y.

def canonicalBaseChangeSquare_isTwoFibreProduct (g : Y' ⟶ D.Y) :
    Bicategory.IsTwoFibreProduct (D.canonicalBaseChangeSquare g)

AlgebraicGeometry.Space.coherentToBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackProjection.lean, line 187. The attribute's comment: “the projection to the base”.

Stacks 08LP, the projection to the base. The rule (T, g, ℱ) ↦ (T, g) which forgets the module is a 1-morphism Coh_{X/Y} ⟶ 𝒮_Y of categories over the big fppf site of S: it lands in the test schemes over Y by construction, and the scheme it names is the one Coh_{X/Y} already projects to.

def coherentToBase (cd : CoherentCategoryData hc D) :
    coherentBasedCategory cd ⥤ᵇ baseBasedCategory D.Y

Tag 08KD, a lemma

Tag 08KD in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation.isLimitPreserving_coherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackLimitFlatProperSupport.lean, line 706. The attribute's comment: “at a small index category”.

Stacks 08KD. In Situation 08KB, let f : X ⟶ Y be a morphism of finite presentation of algebraic spaces over S and assume Y locally of finite presentation over S. Then Coh_{X/Y} is limit preserving in the sense of Artin's Axioms, Definition 07XL: for every cofiltered inverse system of affine schemes T_j of the big fppf site, indexed by a category in the scheme universe, whose limit T in schemes lies in the site, the comparison functor colim Coh_{X/Y, T_j} ⥤ Coh_{X/Y, T} is an equivalence.

The index category is taken in the scheme universe, which is the smallness the source's directed sets have, as in AlgebraicGeometry.isLimitPreservingPolarizedUnconditional.

theorem isLimitPreserving_coherent
    (hY : IsLocallyOfFinitePresentation B S hS (terminal.from D.Y.1)) :
    Deformation.Artin.IsLimitPreserving.{u, u, u} B S hS D.coherentCFG

Tag 08LQ, a lemma

Tag 08LQ in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation.fiberSquareComparison_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackPushoutModules.lean, line 485.

Stacks Project, Tag 08LQ. In Situation 08KB, let f : X ⟶ B be a morphism of algebraic spaces over S of finite presentation, and let
  Z ---i---> Z'
  |          |
  f          a
  v          v
  Y ---b---> Y'
be a pushout in the category of schemes over S with Z ⟶ Z' a thickening and Z ⟶ Y affine (Stacks 07RT). Then the functor on fibre categories Coh_{X/B, Y'} ⟶ Coh_{X/B, Y} ×_{Coh_{X/B, Z}} Coh_{X/B, Z'} is an equivalence.

Here Coh_{X/B} is the category of AlgebraicGeometry.Space.CoherentSituation.categoryData fibred over the schemes over S by AlgebraicGeometry.Space.coherentSiteProjection, and the functor is Deformation.Artin.fiberSquareComparison at its chosen pullbacks, for the square f ≫ b = i ≫ a of schemes over S, which commutes by AlgebraicGeometry.Space.CoherentSituation.comm_of_isPushout_toScheme.

The proof follows the source: the map B(Y') ⟶ B(Y) ×_{B(Z)} B(Z') is bijective (Stacks 07SY), which fixes the morphism Y' ⟶ B (fiberSquareComparison_isEquivalence_of_modulesGlueOver), and the statement becomes Stacks 08KV for the base change X ×_B Y' ⟶ Y' (modulesGlueOver_of_isPushout).

theorem fiberSquareComparison_isEquivalence (D : CoherentSituation B S hS)
    {Z Z' Y Y' : BigFppfOver B S hS} (i : Z ⟶ Z') (f : Z ⟶ Y) (a : Z' ⟶ Y') (b : Y ⟶ Y')
    (hi : Stacks.Thickenings.IsThickening ((BigFppfOver.toScheme B S hS).map i))
    [AlgebraicGeometry.IsAffineHom ((BigFppfOver.toScheme B S hS).map f)]
    (hsq : IsPushout ((BigFppfOver.toScheme B S hS).map i)
      ((BigFppfOver.toScheme B S hS).map f) ((BigFppfOver.toScheme B S hS).map a)
      ((BigFppfOver.toScheme B S hS).map b)) :
    letI : Category.{u + 1} (CoherentObject D) := D.categoryData.category
    letI : (coherentSiteProjection D.categoryData).IsFibered :=
      D.isFiberedInGroupoids_siteProjection.isFibered
    (Deformation.Artin.fiberSquareComparison (coherentSiteProjection D.categoryData)
      (coherentSiteProjection D.categoryData).chosenPullbacks f i b a
        (comm_of_isPushout_toScheme hsq)).IsEquivalence

Tag 08W7, a lemma

Tag 08W7 in the Stacks Project.

AlgebraicGeometry.Space.isFinitePresentationOnSite_tfae_of_isPullback_of_isFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackThickeningFinitePresentation.lean, line 102.

Stacks 08W7. Let X ⟶ X' over T ⟶ T' be a cartesian square of algebraic spaces in which t : T ⟶ T' is a first order thickening, let ℱ' be an 𝒪_{X'}-module flat over T' and set ℱ = i^*ℱ'. Then the following are equivalent: (1) ℱ' is a quasi-coherent 𝒪_{X'}-module of finite presentation; (2) ℱ' is an 𝒪_{X'}-module of finite presentation; (3) ℱ is a quasi-coherent 𝒪_X-module of finite presentation; (4) ℱ is an 𝒪_X-module of finite presentation.

theorem isFinitePresentationOnSite_tfae_of_isPullback_of_isFirstOrderThickening
    {T T' X X' : AlgebraicSpaces B S hS} (t : T ⟶ T') [Mono t.hom]
    (ht : IsFirstOrderThickening B S hS T' (Subfunctor.range t.hom))
    (i : X ⟶ X') (f : X ⟶ T) (f' : X' ⟶ T') (hsq : IsPullback i f f' t)
    (F' : Modules.{u, u} B S hS X'.1 X'.2) (hflat : IsFlatOver B S hS X'.2 f'.hom F') :
    List.TFAE
      [F'.IsQuasicoherentOnSite ∧ F'.IsFinitePresentationOnSite,
        F'.IsFinitePresentationOnSite,
        ((modulePullback B S hS i).obj F').IsQuasicoherentOnSite ∧
          ((modulePullback B S hS i).obj F').IsFinitePresentationOnSite,
        ((modulePullback B S hS i).obj F').IsFinitePresentationOnSite]

Tag 08W8, a lemma

Tag 08W8 in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation.finiteDimensional_tangentSpace_and_infinitesimalAutomorphisms_cohDef, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackInfFinite.lean, line 686.

Stacks 08W8. In Situation 08KB (f : X ⟶ Y of finite presentation) assume that S is locally Noetherian and Y ⟶ S locally of finite presentation. Let k be a field of finite type over S, with Spec Λ ⊆ S an affine open through which Spec k ⟶ S factors and Λ → k finite as in Section 07T2, and let x₀ = (Spec k, g₀, 𝒢₀) be an object of Coh_{X/Y} over Spec k. Then the tangent space T𝓕 and the infinitesimal automorphisms Inf(𝓕) of 𝓕 = 𝓕_{Coh_{X/Y}, k, x₀} are finite-dimensional over k. The vector-space structures are those of the deformation category 𝓕 (Stacks 07WU with Stacks 07WQ), which the conclusion records.

The conclusion spells out the two clauses of Deformation.IsFiniteDimensionalDeformationCategory: that predicate asks the morphisms of 𝓕 to live in the universe of the rings of 𝒞_Λ, while the morphisms of Coh_{X/Y}, which carry morphisms of sheaves of modules, live one universe higher.

theorem finiteDimensional_tangentSpace_and_infinitesimalAutomorphisms_cohDef
    [IsLocallyNoetherian S]
    (hlfp : IsLocallyOfFinitePresentation B S hS (terminal.from D.Y.1)) [Module.Finite Λ k]
    (hiΛ : AlgebraicGeometry.IsOpenImmersion iΛ)
    (hfinite : AlgebraicGeometry.LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      AlgebraicGeometry.QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    ∃ hp : IsDeformationCategory.{u, u, u} (D.cohDef iΛ x₀ hx₀).projection,
      (letI : Fact (IsPredeformationCategory.{u, u, u}
          (BasedCategory.ofFunctor (D.cohDef iΛ x₀ hx₀).projection).p) := ⟨hp.predeformation⟩;
        letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
          (isomorphismClasses (BasedCategory.ofFunctor (D.cohDef iΛ x₀ hx₀).projection)
            hp.predeformation.cofibered))) := ⟨tangentConditionS2.{u, u, u} hp⟩;
        FiniteDimensional k (tangentSpaceArtinian.{u, u, u} Λ k
          (isomorphismClasses (BasedCategory.ofFunctor (D.cohDef iΛ x₀ hx₀).projection)
            hp.predeformation.cofibered))) ∧
      ∀ (x : (D.cohDef iΛ x₀ hx₀).carrier),
        (D.cohDef iΛ x₀ hx₀).projection.obj x = Deformation.residueFieldObject.{u, u, u} Λ k →
        ∀ PF : ChosenPushforwardsAt (D.cohDef iΛ x₀ hx₀).projection x, FiniteDimensional k
          ↥((infinitesimalAutomorphismLinearLift.{u, u, u} PF hp.satisfiesRS).functor.obj
            (FGModuleCat.of k (ULift.{u} k)))

Tag 08W9, a lemma

Tag 08W9 in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation.isEquivalence_approximationFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackApproximation.lean, line 942.

In Situation 08KB, with f : X ⟶ Y separated, the functor of Artin's Axioms, Equation 07X6, at Coh_{X/Y} — from objects over spectra of Noetherian complete local rings with residue field of finite type over S to formal objects — is an equivalence. No Noetherian hypothesis on S is assumed.

theorem isEquivalence_approximationFunctor (hsep : IsSeparated B S hS D.f.hom) :
    letI : Category.{u + 1} (CoherentObject D) := D.categoryData.category
    D.approximationFunctor.IsEquivalence

Tag 08WA, a lemma

Tag 08WA in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation.hasOpenVersality_coherentCFG_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackOpenVersalityOfFlat.lean, line 49.

Openness of versality for Coh_{X/B} (Stacks 08WA). In Situation Stacks 08KB assume that S is a locally Noetherian scheme, S = B (here: the base Y is final) and f : X → B is flat. Then 𝒳 = Coh_{X/B} satisfies openness of versality (Stacks 07XQ).

This is the second proof of the source, through Stacks 0CYF: the diagonal of 𝒳 is representable by algebraic spaces (Stacks 08W6), 𝒳 satisfies (RS*) (Stacks 08LQ) and is limit preserving (Stacks 08KD), and over a Noetherian affine chart x = (Spec A, ℱ) the tangent space is T_x(M) = Ext¹_{X_A}(ℱ, ℱ ⊗ f^*M̃), naturally in M, and the obstruction class of a square-zero thickening A' → A with kernel I lies in Ext²_{X_A}(ℱ, ℱ ⊗ f^*Ĩ), functorially along surjections of thickenings (Stacks 08VW, 0CYE).

theorem hasOpenVersality_coherentCFG_of_isFlat
    [_root_.AlgebraicGeometry.IsLocallyNoetherian S] (hY : IsTerminal D.Y)
    (hflat : IsFlat B S hS D.f.hom) :
    HasOpenVersality ((coherentCFG D).val.p ⋙ Over.post B.inclusion)

Tag 08WC, a theorem

Tag 08WC in the Stacks Project.

AlgebraicGeometry.Space.CoherentSituation.isAlgebraicStack_coherentCFG_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackAlgebraicFlat.lean, line 40.

Algebraicity of the stack of coherent sheaves, flat case. Let S be a scheme and f : X ⟶ B a morphism of algebraic spaces over S which is of finite presentation (a field of the standing datum D of Situation 08KB), separated and flat. Then Coh_{X/B} is an algebraic stack over S.

theorem isAlgebraicStack_coherentCFG_of_isFlat.{w} {B : BigFppfSite.{u}} {S : Scheme.{u}}
    {hS : B.Contains S} (D : CoherentSituation B S hS) (hsep : IsSeparated B S hS D.f.hom)
    (hflat : IsFlat B S hS D.f.hom) :
    Stack.IsAlgebraicStack.{u, w} B S hS D.coherentCFG.val

Sources

LeanAlgebraicGeometry.Space.CoherentSituation · AlgebraicGeometry.Space.CoherentObject · AlgebraicGeometry.Space.CoherentHom · AlgebraicGeometry.Space.CoherentSituation.categoryData · AlgebraicGeometry.Space.CoherentSituation.projection_isFiberedInGroupoids · AlgebraicGeometry.Space.coherentProjection_isFiberedInGroupoids · AlgebraicGeometry.Space.coherentProjection_isFiberedInGroupoids' · AlgebraicGeometry.Space.CoherentSituation.coherentCFG_diagonal_isRepresentableByAlgebraicSpaces

Section99.6 The stack of coherent sheaves in the non-flat case #

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

Tag 09DS, a theorem

Tag 09DS in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicStack_coherentCFG, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackIsAlgebraic.lean, line 35.

Algebraicity of the stack of coherent sheaves. Let S be a scheme and let f : X ⟶ Y be a morphism of algebraic spaces over S, of finite presentation (part of the standing datum D of Situation 08KB) and separated. Then Coh_{X/Y} is an algebraic stack over S.

theorem isAlgebraicStack_coherentCFG.{w} {B : BigFppfSite.{u}} {S : Scheme.{u}}
    {hS : B.Contains S} (D : CoherentSituation B S hS) (hsep : IsSeparated B S hS D.f.hom) :
    Stack.IsAlgebraicStack.{u, w} B S hS (coherentCFG D).val

Sources

LeanAlgebraicGeometry.Space.isAlgebraicStack_coherentCFG

Section99.7 The functor of quotients #

Section 99.7 of the Stacks Project, Tag 082L. 12 tags here are carried by 48 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 082M, a situation

Tag 082M in the Stacks Project.

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

Stacks 082M, the standing data. A morphism f : X ⟶ Y of algebraic spaces over S together with a quasi-coherent 𝒪_X-module F: the data whose quotients, flat over the test scheme, the functor of quotients of F/X/Y classifies.

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

AlgebraicGeometry.Space.QuotientSituation.mk_kernel_quotientProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctor.lean, line 158. The attribute's comment: “the identification of two quotients of F_T that have the same kernel: the submodules of F_T list the quotients of F_T once each”.

The kernel of the projection F_T ⟶ F_T / K is K again. Together with surjectivity of the projection this says that the submodules of F_T list the quotients of F_T once each, which is the source's identification of two quotients with the same kernel.

theorem mk_kernel_quotientProjection (T : SchemesOver D.Y)
    (K : Subobject (D.baseChangeModule T)) :
    Subobject.mk (kernel.ι (D.quotientProjection T K)) = K

AlgebraicGeometry.Space.QuotientSituation.quotients, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctor.lean, line 178. The attribute's comment: “the set of quotients”.

Stacks 082M. The set Q_{F/X/Y}(T) of quotients of F_T which are quasi-coherent and flat over the test scheme T, the two conditions of the source.

A quotient of F_T is recorded by its kernel, a submodule K of F_T, the quotient itself being F_T / K; this is exactly the source's identification of two quotients of F_T that have the same kernel.

def quotients (T : SchemesOver D.Y) : Set (Subobject (D.baseChangeModule T))

AlgebraicGeometry.Space.QuotientSituation.finitePresentationQuotients, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctor.lean, line 185. The attribute's comment: “the finite-presentation subfunctor”.

Stacks 082M. The subset Q^{fp}_{F/X/Y}(T) of Q_{F/X/Y}(T) consisting of those quotients F_T ⟶ Q for which Q is of finite presentation as an 𝒪_{X_T}-module.

def finitePresentationQuotients (T : SchemesOver D.Y) :
    Set (Subobject (D.baseChangeModule T))

AlgebraicGeometry.Space.QuotientSituation.quotientPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorPullback.lean, line 171. The attribute's comment: “the pullback Q' = (X_{T'} ⟶ X_T)^*Q of a quotient of F_T along a morphism T' ⟶ T of test schemes over Y”.

The pullback of a quotient of F_T along a morphism h : T' ⟶ T of test schemes, Q ↦ (X_{T'} ⟶ X_T)^*Q, recorded by its kernel.

def quotientPullback {T' T : SchemesOver D.Y} (h : T' ⟶ T)
    (K : Subobject (D.baseChangeModule T)) : Subobject (D.baseChangeModule T')

AlgebraicGeometry.Space.QuotientSituation.quotientPullback_mem_quotients', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorPullback.lean, line 247. The attribute's comment: “the pullback clause: if F_T ⟶ Q is an element of Q_{F/X/Y}(T) and T' ⟶ T is a morphism of schemes over Y, then Q' = (X_{T'} ⟶ X_T)^*Q is a quasi-coherent 𝒪_{X_{T'}}-module flat over T', so it is an element of Q_{F/X/Y}(T')”.

The pullback of a quotient of F_T which is quasi-coherent and flat over T is quasi-coherent and flat over T'.

theorem quotientPullback_mem_quotients' {T' T : SchemesOver D.Y} (h : T' ⟶ T)
    (K : Subobject (D.baseChangeModule T)) (hK : K ∈ D.quotients T) :
    D.quotientPullback h K ∈ D.quotients T'

AlgebraicGeometry.Space.QuotientSituation.quotientPullback_mem_finitePresentationQuotients, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorPullback.lean, line 259. The attribute's comment: “Q^{fp}_{F/X/Y} is a subfunctor of Q_{F/X/Y}: finite presentation of a quotient is preserved by the pullback along a morphism of test schemes, so the finitely presented quotients are stable under the transition maps”.

The pullback of a finitely presented quotient is a finitely presented quotient.

theorem quotientPullback_mem_finitePresentationQuotients {T' T : SchemesOver D.Y} (h : T' ⟶ T)
    (K : Subobject (D.baseChangeModule T)) (hK : K ∈ D.finitePresentationQuotients T) :
    D.quotientPullback h K ∈ D.finitePresentationQuotients T'

AlgebraicGeometry.Space.QuotientSituation.quotientsFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorPullback.lean, line 319. The attribute's comment: “the functor Q_{F/X/Y} : (Sch/Y)ᵒᵖ ⥤ Sets obtained from the pullback clause, through its value at a test scheme T over Y, which is the set Q_{F/X/Y}(T)”.

The value of the functor of quotients at a test scheme T over Y is the set Q_{F/X/Y}(T).

theorem quotientsFunctor_obj (T : SchemesOver D.Y) :
    D.quotientsFunctor.obj (Opposite.op T) = D.quotients T

AlgebraicGeometry.Space.QuotientSituation.quotientsFunctor_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorPullback.lean, line 327. The attribute's comment: “the functor Q_{F/X/Y} : (Sch/Y)ᵒᵖ ⥤ Sets obtained from the pullback clause, through its transition maps, which are the pullback Q ↦ (X_{T'} ⟶ X_T)^*Q of quotients”.

The action of the functor of quotients on a morphism of test schemes is pullback of quotients.

theorem quotientsFunctor_map {T' T : SchemesOver D.Y} (h : T' ⟶ T)
    (K : Subobject (D.baseChangeModule T)) (hK : K ∈ D.quotients T) :
    (D.quotientsFunctor.map (Opposite.op h)
      ⟨K, hK⟩ : D.quotients T').1 = D.quotientPullback h K

AlgebraicGeometry.Space.QuotientSituation.finitePresentationQuotientsFunctorToQuotientsFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorPullback.lean, line 356. The attribute's comment: “Q^{fp}_{F/X/Y} : (Sch/Y)ᵒᵖ ⥤ Sets is a subfunctor of Q_{F/X/Y}: the inclusion of the finitely presented quotients into all of them is a morphism of functors”.

The finite-presentation subfunctor is a subfunctor of the functor of quotients: at every test scheme its value is a subset of the value of AlgebraicGeometry.Space.QuotientSituation.quotientsFunctor, and the two actions agree.

def finitePresentationQuotientsFunctorToQuotientsFunctor :
    D.finitePresentationQuotientsFunctor ⟶ D.quotientsFunctor

AlgebraicGeometry.Space.QuotientSituation.sourceRestricted, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorSourceSheaf.lean, line 210. The attribute's comment: “the standing data on a member of a covering of the source”.

Situation 082M on a member of a covering of the source. For a morphism a : W ⟶ X of algebraic spaces, the standing data consisting of W, the composite a ≫ f : W ⟶ Y and the pullback a^*F of the module.

Its functor of quotients is the source's Q_{F i/X i/Y} when a is a member of a covering of X, and the source's Q_{F ijk/X ijk/Y} when a is the composite X ijk ⟶ X i ×_X X j ⟶ X: in both cases the module is the pullback of F to the member, which is what the source writes.

Quasi-coherence of a^*F is Stacks 03GA, which holds along an arbitrary morphism of algebraic spaces by AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePullback_of_isQuasicoherentOnSite of StacksFrontier/AlgebraicGeometry/Spaces/ModulePullbackQuasicoherentFromChartDiagrams.lean, so no local-presentation hypothesis on a is asked for.

It is made reducible below so that the identifications (D.sourceRestricted a).Y = D.Y and (D.sourceRestricted a).f = a ≫ D.f, on which the types of the restriction maps below depend, are available to the unifier.

def sourceRestricted {W : AlgebraicSpaces B S hS} (a : W ⟶ D.X) :
    QuotientSituation B S hS

Tag 082N, an equation

Tag 082N in the Stacks Project.

AlgebraicGeometry.Space.QuotientSituation.quotientsFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorPullback.lean, line 305. The attribute's comment: “the functor of quotients Q_{F/X/Y} of F/X/Y, with its two functor laws and the stability of the quotients of the source under pullback along a morphism of test schemes”. References: SGA 3 XV (3.8), “more general”.

The functor of quotients of F/X/Y, Q_{F/X/Y} : (Sch/Y)ᵒᵖ ⥤ Sets: its value at a test scheme T over Y is the set Q_{F/X/Y}(T) of quotients of F_T that are quasi-coherent and flat over T, and its action on a morphism of test schemes is pullback of quotients.

def quotientsFunctor : (SchemesOver D.Y)ᵒᵖ ⥤ Type (u + 1)

Tag 0CZL, an equation

Tag 0CZL in the Stacks Project.

AlgebraicGeometry.Space.QuotientSituation.finitePresentationQuotientsFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorPullback.lean, line 338. The attribute's comment: “the finite-presentation subfunctor Q^{fp}_{F/X/Y} of the functor of quotients”.

The finite-presentation subfunctor Q^{fp}_{F/X/Y} : (Sch/Y)ᵒᵖ ⥤ Sets of the functor of quotients: its value at a test scheme T is the subset of Q_{F/X/Y}(T) of those quotients that are of finite presentation as 𝒪_{X_T}-modules, and its action on a morphism of test schemes is pullback of quotients.

def finitePresentationQuotientsFunctor : (SchemesOver D.Y)ᵒᵖ ⥤ Type (u + 1)

Tag 08IT, a remark

Tag 08IT in the Stacks Project.

AlgebraicGeometry.Space.QuotientSituation.canonicalBaseChangedSituation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorBaseChange.lean, line 497. The attribute's comment: “the base-changed situation F'/X'/B'”.

The standing data of Stacks 082M obtained by changing the base algebraic space along p : B' ⟶ B: source X' = X ×_B B', morphism the second projection, module the pullback F' of F, quasi-coherent by Stacks 03GA.

abbrev canonicalBaseChangedSituation : QuotientSituation B S hS

AlgebraicGeometry.Space.QuotientSituation.canonicalBaseChangeQuotientModuleIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorBaseChange.lean, line 505. The attribute's comment: “the identification of the quotients themselves, F'_T/K' = F_T/K under X'_T ≅ X_T”.

The quotients themselves correspond, at the canonical pseudofunctoriality datum: the quotient F'_T/K' named by the subobject corresponding to K is the inverse image along X'_T ≅ X_T of the quotient F_T/K.

def canonicalBaseChangeQuotientModuleIso (T : SchemesOver Y')
    (K : Subobject (D.baseChangeModule ((CostructuredArrow.map p).obj T))) :
    (D.canonicalBaseChangedSituation p).quotientModule T
        (D.baseChangeSubobjectEquiv p (D.isQuasicoherentOnSite_baseChangedSourceModule p)
          (modulePushforwardCoherence B S hS) T K) ≅
      (modulePullback B S hS
          (D.baseChangeFiberIso p (D.isQuasicoherentOnSite_baseChangedSourceModule p) T).hom).obj
        (D.quotientModule ((CostructuredArrow.map p).obj T) K)

AlgebraicGeometry.Space.QuotientSituation.mem_quotients_canonicalBaseChange_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorBaseChange.lean, line 542. The attribute's comment: “the identification Q(F'/X'/B')(T) = Q(F/X/B)(T), in membership form”.

For a test scheme T over B' a subobject of F'_T is an element of Q_{F'/X'/B'}(T) exactly when the corresponding subobject of F_T is an element of Q_{F/X/B}(T), where on the right T is read as a scheme over B through T ⟶ B' ⟶ B.

theorem mem_quotients_canonicalBaseChange_iff (T : SchemesOver Y')
    (K : Subobject (D.baseChangeModule ((CostructuredArrow.map p).obj T))) :
    D.baseChangeSubobjectEquiv p (D.isQuasicoherentOnSite_baseChangedSourceModule p)
        (modulePushforwardCoherence B S hS) T K ∈
        (D.canonicalBaseChangedSituation p).quotients T ↔
      K ∈ D.quotients ((CostructuredArrow.map p).obj T)

AlgebraicGeometry.Space.QuotientSituation.quotients_canonicalBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorBaseChange.lean, line 558. The attribute's comment: “the identification Q(F'/X'/B')(T) = Q(F/X/B)(T)”.

Q_{F'/X'/B'}(T) = Q_{F/X/B}(T): the canonical bijection of the two lattices of subobjects carries the set of quotients of Stacks 082M for F/X/B at T, read as a scheme over B, onto the one for F'/X'/B' at T, read as a scheme over B'.

theorem quotients_canonicalBaseChange (T : SchemesOver Y') :
    (D.canonicalBaseChangedSituation p).quotients T =
      D.baseChangeSubobjectEquiv p (D.isQuasicoherentOnSite_baseChangedSourceModule p)
          (modulePushforwardCoherence B S hS) T ''
        D.quotients ((CostructuredArrow.map p).obj T)

AlgebraicGeometry.Space.QuotientSituation.quotientsCanonicalBaseChangeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorBaseChange.lean, line 567. The attribute's comment: “the bijection Q(F'/X'/B')(T) ≃ Q(F/X/B)(T)”.

The equality Q_{F'/X'/B'}(T) = Q_{F/X/B}(T) read as a bijection of the two sets.

def quotientsCanonicalBaseChangeEquiv (T : SchemesOver Y') :
    D.quotients ((CostructuredArrow.map p).obj T) ≃
      (D.canonicalBaseChangedSituation p).quotients T

AlgebraicGeometry.Space.QuotientSituation.mem_finitePresentationQuotients_canonicalBaseChange_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorBaseChange.lean, line 579. The attribute's comment: “the same identification for the finite-presentation subfunctor, in membership form”.

The same identification for Q^{fp}, in membership form: a subobject of F'_T is an element of Q^{fp}_{F'/X'/B'}(T) exactly when the corresponding subobject of F_T is an element of Q^{fp}_{F/X/B}(T).

theorem mem_finitePresentationQuotients_canonicalBaseChange_iff (T : SchemesOver Y')
    (K : Subobject (D.baseChangeModule ((CostructuredArrow.map p).obj T))) :
    D.baseChangeSubobjectEquiv p (D.isQuasicoherentOnSite_baseChangedSourceModule p)
        (modulePushforwardCoherence B S hS) T K ∈
        (D.canonicalBaseChangedSituation p).finitePresentationQuotients T ↔
      K ∈ D.finitePresentationQuotients ((CostructuredArrow.map p).obj T)

AlgebraicGeometry.Space.QuotientSituation.finitePresentationQuotients_canonicalBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorBaseChange.lean, line 600. The attribute's comment: “the same identification for the finite-presentation subfunctor”.

The same identification for Q^{fp}: Q^{fp}_{F'/X'/B'}(T) = Q^{fp}_{F/X/B}(T) under the canonical bijection of the two lattices of subobjects.

theorem finitePresentationQuotients_canonicalBaseChange (T : SchemesOver Y') :
    (D.canonicalBaseChangedSituation p).finitePresentationQuotients T =
      D.baseChangeSubobjectEquiv p (D.isQuasicoherentOnSite_baseChangedSourceModule p)
          (modulePushforwardCoherence B S hS) T ''
        D.finitePresentationQuotients ((CostructuredArrow.map p).obj T)

AlgebraicGeometry.Space.QuotientSituation.finitePresentationQuotientsCanonicalBaseChangeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorBaseChange.lean, line 610. The attribute's comment: “the bijection for the finite-presentation subfunctor”.

The equality Q^{fp}_{F'/X'/B'}(T) = Q^{fp}_{F/X/B}(T) read as a bijection of the two sets.

def finitePresentationQuotientsCanonicalBaseChangeEquiv (T : SchemesOver Y') :
    D.finitePresentationQuotients ((CostructuredArrow.map p).obj T) ≃
      (D.canonicalBaseChangedSituation p).finitePresentationQuotients T

Tag 08IU, a remark

Tag 08IU in the Stacks Project.

AlgebraicGeometry.Space.bijOn_quotientRestrict_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientDescentClauses.lean, line 492. References: SGA 1 VIII (1.8), “more general”.

Stacks 08IU. Let X be an algebraic space over a scheme S of a big fppf site, let F be a quasi-coherent 𝒪_X-module, let {f i : X i ⟶ X} be an fpqc covering and for each i, j let {g i j k : X ijk ⟶ X i ×_X X j} be an fpqc covering. Then restriction along the members of the covering is a bijection from the quotients F ⟶ Q with Q quasi-coherent onto the families of quotients f i ^* F ⟶ Q i with Q i quasi-coherent such that Q i and Q j restrict to the same quotient on every X ijk.

A quotient is recorded by its kernel, a subobject of the module, as in Situation 082M; the restriction of a quotient of F along f i is AlgebraicGeometry.Space.quotientRestrict, and the restrictions of Q i and Q j to X ijk are compared as quotients of the single inverse image of F along X ijk ⟶ X, through AlgebraicGeometry.Space.quotientRestrictOver.

Injectivity is the faithfulness clause of Stacks 04W8 applied to the kernels, which are quasi-coherent. For surjectivity, agreement on the X ijk gives agreement on X i ×_X X j (AlgebraicGeometry.Space.quotientRestrict_pairFst_eq_of_refinement), and the family descends by AlgebraicGeometry.Space.exists_quotientRestrict_eq_of_isFpqcCovering.

theorem bijOn_quotientRestrict_of_isFpqcCovering {I : Type v} {X : AlgebraicSpaces B S hS}
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    {Xi : I → AlgebraicSpaces B S hS} (f : ∀ i, Xi i ⟶ X)
    (hf : IsFpqcCovering B S hS fun i ↦ (f i).hom)
    {J : I → I → Type w} {Xijk : ∀ i j, J i j → AlgebraicSpaces B S hS}
    (g : ∀ i j k, Xijk i j k ⟶ QuasiCoherentDescent.pair B S hS Xi f i j)
    (hg : ∀ i j, IsFpqcCovering B S hS fun k ↦ (g i j k).hom) :
    Set.BijOn (fun (K : Subobject F) i ↦ quotientRestrict (f i) K)
      {K | (cokernel K.arrow).IsQuasicoherentOnSite}
      {Q | (∀ i, (cokernel (Q i).arrow).IsQuasicoherentOnSite) ∧
        ∀ i j k, quotientRestrictOver (g i j k ≫ QuasiCoherentDescent.pairFst B S hS Xi f i j)
            rfl F (Q i) =
          quotientRestrictOver (g i j k ≫ QuasiCoherentDescent.pairSnd B S hS Xi f i j)
            (pair_comp_condition f i j (g i j k)) F (Q j)}

AlgebraicGeometry.Space.eq_of_quotientRestrict_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorDescent.lean, line 306. The attribute's comment: “injectivity of the displayed bijection — a quasi-coherent quotient with quasi-coherent kernel is determined by its restrictions along the fpqc covering. Once conditional on the faithfulness clause of Stacks 04W8, it is discharged by AlgebraicGeometry.Space.modulePullback_reflectsZero_of_isFpqcCovering. Surjectivity needs the fullness and effectivity clauses of Stacks 04W8, which this development does not prove”.

Stacks 08IU, injectivity of the displayed bijection. Let X be an algebraic space over a scheme S of a big fppf site, let F be an 𝒪_X-module and let {p i : Z i ⟶ X} be an fpqc covering. A quotient of F whose quotient module and whose kernel are quasi-coherent is determined by its restrictions along the members of the covering: two such quotients that restrict to the same quotient of p i ^* F for every i are the same quotient of F.

This is one half of the bijection the source displays, and it uses only the covering {Z i ⟶ X}: the refining coverings {X ijk ⟶ X i ×_X X j} of the source cut down the right-hand set, so they bear on surjectivity only. Surjectivity is the fullness and the effectivity clauses of Stacks 04W8 together with the fpqc locality of surjectivity of a homomorphism, none of which this development carries; see the implementation notes.

theorem eq_of_quotientRestrict_eq
    {I : Type v} {X : AlgebraicSpaces B S hS} {Z : I → AlgebraicSpaces B S hS}
    (p : ∀ i, Z i ⟶ X) (hp : IsFpqcCovering B S hS fun i ↦ (p i).hom)
    {F : Modules.{u, u} B S hS X.1 X.2} {K K' : Subobject F}
    (hK : (K : Modules.{u, u} B S hS X.1 X.2).IsQuasicoherentOnSite)
    (hK' : (K' : Modules.{u, u} B S hS X.1 X.2).IsQuasicoherentOnSite)
    (hQ : (cokernel K.arrow).IsQuasicoherentOnSite)
    (hQ' : (cokernel K'.arrow).IsQuasicoherentOnSite)
    (h : ∀ i, quotientRestrict (p i) K = quotientRestrict (p i) K') : K = K'

AlgebraicGeometry.Space.injOn_quotientRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorDescent.lean, line 325. The attribute's comment: “injectivity of the displayed bijection, read as the injectivity of the restriction map on the set of quotients of the source whose quotient module and whose kernel are quasi-coherent. Once conditional on the faithfulness clause of Stacks 04W8, it is discharged by AlgebraicGeometry.Space.modulePullback_reflectsZero_of_isFpqcCovering”.

Stacks 08IU, injectivity of the displayed bijection, read as the injectivity of the map the source writes down: restriction along an fpqc covering {p i : Z i ⟶ X} is injective on the set of quotients of F whose quotient module and whose kernel are quasi-coherent.

theorem injOn_quotientRestrict
    {I : Type v} {X : AlgebraicSpaces B S hS} {Z : I → AlgebraicSpaces B S hS}
    (p : ∀ i, Z i ⟶ X) (hp : IsFpqcCovering B S hS fun i ↦ (p i).hom)
    (F : Modules.{u, u} B S hS X.1 X.2) :
    Set.InjOn (fun (K : Subobject F) i ↦ quotientRestrict (p i) K)
      {K | (K : Modules.{u, u} B S hS X.1 X.2).IsQuasicoherentOnSite ∧
        (cokernel K.arrow).IsQuasicoherentOnSite}

Tag 082P, a lemma

Tag 082P in the Stacks Project.

AlgebraicGeometry.Space.QuotientSituation.quotientsFunctor_isSheaf_fpqcTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorFpqcSheaf.lean, line 174. The attribute's comment: “the functor of quotients Q_{F/X/Y}”.

Stacks 082P for Q_{F/X/Y}. The functor of quotients Q_{F/X/Y} : (Sch/Y)ᵒᵖ ⥤ Sets of Stacks 082N satisfies the sheaf property for the fpqc topology.

theorem quotientsFunctor_isSheaf_fpqcTopology :
    Presheaf.IsSheaf (fpqcTopology D.Y) D.quotientsFunctor

AlgebraicGeometry.Space.QuotientSituation.finitePresentationQuotientsFunctor_isSheaf_fpqcTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorFpqcSheaf.lean, line 183. The attribute's comment: “the finite-presentation subfunctor Q^{fp}_{F/X/Y}”.

Stacks 082P for Q^{fp}_{F/X/Y}. The finite-presentation subfunctor of the functor of quotients satisfies the sheaf property for the fpqc topology.

theorem finitePresentationQuotientsFunctor_isSheaf_fpqcTopology :
    Presheaf.IsSheaf (fpqcTopology D.Y) D.finitePresentationQuotientsFunctor

AlgebraicGeometry.Space.QuotientSituation.isSheafFor_quotientsFunctor_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorFpqcSheaf.lean, line 175.

In Situation 082M the functor of quotients satisfies the sheaf property for the fpqc topology: for every fpqc covering {U i ⟶ T} of schemes over Y, every compatible family of quotients of the F_{U i}, quasi-coherent and flat over U i, has a unique amalgamation, a quotient of F_T quasi-coherent and flat over T.

theorem isSheafFor_quotientsFunctor_of_isFpqcCovering
    (hg : IsFpqcCovering B S hS fun i ↦ ((schemeSpaceFunctor B S hS).map (g i).left).hom) :
    Presieve.IsSheafFor D.quotientsFunctor (Presieve.ofArrows U g)

AlgebraicGeometry.Space.QuotientSituation.isSheafFor_finitePresentationQuotientsFunctor_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorFpqcSheaf.lean, line 198.

In Situation 082M the finite-presentation subfunctor of the functor of quotients satisfies the sheaf property for the fpqc topology: for every fpqc covering {U i ⟶ T} of schemes over Y, every compatible family of finitely presented quotients of the F_{U i}, flat over U i, has a unique amalgamation, a finitely presented quotient of F_T flat over T.

theorem isSheafFor_finitePresentationQuotientsFunctor_of_isFpqcCovering
    (hg : IsFpqcCovering B S hS fun i ↦ ((schemeSpaceFunctor B S hS).map (g i).left).hom) :
    Presieve.IsSheafFor D.finitePresentationQuotientsFunctor (Presieve.ofArrows U g)

Tag 0D3U, a lemma

Tag 0D3U in the Stacks Project.

AlgebraicGeometry.Space.QuotientSituation.morEquivSpaceQuotient, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorPoints.lean, line 363. The attribute's comment: “the displayed identification for Q_{F/X/Y}, in the case where the algebraic space is a scheme of the big fppf site: the morphisms of sheaves into the functor of quotients of Stacks 082P are the pairs of a morphism to Y and a quotient, quasi-coherent and flat over the base, of the pullback of F to the base change along it. Conditional on the one hypothesis of Stacks 082N still carried, the pseudofunctoriality of the inverse images of Stacks 03LU. The case of a general algebraic space is not covered: it needs the descent of the quotient along a surjective étale chart, which is the fullness and effectivity clauses of Stacks 04W8 together with Stacks 0262, 05VY and 060V, none of which this development carries”.

Stacks 0D3U for a representable algebraic space. The morphisms of sheaves on the big fppf site of S from a scheme U of the site into Q_{F/X/Y} are the pairs (h, Q) consisting of a morphism h : U ⟶ Y of algebraic spaces and a quotient of F_U, quasi-coherent and flat over U, where F_U is the pullback of F to X ×_{Y, h} U.

This is the source's displayed identification in the case where the algebraic space T is a scheme of the site, which is the base of the source's proof: that proof chooses a scheme U with a surjective étale morphism U ⟶ T, reads the transformation at it as a pair over U, and descends. The identification here is the Yoneda lemma for the sheaf of Stacks 082P, whose value at U is the set of those pairs; the sheaf of the algebraic space of U is lifted to the universe of the functor of quotients, which adds and loses no morphism.

def morEquivSpaceQuotient (hc : ModulePushforwardCoherence B S hS)
    (U : BigFppfOver B S hS) :
    (uliftYoneda.{u + 1}.obj U ⟶ D.totalQuotientsFunctor hc) ≃
      D.SpaceQuotients ((schemeSpaceFunctor B S hS).obj U)

AlgebraicGeometry.Space.QuotientSituation.morEquivSpaceQuotientOfAlgebraicSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorSpaceDescent.lean, line 685. The attribute's comment: “the first displayed identification, for Q_{F/X/Y} and an arbitrary algebraic space T”.

For an algebraic space T over S, the morphisms of sheaves on the big fppf site of S from T into the functor of quotients Q_{F/X/Y} of Stacks 082P are in bijection with the pairs (h, F_T ⟶ Q) consisting of a morphism h : T ⟶ Y of algebraic spaces and a quotient of the pullback F_T of F to X ×_{Y, h} T which is quasi-coherent and flat over T.

The sheaf of T is lifted to the universe of the functor of quotients. The inverse sends a pair to the transformation restricting it along the chart t : V ⟶ T of each section t of T over a scheme V of the site (AlgebraicGeometry.Space.QuotientSituation.SpaceQuotient.toMor).

def morEquivSpaceQuotientOfAlgebraicSpace (T : AlgebraicSpaces B S hS) :
    (T.obj ⋙ uliftFunctor.{u + 1, u} ⟶
        D.totalQuotientsFunctor (modulePushforwardCoherence B S hS)) ≃
      D.SpaceQuotients T

AlgebraicGeometry.Space.QuotientSituation.morEquivSpaceFinitePresentationQuotientOfAlgebraicSpaceUnconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorSpaceDescent.lean, line 761. The attribute's comment: “the second displayed identification, for Q^{fp}_{F/X/Y} and an arbitrary algebraic space T”.

For an algebraic space T over S, the morphisms of sheaves on the big fppf site of S from T into the finite-presentation subfunctor Q^{fp}_{F/X/Y} of Stacks 0CZL are in bijection with the pairs (h, F_T ⟶ Q) consisting of a morphism h : T ⟶ Y and a quotient of F_T which is of finite presentation and flat over T.

The subfunctor is formed with the pseudofunctoriality of inverse images AlgebraicGeometry.Space.modulePushforwardCoherence and the preservation of finite presentation by the base-change pullbacks AlgebraicGeometry.Space.QuotientSituation.pullbackPreservesFinitePresentation.

def morEquivSpaceFinitePresentationQuotientOfAlgebraicSpaceUnconditional
    (T : AlgebraicSpaces B S hS) :
    (T.obj ⋙ uliftFunctor.{u + 1, u} ⟶
        D.totalFinitePresentationQuotientsFunctor (modulePushforwardCoherence B S hS)
          D.pullbackPreservesFinitePresentation) ≃
      D.SpaceFinitePresentationQuotients T

Tag 08IV, a lemma

Tag 08IV in the Stacks Project.

AlgebraicGeometry.Space.QuotientSituation.bijOn_restrictQuotientToMember, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorSourceSheaf.lean, line 611. The attribute's comment: “the full bijection onto the matching families, every T, with nothing assumed beyond Situation 082M and the two coverings: 03LU for commutativity, 04W8 faithfulness and 03DO kernels for injectivity, 03GA and 05VW along the flat members of the covering for the restrictions, Remark 08IT (04W8 fullness and effectivity, at the quasi-coherent module of the situation) and 05VY for surjectivity”.

Stacks 08IV. In Situation 082M, let {a i : W i ⟶ X} be an fpqc covering of the source, let P i j be the fibre product W i ×_X W j and let {Z i j k ⟶ P i j} be fpqc coverings. For every scheme T over Y the diagram

Q_{F/X/Y}(T) ⟶ ∏_i Q_{F i/W i/Y}(T) ⇉ ∏_{ijk} Q_{F ijk/Z i j k/Y}(T)

presents the first arrow as the equalizer of the other two: restriction is a bijection from Q_{F/X/Y}(T) onto the set of families (Q i) whose two restrictions to each Z i j k agree.

The three halves of this are AlgebraicGeometry.Space.QuotientSituation.restrictQuotientToMember_mem_quotients together with AlgebraicGeometry.Space.QuotientSituation.restrictQuotientBetweenMembers_toMember, AlgebraicGeometry.Space.QuotientSituation.eq_of_restrictQuotientToMember_eq and AlgebraicGeometry.Space.QuotientSituation.exists_mem_quotients_restrictQuotientToMember_eq.

Nothing beyond Situation 082M and the two coverings is assumed.

theorem bijOn_restrictQuotientToMember
    {I : Type v} {κ : I → I → Type v} {W : I → AlgebraicSpaces B S hS}
    {P : I → I → AlgebraicSpaces B S hS} {Z : ∀ i j, κ i j → AlgebraicSpaces B S hS}
    (a : ∀ i, W i ⟶ D.X) {c₀ : ∀ i j, P i j ⟶ W i} {c₁ : ∀ i j, P i j ⟶ W j}
    {d : ∀ i j, P i j ⟶ D.X} (q : ∀ i j k, Z i j k ⟶ P i j) {e : ∀ i j k, Z i j k ⟶ D.X}
    (hcov : IsFpqcCovering B S hS fun i ↦ (a i).hom)
    (hP : ∀ i j, IsPullback (c₀ i j) (c₁ i j) (a i) (a j))
    (hd₀ : ∀ i j, c₀ i j ≫ a i = d i j) (hd₁ : ∀ i j, c₁ i j ≫ a j = d i j)
    (hqcov : ∀ i j, IsFpqcCovering B S hS fun k ↦ (q i j k).hom)
    (he₀ : ∀ i j k, (q i j k ≫ c₀ i j) ≫ a i = e i j k)
    (he₁ : ∀ i j k, (q i j k ≫ c₁ i j) ≫ a j = e i j k) (T : SchemesOver D.Y) :
    Set.BijOn (fun K i ↦
        D.restrictQuotientToMember (a i) T K)
      (D.quotients T)
      {Q | (∀ i, Q i ∈ (D.sourceRestricted (a i)).quotients T) ∧
        ∀ i j k, D.restrictQuotientBetweenMembers (q i j k ≫ c₀ i j) (he₀ i j k) T (Q i) =
          D.restrictQuotientBetweenMembers (q i j k ≫ c₁ i j) (he₁ i j k) T (Q j)}

AlgebraicGeometry.Space.QuotientSituation.bijOn_restrictQuotientToMember_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorSourceSheaf.lean, line 659. The attribute's comment: “the same equalizer property for the finite-presentation subfunctor Q^{fp}, again with nothing assumed and no weakening: the inputs of bijOn_restrictQuotientToMember together with Section 05VR for the restriction maps and 060V on the site for surjectivity”.

Stacks 08IV for the finite-presentation subfunctor. The diagram of Stacks 08IV presents the first arrow as the equalizer of the other two for Q^{fp}_{F/X/Y} as well: restriction is a bijection from Q^{fp}_{F/X/Y}(T) onto the set of families of elements of Q^{fp}_{F i/W i/Y}(T) whose two restrictions to each Z i j k agree.

Only the two outer halves change: the restriction maps preserve finite presentation, which is restrictQuotientToMember_mem_finitePresentationQuotients of this namespace, and the quotient descended by AlgebraicGeometry.Space.QuotientSituation.exists_mem_quotients_restrictQuotientToMember_eq is of finite presentation by AlgebraicGeometry.Space.finitePresentationOnSiteDescendsAlongFpqcCovering, Stacks 060V on the site.

Nothing beyond Situation 082M and the two coverings is assumed.

theorem bijOn_restrictQuotientToMember_finitePresentation
    {I : Type v} {κ : I → I → Type v} {W : I → AlgebraicSpaces B S hS}
    {P : I → I → AlgebraicSpaces B S hS} {Z : ∀ i j, κ i j → AlgebraicSpaces B S hS}
    (a : ∀ i, W i ⟶ D.X) {c₀ : ∀ i j, P i j ⟶ W i} {c₁ : ∀ i j, P i j ⟶ W j}
    {d : ∀ i j, P i j ⟶ D.X} (q : ∀ i j k, Z i j k ⟶ P i j) {e : ∀ i j k, Z i j k ⟶ D.X}
    (hcov : IsFpqcCovering B S hS fun i ↦ (a i).hom)
    (hP : ∀ i j, IsPullback (c₀ i j) (c₁ i j) (a i) (a j))
    (hd₀ : ∀ i j, c₀ i j ≫ a i = d i j) (hd₁ : ∀ i j, c₁ i j ≫ a j = d i j)
    (hqcov : ∀ i j, IsFpqcCovering B S hS fun k ↦ (q i j k).hom)
    (he₀ : ∀ i j k, (q i j k ≫ c₀ i j) ≫ a i = e i j k)
    (he₁ : ∀ i j k, (q i j k ≫ c₁ i j) ≫ a j = e i j k) (T : SchemesOver D.Y) :
    Set.BijOn (fun K i ↦
        D.restrictQuotientToMember (a i) T K)
      (D.finitePresentationQuotients T)
      {Q | (∀ i, Q i ∈ (D.sourceRestricted (a i)).finitePresentationQuotients T) ∧
        ∀ i j k, D.restrictQuotientBetweenMembers (q i j k ≫ c₀ i j) (he₀ i j k) T (Q i) =
          D.restrictQuotientBetweenMembers (q i j k ≫ c₁ i j) (he₁ i j k) T (Q j)}

AlgebraicGeometry.Space.QuotientSituation.bijOn_restrictQuotientToMember_of_isFpqcCovering, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorSourceSheafUnconditional.lean, line 81.

In Situation 082M, let {a i : W i ⟶ X} be an fpqc covering of the source, let P i j be the fibre product W i ×_X W j and let {Z i j k ⟶ P i j} be fpqc coverings. For every scheme T over Y the diagram

Q_{F/X/Y}(T) ⟶ ∏_i Q_{F i/W i/Y}(T) ⇉ ∏_{ijk} Q_{F ijk/Z i j k/Y}(T)

presents the first arrow as the equalizer of the other two: restriction is a bijection from Q_{F/X/Y}(T) onto the set of families (Q i) of elements of the Q_{F i/W i/Y}(T) whose two restrictions pr₀^*, pr₁^* to each Z i j k agree. Being a bijection onto that set is the commutativity pr₀^* ∘ res = pr₁^* ∘ res, the injectivity of res, and the surjectivity of res onto the equalizer.

Here F i is the inverse image of F along a i and F ijk the inverse image of F along the single morphism e i j k : Z i j k ⟶ X.

alias bijOn_restrictQuotientToMember_of_isFpqcCovering

AlgebraicGeometry.Space.QuotientSituation.bijOn_restrictQuotientToMember_finitePresentation_of_isFpqcCovering, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorSourceSheafUnconditional.lean, line 89.

The diagram of Stacks 08IV presents the first arrow as the equalizer of the other two for Q^{fp}_{F/X/Y} as well: restriction is a bijection from Q^{fp}_{F/X/Y}(T) onto the set of families of elements of the Q^{fp}_{F i/W i/Y}(T) whose two restrictions to each Z i j k agree.

alias bijOn_restrictQuotientToMember_finitePresentation_of_isFpqcCovering

Tag 082Q, a lemma

Tag 082Q in the Stacks Project.

AlgebraicGeometry.Space.QuotientSituation.finitePresentationQuotientsFunctor_limitPreserving_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorLimitPreservingUnconditional.lean, line 85. The attribute's comment: “corrected per the 082Q erratum: f also locally of finite presentation; as written the statement is false, see not_forall_finitePresentationQuotientsFunctor_limitPreserving”.

Stacks 082Q, corrected. In Situation 082M assume that (a) f : X ⟶ Y is quasi-compact and quasi-separated, and also locally of finite presentation, and (b) F is of finite presentation. Then Q^{fp}_{F/X/Y} is limit preserving: for a directed limit T = lim T_i of affine schemes over Y, Q^{fp}_{F/X/Y}(T) = colim Q^{fp}_{F/X/Y}(T_i).

The tag as written, without local finite presentation of f, is false: not_forall_finitePresentationQuotientsFunctor_limitPreserving (in StacksFrontier.AlgebraicGeometry.Quot.QuotientFunctorLimitPreservingSpaceCounterexample) proves the negation, with X = Spec ℚ[t][y_a]/((t - a) y_a) over Spec ℚ[t] and T = Spec ℚ(t).

theorem finitePresentationQuotientsFunctor_limitPreserving_of_isLocallyOfFinitePresentation
    (D : QuotientSituation B S hS) (hqc : IsQuasiCompact B S hS D.f.hom)
    (hqs : IsQuasiSeparated B S hS D.f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS D.f.hom)
    (hF : D.F.IsFinitePresentationOnSite) :
    LimitPreserving.{u, u + 1, u, u} D.testScheme D.finitePresentationQuotientsFunctor

AlgebraicGeometry.Space.QuotientSituation.finitePresentationQuotientsFunctor_limitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorLimits.lean, line 319. The attribute's comment: “limit preservation of the finite-presentation quotient functor. The three clauses of Stacks 07V7 are carried separately. The faithfulness clause is EventualModuleMapEqOverBaseChangeSystem, which is the conclusion of AlgebraicGeometry.Space.eventually_eq_of_modulePullback_limitProjection_eq written out for the system of base changes; it is a hypothesis here only because that theorem is phrased for a canonical presheaf limit and presenting the system of base changes as one is Stacks 07SF and 07SH, which this development has in a different shape. The essential surjectivity and fullness clauses are carried as genuinely missing, as the notes of StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationModuleColimit.lean record: both need the equivalence of Stacks 03M3, of which only one direction exists. The passage from a descended homomorphism to a surjection with flat target on an affine chart (Stacks 03H6, 05LI and 02JO) is carried too”.

Assume that f is quasi-compact and quasi-separated and that F is of finite presentation. Then the functor Q^{fp}_{F/X/Y} of finitely presented quotients is limit preserving: for every directed system of affine test schemes over Y with affine limit T = lim T_i, the comparison colim Q^{fp}_{F/X/Y}(T_i) ⟶ Q^{fp}_{F/X/Y}(T) is a bijection, that is, the cocone of values at the stages exhibits the value at T as their filtered colimit.

theorem finitePresentationQuotientsFunctor_limitPreserving
    (hc : ModulePushforwardCoherence B S hS)
    (hfpall : PullbackPreservesFinitePresentationEverywhere B S hS)
    (hdesc : ∀ (I : Type (max w w')) [Category.{w'} I] [IsCofiltered I],
      D.FlatQuotientsDescendToStage I)
    (hrigid : ∀ (I : Type (max w w')) [Category.{w'} I] [IsCofiltered I],
      D.FlatQuotientIsosDescendToStage I)
    (hfaith : ∀ (I : Type (max w w')) [Category.{w'} I] [IsCofiltered I],
      D.EventualModuleMapEqOverBaseChangeSystem I)
    (hqcf : IsQuasiCompact B S hS D.f.hom) (hqsf : IsQuasiSeparated B S hS D.f.hom)
    (hF : D.F.IsFinitePresentationOnSite) :
    LimitPreserving.{u, u + 1, w, w', u + 1, u} D.testScheme
      D.finitePresentationQuotientsFunctor

Tag 08IW, a lemma

Tag 08IW in the Stacks Project.

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

Stacks 08IW, for Q_{F/X/B}: for a pushout Y' = Y ⊔_Z Z' of schemes over B along a thickening Z ⟶ Z' and an affine morphism Z ⟶ Y, the natural map Q_{F/X/B}(Y') ⟶ Q_{F/X/B}(Y) ×_{Q_{F/X/B}(Z)} Q_{F/X/B}(Z') is bijective.

theorem quotientsPushoutMap_bijective :
    Function.Bijective (D.quotientsPushoutMap i f g h hpo)

AlgebraicGeometry.Space.QuotientSituation.finitePresentationQuotientsPushoutMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorPushoutBijective.lean, line 80.

Stacks 08IW, for Q^{fp}_{F/X/B}: if moreover X ⟶ B is locally of finite presentation, the natural map Q^{fp}(Y') ⟶ Q^{fp}(Y) ×_{Q^{fp}(Z)} Q^{fp}(Z') is bijective.

theorem finitePresentationQuotientsPushoutMap_bijective
    (hlfp : IsLocallyOfFinitePresentation B S hS D.f.hom) :
    Function.Bijective (D.finitePresentationQuotientsPushoutMap i f g h hpo)

Tag 0CZU, a remark

Tag 0CZU in the Stacks Project.

AlgebraicGeometry.Space.QuotientSituation.quotientObstruction_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorObstruction.lean, line 253.

Remark 0CZU: the obstruction vanishes exactly when the quotient lifts. For x ∈ Q(T) given by K ⊂ F_T, o_x(T') = 0 if and only if there is x' ∈ Q(T') restricting to x.

theorem quotientObstruction_eq_zero_iff {K : Subobject (D.baseChangeModule T)}
    (hK : K ∈ D.quotients T) :
    D.quotientObstruction hF h hh K = 0 ↔ ∃ K' ∈ D.quotients T', D.quotientPullback h K' = K

AlgebraicGeometry.Space.QuotientSituation.mem_finitePresentationQuotients_of_quotientPullback_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorObstruction.lean, line 272.

Remark 0CZU, finite presentation (Stacks 08VU). If x ∈ Q^{fp}(T), every lift x' ∈ Q(T') of x lies in Q^{fp}(T').

theorem mem_finitePresentationQuotients_of_quotientPullback_eq
    {K : Subobject (D.baseChangeModule T)} (hK : K ∈ D.finitePresentationQuotients T)
    {K' : Subobject (D.baseChangeModule T')} (hK' : K' ∈ D.quotients T')
    (hpb : D.quotientPullback h K' = K) :
    K' ∈ D.finitePresentationQuotients T'

AlgebraicGeometry.Space.QuotientSituation.reductionShortComplex_relativeSquare_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorObstruction.lean, line 319.

Remark 0CZU: 0 ⟶ f_T^*𝒥 ⊗ F_T ⟶ F_{T'} ⟶ F_T ⟶ 0 is exact. Since F_{T'} is flat over T', the reduction π : F_{T'} ⟶ F_T (read on X_{T'}) has kernel f_T^*𝒥 ⊗ F_T, embedded by i.

theorem reductionShortComplex_relativeSquare_shortExact :
    (reductionShortComplex (smallEtaleRingedToposHom B S hS (D.relativeMap h))
      (D.relativeSquareThickening h) (D.relativeSquareLeft h)
      (relBaseRight (smallEtaleRingedToposHom B S hS (D.projection T')))
      (D.relativeMapFirstOrderThickening h hh) (D.relativeSquareThickeningFirstOrderThickening h hh)
      (D.relativeSquare_comm h) (D.baseChangeModule T') (D.isStrict_relativeSquare h hh)
      (D.isFlat_baseChangeModule_relBaseRight hF T')).ShortExact

AlgebraicGeometry.Space.QuotientSituation.isIso_baseIdealTensorToIdealTensor_relativeSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorObstruction.lean, line 339.

Remark 0CZU: f_T^*𝒥 ⊗ F_T = I ⊗ F_T (Stacks 08MQ). The canonical comparison of f_T^*𝒥 ⊗ F_T with I ⊗ F_T, for F_T = F_{T'}|_{X_T}, is an isomorphism.

theorem isIso_baseIdealTensorToIdealTensor_relativeSquare :
    IsIso (baseIdealTensorToIdealTensor (smallEtaleRingedToposHom B S hS (D.relativeMap h))
      (D.relativeSquareThickening h) (D.relativeSquareLeft h)
      (relBaseRight (smallEtaleRingedToposHom B S hS (D.projection T')))
      (D.relativeMapFirstOrderThickening h hh) (D.relativeSquareThickeningFirstOrderThickening h hh)
      (D.relativeSquare_comm h)
      ((modulePullback B S hS (D.relativeMap h)).obj (D.baseChangeModule T')))

AlgebraicGeometry.Space.QuotientSituation.obstructionKernel_baseIdealTensor_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorObstruction.lean, line 358.

Remark 0CZU: 0 ⟶ K ⊗_{𝒪_T} 𝒥 ⟶ F_T ⊗_{𝒪_T} 𝒥 ⟶ Q ⊗_{𝒪_T} 𝒥 ⟶ 0 is exact, Q being flat over T. Here G ⊗_{𝒪_T} 𝒥 = f_T^*𝒥 ⊗ G.

theorem obstructionKernel_baseIdealTensor_shortExact {K : Subobject (D.baseChangeModule T)}
    (hK : K ∈ D.quotients T) :
    ((ShortComplex.mk (C := SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallEtaleRingedTopos B S hS (D.space T)).O)) (D.obstructionKernel h K).arrow
        (cokernel.π (D.obstructionKernel h K).arrow)
      (cokernel.condition _)).map (baseIdealTensor.{u, u + 1, u, u, u + 1, u, u, u + 1, u}
        (D.relativeSquareThickening h) (D.relativeSquareLeft h)
        (D.relativeSquareThickeningFirstOrderThickening h hh))).ShortExact

AlgebraicGeometry.Space.QuotientSituation.quotientObstructionExtension_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorObstruction.lean, line 376.

Remark 0CZU: the canonical extension 0 ⟶ Q ⊗_{𝒪_T} 𝒥 ⟶ π⁻¹(K)/i(K ⊗_{𝒪_T} 𝒥) ⟶ K ⟶ 0 of 𝒪_{X_T}-modules is short exact. Its class is AlgebraicGeometry.Space.QuotientSituation.quotientObstruction.

theorem quotientObstructionExtension_shortExact (K : Subobject (D.baseChangeModule T)) :
    (quotientLiftExtension (smallEtaleRingedToposHom B S hS (D.relativeMap h))
      (D.relativeSquareThickening h) (D.relativeSquareLeft h)
      (relBaseRight (smallEtaleRingedToposHom B S hS (D.projection T')))
      (D.relativeMapFirstOrderThickening h hh) (D.relativeSquareThickeningFirstOrderThickening h hh)
      (D.relativeSquare_comm h) (D.baseChangeModule T') (D.isStrict_relativeSquare h hh)
      (D.isFlat_baseChangeModule_relBaseRight hF T') (D.obstructionKernel h K)).ShortExact

AlgebraicGeometry.Space.QuotientSituation.isStrict_relativeSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorRelativeSquareStrict.lean, line 549.

Remark 0CZU: the ideal I of X_T ⊂ X_{T'} is a quotient of f_T^*𝒥. The relative square is strict (Stacks 08M9): the map of ideals f̃'^*(f'⁻¹𝒥) ⟶ I of the morphism of thickenings of Stacks 08M7, built from the first order thickenings X_T ⊂ X_{T'} and t̃ = (id, f'⁻¹t^♯) and the commutative square f̃' ∘ i = t̃ ∘ f̃, is an epimorphism.

theorem isStrict_relativeSquare :
    MorphismOfThickenings.IsStrict.{u, u + 1, u, u, u + 1, u, u, u + 1, u, u, u + 1, u}
      (MorphismOfThickenings.ofFirstOrderThickenings.{u, u + 1, u, u, u + 1, u, u + 1, u, u,
          u + 1, u}
        (smallEtaleRingedToposHom B S hS (D.relativeMap h)) (D.relativeSquareThickening h)
        (D.relativeSquareLeft h) (relBaseRight (smallEtaleRingedToposHom B S hS (D.projection T')))
        (D.relativeMapFirstOrderThickening h hh)
        (D.relativeSquareThickeningFirstOrderThickening h hh) (D.relativeSquare_comm h))

AlgebraicGeometry.Space.QuotientSituation.isFirstOrderThickening_range_relativeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorThickening.lean, line 89.

Remark 0CZU, X_T ⊂ X_{T'} is a first order thickening: the image of X_T in X_{T'}, which is the inverse image of the first order thickening T ⊂ T', is a first order thickening of X_{T'} (Stacks 09ZX).

theorem isFirstOrderThickening_range_relativeMap :
    IsFirstOrderThickening B S hS (D.space T') (Subfunctor.range (D.relativeMap h).hom)

Tag 0CZV, a remark

Tag 0CZV in the Stacks Project.

AlgebraicGeometry.Space.QuotientSituation.exists_addTorsor_quotientLifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotientFunctorDeformationTorsor.lean, line 168.

In Situation 082M with F flat over B, let T ⊂ T' be a first order thickening of schemes over B with ideal sheaf 𝒥, and let x ∈ Q_{F/X/B}(T) be given by 0 ⟶ 𝒦 ⟶ F_T ⟶ 𝒬 ⟶ 0 (K ∈ D.quotients T). If the obstruction o_x(T') of Remark 0CZU vanishes (D.quotientObstruction hF h hh K = 0), the set of lifts x' ∈ Q_{F/X/B}(T') of x (D.quotientLifts h K: the K' ∈ D.quotients T' with D.quotientPullback h K' = K) is a principal homogeneous space under Hom_{𝒪_{X_T}}(𝒦, 𝒬 ⊗_{𝒪_T} 𝒥) (D.deformationGroup h hh K), with the action of the remark: φ sends 𝒦' to 𝒦'_φ (D.quotientLiftAction hF h hh hK φ K').

theorem exists_addTorsor_quotientLifts {K : Subobject (D.baseChangeModule T)}
    (hK : K ∈ D.quotients T) (ho : D.quotientObstruction.{e} hF h hh K = 0) :
    ∃ Tor : AddTorsor (D.deformationGroup h hh K) (D.quotientLifts h K),
      ∀ (φ : D.deformationGroup h hh K) (K' : D.quotientLifts h K),
        (Tor.vadd φ K').val = D.quotientLiftAction hF h hh hK φ K'

Sources

Section99.8 The Quot functor #

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

Tag 09TR, a situation

Tag 09TR in the Stacks Project.

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

A quotient situation — a morphism f : X ⟶ B of algebraic spaces over S together with a quasi-coherent 𝒪_X-module F — whose morphism is moreover of finite presentation.

structure QuotSituation (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    extends QuotientSituation B S hS

AlgebraicGeometry.Space.QuotSituation.properlySupportedQuotients, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctor.lean, line 128. The attribute's comment: “the set of quotients”.

The set Quot_{F/X/B}(T) of quotients of F_T which are quasi-coherent, of finite presentation, flat over the test scheme T and with support proper over T, each recorded by its kernel K, the quotient being F_T / K.

def properlySupportedQuotients (T : SchemesOver D.Y) :
    Set (Subobject (D.baseChangeModule T))

AlgebraicGeometry.Space.QuotSituation.isProperlySupportedOver_modulePullback_quotientModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctor.lean, line 150. The attribute's comment: “the subfunctor of the finitely presented quotients”.

For a quotient in Quot_{F/X/B}(T) and a morphism U ⟶ T of test schemes, the inverse image of that quotient along X_U ⟶ X_T again has support proper over the test scheme.

theorem isProperlySupportedOver_modulePullback_quotientModule {U T : SchemesOver D.Y}
    (h : U ⟶ T) {K : Subobject (D.baseChangeModule T)}
    (hK : K ∈ D.properlySupportedQuotients T) :
    D.IsProperlySupportedOver U
      ((modulePullback B S hS (D.relativeMap h)).obj (D.quotientModule T K))

AlgebraicGeometry.Space.QuotSituation.quotientPullback_mem_properlySupportedQuotients, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPresheaf.lean, line 102. The attribute's comment: “stability of the four conditions under pullback of quotients”.

The pullback of a quotient in Quot_{F/X/B}(T) along a morphism T' ⟶ T of test schemes lies in Quot_{F/X/B}(T').

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

AlgebraicGeometry.Space.QuotSituation.quotFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPresheaf.lean, line 119. The attribute's comment: “the Quot functor on the test schemes over the base”.

The Quot functor Quot_{F/X/B} : (Sch/B)ᵒᵖ ⥤ Sets of F/X/B: its value at a test scheme T over B is the set Quot_{F/X/B}(T) of quotients of F_T that are quasi-coherent, of finite presentation, flat over T and with support proper over T, and its action on a morphism of test schemes is pullback of quotients.

def quotFunctor : (SchemesOver D.Y)ᵒᵖ ⥤ Type (u + 1)

AlgebraicGeometry.Space.QuotFamilyOver, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPresheaf.lean, line 160. The attribute's comment: “quotients over the schemes of the site”.

A quotient classified by the Quot functor over a scheme of the big fppf site rather than over a test scheme of B: the morphism to B the quotient lies over, together with a quotient over the resulting test scheme.

structure QuotFamilyOver (D : QuotSituation B S hS) (T : BigFppfOver B S hS)

AlgebraicGeometry.Space.QuotSituation.quotSitePresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPresheaf.lean, line 245. The attribute's comment: “the presheaf on the schemes of the site”.

The Quot functor read as a presheaf on the schemes of the big fppf site: a section over T is a morphism T ⟶ B together with a quotient of F_T for the resulting test scheme, and restriction pulls back both.

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

AlgebraicGeometry.Space.QuotSituation.quotSitePresheafToBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPresheaf.lean, line 254. The attribute's comment: “the canonical morphism to the base”.

The canonical morphism from the Quot presheaf to the universe lift of the base algebraic space B, sending a quotient to the morphism to B it lies over.

def quotSitePresheafToBase :
    D.quotSitePresheaf ⟶ D.Y.obj ⋙ uliftFunctor.{u + 1, u}

Tag 09TT, a lemma

Tag 09TT in the Stacks Project.

AlgebraicGeometry.Space.QuotSituation.quotFunctor_isSheaf_fpqcTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorFpqcSheaf.lean, line 233.

Stacks 09TT. In Situation 09TR, the Quot functor Quot_{F/X/B} : (Sch/B)ᵒᵖ ⥤ Sets satisfies the sheaf property for the fpqc topology: for every fpqc covering {T i ⟶ T} of schemes over B, a family of quotients of the F_{T i} — quasi-coherent, of finite presentation, flat over T i and with support proper over T i — which agree on the overlaps comes from a unique such quotient of F_T.

The topology is AlgebraicGeometry.Space.fpqcTopology on the test schemes over B. The proof is the source's: the functor of finitely presented quotients is an fpqc sheaf (Stacks 082P, …finitePresentationQuotientsFunctor_isSheaf_fpqcTopology), and the condition of proper support descends along fpqc coverings of the test scheme (AlgebraicGeometry.Space.QuotSituation.mem_properlySupportedQuotients_of_isFpqcCovering).

theorem quotFunctor_isSheaf_fpqcTopology :
    Presheaf.IsSheaf (fpqcTopology D.Y) D.quotFunctor

AlgebraicGeometry.Space.QuotSituation.quotSitePresheaf_isSheaf_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorFpqcSheaf.lean, line 552. The attribute's comment: “the Quot functor read on the schemes over S together with its morphism to B”.

Stacks 09TT, for the presheaf of pairs on the big fppf site of S. The source also reads Quot_{F/X/B} as a functor on the schemes over S with a morphism to B: its value at T is the set of pairs (h : T ⟶ B, Q) with Q a member of Quot_{F/X/B}(T) for the test scheme (T, h). That presheaf, AlgebraicGeometry.Space.QuotSituation.quotSitePresheaf, satisfies the sheaf property for the fpqc topology of the big fppf site of S.

theorem quotSitePresheaf_isSheaf_fpqc :
    Presheaf.IsSheaf ((Scheme.fpqcPrecoverage.comap (BigFppfOver.toScheme B S hS)).toGrothendieck)
      D.quotSitePresheaf

AlgebraicGeometry.Space.QuotSituation.quotSitePresheaf_isSheaf, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorFpqcSheaf.lean, line 589. The attribute's comment: “the fppf sheaf property of the Quot presheaf of pairs on the big fppf site over S, unconditionally; it is the consequence, for the coarser fppf topology, of the source's fpqc statement, which is quotSitePresheaf_isSheaf_fpqc. This name is an alias of quotSitePresheaf_isSheaf_fppf.”.

Stacks 09TT. The Quot functor Quot_{F/X/B} of Stacks 09TR, read as a presheaf on the schemes of the big fppf site of S, satisfies the sheaf condition for the fppf topology of that site: a compatible family, for an fppf covering of a scheme T of the site, of pairs consisting of a morphism to B and a quotient of the corresponding pullback of F which is quasi-coherent, of finite presentation, flat over the member and with support proper over it, comes from a unique such pair over T.

This name is an alias of AlgebraicGeometry.Space.QuotSituation.quotSitePresheaf_isSheaf_fppf, which has no hypothesis: the separatedness and glueing of quotients along a covering of a test scheme are the theorems AlgebraicGeometry.Space.QuotSituation.quotientsSeparatedForCoverings_properlySupportedQuotients and …quotientsGlueAlongCoverings_properlySupportedQuotients, and the sheaf property is deduced from the fpqc one, AlgebraicGeometry.Space.QuotSituation.quotSitePresheaf_isSheaf_fpqc, as the fppf topology of the site is coarser than its fpqc topology.

alias quotSitePresheaf_isSheaf

Tag 0D3V, a lemma

Tag 0D3V in the Stacks Project.

AlgebraicGeometry.Space.QuotSituation.morEquivSpaceProperlySupportedQuotient, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPoints.lean, line 219. The attribute's comment: “RESTRICTED: the displayed identification, read as a bijection, only for an algebraic space T that is a scheme of the big fppf site; the general case needs the fullness and effectivity of quasi-coherent descent, which this development lacks”.

Stacks 0D3V for a representable algebraic space. The morphisms of sheaves on the big fppf site of S from a scheme U of the site into Quot_{F/X/B} are the pairs (h, Q) consisting of a morphism h : U ⟶ B of algebraic spaces and a quotient of F_U which is quasi-coherent, of finite presentation, flat over U and has support proper over U, where F_U is the pullback of F to X ×_{B, h} U.

This is the source's displayed identification in the case where the algebraic space T is a scheme of the site, which is the base of the source's proof: that proof chooses a scheme U with a surjective étale morphism U ⟶ T, reads the transformation at it as a pair over U, and descends. The identification here is the Yoneda lemma for the sheaf of Stacks 09TT, whose value at U is the set of those pairs; the sheaf of the algebraic space of U is lifted to the universe of the Quot presheaf, which adds and loses no morphism. The general case is not covered; see the implementation notes for the precise obstruction.

def morEquivSpaceProperlySupportedQuotient (U : BigFppfOver B S hS) :
    (uliftYoneda.{u + 1}.obj U ⟶ D.quotSitePresheaf) ≃
      D.SpaceProperlySupportedQuotients ((schemeSpaceFunctor B S hS).obj U)

AlgebraicGeometry.Space.QuotSituation.morEquivSpaceProperlySupportedQuotientOfAlgebraicSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorPointsAlgebraicSpace.lean, line 105. The attribute's comment: “the displayed identification, read as a bijection, for an arbitrary algebraic space T over S”.

In Situation 09TR, let T be an algebraic space over S. The morphisms of sheaves on the big fppf site of S from T into Quot_{F/X/B} are in bijection with the pairs (h, F_T ⟶ Q) consisting of a morphism h : T ⟶ B of algebraic spaces and a quotient Q of the pullback F_T of F to the algebraic space X ×_{B, h} T, with Q quasi-coherent, of finite presentation, flat over T and with support proper over T.

The left-hand side is the Quot presheaf AlgebraicGeometry.Space.QuotSituation.quotSitePresheaf, with the sheaf of T lifted to its universe. The inverse sends a pair to the transformation restricting it along the chart t : V ⟶ T of every section t of T over a scheme V of the site.

def morEquivSpaceProperlySupportedQuotientOfAlgebraicSpace (T : AlgebraicSpaces B S hS) :
    (T.obj ⋙ uliftFunctor.{u + 1, u} ⟶ D.quotSitePresheaf) ≃
      D.SpaceProperlySupportedQuotients T

Tag 09TU, a proposition

Tag 09TU in the Stacks Project.

AlgebraicGeometry.Space.QuotSituation.exists_quotSitePresheafModel_of_small, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorAlgebraicSpace.lean, line 254. The attribute's comment: “the size clause: a model of the Quot presheaf in the universe of the site”.

Stacks 09TU, the size clause. Assume that over every scheme T of the big fppf site of S the set of pairs consisting of a morphism T ⟶ B and a quotient of F_T which is quasi-coherent, of finite presentation, flat over T and with support proper over T is small. Then the Quot presheaf of Stacks 09TR has a model in the universe of the site: a presheaf of Type u whose sections over every scheme of the site are exactly those pairs and whose canonical morphism to B is the one of Stacks 09TR.

This is the clause of Stacks 09TU which makes its two geometric clauses statable — an algebraic space takes values in the universe of the site, whereas quotients are recorded by subobjects and so live one universe up — and it is the content the source leaves to its set-theoretic conventions. The two geometric clauses, algebraicity of the model and local finite presentation of its morphism to B, are not proved; by AlgebraicGeometry.Space.QuotSitePresheafModel.isAlgebraicSpace_and_lfp_of_model they hold for the model produced here exactly when they hold for any model at all.

theorem exists_quotSitePresheafModel_of_small
    (hsmall : ∀ T : BigFppfOver B S hS, Small.{u} (QuotFamilyOver D T)) :
    ∃ M : QuotSitePresheafModel D,
      (∀ T : (BigFppfOver B S hS)ᵒᵖ, Nonempty (M.presheaf.obj T ≃ QuotFamilyOver D T.unop)) ∧
        Functor.whiskerRight M.toBase uliftFunctor.{u + 1, u} =
          M.iso.hom ≫ D.quotSitePresheafToBase

AlgebraicGeometry.Space.QuotSituation.isAlgebraicSpace_and_isLocallyOfFinitePresentation_quot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorAlgebraicSpaceSeparated.lean, line 94. The attribute's comment: “both assertions, f of finite presentation and separated: Quot_{F/X/B} is an algebraic space for F étale-locally generated by fewer than μ sections with μ below the cutoff of the site (every F of finite type), and it is locally of finite presentation over B for F of finite presentation; for an arbitrary quasi-coherent F the first assertion is false on the size-bounded site (F free of rank the cutoff plus one over a separably closed field)”.

Stacks 09TU. Let f : X ⟶ B be a morphism of algebraic spaces over S which is of finite presentation (a field of the standing datum D of Situation 09TR) and separated, and let F be a quasi-coherent 𝒪_X-module.

If F is étale-locally generated by fewer than μ sections for some μ below the cutoff of the site (for instance if F is of finite type), then Quot_{F/X/B} is an algebraic space: a model of it in the universe of the site exists, and every such model is an algebraic space.

If F is of finite presentation, then every model of Quot_{F/X/B} is an algebraic space whose morphism to B is locally of finite presentation.

Without the bound on generators in (1), the first assertion fails on the size-bounded site: for F free of rank the cutoff plus one over the spectrum of a separably closed field, the Quot functor has at least 2 ^ cutoff points, an algebraic space of the site fewer than the cutoff.

theorem isAlgebraicSpace_and_isLocallyOfFinitePresentation_quot
    (hsep : IsSeparated B S hS D.f.hom) :
    ((∃ μ < B.cutoff, IsEtaleLocallyGeneratedBelow B S hS μ D.F) →
        Nonempty (QuotSitePresheafModel D) ∧
          ∀ N : QuotSitePresheafModel D, IsAlgebraicSpace B S hS N.presheaf) ∧
      (D.F.IsFinitePresentationOnSite →
        ∀ N : QuotSitePresheafModel D,
          IsAlgebraicSpace B S hS N.presheaf ∧ IsLocallyOfFinitePresentation B S hS N.toBase)

AlgebraicGeometry.Space.QuotSituation.isAlgebraicSpace_quot_of_isFiniteTypeOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotFunctorAlgebraicSpaceSeparated.lean, line 112. The attribute's comment: “the first assertion for F of finite type”.

Stacks 09TU, the first assertion for F of finite type. If f is of finite presentation and separated and F is of finite type, then every model of Quot_{F/X/B} in the universe of the site is an algebraic space.

theorem isAlgebraicSpace_quot_of_isFiniteTypeOnSite (hsep : IsSeparated B S hS D.f.hom)
    (hF : SheafOfModules.IsFiniteTypeOnSite D.F) (N : QuotSitePresheafModel D) :
    IsAlgebraicSpace B S hS N.presheaf

Tag 0CZW, a remark

Tag 0CZW in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_and_isLocallyOfFinitePresentation_quotOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotArtinAlgebraic.lean, line 54. The attribute's comment: “Quot_{F/X/S} is an algebraic space locally of finite presentation over S, by Artin's axioms (Stacks 07Y1)”.

Quot_{F/X/S} is an algebraic space locally of finite presentation over S. Let S be Noetherian with all local rings G-rings, f : X ⟶ S separated and of finite presentation, and F a quasi-coherent 𝒪_X-module of finite presentation, flat over S. Then every model of Quot_{F/X/S} in the universe of the site is an algebraic space whose morphism to S is locally of finite presentation.

theorem isAlgebraicSpace_and_isLocallyOfFinitePresentation_quotOverBase
    [AlgebraicGeometry.IsNoetherian S] (hG : ∀ s : S, IsGRing (S.presheaf.stalk s))
    (hsep : IsSeparated B S hS f.hom) (hFfp : F.IsFinitePresentationOnSite)
    (hflat : IsFlatOver B S hS X.2 f.hom F) :
    ∀ N : QuotSitePresheafModel (quotOverBase X f hf F hF),
      IsAlgebraicSpace B S hS N.presheaf ∧ IsLocallyOfFinitePresentation B S hS N.toBase

AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_diag_quotOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotArtinAxioms.lean, line 540. The attribute's comment: “the diagonal of Quot_{F/X/S} is representable by algebraic spaces”.

Stacks 0CZW, the diagonal. In the situation of the remark, the diagonal Quot_{F/X/S} ⟶ Quot_{F/X/S} × Quot_{F/X/S} is representable (by closed immersions of schemes, hence by algebraic spaces): for two quotients F_T ⟶ 𝒬ᵢ, the locus of T over which they agree is a closed subscheme of T, by Stacks 083M (the remark's own argument, through the vanishing of 𝒦₁ ⟶ 𝒬₂ and of 𝒦₂ ⟶ 𝒬₁).

theorem isRepresentableByAlgebraicSpaces_diag_quotOverBase :
    IsRepresentableByAlgebraicSpaces B S hS (diag (quotOverBasePresheaf X f hf F hF))

AlgebraicGeometry.Space.isSheaf_quotOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotArtinAxioms.lean, line 548. The attribute's comment: “axiom [0]: Quot_{F/X/S} is a sheaf, for the fppf and hence for the étale topology”.

Stacks 0CZW, axiom [0]. In the situation of the remark, Quot_{F/X/S} is a sheaf for the étale topology (indeed for the fppf topology), by Stacks 09TT.

theorem isSheaf_quotOverBase :
    Presheaf.IsSheaf (BigFppfOver.topology B S hS) (quotOverBasePresheaf X f hf F hF) ∧
      Presheaf.IsSheaf ((AlgebraicGeometry.etaleTopology B).over (B.obj hS))
        (quotOverBasePresheaf X f hf F hF)

AlgebraicGeometry.Space.satisfiesRS_quotOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotArtinAxioms.lean, line 561. The attribute's comment: “axiom [2]: Quot_{F/X/S} satisfies the Rim-Schlessinger condition (RS)”.

Stacks 0CZW, axiom [2]. In the situation of the remark, Quot_{F/X/S} satisfies the Rim–Schlessinger condition: for a pushout Y' = Y ⨿_X X' of spectra of Artinian local rings of finite type over S along a closed immersion X ⟶ X', the map Quot(Y') ⟶ Quot(Y) ×_{Quot(X)} Quot(X') is bijective; equivalently the category fibred in sets 𝒮_{Quot} satisfies (RS) of Stacks 07WP. This is Stacks 08IW together with the descent of the properness of the support across the thickening Y ⟶ Y'.

theorem satisfiesRS_quotOverBase :
    Deformation.Artin.SatisfiesRSFunctor B S hS (quotOverBasePresheaf X f hf F hF) ∧
      Deformation.Artin.SatisfiesRS B S hS
        (Stack.fibredCategory B S hS (quotOverBasePresheaf X f hf F hF)).val.p
        (Stack.fibredCategory B S hS (quotOverBasePresheaf X f hf F hF)).isFiberedInGroupoids

AlgebraicGeometry.Space.isEffective_quotOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotArtinEffective.lean, line 172. The attribute's comment: “axiom [4]: formal objects of Quot_{F/X/S} are effective”.

Stacks 0CZW, axiom [4]: formal objects of Quot_{F/X/S} are effective. For f separated and F of finite presentation, every formal object of 𝒮_{Quot_{F/X/S}} over a Noetherian complete local ring is effective. This is Grothendieck's existence theorem (Stacks 08BE) applied to the quotient modules, together with the algebraization of the quotient maps (representability of Hom sheaves, Stacks 08K6) and their surjectivity, checked on the closed fibre.

theorem isEffective_quotOverBase (hsep : IsSeparated B S hS f.hom)
    (hFfp : F.IsFinitePresentationOnSite)
    (ξ : FormalObject B S hS
      (Stack.fibredCategory B S hS (quotOverBasePresheaf X f hf F hF)).val.p) :
    FormalObject.IsEffective B S hS
      (Stack.fibredCategory B S hS (quotOverBasePresheaf X f hf F hF)).val.p
      (Stack.fibredCategory B S hS (quotOverBasePresheaf X f hf F hF)).property ξ

AlgebraicGeometry.Space.limitPreserving_quotOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotArtinLimits.lean, line 115. The attribute's comment: “axiom [1]: Quot_{F/X/S} is limit preserving”.

Stacks 0CZW, axiom [1]. In the situation of the remark (F of finite presentation), Quot_{F/X/S} is limit preserving: for every cofiltered system of affine schemes Tᵢ of the site with limit T in schemes, the map colim Quot(Tᵢ) ⟶ Quot(T) is bijective. A quotient over the limit descends to a stage (Stacks 082Q, with the descent of flatness and of proper support), and two quotients over a stage agreeing over the limit agree at a later stage.

theorem limitPreserving_quotOverBase (hFfp : F.IsFinitePresentationOnSite) :
    AlgebraicGeometry.LimitPreserving.{u, u, u, u} (BigFppfOver.toScheme B S hS)
      (quotOverBasePresheaf X f hf F hF)

AlgebraicGeometry.Space.hasFiniteDimensionalTangentSpaces_quotOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotArtinTangentSpaces.lean, line 493. The attribute's comment: “axiom [3]: the tangent spaces of Quot_{F/X/S} at finite type points are finite dimensional”.

Stacks 0CZW, axiom [3]. In the situation of the remark, with F of finite presentation and flat over S, the tangent spaces of Quot_{F/X/S} at the points over fields of finite type over S are finite-dimensional, for their canonical vector space structure.

A lift over k[V] of a point F_k ⟶ F_k/𝒦₀ is a quotient of F_{k[V]} flat over k[V]; its difference with the trivial lift is a morphism 𝒦₀ ⟶ (F_k/𝒦₀) ⊗ V, natural in V and determining the lift, so the tangent space embeds k-linearly into Hom(𝒦₀, F_k/𝒦₀) (the deformation theory of quotients of Stacks 0CZV). That space is finite-dimensional because 𝒦₀ is coherent and F_k/𝒦₀ is coherent with support proper over k (Stacks 0D0T).

theorem hasFiniteDimensionalTangentSpaces_quotOverBase (hFfp : F.IsFinitePresentationOnSite)
    (hflat : IsFlatOver B S hS X.2 f.hom F) :
    Stack.HasFiniteDimensionalTangentSpaces B S hS
      (Stack.fibredCategory B S hS (quotOverBasePresheaf X f hf F hF))

AlgebraicGeometry.Space.isOpenVersality_quotOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/QuotArtinTower.lean, line 125. The attribute's comment: “axiom [5]: openness of versality for Quot_{F/X/S}”.

Stacks 0CZW, axiom [5]: openness of versality for Quot_{F/X/S}. For S locally Noetherian, f separated and F of finite presentation, a finite type point of a scheme locally of finite type over S at which an object of Quot_{F/X/S} is versal has an open neighbourhood of finite type points at which it is versal. This is Stacks 0CXU: the diagonal is representable, (RS*) holds, Quot_{F/X/S} is limit preserving (axiom [1]), and towers of square-zero thickenings of affine schemes are effective, by Grothendieck existence for such towers (Stacks 0CXB), representability of Hom sheaves (Stacks 08K6) and Nakayama.

theorem isOpenVersality_quotOverBase [AlgebraicGeometry.IsLocallyNoetherian S]
    (hsep : IsSeparated B S hS f.hom) (hFfp : F.IsFinitePresentationOnSite) :
    ∀ U : Over S, LocallyOfFiniteType U.hom →
      ∀ (y : (Stack.fibredCategory B S hS (quotOverBasePresheaf X f hf F hF)).val.obj)
        (hy : ((Stack.fibredCategory B S hS (quotOverBasePresheaf X f hf F hF)).val.p ⋙
          Over.post B.inclusion).obj y = U)
        (u : U.left),
        AlgebraicGeometry.IsFiniteTypePoint u →
        Deformation.Artin.IsVersalAt U ((Stack.fibredCategory B S hS
          (quotOverBasePresheaf X f hf F hF)).val.p ⋙ Over.post B.inclusion) u y hy →
        ∃ V : U.left.Opens, u ∈ V.1 ∧
          ∀ u' ∈ V.1, AlgebraicGeometry.IsFiniteTypePoint u' →
            Deformation.Artin.IsVersalAt U ((Stack.fibredCategory B S hS
              (quotOverBasePresheaf X f hf F hF)).val.p ⋙ Over.post B.inclusion) u' y hy

Sources

Section99.9 The Hilbert functor #

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

Tag 0CZY, a situation

Tag 0CZY in the Stacks Project.

AlgebraicGeometry.Space.HilbertFamily, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctor.lean, line 186. The attribute's comment: “families classified by the functor”.

Stacks 0CZY. A family classified by the Hilbert functor of f : X ⟶ Y over a scheme T over Y: a closed subspace of the base change X_T which is of finite presentation, flat and proper over T.

structure HilbertFamily (f : X ⟶ Y) (T : SchemesOverPresheaf B S hS Y)

AlgebraicGeometry.Space.hilbertFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctor.lean, line 289. The attribute's comment: “the Hilbert functor”.

Stacks 0CZY. The Hilbert functor of f : X ⟶ Y: it sends a scheme T over Y to the set of closed subspaces of X_T which are of finite presentation, flat and proper over T, and a morphism of schemes over Y to base change of those subspaces.

def hilbertFunctor (f : X ⟶ Y) : (SchemesOverPresheaf B S hS Y)ᵒᵖ ⥤ Type (u + 1)

AlgebraicGeometry.Space.hilbertFunctor_map_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctor.lean, line 302. The attribute's comment: “base change in the Hilbert functor”.

Stacks 0CZY. The Hilbert functor acts by inverse image of closed subspaces along the transition maps of base changes.

theorem hilbertFunctor_map_obj (f : X ⟶ Y) {T T' : SchemesOverPresheaf B S hS Y} (g : T' ⟶ T)
    (z : HilbertFamily f T) :
    ((hilbertFunctor f).map g.op z).Z = z.Z.preimage (schemeBaseChangeMap f g)

AlgebraicGeometry.Space.HilbertFamilyOver, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctor.lean, line 310. The attribute's comment: “families over the schemes of the site”.

Stacks 0CZY. A family classified by the Hilbert functor, over a scheme of the big fppf site rather than over a scheme of Y: the morphism to Y it lies over, together with a family over the resulting scheme over Y.

structure HilbertFamilyOver (f : X ⟶ Y) (T : BigFppfOver B S hS)

AlgebraicGeometry.Space.hilbertPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctor.lean, line 391. The attribute's comment: “the presheaf on the schemes of the site”.

Stacks 0CZY. The Hilbert functor read as a presheaf on the schemes of the big fppf site: a section over T is a morphism T ⟶ Y together with a family over T for the resulting scheme over Y, and restriction pulls back both.

def hilbertPresheaf (f : X ⟶ Y) : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (u + 1)

AlgebraicGeometry.Space.hilbertPresheafToBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctor.lean, line 401. The attribute's comment: “the canonical morphism to the base”.

Stacks 0CZY. The canonical morphism from the Hilbert presheaf to the base algebraic space Y, sending a family to the morphism to Y it lies over. Its target is the universe lift of Y because subfunctors of a presheaf on the site live one universe up.

def hilbertPresheafToBase (f : X ⟶ Y) : hilbertPresheaf f ⟶ Y.obj ⋙ uliftFunctor.{u + 1, u}

Tag 0D00, a lemma

Tag 0D00 in the Stacks Project.

AlgebraicGeometry.Space.hasProperSupport_pushforwardStructureSheaf_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFamilyStructureSheafDictionary.lean, line 168. The attribute's comment: “the proper-support entry of the dictionary, both directions”.

The proper-support entry of the dictionary of Stacks 0D00, in both directions. Let g : X ⟶ T be locally of finite type and let Z ⊆ X be a closed subspace with inclusion i. The module i_*𝒪_Z has support proper over T in the sense of Stacks 0CZD exactly when the composite Z ⟶ T is proper.

theorem hasProperSupport_pushforwardStructureSheaf_iff (g : X ⟶ T)
    (hg : IsLocallyOfFiniteType B S hS g.hom) :
    HasProperSupport B S hS X.property T.property g.hom hg
        ((SheafOfModules.toSheaf _).obj (pushforwardStructureSheaf B S hS X Z)) ↔
      IsProper B S hS (Z.1.ι ≫ g.hom)

AlgebraicGeometry.Space.hilbertFamilyOfQuotConditions, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFamilyStructureSheafDictionary.lean, line 388. The attribute's comment: “the converse construction: a quotient of the structure sheaf is a Hilbert family”.

Stacks 0D00, the converse construction. Let f : X ⟶ Y be a morphism of algebraic spaces of finite presentation, let T be a scheme of the site over Y, and let W be a closed subspace of the base change X_T with inclusion i. If the quotient 𝒪_{X_T} ⟶ i_*𝒪_W it determines is of finite presentation, is flat over T and has support proper over T, then W is a family classified by the Hilbert functor of f over T.

def hilbertFamilyOfQuotConditions (f : X ⟶ Y) (hf : IsFinitePresentation B S hS f.hom)
    (T : SchemesOverPresheaf B S hS Y)
    (W : ClosedSubspaces B S hS (schemeBaseChange f T))
    (hfpq : (pushforwardStructureSheaf B S hS
      (schemeBaseChangeSpace f T) W).IsFinitePresentationOnSite)
    (hflat : IsFlatOver B S hS (schemeBaseChangeSpace f T).property
      (schemeBaseChangeProjectionHom B S hS f T).hom
      (pushforwardStructureSheaf B S hS (schemeBaseChangeSpace f T) W))
    (hproper : HasProperSupport B S hS (schemeBaseChangeSpace f T).property
      (schemeOverSpace T).property (schemeBaseChangeProjectionHom B S hS f T).hom
      (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation B S hS
        (isFinitePresentation_schemeBaseChangeProjection f hf T).1)
      ((SheafOfModules.toSheaf _).obj
        (pushforwardStructureSheaf B S hS (schemeBaseChangeSpace f T) W))) :
    HilbertFamily f T

AlgebraicGeometry.Space.exists_hilbertFamily_definingIdealSheaf_eq_of_quotConditions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFamilyStructureSheafDictionary.lean, line 433. The attribute's comment: “the converse construction, from a quasi-coherent sheaf of ideals”.

Stacks 0D00, the converse construction from the sheaf of ideals. A sheaf of ideals 𝓘 ⊆ 𝒪_{X_T} whose quotient 𝒪_{X_T}/𝓘 is of finite presentation, flat over T and with support proper over T is the defining ideal sheaf of a family classified by the Hilbert functor of f over T.

theorem exists_hilbertFamily_definingIdealSheaf_eq_of_quotConditions (f : X ⟶ Y)
    (hf : IsFinitePresentation B S hS f.hom) (T : SchemesOverPresheaf B S hS Y)
    (I : (SheafOfModules.unit
      (structureRingSheaf B S hS (schemeBaseChangeSpace f T))).Submodule)
    (hfpq : (cokernel I.ι : Modules.{u, u} B S hS (schemeBaseChangeSpace f T).1
      (schemeBaseChangeSpace f T).2).IsFinitePresentationOnSite)
    (hflat : IsFlatOver B S hS (schemeBaseChangeSpace f T).property
      (schemeBaseChangeProjectionHom B S hS f T).hom
      (cokernel I.ι : Modules.{u, u} B S hS (schemeBaseChangeSpace f T).1
        (schemeBaseChangeSpace f T).2))
    (hproper : HasProperSupport B S hS (schemeBaseChangeSpace f T).property
      (schemeOverSpace T).property (schemeBaseChangeProjectionHom B S hS f T).hom
      (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation B S hS
        (isFinitePresentation_schemeBaseChangeProjection f hf T).1)
      ((SheafOfModules.toSheaf _).obj (cokernel I.ι :
        Modules.{u, u} B S hS (schemeBaseChangeSpace f T).1
          (schemeBaseChangeSpace f T).2))) :
    ∃ z : HilbertFamily f T,
      definingIdealSheaf B S hS (schemeBaseChangeSpace f T) ⟨z.Z, z.closed⟩ = I

AlgebraicGeometry.Space.exists_hilbertPresheafIso_quotSitePresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertQuotFunctorEquality.lean, line 279.

In Situation 0CZY we have Hilb_{X/B} = Quot_{𝒪_X/X/B}: the Hilbert functor of f and the Quot functor of its structure sheaf are isomorphic presheaves on the schemes of the big fppf site, by an isomorphism over Y.

theorem exists_hilbertPresheafIso_quotSitePresheaf :
    ∃ e : hilbertPresheaf f ≅ (structureSheafQuotSituation f hf).quotSitePresheaf,
      e.hom ≫ (structureSheafQuotSituation f hf).quotSitePresheafToBase =
        hilbertPresheafToBase f

AlgebraicGeometry.Space.hilbertFamilySubobject_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertQuotObjectwise.lean, line 240. The attribute's comment: “the forward construction: a Hilbert family is a quotient of the structure sheaf”.

The quotient of F_T that a family classified by the Hilbert functor of f over T determines lies in Quot_{𝒪_X/X/B}(T): it is quasi-coherent, of finite presentation, flat over T and has support proper over T.

theorem hilbertFamilySubobject_mem (z : HilbertFamily f T) :
    hilbertFamilySubobject f hf T z ∈
      (structureSheafQuotSituation f hf).properlySupportedQuotients
        (structureSheafTestScheme T)

Declarations registered for the tag:

AlgebraicGeometry.Space.isFlatOver_pushforwardStructureSheaf_iff, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Quot/HilbertQuotObjectwise.lean, line 76 (StacksFrontier): “the flatness entry of the dictionary, both directions”.
AlgebraicGeometry.Space.isFinitePresentationOnSite_pushforwardStructureSheaf_hilbertFamily_unconditional, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Quot/HilbertQuotObjectwise.lean, line 79 (StacksFrontier): “the finite-presentation entry of the dictionary, for a Hilbert family”.

Tag 0D3W, a lemma

Tag 0D3W in the Stacks Project.

AlgebraicGeometry.Space.morEquivSpaceHilbertFamily, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorPoints.lean, line 754. The attribute's comment: “the identification as a bijection, for an arbitrary algebraic space”.

Stacks 0D3W. For an algebraic space T over S the morphisms of sheaves on the big fppf site of S from T into the Hilbert presheaf Hilb_{X/Y} of Stacks 0CZY are the pairs (h, Z) consisting of a morphism h : T ⟶ Y of algebraic spaces and a closed subspace Z of X_T = X ×_{Y, h} T which is of finite presentation, flat and proper over T.

The source writes = between a set of morphisms of sheaves and a set of pairs; those are two different types here, so the honest reading is a bijection, and it is given as an Equiv, that is as data. Both directions are constructed: the forward map is AlgebraicGeometry.Space.hilbertMorFamily, which reads the morphism h off the canonical morphism to Y and glues the closed subspaces of the charts, and the inverse is AlgebraicGeometry.Space.SpaceHilbertFamily.toMor, which restricts a pair to every chart; nothing is chosen from an existence statement.

The hypothesis hloc is the descent input AlgebraicGeometry.Space.IsHilbertLocalOnBase, which is all that the general case needs beyond the gluing proved here; it holds unconditionally when T is a scheme of the site.

def morEquivSpaceHilbertFamily (f : X ⟶ Y) (T : AlgebraicSpaces B S hS)
    (hloc : IsHilbertLocalOnBase f T) :
    (T.obj ⋙ uliftFunctor.{u + 1, u} ⟶ hilbertPresheaf f) ≃ SpaceHilbertFamily f T

AlgebraicGeometry.Space.morEquivSpaceHilbertFamilyOfScheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorPoints.lean, line 781. The attribute's comment: “the identification for a scheme of the big fppf site, unconditionally”.

Stacks 0D3W for a scheme of the big fppf site. The morphisms of sheaves from a scheme U of the site into the Hilbert presheaf Hilb_{X/Y} of Stacks 0CZY are the pairs (h, Z) consisting of a morphism h : U ⟶ Y of algebraic spaces and a closed subspace Z of X_U = X ×_{Y, h} U which is of finite presentation, flat and proper over U.

This is AlgebraicGeometry.Space.morEquivSpaceHilbertFamily at the algebraic space of U, where the descent input is discharged by the identity chart, so nothing is assumed.

def morEquivSpaceHilbertFamilyOfScheme (f : X ⟶ Y) (U : BigFppfOver B S hS) :
    (uliftYoneda.{u + 1}.obj U ⟶ hilbertPresheaf f) ≃
      SpaceHilbertFamily f ⟨yoneda.obj U, isAlgebraicSpace_yoneda B S hS U⟩

AlgebraicGeometry.Space.morEquivSpaceHilbertFamilyOfAlgebraicSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorPointsDescent.lean, line 187. The attribute's comment: “the identification as a bijection, for an arbitrary algebraic space, unconditionally”.

The points of the Hilbert functor with values in an algebraic space. In Situation 0CZY, for an algebraic space T over S the morphisms of sheaves on the big fppf site of S from T into the Hilbert presheaf Hilb_{X/Y} are the pairs (h, Z) consisting of a morphism h : T ⟶ Y of algebraic spaces and a closed subspace Z of X_T = X ×_{Y, h} T which is of finite presentation, flat and proper over T.

The identification is a bijection, given as an Equiv; the finite presentation of f imposed by Situation 0CZY is not needed. The sheaf of T is lifted to the universe of Hilb_{X/Y}, which adds or loses no morphism.

def morEquivSpaceHilbertFamilyOfAlgebraicSpace (f : X ⟶ Y) (T : AlgebraicSpaces B S hS) :
    (T.obj ⋙ uliftFunctor.{u + 1, u} ⟶ hilbertPresheaf f) ≃ SpaceHilbertFamily f T

Tag 0D01, a proposition

Tag 0D01 in the Stacks Project.

AlgebraicGeometry.Space.exists_hilbertPresheafModel_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorAlgebraicSpace.lean, line 115.

Stacks 0D01. For a morphism f : X ⟶ B of algebraic spaces over S which is of finite presentation and separated, the Hilbert functor Hilb_{X/B} of Stacks 0CZY is an algebraic space locally of finite presentation over B: there is a model of the Hilbert presheaf in the universe of the site which is an algebraic space and whose canonical morphism to B is locally of finite presentation.

This is the source's deduction from Stacks 0D00 and Stacks 09TU, both of which are carried as hypotheses because neither is in the library. Stacks 09TU is N together with halg and hlfp: a model of the Quot presheaf of a situation on f which is an algebraic space whose morphism to B is locally of finite presentation. Stacks 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 standing hypotheses that f be of finite presentation and separated are recorded as _hfp and _hsep; the deduction itself does not consume them, since they enter through Stacks 09TU, which is carried. The content delivered is the transport: the Quot model is already a model of the Hilbert presheaf through e, and its morphism to B is the Hilbert one by AlgebraicGeometry.Space.HilbertPresheafModel.toBase_eq_of_iso.

theorem exists_hilbertPresheafModel_isAlgebraicSpace {X : AlgebraicSpaces B S hS}
    (D : QuotSituation B S hS) (f : X ⟶ D.Y)
    (_hfp : IsFinitePresentation B S hS f.hom) (_hsep : IsSeparated B S hS f.hom)
    (N : QuotSitePresheafModel D) (halg : IsAlgebraicSpace B S hS N.presheaf)
    (hlfp : IsLocallyOfFinitePresentation B S hS N.toBase)
    (e : hilbertPresheaf f ≅ D.quotSitePresheaf)
    (he : e.hom ≫ D.quotSitePresheafToBase = hilbertPresheafToBase f) :
    ∃ M : HilbertPresheafModel f,
      IsAlgebraicSpace B S hS M.presheaf ∧
        IsLocallyOfFinitePresentation B S hS M.toBase

AlgebraicGeometry.Space.exists_hilbertPresheafModel_isAlgebraicSpace_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/HilbertFunctorAlgebraicSpaceOfSeparated.lean, line 52.

Let S be a scheme and f : X ⟶ Y a morphism of algebraic spaces over S. If f is of finite presentation and separated, then the Hilbert functor Hilb_{X/Y} of Stacks 0CZY is an algebraic space locally of finite presentation over Y: it has a model in the universe of the site which is an algebraic space whose canonical morphism to Y is locally of finite presentation.

theorem exists_hilbertPresheafModel_isAlgebraicSpace_of_isSeparated
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hfp : IsFinitePresentation B S hS f.hom) (hsep : IsSeparated B S hS f.hom) :
    ∃ M : HilbertPresheafModel f,
      IsAlgebraicSpace B S hS M.presheaf ∧ IsLocallyOfFinitePresentation B S hS M.toBase

Sources

LeanAlgebraicGeometry.Space.HilbertFamily · AlgebraicGeometry.Space.hilbertFunctor · AlgebraicGeometry.Space.hilbertFunctor_map_obj · AlgebraicGeometry.Space.HilbertFamilyOver · AlgebraicGeometry.Space.hilbertPresheaf · AlgebraicGeometry.Space.hilbertPresheafToBase · AlgebraicGeometry.Space.hasProperSupport_pushforwardStructureSheaf_iff · AlgebraicGeometry.Space.hilbertFamilyOfQuotConditions

Section99.10 The Picard stack #

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

Tag 0D03, a lemma

Tag 0D03 in the Stacks Project.

AlgebraicGeometry.Space.picardToCoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackOpenImmersion.lean, line 240. The attribute's comment: “the natural map Picardstack_{X/B} -> Cohstack_{X/B} as a 1-morphism of categories fibred in groupoids, (T, g, L) going to (T, g, L), for f flat and proper, f of finite presentation being part of the standing data D of Situation 08KB”.

The natural map Pic_{X/B} ⟶ Coh_{X/B} as a 1-morphism of categories fibred in groupoids over the big fppf site of S.

def picardToCoherent (D : CoherentSituation B S hS) (hflat : IsFlat B S hS D.f.hom)
    (hproper : IsProper B S hS D.f.hom) :
    picardCFG (modulePushforwardCoherence B S hS) D.toPicardSituation ⟶ coherentCFG D

AlgebraicGeometry.Space.range_subset_fibrewiseEtaleRankOneFreeLocus_of_isInvertibleModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackOpenImmersion.lean, line 328. The attribute's comment: “part two of the proof, the implication (b) => (a) complete, at the source's own U = T \ f_T(|X_T| \ W_1) and the source's own condition (b): if F_T' is invertible then |T'| maps into U. The hypotheses on F are 0CZT's own three conditions, which an object of Coh_{X/Y} has.”.

If the pullback F_{T'} of an object F of Coh_{X/Y} along X_g : X_{T'} ⟶ X_T is invertible, then |T'| maps into U = T ∖ f_T(|X_T| ∖ W₁).

theorem range_subset_fibrewiseEtaleRankOneFreeLocus_of_isInvertibleModule
    (D : CoherentSituation B S hS) {T' T : SchemesOver D.Y} (g : T' ⟶ T)
    (F : Modules.{u, u} B S hS (D.space T).1 (D.space T).2)
    (hqc : F.IsQuasicoherentOnSite) (hfp : F.IsFinitePresentationOnSite)
    (hflat : IsFlatOver B S hS (D.space T).2 (D.projection T).hom F)
    (hF : IsInvertibleModule (D.space T') ((modulePullback B S hS (D.relativeMap g)).obj F)) :
    Set.range (pointsMap B S hS ((schemeSpaceFunctor B S hS).obj T'.left).1
        ((schemeSpaceFunctor B S hS).map g.left).hom) ⊆
      fibrewiseEtaleRankOneFreeLocus D T F

AlgebraicGeometry.Space.hasOpenLocus_picardToCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackOpenImmersion.lean, line 423. The attribute's comment: “part two of the proof, the open subscheme U of every object (T, g, F) of Cohstack_{X/B}, read on scheme-valued points: an object over the base factors through U exactly when its image comes from Picardstack_{X/B}”.

The open locus of the natural map. For every scheme-valued point y of Coh_{X/Y} over an object U of the big fppf site of S, there is an open subscheme V ⊆ U through which an object T of the big fppf site of U factors exactly when y(T) comes from Pic_{X/Y}.

theorem hasOpenLocus_picardToCoherent (D : CoherentSituation B S hS)
    (hflat : IsFlat B S hS D.f.hom) (hproper : IsProper B S hS D.f.hom) :
    Stack.HasOpenLocus B S hS (picardToCoherentBased D hflat hproper)

AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_and_isOpenImmersion_picardToCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackOpenImmersion.lean, line 477. The attribute's comment: “the whole statement: the natural map Picardstack_{X/B} -> Cohstack_{X/B}, for f flat, of finite presentation (the standing data D of Situation 08KB) and proper, 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))”.

Let f : X ⟶ B be a morphism of algebraic spaces over S which is flat, of finite presentation and proper, given by the data D of Situation 08KB with hflat and hproper. The natural map Pic_{X/B} ⟶ Coh_{X/B} is representable by open immersions: it is representable by algebraic spaces (Stacks 02ZW), and every algebraic space representing its base change along a scheme-valued point of Coh_{X/B} is an open subspace of that scheme (Stacks 04XB at open immersions).

theorem isRepresentableByAlgebraicSpaces_and_isOpenImmersion_picardToCoherent
    (D : CoherentSituation B S hS) (hflat : IsFlat B S hS D.f.hom)
    (hproper : IsProper B S hS D.f.hom) :
    Stack.IsRepresentableByAlgebraicSpaces B S hS (picardToCoherent D hflat hproper).hom ∧
      Stack.IsOpenImmersion B S hS (picardToCoherent D hflat hproper)

AlgebraicGeometry.Space.picardObjectToCoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackOpenInCoherentStack.lean, line 687. The attribute's comment: “part one of the proof, the well-definedness of the natural map, on objects: the triple (T, g, L) of Section 0372 goes to the same triple in Situation 08KB. All three conditions 08KB imposes are proved, with no hypothesis beyond the tag's own flatness and properness of f. Finite presentation of an invertible module -- and with it quasi-coherence -- is Tag 0B8N(b) on the small etale site. The two citations the source makes are performed: the projection X_T -> T is flat by Tag 03MO and proper by Tag 04WP (isFlat_projection, isProper_projection). Their module-theoretic halves are isFlatOver_of_isInvertibleModule (Tag 05VV, through the geometric-stalk criterion and Tag 05VX(1), the geometric stalk of an invertible module being free of rank one) and isProperOver_supportOfSheaf_of_isInvertibleModule (Tag 0CZD, the support being closed by Tag 07TZ and proper over the base by Tag 04XY). What remains of the tag is the second part of its proof, the open locus in T.”.

Stacks 0D03, the first part of the proof: the natural map Pic_{X/B} ⟶ Coh_{X/B} on objects. A triple (T, g, L) of the Picard stack of Section 0372 is sent to the same triple (T, g, L) viewed in Situation 08KB.

The three conditions of Situation 08KB hold for an invertible L for the reasons the source gives, and all three are proved. Finite presentation is AlgebraicGeometry.Space.isFinitePresentationOnSite_of_isInvertibleModule and quasi-coherence follows from it. Flatness over T is AlgebraicGeometry.Space.isFlatOver_of_isInvertibleModule applied to the projection X_T ⟶ T, which is flat by Stacks 03MO. Properness of the support over T is AlgebraicGeometry.Space.isProperOver_supportOfSheaf_of_isInvertibleModule applied to the same projection, which is proper by Stacks 04WP and therefore locally of finite type.

def picardObjectToCoherent (D : CoherentSituation B S hS) (hflat : IsFlat B S hS D.f.hom)
    (hproper : IsProper B S hS D.f.hom)
    (A : PicardObject D.toPicardSituation) : CoherentObject D

AlgebraicGeometry.Space.isOpen_fibrewiseEtaleFreeLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackOpenInCoherentStack.lean, line 887. The attribute's comment: “part two of the proof, the construction of the open T \ f_T(|X_T| \ W) and its openness, unconditionally, as an open SUBSET of |T| for the point topology -- realizing it as an open subscheme of T is done in hasOpenLocus_picardToCoherent of Quot/PicardStackOpenImmersion.lean. W is the etale free locus of Tag 0CZT, open by the mechanism of that tag's openness clause (isOpen_of_etale_witness); the projection X_T -> T is proper by Tag 04WP, hence closed on points. This is the FIRST of the source's two reductions only; the source's own U is the same construction at the RANK-ONE locus, isOpen_fibrewiseEtaleRankOneFreeLocus, which performs both reductions at once. The source's parenthetical quasi-compactness assumption on T is not needed for either: it belongs to the decomposition X_T = X_0 + X_1 + ... by rank, which the rank-one locus makes unnecessary.”.

Stacks 0D03, the construction of the open U of the second part of the proof. The locus is open in |T| when f is proper.

The étale free locus is open, so its complement is closed, and the projection |X_T| ⟶ |T| is a closed map because X_T ⟶ T is proper by Stacks 04WP; the image of that complement is therefore closed and the locus, its complement, is open.

theorem isOpen_fibrewiseEtaleFreeLocus (D : CoherentSituation B S hS)
    (hf : IsProper B S hS D.f.hom) (T : SchemesOver D.Y)
    (F : Modules.{u, u} B S hS (D.space T).1 (D.space T).2) :
    IsOpen (fibrewiseEtaleFreeLocus D T F)

AlgebraicGeometry.Space.isOpen_fibrewiseEtaleRankOneFreeLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackOpenInCoherentStack.lean, line 911. The attribute's comment: “part two of the proof, the construction of the open U = T \ f_T(|X_T| \ W_1) and its openness, unconditionally, as an open SUBSET of |T| for the point topology -- realizing it as an open subscheme of T is done in hasOpenLocus_picardToCoherent of Quot/PicardStackOpenImmersion.lean. W_1 is the locus of Tag 0CZT with the rank pinned to ONE, and this U is the source's own U: it is the composite of the source's two reductions, since |X_T| \ W_1 = (|X_T| \ W) + X_0 + X_2 + ..., so the source's decomposition of a finite locally free module by rank is not needed and neither is its parenthetical quasi-compactness assumption on T. Openness of W_1 is the mechanism of the openness clause of 0CZT (isOpen_of_etale_witness) and the projection X_T -> T is proper by Tag 04WP, hence closed on points.”.

Stacks 0D03, the construction of the open U of the second part of the proof, at the source's own U. The rank-one locus is open in |T| when f is proper.

The rank-one étale free locus W₁ is open with no hypothesis (AlgebraicGeometry.Space.isOpen_etaleRankOneFreeLocus, the mechanism of the openness clause of Stacks 0CZT), and the projection |X_T| ⟶ |T| is a closed map because X_T ⟶ T is proper by Stacks 04WP; so the image of the closed complement is closed and the locus is open. No decomposition of X_T by rank is used, and so no quasi-compactness of T.

theorem isOpen_fibrewiseEtaleRankOneFreeLocus (D : CoherentSituation B S hS)
    (hf : IsProper B S hS D.f.hom) (T : SchemesOver D.Y)
    (F : Modules.{u, u} B S hS (D.space T).1 (D.space T).2) :
    IsOpen (fibrewiseEtaleRankOneFreeLocus D T F)

AlgebraicGeometry.Space.range_pointsMap_relativeMap_subset_etaleFreeLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackOpenInCoherentStack.lean, line 967. The attribute's comment: “part two of the proof, the implication (a) => (b) on points, unconditionally: if |T'| maps into U -- which is how condition (a), that T' -> T factors through U, is read here, U being produced as an open subset of |T| -- then |X_T'| maps into the etale free locus W of F. This is the direction that needs no base-change property of W, as the source's own argument shows; it is the commutation of X_g with the projections to the test schemes together with the description of U as the points whose whole fibre lies in W. The remaining step needs neither the rank decomposition nor a conditional clause of Tag 0B8Q: the rank decomposition is not needed at all -- pinning the rank to one at the level of the locus replaces it, see range_pointsMap_relativeMap_subset_etaleRankOneFreeLocus -- and the clause of Tag 0B8Q the step would use is the UNCONDITIONAL one, which holds at this site. What the step does need is recorded on that rank-one statement.”.

Stacks 0D03, the implication (a) ⟹ (b) of the second part of the proof, on points. If a morphism g : T' ⟶ T of test schemes over Y maps |T'| into the locus, then the induced morphism X_g : X_{T'} ⟶ X_T maps |X_{T'}| into the étale free locus of F.

A point x' of |X_{T'}| goes to a point x of |X_T| lying over the image in |T| of the point of |T'| below x', because X_g commutes with the two projections to the test schemes; that image lies in the locus, so x lies in the étale free locus. No base-change property of the locus is used.

theorem range_pointsMap_relativeMap_subset_etaleFreeLocus (D : CoherentSituation B S hS)
    {T' T : SchemesOver D.Y} (g : T' ⟶ T)
    (F : Modules.{u, u} B S hS (D.space T).1 (D.space T).2)
    (hg : Set.range (pointsMap B S hS ((schemeSpaceFunctor B S hS).obj T'.left).1
        ((schemeSpaceFunctor B S hS).map g.left).hom) ⊆ fibrewiseEtaleFreeLocus D T F) :
    Set.range (pointsMap B S hS (D.space T').1 (D.relativeMap g).hom) ⊆
      etaleFreeLocus B S hS F

AlgebraicGeometry.Space.range_pointsMap_relativeMap_subset_etaleRankOneFreeLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackOpenInCoherentStack.lean, line 1002. The attribute's comment: “part two of the proof, the implication (a) => (b) on points at the source's own U, unconditionally: if |T'| maps into U = T \ f_T(|X_T| \ W_1) -- which is how condition (a), that T' -> T factors through U, is read here, U being produced as an open subset of |T| -- then |X_T'| maps into the RANK-ONE etale free locus W_1 of F. This is the direction that needs no base-change property of the locus, as the source's own argument shows; it is the commutation of X_g with the projections to the test schemes together with the description of U as the points whose whole fibre lies in W_1. Pinning the rank to one at the level of the locus is what replaces the source's decomposition X_T = X_0 + X_1 + ... by rank, which is not available for algebraic spaces. The passage from rank-one freeness in an etale neighbourhood of every point of |X_T'| to invertibility of F_T' takes two steps -- the easy inclusion of the base-change clause of Tag 0CZT and the local-to-global refinement for the unconditional clause of Tag 0B8Q; both steps are proved (preimage_etaleRankOneFreeLocus_subset and isFiniteLocallyFreeOfRank_one_of_forall_mem_etaleRankOneFreeLocus), and the complete implication -- |T'| into U gives F_T' INVERTIBLE, unconditionally -- is isInvertibleModule_modulePullback_relativeMap_of_subset_fibrewiseEtaleRankOneFreeLocus below.”.

Stacks 0D03, the implication (a) ⟹ (b) of the second part of the proof, on points, at the source's own U. If a morphism g : T' ⟶ T of test schemes over Y maps |T'| into the rank-one locus, then X_g : X_{T'} ⟶ X_T maps |X_{T'}| into the rank-one étale free locus of F.

This is AlgebraicGeometry.Space.range_pointsMap_relativeMap_subset_of_subset_fibrewiseLocus at W₁, and it is the implication the source proves — its U is the rank-one locus, so what (a) yields is rank-one freeness at every point of |X_{T'}| rather than freeness of some rank. No decomposition by rank and no base-change property of the locus is used.

theorem range_pointsMap_relativeMap_subset_etaleRankOneFreeLocus (D : CoherentSituation B S hS)
    {T' T : SchemesOver D.Y} (g : T' ⟶ T)
    (F : Modules.{u, u} B S hS (D.space T).1 (D.space T).2)
    (hg : Set.range (pointsMap B S hS ((schemeSpaceFunctor B S hS).obj T'.left).1
        ((schemeSpaceFunctor B S hS).map g.left).hom) ⊆
      fibrewiseEtaleRankOneFreeLocus D T F) :
    Set.range (pointsMap B S hS (D.space T').1 (D.relativeMap g).hom) ⊆
      etaleRankOneFreeLocus B S hS F

AlgebraicGeometry.Space.range_pointsMap_relativeMap_subset_etaleFreeLocus_of_forall_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackOpenInCoherentStack.lean, line 1090. The attribute's comment: “part two of the proof, the implication (b) => (a) on points: if F_T' is free in an etale neighbourhood of every point then |X_T'| maps into the etale free locus W of F. UNCONDITIONAL. This is the direction the source derives from the base-change clause of Tag 0CZT, and that clause is proved: etaleFreeLocus_modulePullback_eq of Spaces/EtaleFreeLocusBaseChange.lean, registered on 0CZT with a which-part note, states the EQUALITY W(F_T') = |X_g|^(-1)(W(F)) at an arbitrary cartesian square. This statement binds no hypothesis standing in for that equality; its binders are D, g, F, 0CZT's own three conditions on F, and the antecedent (b). The source's route is what was assembled: clause (4) of Tag 0CZS (exists_chartOpen_over_iso_free_iff_flat_geometricFibreModuleStalk) at the image point, the base-change invariance of clause (1) (flat_geometricFibreModuleStalk_modulePullback_iff of Spaces/GeometricFibreStalkBaseChange.lean) for the transport, and the etale-locality of clause (1) (flat_geometricFibreModuleStalk_comp_modulePullback_iff of Spaces/GeometricFibreStalkEtaleLocal.lean) at the point upstairs. Condition (2) of Tag 05WY is NOT needed and is still neither stated nor proved; that is a gap in the registration of Tag 05WY alone. F carries 0CZT's own three hypotheses, quasi-coherent, of finite presentation and flat over T, which is exactly what an object of Coh_{X/Y} is (CoherentObject), so no consumer pays for them.”.

Stacks 0D03, the implication (b) ⟹ (a) of the second part of the proof, on points. If the pullback of F along X_g : X_{T'} ⟶ X_T is free in an étale neighbourhood of every point of |X_{T'}| — which is the case when that pullback is invertible — then X_g maps |X_{T'}| into the étale free locus of F.

This is the source's "if T' ⟶ T satisfies (b) then |X_{T'}| ⟶ |X_T| maps into W", and it is exactly where the base-change clause of Stacks 0CZT enters. That clause is now proved, as AlgebraicGeometry.Space.etaleFreeLocus_modulePullback_eq of StacksFrontier/AlgebraicGeometry/Spaces/EtaleFreeLocusBaseChange.lean, so this statement is unconditional. F carries Stacks 0CZT's own hypotheses — quasi-coherent, of finite presentation and flat over T — which is what an object of Coh_{X/Y} is, and local finite presentation of the projection X_T ⟶ T costs nothing (AlgebraicGeometry.Space.isLocallyOfFinitePresentation_projection). The square of the morphism of test schemes is cartesian by AlgebraicGeometry.Space.isPullback_baseChangeMap, which is the form the clause is stated at.

theorem range_pointsMap_relativeMap_subset_etaleFreeLocus_of_forall_mem
    (D : CoherentSituation B S hS)
    {T' T : SchemesOver D.Y} (g : T' ⟶ T)
    (F : Modules.{u, u} B S hS (D.space T).1 (D.space T).2)
    (hqc : F.IsQuasicoherentOnSite) (hfp : F.IsFinitePresentationOnSite)
    (hflat : IsFlatOver B S hS (D.space T).2 (D.projection T).hom F)
    (hF : ∀ x' : points B S hS (D.space T').1,
      x' ∈ etaleFreeLocus B S hS ((modulePullback B S hS (D.relativeMap g)).obj F)) :
    Set.range (pointsMap B S hS (D.space T').1 (D.relativeMap g).hom) ⊆
      etaleFreeLocus B S hS F

AlgebraicGeometry.Space.range_pointsMap_relativeMap_subset_etaleFreeLocus_of_isInvertibleModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackOpenInCoherentStack.lean, line 1143. The attribute's comment: “part two of the proof, the implication (b) => (a) on points, with (b) at the source's own condition that F_T' be INVERTIBLE rather than at the etale-local freeness of the preceding statement. The step from invertibility to freeness in an etale neighbourhood of every point is unconditional here (mem_etaleFreeLocus_of_isInvertibleModule): the converse clause of Tag 0B8Q applies to the small etale ringed site of an algebraic space, which is locally ringed by Tag 04KH, in its universe-flexible form -- the site has its objects one universe above the sections of its structure sheaf, so the two carriers of 0B8Q stated for a bare ringed site do not instantiate -- and Tag 04M0 identifies a trivialization on a slice of that site with freeness of the pullback to the chart space, which is how the locus W of Tag 0CZT is phrased. UNCONDITIONAL. The base-change clause of Tag 0CZT, which this direction needs, is now proved: etaleFreeLocus_modulePullback_eq of Spaces/EtaleFreeLocusBaseChange.lean. This statement binds no hypothesis standing in for that equality; its binders are D, g, F, 0CZT's own three conditions on F, and the antecedent (b). The base-change invariance of clause (1) of Tag 0CZS (flat_geometricFibreModuleStalk_modulePullback_iff) does NOT need condition (2) of Tag 05WY. The converse implication, from |T'| mapping into U to invertibility of F_T', does not need the source's rank decomposition of X_T. The decomposition is replaced by pinning the rank to one at the level of the locus (etaleRankOneFreeLocus), and that converse is complete in isInvertibleModule_modulePullback_relativeMap_of_subset_fibrewiseEtaleRankOneFreeLocus. F carries 0CZT's own three hypotheses, quasi-coherent, of finite presentation and flat over T, which is exactly what an object of Coh_{X/Y} is (CoherentObject).”.

Stacks 0D03, the implication (b) ⟹ (a) of the second part of the proof, at the source's own condition (b). If the pullback F_{T'} of F along X_g : X_{T'} ⟶ X_T is invertible — which is condition (b) of the source, and not merely the étale-local freeness that Space.range_pointsMap_relativeMap_subset_etaleFreeLocus_of_forall_mem asks for — then X_g maps |X_{T'}| into the étale free locus of F.

The passage from invertibility of F_{T'} to its freeness in an étale neighbourhood of every point of |X_{T'}| is AlgebraicGeometry.Space.mem_etaleFreeLocus_of_isInvertibleModule and is unconditional: it is the converse clause of Stacks 0B8Q at the small étale ringed site of an algebraic space, which is locally ringed by Stacks 04KH, together with the comparison of Stacks 04M0 between the slices of that site and the small étale sites of the chart spaces. The base-change clause of Stacks 0CZT is still used, for the same reason as in Space.range_pointsMap_relativeMap_subset_etaleFreeLocus_of_forall_mem, and it is now proved (AlgebraicGeometry.Space.etaleFreeLocus_modulePullback_eq), so this statement is unconditional as well; F carries Stacks 0CZT's own hypotheses here too, which is what an object of Coh_{X/Y} is.

theorem range_pointsMap_relativeMap_subset_etaleFreeLocus_of_isInvertibleModule
    (D : CoherentSituation B S hS)
    {T' T : SchemesOver D.Y} (g : T' ⟶ T)
    (F : Modules.{u, u} B S hS (D.space T).1 (D.space T).2)
    (hqc : F.IsQuasicoherentOnSite) (hfp : F.IsFinitePresentationOnSite)
    (hflat : IsFlatOver B S hS (D.space T).2 (D.projection T).hom F)
    (hF : IsInvertibleModule (D.space T')
      ((modulePullback B S hS (D.relativeMap g)).obj F)) :
    Set.range (pointsMap B S hS (D.space T').1 (D.relativeMap g).hom) ⊆
      etaleFreeLocus B S hS F

AlgebraicGeometry.Space.isInvertibleModule_modulePullback_relativeMap_of_subset_fibrewiseEtaleRankOneFreeLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackOpenInCoherentStack.lean, line 1192. The attribute's comment: “part two of the proof, the implication (a) => (b) COMPLETE and unconditional, at the source's own U and the source's own condition (b): if |T'| maps into U = T \ f_T(|X_T| \ W_1) -- which is how condition (a), that T' -> T factors through U, is read here, U being produced as an open SUBSET of |T| for the point topology -- then F_T' is INVERTIBLE. This completes the direction whose last two steps were recorded as missing on range_pointsMap_relativeMap_subset_etaleRankOneFreeLocus: (i) the easy inclusion of the base-change clause of Tag 0CZT, |X_g|^{-1}(W_1(F)) subset W_1(F_T'), which is preimage_etaleRankOneFreeLocus_subset and holds for an arbitrary morphism of algebraic spaces; and (ii) the local-to-global refinement from a trivialization through every POINT of |X_T'| to a trivializing covering family of every OBJECT of the small etale site, which is isFiniteLocallyFreeOfRank_one_of_forall_mem_etaleRankOneFreeLocus -- the chosen neighbourhoods form an etale covering, so their charts cover the final object (coversTop_of_isEtaleCovering, the slice form of Tag 04M0), and the rank clause of Tag 0409 is local on such a family. The unconditional clause of Tag 0B8Q then gives invertibility. The source's decomposition of X_T by rank is not used, and neither is the base-change clause of Tag 0CZT: the hard inclusion of that clause is what the CONVERSE implication (b) => (a) needs, and it is proved in etaleFreeLocus_modulePullback_eq of Spaces/EtaleFreeLocusBaseChange.lean.”.

Stacks 0D03, the implication (a) ⟹ (b) of the second part of the proof, complete. If a morphism g : T' ⟶ T of test schemes over Y maps |T'| into the source's own locus U = T ∖ f_T(|X_T| ∖ W₁), then the pullback F_{T'} of F along X_g : X_{T'} ⟶ X_T is invertible — which is the source's condition (b). Unconditionally.

The three steps are each unconditional. Condition (a) puts every point of |X_{T'}| over a point of the rank-one étale free locus of F (AlgebraicGeometry.Space.range_pointsMap_relativeMap_subset_etaleRankOneFreeLocus); the easy inclusion of the base-change clause of Stacks 0CZT carries that locus forward along X_g (AlgebraicGeometry.Space.preimage_etaleRankOneFreeLocus_subset, a pullback of a rank-one free module being rank-one free); and a module whose rank-one étale free locus is all of |X_{T'}| has rank one on the small étale site (AlgebraicGeometry.Space.isFiniteLocallyFreeOfRank_one_of_forall_mem_etaleRankOneFreeLocus, the local-to-global refinement), hence is invertible by the unconditional clause of Stacks 0B8Q (AlgebraicGeometry.Space.isInvertibleModule_iff_isFiniteLocallyFreeOfRank_one).

Neither the base-change clause of Stacks 0CZT nor the source's decomposition of X_T by rank is used: the hard inclusion of that clause is what the converse implication needs, and the decomposition is replaced by pinning the rank to one at the level of the locus.

theorem isInvertibleModule_modulePullback_relativeMap_of_subset_fibrewiseEtaleRankOneFreeLocus
    (D : CoherentSituation B S hS) {T' T : SchemesOver D.Y} (g : T' ⟶ T)
    (F : Modules.{u, u} B S hS (D.space T).1 (D.space T).2)
    (hg : Set.range (pointsMap B S hS ((schemeSpaceFunctor B S hS).obj T'.left).1
        ((schemeSpaceFunctor B S hS).map g.left).hom) ⊆
      fibrewiseEtaleRankOneFreeLocus D T F) :
    IsInvertibleModule (D.space T') ((modulePullback B S hS (D.relativeMap g)).obj F)

AlgebraicGeometry.Space.picardToCoherentHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackToCoherentStack.lean, line 112. The attribute's comment: “the natural map Picardstack_{X/B} -> Cohstack_{X/B} on hom-sets, together with picardObjectToCoherent on objects: the first part of the source's proof, in which the triple (T, g, L) of Section 0372 is sent to the same triple in Situation 08KB and the morphism (h, a) to the morphism (h, a). The map on hom-sets is a BIJECTION, so the natural map is fully faithful and Picardstack_{X/B} is the full subcategory of Cohstack_{X/B} on the objects with invertible module. The binders are D and the tag's own flatness and properness of f, which the object map needs. The whole statement of the tag is isRepresentableByAlgebraicSpaces_and_isOpenImmersion_picardToCoherent of Quot/PicardStackOpenImmersion.lean.”.

Stacks 0D03, the natural map on hom-sets is a bijection. The hom-sets of Pic_{X/B} and of Coh_{X/B} between two objects and their images are the same pair of data — a morphism of test schemes over the base and an isomorphism of the inverse image of the module of the target with the module of the source — so the natural map identifies them.

So the natural map is fully faithful, and Pic_{X/B} is the full subcategory of Coh_{X/B} on the objects whose module is invertible: the fibre of the map over an object (T, g, F) of Coh_{X/B} is the set of proofs that F is invertible, which is a subsingleton. That is the structural reason the tag asserts an open immersion rather than a general morphism.

def picardToCoherentHomEquiv (D : CoherentSituation B S hS) (hflat : IsFlat B S hS D.f.hom)
    (hproper : IsProper B S hS D.f.hom) (A C : PicardObject D.toPicardSituation) :
    PicardHom A C ≃ CoherentHom (picardObjectToCoherent D hflat hproper A)
      (picardObjectToCoherent D hflat hproper C)

Tag 0D04, a proposition

Tag 0D04 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.isAlgebraicStack_picardCFG, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Quot/PicardStackAlgebraicRegistration.lean, line 30 (StacksFrontier): “the full statement. f : X ⟶ B is flat (hflat), of finite presentation (a field of the standing datum D of Situation 08KB) and proper (hproper); then Picardstack_{X/B} is an algebraic stack. Nothing is assumed beyond the source's hypotheses.”.

Sources

LeanAlgebraicGeometry.Space.picardToCoherent · AlgebraicGeometry.Space.range_subset_fibrewiseEtaleRankOneFreeLocus_of_isInvertibleModule · AlgebraicGeometry.Space.hasOpenLocus_picardToCoherent · AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_and_isOpenImmersion_picardToCoherent · AlgebraicGeometry.Space.picardObjectToCoherent · AlgebraicGeometry.Space.isOpen_fibrewiseEtaleFreeLocus · AlgebraicGeometry.Space.isOpen_fibrewiseEtaleRankOneFreeLocus · AlgebraicGeometry.Space.range_pointsMap_relativeMap_subset_etaleFreeLocus

Section99.11 The Picard functor #

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

Tag 0D25, a situation

Tag 0D25 in the Stacks Project.

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

Stacks 0D25. The standing data of the relative Picard functor: a morphism f : X ⟶ base of algebraic spaces over the scheme S.

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

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

Stacks 0D25. The presheaf T ↦ Pic(X_T) on the schemes over the base, whose fppf sheafification is the relative Picard functor. Its action on a morphism of test schemes is pullback of Picard classes.

def picardPresheaf : (s.SchemesOver)ᵒᵖ ⥤ Type (u + 1)

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

Stacks 0D25. The relative Picard functor Pic_{X/base} : (Sch/base)ᵒᵖ ⥤ Sets: the fppf sheafification of the presheaf T ↦ Pic(X_T) of isomorphism classes of invertible modules on the base changes.

def picardFunctor : (s.SchemesOver)ᵒᵖ ⥤ Type (u + 1)

Tag 0D26, a lemma

Tag 0D26 in the Stacks Project.

AlgebraicGeometry.Space.PicardSituation.fibreIsoClassEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardFunctorSheafification.lean, line 227. The attribute's comment: “ONLY the identification of Ob(Picardstack_{X/B,T})/≅ with Pic(X_T) at one test scheme; the sheafification statement is isIso_sheafifyLift_toPicardFunctorOfIsoClasses”.

Ob(Picardstack_{X/B, T})/≅ is Pic(X_T). The isomorphism class of an object of the fibre of the Picard stack over T goes to the class in Pic(X_T) of its invertible module.

def fibreIsoClassEquiv (T : s.SchemesOver) :
    _root_.Quotient (isIsomorphicSetoid
        ((picardProjection (modulePushforwardCoherence B S hS) s).Fiber T)) ≃ s.picardAt T

AlgebraicGeometry.Space.PicardSituation.isoClassPresheafIsoPicardPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardFunctorSheafification.lean, line 294. The attribute's comment: “ONLY the identification of the presheaf T ↦ Ob(Picardstack_{X/B,T})/≅ with the presheaf T ↦ Pic(X_T); the sheafification statement is isIso_sheafifyLift_toPicardFunctorOfIsoClasses”.

The presheaf T ↦ Ob(Picardstack_{X/B, T})/≅ is the presheaf T ↦ Pic(X_T). At each test scheme it is AlgebraicGeometry.Space.PicardSituation.fibreIsoClassEquiv.

def isoClassPresheafIsoPicardPresheaf :
    (picardProjection (modulePushforwardCoherence B S hS) s).isoClassPresheaf ≅
      s.picardPresheaf

AlgebraicGeometry.Space.PicardSituation.isIso_sheafifyLift_toPicardFunctorOfIsoClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardFunctorSheafification.lean, line 318. The attribute's comment: “the relative Picard functor is the fppf sheafification of the presheaf of isomorphism classes of objects of the fibres of the Picard stack”.

In Situation 0D25 the relative Picard functor Pic_{X/B} is the fppf sheafification of the presheaf T ↦ Ob(Picardstack_{X/B, T})/≅ of isomorphism classes of objects of the fibre categories of the Picard stack: Pic_{X/B} is an fppf sheaf (AlgebraicGeometry.Space.PicardSituation.isSheaf_picardFunctor) and the canonical map AlgebraicGeometry.Space.PicardSituation.toPicardFunctorOfIsoClasses from that presheaf into it factors through the sheafification by an isomorphism.

theorem isIso_sheafifyLift_toPicardFunctorOfIsoClasses :
    IsIso (sheafifyLift s.fppfTopology s.toPicardFunctorOfIsoClasses s.isSheaf_picardFunctor)

Tag 0D27, a lemma

Tag 0D27 in the Stacks Project.

AlgebraicGeometry.Space.PicardSituation.exact_picardSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardExactSequence.lean, line 98.

Stacks 0D27. In Situation 0D25, if 𝒪_T ⟶ f_{T, *}𝒪_{X_T} is an isomorphism for every scheme T over the base, then for every such T the sequence 0 ⟶ Pic(T) ⟶ Pic(X_T) ⟶ Pic_{X/B}(T) is exact: pullback along f_T is injective, and a class of X_T maps to the trivial element of the relative Picard functor exactly when it is pulled back from T.

theorem exact_picardSequence (h : s.StructureSheafMapIso) (T : s.SchemesOver) :
    Function.Injective (s.basePicardPullback T) ∧
      ∀ x : s.picardAt T, s.picardClassMap T x = s.picardClassMap T 0 ↔
        x ∈ Set.range (s.basePicardPullback T)

AlgebraicGeometry.Space.PicardSituation.injective_basePicardPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardFunctor.lean, line 460. The attribute's comment: “exactness at the Picard group of the test scheme, conditional on the unit of the Stacks 03LU adjunction being an isomorphism at an invertible module”.

Stacks 0D27, exactness at Pic(T). If 𝒪_T ⟶ f_{T, *}𝒪_{X_T} is an isomorphism for every scheme T over the base, then pullback along f_T is an injection Pic(T) ⟶ Pic(X_T): an invertible 𝒪_T-module is determined up to isomorphism by its inverse image on X_T.

theorem injective_basePicardPullback (hu : ModulePushforwardUnitIso B S hS)
    (h : s.StructureSheafMapIso) (T : s.SchemesOver) :
    Function.Injective (s.basePicardPullback T)

Tag 0D28, a lemma

Tag 0D28 in the Stacks Project.

AlgebraicGeometry.Space.PicardSituation.picardSequence_splitExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardSequenceSplitExact.lean, line 268.

In Situation 0D25 let σ : B ⟶ X be a section of f, and assume that 𝒪_T ⟶ f_{T, *}𝒪_{X_T} is an isomorphism for every scheme T over B. Then for every T

0 ⟶ Pic(T) ⟶ Pic(X_T) ⟶ Pic_{X/B}(T) ⟶ 0

is a split exact sequence with splitting σ_T^* : Pic(X_T) ⟶ Pic(T), the first arrow being pullback along f_T : X_T ⟶ T and the second the canonical map to the fppf sheafification Pic_{X/B}. Spelled out:

the first arrow is injective;

two classes on X_T have the same image in Pic_{X/B}(T) exactly when they differ by a class pulled back from T, and in particular (exactness at Pic(X_T)) a class maps to the image of the trivial class exactly when it is pulled back from T;

the second arrow is surjective;

σ_T^* is a left inverse of the first arrow;

the second arrow restricts to a bijection from the kernel of σ_T^* onto Pic_{X/B}(T), the identification Pic_{X/B}(T) = ker(σ_T^*) of the proof.

theorem picardSequence_splitExact (hstr : s.StructureSheafMapIso) (T : s.SchemesOver) :
    Function.Injective (s.basePicardPullback T) ∧
      (∀ x y : s.picardAt T, s.picardClassMap T x = s.picardClassMap T y ↔
        x - y ∈ Set.range (s.basePicardPullback T)) ∧
      (∀ x : s.picardAt T, s.picardClassMap T x = s.picardClassMap T 0 ↔
        x ∈ Set.range (s.basePicardPullback T)) ∧
      Function.Surjective (s.picardClassMap T) ∧
      Function.LeftInverse (sectionPicardPullback σ hσ T) (s.basePicardPullback T) ∧
      Function.Bijective (fun x : (sectionPicardPullbackHom σ hσ T).ker ↦
        s.picardClassMap T (x : s.picardAt T))

AlgebraicGeometry.Space.PicardSituation.leftInverse_sectionPicardPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardSequenceSplitting.lean, line 253. The attribute's comment: “auxiliary: the splitting by σ_T^* for an arbitrary 03LU coherence datum; the full statement, with no hypothesis, is picardSequence_splitExact”.

Stacks 0D28, the splitting. Pullback of Picard classes along the section σ_T : T ⟶ X_T of the base change retracts pullback along the projection f_T : X_T ⟶ T: σ_T^* ∘ f_T^* is the identity of Pic(T). This is the splitting of the sequence

0 ⟶ Pic(T) ⟶ Pic(X_T) ⟶ Pic_{X/B}(T) ⟶ 0

of Stacks 0D28, and it holds with no hypothesis on 𝒪_T ⟶ f_{T, *}𝒪_{X_T}.

theorem leftInverse_sectionPicardPullback (hc : ModulePushforwardCoherence B S hS)
    (σ : s.base ⟶ s.X) (hσ : σ ≫ s.f = 𝟙 s.base) (T : s.SchemesOver) :
    Function.LeftInverse (sectionPicardPullback σ hσ T) (s.basePicardPullback T)

AlgebraicGeometry.Space.PicardSituation.injective_basePicardPullback_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardSequenceSplitting.lean, line 267. The attribute's comment: “auxiliary: exactness at Pic(T) for an arbitrary 03LU coherence datum; the full statement, with no hypothesis, is picardSequence_splitExact”.

Stacks 0D28, exactness at Pic(T). In Situation 0D25 with a section σ : B ⟶ X of f, pullback along the projection f_T : X_T ⟶ T of the base change is an injection Pic(T) ⟶ Pic(X_T): it is retracted by σ_T^*.

Stacks 0D27 obtains the same conclusion from 𝒪_T ⟶ f_{T, *}𝒪_{X_T} being an isomorphism; with a section neither that hypothesis nor the unit of the Stacks 03LU adjunction being an isomorphism at an invertible module is needed.

theorem injective_basePicardPullback_of_section (hc : ModulePushforwardCoherence B S hS)
    (σ : s.base ⟶ s.X) (hσ : σ ≫ s.f = 𝟙 s.base) (T : s.SchemesOver) :
    Function.Injective (s.basePicardPullback T)

AlgebraicGeometry.Space.PicardSituation.existsUnique_add_sectionPicardPullback_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardSequenceSplitting.lean, line 293. The attribute's comment: “auxiliary: the direct sum decomposition for an arbitrary 03LU coherence datum; the full statement, with no hypothesis, is picardSequence_splitExact”.

Stacks 0D28, the direct sum decomposition. The splitting makes Pic(X_T) the direct sum of the image of Pic(T) under f_T^* and the kernel of σ_T^*: every Picard class on X_T is the sum of the pullback of a unique Picard class on T and a unique class killed by σ_T^*.

This is what "the sequence of Stacks 0D28 is split" says internally to Pic(X_T); the identification of the kernel of σ_T^* with Pic_{X/B}(T), which is the remaining content of Stacks 0D28, is not proved here.

theorem existsUnique_add_sectionPicardPullback_eq_zero (hc : ModulePushforwardCoherence B S hS)
    (σ : s.base ⟶ s.X) (hσ : σ ≫ s.f = 𝟙 s.base) (T : s.SchemesOver) (x : s.picardAt T) :
    ∃! p : s.basePicardAt T × s.picardAt T,
      sectionPicardPullback σ hσ T p.2 = 0 ∧
        x = s.basePicardPullback T p.1 + p.2

Tag 0D29, a lemma

Tag 0D29 in the Stacks Project.

AlgebraicGeometry.Space.sectionedPicardCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackCategory.lean, line 380. The attribute's comment: “the rigidified category Picardstack_{X/B, sigma}, conditional on the pseudofunctoriality of the restriction along the section”.

Stacks 0D29, the category Picardstack_{X/B, σ}. The objects are the quadruples (T, h, L, α) and the morphisms are the morphisms of Picardstack_{X/B} compatible with the trivialisations; the identities and the composition are those of Picardstack_{X/B}.

def sectionedPicardCategory (hc : ModulePushforwardCoherence B S hS)
    (ht : SectionTransportCoherence hc σ hσ) :
    Category.{u + 1} (PicardSituation.SectionedPicardObject σ hσ)

AlgebraicGeometry.Space.forgetTrivializationBased, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackCategory.lean, line 480. The attribute's comment: “the functor forgetting the trivialization along the section, as a functor over the big fppf site”.

Stacks 0D29, the functor Picardstack_{X/B, σ} ⟶ Picardstack_{X/B} forgetting the trivialisation along the section, as a functor over the big fppf site of S.

def forgetTrivializationBased (hc : ModulePushforwardCoherence B S hS)
    (ht : SectionTransportCoherence hc σ hσ) :
    sectionedPicardBasedCategory hc ht ⥤ᵇ picardBasedCategory hc s

AlgebraicGeometry.Space.forgetTrivialization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackCategory.lean, line 504. The attribute's comment: “the 1-morphism of categories fibred in groupoids forgetting the trivialization along the section”.

Stacks 0D29, the 1-morphism Picardstack_{X/B, σ} ⟶ Picardstack_{X/B} of the 2-category of categories fibred in groupoids over the big fppf site of S.

def forgetTrivialization (hc : ModulePushforwardCoherence B S hS)
    (ht : SectionTransportCoherence hc σ hσ) :
    sectionedPicardCFG hc ht ⟶ picardCFG hc s

AlgebraicGeometry.Space.sectionedPicardCFG_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackSectionedIsStack.lean, line 541.

Stacks 0D29. In Situation 0D25, given a section σ of f : X ⟶ B, the rigidified Picard stack Picardstack_{X/B, σ} is a stack in groupoids over (Sch/S)_fppf.

theorem sectionedPicardCFG_isStackInGroupoids (s : PicardSituation B S hS) (σ : s.base ⟶ s.X)
    (hσ : σ ≫ s.f = 𝟙 s.base) :
    (sectionedPicardCFG (modulePushforwardCoherence B S hS)
      (sectionTransportCoherence _ σ hσ)).val.p.IsStackInGroupoids.{w}
        (BigFppfOver.topology B S hS)

Tag 0D2A, a lemma

Tag 0D2A in the Stacks Project.

AlgebraicGeometry.Space.forgetTrivialization_representable_surjective_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardForgetTrivializationRepresentable.lean, line 475.

In Situation 0D25, let σ : B ⟶ X be a section. The 1-morphism Picardstack_{X/B, σ} ⟶ Picardstack_{X/B} forgetting the trivialisation is representable, surjective and smooth: its base change along every 1-morphism from a slice of the site is represented by an object of the site (Stacks 02Y7, 04ST), it is representable by algebraic spaces (Stacks 02ZW), and every algebraic space representing its base change along a scheme-valued point has surjective and smooth structural morphism (Stacks 03YK, 04SX).

theorem forgetTrivialization_representable_surjective_smooth :
    Stacks.RepresentableMorphism.IsRepresentableMorphism
        (sectionedPicardCFG (modulePushforwardCoherence B S hS)
          (sectionTransportCoherence (modulePushforwardCoherence B S hS) σ hσ)).val.p
        (picardCFG (modulePushforwardCoherence B S hS) s).val.p
        (forgetTrivialization (modulePushforwardCoherence B S hS)
          (sectionTransportCoherence (modulePushforwardCoherence B S hS) σ hσ)).hom.toFunctor ∧
      ∃ hf : Stack.IsRepresentableByAlgebraicSpaces B S hS
          (forgetTrivialization (modulePushforwardCoherence B S hS)
            (sectionTransportCoherence (modulePushforwardCoherence B S hS) σ hσ)).hom,
        Stack.HasRelativeProperty.{u, u + 1, u + 1, u} B S hS
            (Space.surjectiveMorphismProperty B S hS)
            (forgetTrivialization (modulePushforwardCoherence B S hS)
              (sectionTransportCoherence (modulePushforwardCoherence B S hS) σ hσ)) hf ∧
          Stack.HasRelativeProperty.{u, u + 1, u + 1, u} B S hS
            (Space.smoothMorphismProperty B S hS)
            (forgetTrivialization (modulePushforwardCoherence B S hS)
              (sectionTransportCoherence (modulePushforwardCoherence B S hS) σ hσ)) hf

AlgebraicGeometry.Space.forgetTrivializationFibreEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackCategory.lean, line 528. The attribute's comment: “ONLY the fibre identification the proof rests on: the fibre of Picardstack_{X/B,sigma} -> Picardstack_{X/B} over (T,h,L) is the set of trivializations O_T = sigma_T^L, that is Isom_T(O_T, sigma_T^L). NONE of the three clauses - representable, surjective, smooth - is proved; see the implementation notes of this file for the three obstructions”.

The fibre of the 1-morphism of Stacks 0D2A is the set of trivialisations along the section. The objects of Picardstack_{X/B, σ} lying over an object (T, h, L) of Picardstack_{X/B} are the quadruples (T, h, L, α), so they correspond bijectively to the trivialisations α : 𝒪_T ≅ σ_T^*L; the fibre is Isom_T(𝒪_T, σ_T^*L), which is the identification the source's proof of Stacks 0D2A rests on.

def forgetTrivializationFibreEquiv (A : PicardObject s) :
    (structureModule (s.baseSpaceAt A.T) ≅
        (PicardSituation.sectionPullback σ hσ A.T).obj A.lineBundle) ≃
      {A' : PicardSituation.SectionedPicardObject σ hσ // A'.toPicardObject = A}

AlgebraicGeometry.Space.exists_sectionedPicardObject_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackCategory.lean, line 549. The attribute's comment: “ONLY the object-level content of clause (2): an object (T,h,L) of Picardstack_{X/B} lifts along the 1-morphism of this tag exactly when sigma_T^*[L] = 0 in Pic(T). The three clauses themselves - representable, surjective and smooth in the sense of Stacks 02ZW and 03YK - are NOT proved; see the implementation notes of this file”.

An object of Picardstack_{X/B} lies in the image of the 1-morphism of Stacks 0D2A exactly when the class of its invertible module is killed by σ_T^*. By the fibre identification a lift is a trivialisation of L along the section, and by Stacks 0D2B such a trivialisation exists exactly when σ_T^*[L] = 0 in Pic(T).

theorem exists_sectionedPicardObject_iff (A : PicardObject s) :
    (∃ A' : PicardSituation.SectionedPicardObject σ hσ, A'.toPicardObject = A) ↔
      PicardSituation.sectionPicardPullback σ hσ A.T
        (picardClass (s.baseChange A.T) A.lineBundle A.invertible) = 0

Tag 0D2B, a lemma

Tag 0D2B in the Stacks Project.

AlgebraicGeometry.Space.PicardSituation.sectionPicardPullback_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackSection.lean, line 253. The attribute's comment: “the index set of the disjoint union: the kernel of σ_T^* on Pic(X_T) is exactly the set of classes of the invertible modules admitting a trivialisation along σ_T, i.e. of those underlying an object of Picardstack_{X/B, σ}. The fibred-in-setoids conclusion and the injectivity of the description are NOT proved: both need the global units of the structure sheaf of an algebraic space, which this development does not carry”.

The elements of the kernel of σ_T^* are exactly the Picard classes of the invertible 𝒪_{X_T}-modules carrying a trivialisation along σ_T.

This is the identification of the index set of the disjoint union of Stacks 0D2B: for a test scheme (T, h) over the base, the invertible modules underlying the objects of Picardstack_{X/B, σ} over (T, h) — the modules L for which a rigidifying isomorphism α : σ_T^*L ≅ 𝒪_T exists — are precisely those whose class is killed by σ_T^* : Pic(X_T) ⟶ Pic(T). Stacks 0D2B's description of the isomorphism classes of Picardstack_{X/B, σ} over T as ⨿_h ker(σ_T^*) is the sum of this statement over the objects (T, h) of AlgebraicGeometry.Space.PicardSituation.SchemesOver.

The two other halves of Stacks 0D2B are not proved: that the stack is fibred in setoids, and that two objects with the same underlying class are isomorphic. Both need the global units of the structure sheaf of an algebraic space, which this development does not carry; see the implementation notes of the file.

theorem sectionPicardPullback_eq_zero_iff (σ : s.base ⟶ s.X) (hσ : σ ≫ s.f = 𝟙 s.base)
    (T : s.SchemesOver) (x : s.picardAt T) :
    sectionPicardPullback σ hσ T x = 0 ↔
      ∃ (L : Modules.{u, u} B S hS (s.baseChange T).1 (s.baseChange T).2)
        (hL : IsInvertibleModule (s.baseChange T) L), picardClass _ L hL = x ∧
          Nonempty ((modulePullback B S hS (baseChangeSection σ hσ T)).obj L ≅
            structureModule (s.baseSpaceAt T))

AlgebraicGeometry.Space.sectionedPicardCFG_isFiberedInSetoids_and_isoClassEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackSectionSetoid.lean, line 437.

In Situation 0D25, let σ be a section of f : X ⟶ B and assume that 𝒪_T ⟶ f_{T, *}𝒪_{X_T} is an isomorphism for every test scheme T over B. Then Picardstack_{X/B, σ} ⟶ (Sch/S)_{fppf} is fibred in setoids, and its set of isomorphism classes over a scheme T is ∐_{h : T ⟶ B} Ker(σ_T^* : Pic(X ×_{B, h} T) ⟶ Pic(T)), through the bijection AlgebraicGeometry.Space.sectionedPicardIsoClassEquiv sending the class of (T, h, L, α) to (h, [L]).

Picardstack_{X/B, σ} is AlgebraicGeometry.Space.sectionedPicardCFG at the pseudofunctoriality AlgebraicGeometry.Space.modulePushforwardCoherence of Stacks 03LU and the coherence AlgebraicGeometry.Space.sectionTransportCoherence of the restriction along the section, both unconditional.

theorem sectionedPicardCFG_isFiberedInSetoids_and_isoClassEquiv {s : PicardSituation B S hS}
    (σ : s.base ⟶ s.X) (hσ : σ ≫ s.f = 𝟙 s.base) (hstr : s.StructureSheafMapIso) :
    (sectionedPicardCFG (modulePushforwardCoherence B S hS)
        (sectionTransportCoherence _ σ hσ)).val.p.IsFiberedInSetoids ∧
      ∀ A : PicardSituation.SectionedPicardObject σ hσ,
        sectionedPicardIsoClassEquiv (modulePushforwardCoherence B S hS)
            (sectionTransportCoherence _ σ hσ) hstr A.testScheme.left
            (Quotient.mk _ ⟨A, rfl⟩) =
          ⟨A.testScheme.hom, ⟨picardClass _ A.toPicardObject.lineBundle
            A.toPicardObject.invertible,
            (PicardSituation.sectionPicardPullback_picardClass_eq_zero_iff σ hσ A.testScheme
              _ _).2 ⟨A.trivialization.symm⟩⟩⟩

Tag 0D2C, a proposition

Tag 0D2C in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpaceOver_picardFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardFunctorIsAlgebraicSpace.lean, line 93. The attribute's comment: “the full statement: f flat (hflat), of finite presentation (hfp) and proper (hproper), and O_T -> f_{T,*}O_{X_T} an isomorphism for every scheme T over the base (hstr); Pic_{X/B} is an algebraic space over B”.

The Picard functor is an algebraic space. Let S be a scheme and f : X ⟶ Y a morphism of algebraic spaces over S such that

f is flat, of finite presentation and proper, and

𝒪_T ⟶ f_{T, *}𝒪_{X_T} is an isomorphism for all schemes T over Y.

Then the relative Picard functor Pic_{X/Y} is an algebraic space over Y.

theorem isAlgebraicSpaceOver_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) :
    IsAlgebraicSpaceOver (PicardSituation.mk X Y f).picardFunctor

Tag 0D2D, a lemma

Tag 0D2D in the Stacks Project.

AlgebraicGeometry.Space.PicardSituation.isImmersion_picardEqualizer_and_isLocallySeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardDiagonalImmersion.lean, line 244.

Let f : X ⟶ B be a morphism of algebraic spaces over S which is flat, of finite presentation and proper, such that 𝒪_T ⟶ f_{T,*}𝒪_{X_T} is an isomorphism for every scheme T over B. Then the diagonal Pic_{X/B} ⟶ Pic_{X/B} ×_B Pic_{X/B} is representable by immersions: for every scheme T over B and all x, y ∈ Pic_{X/B}(T), the subfunctor of h_T of the morphisms T' ⟶ T with x|_{T'} = y|_{T'} (the base change of the diagonal along (x, y)) is represented by immersions. In other words, Pic_{X/B} ⟶ B is locally separated: every morphism of presheaves q : F ⟶ B whose fibres are identified with Pic_{X/B}, naturally in the test scheme, has diagonal an immersion.

theorem isImmersion_picardEqualizer_and_isLocallySeparated (hflat : IsFlat B S hS s.f.hom)
    (hfp : IsFinitePresentation B S hS s.f.hom) (hp : IsProper B S hS s.f.hom)
    (h : s.StructureSheafMapIso) :
    (∀ (T : s.SchemesOver) (x y : s.picardFunctor.obj (op T)),
      IsImmersion B S hS (s.picardEqualizer T x y).ι) ∧
    ∀ (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (q : F ⟶ s.base.1)
      (e : ∀ T : s.SchemesOver, s.picardFunctor.obj (op T) ≃
        {x : F.obj (op T.left) //
          q.app (op T.left) x =
            yonedaEquiv (show yoneda.obj T.left ⟶ s.base.1 from T.hom.hom)}),
      (∀ (T U : s.SchemesOver) (g : T ⟶ U) (x : s.picardFunctor.obj (op U)),
        (e T (s.picardFunctor.map g.op x)).val = F.map g.left.op (e U x).val) →
      IsLocallySeparated B S hS q

Sources

Section99.12 Relative morphisms #

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

Tag 0D1A, a lemma

Tag 0D1A in the Stacks Project.

AlgebraicGeometry.Space.graphTransformation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/GraphOfRelativeMorphism.lean, line 414. The attribute's comment: “the graph transformation”.

Stacks 0D1A. The graph transformation Mor_Q(Z, X) ⟶ Hilb_{Z ×_Q X / Q}: it carries a relative morphism (a, b) at a test scheme T to the graph of b, a closed subspace of (Z ×_Q X)_T which is of finite presentation, flat and proper over T because z is. It is natural because the graph of a restriction is the inverse image of the graph (AlgebraicGeometry.Space.range_graphMap_restrict). The source is composed with the universe lift, the Hilbert presheaf taking values one universe up.

def graphTransformation (hsep : IsSeparated B S hS x) (hfp : IsFinitePresentation B S hS z)
    (hflat : IsFlat B S hS z) (hproper : IsProper B S hS z) :
    relativeHom B S hS Z X Q z x hZ hX hQ ⋙ uliftFunctor.{u + 1, u} ⟶
      hilbertPresheaf (graphAmbientMap B S hS z x hZ hX hQ)

AlgebraicGeometry.Space.graphTransformation_app_family_Z, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/GraphOfRelativeMorphism.lean, line 449. The attribute's comment: “the transformation is the graph”.

Stacks 0D1A. The graph transformation maps a relative morphism to its graph: the closed subspace of the family it produces is the range of the graph map.

theorem graphTransformation_app_family_Z (hsep : IsSeparated B S hS x)
    (hfp : IsFinitePresentation B S hS z) (hflat : IsFlat B S hS z) (hproper : IsProper B S hS z)
    (T : BigFppfOver B S hS) (p : (relativeHom B S hS Z X Q z x hZ hX hQ).obj (Opposite.op T)) :
    ((graphTransformation hZ hX hQ hsep hfp hflat hproper).app (Opposite.op T)
        (ULift.up p)).family.Z =
      Subfunctor.range (graphMap (relativeHomSections B S hS Z X Q z x hZ hX hQ T p))

AlgebraicGeometry.Space.graphTransformation_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/GraphOfRelativeMorphism.lean, line 461. The attribute's comment: “injectivity”.

Stacks 0D1A. The graph transformation is injective at every test scheme: two relative morphisms with the same graph have the same first component, and then AlgebraicGeometry.Space.relativeMorphism_eq_of_range_graphMap_eq identifies them.

theorem graphTransformation_injective (hsep : IsSeparated B S hS x)
    (hfp : IsFinitePresentation B S hS z) (hflat : IsFlat B S hS z) (hproper : IsProper B S hS z)
    (T : BigFppfOver B S hS) :
    Function.Injective
      ((graphTransformation hZ hX hQ hsep hfp hflat hproper).app (Opposite.op T))

Tag 0D1B, a lemma

Tag 0D1B in the Stacks Project.

AlgebraicGeometry.Space.graphTransformation_relative_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeMorphismsOpenInHilbert.lean, line 415.

The graph transformation Mor_Q(Z, X) ⟶ Hilb_{Z ×_Q X / Q} is representable by open immersions.

theorem graphTransformation_relative_isOpenImmersion (hsep : IsSeparated B S hS x)
    (hfp : IsFinitePresentation B S hS z) (hflat : IsFlat B S hS z)
    (hproper : IsProper B S hS z) :
    (MorphismProperty.inverseImage (@AlgebraicGeometry.IsOpenImmersion.{u})
        (BigFppfOver.toScheme B S hS)).relative
      (yoneda ⋙ (Functor.whiskeringRight _ _ _).obj uliftFunctor.{u + 1, u})
      (graphTransformation hZ hX hQ hsep hfp hflat hproper)

Tag 0D1C, a proposition

Tag 0D1C in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_relativeHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeMorphismAlgebraicSpace.lean, line 198. The attribute's comment: “algebraicity”.

Stacks 0D1C, algebraicity. For x of finite presentation and separated and z of finite presentation, flat and proper, the relative morphism functor Mor_Q(Z, X) is an algebraic space over S.

It is realised as an open subspace of a model of the Hilbert functor of Z ×_Q X over Q by Stacks 0D1A and 0D1B, and that model is an algebraic space by Stacks 0D01, AlgebraicGeometry.Space.hasHilbertModelsOver_of_isAlgebraicSpace; an open immersion is representable, so Stacks 02WY transfers algebraicity to the source.

theorem isAlgebraicSpace_relativeHom (hx_fp : IsFinitePresentation B S hS x)
    (hx_sep : IsSeparated 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) :
    IsAlgebraicSpace B S hS (relativeHom B S hS Z X Q z x hZ hX hQ)

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_relativeHomProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeMorphismAlgebraicSpace.lean, line 216. The attribute's comment: “local finite presentation over the base”.

Stacks 0D1C, local finite presentation over the base. For x of finite presentation and separated and z of finite presentation, flat and proper, the projection Mor_Q(Z, X) ⟶ Q is locally of finite presentation.

The projection factors through a model of the Hilbert functor of Z ×_Q X over Q (AlgebraicGeometry.Space.morToHilbertModel_comp_toBase); the first factor is an open immersion, hence locally of finite presentation, and the second is locally of finite presentation by Stacks 0D01, AlgebraicGeometry.Space.hasHilbertModelsOver_of_isAlgebraicSpace.

theorem isLocallyOfFinitePresentation_relativeHomProjection
    (hx_fp : IsFinitePresentation B S hS x) (hx_sep : IsSeparated 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) :
    IsLocallyOfFinitePresentation B S hS
      (relativeHomProjection B S hS Z X Q z x hZ hX hQ)

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

Let z : Z ⟶ Q and x : X ⟶ Q be morphisms of algebraic spaces over S. Assume x is of finite presentation and separated, and z is of finite presentation, flat and proper. Then Mor_Q(Z, X) is an algebraic space, and its projection to Q is locally of finite presentation.

theorem isAlgebraicSpace_relativeHom_and_isLocallyOfFinitePresentation
    {Z X Q : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (z : Z ⟶ Q) (x : X ⟶ Q)
    (hZ : IsAlgebraicSpace B S hS Z) (hX : IsAlgebraicSpace B S hS X)
    (hQ : IsAlgebraicSpace B S hS Q)
    (hx_fp : IsFinitePresentation B S hS x) (hx_sep : IsSeparated 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) :
    IsAlgebraicSpace B S hS (relativeHom 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)

Sources

LeanAlgebraicGeometry.Space.graphTransformation · AlgebraicGeometry.Space.graphTransformation_app_family_Z · AlgebraicGeometry.Space.graphTransformation_injective · AlgebraicGeometry.Space.graphTransformation_relative_isOpenImmersion · AlgebraicGeometry.Space.isAlgebraicSpace_relativeHom · AlgebraicGeometry.Space.isLocallyOfFinitePresentation_relativeHomProjection · AlgebraicGeometry.Space.isAlgebraicSpace_relativeHom_and_isLocallyOfFinitePresentation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

99.3 The Hom functor to 99.12 Relative morphisms

Section99.3 The Hom functor#

Tag 08JT, a situation

Tag 08JV, a lemma

Tag 0D3S, a lemma

Tag 08JW, a remark

Tag 08K3, a lemma

Tag 08K4, a lemma

Tag 08K5, a lemma

Tag 08JX, a lemma

Tag 08JY, a lemma

Tag 08K6, a proposition

Sources

Section99.4 The Isom functor#

Tag 08K7, the section

Tag 08K8, a lemma

Tag 0D3T, a lemma

Tag 08K9, a proposition

Sources

Section99.5 The stack of coherent sheaves#

Tag 08KB, a situation

Tag 08W5, a lemma

Tag 08W6, a lemma

Tag 08KC, a lemma

Tag 08LP, a remark

Tag 08KD, a lemma

Tag 08LQ, a lemma

Tag 08W7, a lemma

Tag 08W8, a lemma

Tag 08W9, a lemma

Tag 08WA, a lemma

Tag 08WC, a theorem

Sources

Section99.6 The stack of coherent sheaves in the non-flat case#

Tag 09DS, a theorem

Sources

Section99.7 The functor of quotients#

Tag 082M, a situation

Tag 082N, an equation

Tag 0CZL, an equation

Tag 08IT, a remark

Tag 08IU, a remark

Tag 082P, a lemma

Tag 0D3U, a lemma

Tag 08IV, a lemma

Tag 082Q, a lemma

Tag 08IW, a lemma

Tag 0CZU, a remark

Tag 0CZV, a remark

Sources

Section99.8 The Quot functor#

Tag 09TR, a situation

Tag 09TT, a lemma

Tag 0D3V, a lemma

Tag 09TU, a proposition

Tag 0CZW, a remark

Sources

Section99.9 The Hilbert functor#

Tag 0CZY, a situation

Tag 0D00, a lemma

Tag 0D3W, a lemma

Tag 0D01, a proposition

Sources

Section99.10 The Picard stack#

Tag 0D03, a lemma

Tag 0D04, a proposition

Sources

Section99.11 The Picard functor#

Tag 0D25, a situation

Tag 0D26, a lemma

Tag 0D27, a lemma

Tag 0D28, a lemma

Tag 0D29, a lemma

Tag 0D2A, a lemma

Tag 0D2B, a lemma

Tag 0D2C, a proposition

Tag 0D2D, a lemma

Sources

Section99.12 Relative morphisms#

Tag 0D1A, a lemma

Section99.3 The Hom functor #

Section99.4 The Isom functor #

Section99.5 The stack of coherent sheaves #

Section99.6 The stack of coherent sheaves in the non-flat case #

Section99.7 The functor of quotients #

Section99.8 The Quot functor #

Section99.9 The Hilbert functor #

Section99.10 The Picard stack #

Section99.11 The Picard functor #

Section99.12 Relative morphisms #