102 Limits of Algebraic Stacks

Chapter 102 of the Stacks Project, Limits of Algebraic Stacks, Tag 0CMM: the 5 sections of its 7 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 15 tags are carried by 35 declarations of the repository (all in StacksFrontier) and 3 registered declarations.

Section102.3 Morphisms of finite presentation#

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

Tag 0CMR, a definition

Tag 0CMR in the Stacks Project.

AlgebraicGeometry.Stack.IsLimitPreserving, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingMorphism.lean, line 138.

Stacks 0CMR. A 1-morphism f : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf category of S is limit preserving when, for every cofiltered inverse system of affine schemes over S whose image in schemes has a limiting cone, the canonical square

colim 𝒳_{Uᵢ} ⟶ 𝒳_U, colim 𝒴_{Uᵢ} ⟶ 𝒴_U

of fibre categories, with vertical maps induced by f, is a 2-fibre product.

The square is the determinate one: the vertical map out of the colimit is the colimit of the componentwise maps AlgebraicGeometry.Stack.splitFiberMap of strict split fibres, and the filling 2-cell is, on every colimit generator, the canonical base-change comparison of the fibred 1-morphism underlying f.

abbrev IsLimitPreserving (f : 𝒳 ⟶ 𝒴) : Prop

Tag 0CMS, a lemma

Tag 0CMS in the Stacks Project.

AlgebraicGeometry.Stack.isLimitPreservingOnObjects_of_isLimitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingMorphismObjects.lean, line 77.

Stacks 0CMS. A limit preserving 1-morphism of categories fibred in groupoids over the big fppf category of S is limit preserving on objects: every object over an affine inverse limit, with a cartesian comparison to an object at a finite stage, descends to a later stage.

theorem isLimitPreservingOnObjects_of_isLimitPreserving
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, vX, u + 1, uX}
      (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (hf : IsLimitPreserving.{u, v, w, uX, vX} B S hS f) :
    BigFppfOver.IsLimitPreservingOnObjects.{u, v, w, vX, uX}
      B S hS 𝒳 𝒴 f

Tag 0CMT, a lemma

Tag 0CMT in the Stacks Project.

AlgebraicGeometry.Stack.isLimitPreserving_twoFibreProductSnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingBaseChangeCoherence.lean, line 646.

Stacks 0CMT. The base change p' : 𝒳 ×_𝒴 𝒵 ⟶ 𝒵 of a limit preserving 1-morphism p of categories fibred in groupoids over the big fppf category of a scheme S is limit preserving.

Both conditions are properties of AlgebraicGeometry.Stack.canonicalSquare -- of p' for the conclusion and of p for the hypothesis -- by AlgebraicGeometry.Stack.isLimitPreserving_iff_isTwoFibreProduct_canonicalSquare, and the two squares are 2-cartesian together by AlgebraicGeometry.Stack.isEquivalence_squareComparison_canonicalSquare_twoFibreProductSnd. The input the source leaves implicit is that filtered colimits of categories commute with 2-fibre products, which is what identifies colim (𝒳 ×_𝒴 𝒵)_{Uᵢ} with colim 𝒳_{Uᵢ} ×_{colim 𝒴_{Uᵢ}} colim 𝒵_{Uᵢ}.

theorem isLimitPreserving_twoFibreProductSnd
    (hp : IsLimitPreserving.{u, v, w, max (u + 1) v w, max u v} B S hS p) :
    IsLimitPreserving.{u, v, w, max (u + 1) v w, max u v} B S hS
      (BigFppfOver.twoFibreProductSnd.{u, v, w} B S hS 𝒳 𝒴 𝒵 p q)

AlgebraicGeometry.Stack.isLimitPreservingOnObjects_twoFibreProductSnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingBaseChangeObjects.lean, line 52. The attribute's comment: “limit preservation on objects of the base change”.

The base change along q of a limit preserving 1-morphism p of categories fibred in groupoids over the big fppf category of S is limit preserving on objects: every object of 𝒳 ×_𝒴 𝒵 over an affine inverse limit, with a cartesian comparison to an object of 𝒵 at a finite stage, descends to a later stage.

theorem isLimitPreservingOnObjects_twoFibreProductSnd
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, max u v, u + 1, max (u + 1) v w}
      (BigFppfOver B S hS))
    (p : 𝒳 ⟶ 𝒴) (q : 𝒵 ⟶ 𝒴)
    (hp : IsLimitPreserving.{u, v, w, max (u + 1) v w, max u v} B S hS p) :
    BigFppfOver.IsLimitPreservingOnObjects.{u, v, w} B S hS
      (BigFppfOver.twoFibreProduct B S hS 𝒳 𝒴 𝒵 p q) 𝒵
      (BigFppfOver.twoFibreProductSnd B S hS 𝒳 𝒴 𝒵 p q)

Tag 0CMU, a lemma

Tag 0CMU in the Stacks Project.

AlgebraicGeometry.Stack.isLimitPreserving_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingMorphismComposition.lean, line 134.

Stacks 0CMU. The composite of two limit preserving 1-morphisms of categories fibred in groupoids over the big fppf category of S is limit preserving: the square of Stacks 0CMR for the composite is the horizontal pasting of the two given 2-cartesian squares.

theorem isLimitPreserving_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, vX, u + 1, uX} (BigFppfOver B S hS)}
    (p : 𝒳 ⟶ 𝒴) (q : 𝒴 ⟶ 𝒵)
    (hp : IsLimitPreserving.{u, v, w, uX, vX} B S hS p)
    (hq : IsLimitPreserving.{u, v, w, uX, vX} B S hS q) :
    IsLimitPreserving.{u, v, w, uX, vX} B S hS (p ≫ q)

Tag 0CMV, a lemma

Tag 0CMV in the Stacks Project.

AlgebraicGeometry.Stack.isLimitPreservingOnObjects_of_isLimitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingMorphismObjects.lean, line 77. The attribute's comment: “the implication (1) ⇒ (2), which holds here without the representability hypothesis that Tag 0CMV carries, and for index categories in any universe. The whole three-part equivalence is AlgebraicGeometry.Stack.isLimitPreserving_tfae, for index categories in the universe of the schemes”.

Stacks 0CMS. A limit preserving 1-morphism of categories fibred in groupoids over the big fppf category of S is limit preserving on objects: every object over an affine inverse limit, with a cartesian comparison to an object at a finite stage, descends to a later stage.

