70.3 Morphisms of finite… to 70.14 Sections with support in…

Section70.3 Morphisms of finite presentation#

Section 70.3 of the Stacks Project, Tag 049I. 13 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 049J, a definition

Tag 049J in the Stacks Project.

AlgebraicGeometry.LimitPreserving, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/LimitPreserving.lean, line 49. The attribute's comment: “part (1)”. References: SGA 3 XI (3.2), “definition of (*)”.

Stacks Project, Tag 049J. A presheaf of sets preserves inverse limits of affine schemes as filtered colimits of sets, relative to its underlying-scheme functor.

abbrev LimitPreserving {C : Type z} [Category C]
    (toScheme : C ⥤ Scheme.{u}) (F : Cᵒᵖ ⥤ Type v) : Prop

AlgebraicGeometry.RelativelyLimitPreserving, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/LimitPreserving.lean, line 78. The attribute's comment: “part (2)”.

Stacks Project, Tag 049J. A transformation is relatively limit preserving when the presheaf of lifts of every target section is limit preserving over that section's base.

abbrev RelativelyLimitPreserving
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v}
    (a : F ⟶ G) : Prop
Tag 049K, an equation

Tag 049K in the Stacks Project.

AlgebraicGeometry.isPullback_sectionFiberι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/SectionFiber.lean, line 121.

Stacks Project, Tag 049K. The presheaf of lifts of a section y of G over X through a transformation a : F ⟶ G of presheaves of sets on the big fppf site over S is the fibre product

  F_y = F|_{(Sch/X)_fppf} ×_{G|_{(Sch/X)_fppf}} *

of presheaves on the big fppf site over X, where * is the final presheaf and the morphism * ⟶ G|_{(Sch/X)_fppf} is the point named by y. That is, the inclusion of the fibre into the restriction of F along the localization functor and its structural morphism to the final presheaf exhibit it as the fibre product of the restriction of a and of that point.

theorem isPullback_sectionFiberι :
    IsPullback (sectionFiberι B S hS a X y) (sectionFiberToFinal B S hS a X y)
      (Functor.whiskerLeft (Over.forget X).op a) (pointOfSection B S hS G X y)
Tag 06BC, a lemma

Tag 06BC in the Stacks Project.

AlgebraicGeometry.relativelyLimitPreserving_iff_affineLimit_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/AffineCriterion.lean, line 563.

The affine-limit comparison square characterizes relative limit preservation of a transformation of presheaves.

public theorem relativelyLimitPreserving_iff_affineLimit_isPullback
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v}
    (a : F ⟶ G) :
    RelativelyLimitPreserving.{u, v, max w w', w'} B S hS a ↔
      ∀ (I : Type (max w w')) [Category.{w'} I] [IsCofiltered I]
        (D : I ⥤ BigFppfOver B S hS) (c : Cone D),
        IsLimit ((BigFppfOver.toScheme B S hS).mapCone c) →
        (∀ i, IsAffine ((BigFppfOver.toScheme B S hS).obj (D.obj i))) →
        IsAffine ((BigFppfOver.toScheme B S hS).obj c.pt) →
          let U := CategoryTheory.uliftFunctor.{max w w', v}
          let F' := F ⋙ U
          let G' := G ⋙ U
          IsPullback
            (colimit.desc (D.op ⋙ F') (F'.mapCocone c.op))
            (colimMap (Functor.whiskerLeft D.op (Functor.whiskerRight a U)))
            (U.map (a.app (Opposite.op c.pt)))
            (colimit.desc (D.op ⋙ G') (G'.mapCocone c.op))
Tag 049L, a lemma

Tag 049L in the Stacks Project.

AlgebraicGeometry.relativelyLimitPreserving_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/Sorites.lean, line 45.

The composition of two relatively limit-preserving transformations is relatively limit preserving.

public theorem relativelyLimitPreserving_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v}
    (a : F ⟶ G) (b : G ⟶ H)
    (ha : RelativelyLimitPreserving.{u, v, max w w', w'} B S hS a)
    (hb : RelativelyLimitPreserving.{u, v, max w w', w'} B S hS b) :
    RelativelyLimitPreserving.{u, v, max w w', w'} B S hS (a ≫ b)
Tag 0GDY, a lemma

Tag 0GDY in the Stacks Project.

AlgebraicGeometry.relativelyLimitPreserving_of_comp_of_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/Sorites.lean, line 74.

If b and a ≫ b preserve limits relatively, then so does a.