theorem isLimitPreservingOnObjects_of_isLimitPreserving
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, vX, u + 1, uX}
      (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (hf : IsLimitPreserving.{u, v, w, uX, vX} B S hS f) :
    BigFppfOver.IsLimitPreservingOnObjects.{u, v, w, vX, uX}
      B S hS 𝒳 𝒴 f

AlgebraicGeometry.Stack.isLimitPreserving_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingRepresentableTFAE.lean, line 134. The attribute's comment: “index categories in the universe of the schemes”.

Stacks 0CMV. For a 1-morphism f : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf category of S which is representable by algebraic spaces the following are equivalent: f is limit preserving (Stacks 0CMR); f is limit preserving on objects (Stacks 06CU); and f is locally of finite presentation in the sense of Stacks 03YK, that is, every algebraic space representing a base change of f along a scheme-valued point of 𝒴 has locally finitely presented structural morphism.

All three conditions are read for index categories in the universe of the schemes; see the implementation notes.

theorem isLimitPreserving_tfae (hp : IsRepresentableByAlgebraicSpaces B S hS f.hom) :
    List.TFAE
      [IsLimitPreserving.{u, u, u, u + 1, u} B S hS f,
       BigFppfOver.IsLimitPreservingOnObjects.{u, u, u, u, u + 1} B S hS 𝒳 𝒴 f,
       ∀ (U : BigFppfOver B S hS)
         (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.obj)
         (_hy : y ⋙ 𝒴.val.p = Over.map U.hom)
         (F : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
         (hF : IsAlgebraicSpace B U.left.1 U.left.2 F),
         Nonempty (StacksRepresentableCFG.EquivalenceOver
           (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.val.p 𝒴.val.p y
             (CatFiberedInGroupoids.homFunctor f))
           (presheafOfCategories (F ⋙ typeToCat)).p) →
         Space.IsLocallyOfFinitePresentation B S hS
           (algebraicSpaceMap B S hS U
             ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj
               ⟨F, hF⟩)).hom]

Declarations registered for the tag:

• AlgebraicGeometry.Stack.isLimitPreservingOnObjects_iff_isLocallyOfFinitePresentation, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingRepresentableTFAE.lean, line 90 (StacksFrontier): “the equivalence of (2) and (3), which is Stacks 06CX”.

Tag 0CMW, a lemma

Tag 0CMW in the Stacks Project.

AlgebraicGeometry.Stack.isFullyFaithfulOnAffineLimits_iff_isEquivalence_squareDiagonalComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingCanonicalDiagonal.lean, line 252. The attribute's comment: “condition (2) as the diagonal of the canonical 0CMR square being an equivalence”.

Condition (2) of Stacks 0CMW is the diagonal of the canonical square being an equivalence. The canonical functor colim 𝒳_{Uᵢ} ⟶ 𝒳_U ×_{𝒴_U} colim 𝒴_{Uᵢ} is fully faithful at every directed limit of affine schemes over S exactly when, at every such limit, the comparison of the square of relative diagonals of AlgebraicGeometry.Stack.canonicalSquare is an equivalence.

This is the half of Stacks 0CMW that does not involve the diagonal 1-morphism Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳: it is the category-theoretic criterion of the source's proof, applied to the determinate square of Stacks 0CMR.

theorem isFullyFaithfulOnAffineLimits_iff_isEquivalence_squareDiagonalComparison (f : 𝒳 ⟶ 𝒴) :
    IsFullyFaithfulOnAffineLimits.{u, v, w, uX, vX} B S hS f ↔
      ∀ (I : Type v) [Category.{w} I] [IsCofiltered I]
        (D : I ⥤ BigAffineFppf B S hS) (c : Cone D),
        IsLimit ((BigAffineFppf.toScheme B S hS).mapCone c) →
        (Cat.squareDiagonalComparison
          (canonicalSquare.{u, v, w, uX, vX} B S hS f (D ⋙ BigAffineFppf.inclusion B S hS)
            ((BigAffineFppf.inclusion B S hS).mapCone c))).IsEquivalence

AlgebraicGeometry.Stack.isFullyFaithfulOnAffineLimits_of_isLimitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingDiagonal.lean, line 135. The attribute's comment: “condition (2) holds for a limit preserving 1-morphism”.

Stacks 0CMW, condition (2) for a limit preserving 1-morphism. If the square of Stacks 0CMR is 2-cartesian then its comparison functor into the explicit 2-fibre product is an equivalence, so the canonical functor colim 𝒳_{Uᵢ} ⟶ 𝒳_U ×_{𝒴_U} colim 𝒴_{Uᵢ} is fully faithful.

theorem isFullyFaithfulOnAffineLimits_of_isLimitPreserving (f : 𝒳 ⟶ 𝒴)
    (hf : IsLimitPreserving.{u, v, w, uX, vX} B S hS f) :
    IsFullyFaithfulOnAffineLimits.{u, v, w, uX, vX} B S hS f

AlgebraicGeometry.Stack.isLimitPreserving_twoFibreProductDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingDiagonalCriterion.lean, line 293.

Stacks 0CMW. The relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 of a 1-morphism of categories fibred in groupoids over the big fppf category of S is limit preserving if and only if, at every directed limit U = lim Uᵢ of affine schemes over S, the canonical functor colim 𝒳_{Uᵢ} ⟶ 𝒳_U ×_{𝒴_U} colim 𝒴_{Uᵢ} is fully faithful.

Both sides are properties of AlgebraicGeometry.Stack.canonicalSquare -- of Δ on the left, of f on the right -- and the two squares are equivalent, so the source's criterion CategoryTheory.Limits.CategoricalPullback.fullyFaithful_squareComparison_iff transfers between them.

theorem isLimitPreserving_twoFibreProductDiagonal_iff :
    IsLimitPreserving.{u, v, w, max (u + 1) v w, max u v} B S hS
        (BigFppfOver.twoFibreProductDiagonal.{u, v, w} B S hS 𝒳 𝒴 f) ↔
      IsFullyFaithfulOnAffineLimits.{u, v, w, max (u + 1) v w, max u v} B S hS f

AlgebraicGeometry.Stack.isLimitPreserving_twoFibreProductDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingDiagonalCriterion.lean, line 317.

Stacks 0CMW, the "in particular" clause. A limit preserving 1-morphism of categories fibred in groupoids has a limit preserving relative diagonal: it satisfies the full faithfulness condition by AlgebraicGeometry.Stack.isFullyFaithfulOnAffineLimits_of_isLimitPreserving, and that condition is limit preservation of the diagonal.

theorem isLimitPreserving_twoFibreProductDiagonal
    (hf : IsLimitPreserving.{u, v, w, max (u + 1) v w, max u v} B S hS f) :
    IsLimitPreserving.{u, v, w, max (u + 1) v w, max u v} B S hS
      (BigFppfOver.twoFibreProductDiagonal.{u, v, w} B S hS 𝒳 𝒴 f)

CategoryTheory.Limits.CategoricalPullback.fullyFaithful_squareComparison_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/CategoricalPullbackSquareDiagonal.lean, line 490. The attribute's comment: “the category-theoretic reduction of the equivalence (1) <=> (2)”.

The category-theoretic core of Stacks 0CMW. For a 2-commutative square of categories whose corners C and D' are groupoids, the comparison functor A : C' ⥤ C ×_D D' is fully faithful if and only if the comparison functor B : C' ⥤ C ×_{Δ_p, C ×_D C} (C' ×_{D'} C') of the square of relative diagonals is an equivalence.

theorem fullyFaithful_squareComparison_iff [IsGroupoid C] [IsGroupoid D'] :
    ((squareComparison a u p b α).Full ∧ (squareComparison a u p b α).Faithful) ↔
      (diagonalComparison a u p b α).IsEquivalence

Tag 0CMX, a lemma

Tag 0CMX in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLimitPreserving_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingOfFinitePresentation.lean, line 84. The attribute's comment: “an algebraic stack locally of finite presentation over S is limit preserving, and so is its structure morphism”.

Stacks 0CMX. Let 𝒳 be an algebraic stack over S whose structure morphism 𝒳 → S is locally of finite presentation. Then 𝒳 is limit preserving in the sense of Artin's Axioms, Definition 07XL: for every cofiltered system of affine schemes Tᵢ over S with limit T, the comparison functor colim 𝒳_{Tᵢ} ⥤ 𝒳_T is an equivalence. Equivalently, the structure morphism 𝒳 → S is limit preserving in the sense of Stacks 0CMR. The index categories are taken in the scheme universe, which is the smallness the source's directed sets have.

theorem isLimitPreserving_of_isLocallyOfFinitePresentation
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (hf : IsLocallyOfFinitePresentation B S hS (structureMorphism B S hS 𝒳)) :
    Deformation.Artin.IsLimitPreserving.{u, u, u, u + 1, u} B S hS 𝒳.val ∧
      Stack.IsLimitPreserving.{u, u, u, u + 1, u} B S hS (structureMorphism B S hS 𝒳).hom

AlgebraicGeometry.Stack.hasPropertyOnSomeSmoothDiagram_relativelyLimitPreserving_structure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingSmoothDiagram.lean, line 157. The attribute's comment: “only the smooth-diagram reduction; the conclusion is not 07XL”.

An algebraic stack locally of finite presentation over its base has a relatively limit preserving smooth presentation. This is AlgebraicGeometry.Stack.hasPropertyOnSomeSmoothDiagram_relativelyLimitPreserving at the structure morphism of Stacks 050D, and it is the algebraic-spaces input to the proof of Stacks 0CMX: the presenting algebraic space of 𝒳 is relatively limit preserving over the algebraic stack represented by S.

The attribute's clause string is deliberately narrow. This statement does not give the conclusion of Stacks 0CMX, which is limit preservation of 𝒳 in the sense of Definition 07XL; what it carries is the tag's first step, and it is the step that consumes the tag's hypothesis — Stack.AlgebraicStacks.IsLocallyOfFinitePresentation on the structure morphism of Stacks 050D is used, not merely stated. Anyone reading the tag as discharged by this declaration would be misreading it: the conclusion here is about a smooth presentation by an algebraic space, in the vocabulary of Stacks 049J, and the remaining step — limit preservation of the quotient stack — is named with its three missing bridges in the implementation notes of this module.

theorem hasPropertyOnSomeSmoothDiagram_relativelyLimitPreserving_structure
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : Stack.AlgebraicStacks.IsLocallyOfFinitePresentation B S hS
      (structureMorphism B S hS 𝒳)) :
    HasPropertyOnSomeSmoothDiagram B S hS
      (fun _ _ h => RelativelyLimitPreserving.{u, u, u, u} B S hS h)
      (structureMorphism B S hS 𝒳).hom

Tag 0CMY, a proposition

Tag 0CMY in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLimitPreserving_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingFinitePresentationEquivalence.lean, line 73. The attribute's comment: “limit preserving, limit preserving on objects and locally of finite presentation are equivalent for a 1-morphism of algebraic stacks”.

For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S the following are equivalent:

1. f is limit preserving in the sense of Stacks 0CMR;
2. f is limit preserving on objects in the sense of Stacks 06CU;
3. f is locally of finite presentation in the sense of Stacks 06Q2.

Index categories are taken in the universe of the schemes.

theorem isLimitPreserving_tfae {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    List.TFAE [Stack.IsLimitPreserving.{u, u, u, u + 1, u} B S hS f.hom,
      BigFppfOver.IsLimitPreservingOnObjects.{u, u, u} B S hS 𝒳.val 𝒴.val f.hom,
      IsLocallyOfFinitePresentation B S hS f]

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFinitePresentation_of_isLimitPreservingOnObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingObjectsFinitePresentation.lean, line 299. The attribute's comment: “the implication (2) => (3) only”.

A 1-morphism of algebraic stacks over S which is limit preserving on objects, at index categories in the universe u of the schemes, is locally of finite presentation.

theorem AlgebraicStacks.isLocallyOfFinitePresentation_of_isLimitPreservingOnObjects
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : BigFppfOver.IsLimitPreservingOnObjects.{u, u, u, u, u + 1}
      B S hS 𝒳.val 𝒴.val f.hom) :
    Stack.AlgebraicStacks.IsLocallyOfFinitePresentation B S hS f

Sources

• Section 102.3, Tag 0CMQ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.IsLimitPreserving · AlgebraicGeometry.Stack.isLimitPreservingOnObjects_of_isLimitPreserving · AlgebraicGeometry.Stack.isLimitPreserving_twoFibreProductSnd · AlgebraicGeometry.Stack.isLimitPreservingOnObjects_twoFibreProductSnd · AlgebraicGeometry.Stack.isLimitPreserving_comp · AlgebraicGeometry.Stack.isLimitPreserving_tfae · AlgebraicGeometry.Stack.isLimitPreservingOnObjects_iff_isLocallyOfFinitePresentation · AlgebraicGeometry.Stack.isFullyFaithfulOnAffineLimits_iff_isEquivalence_squareDiagonalComparison

Section102.4 Descending properties#

Section 102.4 of the Stacks Project, Tag 0CPX. 2 tags here are carried by 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CPY, a situation

Tag 0CPY in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Space.DescentSituation, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties.lean, line 32 (StacksFrontier).

Tag 0CPZ, a lemma

Tag 0CPZ in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Space.DescentSituation.exists_isSeparated_stage_of_siteContainsBaseChangeLimits, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedAtFiniteStageRegistration.lean, line 26 (StacksFrontier): “under the chapter's standing convention of Section 70.2 (tag 07SD) on the system, as for 0851 and 07SQ; without it the statement fails in this bounded site (SiteConventionCounterexample)”.

Sources

• Section 102.4, Tag 0CPX
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.DescentSituation · AlgebraicGeometry.Space.DescentSituation.exists_isSeparated_stage_of_siteContainsBaseChangeLimits

Section102.5 Descending relative objects#

Section 102.5 of the Stacks Project, Tag 0CN3. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CN4, a lemma

Tag 0CN4 in the Stacks Project.

AlgebraicGeometry.Stack.StackDescentSystem.exists_stage_model_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DescendingStacksAlongLimit.lean, line 894. The attribute's comment: “a reduction, not a proof: inputs of the source's proof are carried as the explicit hypotheses hPresentation (Stacks 04T4 (4), (5), Stacks 04T5 (2) and the 050K/050H bookkeeping, with Stacks 04YC discharged), hDescent (what is left of Stacks 07SK and 0CN2 on a groupoid object once the essential-surjectivity clause is discharged: the descent of s, t, c, the pointwiseGroupoid field, the common stage, and Stacks 046Q), hStageStackModel (a universe-lifting datum, not a mathematical assumption: a quotient stack has hom universe one above that of AlgebraicStacks), hModelFinitePresentation (Stacks 06Q2 evaluated on a quotient stack) and hModelComparison (Stacks 044P, 044R, 046Q and 04Y1 for a base-changed groupoid); what is discharged here is Stacks 07SF for the limit with its quasi-compactness and quasi-separatedness, the essential-surjectivity clause of Stacks 07SK for the object and arrow spaces of the presenting groupoid, Stacks 04TK on the descended groupoid, and the assembly of the conclusion”.

Stacks 0CN4. Let (X_i) be a directed inverse system of quasi-compact, quasi-separated algebraic spaces over S with affine transition morphisms, and let X = lim X_i. If 𝒳 is an algebraic stack of finite presentation over X, then there are a stage i and an algebraic stack 𝒳_i of finite presentation over X_i with 𝒳 ≅ 𝒳_i ×_{X_i} X as algebraic stacks over X.

Five inputs are carried as explicit hypotheses — hPresentation, hDescent, hStageStackModel, hModelFinitePresentation and hModelComparison. None is a restatement of this conclusion, and hStageStackModel is a universe-lifting datum rather than a mathematical assumption. The module's implementation notes say what each one is, which declaration of the library it would come from, and — for Stacks 0CN2 — exactly why the existing result falls short. What is discharged here is Stacks 07SF for the limit with its quasi-compactness and quasi-separatedness, the essential-surjectivity clause of Stacks 07SK for the object and arrow spaces of the presenting groupoid, Stacks 04TK on the descended groupoid, and the assembly of the conclusion.

theorem exists_stage_model_of_isFinitePresentation
    (hPresentation : GroupoidPresentationOfAffineSmoothChart.{u, w} B S hS hZ)
    (hDescent : C.GroupoidStructureDescendsToStage)
    (hStageStackModel : C.StageStackModel.{u, w})
    (hModelFinitePresentation : C.ModelIsFinitePresentation.{u, w})
    (hModelComparison : C.ModelBaseChangeComparison.{u, w})
    (𝒳 : AlgebraicStacks.{u, w} B S hS) (f : 𝒳 ⟶ C.limitStack.{u, w})
    (hf : AlgebraicStacks.IsFinitePresentation B S hS f) :
    ∃ (i : Iᵒᵖ) (𝒳ᵢ : AlgebraicStacks.{u, w} B S hS) (fᵢ : 𝒳ᵢ ⟶ C.stageStack.{u, w} i),
      AlgebraicStacks.IsFinitePresentation B S hS fᵢ ∧
        ∃ e : Bicategory.Equivalence 𝒳
          (twoFibreProductAlgebraicStack.{u, w} B S hS fᵢ
            (C.limitStackProjection.{u, w} i)),
          Nonempty (e.hom ≫ (twoFibreProductSquareAlgebraicStacks.{u, w} B S hS fᵢ
            (C.limitStackProjection.{u, w} i)).snd ≅ f)

AlgebraicGeometry.Stack.StackDescentSystem.exists_stage_model_of_isFinitePresentation_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DescendingStacksAlongLimitTheorem.lean, line 76. The attribute's comment: “The directed set I indexes the system as a covariant diagram on the cofiltered category Iᵒᵖ, and StackDescentSystem bounds the cardinality of Iᵒᵖ and of its hom types by the cofinality of the cutoff of the big fppf site, which is what keeps the limit X inside the site. The isomorphism 𝒳 ≅ 𝒳_i ×_{X_i} X over X is an equivalence in the 2-category of algebraic stacks whose forward 1-morphism followed by the projection to X is 2-isomorphic to the structure 1-morphism of 𝒳.”.

Stacks 0CN4. Let (X_i) be a directed inverse system of quasi-compact, quasi-separated algebraic spaces over S with affine transition morphisms, and let X = lim X_i. If 𝒳 is an algebraic stack of finite presentation over X, then there are a stage i and an algebraic stack 𝒳_i of finite presentation over X_i with 𝒳 ≅ 𝒳_i ×_{X_i} X as algebraic stacks over X.

This is the statement of StackDescentSystem.exists_stage_model_of_isFinitePresentation with none of its hypotheses. The system satisfies the chapter's convention (StackDescentSystem.siteContainsBaseChangeLimits), and under the convention the statement is AlgebraicGeometry.Stack.AlgebraicStacks.finitePresentationStackDescendsStatement_holds.

theorem exists_stage_model_of_isFinitePresentation_unconditional
    (C : StackDescentSystem B S hS hZ I)
    (𝒳 : AlgebraicStacks.{u, w} B S hS) (f : 𝒳 ⟶ C.limitStack.{u, w})
    (hf : AlgebraicStacks.IsFinitePresentation B S hS f) :
    ∃ (i : Iᵒᵖ) (𝒳ᵢ : AlgebraicStacks.{u, w} B S hS) (fᵢ : 𝒳ᵢ ⟶ C.stageStack.{u, w} i),
      AlgebraicStacks.IsFinitePresentation B S hS fᵢ ∧
        ∃ e : Bicategory.Equivalence 𝒳
          (twoFibreProductAlgebraicStack.{u, w} B S hS fᵢ
            (C.limitStackProjection.{u, w} i)),
          Nonempty (e.hom ≫ (twoFibreProductSquareAlgebraicStacks.{u, w} B S hS fᵢ
            (C.limitStackProjection.{u, w} i)).snd ≅ f)

Sources

• Section 102.5, Tag 0CN3
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.StackDescentSystem.exists_stage_model_of_isFinitePresentation · AlgebraicGeometry.Stack.StackDescentSystem.exists_stage_model_of_isFinitePresentation_unconditional

Section102.6 Finite type closed in finite presentation#

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

Tag 0CQ1, a lemma

Tag 0CQ1 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exists_isFinitePresentation_isClosedImmersion_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ClosedImmersionIntoFinitePresentationArbitraryBase.lean, line 60.

Stacks 0CQ1. Let f : 𝒳 ⟶ Y be a 1-morphism from an algebraic stack over a scheme S to an algebraic space over S, with f of finite type and quasi-separated and Y quasi-compact and quasi-separated. Then there are a 1-morphism of finite presentation f' : 𝒳' ⟶ Y and a closed immersion i : 𝒳 ⟶ 𝒳' of algebraic stacks over Y, that is, with i ≫ f' ≅ f.

The source's proof, which approximates Y by Noetherian algebraic spaces (Stacks 07SU), takes place over Spec ℤ, where it is AlgebraicGeometry.Stack.exists_finitePresentation_closedImmersion_overIntegers with Stacks 07SU supplied by AlgebraicGeometry.Space.hasNoetherianApproximation_of_isQuasiCompactSpace. Construction A of Stacks 04X5 carries f to a quasi-separated 1-morphism, locally of finite type, from a quasi-compact algebraic stack to the view Λ Y of Y over Spec ℤ, which is again quasi-compact and quasi-separated; the factorization obtained there descends to S (AlgebraicGeometry.Stack.exists_descent_changeBase), and finite presentation and being a closed immersion descend along Construction A.

theorem exists_isFinitePresentation_isClosedImmersion_of_isFiniteType (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S)
    (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hY : IsAlgebraicSpace B S hS Y)
    (𝒳 : AlgebraicStacks.{u, w} B S hS) (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS Y hY)
    (hft : IsFiniteType B S hS f) (hqs : IsQuasiSeparated B S hS f)
    (hYqc : Space.IsQuasiCompactSpace B S hS Y)
    (hYqs : Space.IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y) :
    ∃ (𝒳' : AlgebraicStacks.{u, w} B S hS)
      (f' : 𝒳' ⟶ algebraicSpaceStack.{u, w} B S hS Y hY) (i : 𝒳 ⟶ 𝒳'),
      IsFinitePresentation B S hS f' ∧ IsClosedImmersion B S hS i ∧ Nonempty (i ≫ f' ≅ f)

Tag 0CQ2, a lemma

Tag 0CQ2 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.closedImmersionIntoFinitePresentationStatement_holds_overScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedClosedImmersionIntoFinitePresentationArbitraryBase.lean, line 248.

Stacks 0CQ2. Let f : 𝒳 ⟶ Y be a 1-morphism from an algebraic stack over a scheme S to an algebraic space over S, with f of finite type and separated and Y quasi-compact and quasi-separated. Then there are a separated 1-morphism of finite presentation f' : 𝒳' ⟶ Y and a closed immersion i : 𝒳 ⟶ 𝒳' of algebraic stacks over Y, that is, with i ≫ f' ≅ f.

The source's proof, which approximates Y by Noetherian algebraic spaces (Stacks 07SU), takes place over Spec ℤ, where it is AlgebraicGeometry.Stack.exists_separated_finitePresentation_closedImmersion_overIntegers. Construction A of Stacks 04X5 carries f to a separated 1-morphism, locally of finite type, from a quasi-compact algebraic stack to the view Λ Y of Y over Spec ℤ, which is again quasi-compact and quasi-separated; the factorization obtained there descends to S (AlgebraicGeometry.Stack.exists_descent_changeBase), and separatedness, finite presentation and being a closed immersion descend along Construction A.

theorem closedImmersionIntoFinitePresentationStatement_holds_overScheme (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) :
    ClosedImmersionIntoFinitePresentationStatement.{u, w} B S hS

Sources

• Section 102.6, Tag 0CQ0
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.AlgebraicStacks.exists_isFinitePresentation_isClosedImmersion_of_isFiniteType · AlgebraicGeometry.Stack.AlgebraicStacks.closedImmersionIntoFinitePresentationStatement_holds_overScheme

Section102.7 Universally closed morphisms#

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

Tag 0H29, a lemma

Tag 0H29 in the Stacks Project.

AlgebraicGeometry.exists_affine_locallyFinitePresentation_separation_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/ClosedSubsetFibreSeparation.lean, line 49. The attribute's comment: “the case of schemes, for closed subsets”.

Let f : X ⟶ S be a quasi-compact morphism of schemes, g : T ⟶ S a morphism, t ∈ T a point and E ⊆ X ×_S T a closed subset whose image in T misses t. Then there are an affine open neighbourhood V of t, a commutative square V ⟶ T' ⟶ S, V ⟶ T ⟶ S with T' affine and T' ⟶ S locally of finite presentation, and a closed subset E' ⊆ X ×_S T' whose image in T' misses the image of t, such that the preimage of E in X ×_S V lies in the preimage of E'.

This is the case of schemes, for closed subsets, of the separation lemma for algebraic stacks.

theorem exists_affine_locallyFinitePresentation_separation_isClosed
    {X S T : Scheme.{u}} (f : X ⟶ S) [QuasiCompact f] (g : T ⟶ S)
    (t : T) (E : Set ↥(pullback f g)) (hE : IsClosed E)
    (ht : t ∉ Set.image (pullback.snd f g) E) :
    ∃ (V : T.affineOpens) (htV : t ∈ V.1)
      (T' : Scheme.{u}) (_ : IsAffine T') (b : T' ⟶ S)
      (_ : LocallyOfFinitePresentation b) (a : V.1.toScheme ⟶ T')
      (_ : V.1.ι ≫ g = a ≫ b)
      (E' : Set ↥(pullback f b)) (_ : IsClosed E')
      (p : pullback f (V.1.ι ≫ g) ⟶ pullback f g)
      (q : pullback f (V.1.ι ≫ g) ⟶ pullback f b),
      (p ≫ pullback.fst f g = pullback.fst f (V.1.ι ≫ g)) ∧
      (p ≫ pullback.snd f g = pullback.snd f (V.1.ι ≫ g) ≫ V.1.ι) ∧
      (q ≫ pullback.fst f b = pullback.fst f (V.1.ι ≫ g)) ∧
      (q ≫ pullback.snd f b = pullback.snd f (V.1.ι ≫ g) ≫ a) ∧
      (a ⟨t, htV⟩ ∉ Set.image (pullback.snd f b) E') ∧
      (p ⁻¹' E ⊆ q ⁻¹' E')

AlgebraicGeometry.Stack.exists_affine_finitePresentation_separation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ClosedSubsetSeparationAlgebraicStack.lean, line 438.

Stacks 0H29. Let g : Z ⟶ Y be a morphism of the big fppf category of S between objects with affine underlying schemes, let f : 𝒳 ⟶ Y be a quasi-compact 1-morphism of algebraic stacks over S with 𝒳 quasi-compact, let z be a point of Z and let T ⊆ |𝒳 ×_Y Z| be a closed subset whose image in |Z| misses z. Then there are an open neighbourhood V of z in Z, a commutative square V ⟶ Z' ⟶ Y, V ⟶ Z ⟶ Y, and a closed subset T' ⊆ |𝒳 ×_Y Z'| such that

1. Z' is affine and of finite presentation over Y,
2. the image of z in |Z'| misses the image of T' in |Z'|, and
3. the inverse image of T in |𝒳 ×_Y V| maps into T'.

The two comparison 1-morphisms of the last two clauses are the canonical ones AlgebraicGeometry.Stack.factorMap; their compatibilities with the projections of the three base changes are AlgebraicGeometry.Stack.factorIsoFst and AlgebraicGeometry.Stack.factorIsoSnd.

theorem exists_affine_finitePresentation_separation {Y Z : BigFppfOver B S hS}
    (hY : IsAffine ((BigFppfOver.toScheme B S hS).obj Y))
    (hZ : IsAffine ((BigFppfOver.toScheme B S hS).obj Z)) (g : Z ⟶ Y)
    {𝒳 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ schemeStack.{u, w} B S hS Y)
    (_hf : IsQuasiCompactMorphism.{u, w} B S hS f)
    (h𝒳 : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (z : AlgebraicStacks.points B S hS (schemeStack.{u, w} B S hS Z))
    (T : Set (AlgebraicStacks.points B S hS (baseChangeSquare B S hS f g).pt))
    (hT : @IsClosed _ (pointTopology B S hS (baseChangeSquare B S hS f g).pt.val) T)
    (hz : z ∉ AlgebraicStacks.pointsMap B S hS (baseChangeSquare B S hS f g).fst '' T) :
    ∃ (V : BigFppfOver B S hS) (j : V ⟶ Z),
      AlgebraicGeometry.IsOpenImmersion ((BigFppfOver.toScheme B S hS).map j) ∧
      ∃ v : AlgebraicStacks.points B S hS (schemeStack.{u, w} B S hS V),
        AlgebraicStacks.pointsMap B S hS (schemeStackMap.{u, w} B S hS j) v = z ∧
        ∃ (Z' : BigFppfOver B S hS) (b : Z' ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj Z') ∧
          FinitePresentation ((BigFppfOver.toScheme B S hS).map b) ∧
          ∃ (a : V ⟶ Z') (hab : j ≫ g = a ≫ b)
            (T' : Set (AlgebraicStacks.points B S hS (baseChangeSquare B S hS f b).pt)),
            @IsClosed _ (pointTopology B S hS (baseChangeSquare B S hS f b).pt.val) T' ∧
            AlgebraicStacks.pointsMap B S hS (schemeStackMap.{u, w} B S hS a) v ∉
              AlgebraicStacks.pointsMap B S hS (baseChangeSquare B S hS f b).fst '' T' ∧
            AlgebraicStacks.pointsMap B S hS (factorMap B S hS f (j ≫ g) a b hab) ''
                (AlgebraicStacks.pointsMap B S hS
                  (factorMap B S hS f (j ≫ g) j g rfl) ⁻¹' T) ⊆ T'

AlgebraicGeometry.Stack.AlgebraicStacks.image_preimage_eq_preimage_image_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsCartesianSquare.lean, line 56. The attribute's comment: “the cartesian-square step of the proof, on points”.

For a 2-fibre product square of algebraic stacks over S with legs fst : 𝒫 ⟶ 𝒳 and snd : 𝒫 ⟶ 𝒬 over a cospan g : 𝒳 ⟶ 𝒴, f : 𝒬 ⟶ 𝒴, and for any subset T of |𝒳|, the image in |𝒬| of the preimage of T in |𝒫| is the preimage in |𝒬| of the image of T in |𝒴|.

theorem image_preimage_eq_preimage_image_of_isTwoFibreProduct
    {𝒳 𝒬 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} {g : 𝒳 ⟶ 𝒴} {f : 𝒬 ⟶ 𝒴}
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (T : Set (points B S hS 𝒳)) :
    pointsMap B S hS P.snd '' (pointsMap B S hS P.fst ⁻¹' T) =
      pointsMap B S hS f ⁻¹' (pointsMap B S hS g '' T)

AlgebraicGeometry.Stack.AlgebraicStacks.image_closure_image_subset_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsCartesianSquare.lean, line 80. The attribute's comment: “the descent step of the proof, along a cartesian square with surjective open legs”.

Let P be a 2-fibre product square of algebraic stacks over S with legs fst : 𝒫 ⟶ 𝒳 and snd : 𝒫 ⟶ 𝒬 over a cospan g : 𝒳 ⟶ 𝒴, f : 𝒬 ⟶ 𝒴, with f surjective and open on points, and let π : 𝒴 ⟶ 𝒵 be a 1-morphism. If a closed subset T' ⊆ |𝒬| contains the image of the preimage of T ⊆ |𝒳|, then the image in |𝒵| of the closure of the image of T in |𝒴| is contained in the image of T' in |𝒵|.

theorem image_closure_image_subset_of_isTwoFibreProduct
    {𝒳 𝒬 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} {g : 𝒳 ⟶ 𝒴} {f : 𝒬 ⟶ 𝒴} (π : 𝒴 ⟶ 𝒵)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hsurj : Function.Surjective (pointsMap B S hS f))
    (hopen : letI := Stack.pointTopology B S hS 𝒬.val
      letI := Stack.pointTopology B S hS 𝒴.val
      IsOpenMap (pointsMap B S hS f))
    (T : Set (points B S hS 𝒳)) (T' : Set (points B S hS 𝒬))
    (hT' : letI := Stack.pointTopology B S hS 𝒬.val
      IsClosed T')
    (hsub : pointsMap B S hS P.snd '' (pointsMap B S hS P.fst ⁻¹' T) ⊆ T') :
    letI := Stack.pointTopology B S hS 𝒴.val
    pointsMap B S hS π '' closure (pointsMap B S hS g '' T) ⊆
      pointsMap B S hS (f ≫ π) '' T'

IsOpenMap.image_closure_subset_image_of_preimage_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Maps/ClosureImageSurjectiveOpen.lean, line 26. The attribute's comment: “the closure step of the proof, along a surjective open map”.

For a surjective open continuous map q : X → Y, a closed subset T ⊆ X containing q ⁻¹' A also contains q ⁻¹' closure A; hence the image of closure A along any map π : Y → Z is contained in the image of T along π ∘ q.

theorem IsOpenMap.image_closure_subset_image_of_preimage_subset
    {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] {q : X → Y}
    (hopen : IsOpenMap q) (hcont : Continuous q) (hsurj : Function.Surjective q) (π : Y → Z)
    {A : Set Y} {T : Set X} (hT : IsClosed T) (h : q ⁻¹' A ⊆ T) :
    π '' closure A ⊆ (π ∘ q) '' T

Tag 0H2A, a lemma

Tag 0H2A in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_baseChange_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedSmoothLocal.lean, line 533. The attribute's comment: “closedness of a base change descends along an immersion of the base”.

Stacks 0H2A: closedness of a base change descends along an immersion of the base. Let F : 𝒬 ⟶ ℬ be closed on points and let ι : 𝒞 ⟶ ℬ be an immersion of algebraic stacks over S. Then the base change of F along ι — the map |𝒬 ×_ℬ 𝒞| → |𝒞| — is closed on points.

This is the step of the proof of Stacks 0H2A which writes a closed subset of |𝒳 ×_𝒴 Z| as the pullback of a closed subset of |𝐀ⁿ × 𝒳| along the immersion Z ⟶ 𝐀ⁿ_V of Stacks 04II. The base change of ι is an immersion by Stacks 045C at the immersion property, hence a topological embedding on points by Stacks 0H20; the square is cartesian on points by Stacks 04XH; and isClosedMap_of_isEmbedding_of_cartesian concludes. Only the embedding property of Stacks 0H20 is used, not the local closedness of the range.

theorem isClosed_baseChange_of_isImmersion
    {𝒬 𝒞 ℬ : Stack.AlgebraicStacks.{u, w} B S hS} (F : 𝒬 ⟶ ℬ) (ι : 𝒞 ⟶ ℬ)
    (hι : IsImmersion B S hS ι) (hF : IsClosed B S hS F) :
    IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS ι F).fst

AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_baseChange_affine_isLocallyOfFinitePresentation_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedSmoothLocal.lean, line 620. The attribute's comment: “(1) implies (2)”.

Stacks 0H2A, (1) implies (2). If f is universally closed then, for every object Z of the site whose scheme is affine and every 1-morphism Stack.schemeStack Z ⟶ 𝒴 which is locally of finite presentation, the map |𝒳 ×_𝒴 Z| → |Z| is closed. Neither adjective is used: the clause is the restriction of universal closedness to those bases.

theorem isClosed_baseChange_affine_isLocallyOfFinitePresentation_of_universallyClosed
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : UniversallyClosed B S hS f) :
    ∀ (Z : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
      ∀ (g : Stack.schemeStack.{u, w} B S hS Z ⟶ 𝒴),
        IsLocallyOfFinitePresentation B S hS g →
          IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS g f).fst

AlgebraicGeometry.Stack.AlgebraicStacks.exists_chart_forall_isClosed_baseChange_affineSpaceChart_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedSmoothLocal.lean, line 637. The attribute's comment: “(1) implies (3)”.

Stacks 0H2A, (1) implies (3). If f is universally closed then there are a scheme V of the site and a smooth surjective 1-morphism Stack.schemeStack V ⟶ 𝒴 such that, for every n ≥ 0, the base change of f to affine n-space over V — the map |𝐀^n × (𝒳 ×_𝒴 V)| → |𝐀^n × V| — is closed.

Any smooth surjective chart of 𝒴 by a scheme of the site serves, and every one of the base changes is closed because f is universally closed.

theorem exists_chart_forall_isClosed_baseChange_affineSpaceChart_of_universallyClosed
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : UniversallyClosed B S hS f) :
    ∃ (V : BigFppfOver B S hS) (a : Stack.schemeStack.{u, w} B S hS V ⟶ 𝒴),
      Stack.IsSurjective B S hS a ∧ IsSmooth B S hS a ∧
        ∀ n : ℕ, IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS
          (Stack.schemeStackMap.{u, w} B S hS (affineSpaceChartHom B S hS V n) ≫ a) f).fst

AlgebraicGeometry.Stack.AlgebraicStacks.exists_chart_forall_isClosed_baseChange_affineSpaceChart_of_isClosed_affine_lfp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedSmoothLocal.lean, line 659. The attribute's comment: “(2) implies (3)”.

Stacks 0H2A, (2) implies (3). Suppose every base change of f to an affine scheme of the site along a 1-morphism locally of finite presentation is closed. Then the conclusion of (3) holds for any smooth surjective chart a : Stack.schemeStack V ⟶ 𝒴 of 𝒴 by a scheme of the site.

Fix n. The target of the base change is the stack of affine n-space over V; its affine opens cover it and their inclusions are open immersions, hence smooth, so closedness can be read on that cover. Over one affine open W the base change of f is the base change along the composite W ⟶ 𝐀^n_V ⟶ V ⟶ 𝒴, whose scheme W is affine and which is locally of finite presentation — the inclusion of an open is, the projection of affine n-space is, and a is smooth hence locally of finite presentation by Stacks 0DNP. So (2) applies to it.

theorem exists_chart_forall_isClosed_baseChange_affineSpaceChart_of_isClosed_affine_lfp
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (h : ∀ (Z : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
      ∀ (g : Stack.schemeStack.{u, w} B S hS Z ⟶ 𝒴),
        IsLocallyOfFinitePresentation B S hS g →
          IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS g f).fst) :
    ∃ (V : BigFppfOver B S hS) (a : Stack.schemeStack.{u, w} B S hS V ⟶ 𝒴),
      Stack.IsSurjective B S hS a ∧ IsSmooth B S hS a ∧
        ∀ n : ℕ, IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS
          (Stack.schemeStackMap.{u, w} B S hS (affineSpaceChartHom B S hS V n) ≫ a) f).fst

AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_baseChange_schemeStackMap_of_forall_isClosed_baseChange_affineSpaceChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedSmoothLocal.lean, line 759. The attribute's comment: “(3) implies (2), the step at a target represented by a scheme, stated at the hypotheses of Tag 04II: a quasi-affine source and a morphism locally of finite type”.

Stacks 0H2A, the step of (3) implies (2) at a target represented by a scheme. Let f : 𝒳 ⟶ Stack.schemeStack W be a 1-morphism of algebraic stacks over S whose base change to affine n-space over W is closed on points for every n ≥ 0. Then for every morphism p : Z ⟶ W of the site whose source scheme is quasi-affine and which is locally of finite type, the base change of f along the 1-morphism that p induces is closed on points.

By Stacks 04II such a Z immerses over W into affine n-space over W for some n. That immersion of schemes induces an immersion of the represented algebraic stacks, and closedness of a base change descends along an immersion of the base.

theorem isClosed_baseChange_schemeStackMap_of_forall_isClosed_baseChange_affineSpaceChart
    {𝒳 : Stack.AlgebraicStacks.{u, w} B S hS} {W : BigFppfOver B S hS}
    (f : 𝒳 ⟶ Stack.schemeStack.{u, w} B S hS W)
    (h : ∀ n : ℕ, IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS
      (Stack.schemeStackMap.{u, w} B S hS (affineSpaceChartHom B S hS W n)) f).fst)
    {Z : BigFppfOver B S hS} (p : Z ⟶ W)
    (hZ : ((BigFppfOver.toScheme B S hS).obj Z).IsQuasiAffine)
    (hp : LocallyOfFiniteType ((BigFppfOver.toScheme B S hS).map p)) :
    IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS
      (Stack.schemeStackMap.{u, w} B S hS p) f).fst

AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_baseChange_affine_isLocallyOfFinitePresentation_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedSmoothLocal.lean, line 803. The attribute's comment: “clause (2) is inherited by a base change along a 1-morphism locally of finite presentation”.

Clause (2) of Stacks 0H2A is inherited by a base change along a 1-morphism locally of finite presentation. Suppose every base change of f : 𝒳 ⟶ 𝒴 to an affine scheme of the site along a 1-morphism locally of finite presentation is closed on points, and let b : 𝒴' ⟶ 𝒴 be locally of finite presentation. Then the same holds for the base change of f along b: a 1-morphism Stack.schemeStack Z ⟶ 𝒴' locally of finite presentation composes with b to one locally of finite presentation, and base changing twice is base changing once.

theorem isClosed_baseChange_affine_isLocallyOfFinitePresentation_baseChange
    {𝒳 𝒴 𝒴' : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (b : 𝒴' ⟶ 𝒴)
    (hb : IsLocallyOfFinitePresentation B S hS b)
    (h : ∀ (Z : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
      ∀ (g : Stack.schemeStack.{u, w} B S hS Z ⟶ 𝒴), IsLocallyOfFinitePresentation B S hS g →
        IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS g f).fst)
    (Z : BigFppfOver B S hS) (hZ : IsAffine ((BigFppfOver.toScheme B S hS).obj Z))
    (g : Stack.schemeStack.{u, w} B S hS Z ⟶ 𝒴') (hg : IsLocallyOfFinitePresentation B S hS g) :
    IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS g
      (Stack.twoFibreProductSquareAlgebraicStacks B S hS b f).fst).fst

AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_of_forall_schemeStack_target_of_isClosed_affine_lfp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedSmoothLocal.lean, line 825. The attribute's comment: “(2) implies (1), the reduction to a target represented by a scheme; the remaining input is Tag 0H29 for algebraic stacks, carried as hred”.

Stacks 0H2A, the reduction of (2) implies (1) to a target represented by a scheme. If clause (2) implies universal closedness whenever the target is the algebraic stack of a scheme of the site, then it implies universal closedness for an arbitrary target.

Every algebraic stack over S has a smooth surjective chart by a scheme of the site, universal closedness descends along it, and it is locally of finite presentation by Stacks 0DNP, so clause (2) for f gives clause (2) for the base change of f to that chart.

theorem universallyClosed_of_forall_schemeStack_target_of_isClosed_affine_lfp
    (hred : ∀ (V : BigFppfOver B S hS) (𝒲 : Stack.AlgebraicStacks.{u, w} B S hS)
      (f' : 𝒲 ⟶ Stack.schemeStack.{u, w} B S hS V),
        (∀ (Z : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
          ∀ (g : Stack.schemeStack.{u, w} B S hS Z ⟶ Stack.schemeStack.{u, w} B S hS V),
            IsLocallyOfFinitePresentation B S hS g →
              IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS g f').fst) →
        UniversallyClosed B S hS f')
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (h : ∀ (Z : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
      ∀ (g : Stack.schemeStack.{u, w} B S hS Z ⟶ 𝒴), IsLocallyOfFinitePresentation B S hS g →
        IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS g f).fst) :
    UniversallyClosed B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_of_isQuasiCompactMorphism_of_isClosed_affine_lfp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedSmoothLocalQuasiCompact.lean, line 389. The attribute's comment: “(2) implies (1), with the reduction to a target represented by a scheme”.

Stacks 0H2A, (2) implies (1), with the reduction to a target represented by a scheme. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact 1-morphism of algebraic stacks over S such that the base change of f to every affine scheme of the site along a 1-morphism locally of finite presentation is closed on points. Then f is universally closed.

Pick a smooth surjective chart a : Stack.schemeStack V ⟶ 𝒴 of 𝒴 by a scheme of the site. Universal closedness descends along a, so it is enough to prove it for the base change of f along a, whose target is represented by a scheme of the site; that base change is quasi-compact by Stacks 050V, and it inherits the hypothesis because a is locally of finite presentation by Stacks 0DNP and clause (2) is inherited by a base change along a 1-morphism locally of finite presentation.

theorem universallyClosed_of_isQuasiCompactMorphism_of_isClosed_affine_lfp
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : Stack.IsQuasiCompactMorphism.{u, w} B S hS f)
    (h : ∀ Z : BigFppfOver B S hS, IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
      ∀ g : Stack.schemeStack.{u, w} B S hS Z ⟶ 𝒴, IsLocallyOfFinitePresentation B S hS g →
        IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS g f).fst) :
    UniversallyClosed B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_of_exists_chart_forall_isClosed_baseChange_affineSpaceChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedSmoothLocalQuasiCompact.lean, line 419. The attribute's comment: “(3) implies (1)”.

Stacks 0H2A, (3) implies (1). Suppose there are a scheme V of the site and a smooth surjective 1-morphism a : Stack.schemeStack V ⟶ 𝒴 such that the base change of the quasi-compact f to affine n-space over V is closed on points for every n ≥ 0. Then f is universally closed.

Universal closedness descends along a, so it is enough to prove it for the base change f' of f along a, whose target is represented by a scheme of the site. By (2) implies (1) at such a target it is enough to show that the base change of f' to every affine scheme of the site along a morphism of the site locally of finite presentation is closed on points; an affine scheme is quasi-affine and a morphism locally of finite presentation is locally of finite type, so this is the step of (3) implies (2) at a target represented by a scheme, which goes through the immersion into affine n-space of Stacks 04II.

theorem universallyClosed_of_exists_chart_forall_isClosed_baseChange_affineSpaceChart
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : Stack.IsQuasiCompactMorphism.{u, w} B S hS f)
    (h : ∃ (V : BigFppfOver B S hS) (a : Stack.schemeStack.{u, w} B S hS V ⟶ 𝒴),
      Stack.IsSurjective B S hS a ∧ IsSmooth B S hS a ∧
        ∀ n : ℕ, IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS
          (Stack.schemeStackMap.{u, w} B S hS (affineSpaceChartHom B S hS V n) ≫ a) f).fst) :
    UniversallyClosed B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_tfae_of_isQuasiCompactMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedSmoothLocalQuasiCompact.lean, line 453.

Stacks 0H2A. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact 1-morphism of algebraic stacks over S. The following are equivalent:

1. f is universally closed;
2. for every object Z of the site whose underlying scheme is affine and every 1-morphism Stack.schemeStack Z ⟶ 𝒴 locally of finite presentation, the map |𝒳 ×_𝒴 Z| → |Z| is closed;
3. there are an object V of the site and a smooth surjective 1-morphism a : Stack.schemeStack V ⟶ 𝒴 such that |𝐀^n × (𝒳 ×_𝒴 V)| → |𝐀^n × V| is closed for every n ≥ 0.

Clause (3) is read as closedness of the base change of f along the composite 𝐀^n_V ⟶ V ⟶ 𝒴, which is what |𝐀^n × (𝒳 ×_𝒴 V)| → |𝐀^n × V| is over V.

theorem universallyClosed_tfae_of_isQuasiCompactMorphism
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : Stack.IsQuasiCompactMorphism.{u, w} B S hS f) :
    List.TFAE
      [UniversallyClosed B S hS f,
        ∀ Z : BigFppfOver B S hS, IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
          ∀ g : Stack.schemeStack.{u, w} B S hS Z ⟶ 𝒴, IsLocallyOfFinitePresentation B S hS g →
            IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS g f).fst,
        ∃ (V : BigFppfOver B S hS) (a : Stack.schemeStack.{u, w} B S hS V ⟶ 𝒴),
          Stack.IsSurjective B S hS a ∧ IsSmooth B S hS a ∧
            ∀ n : ℕ, IsClosed B S hS
              (Stack.twoFibreProductSquareAlgebraicStacks B S hS
                (Stack.schemeStackMap.{u, w} B S hS (affineSpaceChartHom B S hS V n) ≫ a)
                f).fst]

Sources

• Section 102.7, Tag 0H28
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.exists_affine_locallyFinitePresentation_separation_isClosed · AlgebraicGeometry.Stack.exists_affine_finitePresentation_separation · AlgebraicGeometry.Stack.AlgebraicStacks.image_preimage_eq_preimage_image_of_isTwoFibreProduct · AlgebraicGeometry.Stack.AlgebraicStacks.image_closure_image_subset_of_isTwoFibreProduct · IsOpenMap.image_closure_subset_image_of_preimage_subset · AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_baseChange_of_isImmersion · AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_baseChange_affine_isLocallyOfFinitePresentation_of_universallyClosed · AlgebraicGeometry.Stack.AlgebraicStacks.exists_chart_forall_isClosed_baseChange_affineSpaceChart_of_universallyClosed

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.