public theorem relativelyLimitPreserving_of_comp_of_right
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v}
    (a : F ⟶ G) (b : G ⟶ H)
    (hba : RelativelyLimitPreserving.{u, v, w, w'} B S hS (a ≫ b))
    (hb : RelativelyLimitPreserving.{u, v, w, w'} B S hS b) :
    RelativelyLimitPreserving.{u, v, w, w'} B S hS a
Tag 049M, a lemma

Tag 049M in the Stacks Project.

AlgebraicGeometry.relativelyLimitPreserving_pullback_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/FibreProducts.lean, line 169.

A relatively limit-preserving transformation of presheaves remains so after pullback along any transformation.

public theorem relativelyLimitPreserving_pullback_fst
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v}
    (a : F ⟶ G) (b : H ⟶ G)
    (ha : RelativelyLimitPreserving.{u, v, w, w'} B S hS a) :
    RelativelyLimitPreserving.{u, v, w, w'} B S hS
      (pullback.fst b a)
Tag 0GDZ, a lemma

Tag 0GDZ in the Stacks Project.

AlgebraicGeometry.relativelyLimitPreserving_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/FibreProducts.lean, line 364.

Relative limit preservation is stable under a fibre product of presheaves over a common intermediate presheaf.

public theorem relativelyLimitPreserving_pullback
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {E F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v}
    (a : F ⟶ G) (b : H ⟶ G) (c : G ⟶ E)
    (hc : RelativelyLimitPreserving.{u, v, w, w'} B S hS c)
    (hca : RelativelyLimitPreserving.{u, v, w, w'} B S hS (a ≫ c))
    (hcb : RelativelyLimitPreserving.{u, v, w, w'} B S hS (b ≫ c)) :
    RelativelyLimitPreserving.{u, v, w, w'} B S hS
      (pullback.fst a b ≫ a ≫ c)
Tag 049O, a lemma

Tag 049O in the Stacks Project.

AlgebraicGeometry.limitPreserving_of_isLocallyBijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/Sheafify.lean, line 988. The attribute's comment: “locally bijective comparison”.

An fppf sheaf receiving a locally bijective map from a limit-preserving presheaf is limit preserving. Local injectivity makes sections that agree at the limit agree at a later stage, and local surjectivity puts every section of the sheaf at a finite stage.

public theorem limitPreserving_of_isLocallyBijective [UnivLE.{max w w', u}]
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v} (η : F ⟶ G)
    [Presheaf.IsLocallySurjective (BigFppfOver.topology B S hS) η]
    [Presheaf.IsLocallyInjective (BigFppfOver.topology B S hS) η]
    (hG : Presheaf.IsSheaf (BigFppfOver.topology B S hS) G)
    (hF : LimitPreserving.{u, v, w, w', u + 1} (BigFppfOver.toScheme B S hS) F) :
    LimitPreserving.{u, v, w, w', u + 1} (BigFppfOver.toScheme B S hS) G

AlgebraicGeometry.limitPreserving_sheafify, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/Sheafify.lean, line 1012.

Fppf sheafification of a limit-preserving presheaf is limit preserving.

public theorem limitPreserving_sheafify [UnivLE.{max w w', u}]
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max (u + 1) v))
    (hF : LimitPreserving.{u, max (u + 1) v, w, w', u + 1}
      (BigFppfOver.toScheme B S hS) F) :
    LimitPreserving.{u, max (u + 1) v, w, w', u + 1}
      (BigFppfOver.toScheme B S hS)
      ((BigFppfOver.topology B S hS).sheafify F)
Tag 049P, a lemma

Tag 049P in the Stacks Project.

AlgebraicGeometry.limitPreserving_of_fppfCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/FppfLocal.lean, line 532.

Limit preservation for an fppf sheaf can be checked on an fppf cover of the base scheme.

public theorem limitPreserving_of_fppfCover
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v)
    (hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
    (E : PreZeroHypercover.{u + 1} (B.obj hS))
    (hE : IsFppfCovering ⟨B.obj hS, E⟩)
    (hlocal : ∀ i : E.I₀,
      LimitPreserving.{u, v, w, w', u + 1}
        (Over.forget (E.X i) ⋙ B.inclusion)
        ((Over.map (E.f i)).op ⋙ F)) :
    LimitPreserving.{u, v, w, w', u + 1}
      (BigFppfOver.toScheme B S hS) F
Tag 049Q, a lemma

Tag 049Q in the Stacks Project.

AlgebraicGeometry.relativelyLimitPreserving_sheafifyMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/SheafifyRelative.lean, line 538.

Sheafification preserves relative limit preservation of a transformation of presheaves on the big fppf site.

public theorem relativelyLimitPreserving_sheafifyMap [UnivLE.{max w w', u}]
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max (u + 1) v)}
    (a : F ⟶ G)
    (ha : RelativelyLimitPreserving.{u, max (u + 1) v, w, w'}
      B S hS a) :
    RelativelyLimitPreserving.{u, max (u + 1) v, w, w'} B S hS
      (sheafifyMap (BigFppfOver.topology B S hS) a)
Tag 04AK, a proposition

Tag 04AK in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_iff_relativelyLimitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/LimitPreservingIff.lean, line 191.

Stacks 04AK. A morphism of algebraic spaces over a scheme S is locally of finite presentation if and only if it is relatively limit preserving as a transformation of functors on the big fppf site of S.

Both conditions are read at index categories in the universe of the schemes.

theorem isLocallyOfFinitePresentation_iff_relativelyLimitPreserving
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsLocallyOfFinitePresentation B S hS f ↔
      RelativelyLimitPreserving.{u, u, u, u} B S hS f

AlgebraicGeometry.relativelyLimitPreserving_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/LimitPreservingOfFinitePresentation.lean, line 226. The attribute's comment: “locally of finite presentation implies relatively limit preserving”.

A morphism of algebraic spaces over S which is locally of finite presentation is relatively limit preserving, for index categories in the universe of the schemes.

theorem relativelyLimitPreserving_of_isLocallyOfFinitePresentation
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    {a : F ⟶ G} (ha : Space.IsLocallyOfFinitePresentation B S hS a) :
    RelativelyLimitPreserving.{u, u, u, u} B S hS a

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_relativelyLimitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/Representable.lean, line 357. The attribute's comment: “the implication from relatively limit preserving to locally of finite presentation”.

Stacks 04AK, the implication from relative limit preservation towards local finite presentation. A relatively limit-preserving transformation of presheaves on the big fppf site of S is locally of finite presentation as a morphism of algebraic spaces.

This is AlgebraicGeometry.isLocallyOfFinitePresentation_of_relativelyLimitPreserving with its scheme-level input discharged by AlgebraicGeometry.locallyOfFinitePresentation_of_relativelyLimitPreserving_yoneda_map — the implication (2) ⇒ (1) of Stacks 01ZC for a morphism of the site.

theorem Space.isLocallyOfFinitePresentation_of_relativelyLimitPreserving
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : X ⟶ Y}
    (hf : RelativelyLimitPreserving.{u, u, u, u} B S hS f) :
    Space.IsLocallyOfFinitePresentation B S hS f
Tag 05N0, a remark

Tag 05N0 in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_terminal_iff_limitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/LimitPreservingFunctorOfPoints.lean, line 291.

Stacks 05N0. An algebraic space X over a scheme S is locally of finite presentation over S if and only if X, read as a functor on the big fppf site of S, is limit preserving.

This is the case of Stacks 04AK in which the target is the terminal presheaf, so that the morphism is the structure morphism of X to S. Only the implication (1) ⇒ (2) of Stacks 04AK is used; the converse is obtained from Stacks 0CM6 instead, so no undischarged hypothesis enters. Compare Stacks 05LX, AlgebraicGeometry.Scheme.locallyOfFinitePresentation_iff_isLimitPreserving_yoneda, which is this statement for a scheme.

theorem isLocallyOfFinitePresentation_terminal_iff_limitPreserving
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X) :
    IsLocallyOfFinitePresentation B S hS (terminal.from X) ↔
      LimitPreserving.{u, u, u, u, u + 1, u} (BigFppfOver.toScheme B S hS) X
Tag 0CM6, a lemma

Tag 0CM6 in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_affineLimit_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/SurjectiveCriterion.lean, line 346.

Stacks 0CM6. A morphism of algebraic spaces over S is locally of finite presentation as soon as, for every cofiltered inverse limit of affine objects of the site, the comparison map from the colimit of the sections of the source to the fibre product of the sections over the limit with the colimit of the sections of the target is surjective.

theorem isLocallyOfFinitePresentation_of_affineLimit_surjective
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hsurj : ∀ (I : Type u) [Category.{u} I] [IsCofiltered I]
      (D : I ⥤ BigFppfOver B S hS) (c : Cone D),
      IsLimit ((BigFppfOver.toScheme B S hS).mapCone c) →
      (∀ i, IsAffine ((BigFppfOver.toScheme B S hS).obj (D.obj i))) →
      IsAffine ((BigFppfOver.toScheme B S hS).obj c.pt) →
      ∀ (x : X.obj (Opposite.op c.pt)) (y : colimit (D.op ⋙ Y)),
        f.app (Opposite.op c.pt) x = colimit.desc (D.op ⋙ Y) (Y.mapCocone c.op) y →
        ∃ z : colimit (D.op ⋙ X),
          colimit.desc (D.op ⋙ X) (X.mapCocone c.op) z = x ∧
          colimMap (Functor.whiskerLeft D.op f) z = y) :
    IsLocallyOfFinitePresentation B S hS f
Sources
LeanAlgebraicGeometry.LimitPreserving · AlgebraicGeometry.RelativelyLimitPreserving · AlgebraicGeometry.isPullback_sectionFiberι · AlgebraicGeometry.relativelyLimitPreserving_iff_affineLimit_isPullback · AlgebraicGeometry.relativelyLimitPreserving_comp · AlgebraicGeometry.relativelyLimitPreserving_of_comp_of_right · AlgebraicGeometry.relativelyLimitPreserving_pullback_fst · AlgebraicGeometry.relativelyLimitPreserving_pullback

Section70.4 Limits of algebraic spaces#

Section 70.4 of the Stacks Project, Tag 07SE. 7 tags here are carried by 19 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07SE, the section

Tag 07SE in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_limit_of_isAffineHom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/AffineOverBase.lean, line 141. The attribute's comment: “the content the section is cited for: a cofiltered inverse limit of algebraic spaces affine over a base is an algebraic space; the section's own numbered results 07SF, 07SG, 07SH, 0CUH, 0CUI and 0CP4 are not proved here”.

Stacks 07SE. The inverse limit of a cofiltered inverse system of algebraic spaces over S, each affine over one fixed algebraic space T, is an algebraic space over S, provided the index category is small enough for the site.

Affineness of the transition morphisms, which is what Stacks 07SF asks for, is supplied by AlgebraicGeometry.Space.isAffineHom_map_of_isAffineHom_app.

theorem isAlgebraicSpace_limit_of_isAffineHom_app (hSize : #I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i)) (hT : IsAlgebraicSpace B S hS T)
    (hτ : ∀ i, IsAffineHom B S hS (τ.app i)) :
    IsAlgebraicSpace B S hS (limit D)

AlgebraicGeometry.Space.isAffineHom_limitπ_comp_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/AffineOverBase.lean, line 157. The attribute's comment: “the content the section is cited for: the structure morphism of a cofiltered inverse limit of algebraic spaces affine over a base is affine; the section's own numbered results 07SF, 07SG, 07SH, 0CUH, 0CUI and 0CP4 are not proved here”.

Stacks 07SE. The structure morphism of the inverse limit of a cofiltered inverse system of algebraic spaces each affine over one fixed algebraic space T is affine over T.

It factors as the projection to a stage, which is affine by Stacks 07SF, part (1), followed by the structure morphism of that stage.

theorem isAffineHom_limitπ_comp_app (hSize : #I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i)) (hT : IsAlgebraicSpace B S hS T)
    (hτ : ∀ i, IsAffineHom B S hS (τ.app i)) (i : I) :
    IsAffineHom B S hS (limit.π D i ≫ τ.app i)

AlgebraicGeometry.Space.exists_isAffine_representation_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/AffineOverBase.lean, line 187. The attribute's comment: “the content the section is cited for, combined with Limits, Section 01YV: a cofiltered inverse limit of algebraic spaces affine over an affine base is represented by an affine object of the site; the section's own numbered results 07SF, 07SG, 07SH, 0CUH, 0CUI and 0CP4 are not proved here”.

Stacks 07SE, over an affine base. The inverse limit of a cofiltered inverse system of algebraic spaces over S, each affine over one fixed affine object Z of the site, is represented by an affine object of the site, by an isomorphism carrying the structure morphism of the limit to a morphism of the site.

The structure morphism of the limit is affine, so its base change along the identity of yoneda Z is represented by an affine object of the site; a base change along an identity is an isomorphism.

theorem exists_isAffine_representation_limit (hSize : #I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hτ : ∀ i, IsAffineHom B S hS (τ.app i)) (i₀ : I) :
    ∃ (W : BigAffineFppf B S hS)
      (e : yoneda.obj ((BigAffineFppf.inclusion B S hS).obj W) ≅ limit D)
      (q : (BigAffineFppf.inclusion B S hS).obj W ⟶
        (BigAffineFppf.inclusion B S hS).obj Z),
      e.hom ≫ limit.π D i₀ ≫ τ.app i₀ = yoneda.map q
Tag 07SF, a lemma

Tag 07SF in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineLimitExistence.lean, line 599. The attribute's comment: “existence”.

Stacks 07SF, existence. The inverse limit of a cofiltered inverse system of algebraic spaces over S with affine transition morphisms is an algebraic space over S, provided the index category is small enough for the site: its object type and all of its morphism types have cardinality below the cofinality of the site's size cutoff.

The limit is a sheaf by AlgebraicGeometry.Space.isSheaf_limit, and the remaining two conditions of Stacks 025Y follow from Stacks 02WY applied to the projection to any one stage, which is relatively representable by AlgebraicGeometry.Space.relativelyRepresentable_limitπ.

theorem isAlgebraicSpace_limit (hSize : #I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f)) :
    IsAlgebraicSpace B S hS (limit D)

AlgebraicGeometry.Space.isAlgebraicSpace_limit_of_isSiteSmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineLimitExistence.lean, line 707. The attribute's comment: “existence”.

Stacks 07SF, existence. The inverse limit of a cofiltered inverse system of algebraic spaces over S with affine transition morphisms is an algebraic space over S, provided the system is small for the site: either its index category is small compared with the cofinality of the site's size cutoff, its object type and all of its morphism types, or its transition morphisms are monomorphisms. See AlgebraicGeometry.Space.IsSiteSmall.

The limit is a sheaf by AlgebraicGeometry.Space.isSheaf_limit, and the remaining two conditions of Stacks 025Y follow from Stacks 02WY applied to the projection to any one stage, which is relatively representable by AlgebraicGeometry.Space.relativelyRepresentable_limitπ_of_isSiteSmall.

theorem isAlgebraicSpace_limit_of_isSiteSmall (hb : IsSiteSmall B S hS D)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f)) :
    IsAlgebraicSpace B S hS (limit D)

AlgebraicGeometry.Space.isAlgebraicSpace_limit_of_limitInSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineLimitExistence.lean, line 729. The attribute's comment: “existence”.

Stacks 07SF, existence, under the chapter's standing convention. The inverse limit of a cofiltered inverse system of algebraic spaces over S with affine transition morphisms is an algebraic space over S.

This is the faithful statement of the tag. The source states no condition on the index: it assumes only the convention of Section 70.2 that every ring considered has its spectrum in the big fppf site, which for this proof says that each limit of a diagram of base changes, to a test object of the site, of the stages over one stage lies in the site. That is AlgebraicGeometry.BigFppfOver.LimitInSite of a lift of such a diagram through the Yoneda embedding. The proof is the one of AlgebraicGeometry.Space.isAlgebraicSpace_limit_of_isSiteSmall, which proves the same conclusion from the strictly stronger AlgebraicGeometry.Space.IsSiteSmall, with the appeal to smallness replaced by the convention at the stage, test object and point in hand.

theorem isAlgebraicSpace_limit_of_limitInSite
    (hconv : ∀ (i : I) (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ D.obj i)
      (W : Over i ⥤ BigFppfOver B S hS),
      (W ⋙ yoneda ≅ (Over.post (X := i) D ⋙ Over.pullback g) ⋙
        Over.forget (yoneda.obj Z)) → BigFppfOver.LimitInSite W)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f)) :
    IsAlgebraicSpace B S hS (limit D)

AlgebraicGeometry.Space.isLimitPullbackLimitOverPost, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ApproximationSteps.lean, line 483. The attribute's comment: “part (2)”.

For a cofiltered inverse system D of presheaves on the big fppf site of S, a stage i and a morphism g : T ⟶ D i, the base changes of the stages over i along g form an inverse system whose limit is the base change of limit D along g. The cone is the limit cone of D, restricted to the stages over i and base changed along g.

noncomputable def isLimitPullbackLimitOverPost (i : I)
    {T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : T ⟶ D.obj i) :
    IsLimit ((Over.forget T).mapCone
      ((Over.pullback g).mapCone ((limit.cone D).overPost i)))

AlgebraicGeometry.Space.isAffineHom_limitπ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ApproximationSteps.lean, line 548. The attribute's comment: “part (1)”.

Every projection from the inverse limit of a cofiltered inverse system of algebraic spaces with affine transition morphisms is affine, provided the index category is small enough for the site: its object type and all of its morphism types have cardinality below the cofinality of the site's size cutoff.

theorem isAffineHom_limitπ (hSize : #I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (i : I) : IsAffineHom B S hS (limit.π D i)

AlgebraicGeometry.Space.isAffineHom_limitπ_of_siteContainsBaseChangeLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ApproximationSteps.lean, line 1082. The attribute's comment: “part (1)”.

Every projection from the inverse limit of a cofiltered inverse system of algebraic spaces with affine transition morphisms is affine, provided the system satisfies AlgebraicGeometry.Space.SiteContainsBaseChangeLimits.

theorem isAffineHom_limitπ_of_siteContainsBaseChangeLimits
    (hconv : SiteContainsBaseChangeLimits B S hS D)
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (i : I) : IsAffineHom B S hS (limit.π D i)

AlgebraicGeometry.Space.isAffineHom_limitπ_of_isSiteSmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ApproximationSteps.lean, line 1095. The attribute's comment: “part (1)”. References: SGA 3 XI (4.3), “partial”.

Every projection from the inverse limit of a cofiltered inverse system of algebraic spaces with affine transition morphisms is affine, provided the system is small for the site in the sense of AlgebraicGeometry.Space.IsSiteSmall.

theorem isAffineHom_limitπ_of_isSiteSmall (hb : IsSiteSmall B S hS D)
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (i : I) : IsAffineHom B S hS (limit.π D i)

AlgebraicGeometry.Space.AffineChartSystem.limitBridge, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/AffineChartSystem.lean, line 338. The attribute's comment: “limit of the affine charts at a stage”.

The limit of a chart system. A chart system indexed by a slice of a sufficiently small index category has a limit in the big fppf site of S, whose underlying scheme is a limit of the underlying schemes of the charts and which represents the base change of limit.π D i₀ along f₀.

noncomputable def limitBridge [IsCofiltered I] (C : AffineChartSystem B S hS i₀ D U₀ f₀)
    (hSize : #I < B.cutoff.ord.cof) (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof) :
    LimitBridge C

AlgebraicGeometry.Space.AffineChartSystem.limitBridgeOfLimitInSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/AffineChartSystem.lean, line 629. The attribute's comment: “limit of the affine charts at a stage”.

The limit of a chart system whose limit of charts lies in the site. A chart system whose limit of charts lies in the site has a limit in the big fppf site of S, whose underlying scheme is a limit of the underlying schemes of the charts and which represents the base change of limit.π D i₀ along f₀.

noncomputable def limitBridgeOfLimitInSite [IsCofiltered I]
    (C : AffineChartSystem B S hS i₀ D U₀ f₀)
    (hL : BigFppfOver.LimitInSite C.siteDiagram) :
    LimitBridge C

AlgebraicGeometry.Space.AffineChartSystem.limitBridgeOfIsSiteSmall, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/AffineChartSystem.lean, line 660. The attribute's comment: “limit of the affine charts at a stage”.

The limit of a chart system of a system small for the site. A chart system of a system which is small for the site has a limit in the big fppf site of S, whose underlying scheme is a limit of the underlying schemes of the charts and which represents the base change of limit.π D i₀ along f₀.

noncomputable def limitBridgeOfIsSiteSmall [IsCofiltered I]
    (C : AffineChartSystem B S hS i₀ D U₀ f₀)
    (hb : Space.IsSiteSmall B S hS D) :
    LimitBridge C
Tag 07SG, an equation

Tag 07SG in the Stacks Project.

AlgebraicGeometry.Space.exists_quotient_presentation_of_affine_transition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/QuotientPresentation.lean, line 1354.

Let D be a cofiltered inverse system of algebraic spaces over S with affine transition morphisms and p₀ : U₀ ⟶ D i₀ a surjective étale atlas of one stage. Then there are a scheme U over S with f : U ⟶ U₀ and q : U ⟶ lim D making U = U₀ ×_{D i₀} lim D, and an étale equivalence relation R on U that is the kernel pair of q, such that the canonical map from U/R to the limit of the inverse system is an isomorphism of fppf sheaves.

The atlas U₀ is required to be one of the site's schemes (hU₀mem), as in Stacks 07SG, which chooses a scheme U₀ together with a surjective étale morphism U₀ → X₀; an atlas of an algebraic space is an object of the site by construction, cf. AlgebraicGeometry.IsAlgebraicSpace.exists_atlas.

public theorem exists_quotient_presentation_of_affine_transition
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ Sheaf (BigFppfOver.topology B S hS) (Type u))
    [HasLimit D] [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    (hD : ∀ i, AlgebraicGeometry.IsAlgebraicSpace B S hS (D.obj i).obj)
    (hAffine : ∀ {i j : I} (f : i ⟶ j),
      AlgebraicGeometry.Space.IsAffineHom B S hS (D.map f).hom)
    (i₀ : I) (U₀ : Over S) (hU₀mem : B.Contains U₀.left)
    (hU₀ : Presheaf.IsSheaf (BigFppfOver.topology B S hS)
      (Stacks.Groupoids.points (BigFppfOver.toOver B S hS) U₀))
    (p₀ : representedSheaf B S hS U₀ hU₀ ⟶ D.obj i₀)
    (hp₀ : Epi p₀)
    (hp₀Etale :
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (AlgebraicGeometry.BigFppfOver.toScheme B S hS))) p₀.hom)
    : ∃ (U : Over S)
        (hU : Presheaf.IsSheaf (BigFppfOver.topology B S hS)
          (Stacks.Groupoids.points (BigFppfOver.toOver B S hS) U))
        (R : Over S) (j : Stacks.Groupoids.PreRelation R U)
        (q : representedSheaf B S hS U hU ⟶ limit D)
        (f : U ⟶ U₀),
        IsPullback
          ((BigFppfOver.toOver B S hS).op.whiskerLeft (yoneda.map f))
          q.hom p₀.hom (limit.π D i₀).hom ∧
        ∃ (hq : Stacks.Groupoids.sourceMap (BigFppfOver.toOver B S hS) j ≫ q.hom =
            Stacks.Groupoids.targetMap (BigFppfOver.toOver B S hS) j ≫ q.hom),
          IsPullback
            (Stacks.Groupoids.sourceMap (BigFppfOver.toOver B S hS) j)
            (Stacks.Groupoids.targetMap (BigFppfOver.toOver B S hS) j)
            q.hom q.hom ∧
          Stacks.Groupoids.IsEtaleEquivalenceRelation j ∧
          IsIso (canonicalQuotientToLimit B S hS D j hU q hq)
Tag 07SH, a lemma

Tag 07SH in the Stacks Project.

AlgebraicGeometry.Space.isLimitPullbackLimitOverPost, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ApproximationSteps.lean, line 483. The attribute's comment: “base change of the limit is the limit of the base changes”.

For a cofiltered inverse system D of presheaves on the big fppf site of S, a stage i and a morphism g : T ⟶ D i, the base changes of the stages over i along g form an inverse system whose limit is the base change of limit D along g. The cone is the limit cone of D, restricted to the stages over i and base changed along g.

noncomputable def isLimitPullbackLimitOverPost (i : I)
    {T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : T ⟶ D.obj i) :
    IsLimit ((Over.forget T).mapCone
      ((Over.pullback g).mapCone ((limit.cone D).overPost i)))
Tag 0CUH, a lemma

Tag 0CUH in the Stacks Project.

AlgebraicGeometry.Space.isClosedImmersion_limitMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LimitClosedImmersion.lean, line 111.

A stagewise closed immersion between inverse systems of algebraic spaces with affine transition morphisms induces a closed immersion of their inverse limits.

theorem isClosedImmersion_limitMap
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    {X Y : I ⥤ (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (η : X ⟶ Y)
    (hX : ∀ i, IsAlgebraicSpace B S hS (X.obj i))
    (hY : ∀ i, IsAlgebraicSpace B S hS (Y.obj i))
    (hXAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (X.map f))
    (hYAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (Y.map f))
    (hClosed : ∀ i, IsClosedImmersion B S hS (η.app i)) :
    IsClosedImmersion B S hS (limMap η)
Tag 0CUI, a lemma

Tag 0CUI in the Stacks Project.

AlgebraicGeometry.Space.isReduced_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/Reduced.lean, line 495.

A cofiltered inverse limit of reduced algebraic spaces with affine transition morphisms is reduced.

public theorem Space.isReduced_limit
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hSize : Cardinal.mk I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, Cardinal.mk (i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, AlgebraicGeometry.IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j),
      AlgebraicGeometry.Space.IsAffineHom B S hS (D.map f))
    (hReduced : ∀ i, AlgebraicGeometry.Space.HasEtaleLocalProperty B S hS (D.obj i)
      (fun X : Scheme.{u} => IsReduced X)) :
    AlgebraicGeometry.Space.HasEtaleLocalProperty B S hS (limit D)
      (fun X : Scheme.{u} => IsReduced X)
Tag 0CP4, a lemma

Tag 0CP4 in the Stacks Project.

AlgebraicGeometry.Space.affineLimitSquare_iff_qcqsLimitSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/QcqsCriterion.lean, line 1116.

Stacks 0CP4. For a morphism of algebraic spaces over S, the affine-limit comparison square is cartesian for every sufficiently small cofiltered inverse system of affine objects exactly when the comparison square of morphism sets is cartesian for every sufficiently small cofiltered inverse system of quasi-compact and quasi-separated algebraic spaces with affine transition morphisms.

theorem affineLimitSquare_iff_qcqsLimitSquare (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    AffineLimitSquare B S hS f ↔ QcqsLimitSquare B S hS hZ f

AlgebraicGeometry.Space.qcqsLimitSquare_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation/QcqsCriterion.lean, line 1141. The attribute's comment: “the implication from locally of finite presentation”.

Stacks 0CP4. A morphism of algebraic spaces over S which is locally of finite presentation satisfies the comparison condition for cofiltered limits of quasi-compact and quasi-separated algebraic spaces with affine transition morphisms.

theorem qcqsLimitSquare_of_isLocallyOfFinitePresentation (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFinitePresentation B S hS f) :
    QcqsLimitSquare B S hS hZ f
Sources
LeanAlgebraicGeometry.Space.isAlgebraicSpace_limit_of_isAffineHom_app · AlgebraicGeometry.Space.isAffineHom_limitπ_comp_app · AlgebraicGeometry.Space.exists_isAffine_representation_limit · AlgebraicGeometry.Space.isAlgebraicSpace_limit · AlgebraicGeometry.Space.isAlgebraicSpace_limit_of_isSiteSmall · AlgebraicGeometry.Space.isAlgebraicSpace_limit_of_limitInSite · AlgebraicGeometry.Space.isLimitPullbackLimitOverPost · AlgebraicGeometry.Space.isAffineHom_limitπ

Section70.5 Descending properties#

Section 70.5 of the Stacks Project, Tag 0826. 17 tags here are carried by 30 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CUJ, a lemma

Tag 0CUJ in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_point_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/Points.lean, line 292.

Stacks 0CUJ. Let D be a directed inverse system of decent algebraic spaces over S with affine transition morphisms, indexed by a category whose object type and whose morphism types are smaller than the cofinality of the site's size cutoff. Then a family of points of the stages which is compatible with the transition morphisms is induced by exactly one point of limit D; that is, |lim D| = lim |D| as sets.

theorem existsUnique_point_limit (D : I ⥤ (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hSize : #I < B.cutoff.ord.cof)
    (_hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (_hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (hDecent : ∀ i, IsDecentSpace B S hS (D.obj i))
    (x : ∀ i, points B S hS (D.obj i))
    (hx : ∀ {i j : I} (f : i ⟶ j), pointsMap B S hS (D.obj i) (D.map f) (x i) = x j) :
    ∃! y : points B S hS (limit D),
      ∀ i, pointsMap B S hS (limit D) (limit.π D i) y = x i
Tag 086V, a lemma

Tag 086V in the Stacks Project.

AlgebraicGeometry.Space.isHomeomorph_pointsLimitComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/PointsLimitHomeomorph.lean, line 78.

Stacks 086V. Let D be a directed inverse system of decent algebraic spaces over S with affine transition morphisms, indexed by a category small enough for the site, so that limit D is an algebraic space by Stacks 07SF. Then |limit D| = lim |D i| as topological spaces: the canonical map AlgebraicGeometry.Space.pointsLimitComparison from the points of the limit to the inverse limit of the point spaces of the stages is a homeomorphism.

It is bijective by Stacks 0CUJ, AlgebraicGeometry.Space.existsUnique_point_limit, which is where decency is used, and it is inducing because the point topology of the limit is the inverse-limit topology, AlgebraicGeometry.Space.pointTopology_limit.

theorem isHomeomorph_pointsLimitComparison (hSize : #I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (hDecent : ∀ i, IsDecentSpace B S hS (D.obj i)) :
    IsHomeomorph (pointsLimitComparison B S hS D)

AlgebraicGeometry.Space.pointTopology_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/PointTopology.lean, line 223.

The point topology of the limit of a cofiltered inverse system of algebraic spaces over S with affine transition morphisms, indexed by a small enough category, is the infimum of the topologies induced by the limit projections on points.

theorem pointTopology_limit (hSize : #I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f)) :
    pointTopology B S hS (limit D) =
      ⨅ i : I, TopologicalSpace.induced (pointsMap B S hS (limit D) (limit.π D i))
        (pointTopology B S hS (D.obj i))

AlgebraicGeometry.Space.pointTopology_limit_of_isSiteSmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/PointTopology.lean, line 375.

The point topology of the limit of a cofiltered inverse system of algebraic spaces over S with affine transition morphisms, indexed by a site-small category, is the infimum of the topologies induced by the limit projections on points.

theorem pointTopology_limit_of_isSiteSmall (hb : IsSiteSmall B S hS D)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f)) :
    pointTopology B S hS (limit D) =
      ⨅ i : I, TopologicalSpace.induced (pointsMap B S hS (limit D) (limit.π D i))
        (pointTopology B S hS (D.obj i))
Tag 086W, a lemma

Tag 086W in the Stacks Project.

AlgebraicGeometry.Space.nonempty_points_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/NonemptyLimit.lean, line 117.

Stacks 086W. The inverse limit of a cofiltered inverse system of nonempty quasi-compact algebraic spaces over S with affine transition morphisms has a point, provided the index category is small enough for the site: its object type and all of its morphism types have cardinality below the cofinality of the site's size cutoff.

theorem nonempty_points_limit (hSize : #I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (hCompact : ∀ i, IsQuasiCompactSpace B S hS (D.obj i))
    (hNonempty : ∀ i, Nonempty (points B S hS (D.obj i))) :
    Nonempty (points B S hS (limit D))
Tag 0CUK, a lemma

Tag 0CUK in the Stacks Project.

AlgebraicGeometry.Space.closure_singleton_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ClosureOfPoint.lean, line 150. The attribute's comment: “as sets”.

Stacks 0CUK, as sets. Let x be a point of the limit X of a cofiltered inverse system of algebraic spaces over S with affine transition morphisms, with images x i in the stages. The closure of x in |X| is the intersection of the preimages of the closures of the x i, that is, the inverse limit of those closures.

theorem closure_singleton_limit (hSize : #I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (x : points B S hS (limit D)) :
    closure {x} = ⋂ i : I, pointsMap B S hS (limit D) (limit.π D i) ⁻¹'
      closure {pointsMap B S hS (limit D) (limit.π D i) x}

AlgebraicGeometry.Space.existsUnique_point_closure_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ClosureOfPoint.lean, line 215. The attribute's comment: “as sets, for a compatible family of points”.

Stacks 0CUK, as sets. The set-level assertion read through the identification |X| = lim |D i| of Stacks 0CUJ, for a compatible family of points.

theorem existsUnique_point_closure_limit (hSize : #I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (hDecent : ∀ i, IsDecentSpace B S hS (D.obj i))
    (x : points B S hS (limit D)) (z : ∀ i, points B S hS (D.obj i))
    (hz : ∀ {i j : I} (f : i ⟶ j), pointsMap B S hS (D.obj i) (D.map f) (z i) = z j)
    (hzmem : ∀ i, z i ∈ closure {pointsMap B S hS (limit D) (limit.π D i) x}) :
    ∃! y : points B S hS (limit D), y ∈ closure {x} ∧
      ∀ i, pointsMap B S hS (limit D) (limit.π D i) y = z i

AlgebraicGeometry.Space.exists_iso_limit_reducedClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ClosureOfPoint.lean, line 429. The attribute's comment: “as algebraic spaces with the reduced induced structure”.

Stacks 0CUK, as algebraic spaces. Let x be a point of the limit X of a cofiltered inverse system of algebraic spaces over S with affine transition morphisms. The closure of x, with its reduced induced structure, is the limit of the closures of the images x i with theirs: those closures form an inverse system of algebraic spaces with affine transition morphisms, its limit is reduced, and the inclusion of the closure of x into X factors through an isomorphism onto that limit.

theorem exists_iso_limit_reducedClosure (hSize : #I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (x : points B S hS (limit D)) :
    ∃ (E : I ⥤ (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (η : E ⟶ D)
      (e : (reducedClosedSubspace B S hS (limit D)
          (isAlgebraicSpace_limit B S hS D hSize hHomSize hD hAffine)
          (closure {x}) isClosed_closure).toFunctor ≅ limit E),
      (∀ i : I, ∃ eᵢ : E.obj i ≅ (reducedClosedSubspace B S hS (D.obj i) (hD i)
            (closure {pointsMap B S hS (limit D) (limit.π D i) x}) isClosed_closure).toFunctor,
          eᵢ.hom ≫ (reducedClosedSubspace B S hS (D.obj i) (hD i)
            (closure {pointsMap B S hS (limit D) (limit.π D i) x}) isClosed_closure).ι
            = η.app i) ∧
        (∀ i, IsAlgebraicSpace B S hS (E.obj i)) ∧
        (∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (E.map f)) ∧
        HasEtaleLocalProperty B S hS (limit E) (fun Y : Scheme.{u} ↦ IsReduced Y) ∧
        e.hom ≫ limMap η = (reducedClosedSubspace B S hS (limit D)
          (isAlgebraicSpace_limit B S hS D hSize hHomSize hD hAffine)
          (closure {x}) isClosed_closure).ι
Tag 084R, a situation

Tag 084R in the Stacks Project.

AlgebraicGeometry.Space.LimitSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LimitSituation.lean, line 203.

Situation 084R. A limit situation for a presheaf X on the big fppf site of S: a directed index set with a chosen element, an inverse system of algebraic spaces over S indexed by it whose transition morphisms are affine and whose stages are quasi-compact and quasi-separated, and an identification of X with the limit of that system.

This is the algebraic-space analogue of AlgebraicGeometry.DescentSituation, which is Situation 086P for schemes, and the two have the same fields. By Stacks 07SF the limit of such a system is an algebraic space over S, so the situation is not vacuous for a reason it should not be: AlgebraicGeometry.Space.LimitSituation.const builds one for every quasi-compact quasi-separated algebraic space.

structure LimitSituation (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hZ : B.Contains (⊤_ Scheme.{u})) (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)

Declarations registered for the tag:

Tag 07SI, a lemma

Tag 07SI in the Stacks Project.

AlgebraicGeometry.Space.LimitSituation.isSectionsColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/QuasicoherentSectionsColimit.lean, line 65.

Let ℱ₀ be a quasi-coherent module on X₀, and set ℱᵢ = f_{0i}^*ℱ₀ and ℱ = f_0^*ℱ₀. Then Γ(X, ℱ) = colim_{i ≥ 0} Γ(Xᵢ, ℱᵢ), in the elementwise form AlgebraicGeometry.Space.LimitSituation.IsSectionsColimit, for an index set below the cofinality of the site's size cutoff.

theorem isSectionsColimit (hI : #A.I < B.cutoff.ord.cof)
    (F₀ : Modules.{u, u} B S hS (A.stage A.base).obj (A.stage A.base).property)
    (hF₀ : F₀.IsQuasicoherentOnSite) :
    A.IsSectionsColimit F₀ (A.isAlgebraicSpace_of_mk_lt hI)

AlgebraicGeometry.Space.LimitSituation.isSectionsColimit_of_baseChangeSizeBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/QuasicoherentSectionsColimitSizeBounded.lean, line 350. The attribute's comment: “Situation 084R on the bounded site, with the size conventions of Tag 07SD read as an index set below the cutoff with uniformly bounded base changes of the stages; with no size condition the statement is false, Refute07SI.not_forall_isSectionsColimit”.

Stacks 07SI. In Situation 084R, let ℱ₀ be a quasi-coherent module on X₀, and set ℱᵢ = f_{0i}^*ℱ₀ and ℱ = f_0^*ℱ₀. Then Γ(X, ℱ) = colim_{i ≥ 0} Γ(Xᵢ, ℱᵢ), in the elementwise form AlgebraicGeometry.Space.LimitSituation.IsSectionsColimit.

The size condition, an index set below the cutoff with uniformly bounded base changes, is how the bounded site reads the size conventions of the source (Tag 07SD); with no size condition the statement is false, by AlgebraicGeometry.Space.Refute07SI.not_forall_isSectionsColimit.

theorem isSectionsColimit_of_baseChangeSizeBounded (hI : #A.I < B.cutoff)
    (hB : BaseChangeSizeBounded B S hS A.system) (hF₀ : F₀.IsQuasicoherentOnSite) :
    A.IsSectionsColimit F₀ (A.isAlgebraicSpace_of_baseChangeSizeBounded hI hB)
Tag 0827, a lemma

Tag 0827 in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_isQuasiCompactSpace_preimage_eq_of_isSiteSmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendOpens.lean, line 327. References: EGA IV (8.2.11).

Stacks 0827. Notation and assumptions as in Situation 084R: let X = limit D be the limit of a cofiltered inverse system D of algebraic spaces over S with affine transition morphisms, the index category being small enough for the site so that X is an algebraic space by Stacks 07SF. Then for every quasi-compact open subspace U ⊆ X there is a stage i and a quasi-compact open subspace of D i whose inverse image in X is U.

Neither quasi-separatedness nor quasi-compactness of the stages, which Situation 084R also assumes, is needed.

theorem exists_isOpenSubspace_isQuasiCompactSpace_preimage_eq_of_isSiteSmall (hb : IsSiteSmall B S
    hS D)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (U : Subfunctor (limit D)) (hU : IsOpenSubspace B S hS U)
    (hUqc : IsQuasiCompactSpace B S hS U.toFunctor) :
    ∃ (i : I) (V : Subfunctor (D.obj i)), IsOpenSubspace B S hS V ∧
      IsQuasiCompactSpace B S hS V.toFunctor ∧ V.preimage (limit.π D i) = U

AlgebraicGeometry.Space.exists_isOpenSubspace_isQuasiCompactSpace_preimage_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendOpens.lean, line 348. References: EGA IV (8.2.11).

Stacks 0827. Notation and assumptions as in Situation 084R: let X = limit D be the limit of a cofiltered inverse system D of algebraic spaces over S with affine transition morphisms, the index category being small enough for the site so that X is an algebraic space by Stacks 07SF. Then for every quasi-compact open subspace U ⊆ X there is a stage i and a quasi-compact open subspace of D i whose inverse image in X is U.

Neither quasi-separatedness nor quasi-compactness of the stages, which Situation 084R also assumes, is needed.

theorem exists_isOpenSubspace_isQuasiCompactSpace_preimage_eq (hSize : #I < B.cutoff.ord.cof)
    (hHomSize : ∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (U : Subfunctor (limit D)) (hU : IsOpenSubspace B S hS U)
    (hUqc : IsQuasiCompactSpace B S hS U.toFunctor) :
    ∃ (i : I) (V : Subfunctor (D.obj i)), IsOpenSubspace B S hS V ∧
      IsQuasiCompactSpace B S hS V.toFunctor ∧ V.preimage (limit.π D i) = U
Tag 084S, a lemma

Tag 084S in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentSystem.exists_isIso_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/Isomorphism.lean, line 363. References: EGA IV (8.8.2.5), “f iso ⇒ f_i iso”.

Stacks 0852, and Stacks 084S. In the situation of Stacks 084W, if the base change f of f₀ to the limit B is an isomorphism and f₀ is locally of finite presentation, then the base change f_i of f₀ to some stage B_i is an isomorphism.

This is Stacks 0852. Stacks 084S draws the same conclusion in the limit situation of Stacks 084R, with the source and the target in addition assumed representable over the stage; hypothesis (a) of that tag is not needed here, since the three properties into which being an isomorphism is decomposed all descend without it.

theorem exists_isIso_mapAt (hf : IsIso D.mapLimit)
    (hfp : IsLocallyOfFinitePresentation B S hS D.map₀) :
    ∃ (i : I) (hi : D.initial ≤ i), IsIso (D.mapAt i hi)
Tag 084T, a lemma

Tag 084T in the Stacks Project.

AlgebraicGeometry.Space.DescentSituation.exists_isAbsolutelySeparated_system_obj_of_isSiteSmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/SeparatedDescent.lean, line 818.

Stacks 084T. In the situation of Stacks 084R, over an arbitrary base scheme, if the limit X of the inverse system is separated then some stage X_i is separated.

Separatedness is the absolute notion, taken over the terminal scheme, so the whole descent may be read there: the relocalization along S ⟶ Spec ℤ carries the descent situation over S to one over the terminal scheme, which is affine, and the absolute separatedness of a presheaf and of its view over the terminal scheme are the same condition.

theorem exists_isAbsolutelySeparated_system_obj_of_isSiteSmall {I : Type u} [Preorder I]
    [IsDirected I (· ≤ ·)] (D : DescentSituation B S hS hZ I)
    (hb : Space.IsSiteSmall B S hS D.system)
    (hX : IsAbsolutelySeparated B S hS hZ D.limitCone.pt) :
    ∃ i, D.base ≤ i ∧ IsAbsolutelySeparated B S hS hZ (D.system.obj (op i))

AlgebraicGeometry.Space.DescentSituation.exists_isAbsolutelySeparated_system_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/SeparatedDescent.lean, line 838.

Stacks 084T. In the situation of Stacks 084R, over an arbitrary base scheme, if the limit X of the inverse system is separated then some stage X_i is separated.

Separatedness is the absolute notion, taken over the terminal scheme, so the whole descent may be read there: the relocalization along S ⟶ Spec ℤ carries the descent situation over S to one over the terminal scheme, which is affine, and the absolute separatedness of a presheaf and of its view over the terminal scheme are the same condition.

theorem exists_isAbsolutelySeparated_system_obj {I : Type u} [Preorder I]
    [IsDirected I (· ≤ ·)] (D : DescentSituation B S hS hZ I) (hI : #I < B.cutoff.ord.cof)
    (hX : IsAbsolutelySeparated B S hS hZ D.limitCone.pt) :
    ∃ i, D.base ≤ i ∧ IsAbsolutelySeparated B S hS hZ (D.system.obj (op i))
Tag 07SQ, a lemma

Tag 07SQ in the Stacks Project.

AlgebraicGeometry.Space.DescentSituation.exists_isAffineSpace_system_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/AffineStage/ExistsAffineStage.lean, line 174. The attribute's comment: “Correction: the index set is taken smaller than the cofinality of the site's size cutoff, the form the convention of Section 70.2 takes in this size model; without it the statement is false here (a system of projective lines over fields of sizes cofinal in the cutoff has empty, hence affine, limit)”.

Stacks 07SQ. In the situation of Stacks 084R over a scheme S — a directed inverse system of quasi-compact and quasi-separated algebraic spaces over S with affine transition morphisms, with a chosen limit X and a chosen index 0 — if X is affine then so is some stage X_i with 0 ≤ i.

The index set may live in any universe; its cardinality is asked to be below the cofinality of the size cutoff of the site, which is how the standing convention of Section 70.2 of the source (every ring considered has its spectrum in the site) reads in this size model. Without it the statement fails here: for fields F_a (a below the cofinality) of sizes cofinal in the cutoff, the system P¹_{F_a} has no point over any object of the site, so its limit is the empty, affine, scheme while no stage is affine.

The index set is replaced by an order-isomorphic one in the universe of the site, AlgebraicGeometry.Space.DescentSituation.exists_orderIso_of_lift_mk_lt, along which the situation is reindexed, and the case of an index set in that universe is AlgebraicGeometry.Space.DescentSituation.exists_isAffineSpace_system_obj_of_mk_lt.

theorem DescentSituation.exists_isAffineSpace_system_obj {B : BigFppfSite.{u}} {S : Scheme.{u}}
    {hS : B.Contains S} {hZ : B.Contains (⊤_ Scheme.{u})} {I : Type v} [Preorder I]
    [IsDirected I (· ≤ ·)] (D : DescentSituation B S hS hZ I)
    (hI : Cardinal.lift.{u} #I < Cardinal.lift.{v} B.cutoff.ord.cof)
    (hX : IsAffineSpace B S hS D.limitCone.pt) :
    ∃ i, D.base ≤ i ∧ IsAffineSpace B S hS (D.system.obj (op i))

AlgebraicGeometry.Space.hasAffineStageDescent_of_chartsBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/AffineStageDescentChartsBounded.lean, line 161.

In the situation of Stacks 084R, if the limit X of the inverse system is an affine algebraic space then X_i is an affine algebraic space for some i beyond the distinguished index, the charts of the system being bounded in the sense of AlgebraicGeometry.Space.ChartsBounded.

The size restriction cannot be dropped: Stacks.Refute07SQ.not_statement07SQ exhibits a descent situation over an index as large as the cutoff whose limit is the empty algebraic space, which is affine, and none of whose stages is affine.

theorem hasAffineStageDescent_of_chartsBounded : HasAffineStageDescent B S hS hZ

AlgebraicGeometry.Space.DescentSituation.exists_isAffineSpace_system_obj_of_siteContainsBaseChangeLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/AffineStageSiteSmall.lean, line 716.

Stacks 07SQ. In the situation of Stacks 084R, over an arbitrary base scheme, if the limit X of the inverse system is an affine algebraic space then so is some stage X_i with i at or beyond the distinguished index.

The only hypothesis beyond Situation 084R is the chapter's standing convention of Section 70.2 (tag 07SD), that every ring considered has its spectrum in the big fppf site; for this system it is AlgebraicGeometry.Space.SiteContainsBaseChangeLimits: for every stage, every affine scheme-valued point of it and the base changes to that point of the later stages, the limit of those affine schemes — the spectrum of the colimit of their rings — lies in the site. Nothing is asked of the index. The convention is used three times: to make the limit of the affine charts of the system an object of the site (Stacks 07SF), to make the ring of global functions of the limit the filtered colimit of those of the stages (Stacks 07SI for the structure sheaf), and in Stacks 084S.

It cannot be dropped. Index the stages by the finite subsets of a field F of cardinality at least the cutoff of the site, the stage at a subset being the punctured affine plane over the subring of F it generates: a directed system of quasi-compact separated schemes with affine transition morphisms, none of them affine. A nonempty object of the site has too small a ring of functions to receive F, so the limit of the system in the site is empty, hence affine. See AlgebraicGeometry.Space.DescentSituation.not_forall_exists_isAffineSpace_system_obj; that the system violates the convention is AlgebraicGeometry.Space.SiteConventionCounterexample.not_siteContainsBaseChangeLimits.

Affineness of an algebraic space is the absolute notion, taken over the terminal scheme, so the whole descent is read there: the relocalization along S ⟶ Spec ℤ carries the descent situation over S to one over the terminal scheme, which is where the identification of an affine algebraic space with the spectrum of its global functions is available, and the convention survives that passage, AlgebraicGeometry.Space.DescentSituation.siteContainsBaseChangeLimits_viewOverIntegers.

theorem exists_isAffineSpace_system_obj_of_siteContainsBaseChangeLimits
    (hconv : SiteContainsBaseChangeLimits B S hS D.system)
    (hX : IsAffineSpace B S hS D.limitCone.pt) :
    ∃ i, D.base ≤ i ∧ IsAffineSpace B S hS (D.system.obj (op i))
Tag 084U, an equation

Tag 084U in the Stacks Project.

AlgebraicGeometry.Space.commSq_chart_specOfGlobalFunctions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpecGlobalFunctionsChartSquare.lean, line 274.

Let A be a u-model of the ring of global functions of an algebraic space X over S, let V be an étale scheme chart of X, let g₁, …, gₙ be polynomials in n variables over A and let h₁, …, hₙ be global functions on V with g_λ(h) = 0. Write C = A[x₁, …, xₙ]/(g₁, …, gₙ). Then the square whose top is the chart, whose left vertical is a canonical morphism p : X ⟶ Spec A, whose right vertical is the morphism V ⟶ Spec C attached to AlgebraicGeometry.Space.coordinateHom and whose bottom is the spectrum of A → C commutes.

The hypothesis hp is the chart formula of AlgebraicGeometry.Space.exists_specMap_of_globalHom, which determines p.

theorem commSq_chart_specOfGlobalFunctions (X : AlgebraicSpaces B S hS)
    (V : SmallEtale B S hS X.1) (A : Type u) [CommRing A]
    (e : A ≃+* globalFunctions B S hS X.1) {n : ℕ} (g : Fin n → MvPolynomial (Fin n) A)
    (h : Fin n → Γ((BigFppfOver.toScheme B S hS).obj V.1.left, ⊤))
    (hrel : ∀ l, MvPolynomial.eval₂
      ((globalFunctionsChartRestriction B S hS X V).comp e.toRingHom) h (g l) = 0)
    (p : X.1 ⟶ schemePoints B S hS (Spec (CommRingCat.of A)))
    (hp : yonedaEquiv (V.1.hom ≫ p) =
      specMapOfGlobalHom A ((globalFunctionsChartRestriction B S hS X V).comp e.toRingHom)) :
    V.1.hom ≫ p =
      yonedaEquiv.symm (specMapOfGlobalHom (presentationAlgebra g)
          (coordinateHom g ((globalFunctionsChartRestriction B S hS X V).comp e.toRingHom)
            h hrel)) ≫
        schemePointsMap B S hS
          (Spec.map (CommRingCat.ofHom (presentationStructureHom g)))
Tag 07SR, a lemma

Tag 07SR in the Stacks Project.

AlgebraicGeometry.Space.DescentSituation.exists_isRepresentable_system_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/SchemeStage.lean, line 207. The attribute's comment: “Correction: the index set is taken smaller than the cofinality of the site's size cutoff, the form the convention of Section 70.2 takes in this size model; without it the statement is false here (base changes of a non locally separated space to fields of sizes cofinal in the cutoff have empty limit, a scheme, and no stage a scheme)”.

In the situation of Stacks 084R over a scheme S — a directed inverse system of quasi-compact and quasi-separated algebraic spaces over S with affine transition morphisms, together with a chosen limit X — if X is a scheme then some stage X_i is a scheme. The index set may live in any universe; its cardinality is asked to be below the cofinality of the site's size cutoff.

theorem exists_isRepresentable_system_obj {I : Type v} [Preorder I] [IsDirected I (· ≤ ·)]
    (D : DescentSituation B S hS hZ I)
    (hI : Cardinal.lift.{u} #I < Cardinal.lift.{v} B.cutoff.ord.cof)
    (hX : D.limitCone.pt.IsRepresentable) :
    ∃ i, (D.system.obj (op i)).IsRepresentable

AlgebraicGeometry.Space.DescentSituation.exists_isRepresentable_system_obj_of_siteContainsBaseChangeLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/SchemeStageSiteSmall.lean, line 283.

In the situation of Stacks 084R — a directed inverse system of quasi-compact and quasi-separated algebraic spaces over S with affine transition morphisms, together with a chosen limit X, under the convention of Section 70.2 (tag 07SD) that the rings the chapter forms have their spectra in the big fppf site — if X is a scheme then there is a stage X_i which is a scheme. Nothing is asked of the index set beyond directedness.

theorem exists_isRepresentable_system_obj_of_siteContainsBaseChangeLimits {I : Type u}
    [Preorder I] [IsDirected I (· ≤ ·)]
    (D : DescentSituation B S hS hZ I) (hconv : SiteContainsBaseChangeLimits B S hS D.system)
    (hX : D.limitCone.pt.IsRepresentable) :
    ∃ i, (D.system.obj (op i)).IsRepresentable
Tag 0828, a lemma

Tag 0828 in the Stacks Project.

AlgebraicGeometry.Space.eventually_isClosedImmersion_comp_limitπ', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ClosedImmersionDescent/EventualImmersion.lean, line 502. The attribute's comment: “part (1): closed immersions”.

Stacks 0828, part (1). Let X = lim Xᵢ be a directed limit of algebraic spaces over an algebraic space Bspace, with affine transition morphisms and quasi-compact stages, and let f : Y ⟶ X be a closed immersion with Y locally of finite type over Bspace. Then Y ⟶ Xᵢ is a closed immersion for all sufficiently large i.

theorem eventually_isClosedImmersion_comp_limitπ'
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (contains : B.Contains S)
    {I : Type u} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (Bspace : (BigFppfOver B S contains)ᵒᵖ ⥤ Type u)
    (algebraicBase : IsAlgebraicSpace B S contains Bspace)
    (D : Iᵒᵖ ⥤ (BigFppfOver B S contains)ᵒᵖ ⥤ Type u)
    (algebraicStage : ∀ i, IsAlgebraicSpace B S contains (D.obj (op i)))
    (t : D ⟶ (Functor.const Iᵒᵖ).obj Bspace)
    (c : Cone D) (isLimit : IsLimit c) (s : c.pt ⟶ Bspace)
    (commutes : c.π ≫ t = (Functor.const Iᵒᵖ).map s)
    (Y : (BigFppfOver B S contains)ᵒᵖ ⥤ Type u)
    (algebraic : IsAlgebraicSpace B S contains Y)
    (f : Y ⟶ c.pt)
    (quasiCompactStage : ∀ i, IsQuasiCompactSpace B S contains (D.obj (op i)))
    (affine : ∀ ⦃i j : I⦄ (h : i ≤ j), Space.IsAffineHom B S contains (D.map (homOfLE h).op))
    (finiteType : Space.IsLocallyOfFiniteType B S contains (f ≫ s))
    (closed : Space.IsClosedImmersion B S contains f) :
    ∀ᶠ i in atTop, Space.IsClosedImmersion B S contains (f ≫ c.π.app (op i))

AlgebraicGeometry.Space.eventually_isImmersion_comp_limitπ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ClosedImmersionDescent/EventualImmersion.lean, line 727. The attribute's comment: “part (2): immersions”.

Stacks 0828, part (2). Let X = lim Xᵢ be a directed limit of algebraic spaces over an algebraic space Bspace, with affine transition morphisms and quasi-separated stages, and let f : Y ⟶ X be an immersion whose source is quasi-compact and locally of finite type over Bspace. Then Y ⟶ Xᵢ is an immersion for all sufficiently large i.

The image of Y in one stage Xᵢ₀ lies in a quasi-compact open subspace V, and the system of preimages of V in the stages above i₀ has quasi-compact stages and limit the preimage of V in X, through which f factors by an immersion. An affine étale atlas of V reduces the statement to schemes, where it is Stacks 081B, part (2) (AlgebraicGeometry.EventualLimit.eventually_isImmersion_comp_π_app), and the immersion is carried back to the stages by effective descent of immersions along surjective étale morphisms; quasi-separatedness of Xᵢ₀ makes the base change of Y to the atlas quasi-compact.

theorem eventually_isImmersion_comp_limitπ
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (contains : B.Contains S)
    {I : Type u} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (Bspace : (BigFppfOver B S contains)ᵒᵖ ⥤ Type u)
    (algebraicBase : IsAlgebraicSpace B S contains Bspace)
    (D : Iᵒᵖ ⥤ (BigFppfOver B S contains)ᵒᵖ ⥤ Type u)
    (algebraicStage : ∀ i, IsAlgebraicSpace B S contains (D.obj (op i)))
    (t : D ⟶ (Functor.const Iᵒᵖ).obj Bspace)
    (c : Cone D) (isLimit : IsLimit c) (s : c.pt ⟶ Bspace)
    (commutes : c.π ≫ t = (Functor.const Iᵒᵖ).map s)
    (Y : (BigFppfOver B S contains)ᵒᵖ ⥤ Type u)
    (algebraic : IsAlgebraicSpace B S contains Y)
    (quasiCompact : IsQuasiCompactSpace B S contains Y)
    (f : Y ⟶ c.pt)
    (affine : ∀ ⦃i j : I⦄ (h : i ≤ j), IsAffineHom B S contains (D.map (homOfLE h).op))
    (quasiSeparated : ∀ i,
      IsAbsolutelyQuasiSeparated B S contains B.contains_terminal (D.obj (op i)))
    (finiteType : IsLocallyOfFiniteType B S contains (f ≫ s))
    (immersion : IsImmersion B S contains f) :
    ∀ᶠ i in atTop, IsImmersion B S contains (f ≫ c.π.app (op i))

AlgebraicGeometry.Space.eventually_isIso_comp_limitπ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/EventualIsomorphism.lean, line 420. The attribute's comment: “part (3): isomorphism”. References: SGA 3 XI (3.11), “more general”.

An isomorphism onto a directed limit is eventually an isomorphism onto the stages. Let X = lim Xᵢ be a directed limit of algebraic spaces over an algebraic space Bspace and let f : Y ⟶ X be an isomorphism. If the stages Xᵢ are quasi-compact and locally of finite type over Bspace, the transition morphisms are closed immersions, and Y is locally of finite presentation over Bspace, then Y ⟶ Xᵢ is an isomorphism for all sufficiently large i.

theorem eventually_isIso_comp_limitπ
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (contains : B.Contains S)
    {I : Type v} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (Bspace : (BigFppfOver B S contains)ᵒᵖ ⥤ Type u)
    (algebraicBase : IsAlgebraicSpace B S contains Bspace)
    (D : Iᵒᵖ ⥤ (BigFppfOver B S contains)ᵒᵖ ⥤ Type u)
    (algebraicStage : ∀ i, IsAlgebraicSpace B S contains (D.obj (op i)))
    (t : D ⟶ (Functor.const Iᵒᵖ).obj Bspace)
    (c : Cone D) (isLimit : IsLimit c) (s : c.pt ⟶ Bspace)
    (commutes : c.π ≫ t = (Functor.const Iᵒᵖ).map s)
    (Y : (BigFppfOver B S contains)ᵒᵖ ⥤ Type u) (algebraic : IsAlgebraicSpace B S contains Y)
    (f : Y ⟶ c.pt) (iso : IsIso f)
    (quasiCompactStage : ∀ i, IsQuasiCompactSpace B S contains (D.obj (op i)))
    (finiteType : ∀ i, IsLocallyOfFiniteType B S contains (t.app (op i)))
    (closed : ∀ ⦃i j : I⦄ (h : i ≤ j), IsClosedImmersion B S contains (D.map (homOfLE h).op))
    (finitePresentation : IsLocallyOfFinitePresentation B S contains (f ≫ s)) :
    ∀ᶠ i in atTop, IsIso (f ≫ c.π.app (op i))

AlgebraicGeometry.Space.eventually_mono_comp_limitπ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/EventualMonomorphism.lean, line 162. The attribute's comment: “part (4): monomorphism”.

Stacks 0828, part (4). Let X = lim Xᵢ be a directed limit of algebraic spaces over an algebraic space Bspace, with affine transition morphisms and quasi-separated stages, and let f : Y ⟶ X be a monomorphism whose source is quasi-compact and locally of finite type over Bspace. Then Y ⟶ Xᵢ is a monomorphism for all sufficiently large i.

theorem eventually_mono_comp_limitπ
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (contains : B.Contains S)
    {I : Type v} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (Bspace : (BigFppfOver B S contains)ᵒᵖ ⥤ Type u)
    (algebraicBase : IsAlgebraicSpace B S contains Bspace)
    (D : Iᵒᵖ ⥤ (BigFppfOver B S contains)ᵒᵖ ⥤ Type u)
    (algebraicStage : ∀ i, IsAlgebraicSpace B S contains (D.obj (op i)))
    (t : D ⟶ (Functor.const Iᵒᵖ).obj Bspace)
    (c : Cone D) (isLimit : IsLimit c) (s : c.pt ⟶ Bspace)
    (commutes : c.π ≫ t = (Functor.const Iᵒᵖ).map s)
    (Y : (BigFppfOver B S contains)ᵒᵖ ⥤ Type u) (algebraic : IsAlgebraicSpace B S contains Y)
    (quasiCompact : IsQuasiCompactSpace B S contains Y)
    (f : Y ⟶ c.pt) [Mono f]
    (affine : ∀ ⦃i j : I⦄ (h : i ≤ j), IsAffineHom B S contains (D.map (homOfLE h).op))
    (quasiSeparated : ∀ i,
      IsAbsolutelyQuasiSeparated B S contains B.contains_terminal (D.obj (op i)))
    (finiteType : IsLocallyOfFiniteType B S contains (f ≫ s)) :
    ∀ᶠ i in atTop, Mono (f ≫ c.π.app (op i))
Tag 086X, a lemma

Tag 086X in the Stacks Project.

AlgebraicGeometry.Space.DescentSituation.exists_isSeparated_system_app_of_isSiteSmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/SeparatedDescent.lean, line 1093.

Stacks 086X. Let Y be a quasi-separated algebraic space over S and let X = lim X_i be a directed limit, over Y and with affine transition morphisms, of quasi-compact and quasi-separated algebraic spaces over S, as in the standing situation of Stacks 084R. If X ⟶ Y is separated then X_i ⟶ Y is separated for all i large enough.

Fix the distinguished stage 0 of the system and choose an affine étale surjective chart U ⟶ X_0, which exists because X_0 is quasi-compact, and let u : U ⟶ Y be its composite with the structure morphism. Base changing the whole situation along u is again a situation of Stacks 084R — the stages stay quasi-compact because U is quasi-compact and Y is quasi-separated — whose limit X ×_Y U is separated over the affine scheme U, hence a separated algebraic space. So some stage X_i ×_Y U is separated by Stacks 084T, that is, X_i ×_Y U ⟶ U is separated. Affineness of the transition morphism X_i ⟶ X_0 turns the chart U ⟶ X_0 into a chart U_i = U ×_{X_0} X_i ⟶ X_i of that stage, again surjective and étale and with U_i ⟶ X_i ⟶ Y factoring through u; separatedness of X_i ⟶ Y therefore descends from that of X_i ×_Y U ⟶ U. Finally the transition morphisms are affine, hence separated, so X_k ⟶ Y is separated for every k ≥ i.

theorem DescentSituation.exists_isSeparated_system_app_of_isSiteSmall [IsDirected I (· ≤ ·)]
    (D : DescentSituation B S hS hZ I) (hb : Space.IsSiteSmall B S hS D.system)
    (hY : IsAlgebraicSpace B S hS Y) (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y)
    (t : D.system ⟶ (Functor.const Iᵒᵖ).obj Y) (f : D.limitCone.pt ⟶ Y)
    (hf : ∀ j, D.limitCone.π.app j ≫ t.app j = f) (hsep : IsSeparated B S hS f) :
    ∃ i, D.base ≤ i ∧ ∀ k, i ≤ k → IsSeparated B S hS (t.app (op k))

AlgebraicGeometry.Space.DescentSituation.exists_isSeparated_system_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/SeparatedDescent.lean, line 1160.

Stacks 086X. Let Y be a quasi-separated algebraic space over S and let X = lim X_i be a directed limit, over Y and with affine transition morphisms, of quasi-compact and quasi-separated algebraic spaces over S, as in the standing situation of Stacks 084R. If X ⟶ Y is separated then X_i ⟶ Y is separated for all i large enough.

Fix the distinguished stage 0 of the system and choose an affine étale surjective chart U ⟶ X_0, which exists because X_0 is quasi-compact, and let u : U ⟶ Y be its composite with the structure morphism. Base changing the whole situation along u is again a situation of Stacks 084R — the stages stay quasi-compact because U is quasi-compact and Y is quasi-separated — whose limit X ×_Y U is separated over the affine scheme U, hence a separated algebraic space. So some stage X_i ×_Y U is separated by Stacks 084T, that is, X_i ×_Y U ⟶ U is separated. Affineness of the transition morphism X_i ⟶ X_0 turns the chart U ⟶ X_0 into a chart U_i = U ×_{X_0} X_i ⟶ X_i of that stage, again surjective and étale and with U_i ⟶ X_i ⟶ Y factoring through u; separatedness of X_i ⟶ Y therefore descends from that of X_i ×_Y U ⟶ U. Finally the transition morphisms are affine, hence separated, so X_k ⟶ Y is separated for every k ≥ i.

theorem DescentSituation.exists_isSeparated_system_app [IsDirected I (· ≤ ·)]
    (D : DescentSituation B S hS hZ I) (hI : #I < B.cutoff.ord.cof)
    (hY : IsAlgebraicSpace B S hS Y) (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y)
    (t : D.system ⟶ (Functor.const Iᵒᵖ).obj Y) (f : D.limitCone.pt ⟶ Y)
    (hf : ∀ j, D.limitCone.π.app j ≫ t.app j = f) (hsep : IsSeparated B S hS f) :
    ∃ i, D.base ≤ i ∧ ∀ k, i ≤ k → IsSeparated B S hS (t.app (op k))
Tag 0A0R, a lemma

Tag 0A0R in the Stacks Project.

Declarations registered for the tag:

Tag 0A0S, a lemma

Tag 0A0S in the Stacks Project.

AlgebraicGeometry.Space.eventually_isFinite_of_isLimit_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/EventualFiniteness.lean, line 193.

Stacks 0A0S. Let X = lim X_i be a directed limit of algebraic spaces over an algebraic space Y, with affine transition morphisms. If Y is quasi-compact and quasi-separated, every X_i is quasi-compact and quasi-separated, the transition morphisms are finite, every X_i → Y is locally of finite type and X → Y is integral, then X_i → Y is finite for all sufficiently large i.

The limit X is an algebraic space by Stacks 07SF (AlgebraicGeometry.Space.isAlgebraicSpace_limit_of_isSiteSmall), so that is not assumed. Every input of the source's proof is discharged: the affine étale chart of Y by Stacks 03H6, the affine stage of the base-changed system by Stacks 07SQ, the finiteness of the base-changed stages descending to finiteness over Y by Stacks 03ZQ, and the scheme case by Stacks 09ZN. The index set is asked to be small compared to the cofinality of the site's size cutoff, the Stacks 07SF bound that both Stacks 07SQ and the passage from the site to schemes carry here.

theorem eventually_isFinite_of_isLimit_of_isIntegral
    {I : Type u} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (hI : #I < B.cutoff.ord.cof)
    (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (D : Iᵒᵖ ⥤ ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (p : D ⟶ (Functor.const Iᵒᵖ).obj Y)
    (c : Cone D) (hc : IsLimit c) (f : c.pt ⟶ Y)
    (hf : ∀ i : I, f = c.π.app (op i) ≫ p.app (op i))
    (hY : IsAlgebraicSpace B S hS Y)
    (hD : ∀ i : I, IsAlgebraicSpace B S hS (D.obj (op i)))
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y)
    (hDqc : ∀ i : I, IsQuasiCompactSpace B S hS (D.obj (op i)))
    (hDqs : ∀ i : I, IsAbsolutelyQuasiSeparated B S hS hZ (D.obj (op i)))
    (haffine : ∀ {i j : I} (h : i ≤ j), IsAffineHom B S hS (D.map (homOfLE h).op))
    (hfinite : ∀ {i j : I} (h : i ≤ j), IsFinite B S hS (D.map (homOfLE h).op))
    (hfiniteType : ∀ i : I, IsLocallyOfFiniteType B S hS (p.app (op i)))
    (hintegral : IsIntegralHom B S hS f) :
    ∀ᶠ i : I in Filter.atTop, IsFinite B S hS (p.app (op i))
Tag 0A0T, a lemma

Tag 0A0T in the Stacks Project.

AlgebraicGeometry.Space.eventually_isClosedImmersion_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/EventuallyClosedImmersionOverBase.lean, line 619.

Stacks 0A0T. Let Y be an algebraic space over S and let X = lim X_i be a directed limit of algebraic spaces over Y with affine transition morphisms. Assume Y is quasi-compact and quasi-separated, the X_i are quasi-compact and quasi-separated, the transition morphisms X_{i'} ⟶ X_i are closed immersions, each X_i ⟶ Y is locally of finite type, and X ⟶ Y is a closed immersion. Then X_i ⟶ Y is a closed immersion for i large enough.

Closed immersions are affine, so the source's assumption that the transition morphisms are affine is implied by the assumption that they are closed immersions and is not stated separately.

The proof is AlgebraicGeometry.Space.eventually_isClosedImmersion_app_of_isRepresentable_stage, which is the source's argument down to its appeal to Stacks 07SR, fed with the stage that Stacks 07SR provides: the limit of the system base changed along an affine étale surjective chart of Y is a closed subspace of an affine scheme, hence a scheme, so AlgebraicGeometry.Space.DescentSituation.exists_isRepresentable_system_obj_of_isSiteSmall makes some stage of that base changed system a scheme.

The index type is I : Type u and its cardinality is asked to be small compared to the cofinality of the site's size cutoff, as in Situation 084R (AlgebraicGeometry.Space.LimitSituation) and as in every result of that family which this library proves — Stacks 07SF, Stacks 0827, Stacks 084T, Stacks 086X, Stacks 07SQ and Stacks 07SR. The bound is used only to invoke Stacks 07SR.

theorem eventually_isClosedImmersion_app
    {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)] [Nonempty I]
    {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (D : Iᵒᵖ ⥤ (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (t : D ⟶ (Functor.const Iᵒᵖ).obj Y)
    (c : Cone D) (hc : IsLimit c) (f : c.pt ⟶ Y)
    (hcomm : c.π ≫ t = (Functor.const Iᵒᵖ).map f)
    (hY : IsAlgebraicSpace B S hS Y) (hX : IsAlgebraicSpace B S hS c.pt)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj (op i)))
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y)
    (hDqc : ∀ i, IsQuasiCompactSpace B S hS (D.obj (op i)))
    (hDqs : ∀ i, IsAbsolutelyQuasiSeparated B S hS hZ (D.obj (op i)))
    (hClosed : ∀ {a b : Iᵒᵖ} (φ : a ⟶ b), IsClosedImmersion B S hS (D.map φ))
    (hFT : ∀ i, IsLocallyOfFiniteType B S hS (t.app (op i)))
    (hf : IsClosedImmersion B S hS f) (hI : #I < B.cutoff.ord.cof) :
    ∀ᶠ i in atTop, IsClosedImmersion B S hS (t.app (op i))
Sources
LeanAlgebraicGeometry.Space.existsUnique_point_limit · AlgebraicGeometry.Space.isHomeomorph_pointsLimitComparison · AlgebraicGeometry.Space.pointTopology_limit · AlgebraicGeometry.Space.pointTopology_limit_of_isSiteSmall · AlgebraicGeometry.Space.nonempty_points_limit · AlgebraicGeometry.Space.closure_singleton_limit · AlgebraicGeometry.Space.existsUnique_point_closure_limit · AlgebraicGeometry.Space.exists_iso_limit_reducedClosure

Section70.6 Descending properties of morphisms#

Section 70.6 of the Stacks Project, Tag 084V. 14 tags here are carried by 19 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 084W, a situation

Tag 084W in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentSystem, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingMorphisms.lean, line 111.

Stacks 084W. The standing situation for descending a property of a morphism of algebraic spaces along a directed limit: a directed inverse system of algebraic spaces over S with affine transition morphisms and algebraic limit, a distinguished stage of the system, and a morphism of quasi-compact quasi-separated algebraic spaces over that stage.

structure MorphismDescentSystem (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hZ : B.Contains (⊤_ Scheme.{u})) (I : Type u) [Preorder I] [IsDirected I (· ≤ ·)]
Tag 07SL, a lemma

Tag 07SL in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentSystem.exists_isEtale_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingMorphismProperties.lean, line 1262. References: EGA IV (17.7.8), “(ii) étale”.

Stacks 07SL. In the situation of Stacks 084W, if the base change f of f₀ to the limit B is étale and f₀ is locally of finite presentation, then the base change f_i of f₀ to some stage B_i is étale.

theorem exists_isEtale_mapAt (D : MorphismDescentSystem B S hS hZ I)
    (etale : IsEtale B S hS D.mapLimit) (fp : IsLocallyOfFinitePresentation B S hS D.map₀) :
    ∃ (i : I) (le : D.initial ≤ i), IsEtale B S hS (D.mapAt i le)
Tag 0CN2, a lemma

Tag 0CN2 in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentSystem.exists_isSmooth_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingMorphismProperties.lean, line 1281. References: EGA IV (17.12.6), “f smooth ⇒ ∃λ”; EGA IV (17.7.8), “(ii) smooth”.

Stacks 0CN2. In the situation of Stacks 084W, if the base change f of f₀ to the limit B is smooth and f₀ is locally of finite presentation, then the base change f_i of f₀ to some stage B_i is smooth.

theorem exists_isSmooth_mapAt (D : MorphismDescentSystem B S hS hZ I)
    (smooth : IsSmooth B S hS D.mapLimit) (fp : IsLocallyOfFinitePresentation B S hS D.map₀) :
    ∃ (i : I) (le : D.initial ≤ i), IsSmooth B S hS (D.mapAt i le)

AlgebraicGeometry.Space.MorphismDescentSystem.exists_isSmooth_mapAt_op, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingMorphismProperties.lean, line 1435. The attribute's comment: “the cofiltered-covariant form: the conclusion ranges over a morphism of the cofiltered index category Iᵒᵖ carrying the covariant diagram base, which is the indexing the library's Stacks 07SK consumes, rather than over an inequality of the directed preorder I; the mathematical content is that of the inequality form beside it”.

Stacks 0CN2 in the covariant indexing of Stacks 07SK. In the situation of Stacks 084W, if the base change f of f₀ to the limit B is smooth and f₀ is locally of finite presentation, then there is a morphism j ⟶ 0 of the cofiltered index category Iᵒᵖ along which the base change of f₀ is smooth.

This is AlgebraicGeometry.Space.MorphismDescentSystem.exists_isSmooth_mapAt with its conclusion read over a morphism of Iᵒᵖ instead of an inequality of I; the transition morphism is the same one, by AlgebraicGeometry.Space.MorphismDescentSystem.base_map_eq_baseAtToInitial. It is the shape in which the conclusions of Stacks 07SK are stated, so the two can be used together.

theorem exists_isSmooth_mapAt_op (D : MorphismDescentSystem B S hS hZ I)
    (smooth : IsSmooth B S hS D.mapLimit) (fp : IsLocallyOfFinitePresentation B S hS D.map₀) :
    ∃ (j : Iᵒᵖ) (g : j ⟶ op D.initial),
      IsSmooth B S hS (D.mapAt j.unop (leOfHom g.unop))
Tag 07SN, a lemma

Tag 07SN in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentSystem.exists_isSurjective_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingMorphismProperties.lean, line 1271.

Stacks 07SN. In the situation of Stacks 084W, if the base change f of f₀ to the limit B is surjective and f₀ is locally of finite presentation, then the base change f_i of f₀ to some stage B_i is surjective.

theorem exists_isSurjective_mapAt
    (D : MorphismDescentSystem B S hS hZ I) (surjective : IsSurjective B S hS D.mapLimit)
    (fp : IsLocallyOfFinitePresentation B S hS D.map₀) :
    ∃ (i : I) (le : D.initial ≤ i), IsSurjective B S hS (D.mapAt i le)
Tag 084X, a lemma

Tag 084X in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentSystem.exists_universallyInjective_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingMorphismProperties.lean, line 1374.

Stacks 084X. In the situation of Stacks 084W, if the base change f of f₀ to the limit B is universally injective and f₀ is locally of finite type, then the base change f_i of f₀ to some stage B_i is universally injective.

theorem exists_universallyInjective_mapAt
    (D : MorphismDescentSystem B S hS hZ I)
    (injective : UniversallyInjective B S hS D.mapLimit)
    (ft : IsLocallyOfFiniteType B S hS D.map₀) :
    ∃ (i : I) (le : D.initial ≤ i), UniversallyInjective B S hS (D.mapAt i le)
Tag 084Y, a lemma

Tag 084Y in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentSituation.exists_isAffineHom_mapAt_of_isAffineHom_mapLimit_of_siteContainsBaseChangeLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/AffineMorphismDescent.lean, line 211.

Notation and assumptions as in Situation 70.6.1 (tag 084W), carried by AlgebraicGeometry.Space.MorphismDescentSituation, in the chapter's setting of Section 70.2 (tag 07SD): B = lim B_i a directed inverse limit of algebraic spaces over S with affine transition morphisms, f₀ : X₀ ⟶ Y₀ a morphism of algebraic spaces over B₀ with B₀, X₀ and Y₀ quasi-compact and quasi-separated, and f_i : X_i ⟶ Y_i, f : X ⟶ Y its base changes to B_i for i ≥ 0 and to B. If f is affine, then f_i is affine for some i ≥ 0.

The hypothesis hconv is the chapter's standing convention that every ring considered has its spectrum in the big fppf site, read for the system of bases; nothing is asked of the index. The implementation notes of this module show that the statement fails without it; the corresponding failure of Stacks 07SQ, on which the proof rests, is AlgebraicGeometry.Space.DescentSituation.not_forall_exists_isAffineSpace_system_obj.

The proof is the source's: exists_isAffineHom_mapAt_of_descentAffineStage_of_siteContainsBaseChangeLimits with Stacks 07SQ supplied by DescentSituation.exists_isAffineSpace_system_obj_of_siteContainsBaseChangeLimits.

theorem exists_isAffineHom_mapAt_of_isAffineHom_mapLimit_of_siteContainsBaseChangeLimits
    (hconv : SiteContainsBaseChangeLimits B S hS D.base) (hf : IsAffineHom B S hS D.mapLimit) :
    ∃ (i : I) (hi : D.initial ≤ i), IsAffineHom B S hS (D.mapAt i hi)

AlgebraicGeometry.Space.MorphismDescentData.exists_isAffineHom_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/MorphismDescentData.lean, line 205.

In Situation 084W, under the chapter's convention of Section 70.2, if f : X ⟶ Y is affine then f_i : X_i ⟶ Y_i is affine for some i ≥ 0.

theorem exists_isAffineHom_mapAt (hconv : SiteContainsBaseChangeLimits B S hS D.base)
    (hf : IsAffineHom B S hS (D.toMorphismDescentSituation hconv).mapLimit) :
    ∃ (i : I) (hi : D.initial ≤ i),
      IsAffineHom B S hS ((D.toMorphismDescentSituation hconv).mapAt i hi)
Tag 084Z, a lemma

Tag 084Z in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentData.exists_isFinite_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/MorphismDescentData.lean, line 215.

In Situation 084W, under the chapter's convention of Section 70.2, if f is finite and f₀ is locally of finite type, then f_i is finite for some i ≥ 0.

theorem exists_isFinite_mapAt (hconv : SiteContainsBaseChangeLimits B S hS D.base)
    (hf : IsFinite B S hS (D.toMorphismDescentSituation hconv).mapLimit)
    (hf₀ : IsLocallyOfFiniteType B S hS D.map₀) :
    ∃ (i : I) (hi : D.initial ≤ i),
      IsFinite B S hS ((D.toMorphismDescentSituation hconv).mapAt i hi)
Tag 0850, a lemma

Tag 0850 in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentData.exists_isClosedImmersion_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/MorphismDescentData.lean, line 227.

In Situation 084W, under the chapter's convention of Section 70.2, if f is a closed immersion and f₀ is locally of finite type, then f_i is a closed immersion for some i ≥ 0.

theorem exists_isClosedImmersion_mapAt (hconv : SiteContainsBaseChangeLimits B S hS D.base)
    (hf : IsClosedImmersion B S hS (D.toMorphismDescentSituation hconv).mapLimit)
    (hf₀ : IsLocallyOfFiniteType B S hS D.map₀) :
    ∃ (i : I) (hi : D.initial ≤ i),
      IsClosedImmersion B S hS ((D.toMorphismDescentSituation hconv).mapAt i hi)
Tag 0851, a lemma

Tag 0851 in the Stacks Project.

AlgebraicGeometry.Space.exists_isSeparated_pullbackMap_of_siteContainsBaseChangeLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChangeOfBigSite/SeparatedDescent.lean, line 58. The attribute's comment: “under the chapter's convention of Section 70.2 (tag 07SD) on the system of bases, every stage quasi-compact; proved in an enlarged site”.

Stacks 0851. In the situation of Stacks 084W, if the base change f : X ⟶ Y of f₀ : X₀ ⟶ Y₀ to the limit B = lim B_i is separated, then the base change f_i : X_i ⟶ Y_i of f₀ to some stage B_i with i ≥ 0 is separated.

theorem exists_isSeparated_pullbackMap_of_siteContainsBaseChangeLimits {I : Type u} [Preorder I]
    [IsDirected I (· ≤ ·)] [Nonempty I] (base : Iᵒᵖ ⥤ (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hbase : ∀ i, IsAlgebraicSpace B S hS (base.obj i))
    (hAffine : ∀ {i j : Iᵒᵖ} (a : i ⟶ j), IsAffineHom B S hS (base.map a))
    (hconv : SiteContainsBaseChangeLimits B S hS base)
    (hQc : ∀ i, IsQuasiCompactSpace B S hS (base.obj i)) (i₀ : I)
    {X₀ Y₀ : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (p : X₀ ⟶ base.obj (op i₀))
    (q : Y₀ ⟶ base.obj (op i₀)) (f₀ : X₀ ⟶ Y₀) (hf₀ : f₀ ≫ q = p)
    (hX₀ : IsAlgebraicSpace B S hS X₀) (hY₀ : IsAlgebraicSpace B S hS Y₀)
    (hB₀qs : IsAbsolutelyQuasiSeparated B S hS hZ (base.obj (op i₀)))
    (hX₀qc : IsQuasiCompactSpace B S hS X₀) (hX₀qs : IsAbsolutelyQuasiSeparated B S hS hZ X₀)
    (hY₀qc : IsQuasiCompactSpace B S hS Y₀) (hY₀qs : IsAbsolutelyQuasiSeparated B S hS hZ Y₀)
    (hf : IsSeparated B S hS (pullback.map (limit.π base (op i₀)) p (limit.π base (op i₀)) q
      (𝟙 _) f₀ (𝟙 _) (by simp) (by simp [hf₀]))) :
    ∃ (i : I) (hi : i₀ ≤ i), IsSeparated B S hS (pullback.map (base.map (homOfLE hi).op) p
      (base.map (homOfLE hi).op) q (𝟙 _) f₀ (𝟙 _) (by simp) (by simp [hf₀]))

AlgebraicGeometry.Space.MorphismDescentSystem.exists_isSeparated_mapAt_of_isSeparated_mapLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/SeparatedMorphismDescent.lean, line 477.

Stacks 0851. In the situation of Stacks 084W, if the base change f of f₀ to the limit B is separated, then the base change f_i of f₀ to some stage B_i is separated.

theorem exists_isSeparated_mapAt_of_isSeparated_mapLimit (hf : IsSeparated B S hS D.mapLimit) :
    ∃ (i : I) (hi : D.initial ≤ i), IsSeparated B S hS (D.mapAt i hi)
Tag 0852, a lemma

Tag 0852 in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentSystem.exists_isIso_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/Isomorphism.lean, line 363. References: EGA IV (8.8.2.5), “f iso ⇒ f_i iso”.

Stacks 0852, and Stacks 084S. In the situation of Stacks 084W, if the base change f of f₀ to the limit B is an isomorphism and f₀ is locally of finite presentation, then the base change f_i of f₀ to some stage B_i is an isomorphism.

This is Stacks 0852. Stacks 084S draws the same conclusion in the limit situation of Stacks 084R, with the source and the target in addition assumed representable over the stage; hypothesis (a) of that tag is not needed here, since the three properties into which being an isomorphism is decomposed all descend without it.

theorem exists_isIso_mapAt (hf : IsIso D.mapLimit)
    (hfp : IsLocallyOfFinitePresentation B S hS D.map₀) :
    ∃ (i : I) (hi : D.initial ≤ i), IsIso (D.mapAt i hi)
Tag 07SM, a lemma

Tag 07SM in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentSystem.exists_mono_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/Monomorphism.lean, line 137. References: SGA 3 VIB (10.1), “partial”.

If the base change f of f₀ to the limit B is a monomorphism and f₀ is locally of finite type, then the base change f_i of f₀ to some stage B_i is a monomorphism.

theorem exists_mono_mapAt (hf : Mono D.mapLimit)
    (hf₀ : IsLocallyOfFiniteType B S hS D.map₀) :
    ∃ (i : I) (hi : D.initial ≤ i), Mono (D.mapAt i hi)
Tag 08K0, a lemma

Tag 08K0 in the Stacks Project.

AlgebraicGeometry.Space.exists_isFlatOver_baseChange_of_chartLimitsInSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingModuleFlatnessUnbounded.lean, line 115. The attribute's comment: “flatness of a module, with no bound on the index: the 07SD convention in place of the index bound of MorphismDescentSystem, which exists_isFlatOver_mapAt carries”.

Stacks 08K0, flatness of a module, with no bound on the index. Let (B_i) be a cofiltered inverse system of algebraic spaces over S with affine transition morphisms, let i be a stage with B_i quasi-compact and quasi-separated, and let f : X ⟶ Y be a morphism of quasi-compact, quasi-separated algebraic spaces over B_i. Let F₀ be a quasi-coherent 𝒪_X-module of finite presentation. Suppose the pullback of F₀ to lim B_j ×_{B_i} X is flat over lim B_j ×_{B_i} Y, and f is locally of finite presentation. Then for some stage j ⟶ i the pullback of F₀ to B_j ×_{B_i} X is flat over B_j ×_{B_i} Y.

This strengthens AlgebraicGeometry.Space.MorphismDescentSystem.exists_isFlatOver_mapAt. The bound MorphismDescentSystem.indexSize on the index is replaced by hconv. hconv is the chapter's convention 07SD: the limits of the base changes of the stages to the affine objects of the site lie in the site. It is not an assumption beyond the source. It is equivalent to AlgebraicGeometry.Space.SiteContainsBaseChangeLimits, which it states unfolded, and the index bound implies it (AlgebraicGeometry.Space.chartLimitsInSite_of_lt_cof).

theorem exists_isFlatOver_baseChange_of_chartLimitsInSite
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hconv : ∀ (i : I) (Z : BigAffineFppf B S hS)
      (g : yoneda.obj ((BigAffineFppf.inclusion B S hS).obj Z) ⟶ D.obj i)
      (W : Over i ⥤ BigAffineFppf B S hS),
      (W ⋙ (BigAffineFppf.inclusion B S hS ⋙ yoneda) ≅
        (Over.post (X := i) D ⋙ Over.pullback g) ⋙
          Over.forget (yoneda.obj ((BigAffineFppf.inclusion B S hS).obj Z))) →
      ∀ c : Cone (((W ⋙ BigAffineFppf.inclusion B S hS) ⋙
          BigFppfOver.forget B S hS) ⋙ B.inclusion),
        IsLimit c → B.Contains c.pt)
    (hD : ∀ i, IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (i : I) (hB₀qc : IsQuasiCompactSpace B S hS (D.obj i))
    (hB₀qs : IsAbsolutelyQuasiSeparated B S hS hZ (D.obj i))
    {X Y : Over (D.obj i)} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X.left) (hY : IsAlgebraicSpace B S hS Y.left)
    (hXqc : IsQuasiCompactSpace B S hS X.left) (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.left)
    (hYqc : IsQuasiCompactSpace B S hS Y.left) (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y.left)
    (F₀ : Modules.{u, u} B S hS X.left hX)
    [F₀.IsQuasicoherentOnSite] [F₀.IsFinitePresentationOnSite]
    (flat : IsFlatOver B S hS
      (isAlgebraicSpace_pullback B S hS (limit.π D i) X.hom
        (isAlgebraicSpace_limit_of_chartLimitsInSite B S hS D hconv hD hAffine i hB₀qc) hX (hD i))
      (pullback.map (limit.π D i) X.hom (limit.π D i) Y.hom (𝟙 _) f.left (𝟙 _) (by simp)
        (by simp))
      ((modulePullback B S hS (ObjectProperty.homMk (pullback.snd (limit.π D i) X.hom) :
          (⟨pullback (limit.π D i) X.hom,
            isAlgebraicSpace_pullback B S hS (limit.π D i) X.hom
              (isAlgebraicSpace_limit_of_chartLimitsInSite B S hS D hconv hD hAffine i hB₀qc) hX
              (hD i)⟩ : AlgebraicSpaces B S hS) ⟶ ⟨X.left, hX⟩)).obj F₀))
    (fp : IsLocallyOfFinitePresentation B S hS f.left) :
    ∃ (j : I) (e : j ⟶ i), IsFlatOver B S hS
      (isAlgebraicSpace_pullback B S hS (D.map e) X.hom (hD j) hX (hD i))
      (pullback.map (D.map e) X.hom (D.map e) Y.hom (𝟙 _) f.left (𝟙 _) (by simp) (by simp))
      ((modulePullback B S hS (ObjectProperty.homMk (pullback.snd (D.map e) X.hom) :
          (⟨pullback (D.map e) X.hom,
            isAlgebraicSpace_pullback B S hS (D.map e) X.hom (hD j) hX (hD i)⟩ :
              AlgebraicSpaces B S hS) ⟶ ⟨X.left, hX⟩)).obj F₀)

AlgebraicGeometry.Space.MorphismDescentSystem.exists_isFlat_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingMorphismProperties.lean, line 1290. The attribute's comment: “in particular: flatness of the morphism”. References: EGA IV (11.2.6), “F = O_X case”.

Stacks 08K0, flatness of the morphism. In the situation of Stacks 084W, if f₀ is locally of finite presentation and its base change f : X ⟶ Y to the limit is flat, then its base change f_i : X_i ⟶ Y_i to some stage i ≥ 0 is flat.

theorem exists_isFlat_mapAt
    (D : MorphismDescentSystem B S hS hZ I) (flat : IsFlat B S hS D.mapLimit)
    (fp : IsLocallyOfFinitePresentation B S hS D.map₀) :
    ∃ (i : I) (le : D.initial ≤ i), IsFlat B S hS (D.mapAt i le)

AlgebraicGeometry.Space.MorphismDescentSystem.exists_isFlatOver_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingMorphismProperties.lean, line 1301. The attribute's comment: “flatness of a module”.

Stacks 08K0, flatness of a module. In the situation of Stacks 084W, let F₀ be a quasi-coherent 𝒪_{X₀}-module, with pullbacks F_i to X_i and F to X. If F is flat over Y, F₀ is of finite presentation and f₀ is locally of finite presentation, then F_i is flat over Y_i for some stage i ≥ 0.

theorem exists_isFlatOver_mapAt (D : MorphismDescentSystem B S hS hZ I)
    (F₀ : Modules.{u, u} B S hS D.source₀ D.source₀_isAlgebraicSpace)
    [F₀.IsQuasicoherentOnSite] [F₀.IsFinitePresentationOnSite]
    (flat : IsFlatOver B S hS D.sourceLimit_isAlgebraicSpace D.mapLimit
      ((modulePullback B S hS (ObjectProperty.homMk
        (pullback.snd (limit.π D.base (op D.initial)) D.sourceToBase) :
          (⟨D.sourceLimit, D.sourceLimit_isAlgebraicSpace⟩ : AlgebraicSpaces B S hS) ⟶
            ⟨D.source₀, D.source₀_isAlgebraicSpace⟩)).obj F₀))
    (fp : IsLocallyOfFinitePresentation B S hS D.map₀) :
    ∃ (i : I) (le : D.initial ≤ i), IsFlatOver B S hS (D.sourceAt_isAlgebraicSpace i le)
      (D.mapAt i le) ((modulePullback B S hS (ObjectProperty.homMk
        (pullback.snd (D.baseAtToInitial i le) D.sourceToBase) :
          (⟨D.sourceAt i le, D.sourceAt_isAlgebraicSpace i le⟩ : AlgebraicSpaces B S hS) ⟶
            ⟨D.source₀, D.source₀_isAlgebraicSpace⟩)).obj F₀)

Declarations registered for the tag:

Tag 08K1, a lemma

Tag 08K1 in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentData.exists_isProper_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/MorphismDescentData.lean, line 238.

In Situation 084W, under the chapter's convention of Section 70.2, if f is proper and f₀ is locally of finite type, then f_i is proper for some i ≥ 0.

theorem exists_isProper_mapAt (hconv : SiteContainsBaseChangeLimits B S hS D.base)
    (hf : IsProper B S hS (D.toMorphismDescentSituation hconv).mapLimit)
    (hf₀ : IsLocallyOfFiniteType B S hS D.map₀) :
    ∃ (i : I) (hi : D.initial ≤ i),
      IsProper B S hS ((D.toMorphismDescentSituation hconv).mapAt i hi)
Tag 0D4K, a lemma

Tag 0D4K in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentSystem.exists_hasRelativeDimensionLE_mapAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingMorphismProperties.lean, line 1386.

Stacks 0D4K. In the situation of Stacks 084W, if the base change f of f₀ to the limit B has relative dimension at most d and f₀ is locally of finite type, then the base change f_i of f₀ to some stage B_i has relative dimension at most d.

theorem exists_hasRelativeDimensionLE_mapAt (D : MorphismDescentSystem B S hS hZ I) (d : ℕ)
    (dimension : HasRelativeDimensionLE d B S hS D.mapLimit)
    (ft : IsLocallyOfFiniteType B S hS D.map₀) :
    ∃ (i : I) (le : D.initial ≤ i), HasRelativeDimensionLE d B S hS (D.mapAt i le)
Sources
LeanAlgebraicGeometry.Space.MorphismDescentSystem · AlgebraicGeometry.Space.MorphismDescentSystem.exists_isEtale_mapAt · AlgebraicGeometry.Space.MorphismDescentSystem.exists_isSmooth_mapAt · AlgebraicGeometry.Space.MorphismDescentSystem.exists_isSmooth_mapAt_op · AlgebraicGeometry.Space.MorphismDescentSystem.exists_isSurjective_mapAt · AlgebraicGeometry.Space.MorphismDescentSystem.exists_universallyInjective_mapAt · AlgebraicGeometry.Space.MorphismDescentSituation.exists_isAffineHom_mapAt_of_isAffineHom_mapLimit_of_siteContainsBaseChangeLimits · AlgebraicGeometry.Space.MorphismDescentData.exists_isAffineHom_mapAt

Section70.7 Descending relative objects#

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

Tag 07SK, a lemma

Tag 07SK in the Stacks Project.

AlgebraicGeometry.Space.exists_morphism_after_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationDescent.lean, line 3551. The attribute's comment: “fullness”.

A morphism between base changes of finite-presentation algebraic spaces is defined at a sufficiently late stage.

public theorem exists_morphism_after_baseChange
    (i : I) (Yᵢ Zᵢ : Over (D.obj i))
    (hY : AlgebraicGeometry.IsAlgebraicSpace B S hS Yᵢ.left)
    (hZ' : AlgebraicGeometry.IsAlgebraicSpace B S hS Zᵢ.left)
    (hYfp : AlgebraicGeometry.Space.IsFinitePresentation B S hS Yᵢ.hom)
    (hZfp : AlgebraicGeometry.Space.IsFinitePresentation B S hS Zᵢ.hom)
    (f : (Over.pullback (limit.π D i)).obj Yᵢ ⟶
      (Over.pullback (limit.π D i)).obj Zᵢ) :
    ∃ (j : I) (e : j ⟶ i)
      (g : (Over.pullback (D.map e)).obj Yᵢ ⟶
        (Over.pullback (D.map e)).obj Zᵢ)
      (α : (Over.pullback (limit.π D j)).obj
          ((Over.pullback (D.map e)).obj Yᵢ) ≅
        (Over.pullback (limit.π D i)).obj Yᵢ)
      (β : (Over.pullback (limit.π D j)).obj
          ((Over.pullback (D.map e)).obj Zᵢ) ≅
        (Over.pullback (limit.π D i)).obj Zᵢ),
      (α.hom.left ≫ pullback.fst Yᵢ.hom (limit.π D i) =
        pullback.fst ((Over.pullback (D.map e)).obj Yᵢ).hom (limit.π D j) ≫
          pullback.fst Yᵢ.hom (D.map e)) ∧
      (β.hom.left ≫ pullback.fst Zᵢ.hom (limit.π D i) =
        pullback.fst ((Over.pullback (D.map e)).obj Zᵢ).hom (limit.π D j) ≫
          pullback.fst Zᵢ.hom (D.map e)) ∧
      α.hom ≫ f = (Over.pullback (limit.π D j)).map g ≫ β.hom

AlgebraicGeometry.Space.eventually_eq_of_baseChange_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationDescent.lean, line 3726. The attribute's comment: “faithfulness”.

Two finite-stage morphisms that agree over the limit agree at a sufficiently late stage.

public theorem eventually_eq_of_baseChange_eq
    (i : I) (Yᵢ Zᵢ : Over (D.obj i))
    (hY : AlgebraicGeometry.IsAlgebraicSpace B S hS Yᵢ.left)
    (hZ' : AlgebraicGeometry.IsAlgebraicSpace B S hS Zᵢ.left)
    (hYfp : AlgebraicGeometry.Space.IsFinitePresentation B S hS Yᵢ.hom)
    (hZfp : AlgebraicGeometry.Space.IsFinitePresentation B S hS Zᵢ.hom)
    (f g : Yᵢ ⟶ Zᵢ)
    (hfg : (Over.pullback (limit.π D i)).map f =
      (Over.pullback (limit.π D i)).map g) :
    ∃ (j : I) (e : j ⟶ i),
      (Over.pullback (D.map e)).map f =
        (Over.pullback (D.map e)).map g

AlgebraicGeometry.Space.exists_model_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationDescent.lean, line 4598. The attribute's comment: “essential surjectivity”.

Every algebraic space of finite presentation over the limit descends to a finite stage.

public theorem exists_model_of_finitePresentation
    (Y : Over (limit D))
    (hY : AlgebraicGeometry.IsAlgebraicSpace B S hS Y.left)
    (hFp : AlgebraicGeometry.Space.IsFinitePresentation B S hS Y.hom) :
    ∃ (i : I) (Yᵢ : Over (D.obj i)),
      AlgebraicGeometry.IsAlgebraicSpace B S hS Yᵢ.left ∧
        AlgebraicGeometry.Space.IsFinitePresentation B S hS Yᵢ.hom ∧
        Nonempty (Y ≅ (Over.pullback (limit.π D i)).obj Yᵢ)

AlgebraicGeometry.Space.exists_morphism_after_baseChange_of_chartLimitsInSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationDescentUnbounded.lean, line 188. The attribute's comment: “fullness, with no bound on the index: the 07SD convention in place of the cardinality bounds of exists_morphism_after_baseChange”.

Stacks 07SK, fullness, with no bound on the index. A morphism between the base changes to the limit of two algebraic spaces of finite presentation over a stage comes from a morphism at a later stage.

This strengthens AlgebraicGeometry.Space.exists_morphism_after_baseChange: the cardinality bounds on the index category are replaced by hconv. hconv is the convention 07SD of the chapter: the limits of the base changes of the stages to the affine objects of the site lie in the site. It is not an assumption beyond the source. It is AlgebraicGeometry.Space.SiteContainsBaseChangeLimits unfolded, and the index bounds imply it.

It is AlgebraicGeometry.Space.exists_morphism_after_baseChange_of_siteContainsBaseChangeLimits without the hypothesis that the limit is an algebraic space, which Stacks 07SF under the convention supplies.

public theorem exists_morphism_after_baseChange_of_chartLimitsInSite
    (hconv : ∀ (i : I) (Z : AlgebraicGeometry.BigAffineFppf B S hS)
      (g : yoneda.obj ((AlgebraicGeometry.BigAffineFppf.inclusion B S hS).obj Z) ⟶ D.obj i)
      (W : Over i ⥤ AlgebraicGeometry.BigAffineFppf B S hS),
      (W ⋙ (AlgebraicGeometry.BigAffineFppf.inclusion B S hS ⋙ yoneda) ≅
        (Over.post (X := i) D ⋙ Over.pullback g) ⋙
          Over.forget (yoneda.obj ((AlgebraicGeometry.BigAffineFppf.inclusion B S hS).obj Z))) →
      ∀ c : Cone (((W ⋙ AlgebraicGeometry.BigAffineFppf.inclusion B S hS) ⋙
          AlgebraicGeometry.BigFppfOver.forget B S hS) ⋙ B.inclusion),
        IsLimit c → B.Contains c.pt)
    (hD : ∀ i, AlgebraicGeometry.IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.Space.IsAffineHom B S hS (D.map f))
    (hQc : ∀ i, AlgebraicGeometry.Space.IsQuasiCompactSpace B S hS (D.obj i))
    (hQs : ∀ i, AlgebraicGeometry.Space.IsAbsolutelyQuasiSeparated B S hS hZ (D.obj i))
    (i : I) (Yᵢ Zᵢ : Over (D.obj i))
    (hY : AlgebraicGeometry.IsAlgebraicSpace B S hS Yᵢ.left)
    (hZ' : AlgebraicGeometry.IsAlgebraicSpace B S hS Zᵢ.left)
    (hYfp : AlgebraicGeometry.Space.IsFinitePresentation B S hS Yᵢ.hom)
    (hZfp : AlgebraicGeometry.Space.IsFinitePresentation B S hS Zᵢ.hom)
    (f : (Over.pullback (limit.π D i)).obj Yᵢ ⟶
      (Over.pullback (limit.π D i)).obj Zᵢ) :
    ∃ (j : I) (e : j ⟶ i)
      (g : (Over.pullback (D.map e)).obj Yᵢ ⟶
        (Over.pullback (D.map e)).obj Zᵢ)
      (α : (Over.pullback (limit.π D j)).obj
          ((Over.pullback (D.map e)).obj Yᵢ) ≅
        (Over.pullback (limit.π D i)).obj Yᵢ)
      (β : (Over.pullback (limit.π D j)).obj
          ((Over.pullback (D.map e)).obj Zᵢ) ≅
        (Over.pullback (limit.π D i)).obj Zᵢ),
      (α.hom.left ≫ pullback.fst Yᵢ.hom (limit.π D i) =
        pullback.fst ((Over.pullback (D.map e)).obj Yᵢ).hom (limit.π D j) ≫
          pullback.fst Yᵢ.hom (D.map e)) ∧
      (β.hom.left ≫ pullback.fst Zᵢ.hom (limit.π D i) =
        pullback.fst ((Over.pullback (D.map e)).obj Zᵢ).hom (limit.π D j) ≫
          pullback.fst Zᵢ.hom (D.map e)) ∧
      α.hom ≫ f = (Over.pullback (limit.π D j)).map g ≫ β.hom

AlgebraicGeometry.Space.eventually_eq_of_baseChange_eq_of_chartLimitsInSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationDescentUnbounded.lean, line 247. The attribute's comment: “faithfulness, with no bound on the index: the 07SD convention in place of the cardinality bounds of eventually_eq_of_baseChange_eq”.

Stacks 07SK, faithfulness, with no bound on the index. Two morphisms between algebraic spaces of finite presentation over a stage whose base changes to the limit agree already agree at a later stage.

This strengthens AlgebraicGeometry.Space.eventually_eq_of_baseChange_eq: the cardinality bounds on the index category are replaced by hconv. hconv is the convention 07SD of the chapter: the limits of the base changes of the stages to the affine objects of the site lie in the site. It is not an assumption beyond the source. It is AlgebraicGeometry.Space.SiteContainsBaseChangeLimits unfolded, and the index bounds imply it. Without it the statement is false; see the notes opening this section.

It is AlgebraicGeometry.Space.eventually_eq_of_baseChange_eq_of_siteContainsBaseChangeLimits with the convention written out.

public theorem eventually_eq_of_baseChange_eq_of_chartLimitsInSite
    (hconv : ∀ (i : I) (Z : AlgebraicGeometry.BigAffineFppf B S hS)
      (g : yoneda.obj ((AlgebraicGeometry.BigAffineFppf.inclusion B S hS).obj Z) ⟶ D.obj i)
      (W : Over i ⥤ AlgebraicGeometry.BigAffineFppf B S hS),
      (W ⋙ (AlgebraicGeometry.BigAffineFppf.inclusion B S hS ⋙ yoneda) ≅
        (Over.post (X := i) D ⋙ Over.pullback g) ⋙
          Over.forget (yoneda.obj ((AlgebraicGeometry.BigAffineFppf.inclusion B S hS).obj Z))) →
      ∀ c : Cone (((W ⋙ AlgebraicGeometry.BigAffineFppf.inclusion B S hS) ⋙
          AlgebraicGeometry.BigFppfOver.forget B S hS) ⋙ B.inclusion),
        IsLimit c → B.Contains c.pt)
    (hD : ∀ i, AlgebraicGeometry.IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.Space.IsAffineHom B S hS (D.map f))
    (hQc : ∀ i, AlgebraicGeometry.Space.IsQuasiCompactSpace B S hS (D.obj i))
    (hQs : ∀ i, AlgebraicGeometry.Space.IsAbsolutelyQuasiSeparated B S hS hZ (D.obj i))
    (i : I) (Yᵢ Zᵢ : Over (D.obj i))
    (hY : AlgebraicGeometry.IsAlgebraicSpace B S hS Yᵢ.left)
    (hZ' : AlgebraicGeometry.IsAlgebraicSpace B S hS Zᵢ.left)
    (hYfp : AlgebraicGeometry.Space.IsFinitePresentation B S hS Yᵢ.hom)
    (hZfp : AlgebraicGeometry.Space.IsFinitePresentation B S hS Zᵢ.hom)
    (f g : Yᵢ ⟶ Zᵢ)
    (hfg : (Over.pullback (limit.π D i)).map f =
      (Over.pullback (limit.π D i)).map g) :
    ∃ (j : I) (e : j ⟶ i),
      (Over.pullback (D.map e)).map f =
        (Over.pullback (D.map e)).map g

AlgebraicGeometry.Space.exists_model_of_finitePresentation_of_chartLimitsInSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationDescentUnbounded.lean, line 293. The attribute's comment: “essential surjectivity, with no bound on the index: the 07SD convention in place of the cardinality bounds of exists_model_of_finitePresentation”.

Stacks 07SK, essential surjectivity, with no bound on the index. Every algebraic space of finite presentation over the limit is the base change of an algebraic space of finite presentation over some stage.

This strengthens AlgebraicGeometry.Space.exists_model_of_finitePresentation: the cardinality bounds on the index category are replaced by hconv. hconv is the convention 07SD of the chapter: the limits of the base changes of the stages to the affine objects of the site lie in the site. It is not an assumption beyond the source. It is AlgebraicGeometry.Space.SiteContainsBaseChangeLimits unfolded, and the index bounds imply it.

It is AlgebraicGeometry.Space.exists_model_of_finitePresentation_of_siteContainsBaseChangeLimits without the hypothesis that the limit is an algebraic space, which Stacks 07SF under the convention supplies.

public theorem exists_model_of_finitePresentation_of_chartLimitsInSite
    (hconv : ∀ (i : I) (Z : AlgebraicGeometry.BigAffineFppf B S hS)
      (g : yoneda.obj ((AlgebraicGeometry.BigAffineFppf.inclusion B S hS).obj Z) ⟶ D.obj i)
      (W : Over i ⥤ AlgebraicGeometry.BigAffineFppf B S hS),
      (W ⋙ (AlgebraicGeometry.BigAffineFppf.inclusion B S hS ⋙ yoneda) ≅
        (Over.post (X := i) D ⋙ Over.pullback g) ⋙
          Over.forget (yoneda.obj ((AlgebraicGeometry.BigAffineFppf.inclusion B S hS).obj Z))) →
      ∀ c : Cone (((W ⋙ AlgebraicGeometry.BigAffineFppf.inclusion B S hS) ⋙
          AlgebraicGeometry.BigFppfOver.forget B S hS) ⋙ B.inclusion),
        IsLimit c → B.Contains c.pt)
    (hD : ∀ i, AlgebraicGeometry.IsAlgebraicSpace B S hS (D.obj i))
    (hAffine : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.Space.IsAffineHom B S hS (D.map f))
    (hQc : ∀ i, AlgebraicGeometry.Space.IsQuasiCompactSpace B S hS (D.obj i))
    (hQs : ∀ i, AlgebraicGeometry.Space.IsAbsolutelyQuasiSeparated B S hS hZ (D.obj i))
    (Y : Over (limit D))
    (hY : AlgebraicGeometry.IsAlgebraicSpace B S hS Y.left)
    (hFp : AlgebraicGeometry.Space.IsFinitePresentation B S hS Y.hom) :
    ∃ (i : I) (Yᵢ : Over (D.obj i)),
      AlgebraicGeometry.IsAlgebraicSpace B S hS Yᵢ.left ∧
        AlgebraicGeometry.Space.IsFinitePresentation B S hS Yᵢ.hom ∧
        Nonempty (Y ≅ (Over.pullback (limit.π D i)).obj Yᵢ)
Tag 07V7, a lemma

Tag 07V7 in the Stacks Project.

AlgebraicGeometry.Space.eventually_eq_of_modulePullback_limitProjection_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationModuleColimit.lean, line 392. The attribute's comment: “the faithfulness clause of the colimit assertion: two morphisms of finitely presented modules on a stage whose inverse images to the limit agree already agree at a later stage. Granted haffine, the same clause for an inverse system of affine schemes of the site, which is Stacks 01ZR(3) read on their small étale ringed sites — this tree proves Stacks 01ZR(3) only for Mathlib's Scheme.Modules on the Zariski site of opens, and the comparison with the small étale modules of the algebraic space a scheme represents is a functor with no inverse: the notes of StacksFrontier/AlgebraicGeometry/Spaces/RepresentedZariskiRestriction.lean record that neither composite is identified with an identity, that being Stacks 03DX(2), which is proved only over the essential surjectivity AlgebraicGeometry.SmallEtale.QuasicoherentIsEssImageAssociatedModule that StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleEssentialImage.lean does not have; the carried statement is about systems of affine schemes and the conclusion about systems of quasi-compact algebraic spaces, so it is not the universally quantified form of this conclusion. The essential surjectivity and fullness clauses of Stacks 07V7 are not covered: both need the equivalence QCoh(𝒪_X) = QCoh(U, R, s, t, c) of Stacks 03M3, of which this tree has only the functor in one direction”.

Stacks 07V7, the faithfulness clause of the colimit assertion. Two morphisms of finitely presented 𝒪_{X_i}-modules on a stage of the system whose inverse images along the projection of the limit agree already have equal inverse images along a transition morphism from a later stage.

The proof is the source's reduction to an affine chart. Choose a surjective étale chart f₀ : U₀ ⟶ X_i with U₀ affine, available because X_i is quasi-compact, and base change the later stages along it: this is a cofiltered system of affine schemes of the site whose limit is the chart U₀ ×_{X_i} X of the limit, so the carried affine case applies to the inverse images of the two morphisms to that chart and produces a later stage at which they agree over the corresponding chart. The chart of that stage is again surjective and étale, so the inverse image along it is faithful and the two morphisms agree over the stage itself.

theorem eventually_eq_of_modulePullback_limitProjection_eq
    (haffine : EventualModuleMapEqOverAffineSystem B S hS) (i : I)
    (hQc : IsQuasiCompactSpace B S hS (D.obj i))
    (M N : Modules.{u, u} B S hS (stageAlgebraicSpace B S hS D hD i).1
      (stageAlgebraicSpace B S hS D hD i).2)
    (hM : M.IsFinitePresentationOnSite) (hN : N.IsFinitePresentationOnSite) (φ ψ : M ⟶ N)
    (h : (modulePullback B S hS
          (limitProjection B S hS D hSize hHomSize hD hAffine i)).map φ =
        (modulePullback B S hS
          (limitProjection B S hS D hSize hHomSize hD hAffine i)).map ψ) :
    ∃ (j : I) (e : j ⟶ i),
      (modulePullback B S hS (stageTransition B S hS D hD e)).map φ =
        (modulePullback B S hS (stageTransition B S hS D hD e)).map ψ

AlgebraicGeometry.Space.finitePresentationModule_isColimit_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationModuleColimitTheorem.lean, line 168. The attribute's comment: “the category of finitely presented modules on the limit is the colimit of the categories of finitely presented modules on the stages: faithfulness, fullness through the canonical identification of iterated inverse images, and essential surjectivity of the comparison; for a given limit of the system at any cofiltered index category, under the source's own standing convention 07SD that the limits of its affine charts lie in the site; without that convention the statement fails in a size-bounded site (see the notes of ChartLimitsInSite)”.

Stacks 07V7. Let X = lim X_i be the limit of a cofiltered inverse system of quasi-compact and quasi-separated algebraic spaces over S with affine transition morphisms: an algebraic space X = c.pt with a cone c over the system that is limiting in presheaves on the big fppf site of S, whose affine charts X_j ×_{X_i} U have their limits, in schemes, inside the site (the chapter's convention, Stacks 07SD, so that the limit X is the one Stacks 07SF constructs). Then the category of finitely presented 𝒪_X-modules is the colimit of the categories of finitely presented 𝒪_{X_i}-modules: inverse image along the projections X ⟶ X_i is

  1. faithful in the colimit sense: two morphisms on a stage with equal inverse images to X have equal inverse images to a later stage;
  2. full in the colimit sense: a morphism between inverse images to X is, at a later stage, the restriction along X ⟶ X_j of a morphism between the inverse images to X_j;
  3. essentially surjective in the colimit sense: every finitely presented 𝒪_X-module is the inverse image of a finitely presented module on some stage.

The index category is any cofiltered category in the universe of the site; no size bound is imposed on it.

theorem finitePresentationModule_isColimit_of_isLimit [IsCofiltered I]
    (hAffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom B S hS (D.map f))
    (hQc : ∀ i, IsQuasiCompactSpace B S hS (D.obj i))
    (hQs : ∀ i, IsAbsolutelyQuasiSeparated B S hS hZ (D.obj i))
    (hc : IsLimit c) (hL : SiteContainsBaseChangeLimits B S hS D) :
    (∀ (i : I) (M N : Modules.{u, u} B S hS (stageAlgebraicSpace B S hS D hD i).1
        (stageAlgebraicSpace B S hS D hD i).2),
      M.IsFinitePresentationOnSite → N.IsFinitePresentationOnSite → ∀ φ ψ : M ⟶ N,
        (modulePullback B S hS (coneProjection B S hS D hD c hX i)).map φ =
          (modulePullback B S hS (coneProjection B S hS D hD c hX i)).map ψ →
        ∃ (j : I) (e : j ⟶ i),
          (modulePullback B S hS (stageTransition B S hS D hD e)).map φ =
            (modulePullback B S hS (stageTransition B S hS D hD e)).map ψ) ∧
    (∀ (i : I) (M N : Modules.{u, u} B S hS (stageAlgebraicSpace B S hS D hD i).1
        (stageAlgebraicSpace B S hS D hD i).2),
      M.IsFinitePresentationOnSite → N.IsFinitePresentationOnSite →
      ∀ φ : (modulePullback B S hS (coneProjection B S hS D hD c hX i)).obj M ⟶
        (modulePullback B S hS (coneProjection B S hS D hD c hX i)).obj N,
        ∃ (j : I) (e : j ⟶ i)
          (ψ : (modulePullback B S hS (stageTransition B S hS D hD e)).obj M ⟶
            (modulePullback B S hS (stageTransition B S hS D hD e)).obj N),
          moduleHomRestrict M N (coneProjection B S hS D hD c hX j)
            (stageTransition B S hS D hD e) (coneProjection B S hS D hD c hX i)
            (coneProjection_comp B S hS D hD c hX e) ψ = φ) ∧
    (∀ P : Modules.{u, u} B S hS c.pt hX, P.IsFinitePresentationOnSite →
        ∃ (k : I) (Q : Modules.{u, u} B S hS (stageAlgebraicSpace B S hS D hD k).1
            (stageAlgebraicSpace B S hS D hD k).2),
          Q.IsFinitePresentationOnSite ∧
            Nonempty (P ≅ (modulePullback B S hS (coneProjection B S hS D hD c hX k)).obj Q))
Tag 0D2X, a lemma

Tag 0D2X in the Stacks Project.

AlgebraicGeometry.Space.exists_isFiniteLocallyFreeOnSite_stage_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FiniteLocallyFreeStageModel.lean, line 89. The attribute's comment: “(1)”.

Stacks 0D2X, part (1). Let X = lim Xᵢ be the limit of a cofiltered system of quasi-compact and quasi-separated algebraic spaces over S with affine transition morphisms, as in Stacks 07SK. Every finite locally free 𝒪_X-module is the pullback of a finite locally free 𝒪_{Xᵢ}-module for some i.

theorem exists_isFiniteLocallyFreeOnSite_stage_model
    (F : Modules.{u, u} B S hS
      (limitAlgebraicSpace B S hS D hSize hHomSize hD hAffine).1
      (limitAlgebraicSpace B S hS D hSize hHomSize hD hAffine).2)
    (hF : SheafOfModules.IsFiniteLocallyFreeOnSite F) :
    ∃ (i : I) (Fᵢ : Modules.{u, u} B S hS (stageAlgebraicSpace B S hS D hD i).1
        (stageAlgebraicSpace B S hS D hD i).2),
      SheafOfModules.IsFiniteLocallyFreeOnSite Fᵢ ∧
        Nonempty (F ≅ (modulePullback B S hS
          (limitProjection B S hS D hSize hHomSize hD hAffine i)).obj Fᵢ)

AlgebraicGeometry.Space.exists_isInvertibleModule_stage_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FiniteLocallyFreeStageModel.lean, line 111. The attribute's comment: “(2)”.

Stacks 0D2X, part (2). Let X = lim Xᵢ be the limit of a cofiltered system of quasi-compact and quasi-separated algebraic spaces over S with affine transition morphisms, as in Stacks 07SK. Every invertible 𝒪_X-module is the pullback of an invertible 𝒪_{Xᵢ}-module for some i.

theorem exists_isInvertibleModule_stage_model
    (L : Modules.{u, u} B S hS
      (limitAlgebraicSpace B S hS D hSize hHomSize hD hAffine).1
      (limitAlgebraicSpace B S hS D hSize hHomSize hD hAffine).2)
    (hL : IsInvertibleModule (limitAlgebraicSpace B S hS D hSize hHomSize hD hAffine) L) :
    ∃ (i : I) (Lᵢ : Modules.{u, u} B S hS (stageAlgebraicSpace B S hS D hD i).1
        (stageAlgebraicSpace B S hS D hD i).2),
      IsInvertibleModule (stageAlgebraicSpace B S hS D hD i) Lᵢ ∧
        Nonempty (L ≅ (modulePullback B S hS
          (limitProjection B S hS D hSize hHomSize hD hAffine i)).obj Lᵢ)
Sources
LeanAlgebraicGeometry.Space.exists_morphism_after_baseChange · AlgebraicGeometry.Space.eventually_eq_of_baseChange_eq · AlgebraicGeometry.Space.exists_model_of_finitePresentation · AlgebraicGeometry.Space.exists_morphism_after_baseChange_of_chartLimitsInSite · AlgebraicGeometry.Space.eventually_eq_of_baseChange_eq_of_chartLimitsInSite · AlgebraicGeometry.Space.exists_model_of_finitePresentation_of_chartLimitsInSite · AlgebraicGeometry.Space.eventually_eq_of_modulePullback_limitProjection_eq · AlgebraicGeometry.Space.finitePresentationModule_isColimit_of_isLimit

Section70.8 Absolute Noetherian approximation#

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

Tag 07SU, a proposition

Tag 07SU in the Stacks Project.

AlgebraicGeometry.Space.hasNoetherianApproximation_of_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AbsoluteNoetherianApproximation/Main.lean, line 453.

Absolute Noetherian approximation. Let X be a quasi-compact and quasi-separated algebraic space over Spec ℤ, the terminal scheme ⊤_ Scheme, on the big fppf site B. Then there are a directed set I and an inverse system (X_i) of algebraic spaces over I such that (1) the transition morphisms are affine, (2) each X_i is quasi-separated and of finite type over ℤ, and (3) X = lim X_i, the limit being taken in presheaves on the site.

theorem hasNoetherianApproximation_of_isQuasiCompactSpace
    {X : (BigFppfOver B (⊤_ Scheme.{u}) hZ)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (⊤_ Scheme.{u}) hZ X)
    (hqc : IsQuasiCompactSpace B (⊤_ Scheme.{u}) hZ X)
    (hqs : IsAbsolutelyQuasiSeparated B (⊤_ Scheme.{u}) hZ hZ X) :
    HasNoetherianApproximation B (⊤_ Scheme.{u}) hZ hZ X

AlgebraicGeometry.Space.hasNoetherianApproximation_of_isomorphicPresentation_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianApproximationFromPresentation.lean, line 160. The attribute's comment: “granted the Conrad–Lieblich–Olsson construction's output as the general hypothesis hCLO, strengthened by the two cardinality conditions on the index set that make the limit an algebraic space and without which the statement is false”.

Stacks 07SU. Let X be a quasi-compact and quasi-separated algebraic space over S. Then there are a directed set I and an inverse system of algebraic spaces (X_i, f_{ii'}) over I whose transition morphisms are affine, whose stages are quasi-separated and of finite type over Spec ℤ, and whose limit is X.

The tag's own hypotheses — X an algebraic space, quasi-compact and quasi-separated — are the hypotheses here, and the conclusion is the full conclusion of the tag, in the interface AlgebraicGeometry.Space.HasNoetherianApproximation of StacksFrontier/AlgebraicGeometry/Spaces/NoetherianApproximation.lean. What is granted is the single general hypothesis hCLO, the output of the Conrad–Lieblich–Olsson construction, which is quantified over its own algebraic space and does not mention X; see the module documentation for what it carries and for why it is not this conclusion pre-instantiated. It supplies the two cardinality conditions on the index set that Stacks 07SF, existence needs, and which a statement of Stacks 07SU that omits them does not have; that is the correction recorded below.

Proved from it: the limit of the system is an algebraic space (Stacks 07SF, existence), it is its own Noetherian approximation (AlgebraicGeometry.Space.noetherianApproximationLimit), and X is isomorphic to it, which is the step the source's proof ends with (Stacks 0262, as AlgebraicGeometry.Space.exists_iso_of_isomorphic_presentations).

theorem hasNoetherianApproximation_of_isomorphicPresentation_limit
    (hCLO : ∀ Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u, IsAlgebraicSpace B S hS Z →
      IsQuasiCompactSpace B S hS Z → IsAbsolutelyQuasiSeparated B S hS hZ Z →
        ∃ (I : Type u) (inst : Preorder I),
          let _ := inst
          ∃ (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
            (D : Iᵒᵖ ⥤ (BigFppfOver B S hS)ᵒᵖ ⥤ Type u),
            #I < B.cutoff.ord.cof ∧
            (∀ i j : I, #(i ⟶ j) < B.cutoff.ord.cof) ∧
            (∀ j, IsAlgebraicSpace B S hS (D.obj j)) ∧
            (∀ {j j' : Iᵒᵖ} (g : j ⟶ j'), IsAffineHom B S hS (D.map g)) ∧
            (∀ j, IsAbsolutelyQuasiSeparated B S hS hZ (D.obj j)) ∧
            (∀ j, IsFiniteType B (⊤_ Scheme.{u}) hZ
              (terminal.from (viewOverIntegers B S hS hZ (D.obj j)))) ∧
            ∃ (R R' U : BigFppfOver B S hS) (s t : R ⟶ U) (s' t' : R' ⟶ U)
              (a : yoneda.obj U ⟶ Z) (a' : yoneda.obj U ⟶ limit D) (e : R ≅ R'),
              IsPullback (yoneda.map s) (yoneda.map t) a a ∧
              IsPullback (yoneda.map s') (yoneda.map t') a' a' ∧
              e.hom ≫ s' = s ∧ e.hom ≫ t' = t ∧
              (MorphismProperty.presheaf (MorphismProperty.inverseImage
                (@Surjective.{u} : MorphismProperty Scheme.{u})
                (BigFppfOver.toScheme B S hS))) a ∧
              (MorphismProperty.presheaf (MorphismProperty.inverseImage
                (@Etale.{u} : MorphismProperty Scheme.{u})
                (BigFppfOver.toScheme B S hS))) a ∧
              (MorphismProperty.presheaf (MorphismProperty.inverseImage
                (@Surjective.{u} : MorphismProperty Scheme.{u})
                (BigFppfOver.toScheme B S hS))) a' ∧
              (MorphismProperty.presheaf (MorphismProperty.inverseImage
                (@Etale.{u} : MorphismProperty Scheme.{u})
                (BigFppfOver.toScheme B S hS))) a')
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hqc : IsQuasiCompactSpace B S hS X)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X) :
    HasNoetherianApproximation B S hS hZ X
Tag 07SV, an equation

Tag 07SV in the Stacks Project.

AlgebraicGeometry.isPullback_gluedRelationSource_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GluedEtaleRelationTransition.lean, line 303. The attribute's comment: “the displayed square is cartesian, for any base-changed fibre square over W”.

Stacks Project, Tag 07SV. The displayed square of the proof of absolute Noetherian approximation, in the form in which the proof establishes it.

The data: a morphism v : V ⟶ V', open subschemes j : W ⟶ V and j' : W' ⟶ V' with W the inverse image of W', that is with hj cartesian; objects Q, Q' with sections d, d' of projections p, p' — in the application Q = W ×_U W, Q' = W' ×_{U'} W', p and p' are the first projections and d, d' the diagonals — such that Q is the base change of Q' along k, that is with hQ cartesian; and the relations R, R' obtained by glueing V to Q along W and V' to Q' along W', with source maps s, s' which are the identity on the chart V, resp. V', and p, resp. p', followed by the open immersion on the other chart. Then for the morphism r : R ⟶ R' induced by v and q the square

R  --r-->  R'
|          |
s          s'
v          v
V  --v-->  V'

is cartesian. Nothing is assumed about the base over which Q and Q' are fibre products, so this applies verbatim when that base is an algebraic space, as it is in the source.

theorem isPullback_gluedRelationSource_of_isPullback
    {v : V ⟶ V'} {k : W ⟶ W'} {j : W ⟶ V} {j' : W' ⟶ V'} [IsOpenImmersion j']
    {p : Q ⟶ W} {p' : Q' ⟶ W'} {d : W ⟶ Q} {d' : W' ⟶ Q'} [IsOpenImmersion d']
    {q : Q ⟶ Q'} (hj : IsPullback k j j' v) (hQ : IsPullback q p p' k)
    (hd : d ≫ p = 𝟙 W) (hdq : d ≫ q = k ≫ d')
    {a : V ⟶ R} {b : Q ⟶ R} {a' : V' ⟶ R'} {b' : Q' ⟶ R'}
    (hR : IsPushout j d a b) (hR' : IsPushout j' d' a' b')
    {s : R ⟶ V} (hsa : a ≫ s = 𝟙 V) (hsb : b ≫ s = p ≫ j)
    {s' : R' ⟶ V'} (hsa' : a' ≫ s' = 𝟙 V') (hsb' : b' ≫ s' = p' ≫ j')
    {r : R ⟶ R'} (hra : a ≫ r = v ≫ a') (hrb : b ≫ r = q ≫ b') :
    IsPullback r s s' v

AlgebraicGeometry.isPullback_gluedRelationSource, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GluedEtaleRelationTransition.lean, line 378. The attribute's comment: “the displayed square for R_i glued from V_i and W_i x_{U_i} W_i is cartesian”.

Stacks Project, Tag 07SV. The displayed square of the proof of absolute Noetherian approximation, written out for the construction the source performs. Let w' : W' ⟶ U' be étale, let u : U ⟶ U' be arbitrary, and let W = W' ×_{U'} U. Let j' : W' ⟶ V' and j : W ⟶ V be open immersions with W the inverse image of W', that is with hj cartesian. Let R be obtained by glueing V to W ×_U W along the diagonal copy of W, and R' likewise at the primed stage, and let s, s' be the source maps: the identity on the chart V, resp. V', and the first projection on the chart W ×_U W, resp. W' ×_{U'} W'. If r : R ⟶ R' is the morphism induced by v on the glueings, then the square formed by r, s, s' and v is cartesian.

theorem isPullback_gluedRelationSource {u : U ⟶ U'} {v : V ⟶ V'} {w' : W' ⟶ U'} [Etale w']
    {j' : W' ⟶ V'} [IsOpenImmersion j'] {j : pullback w' u ⟶ V}
    (hj : IsPullback (pullback.fst w' u) j j' v)
    {a : V ⟶ R} {b : pullback (pullback.snd w' u) (pullback.snd w' u) ⟶ R}
    {a' : V' ⟶ R'} {b' : pullback w' w' ⟶ R'}
    (hR : IsPushout j (pullback.diagonal (pullback.snd w' u)) a b)
    (hR' : IsPushout j' (pullback.diagonal w') a' b')
    {s : R ⟶ V} (hsa : a ≫ s = 𝟙 V)
    (hsb : b ≫ s = pullback.fst (pullback.snd w' u) (pullback.snd w' u) ≫ j)
    {s' : R' ⟶ V'} (hsa' : a' ≫ s' = 𝟙 V') (hsb' : b' ≫ s' = pullback.fst w' w' ≫ j')
    {r : R ⟶ R'} (hra : a ≫ r = v ≫ a')
    (hrb : b ≫ r = etaleRelationTransition w' u ≫ b') :
    IsPullback r s s' v
Sources
LeanAlgebraicGeometry.Space.hasNoetherianApproximation_of_isQuasiCompactSpace · AlgebraicGeometry.Space.hasNoetherianApproximation_of_isomorphicPresentation_limit · AlgebraicGeometry.isPullback_gluedRelationSource_of_isPullback · AlgebraicGeometry.isPullback_gluedRelationSource

Section70.9 Applications#

Section 70.9 of the Stacks Project, Tag 07V8. 8 tags here are carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07V9, a lemma

Tag 07V9 in the Stacks Project.

AlgebraicGeometry.Space.exists_isFilteredColimit_isFinitePresentationOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentationGeneration/Main.lean, line 108. The attribute's comment: “with a small filtered index category and finite presentation in the on-site rendering of Stacks 03DL(7)”.

Stacks 07V9. Let X be a quasi-compact and quasi-separated algebraic space over a scheme S. Then every quasi-coherent 𝒪_X-module F is a filtered colimit of 𝒪_X-modules of finite presentation: there is a small filtered category I, a diagram D of 𝒪_X-modules of finite presentation indexed by it and a colimit cocone on D with vertex F.

The hypotheses are the source's. The proof does not use absolute Noetherian approximation; it follows the route the source indicates, through the filtration of Decent Spaces, Lemma 07ST, in the form of the induction principle of Stacks 08GP.

theorem exists_isFilteredColimit_isFinitePresentationOnSite
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hqc : IsQuasiCompactSpace B S hS X) (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X)
    (F : Modules.{u, u} B S hS X hX) (hF : F.IsQuasicoherentOnSite) :
    ∃ (I : Type u) (inst : SmallCategory I),
      let _ := inst
      ∃ (_ : IsFiltered I) (D : I ⥤ Modules.{u, u} B S hS X hX)
        (φ : D ⟶ (Functor.const I).obj F),
        (∀ i, (D.obj i).IsFinitePresentationOnSite) ∧ Nonempty (IsColimit (Cocone.mk F φ))

AlgebraicGeometry.Space.exists_isFilteredColimit_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentationGeneration/Main.lean, line 126. The attribute's comment: “in the rendering by Mathlib's finite presentation predicate”.

Stacks 07V9, in the conclusion shape of the conditional statement AlgebraicGeometry.Space.isFilteredColimit_isFinitePresentation_of_isQuasiCompactSpace (an index category with objects in Type (u + 1) and morphisms in Type u, finite presentation in the sense of Mathlib's SheafOfModules.IsFinitePresentation), with none of its carried inputs.

theorem exists_isFilteredColimit_isFinitePresentation
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hqc : IsQuasiCompactSpace B S hS X) (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X)
    (F : Modules.{u, u} B S hS X hX) (hF : F.IsQuasicoherentOnSite) :
    ∃ (K : Type (u + 1)) (inst : Category.{u} K),
      let _ := inst
      ∃ (_ : IsFiltered K) (D : K ⥤ Modules.{u, u} B S hS X hX)
        (φ : D ⟶ (Functor.const K).obj F),
        (∀ k, (D.obj k).IsFinitePresentation) ∧ Nonempty (IsColimit (Cocone.mk F φ))
Tag 0829, a lemma

Tag 0829 in the Stacks Project.

AlgebraicGeometry.Space.finiteTypeQuasicoherentSubobject_isFiltered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeQuasicoherentSubobjects.lean, line 483. The attribute's comment: “the directedness clause, for an arbitrary quasi-coherent module on an arbitrary algebraic space”.

The finite type quasi-coherent submodules of a quasi-coherent module form a directed system.

theorem finiteTypeQuasicoherentSubobject_isFiltered
    (F : Modules.{u, u} B S hS X hX) [F.IsQuasicoherentOnSite] :
    IsFiltered (FiniteTypeQuasicoherentSubobject B S hS X hX F)

AlgebraicGeometry.Space.isFiltered_finiteTypeQuasicoherentSubobject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeQuasicoherentSubobjectsDirected.lean, line 76. The attribute's comment: “directedness, for an arbitrary algebraic space”. References: SGA 3 VIB (11.10), “partial”.

The directedness assertion of Stacks 0829. The quasi-coherent submodules of finite type of a quasi-coherent 𝒪_F-module form a directed system: the image in the module of the direct sum of two of them is a quasi-coherent submodule of finite type containing both.

Stacks 0829 states this for a quasi-compact and quasi-separated algebraic space; those two hypotheses enter only its colimit assertion, through Stacks 07V9, so the statement here is for an arbitrary algebraic space.

theorem isFiltered_finiteTypeQuasicoherentSubobject (G : Modules.{u, u} B S hS F hF)
    [G.IsQuasicoherentOnSite] :
    IsFiltered (FiniteTypeQuasicoherentSubobject B S hS F hF G)

AlgebraicGeometry.Space.nonempty_isColimit_finiteTypeQuasicoherentSubobjectCocone_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeQuasicoherentSubobjectsQcqs.lean, line 98. The attribute's comment: “the colimit clause”.

Stacks 0829, the colimit assertion. Let X be a quasi-compact and quasi-separated algebraic space over a scheme S and let F be a quasi-coherent 𝒪_X-module. Then F is the colimit of the canonical diagram of its finite type quasi-coherent submodules.

The diagram is directed by AlgebraicGeometry.Space.isFiltered_finiteTypeQuasicoherentSubobject, which together with this declaration covers the whole of Stacks 0829.

theorem nonempty_isColimit_finiteTypeQuasicoherentSubobjectCocone_of_qcqs
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hZ : B.Contains (⊤_ Scheme.{u})) (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) (hqc : IsQuasiCompactSpace B S hS X)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X)
    (F : Modules.{u, u} B S hS X hX) [F.IsQuasicoherentOnSite] :
    Nonempty (IsColimit (finiteTypeQuasicoherentSubobjectCocone B S hS X hX F))

AlgebraicGeometry.Space.isFiltered_and_nonempty_isColimit_finiteTypeQuasicoherentSubobjectCocone_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeSubmoduleQcqs.lean, line 350. References: SGA 3 VIB (11.10), “more general”.

Stacks 0829. On a quasi-compact quasi-separated algebraic space X, a quasi-coherent 𝒪_X-module F is the directed colimit of its quasi-coherent submodules of finite type: the category AlgebraicGeometry.Space.FiniteTypeQuasicoherentSubobject of those submodules is filtered and their canonical cocone with point F is a colimit cocone.

Directedness is AlgebraicGeometry.Space.finiteTypeQuasicoherentSubobject_isFiltered, which uses Descent 03DX(2) and the cokernel clause of Stacks 03M1, that is AlgebraicGeometry.Space.isQuasicoherentOnSite_iff_isCartesianOnAffineCharts and AlgebraicGeometry.Space.isClosedUnderCokernels_quasicoherentSheaves. For the colimit, the supremum of the submodules is ⊤: its inclusion is surjective on sections over affine charts, every section there lying in one of them by AlgebraicGeometry.Space.exists_isFiniteType_submodule_mem_of_qcqs.

theorem isFiltered_and_nonempty_isColimit_finiteTypeQuasicoherentSubobjectCocone_of_qcqs
    (hZ : B.Contains (⊤_ Scheme.{u})) (X : AlgebraicSpaces B S hS)
    (hqc : IsQuasiCompactSpace B S hS X.1) (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (F : Modules.{u, u} B S hS X.1 X.2) [hF : F.IsQuasicoherentOnSite] :
    IsFiltered (FiniteTypeQuasicoherentSubobject B S hS X.1 X.2 F) ∧
      Nonempty (IsColimit (finiteTypeQuasicoherentSubobjectCocone B S hS X.1 X.2 F))
Tag 086Y, a lemma

Tag 086Y in the Stacks Project.

AlgebraicGeometry.Space.exists_directed_isFinitePresentation_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentationGeneration/Main.lean, line 146.

Stacks 086Y. Let X be a quasi-compact and quasi-separated algebraic space over a scheme S and let M be a finite type quasi-coherent 𝒪_X-module. Then M is the colimit of a system of 𝒪_X-modules of finite presentation indexed by a directed poset, all of whose transition maps are surjective.

The source writes ℱ = lim ℱ_i, but its proof produces colim 𝒢_i/𝒦_a; the conclusion is a colimit, as in the scheme-level counterpart Stacks 086M.

theorem exists_directed_isFinitePresentation_epi
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hqc : IsQuasiCompactSpace B S hS X) (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X)
    (M : Modules.{u, u} B S hS X hX) [M.IsQuasicoherentOnSite] [M.IsFiniteTypeOnSite] :
    ∃ (I : Type (u + 1)) (_ : PartialOrder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (D : I ⥤ Modules.{u, u} B S hS X hX) (φ : D ⟶ (Functor.const I).obj M)
      (_ : IsColimit (Cocone.mk M φ)),
      (∀ i, (D.obj i).IsFinitePresentationOnSite) ∧
        ∀ (i j : I) (h : i ≤ j), Epi (D.map (homOfLE h))
Tag 082A, a lemma

Tag 082A in the Stacks Project.

AlgebraicGeometry.Space.exists_directed_isFinitePresentation_algebra_of_idealQuotients, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/IdealQuotientApproximationSystem.lean, line 229. The attribute's comment: “PARTIAL, but the construction and not the reindexing: the members A_{i,j} = B_i/I_{i,j} of the source's system and the morphisms between them are constructed here, as quotients of an algebra sheaf on an algebraic space by a sheaf of ideals and factorizations through them, which is the object whose absence was the recorded obstruction. Three inputs are carried, each separately identified. (1) The system datum D, psi -- in the source B_i = Sym(F_i) with the maps induced by Stacks 07V9 -- because at the algebraic space level this tree has the symmetric algebra of a module but neither its functoriality in the module nor the ungraded universal property giving Sym(F_i) to A, both of which exist only for schemes (AlgebraicGeometry.Scheme.Modules.symmetricAlgebraSheafMap, Stacks.SymAlgSheaf.algebraLift), nor quasi-coherence of Sym. (2) Quasi-coherence and finite presentation of each stage, which are conditions on the sections of a sheafification over the affine etale charts; this is where the source's finite generation of I_{i,j} is used, so the ideals here are arbitrary. (3) The colimit property of the constructed cocone, colimits in AlgebraicGeometry.Space.AlgebraSheaf being constructed nowhere in this tree. The source's quasi-compactness and quasi-separatedness are absent because they are used only to produce the system datum, which is hypothesis (1)”.

Stacks Project, Tag 082A, over the system datum. Let S be a scheme, X an algebraic space over S and 𝒜 an 𝒪_X-algebra. Let D be a filtered system of 𝒪_X-algebras with a cocone ψ over 𝒜, and for each i let ℐ_i be a sheaf of ideals of D_i killed by ψ_i and carried into ℐ_j by every transition map. If every quotient D_i/ℐ_i is quasi-coherent of finite presentation and the constructed cocone of those quotients over 𝒜 is colimiting, then 𝒜 is the colimit of a system of quasi-coherent 𝒪_X-algebras of finite presentation indexed by a directed poset.

The members of the system and the morphisms between them are constructed: they are AlgebraicGeometry.Space.idealQuotientSystem and AlgebraicGeometry.Space.idealQuotientSystemCocone, built from the quotient of an algebra sheaf by a sheaf of ideals and its universal property. See the module documentation for what each of the three hypotheses is and why it is a separate missing ingredient rather than the conclusion.

theorem exists_directed_isFinitePresentation_algebra_of_idealQuotients [IsFiltered P]
    (hstage : ∀ p : P, ((D.obj p).idealQuotient (I p)).IsQuasicoherent ∧
      ((D.obj p).idealQuotient (I p)).IsFinitePresentation)
    (hcol : IsColimit (Cocone.mk A (idealQuotientSystemCocone A D ψ I hkill hmap))) :
    ∃ (J : Type u) (_ : PartialOrder J) (_ : Nonempty J) (_ : IsDirected J (· ≤ ·))
      (E : J ⥤ AlgebraSheaf.{u, u} B S hS X hX) (φ : E ⟶ (Functor.const J).obj A)
      (_ : IsColimit (Cocone.mk A φ)),
      ∀ j, (E.obj j).IsQuasicoherent ∧ (E.obj j).IsFinitePresentation

AlgebraicGeometry.Space.exists_directed_isFinitePresentation_algebra_of_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/QuasicoherentAlgebraFinitePresentationColimitQcqs.lean, line 61. The attribute's comment: “a quasi-coherent algebra on a quasi-compact quasi-separated algebraic space is the colimit, among all algebra sheaves, of a system of quasi-coherent algebras of finite presentation indexed by a nonempty directed poset”.

Let S be a scheme, X a quasi-compact and quasi-separated algebraic space over S and 𝒜 a quasi-coherent 𝒪_X-algebra. Then 𝒜 is the colimit, in the category of all 𝒪_X-algebras, of a system of quasi-coherent 𝒪_X-algebras of finite presentation indexed by a nonempty directed partially ordered set. The colimit is taken in AlgebraicGeometry.Space.AlgebraSheaf, which is stronger than in the full subcategory of the quasi-coherent algebras.

theorem exists_directed_isFinitePresentation_algebra_of_isQuasiCompactSpace
    (X : AlgebraicSpaces B S hS) (hqc : IsQuasiCompactSpace B S hS X.1)
    (hqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X.1)
    (A : AlgebraSheaf.{u, u} B S hS X.1 X.2) (hA : A.IsQuasicoherent) :
    ∃ (J : Type u) (_ : PartialOrder J) (_ : Nonempty J) (_ : IsDirected J (· ≤ ·))
      (E : J ⥤ AlgebraSheaf.{u, u} B S hS X.1 X.2) (ψ : E ⟶ (Functor.const J).obj A)
      (_ : IsColimit (Cocone.mk A ψ)),
      ∀ j, (E.obj j).IsQuasicoherent ∧ (E.obj j).IsFinitePresentation
Tag 082B, a lemma

Tag 082B in the Stacks Project.

AlgebraicGeometry.Space.isFiltered_and_isColimit_finiteTypeSubalgebraCocone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeSubalgebraColimit.lean, line 480.

Stacks 082B. Let S be a scheme, X a quasi-compact and quasi-separated algebraic space over S and 𝒜 a quasi-coherent 𝒪_X-algebra. Then 𝒜 is the directed colimit of its finite type quasi-coherent 𝒪_X-subalgebras: they form a filtered category, and the cocone of their inclusions into 𝒜 is a colimit cocone.

Directedness is AlgebraicGeometry.Space.isFiltered_finiteTypeSubalgebra. The cocone is a colimit because its legs are injective on sections and, by AlgebraicGeometry.Space.exists_finiteTypeSubalgebra_section, jointly surjective on the sections over affine étale charts.

theorem isFiltered_and_isColimit_finiteTypeSubalgebraCocone (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS) (hqc : IsQuasiCompactSpace B S hS X.1)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1) (A : AlgebraSheaf.{u, u} B S hS X.1 X.2)
    (hA : A.IsQuasicoherent) :
    IsFiltered (FiniteTypeSubalgebra B S hS X.1 X.2 A) ∧
      Nonempty (IsColimit (finiteTypeSubalgebraCocone B S hS X.1 X.2 A))

AlgebraicGeometry.Space.isFiltered_finiteTypeSubalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SubalgebraJoinFiniteType.lean, line 403. The attribute's comment: “the directedness assertion; the colimit assertion is blocked on Stacks 07SU through 0829 and 07V9 by the source's own route”.

The finite type quasi-coherent subalgebras of a quasi-coherent sheaf of 𝒪_Y-algebras on an algebraic space form a filtered category, with no hypothesis beyond quasi-coherence of the algebra.

Nonemptiness is the image of the canonical morphism from the structure sheaf, and upper bounds are the subalgebras generated by two subalgebras.

theorem isFiltered_finiteTypeSubalgebra (Y : AlgebraicSpaces B S hS)
    (A : AlgebraSheaf.{u, u} B S hS Y.1 Y.2) (hA : A.IsQuasicoherent) :
    IsFiltered (FiniteTypeSubalgebra B S hS Y.1 Y.2 A)
Tag 086Z, a lemma

Tag 086Z in the Stacks Project.

AlgebraicGeometry.Space.exists_directed_isFinite_isFinitePresentation_locallySurjective_of_elementaryData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/AlgebraSheafIdealQuotientColimit.lean, line 729. The attribute's comment: “the same conclusion as AlgebraicGeometry.Space.exists_directed_isFinite_isFinitePresentation_locallySurjective — the directedness of the index, the finiteness and the finite presentation of every stage, the surjectivity of every transition map and the colimit — but over an ELEMENTARY carried input in place of that theorem's hsource. THIS REGISTRATION IS FORMALLY WEAKER THAN THAT ONE AND DOES NOT REPLACE IT: the carried input here is strictly stronger, so the unrestricted reading of the tag remains the one carried there. What this registration claims is that the three non-elementary conjuncts of hsource — quasi-coherence of every quotient B/I_j, finite presentation of every quotient B/I_j, and the colimit property of the constructed cocone — are each DERIVABLE, and it derives them: quasi-coherence from quasi-coherence of B and of I_j by AlgebraicGeometry.Space.AlgebraSheaf.isQuasicoherent_idealQuotient, finite presentation from finite presentation of B and finite generation of the ideal of sections I_j(W) over each affine etale chart by AlgebraicGeometry.Space.AlgebraSheaf.isFinitePresentation_idealQuotient, and the colimit from local surjectivity of f together with local membership in the family of every section f kills by AlgebraicGeometry.Space.nonempty_isColimit_idealQuotientQcohCocone_of_locally. Every conjunct that remains carried is a condition on sections of B, of the I_j and of A over the objects of the small etale site, or on a single affine etale chart. STILL CARRIED, and NOT dischargeable in this tree today: (i) quasi-coherence of AlgebraicGeometry.Space.symmetricAlgebraSheaf for a quasi-coherent module, which is the B of the source and is recorded as absent in StacksFrontier.AlgebraicGeometry.Spaces.SymmetricAlgebraSheafMap (Stacks 01CK/01CL hold for a ringed space, as Stacks.SheafOfModules.isQuasicoherent_symmetricAlgebraSheaf_of_isQuasicoherent, but not for the small etale site of an algebraic space); (ii) finite presentation of that same Sym(F), the sections of which over a chart are only LOCALLY finite sums of homogeneous ones; (iii) integrality at one index, the fourth step of the source. Note also that Stacks 086Y, AlgebraicGeometry.Space.exists_directed_isFinitePresentation_epi_of_isFiniteType, is itself proved only over three carried inputs h07V9, hstage and hcoker, so Stacks 086Z is NOT unconditional in this tree by this route or any other presently available”.

Stacks Project, Tag 086Z, over elementary data about ℬ and the family of ideals. Same conclusion as AlgebraicGeometry.Space.exists_directed_isFinite_isFinitePresentation_locallySurjective: A is the colimit of a system of quasi-coherent 𝒪_Y-algebras over a nonempty directed preorder, every member finite and of finite presentation and every transition map locally surjective.

The carried input no longer mentions the quotients ℬ/ℐ_j except at the single index where integrality is asked. It asks instead: ℬ quasi-coherent and of finite presentation, each ℐ_j quasi-coherent as an 𝒪_Y-module with finitely generated ideal of sections over each affine étale chart, f locally surjective, and every section of ℬ which f kills locally a section of some ℐ_j. Those are the data of the first three steps of the source's proof and nothing more.

See the section documentation above: this is a formally weaker statement than the theorem it calls, deliberately, and it does not make Stacks 086Z unconditional.

theorem exists_directed_isFinite_isFinitePresentation_locallySurjective_of_elementaryData
    (A : QuasicoherentAlgebra B S hS Y)
    (hqc : IsQuasiCompactSpace B S hS Y.obj)
    (hqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.obj)
    (hA : A.obj.IsFinite)
    (hdata :
      IsQuasiCompactSpace B S hS Y.obj →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.obj →
      A.obj.IsFinite →
        ∃ (ℬ : AlgebraSheaf.{u, u} B S hS Y.1 Y.2) (f : ℬ ⟶ A.obj) (J : Type u)
          (inst : SmallCategory J),
          let _ := inst
          ∃ (_ : IsFiltered J) (ι : J → ℬ.IdealSheaf)
            (_ : ∀ j j' : J, (j ⟶ j') → ι j ≤ ι j'),
            (∀ (j : J) (U : (SmallEtale B S hS Y.1)ᵒᵖ) (a : ℬ.right.obj.obj U),
                a ∈ (ι j).obj U → (f.right.hom.app U).hom a = 0) ∧
              ℬ.IsQuasicoherent ∧ ℬ.IsFinitePresentation ∧
              (∀ j, (AlgebraSheaf.idealModule ℬ (ι j)).IsQuasicoherentOnSite) ∧
              (∀ (j : J) (W : SmallEtale B S hS Y.1),
                IsAffine ((SmallEtale.toOver B S hS Y.1 ⋙ BigFppfOver.toScheme B S hS).obj W) →
                  (Stacks.Sites.sectionIdeal (ι j) (op W)).FG) ∧
              Presheaf.IsLocallySurjective (SmallEtale.topology B S hS Y.1) f.right.hom ∧
              (∀ (U : (SmallEtale B S hS Y.1)ᵒᵖ) (a : ℬ.right.obj.obj U),
                  (f.right.hom.app U).hom a = 0 →
                    Stacks.Sites.memSieve (O := ℬ.right) ι a ∈
                      SmallEtale.topology B S hS Y.1 U.unop) ∧
              ∃ j, (ℬ.idealQuotient (ι j)).IsIntegral) :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (D : I ⥤ QuasicoherentAlgebra B S hS Y) (φ : D ⟶ (Functor.const I).obj A),
      Nonempty (IsColimit (Cocone.mk A φ)) ∧
      (∀ i, (D.obj i).obj.IsFinite ∧ (D.obj i).obj.IsFinitePresentation) ∧
      ∀ i j (h : i ≤ j), Presheaf.IsLocallySurjective
        (SmallEtale.topology B S hS Y.obj) (D.map (homOfLE h)).hom.right.hom

AlgebraicGeometry.Space.exists_directed_isFinite_isFinitePresentation_locallySurjective_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FiniteAlgebraFinitePresentationColimitQcqs.lean, line 57.

Stacks Project, Tag 086Z. Let S be a scheme, let Y be a quasi-compact and quasi-separated algebraic space over S and let 𝒜 be a finite quasi-coherent 𝒪_Y-algebra. Then 𝒜 is the colimit of a system of quasi-coherent 𝒪_Y-algebras indexed by a nonempty directed preorder, every member of which is finite and of finite presentation, and every transition map of which is surjective (locally surjective as a morphism of sheaves on the small étale site, which for quasi-coherent algebras is surjectivity on the sections over every affine étale chart).

The proof is the source's. Stacks 086Y gives a quasi-coherent module 𝒢 of finite presentation with an epimorphism 𝒢 ⟶ 𝒜; then AlgebraicGeometry.Space.exists_directed_isFinite_isFinitePresentation_locallySurjective_of_epi forms Sym(𝒢), writes the kernel of Sym(𝒢) ⟶ 𝒜 as the union of its finite type quasi-coherent submodules ℰ (Stacks 0829), takes the quotients Sym(𝒢)/(ℰ), shows they are finite for ℰ large, and reindexes by a directed preorder.

theorem exists_directed_isFinite_isFinitePresentation_locallySurjective_of_isFinite
    (Y : AlgebraicSpaces B S hS) (A : QuasicoherentAlgebra B S hS Y)
    (hqc : IsQuasiCompactSpace B S hS Y.obj)
    (hqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.obj)
    (hA : A.obj.IsFinite) :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (D : I ⥤ QuasicoherentAlgebra B S hS Y) (φ : D ⟶ (Functor.const I).obj A),
      Nonempty (IsColimit (Cocone.mk A φ)) ∧
      (∀ i, (D.obj i).obj.IsFinite ∧ (D.obj i).obj.IsFinitePresentation) ∧
      ∀ i j (h : i ≤ j), Presheaf.IsLocallySurjective
        (SmallEtale.topology B S hS Y.obj) (D.map (homOfLE h)).hom.right.hom

AlgebraicGeometry.Space.exists_directed_isFinite_isFinitePresentation_locallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FiniteAlgebraSurjectiveSystem.lean, line 471. The attribute's comment: “the directedness of the index, the finiteness of every stage, the finite presentation of every stage and the surjectivity of every transition map, over the carried input hsource. hsource is the DATA the first three steps of the source's proof produce, not the system they build: one algebra sheaf B (in the source Sym(F) for the finitely presented module F of Stacks 086Y), a map B to the algebra, and a FILTERED family of sheaves of ideals of B killed by that map and growing along the index (in the source the finite type submodules of the kernel ideal, Stacks 0829), plus quasi-coherence and finite presentation of each quotient B/I_j, the colimit property of the constructed cocone, and integrality — not finiteness — at ONE index, which is the single-index half of the fourth step. hsource is asked only AT THE Y AND THE A OF THE STATEMENT, not for every quasi-compact quasi-separated space and every finite algebra. The MEMBERS AND THE TRANSITION MAPS OF THE SYSTEM ARE NOT CARRIED: they are AlgebraicGeometry.Space.idealQuotientDiagram and AlgebraicGeometry.Space.idealQuotientQcohCocone, built from the quotient of an algebra sheaf on an algebraic space by a sheaf of ideals and its universal property (AlgebraicGeometry.Space.AlgebraSheaf.idealQuotient, idealQuotientMapOfLE, idealQuotientLift), and SURJECTIVITY OF EVERY TRANSITION MAP IS PROVED, by AlgebraicGeometry.Space.isLocallySurjective_idealQuotientQcohDiagram_map, so hsource asserts no surjectivity at all. Of the three inputs that leave Stacks 082A partial in AlgebraicGeometry.Space.exists_directed_isFinitePresentation_algebra_of_idealQuotients, ALL THREE ARE NOW DISCHARGEABLE FROM ELEMENTARY DATA and none may be SUBSTITUTED for: in each case that data is not among the remaining conjuncts of hsource, so replacing a conjunct by it would make hsource STRONGER and this theorem weaker. (1) B and the map are now CONSTRUCTIBLE at the algebraic space level: functoriality of the symmetric algebra is AlgebraicGeometry.Space.symmetricAlgebraSheafMap in Spaces/SymmetricAlgebraSheafMap.lean and the ungraded universal property producing a morphism of algebra sheaves Sym(F) to A out of a morphism of modules F to A is AlgebraicGeometry.Space.SymAlgSheaf.algebraLift in Spaces/SymmetricAlgebraSheafUngradedLift.lean, so with Stacks 086Y one may take B = Sym(F) and the map = algebraLift; quasi-coherence of Sym(F) is still unproved at this level but hsource asks NO quasi-coherence of B, so it is not needed here. (2) The colimit property of the constructed cocone is now EQUIVALENT, at the level of all algebra sheaves, to two elementary local conditions — local surjectivity of the map and local membership of every section it kills in some member of the family — by AlgebraicGeometry.Space.nonempty_isColimit_idealQuotientAlgCocone_iff_locally in Spaces/Limits/AlgebraSheafIdealQuotientColimit.lean, and AlgebraicGeometry.Space.nonempty_isColimit_idealQuotientQcohCocone_of_locally supplies the quasi-coherent form that hsource asks for from those two conditions, with no affine-chart verification and no cohomology. It is NOT substituted into hsource: the quasi-coherent algebras are a full subcategory, whose inclusion reflects but need not preserve colimits, so at that level the implication runs one way only and substituting the local conditions would make this hypothesis STRONGER and the theorem weaker. (3) Quasi-coherence and finite presentation of a sheafified quotient over an affine etale chart — the identification of the sections of B/I_j over such a chart with the objectwise quotient — is NOW PROVED, in Spaces/Limits/AlgebraSheafIdealQuotientCokernel.lean. The step that was missing, the identification of the underlying module of B/I_j with the COKERNEL of the inclusion of I_j, is AlgebraicGeometry.Space.AlgebraSheaf.underlyingModuleIdealQuotientCokernelIso, an epi-mono factorisation in the balanced category of O_Y-modules whose exactness input is AlgebraicGeometry.Space.AlgebraSheaf.kerIdeal_toIdealQuotient (the quotient morphism kills exactly the sections of the ideal, Spaces/Limits/AlgebraSheafIdealQuotientKernel.lean) and whose epimorphism input is local surjectivity of the quotient morphism. From it: quasi-coherence of B/I_j is AlgebraicGeometry.Space.AlgebraSheaf.isQuasicoherent_idealQuotient, by AlgebraicGeometry.Space.isQuasicoherentOnSite_cokernel_unconditional, GIVEN quasi-coherence of B and of I_j; the sections over an affine chart W are B(W)/I_j(W), by AlgebraicGeometry.Space.AlgebraSheaf.bijective_idealQuotientSectionsLift and idealQuotientSectionsRingEquiv, whose surjectivity half is AlgebraicGeometry.Space.surjective_val_app_of_epi_of_isQuasicoherentOnSite, the restated form of Descent 03DW, unconditional in this tree by faithfully flat descent with no Cech cohomology; and finite presentation of B/I_j is AlgebraicGeometry.Space.AlgebraSheaf.isFinitePresentation_idealQuotient, GIVEN finite presentation of B and finite generation of the ideal of sections I_j(W) over every affine chart, which is where the source's finite generation of the ideals enters and is why no finiteness is asked of them here. The conjunct is nevertheless NOT removed from hsource: hsource asks no quasi-coherence of B, no quasi-coherence of the I_j, no finiteness of them and no finite presentation of B, and none of those follow from its remaining conjuncts — finite presentation of a structure-algebra map on every affine chart says nothing about the restriction maps being base changes, so it does not imply quasi-coherence — so dropping the conjunct would require ADDING FOUR NEW ONES (quasi-coherence of B, quasi-coherence of each I_j, finite presentation of B, and finite generation of each I_j(W)), which makes hsource STRONGER and this theorem weaker. What has changed is that a caller holding those four can now produce the conjunct with no further mathematics. Stacks 086Y and Stacks 0829 are both proved here (as AlgebraicGeometry.Space.exists_directed_isFinitePresentation_epi_of_isFiniteType and as AlgebraicGeometry.Space.isColimit_finiteTypeQuasicoherentSubobjectCocone_of_07V9 with AlgebraicGeometry.Space.isFiltered_finiteTypeQuasicoherentSubobject). hsource asserts no finiteness of any stage and no directedness; finiteness of every stage, directedness, surjectivity of every transition map and survival of the colimit are proved. The source argues on one affine étale chart while this tree's finiteness predicates quantify over all of them, so the chart-uniformity of the carried integrality is carried too”.

Stacks Project, Tag 086Z. Let S be a scheme, let Y be a quasi-compact and quasi-separated algebraic space over S and let A be a finite quasi-coherent 𝒪_Y-algebra. Then A is the colimit of a system of quasi-coherent 𝒪_Y-algebras indexed by a nonempty directed preorder, every member of which is finite and of finite presentation, and every transition map of which is surjective.

All four assertions of the source are in the conclusion: the index is a nonempty preorder which is directed, every stage is AlgebraicGeometry.Space.AlgebraSheaf.IsFinite and AlgebraicGeometry.Space.AlgebraSheaf.IsFinitePresentation, every transition map is locally surjective, and the cocone with vertex A is colimiting. Quasi-coherence of the stages is structural, the diagram taking values in AlgebraicGeometry.Space.QuasicoherentAlgebra.

The quasi-compactness and quasi-separatedness of Y and the finiteness of A are used by being handed to hsource, which is the data of the third step of the source's proof — one algebra sheaf and a filtered family of sheaves of ideals of it — together with integrality at a single index, for this Y and this A and no other. The system itself is built from that data by AlgebraicGeometry.Space.idealQuotientDiagram and AlgebraicGeometry.Space.idealQuotientQcohCocone; see the module documentation for what hsource stands for and for what is proved on top of it.

theorem exists_directed_isFinite_isFinitePresentation_locallySurjective
    (Y : AlgebraicSpaces B S hS) (A : QuasicoherentAlgebra B S hS Y)
    (hqc : IsQuasiCompactSpace B S hS Y.obj)
    (hqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.obj)
    (hA : A.obj.IsFinite)
    (hsource :
      IsQuasiCompactSpace B S hS Y.obj →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.obj →
      A.obj.IsFinite →
        ∃ (ℬ : AlgebraSheaf.{u, u} B S hS Y.1 Y.2) (f : ℬ ⟶ A.obj) (J : Type u)
          (inst : SmallCategory J),
          let _ := inst
          ∃ (_ : IsFiltered J) (ι : J → ℬ.IdealSheaf)
            (hι : ∀ j j' : J, (j ⟶ j') → ι j ≤ ι j')
            (hkill : ∀ (j : J) (U : (SmallEtale B S hS Y.1)ᵒᵖ) (a : ℬ.right.obj.obj U),
              a ∈ (ι j).obj U → (f.right.hom.app U).hom a = 0)
            (hqcoh : ∀ j, (ℬ.idealQuotient (ι j)).IsQuasicoherent),
            (∀ j, (ℬ.idealQuotient (ι j)).IsFinitePresentation) ∧
            (∃ j, (ℬ.idealQuotient (ι j)).IsIntegral) ∧
            Nonempty (IsColimit (Cocone.mk A
              (idealQuotientQcohCocone ℬ ι hι A f hkill hqcoh)))) :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (D : I ⥤ QuasicoherentAlgebra B S hS Y) (φ : D ⟶ (Functor.const I).obj A),
      Nonempty (IsColimit (Cocone.mk A φ)) ∧
      (∀ i, (D.obj i).obj.IsFinite ∧ (D.obj i).obj.IsFinitePresentation) ∧
      ∀ i j (h : i ≤ j), Presheaf.IsLocallySurjective
        (SmallEtale.topology B S hS Y.obj) (D.map (homOfLE h)).hom.right.hom
Tag 082C, a lemma

Tag 082C in the Stacks Project.

AlgebraicGeometry.Space.isFiltered_isColimit_finiteSubalgebra_and_exists_directed_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/IntegralAlgebraFiniteColimitQcqs.lean, line 98.

Stacks 082C. Let X be a quasi-compact and quasi-separated algebraic space over a scheme S and let A be an integral quasi-coherent 𝒪_X-algebra. Then

  1. the finite quasi-coherent subalgebras of A form a directed (filtered) category and A is the colimit of the cocone of their inclusions, and
  2. A is the colimit of a directed system, over a nonempty directed preorder, of quasi-coherent 𝒪_X-algebras that are finite and of finite presentation.

The hypotheses are the source's.

theorem isFiltered_isColimit_finiteSubalgebra_and_exists_directed_finite
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (hqc : IsQuasiCompactSpace B S hS X)
    (hqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X)
    (A : AlgebraSheaf.{u, u} B S hS X hX) (hA : A.IsQuasicoherent) (hint : A.IsIntegral) :
    (IsFiltered (FiniteSubalgebra B S hS X hX A) ∧
        Nonempty (IsColimit (finiteSubalgebraCocone B S hS X hX A))) ∧
      ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
        (D : I ⥤ AlgebraSheaf.{u, u} B S hS X hX) (t : D ⟶ (Functor.const I).obj A)
        (_ : IsColimit (Cocone.mk A t)),
        ∀ i, (D.obj i).IsQuasicoherent ∧ (D.obj i).IsFinite ∧ (D.obj i).IsFinitePresentation

AlgebraicGeometry.Space.isFiltered_finiteSubalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/IntegralAlgebraFiniteSubalgebraColimit.lean, line 70. The attribute's comment: “part (1), the directedness assertion, and with no hypothesis beyond quasi-coherence and integrality of the algebra: neither quasi-compactness nor quasi-separatedness of the space is used. The colimit assertion of part (1) is AlgebraicGeometry.Space.nonempty_isColimit_finiteSubalgebraCocone and part (2) is AlgebraicGeometry.Space.exists_directed_isFinite_isFinitePresentation; those two name their own restrictions, this one has none”.

The finite quasi-coherent subalgebras of an integral quasi-coherent sheaf of commutative 𝒪_Y-algebras on an algebraic space Y form a filtered category.

theorem isFiltered_finiteSubalgebra (Y : AlgebraicSpaces B S hS)
    (A : AlgebraSheaf.{u, u} B S hS Y.1 Y.2) (hqcoh : A.IsQuasicoherent)
    (hint : A.IsIntegral) :
    IsFiltered (FiniteSubalgebra B S hS Y.1 Y.2 A)

AlgebraicGeometry.Space.nonempty_isColimit_finiteSubalgebraCocone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/IntegralAlgebraFiniteSubalgebraColimit.lean, line 99. The attribute's comment: “part (1), the colimit assertion, over the carried input hgen: for every affine etale chart U of the space and every section x of the algebra over U there is a finite quasi-coherent subalgebra of the algebra, on the whole space, having x among its sections over U. hgen is the algebraic-space analogue of what the scheme-level development derives from Stacks 01PF, namely Stacks.AlgebraicGeometry.SubalgebraGeneratedByModule.exists_finiteTypeSubalgebra_section, and it is asked only AT THE SPACE AND THE ALGEBRA OF THE STATEMENT. It replaces the colimit assertion of Stacks 082B, which is blocked by the source's own route on Stacks 07SU through Stacks 0829 and Stacks 07V9, and is strictly weaker than it: hgen mentions no cocone, no colimit and no index, and quantifies only over sections over single affine etale charts. Everything else is proved: directedness of the index is AlgebraicGeometry.Space.isFiltered_finiteSubalgebra, which has no restriction at all, sectionwise injectivity of the legs is AlgebraicGeometry.Space.AlgebraSheaf.injective_subobject_arrow_app, and the passage from sections over the affine etale charts to the colimit property is AlgebraicGeometry.Space.AlgebraSheaf.nonempty_isColimit_of_affineChartSections_of_injective. The identification of the finite with the finite type quasi-coherent subalgebras over an integral algebra, which is Algebra Lemma 10.36.5 on the affine etale charts, is proved as AlgebraicGeometry.Space.isQuasicoherentAndIsFinite_eq_isQuasicoherentAndIsFiniteType'”.

An integral quasi-coherent sheaf of commutative 𝒪_Y-algebras A on a quasi-compact and quasi-separated algebraic space Y is the colimit of the cocone of the inclusions of its finite quasi-coherent subalgebras, provided (hgen) every section of A over an affine étale chart of Y lies in the image of one finite quasi-coherent subalgebra of A.

theorem nonempty_isColimit_finiteSubalgebraCocone (Y : AlgebraicSpaces B S hS)
    (A : AlgebraSheaf.{u, u} B S hS Y.1 Y.2) (hqcoh : A.IsQuasicoherent) (hint : A.IsIntegral)
    (hqc : IsQuasiCompactSpace B S hS Y.obj)
    (hqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.obj)
    (hgen : IsQuasiCompactSpace B S hS Y.obj →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.obj →
      ∀ U : SmallEtale B S hS Y.1,
        IsAffine ((SmallEtale.toOver B S hS Y.1 ⋙ BigFppfOver.toScheme B S hS).obj U) →
        ∀ x : A.right.obj.obj (op U),
          ∃ C : FiniteSubalgebra B S hS Y.1 Y.2 A,
            x ∈ Set.range ((C.obj.arrow.right.hom.app (op U)).hom)) :
    Nonempty (IsColimit (finiteSubalgebraCocone B S hS Y.1 Y.2 A))

AlgebraicGeometry.Space.exists_directed_isFinite_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/IntegralAlgebraFiniteSubalgebraColimit.lean, line 191. The attribute's comment: “part (2), over three carried inputs. (a) hgen, the same input as in AlgebraicGeometry.Space.nonempty_isColimit_finiteSubalgebraCocone: every section of the algebra over an affine etale chart lies in the image of one finite quasi-coherent subalgebra on the whole space. Part (1) is PROVED from it here and is not assumed. (b) hstage, the carried input of Stacks 086Z itself — see the module documentation of StacksFrontier.AlgebraicGeometry.Spaces.Limits.FiniteAlgebraSurjectiveSystem for what it says — asked at every finite quasi-coherent algebra on the space rather than at one; Stacks 086Z is not restated, the theorem AlgebraicGeometry.Space.exists_directed_isFinite_isFinitePresentation_locallySurjective is called, so the finiteness, the finite presentation and the directedness of every inner system are that theorem's and not assumed here. (c) hpres, presentability of a finite and finitely presented quasi-coherent algebra ALONG THE TWO SYSTEMS' OWN COCONES, which is the analogue for algebraic spaces of the input the source takes from Cohomology of Spaces Lemma 69.5.3 and is weaker both than that lemma and than CategoryTheory.IsFinitelyPresentable of the stages: nothing is asked about any filtered colimit other than the two being spliced. On schemes the corresponding statement is a theorem, Stacks.AlgebraicGeometry.Tag0817Presentable.presentableAlong_of_isFinitePresentation, proved by carrying Stacks 01ZC across the relative spectrum of Stacks 01SA; for algebraic spaces the relative spectrum of Stacks 081W and the limit-preserving criterion AlgebraicGeometry.Space.exists_stage_map_of_relativelyLimitPreserving of Stacks 04AK are proved but the passage from a colimit of algebra sheaves to a limit of algebraic spaces affine over the base is not, so hpres is not proved. What is proved on top of the three: part (1) from hgen, including its directedness which has no restriction, the lifting of each inner index from Type u to the morphism universe of the quasi-coherent algebras along CategoryTheory.AsSmall, the splice itself, and that every stage of the resulting directed system is finite and of finite presentation. No declaration in this file assumes any assertion of Stacks 082C”.

An integral quasi-coherent sheaf of commutative 𝒪_Y-algebras on a quasi-compact and quasi-separated algebraic space Y is the colimit of a system, indexed by a nonempty directed preorder, of quasi-coherent 𝒪_Y-algebras each of which is finite and of finite presentation, provided hgen (as in nonempty_isColimit_finiteSubalgebraCocone), hstage (every finite quasi-coherent algebra on Y is a filtered colimit of finitely presented quotients of an algebra sheaf, one of them integral) and hpres (every finite and finitely presented quasi-coherent algebra is finitely presentable along every filtered colimit cocone of quasi-coherent algebras).

theorem exists_directed_isFinite_isFinitePresentation (Y : AlgebraicSpaces B S hS)
    (A : QuasicoherentAlgebra B S hS Y) (hint : A.obj.IsIntegral)
    (hqc : IsQuasiCompactSpace B S hS Y.obj)
    (hqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.obj)
    (hgen : IsQuasiCompactSpace B S hS Y.obj →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.obj →
      ∀ U : SmallEtale B S hS Y.1,
        IsAffine ((SmallEtale.toOver B S hS Y.1 ⋙ BigFppfOver.toScheme B S hS).obj U) →
        ∀ x : A.obj.right.obj.obj (op U),
          ∃ C : FiniteSubalgebra B S hS Y.1 Y.2 A.obj,
            x ∈ Set.range ((C.obj.arrow.right.hom.app (op U)).hom))
    (hstage : ∀ C : QuasicoherentAlgebra B S hS Y,
      IsQuasiCompactSpace B S hS Y.obj →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.obj →
      C.obj.IsFinite →
        ∃ (ℬ : AlgebraSheaf.{u, u} B S hS Y.1 Y.2) (f : ℬ ⟶ C.obj) (J : Type u)
          (inst : SmallCategory J),
          let _ := inst
          ∃ (_ : IsFiltered J) (ι : J → ℬ.IdealSheaf)
            (hι : ∀ j j' : J, (j ⟶ j') → ι j ≤ ι j')
            (hkill : ∀ (j : J) (U : (SmallEtale B S hS Y.1)ᵒᵖ) (a : ℬ.right.obj.obj U),
              a ∈ (ι j).obj U → (f.right.hom.app U).hom a = 0)
            (hqcoh : ∀ j, (ℬ.idealQuotient (ι j)).IsQuasicoherent),
            (∀ j, (ℬ.idealQuotient (ι j)).IsFinitePresentation) ∧
            (∃ j, (ℬ.idealQuotient (ι j)).IsIntegral) ∧
            Nonempty (IsColimit (Cocone.mk C
              (idealQuotientQcohCocone ℬ ι hι C f hkill hqcoh))))
    (hpres : ∀ T : QuasicoherentAlgebra B S hS Y, T.obj.IsFinite → T.obj.IsFinitePresentation →
      ∀ (J : Type (u + 1)) [SmallCategory J] [IsFiltered J]
        (Φ : J ⥤ QuasicoherentAlgebra B S hS Y) (c : Cocone Φ), IsColimit c →
        Stacks.FinitelyPresentableComposition.PresentableAlong T c) :
    ∃ (I : Type (u + 1)) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (D : I ⥤ QuasicoherentAlgebra B S hS Y) (φ : D ⟶ (Functor.const I).obj A),
      Nonempty (IsColimit (Cocone.mk A φ)) ∧
      ∀ i, (D.obj i).obj.IsFinite ∧ (D.obj i).obj.IsFinitePresentation
Tag 0853, a lemma

Tag 0853 in the Stacks Project.

AlgebraicGeometry.Space.exists_finiteTypeQuasicoherentSubobject_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeQuasicoherentSubobjectExtension.lean, line 149. The attribute's comment: “submodules as subobjects, restriction to the open as étale module pullback”.

Stacks Project, Tag 0853. Let X be a quasi-compact and quasi-separated algebraic space, U ⊂ X a quasi-compact open, ℱ a quasi-coherent 𝒪_X-module and 𝒢 ⊂ ℱ|_U a quasi-coherent 𝒪_U-submodule of finite type. Then there is a quasi-coherent submodule 𝒢' ⊂ ℱ of finite type with 𝒢'|_U = 𝒢, the equality being an isomorphism of 𝒢'|_U with 𝒢 commuting with the inclusions into ℱ|_U.

theorem exists_finiteTypeQuasicoherentSubobject_extension (j : U ⟶ X)
    (hj : IsOpenImmersion B S hS j.hom)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (hUqc : IsQuasiCompactSpace B S hS U.1)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (G : Subobject ((etaleModulePullback.{u, u} B S hS j
      (isEtale_of_isOpenImmersion B S hS hj)).obj F))
    [(G : Modules.{u, u} B S hS U.1 U.2).IsQuasicoherentOnSite]
    [(G : Modules.{u, u} B S hS U.1 U.2).IsFiniteType] :
    ∃ G' : Subobject F, (G' : Modules.{u, u} B S hS X.1 X.2).IsQuasicoherentOnSite ∧
      (G' : Modules.{u, u} B S hS X.1 X.2).IsFiniteType ∧
      ∃ e : (etaleModulePullback.{u, u} B S hS j
            (isEtale_of_isOpenImmersion B S hS hj)).obj
          (G' : Modules.{u, u} B S hS X.1 X.2) ≅ (G : Modules.{u, u} B S hS U.1 U.2),
        (etaleModulePullback.{u, u} B S hS j
            (isEtale_of_isOpenImmersion B S hS hj)).map G'.arrow = e.hom ≫ G.arrow

AlgebraicGeometry.Space.exists_etaleSubmodule_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeQuasicoherentSubobjectExtensionQcqs.lean, line 81.

Stacks 0853. Let X be a quasi-compact and quasi-separated algebraic space over S, U ⊆ X a quasi-compact open subspace, ℱ a quasi-coherent 𝒪_X-module and 𝒢 ⊆ ℱ|_U a quasi-coherent 𝒪_U-submodule of finite type. Then there is a quasi-coherent submodule 𝒢' ⊆ ℱ of finite type with 𝒢'|_U = 𝒢.

theorem exists_etaleSubmodule_extension (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS) (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (U : Subfunctor X.1) (hU : IsOpenSubspace B S hS U)
    (hUqc : IsQuasiCompactSpace B S hS U.toFunctor)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (G : ((etaleModulePullback.{u, u} B S hS (openSubspaceHom B S hS U hU)
      (isEtale_openSubspaceHom B S hS U hU)).obj F).Submodule)
    (hGq : G.toSheafOfModules.IsQuasicoherentOnSite) (hGf : G.toSheafOfModules.IsFiniteType) :
    ∃ G' : F.Submodule, G'.toSheafOfModules.IsQuasicoherentOnSite ∧
      G'.toSheafOfModules.IsFiniteType ∧
      etaleSubmoduleRestrict B S hS _ (isEtale_openSubspaceHom B S hS U hU) G' = G
Sources
LeanAlgebraicGeometry.Space.exists_isFilteredColimit_isFinitePresentationOnSite · AlgebraicGeometry.Space.exists_isFilteredColimit_isFinitePresentation · AlgebraicGeometry.Space.finiteTypeQuasicoherentSubobject_isFiltered · AlgebraicGeometry.Space.isFiltered_finiteTypeQuasicoherentSubobject · AlgebraicGeometry.Space.nonempty_isColimit_finiteTypeQuasicoherentSubobjectCocone_of_qcqs · AlgebraicGeometry.Space.isFiltered_and_nonempty_isColimit_finiteTypeQuasicoherentSubobjectCocone_of_qcqs · AlgebraicGeometry.Space.exists_directed_isFinitePresentation_epi · AlgebraicGeometry.Space.exists_directed_isFinitePresentation_algebra_of_idealQuotients

Section70.10 Relative approximation#

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

Tag 0GS3, a lemma

Tag 0GS3 in the Stacks Project.

AlgebraicGeometry.Space.hasRelativeApproximation_of_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationApproximation.lean, line 52.

Relative approximation over Spec ℤ, on any big fppf site. A morphism f : X ⟶ Y of quasi-compact quasi-separated algebraic spaces over Spec ℤ is the limit of a directed inverse system of morphisms of quasi-separated algebraic spaces of finite type over Spec ℤ with affine transition morphisms. It is built on an enlargement of the site on which X and Y have small atlases, and descended.

theorem hasRelativeApproximation_of_isQuasiCompactSpace (B : BigFppfSite.{u})
    (hZ : B.Contains (⊤_ Scheme.{u})) {X Y : (BigFppfOver B (⊤_ Scheme.{u}) hZ)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (hX : IsAlgebraicSpace B (⊤_ Scheme.{u}) hZ X)
    (hY : IsAlgebraicSpace B (⊤_ Scheme.{u}) hZ Y)
    (hXqc : IsQuasiCompactSpace B (⊤_ Scheme.{u}) hZ X)
    (hYqc : IsQuasiCompactSpace B (⊤_ Scheme.{u}) hZ Y)
    (hXqs : IsAbsolutelyQuasiSeparated B (⊤_ Scheme.{u}) hZ hZ X)
    (hYqs : IsAbsolutelyQuasiSeparated B (⊤_ Scheme.{u}) hZ hZ Y) :
    HasRelativeApproximation B hZ f
Tag 09NS, a lemma

Tag 09NS in the Stacks Project.

AlgebraicGeometry.Space.exists_isLimit_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationApproximation.lean, line 93.

Stacks 09NS. Let f : X ⟶ Y be a morphism of algebraic spaces over a scheme S, with X quasi-compact and quasi-separated and Y quasi-separated. Then X is the limit of a directed inverse system of algebraic spaces Xᵢ of finite presentation over Y, with affine transition morphisms over Y: an inverse system D of algebraic spaces over S with morphisms tᵢ : Xᵢ ⟶ Y of finite presentation compatible with the affine transition morphisms, and a limit cone X ⟶ Xᵢ over Y.

theorem exists_isLimit_finitePresentation (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hXqc : IsQuasiCompactSpace B S hS X)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y) :
    ∃ (I : Type (u + 1)) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirectedOrder I)
      (D : Iᵒᵖ ⥤ ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
      (t : D ⟶ (Functor.const Iᵒᵖ).obj Y) (p : (Functor.const Iᵒᵖ).obj X ⟶ D)
      (_ : IsLimit (Cone.mk X p)),
      (p ≫ t = (Functor.const Iᵒᵖ).map f) ∧
        (∀ i, IsAlgebraicSpace B S hS (D.obj i)) ∧
        (∀ i, IsFinitePresentation B S hS (t.app i)) ∧
        (∀ {i j : Iᵒᵖ} (g : i ⟶ j), IsAffineHom B S hS (D.map g))
Sources
LeanAlgebraicGeometry.Space.hasRelativeApproximation_of_isQuasiCompactSpace · AlgebraicGeometry.Space.exists_isLimit_finitePresentation

Section70.11 Finite type closed in finite presentation#

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

Tag 0870, a lemma

Tag 0870 in the Stacks Project.

AlgebraicGeometry.Space.exists_directed_limit_isFinitePresentation_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineMorphismDirectedLimit.lean, line 52. The attribute's comment: “the whole statement, under the source's hypotheses only: a directed inverse system of algebraic spaces affine and of finite presentation over Y, with X its limit and the projections compatible with f”.

Stacks 0870. Let S be a scheme and let f : X ⟶ Y be an affine morphism of algebraic spaces over S. If Y is quasi-compact and quasi-separated, then X is a directed limit X = lim X_i of algebraic spaces X_i affine over Y and of finite presentation over Y.

The system is indexed by the opposite of a nonempty directed preorder, so it is an inverse system; t is the family of structure morphisms X_i ⟶ Y, which are affine and of finite presentation, p is the family of projections X ⟶ X_i, each of which composes with the structure morphism to f, and X is the limit of the underlying presheaves, that is, of the fppf sheaves.

theorem exists_directed_limit_isFinitePresentation_of_isAffineHom
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsAffineHom B S hS f)
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y) :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (D : Iᵒᵖ ⥤ ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
      (t : D ⟶ (Functor.const Iᵒᵖ).obj Y) (p : (Functor.const Iᵒᵖ).obj X ⟶ D)
      (_ : IsLimit (Cone.mk X p)),
      (∀ i, IsAlgebraicSpace B S hS (D.obj i)) ∧
        (∀ i, IsAffineHom B S hS (t.app i)) ∧
          (∀ i, IsFinitePresentation B S hS (t.app i)) ∧
            ∀ i, p.app i ≫ t.app i = f
Tag 09YA, a lemma

Tag 09YA in the Stacks Project.

AlgebraicGeometry.Space.integralFiniteSystemOfIsIntegralHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralMorphismDirectedLimit.lean, line 97.

Stacks 09YA. An integral morphism f : X ⟶ Y of algebraic spaces over S, with Y quasi-compact and quasi-separated, presents X as a directed limit X = lim X_i of algebraic spaces X_i finite and of finite presentation over Y.

The system is a directed inverse system of algebraic spaces over Y indexed by a nonempty directed preorder, with a cone from X compatible with f which is a limit cone; every stage is finite and of finite presentation over Y (AlgebraicGeometry.Space.IntegralFiniteSystem). The stages are the relative spectra \underline{Spec}_Y(𝒜_i) (Stacks 081W) of the finite, finitely presented algebras of Stacks 082C presenting f_* 𝒪_X.

def integralFiniteSystemOfIsIntegralHom (f : X ⟶ Y) (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hf : IsIntegralHom B S hS f)
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y) :
    IntegralFiniteSystem B S hS f
Tag 07VR, a lemma

Tag 07VR in the Stacks Project.

AlgebraicGeometry.Space.integralFiniteSystem_of_isFinite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteMorphismLimitPresentation.lean, line 475. The attribute's comment: “granted E, the anti-equivalence of Stacks 081V between the algebraic spaces affine over a base and the quasi-coherent algebras on it, which this library states as a structure with no inhabitant; h086Z, the conclusion of Stacks 086Z that a finite quasi-coherent algebra on a quasi-compact quasi-separated algebraic space is a directed colimit of finite algebras of finite presentation with locally surjective transition maps; and hPushforwardIsFinite, hRelativeSpecIsFinite, hRelativeSpecIsFinitePresentation, the affine-chart comparison between finiteness of a morphism and finiteness of its direct-image algebra, which the source takes as immediate from the construction of the relative spectrum of Stacks 081W. E and h086Z conclude about categories and about algebras, and the comparison is about a single morphism, so none of them is the universally quantified form of this conclusion”.

Stacks 07VR. A finite morphism f : X ⟶ Y of algebraic spaces over S with Y quasi-compact and quasi-separated presents X as a directed inverse limit of algebraic spaces finite and of finite presentation over Y.

The direct-image algebra f_* 𝒪_X is a finite quasi-coherent 𝒪_Y-algebra, so h086Z writes it as a directed colimit of finite algebras of finite presentation with surjective transition maps. Applying the anti-equivalence E turns that colimit into a limit of the relative spectra X_i = \underline{Spec}_Y(𝒜_i); the surjections become monomorphisms, hence closed immersions between spaces finite over Y, and the limit is computed in presheaves by AlgebraicGeometry.Space.isLimit_affineOverToOver.

def integralFiniteSystem_of_isFinite {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hfin : IsFinite B S hS f)
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y)
    (E : AffineAlgebraAntiEquivalence B S hS)
    (hPushforwardIsFinite : ∀ {Y' : AlgebraicSpaces B S hS} (Z : AffineOver B S hS Y'),
      IsFinite B S hS Z.obj.hom.hom → ((E.pushforward Y').obj (op Z)).obj.IsFinite)
    (hRelativeSpecIsFinite : ∀ {Y' : AlgebraicSpaces B S hS}
      (A : QuasicoherentAlgebra B S hS Y'), A.obj.IsFinite →
      IsFinite B S hS (relativeSpec B S hS E A).obj.hom.hom)
    (hRelativeSpecIsFinitePresentation : ∀ {Y' : AlgebraicSpaces B S hS}
      (A : QuasicoherentAlgebra B S hS Y'), A.obj.IsFinite → A.obj.IsFinitePresentation →
      IsFinitePresentation B S hS (relativeSpec B S hS E A).obj.hom.hom)
    (h086Z : ∀ (Y' : AlgebraicSpaces B S hS) (A : QuasicoherentAlgebra B S hS Y'),
      IsQuasiCompactSpace B S hS Y'.obj →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y'.obj →
      A.obj.IsFinite →
      ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
        (D : I ⥤ QuasicoherentAlgebra B S hS Y') (φ : D ⟶ (Functor.const I).obj A),
        Nonempty (IsColimit (Cocone.mk A φ)) ∧
        (∀ i, (D.obj i).obj.IsFinite ∧ (D.obj i).obj.IsFinitePresentation) ∧
        ∀ i j (h : i ≤ j), Presheaf.IsLocallySurjective
          (SmallEtale.topology B S hS Y'.obj) (D.map (homOfLE h)).hom.right.hom) :
    IntegralFiniteSystem B S hS f

Declarations registered for the tag:

Tag 0A0U, a lemma

Tag 0A0U in the Stacks Project.

AlgebraicGeometry.Space.exists_isLimit_closedSubspaces_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ClosedImmersionFinitePresentationLimit.lean, line 106.

Let S be a scheme and let f : X ⟶ Y be a closed immersion of algebraic spaces over S, with Y quasi-compact and quasi-separated. Then X is a directed limit X = lim X_i: there are a nonempty directed index set and an inverse system of closed subspaces X_i ⊆ Y whose transition morphisms are closed immersions and whose inclusions X_i ⟶ Y are closed immersions of finite presentation, together with a limiting cone with vertex X whose legs X ⟶ X_i compose with the inclusions to f.

theorem exists_isLimit_closedSubspaces_of_isClosedImmersion (Y : AlgebraicSpaces B S hS)
    (hYqc : IsQuasiCompactSpace B S hS Y.1) (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y.1)
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y.1)
    (hf : IsClosedImmersion B S hS f) :
    ∃ (I : Type u) (_ : Preorder I) (_ : IsDirected I (· ≤ ·)) (_ : Nonempty I)
      (Z : I → ClosedSubspaces B S hS Y.1) (hZ : ∀ ⦃i j : I⦄, i ≤ j → (Z j).1 ≤ (Z i).1)
      (hle : ∀ i, Subfunctor.range f ≤ (Z i).1),
      (∀ ⦃i j : Iᵒᵖ⦄ (g : i ⟶ j), IsClosedImmersion B S hS
        ((closedSubspaceDiagram B S hS (fun i => (Z i).1) hZ).map g)) ∧
      (∀ i, IsClosedImmersion B S hS (Z i).1.ι ∧ IsFinitePresentation B S hS (Z i).1.ι) ∧
      (∀ i, ((closedSubspaceCone B S hS (fun i => (Z i).1) hZ (Subfunctor.range f) hle).extend
        (Subfunctor.toRange f)).π.app (op i) ≫ (Z i).1.ι = f) ∧
      Nonempty (IsLimit ((closedSubspaceCone B S hS (fun i => (Z i).1) hZ (Subfunctor.range f)
        hle).extend (Subfunctor.toRange f)))

AlgebraicGeometry.Space.hasClosedSubspaceApproximation_of_invariantIdeals, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ClosedSubspaceApproximation.lean, line 575. The attribute's comment: “given the approximating family of invariant ideal sheaves on a chart, which is Stacks 0829 for the ideal sheaf of X read on that chart”.

Stacks 0A0U. Let S be a scheme and let X ⊆ Y be a closed subspace of an algebraic space Y over S. Then X is a directed inverse limit X = lim X_i of closed subspaces of Y whose transition morphisms are closed immersions and whose structure morphisms X_i ⟶ Y are closed immersions of finite presentation, as soon as the ideal sheaf cut out by X on a surjective étale scheme chart V ⟶ Y is the supremum of a monotone family of invariant ideal sheaves of 𝒪_V each of which cuts out a closed subspace of finite presentation over Y.

The approximating family is the hypothesis: it is what Stacks 0829 supplies for the ideal sheaf of X, read on the chart V, together with Stacks 084Q for the finite presentation of the stages. Everything else is proved here and unconditionally: each member of the family cuts out a closed subspace of Y by étale descent, its chart ideal on V is the given ideal sheaf, the family of subspaces is antitone with X contained in every member, and the inclusions exhibit X as the inverse limit.

theorem hasClosedSubspaceApproximation_of_invariantIdeals [Preorder I] [IsDirected I (· ≤ ·)]
    (i₀ : I) (X : ClosedSubspaces B S hS Y.1) (hK : Monotone K)
    (hsup : (⨆ i, K i) = etaleChartKer B S hS Y X (chartOfSurjectiveEtale B S hS Y he))
    (hfp : ∀ i, IsFinitePresentation B S hS
      (invariantSubspace B S hS φ (Subobject.mk (K i).subschemeι)).ι) :
    HasClosedSubspaceApproximation B S hS Y X
Tag 0871, a lemma

Tag 0871 in the Stacks Project.

AlgebraicGeometry.Space.exists_isFinitePresentation_isClosedImmersion_of_isQuasiAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/QuasiAffineClosedInFinitePresentation.lean, line 139. The attribute's comment: “for a target represented by a quasi-compact quasi-separated object of the site; a general algebraic-space target needs the unproved direction of 086S and Stacks 0870”.

A morphism of algebraic spaces over S which is locally of finite type and quasi-affine, whose target is the functor of points of a quasi-compact, quasi-separated scheme of the site, is a closed immersion into an algebraic space of finite presentation over that target.

theorem exists_isFinitePresentation_isClosedImmersion_of_isQuasiAffineHom
    {Z : BigFppfOver B S hS} {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ yoneda.obj Z)
    (hX : IsAlgebraicSpace B S hS X)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hqa : IsQuasiAffineHom B S hS f)
    (hZqc : CompactSpace ((BigFppfOver.toScheme B S hS).obj Z))
    (hZqs : QuasiSeparatedSpace ((BigFppfOver.toScheme B S hS).obj Z)) :
    ∃ (X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f' : X' ⟶ yoneda.obj Z) (i : X ⟶ X'),
      IsAlgebraicSpace B S hS X' ∧ IsFinitePresentation B S hS f' ∧
        IsClosedImmersion B S hS i ∧ i ≫ f' = f

AlgebraicGeometry.Space.exists_isFinitePresentation_isClosedImmersion_of_isQuasiAffineHom_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/QuasiAffineClosedInFinitePresentationQcqs.lean, line 119.

Let S be a scheme and let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type and quasi-affine, with Y quasi-compact and quasi-separated. Then there are a morphism of finite presentation f' : X' ⟶ Y and a closed immersion i : X ⟶ X' with i ≫ f' = f.

theorem exists_isFinitePresentation_isClosedImmersion_of_isQuasiAffineHom_of_qcqs
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hft : IsLocallyOfFiniteType B S hS f) (hfqa : IsQuasiAffineHom B S hS f)
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y) :
    ∃ (X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f' : X' ⟶ Y) (i : X ⟶ X'),
      IsAlgebraicSpace B S hS X' ∧ IsFinitePresentation B S hS f' ∧
        IsClosedImmersion B S hS i ∧ i ≫ f' = f
Tag 0872, a lemma

Tag 0872 in the Stacks Project.

Declarations registered for the tag:

Tag 0873, a proposition

Tag 0873 in the Stacks Project.

AlgebraicGeometry.Space.exists_isClosedImmersion_isSeparated_isFinitePresentation_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ProperLimitOfFinitePresentationEmbedding.lean, line 196.

Let f : X ⟶ Y be a separated morphism of finite type of algebraic spaces over S, with Y quasi-compact and quasi-separated. Then there are a separated morphism of finite presentation f' : X' ⟶ Y and a closed immersion i : X ⟶ X' with i ≫ f' = f.

theorem exists_isClosedImmersion_isSeparated_isFinitePresentation_of_isFiniteType
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hft : IsFiniteType B S hS f)
    (hsep : IsSeparated B S hS f) (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y) :
    ∃ (X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (i : X ⟶ X') (f' : X' ⟶ Y),
      IsAlgebraicSpace B S hS X' ∧ IsClosedImmersion B S hS i ∧ IsSeparated B S hS f' ∧
        IsFinitePresentation B S hS f' ∧ i ≫ f' = f
Sources
LeanAlgebraicGeometry.Space.exists_directed_limit_isFinitePresentation_of_isAffineHom · AlgebraicGeometry.Space.integralFiniteSystemOfIsIntegralHom · AlgebraicGeometry.Space.integralFiniteSystem_of_isFinite · AlgebraicGeometry.Space.exists_integralFiniteSystem_of_isFinite · AlgebraicGeometry.Space.exists_isLimit_closedSubspaces_of_isClosedImmersion · AlgebraicGeometry.Space.hasClosedSubspaceApproximation_of_invariantIdeals · AlgebraicGeometry.Space.exists_isFinitePresentation_isClosedImmersion_of_isQuasiAffineHom · AlgebraicGeometry.Space.exists_isFinitePresentation_isClosedImmersion_of_isQuasiAffineHom_of_qcqs

Section70.12 Approximating proper morphisms#

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

Tag 0A0W, a lemma

Tag 0A0W in the Stacks Project.

AlgebraicGeometry.Space.exists_isLimit_isProper_isFinitePresentation_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ProperLimitOfFinitePresentationEmbedding.lean, line 213.

Let f : X ⟶ Y be a proper morphism of algebraic spaces over S, with Y quasi-compact and quasi-separated. Then X is the directed limit, along closed immersions and over Y, of algebraic spaces proper and of finite presentation over Y, the projections from X being closed immersions.

theorem exists_isLimit_isProper_isFinitePresentation_of_isProper
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsProper B S hS f)
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y) :
    ∃ (I : Type u) (_ : Preorder I) (_ : IsDirected I (· ≤ ·)) (_ : Nonempty I)
      (D : Iᵒᵖ ⥤ (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (t : D ⟶ (Functor.const Iᵒᵖ).obj Y)
      (π : (Functor.const Iᵒᵖ).obj X ⟶ D),
      (∀ i, IsAlgebraicSpace B S hS (D.obj i)) ∧
      (∀ i, IsProper B S hS (t.app i) ∧ IsFinitePresentation B S hS (t.app i)) ∧
      (∀ ⦃i j : Iᵒᵖ⦄ (e : i ⟶ j), IsClosedImmersion B S hS (D.map e)) ∧
      (∀ i, IsClosedImmersion B S hS (π.app i)) ∧
      π ≫ t = (Functor.const Iᵒᵖ).map f ∧
      Nonempty (IsLimit (Cone.mk X π))
Tag 0A0X, a lemma

Tag 0A0X in the Stacks Project.

AlgebraicGeometry.Space.exists_isLimit_isProper_isFinitePresentation_arrow_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ProperLimitOfFinitePresentationEmbedding.lean, line 263.

Let f : X ⟶ Y be a proper morphism of algebraic spaces over Spec ℤ, with Y quasi-compact and quasi-separated. Then f is the limit of a directed system of proper morphisms of finite presentation X_i ⟶ Y_i between algebraic spaces of finite presentation over Spec ℤ, the systems X_i and Y_i having affine transition morphisms.

theorem exists_isLimit_isProper_isFinitePresentation_arrow_of_isProper
    (hZ : B.Contains (⊤_ Scheme.{u}))
    {X Y : ((BigFppfOver B (⊤_ Scheme.{u}) hZ)ᵒᵖ ⥤ Type u)} (hX : IsAlgebraicSpace B _ hZ X) (hY :
      IsAlgebraicSpace B _ hZ Y)
    (f : X ⟶ Y) (hf : IsProper B _ hZ f) (hYqc : IsQuasiCompactSpace B _ hZ Y)
    (hYqs : IsAbsolutelyQuasiSeparated B _ hZ hZ Y) :
    ∃ (I : Type u) (_ : Preorder I) (_ : IsDirected I (· ≤ ·))
      (DX DY : DescentSituation B (⊤_ Scheme.{u}) hZ hZ I) (φ : DX.system ⟶ DY.system)
      (eX : DX.limitCone.pt ≅ X) (eY : DY.limitCone.pt ≅ Y),
      (∀ i : I, DX.limitCone.π.app (op i) ≫ φ.app (op i) =
        eX.hom ≫ f ≫ eY.inv ≫ DY.limitCone.π.app (op i)) ∧
      (∀ i : I, IsProper B _ hZ (φ.app (op i)) ∧ IsFinitePresentation B _ hZ (φ.app (op i))) ∧
      (∀ i : I, IsFinitePresentation B _ hZ (terminal.from (DY.system.obj (op i))))
Tag 08K2, a lemma

Tag 08K2 in the Stacks Project.

AlgebraicGeometry.Space.MorphismDescentData.exists_isProper_schemeTheoreticSupport_moduleAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/MorphismDescentData.lean, line 251.

In Situation 084W, under the chapter's convention of Section 70.2, let F₀ be a quasi-coherent 𝒪_{X₀}-module of finite type and let F and F_i be its pullbacks to X and X_i. If f₀ is locally of finite type and the scheme-theoretic support of F is proper over Y, then the scheme-theoretic support of F_i is proper over Y_i for some i ≥ 0.

theorem exists_isProper_schemeTheoreticSupport_moduleAt
    (hconv : SiteContainsBaseChangeLimits B S hS D.base)
    (F₀ : Modules.{u, u} B S hS (D.toMorphismDescentSituation hconv).source₀Space.1
      (D.toMorphismDescentSituation hconv).source₀Space.2)
    (hqc : F₀.IsQuasicoherentOnSite)
    (hf₀ : IsLocallyOfFiniteType B S hS D.map₀)
    (hft : SheafOfModules.IsFiniteTypeOnSite F₀)
    (hproper : IsProper B S hS
      ((schemeTheoreticSupport B S hS (D.toMorphismDescentSituation hconv).sourceLimitSpace
        ((D.toMorphismDescentSituation hconv).moduleLimit F₀)).ι ≫
          (D.toMorphismDescentSituation hconv).mapLimit)) :
    ∃ (i : I) (hi : D.initial ≤ i), IsProper B S hS
      ((schemeTheoreticSupport B S hS ((D.toMorphismDescentSituation hconv).sourceAtSpace i hi)
        ((D.toMorphismDescentSituation hconv).moduleAt F₀ i hi)).ι ≫
          (D.toMorphismDescentSituation hconv).mapAt i hi)
Sources
LeanAlgebraicGeometry.Space.exists_isLimit_isProper_isFinitePresentation_of_isProper · AlgebraicGeometry.Space.exists_isLimit_isProper_isFinitePresentation_arrow_of_isProper · AlgebraicGeometry.Space.MorphismDescentData.exists_isProper_schemeTheoreticSupport_moduleAt

Section70.13 Embedding into affine space#

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

Tag 088L, a lemma

Tag 088L in the Stacks Project.

AlgebraicGeometry.Space.exists_isImmersion_affineSpaceOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/EmbeddingIntoAffineSpace.lean, line 1019. The attribute's comment: “with the cutoff-cofinality side condition on the sections of U that the directed limit in the proof requires; quasi-separatedness of X is not needed”.

Stacks 088L. Let f : U ⟶ X be a morphism of algebraic spaces over S with U an affine scheme, f locally of finite type and X locally separated. Then U admits an immersion into affine n-space over X, over X.

The hypothesis hcard bounds the ring of sections of U by the cofinality of the site's cutoff; it is not part of Stacks 088L, but is the condition under which the directed limit used in the proof is an algebraic space in this development, inherited from Stacks 07SF and Stacks 0828. See exists_isImmersion_affineSpaceOver_of_isRegular for the form in which it disappears, and the implementation notes of this file for why it cannot be removed outright.

Quasi-separatedness of X, which Stacks 088L also assumes, is not needed: this development's Stacks 0828, part (2) does not assume it of the stages.

theorem exists_isImmersion_affineSpaceOver (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u})) (U : BigFppfOver B S hS)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : yoneda.obj U ⟶ X)
    (hU : IsAffine ((BigFppfOver.toScheme B S hS).obj U))
    (hX : IsAlgebraicSpace B S hS X)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hls : IsAbsolutelyLocallySeparated B S hS hZ X)
    (hcard : #Γ((BigFppfOver.toScheme B S hS).obj U, ⊤) < B.cutoff.ord.cof) :
    ∃ (n : ℕ) (j : yoneda.obj U ⟶ affineSpaceOver B S hS X n),
      j ≫ prod.fst = f ∧ IsImmersion B S hS j

AlgebraicGeometry.Space.exists_isImmersion_affineSpaceOver_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/EmbeddingIntoAffineSpace.lean, line 1068. The attribute's comment: “verbatim, over a big fppf site whose size cutoff is a regular cardinal”.

Stacks 088L over a big fppf site whose size cutoff is a regular cardinal: an affine scheme locally of finite type over a locally separated algebraic space admits an immersion into affine n-space over that space.

Regularity of the cutoff discharges the cardinality side condition of exists_isImmersion_affineSpaceOver for every U: the sections of an affine object of the site are bounded by its size, which is below the cutoff, which is its own cofinality.

theorem exists_isImmersion_affineSpaceOver_of_isRegular (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u})) (hreg : B.cutoff.IsRegular)
    (U : BigFppfOver B S hS) (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : yoneda.obj U ⟶ X)
    (hU : IsAffine ((BigFppfOver.toScheme B S hS).obj U))
    (hX : IsAlgebraicSpace B S hS X)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hls : IsAbsolutelyLocallySeparated B S hS hZ X) :
    ∃ (n : ℕ) (j : yoneda.obj U ⟶ affineSpaceOver B S hS X n),
      j ≫ prod.fst = f ∧ IsImmersion B S hS j

AlgebraicGeometry.Space.exists_isImmersion_affineSpaceOver_of_isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/EmbeddingIntoAffineSpace.lean, line 1124.

Stacks 088L. Let f : U ⟶ X be a morphism of algebraic spaces over S with U an affine scheme, f locally of finite type, and X quasi-separated and locally separated. Then there is an immersion U ⟶ 𝔸ⁿ_X over X.

Writing U = Spec A with A the filtered union of its finite type ℤ-subalgebras Aᵢ, the graph U ⟶ X ⨯ U is an immersion because X is locally separated (Stacks 03KO), and X ⨯ U is the directed limit of the stages X ⨯ Spec Aᵢ, which have affine transition morphisms and are quasi-separated because X is. Stacks 0828, part (2), which places no bound on the index set, then makes U ⟶ X ⨯ Spec Aᵢ an immersion for some i, and Spec Aᵢ is a closed subscheme of affine space over ℤ.

theorem exists_isImmersion_affineSpaceOver_of_isAbsolutelyQuasiSeparated (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) (U : BigFppfOver B S hS)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : yoneda.obj U ⟶ X)
    (hU : IsAffine ((BigFppfOver.toScheme B S hS).obj U))
    (hX : IsAlgebraicSpace B S hS X)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X)
    (hls : IsAbsolutelyLocallySeparated B S hS B.contains_terminal X) :
    ∃ (n : ℕ) (j : yoneda.obj U ⟶ affineSpaceOver B S hS X n),
      j ≫ prod.fst = f ∧ IsImmersion B S hS j
Tag 088M, a remark

Tag 088M in the Stacks Project.

AlgebraicGeometry.Space.exists_not_isAbsolutelyLocallySeparated_not_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/EmbeddingIntoAffineSpaceSharp.lean, line 92. The attribute's comment: “the failure of 088L without local separatedness, carried by 088W and so conditional on the same effective descent hypotheses, and over a site whose cutoff is regular; the open question the remark raises about quasi-separatedness is not a theorem and is not formalized”.

Stacks 088M, the half of the remark which is a theorem: the hypothesis of Stacks 088L that X be locally separated cannot be dropped.

Over a field in which two is invertible there is a finite type morphism f : Y ⟶ X of algebraic spaces with Y an affine scheme and X quasi-separated — so every hypothesis of Stacks 088L except local separatedness holds — such that X is not locally separated and Y admits no immersion over X into relative affine n-space over X, for any n.

The witness is the one of Stacks 088W, the chart 𝔸¹_k ⟶ 𝔸¹_k/R of Stacks 02Z1; failure of local separatedness is read off from the failure of the conclusion of Stacks 088L by contraposition, which is what hreg is for. See the implementation notes of this file for hreg, hdiag and hchart, none of which Stacks 088M has.

The remark also raises the question whether Stacks 088L holds without quasi-separatedness. That is an open question, not a result, and nothing here formalizes it.

theorem exists_not_isAbsolutelyLocallySeparated_not_isImmersion
    (k : Type u) [Field k] (hchar : (2 : k) ≠ 0)
    (B : BigFppfSite.{u}) (hreg : B.cutoff.IsRegular)
    (hS : B.Contains (Spec (.of k))) (hZ : B.Contains (⊤_ Scheme.{u}))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hS) (Type u)]
    (_hdiag : IsEffectiveDescentAlongCoveringSieve B (Spec (.of k)) hS
      (MorphismProperty.monomorphisms Scheme.{u} ⊓ @LocallyOfFiniteType))
    (_hchart : IsEffectiveDescentAlongCoveringSieve B (Spec (.of k)) hS
      (@_root_.AlgebraicGeometry.IsSeparated.{u} ⊓ @LocallyQuasiFinite ⊓
        @LocallyOfFiniteType ⊓ @Surjective ⊓ @Etale : MorphismProperty Scheme.{u})) :
    ∃ (Y : BigFppfOver B (Spec (.of k)) hS)
      (X : (BigFppfOver B (Spec (.of k)) hS)ᵒᵖ ⥤ Type u)
      (f : yoneda.obj Y ⟶ X),
      IsAffine ((BigFppfOver.toScheme B (Spec (.of k)) hS).obj Y) ∧
      IsAlgebraicSpace B (Spec (.of k)) hS X ∧
      IsFiniteType B (Spec (.of k)) hS f ∧
      IsAbsolutelyQuasiSeparated B (Spec (.of k)) hS hZ X ∧
      ¬ IsAbsolutelyLocallySeparated B (Spec (.of k)) hS hZ X ∧
      ∀ (n : ℕ) (j : yoneda.obj Y ⟶ affineSpaceOver B (Spec (.of k)) hS X n),
        j ≫ prod.fst = f → ¬ IsImmersion B (Spec (.of k)) hS j

AlgebraicGeometry.Space.exists_not_isAbsolutelyLocallySeparated_not_isImmersion', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/EmbeddingIntoAffineSpaceSharpUnconditional.lean, line 60. The attribute's comment: “the failure of 088L without local separatedness; the open question the remark raises about quasi-separatedness is not a theorem and is not formalized”.

Stacks 088M, the half of the remark which is a theorem: the hypothesis of Stacks 088L that X be locally separated cannot be dropped.

Over a field in which two is invertible there is a finite type morphism f : Y ⟶ X of algebraic spaces with Y an affine scheme and X quasi-separated — so every hypothesis of Stacks 088L except local separatedness holds — such that X is not locally separated and Y admits no immersion over X into relative affine n-space over X, for any n.

The witness is the one of Stacks 088W, the chart 𝔸¹_k ⟶ 𝔸¹_k/R of Stacks 02Z1, and the failure of local separatedness is the corresponding half of Stacks 02Z1, so the conclusion rests on nothing beyond what Stacks 088M itself assumes. The unprimed exists_not_isAbsolutelyLocallySeparated_not_isImmersion is the same conclusion reached instead by contraposition through Stacks 088L, which costs three further hypotheses (hreg, hdiag, hchart).

The remark also raises the question whether Stacks 088L holds without quasi-separatedness. That is an open question, not a result, and nothing here formalizes it.

theorem exists_not_isAbsolutelyLocallySeparated_not_isImmersion'
    (k : Type u) [Field k] (hchar : (2 : k) ≠ 0)
    (B : BigFppfSite.{u})
    (hS : B.Contains (Spec (.of k))) (hZ : B.Contains (⊤_ Scheme.{u}))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hS) (Type u)] :
    ∃ (Y : BigFppfOver B (Spec (.of k)) hS)
      (X : (BigFppfOver B (Spec (.of k)) hS)ᵒᵖ ⥤ Type u)
      (f : yoneda.obj Y ⟶ X),
      IsAffine ((BigFppfOver.toScheme B (Spec (.of k)) hS).obj Y) ∧
      IsAlgebraicSpace B (Spec (.of k)) hS X ∧
      IsFiniteType B (Spec (.of k)) hS f ∧
      IsAbsolutelyQuasiSeparated B (Spec (.of k)) hS hZ X ∧
      ¬ IsAbsolutelyLocallySeparated B (Spec (.of k)) hS hZ X ∧
      ∀ (n : ℕ) (j : yoneda.obj Y ⟶ affineSpaceOver B (Spec (.of k)) hS X n),
        j ≫ prod.fst = f → ¬ IsImmersion B (Spec (.of k)) hS j
Tag 088N, a lemma

Tag 088N in the Stacks Project.

AlgebraicGeometry.Space.exists_denseOpen_isImmersion_affineSpaceOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DenseOpenEmbeddingIntoAffineSpace/ComponentGlueing.lean, line 347.

Stacks 088N. Let f : Y ⟶ X be a morphism of algebraic spaces over S with X Noetherian and f of finite presentation. Then Y has a dense open subspace which admits, over X, an immersion into relative affine n-space over X.

public theorem exists_denseOpen_isImmersion_affineSpaceOver
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hZ : B.Contains (⊤_ Scheme.{u}))
    {Y X : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : Y ⟶ X)
    (hY : AlgebraicGeometry.IsAlgebraicSpace B S hS Y)
    (hX : AlgebraicGeometry.IsAlgebraicSpace B S hS X)
    (hXN : AlgebraicGeometry.Space.IsNoetherian B S hS hZ X)
    (hf : AlgebraicGeometry.Space.IsFinitePresentation B S hS f) :
    ∃ (V : Subfunctor Y),
      AlgebraicGeometry.Space.IsOpenSubspace B S hS V ∧
      (letI : TopologicalSpace (AlgebraicGeometry.Space.points B S hS Y) :=
          AlgebraicGeometry.Space.pointTopology B S hS Y;
        DenseRange (AlgebraicGeometry.Space.pointsMap B S hS V.toFunctor V.ι)) ∧
      ∃ (n : ℕ) (i : V.toFunctor ⟶ AlgebraicGeometry.Space.affineSpaceOver B S hS X n),
        AlgebraicGeometry.Space.IsImmersion B S hS i ∧
          i ≫ prod.fst = V.ι ≫ f
Sources
LeanAlgebraicGeometry.Space.exists_isImmersion_affineSpaceOver · AlgebraicGeometry.Space.exists_isImmersion_affineSpaceOver_of_isRegular · AlgebraicGeometry.Space.exists_isImmersion_affineSpaceOver_of_isAbsolutelyQuasiSeparated · AlgebraicGeometry.Space.exists_not_isAbsolutelyLocallySeparated_not_isImmersion · AlgebraicGeometry.Space.exists_not_isAbsolutelyLocallySeparated_not_isImmersion' · AlgebraicGeometry.Space.exists_denseOpen_isImmersion_affineSpaceOver

Section70.14 Sections with support in a closed subset#

Section 70.14 of the Stacks Project, Tag 0854. 7 tags here are carried by 17 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0855, a lemma

Tag 0855 in the Stacks Project.

AlgebraicGeometry.Space.hasFiniteTypeQuasicoherentIdealZeroLocus_of_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeIdealOfQuasiCompactOpen.lean, line 254. The attribute's comment: “part (2) implies part (3)”.

Let X be a quasi-compact and quasi-separated algebraic space over S and let U ⊆ X be an open subspace. If U is quasi-compact, then there is a finite type quasi-coherent sheaf of ideals ℐ ⊆ 𝒪_X with |X| ∖ |U| = |V(ℐ)|.

This is AlgebraicGeometry.Space.exists_isFiniteTypeQuasicoherentIdeal_idealZeroLocus_eq_compl_range, which follows the source: the reduced sheaf of ideals of |X| ∖ |U| is cut down by Stacks 0853, AlgebraicGeometry.Space.exists_etaleSubmodule_extension, to a quasi-coherent sheaf of ideals of finite type with the same restriction to U.

theorem hasFiniteTypeQuasicoherentIdealZeroLocus_of_isQuasiCompactSpace
    (hZ : B.Contains (⊤_ Scheme.{u})) (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    {U : Subfunctor X.1} (hU : IsOpenSubspace B S hS U)
    (hUqc : IsQuasiCompactSpace B S hS U.toFunctor) :
    HasFiniteTypeQuasicoherentIdealZeroLocus B S hS X U

AlgebraicGeometry.Space.isQuasiCompactSpace_of_hasFiniteTypeQuasicoherentIdealZeroLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactOpenOfFiniteTypeIdeal.lean, line 129. The attribute's comment: “part (3) implies part (2)”.

Stacks 0855, part (3) implies part (2). Let X be a quasi-compact algebraic space over S and let U ⊆ X be an open subspace. If there is a finite type quasi-coherent sheaf of ideals ℐ ⊆ 𝒪_X with |X| ∖ |U| = |V(ℐ)|, then U is quasi-compact.

An affine étale chart of X surjective on points exists by Tag 03H6. The Zariski sheaf of ideals which ℐ induces on the chart's scheme is of finite type, so the complement of its support is a quasi-compact open of that affine — and hence quasi-compact — scheme, by part (4) ⟹ (2) of [Stacks, Tag 01PH]. That complement maps onto |U| = |X| ∖ |V(ℐ)|, continuously, so |U| is a quasi-compact subset of |X|, and Tag 03E4 turns that into quasi-compactness of the open subspace U.

theorem isQuasiCompactSpace_of_hasFiniteTypeQuasicoherentIdealZeroLocus
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    {U : Subfunctor X.1} (hU : IsOpenSubspace B S hS U)
    (h : HasFiniteTypeQuasicoherentIdealZeroLocus B S hS X U) :
    IsQuasiCompactSpace B S hS U.toFunctor

AlgebraicGeometry.Space.tfae_isQuasiCompact_openSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactOpenTfae.lean, line 56.

Stacks 0855. Let X be a quasi-compact and quasi-separated algebraic space over S and let U ⊆ X be an open subspace. The following are equivalent:

  1. the inclusion U → X is quasi-compact,
  2. U is quasi-compact, and
  3. there exists a finite type quasi-coherent sheaf of ideals ℐ ⊆ 𝒪_X such that |X| ∖ |U| = |V(ℐ)|.
theorem tfae_isQuasiCompact_openSubspace (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS) (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (U : Subfunctor X.1) (hU : IsOpenSubspace B S hS U) :
    List.TFAE [IsQuasiCompact B S hS U.ι, IsQuasiCompactSpace B S hS U.toFunctor,
      HasFiniteTypeQuasicoherentIdealZeroLocus B S hS X U]

AlgebraicGeometry.Space.isQuasiCompact_iff_isQuasiCompactSpace_openSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactSupport.lean, line 205. The attribute's comment: “parts (1) and (2)”.

For an open subspace of a quasi-compact and quasi-separated algebraic space, quasi-compactness of the inclusion is equivalent to quasi-compactness of its source.

theorem isQuasiCompact_iff_isQuasiCompactSpace_openSubspace
    (X : AlgebraicSpaces B S hS)
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (U : {U : Subfunctor X.1 // IsOpenSubspace B S hS U}) :
    IsQuasiCompact B S hS U.1.ι ↔ IsQuasiCompactSpace B S hS U.1.toFunctor
Tag 0856, a lemma

Tag 0856 in the Stacks Project.

AlgebraicGeometry.Space.mem_annihilatorSubmodule_obj_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IdealAnnihilatorAffineSections.lean, line 117. The attribute's comment: “part (2)”.

[Stacks, Tag 0856], part (2): the sections of the annihilator subsheaf over an affine chart. Over an affine étale chart W of an algebraic space, a section of G lies in the subsheaf annihilated by a quasi-coherent sheaf of ideals I exactly when the sections of I over W itself kill it — no restriction to a smaller chart has to be tested.

theorem mem_annihilatorSubmodule_obj_of_isAffine
    (hI : I.toSheafOfModules.IsQuasicoherentOnSite) (W : (SmallEtale B S hS F)ᵒᵖ)
    (hW : IsAffine ((SmallEtale.toOver B S hS F ⋙ BigFppfOver.toScheme B S hS).obj W.unop))
    (s : G.val.obj W) :
    s ∈ (annihilatorSubmodule B S hS F hF I G).toSubmodule.obj W ↔
      ∀ a : (Stacks.SheafOfModules.Tensor.ringSheaf
          (smallEtaleRingedSite B S hS F hF).O).obj.obj W,
        a ∈ I.obj W → a • s = 0

AlgebraicGeometry.Space.exists_germ_annihilatorSubmodule_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IdealAnnihilatorGeometricStalk.lean, line 91. The attribute's comment: “part (3)”.

[Stacks, Tag 0856], part (3): the geometric stalk of the annihilator subsheaf. Let F be an algebraic space, I ⊆ 𝒪_F a quasi-coherent sheaf of ideals of finite type and G a quasi-coherent 𝒪_F-module. An element of the stalk of G at a geometric point x̄ is the germ of a section of the subsheaf annihilated by I exactly when every germ at x̄ of a section of I kills it; that is, G'_x̄ = {s ∈ G_x̄ | I_x̄ s = 0} inside G_x̄.

theorem exists_germ_annihilatorSubmodule_iff
    (hI : I.toSheafOfModules.IsQuasicoherentOnSite)
    (hIft : SheafOfModules.IsFiniteTypeOnSite I.toSheafOfModules)
    (x : GeometricPoint B S hS F)
    (s : geometricModuleStalk B S hS ⟨F, hF⟩ x G) :
    (∃ (N : SmallEtaleNeighborhood x)
        (t : (annihilatorSubmodule B S hS F hF I G).toSheafOfModules.val.obj (op N.chart)),
        geometricModuleStalkGerm B S hS ⟨F, hF⟩ x G N
          ((annihilatorSubmodule B S hS F hF I G).ι.val.app (op N.chart) t) = s) ↔
      ∀ (N : SmallEtaleNeighborhood x) (a : chartRing B S hS F hF N.chart),
        a ∈ I.obj (op N.chart) →
          etaleLocalRingGerm B S hS F x (op N) a • s = 0

AlgebraicGeometry.Space.isQuasicoherentOnSite_annihilatorSubmodule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IdealAnnihilatorQuasicoherentSpace.lean, line 179. The attribute's comment: “part (1)”.

The annihilator subsheaf is quasi-coherent. Let F be an algebraic space, I ⊆ 𝒪_F a quasi-coherent sheaf of ideals of finite type and G a quasi-coherent 𝒪_F-module. The subsheaf of sections of G annihilated by I is quasi-coherent.

theorem isQuasicoherentOnSite_annihilatorSubmodule
    (hI : I.toSheafOfModules.IsQuasicoherentOnSite)
    (hIft : SheafOfModules.IsFiniteTypeOnSite I.toSheafOfModules)
    (hG : G.IsQuasicoherentOnSite) :
    (annihilatorSubmodule B S hS F hF I G).toSheafOfModules.IsQuasicoherentOnSite

AlgebraicGeometry.Space.annihilatorSubmodule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IdealAnnihilatorSubsheaf.lean, line 79. The attribute's comment: “the subsheaf”.

The subsheaf of sections annihilated by an ideal sheaf on an algebraic space, the object of [Stacks, Tag 0856]. Its sections over an étale chart W are the sections of G over W all of whose restrictions are annihilated by the sections of I there, and that rule defines a submodule sheaf of G.

noncomputable def annihilatorSubmodule
    (I : (SheafOfModules.unit
      ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS F hF).O))).Submodule)
    (G : Modules.{u, u} B S hS F hF) : G.Submodule

AlgebraicGeometry.Space.mem_annihilatorSubmodule_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IdealAnnihilatorSubsheaf.lean, line 100. The attribute's comment: “the sections”.

The sections of the annihilator subsheaf of [Stacks, Tag 0856]. A section s of G over an étale chart is annihilated by I exactly when, over every chart W' over it, every section of I kills the restriction of s to W'.

theorem mem_annihilatorSubmodule_obj (W : (SmallEtale B S hS F)ᵒᵖ) (s : G.val.obj W) :
    s ∈ (annihilatorSubmodule B S hS F hF I G).toSubmodule.obj W ↔
      ∀ (W' : (SmallEtale B S hS F)ᵒᵖ) (g : W ⟶ W')
        (a : ((Stacks.SheafOfModules.Tensor.ringSheaf
            (smallEtaleRingedSite B S hS F hF).O)).obj.obj W'),
        a ∈ I.obj W' → a • G.val.restrictₛₗ g s = 0
Tag 0857, a definition

Tag 0857 in the Stacks Project.

Declarations registered for the tag:

Tag 0858, a lemma

Tag 0858 in the Stacks Project.

AlgebraicGeometry.Space.pushforwardSubmodule_annihilatorSubmodule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AnnihilatorSubsheafPushforward.lean, line 386.

[Stacks, Tag 0858]. Let f : X ⟶ Y be a morphism of algebraic spaces, I ⊆ 𝒪_Y a sheaf of ideals and M an 𝒪_X-module on the spaces-étale site. The direct image along f of the subsheaf of sections of M annihilated by f^{-1}I · 𝒪_X is the subsheaf of sections of f_*M annihilated by I.

The source assumes f quasi-compact and quasi-separated, I quasi-coherent of finite type and M quasi-coherent; all three are discharged as unnecessary, being needed in the source only so that the subsheaf of [Stacks, Tag 0857] is available for I and f_*M.

theorem pushforwardSubmodule_annihilatorSubmodule (f : X ⟶ Y)
    (I : (SheafOfModules.unit
      ((Stacks.SheafOfModules.Tensor.ringSheaf (spacesEtaleRingedSite B S hS Y).O))).Submodule)
    (M : SheafOfModules.{u + 1}
      ((Stacks.SheafOfModules.Tensor.ringSheaf (spacesEtaleRingedSite B S hS X).O))) :
    Stacks.SheafOfModules.pushforwardSubmodule (spacesEtaleSharpRing B S hS f) M
        (CoverPreserving.of_isContinuous _ _ _)
        (Stacks.SheafOfModules.annihilatorSubmodule M
          (RingedSite.mul_comm_ringSheaf (spacesEtaleRingedSite B S hS X))
          (Stacks.SheafOfModules.inverseImageIdeal (spacesEtaleSharpRing B S hS f) I)) =
      Stacks.SheafOfModules.annihilatorSubmodule
        ((_root_.SheafOfModules.pushforward.{u + 1}
          (spacesEtaleSharpRing B S hS f)).obj M)
        (RingedSite.mul_comm_ringSheaf (spacesEtaleRingedSite B S hS Y)) I
Tag 0859, a lemma

Tag 0859 in the Stacks Project.

AlgebraicGeometry.Space.sectionSupportedIn_iff_exists_pow_le_annihilator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartBasicOpenLocalization.lean, line 389. The attribute's comment: “part (2): the supported sections over an affine chart are the ideal-power torsion”.

Let T be a subset of the points of an algebraic space F, let U be an affine étale chart of F and let I be a finitely generated ideal of the regular functions on the chart whose zero locus is the preimage of T. A section of a quasi-coherent 𝒪_F-module over U is supported on T exactly when some power of I annihilates it.

Part (1), AlgebraicGeometry.Space.exists_fg_ideal_zeroLocus_eq_preimage_chartPointsMap, supplies such an I whenever T is closed and its complement is the point set of an open subspace with quasi-compact inclusion; AlgebraicGeometry.Space.chartRing of a chart is the ring of global functions on its scheme, so the two are ideals of the same ring.

Quasi-coherence enters only through AlgebraicGeometry.Space.IsCartesianOnAffineCharts, which it implies by Stacks 03DX; it is derived here rather than assumed, since Stacks 0859 already assumes the module quasi-coherent.

theorem sectionSupportedIn_iff_exists_pow_le_annihilator
    (G : Modules.{u, u} B S hS F hF) (hG : G.IsQuasicoherentOnSite)
    (T : Set (points B S hS F)) (U : SmallEtale B S hS F) (hU : IsAffine (chartScheme U))
    {I : Ideal (chartRing B S hS F hF U)} (hIfg : I.FG)
    (hI : chartPointsMap U ⁻¹' T =
      (chartScheme U).zeroLocus (U := ⊤) (I : Set (chartRing B S hS F hF U)))
    (s : G.val.obj (op U)) :
    SectionSupportedIn B S hS F hF T G U s ↔ ∃ n : ℕ, ∀ a ∈ I ^ n, a • s = 0

AlgebraicGeometry.Space.isQuasicoherentOnSite_supportedSectionsSubmodule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartBasicOpenLocalization.lean, line 650. The attribute's comment: “part (3): the subsheaf of sections supported on T is quasi-coherent”.

Let T ⊆ |F| be a closed subset of the points of an algebraic space F whose complement is the point set of an open subspace O ⊆ F with quasi-compact inclusion, and let G be a quasi-coherent 𝒪_F-module. Then the subsheaf of G of sections supported on T is again quasi-coherent.

The hypotheses are T closed, T ⨿ |O| = |F|, and O → F quasi-compact. Quasi-coherence of the subsheaf is SheafOfModules.IsQuasicoherentOnSite (Stacks 03DL (6)), the condition that cuts out AlgebraicGeometry.Space.QuasicoherentSheaves (Stacks 03G9); it follows from AlgebraicGeometry.Space.bijective_sectionsBaseChange_supportedSectionsSubmodule by Descent, Proposition 03DX (2), AlgebraicGeometry.Space.isQuasicoherentOnSite_iff_isCartesianOnAffineCharts.

theorem isQuasicoherentOnSite_supportedSectionsSubmodule
    (G : Modules.{u, u} B S hS F hF) (hG : G.IsQuasicoherentOnSite)
    {T : Set (points B S hS F)} (hT : IsClosed T) {O : Subfunctor F}
    (hO : IsOpenSubspace B S hS O)
    (hOT : Set.range (pointsMap B S hS O.toFunctor O.ι) = Tᶜ)
    (hOqc : IsQuasiCompact B S hS O.ι) :
    (supportedSectionsSubmodule B S hS F hF T G).toSheafOfModules.IsQuasicoherentOnSite

AlgebraicGeometry.Space.supportedSectionsSubmoduleData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedSectionsSubsheaf.lean, line 197. The attribute's comment: “supported-section subsheaf”.

The subsheaf of sections supported in T, together with its defining local membership criterion.

noncomputable def supportedSectionsSubmoduleData (T : Set (points B S hS F))
    (G : Modules.{u, m} B S hS F hF) :
    {N : G.Submodule // ∀ (W : SmallEtale B S hS F)
      (s : G.val.obj (op W)),
      s ∈ N.toSubmodule.obj (op W) ↔
        SectionSupportedIn B S hS F hF T G W s}

AlgebraicGeometry.Space.exists_fg_ideal_zeroLocus_eq_preimage_chartPointsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedSectionsSubsheaf.lean, line 294. The attribute's comment: “part (1): a finite type ideal cutting out the closed subset on an affine chart”.

Let T ⊆ |F| be a closed subset of the points of an algebraic space F, and let U ⊆ F be the open subspace whose points are the complement of T. If the inclusion U → F is quasi-compact then on every affine étale chart φ : W → F the preimage |φ|⁻¹(T) is the zero locus of a finitely generated ideal of 𝒪_F(W).

theorem exists_fg_ideal_zeroLocus_eq_preimage_chartPointsMap (hF : IsAlgebraicSpace B S hS F)
    {T : Set (points B S hS F)} (hT : IsClosed T) {U : Subfunctor F}
    (hU : IsOpenSubspace B S hS U)
    (hUT : Set.range (pointsMap B S hS U.toFunctor U.ι) = Tᶜ)
    (hUqc : IsQuasiCompact B S hS U.ι) (W : SmallEtale B S hS F)
    (hW : IsAffine (chartScheme W)) :
    ∃ I : Ideal Γ(chartScheme W, ⊤), I.FG ∧
      chartPointsMap W ⁻¹' T =
        (chartScheme W).zeroLocus (U := ⊤) (I : Set Γ(chartScheme W, ⊤))
Tag 085A, a definition

Tag 085A in the Stacks Project.

AlgebraicGeometry.Space.supportedSectionsSubmoduleData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedSectionsSubsheaf.lean, line 197. The attribute's comment: “the subsheaf of sections supported on T”.

The subsheaf of sections supported in T, together with its defining local membership criterion.

noncomputable def supportedSectionsSubmoduleData (T : Set (points B S hS F))
    (G : Modules.{u, m} B S hS F hF) :
    {N : G.Submodule // ∀ (W : SmallEtale B S hS F)
      (s : G.val.obj (op W)),
      s ∈ N.toSubmodule.obj (op W) ↔
        SectionSupportedIn B S hS F hF T G W s}
Tag 085B, a lemma

Tag 085B in the Stacks Project.

AlgebraicGeometry.Space.modulePushforward_supportedSectionsSubmodule_range_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedSectionsModulePushforward.lean, line 95. The attribute's comment: “the identification of the two subsheaves of the direct image, with the direct image spelled as the one of Stacks 03LU”.

Stacks 085B with the direct image spelled as the one of Stacks 03LU. For a morphism f : X ⟶ Y of algebraic spaces over S, a closed subset T of the points of Y and an 𝒪_X-module F, the direct image f_* of Stacks 03LU of the subsheaf of sections supported over |f|⁻¹T is the subsheaf of f_*F of sections supported on T: the two canonical inclusions into f_*F have the same image over every étale chart of Y.

This is the same identification as AlgebraicGeometry.Space.pushforward_supportedSectionsSubmodule_range_eq, which states it for the direct image attached to the morphism of ringed topoi of Stacks 03G8. Both spellings are registered, because consumers of the tag are written against one or the other and the passage between them is not available downstream: it is cheap only at the two small equations above, which is why it is made here.

theorem modulePushforward_supportedSectionsSubmodule_range_eq
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (T : Set (points B S hS Y.1))
    (hT : @IsClosed _ (pointTopology B S hS Y.1) T)
    (F : Modules.{u, u} B S hS X.1 X.2)
    (W : SmallEtale B S hS Y.1) :
    Set.range (((modulePushforward B S hS f).map
        (supportedSectionsSubmodule B S hS X.1 X.2
          (pointsMap B S hS X.1 f.hom ⁻¹' T) F).ι).val.app (op W)) =
      Set.range ((supportedSectionsSubmodule B S hS Y.1 Y.2 T
        ((modulePushforward B S hS f).obj F)).ι.val.app (op W))

AlgebraicGeometry.Space.pushforward_supportedSectionsSubmodule_range_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedSectionsPushforward.lean, line 1037. The attribute's comment: “the identification of the two subsheaves of the direct image”.

For a morphism f : X ⟶ Y of algebraic spaces over S, a closed subset T of the points of Y and an 𝒪_X-module F, the direct image of the subsheaf of sections supported over |f|⁻¹T is the subsheaf of f_*F of sections supported on T: the two canonical inclusions into f_*F have the same image over every étale chart of Y.

theorem pushforward_supportedSectionsSubmodule_range_eq
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (T : Set (points B S hS Y.1))
    (hT : @IsClosed _ (pointTopology B S hS Y.1) T)
    (F : Modules.{u, u} B S hS X.1 X.2)
    (W : SmallEtale B S hS Y.1) :
    Set.range ((((smallEtaleRingedToposHom B S hS f).pushforwardModules).map
      (supportedSectionsSubmodule B S hS X.1 X.2
        (pointsMap B S hS X.1 f.hom ⁻¹' T) F).ι).val.app (op W)) =
    Set.range (((supportedSectionsSubmodule B S hS Y.1 Y.2 T
      (((smallEtaleRingedToposHom B S hS f).pushforwardModules).obj F)).ι).val.app (op W))
Sources
LeanAlgebraicGeometry.Space.hasFiniteTypeQuasicoherentIdealZeroLocus_of_isQuasiCompactSpace · AlgebraicGeometry.Space.isQuasiCompactSpace_of_hasFiniteTypeQuasicoherentIdealZeroLocus · AlgebraicGeometry.Space.tfae_isQuasiCompact_openSubspace · AlgebraicGeometry.Space.isQuasiCompact_iff_isQuasiCompactSpace_openSubspace · AlgebraicGeometry.Space.mem_annihilatorSubmodule_obj_of_isAffine · AlgebraicGeometry.Space.exists_germ_annihilatorSubmodule_iff · AlgebraicGeometry.Space.isQuasicoherentOnSite_annihilatorSubmodule · AlgebraicGeometry.Space.annihilatorSubmodule

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.