32.2 Directed limits of schemes… to 32.21 Application to…

Section32.2 Directed limits of schemes with affine transition maps #

Section 32.2 of the Stacks Project, Tag 01YV. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01YV, the section

Tag 01YV in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.isLimitPullbackCone, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/CofilteredLimits/BaseChange.lean, line 151 (StacksFrontier): “base change commutes with the limit of the system (Lemma 01YZ)”.
AlgebraicGeometry.hasLimit_of_isCofiltered_of_isAffineHom, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/CofilteredLimits/Basic.lean, line 631 (StacksFrontier): “the construction of the limit of an inverse system of schemes whose transition morphisms are affine (Lemma 01YX)”.
AlgebraicGeometry.isAffineHom_π_app registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/CofilteredLimits/Basic.lean, line 634 (StacksFrontier): “the projections of the limit are affine (Lemma 01YX (1))”. References: EGA IV (8.13.4), “partial”.
AlgebraicGeometry.isLimitOpensCone registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/CofilteredLimits/Basic.lean, line 636 (StacksFrontier): “the inverse image of an open subscheme under a projection is the limit of its inverse images (Lemma 01YX (2))”.
AlgebraicGeometry.Scheme.affineLimitCone, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Limits/AffineTransition.lean, line 89 (StacksFrontier): “the construction of the limit when all the schemes of the system are affine: the limit cone is Spec of the colimit of the rings of global sections (Lemma 01YW)”.
AlgebraicGeometry.Scheme.hasLimit_of_isAffine, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Limits/AffineTransition.lean, line 92 (StacksFrontier): “existence of the limit when all the schemes of the system are affine (Lemma 01YW)”.

Tag 01YW, a lemma

Tag 01YW in the Stacks Project.

AlgebraicGeometry.Scheme.affineLimitCone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/AffineTransition.lean, line 54. The attribute's comment: “the limit cone, as Spec of the colimit of global sections”. References: SGA 4 VII (5.1), “all schemes affine”.

The limit cone of a diagram of affine schemes, with apex Spec applied to the limit in CommRingCatᵒᵖ of the diagram of rings of global sections.

noncomputable def affineLimitCone : LimitCone D

AlgebraicGeometry.Scheme.hasLimit_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/AffineTransition.lean, line 69. The attribute's comment: “existence of the limit”. References: SGA 4 VII (5.1), “all schemes affine”.

A diagram of affine schemes has a limit in the category of schemes.

theorem hasLimit_of_isAffine : HasLimit D

Tag 01YX, a lemma

Tag 01YX in the Stacks Project.

AlgebraicGeometry.hasLimit_of_isCofiltered_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CofilteredLimits/Basic.lean, line 605. The attribute's comment: “existence”. References: SGA 4 VII (5.1), “existence of lim”.

Limits of inverse systems with affine transition morphisms. A cofiltered diagram of schemes whose transition morphisms are affine has a limit in the category of schemes.

The limit is constructed by gluing, over the affine opens U of a fixed stage D i₀, the affine schemes lim_j (D j ×_{D i₀} U); see AlgebraicGeometry.CofilteredLimit.hasLimit_of_isAffineHom_of_isCofiltered.

theorem hasLimit_of_isCofiltered_of_isAffineHom
    {I : Type u} [Category.{u} I] [IsCofiltered I] (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] : HasLimit D

Declarations registered for the tag:

AlgebraicGeometry.isAffineHom_π_app registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/CofilteredLimits/Basic.lean, line 622 (StacksFrontier): “part (1)”. References: EGA IV (8.13.4), “partial”.
AlgebraicGeometry.isLimitOpensCone registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/CofilteredLimits/Basic.lean, line 624 (StacksFrontier): “part (2)”.

Tag 01YZ, a lemma

Tag 01YZ in the Stacks Project.

AlgebraicGeometry.isLimitPullbackCone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CofilteredLimits/BaseChange.lean, line 132.

Base change commutes with inverse limits of schemes. Let { Dⱼ } be an inverse system of schemes indexed by a cofiltered category, let c be a limit cone over it, let i be an index, and let f : T ⟶ Dᵢ be a scheme over the stage Dᵢ. Then (lim Dⱼ) ×_{Dᵢ} T = lim_{j ≥ i} (Dⱼ ×_{Dᵢ} T).

This is stated for an arbitrary limit cone c, so it applies in particular to the limit of a system with affine transition morphisms, whose existence is AlgebraicGeometry.hasLimit_of_isCofiltered_of_isAffineHom; that specialisation is recorded as AlgebraicGeometry.isLimitPullbackConeLimitCone.

def isLimitPullbackCone [IsCofiltered I] (i : I) (f : T ⟶ D.obj i) :
    IsLimit (pullbackCone D c i f)

Sources

LeanAlgebraicGeometry.isLimitPullbackCone · AlgebraicGeometry.hasLimit_of_isCofiltered_of_isAffineHom · AlgebraicGeometry.isAffineHom_π_app · AlgebraicGeometry.isLimitOpensCone · AlgebraicGeometry.Scheme.affineLimitCone · AlgebraicGeometry.Scheme.hasLimit_of_isAffine

Section32.3 Infinite products #

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

Tag 0CNI, a lemma

Tag 0CNI in the Stacks Project.

CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsConeIsLimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/InfiniteProducts.lean, line 202. The attribute's comment: “limit of finite subproducts”.

A product is canonically the inverse limit of its finite subproducts.

noncomputable def finiteSubproductsConeIsLimit [HasProduct X] :
    IsLimit (finiteSubproductsCone X)

AlgebraicGeometry.hasProduct_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/InfiniteProducts.lean, line 310. The attribute's comment: “existence”.

An arbitrary family of schemes affine over S has a product in the category of schemes over S.

theorem hasProduct_of_isAffineHom {I : Type u} (S : Scheme.{u})
    (T : I → Scheme.{u}) (f : ∀ i, T i ⟶ S) [∀ i, IsAffineHom (f i)] :
    HasProduct (fun i => Over.mk (f i))

AlgebraicGeometry.isAffineHom_finiteSubproductsCone_π_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/InfiniteProducts.lean, line 326. The attribute's comment: “affine projections”.

The canonical projection from the infinite product of a family of schemes affine over S onto any of its finite subproducts is affine.

theorem isAffineHom_finiteSubproductsCone_π_app {I : Type u} (S : Scheme.{u})
    (T : I → Scheme.{u}) (f : ∀ i, T i ⟶ S) [∀ i, IsAffineHom (f i)]
    [HasProduct (fun i => Over.mk (f i))] (J : (Finset (Discrete I))ᵒᵖ) :
    IsAffineHom ((finiteSubproductsCone (fun i => Over.mk (f i))).π.app J).left

Tag 0CNJ, a lemma

Tag 0CNJ in the Stacks Project.

AlgebraicGeometry.surjective_product_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/InfiniteProductsSurjective.lean, line 94.

Stacks Project, Tag 0CNJ. The structure morphism of the product over S of surjective affine morphisms is surjective.

theorem surjective_product_hom {I : Type u} (S : Scheme.{u})
    (T : I → Scheme.{u}) (f : ∀ i, T i ⟶ S) [∀ i, IsAffineHom (f i)]
    [∀ i, Surjective (f i)] :
    letI := hasProduct_of_isAffineHom S T f
    Surjective (∏ᶜ (fun i ↦ Over.mk (f i))).hom

Tag 0CNK, a lemma

Tag 0CNK in the Stacks Project.

AlgebraicGeometry.isIntegralHom_product, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/InfiniteProductsIntegral.lean, line 106.

Stacks Project, Tag 0CNK. The product over a scheme of an arbitrary family of integral morphisms is integral over the base.

theorem isIntegralHom_product {I : Type u} (S : Scheme.{u})
    (T : I → Scheme.{u}) (f : ∀ i, T i ⟶ S) [∀ i, IsIntegralHom (f i)] :
    letI : HasProduct (fun i ↦ Over.mk (f i)) := hasProduct_of_isAffineHom S T f
    IsIntegralHom (∏ᶜ (fun i ↦ Over.mk (f i))).hom

Sources

LeanCategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsConeIsLimit · AlgebraicGeometry.hasProduct_of_isAffineHom · AlgebraicGeometry.isAffineHom_finiteSubproductsCone_π_app · AlgebraicGeometry.surjective_product_hom · AlgebraicGeometry.isIntegralHom_product

Section32.4 Descending properties #

Section 32.4 of the Stacks Project, Tag 081A. 18 tags here are carried by 26 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CUE, a lemma

Tag 0CUE in the Stacks Project.

AlgebraicGeometry.preservesLimit_forget_of_isCofiltered_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/UnderlyingSpace.lean, line 142.

Passing to underlying sets preserves the limit of a cofiltered diagram of schemes with affine transition morphisms.

theorem preservesLimit_forget_of_isCofiltered_of_isAffineHom
    {I : Type u} [Category.{u} I] [IsCofiltered I] (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] :
    PreservesLimit D Scheme.forget

Tag 0CUF, a lemma

Tag 0CUF in the Stacks Project.

AlgebraicGeometry.preservesLimit_forgetToTop_of_isCofiltered_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/UnderlyingSpace.lean, line 98. References: EGA IV (8.2.9).

Passing to underlying topological spaces preserves the limit of a cofiltered diagram of schemes with affine transition morphisms.

theorem preservesLimit_forgetToTop_of_isCofiltered_of_isAffineHom
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] :
    PreservesLimit D Scheme.forgetToTop

Tag 0CUG, a lemma

Tag 0CUG in the Stacks Project.

AlgebraicGeometry.existsUnique_mem_closure_singleton_of_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/PointClosure.lean, line 59. The attribute's comment: “closures_sets”.

Stacks Project, Tag 0CUG. The closure of a point in a cofiltered limit of schemes with affine transition morphisms is the inverse limit, as a set, of the closures of its images.

theorem existsUnique_mem_closure_singleton_of_compatible
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)]
    (c : Cone D) (hc : IsLimit c) (s : c.pt)
    (x : ∀ i, D.obj i)
    (hx : ∀ ⦃i j : I⦄ (f : i ⟶ j), D.map f (x i) = x j)
    (hx_closure : ∀ i, x i ∈ closure ({c.π.app i s} : Set (D.obj i))) :
    ∃! y : c.pt, y ∈ closure ({s} : Set c.pt) ∧ ∀ i, c.π.app i y = x i

AlgebraicGeometry.exists_isLimit_reducedClosures, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/PointClosure.lean, line 262. The attribute's comment: “closures_schemes”.

Stacks Project, Tag 0CUG. The reduced closure of a point of a cofiltered limit of schemes is the limit, as a scheme, of the reduced closures of its images.

theorem exists_isLimit_reducedClosures
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)]
    (c : Cone D) (hc : IsLimit c) (s : c.pt) :
    ∃ (E : I ⥤ Scheme.{u}) (ι : E ⟶ D) (c' : Cone E)
      (e : c'.pt ≅ (Scheme.IdealSheafData.vanishingIdeal
        (Closeds.closure ({s} : Set c.pt))).subscheme),
      (∀ i, ∃ eᵢ : E.obj i ≅ (Scheme.IdealSheafData.vanishingIdeal
        (Closeds.closure ({c.π.app i s} : Set (D.obj i)))).subscheme,
        eᵢ.hom ≫ (Scheme.IdealSheafData.vanishingIdeal
          (Closeds.closure ({c.π.app i s} : Set (D.obj i)))).subschemeι = ι.app i) ∧
      (∀ i, c'.π.app i ≫ ι.app i =
        e.hom ≫ (Scheme.IdealSheafData.vanishingIdeal
          (Closeds.closure ({s} : Set c.pt))).subschemeι ≫ c.π.app i) ∧
      Nonempty (IsLimit c')

AlgebraicGeometry.residueField_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/ResidueField.lean, line 100. The attribute's comment: “residue_fields”.

Stacks Project, Tag 0CUG. The residue field of a point in a cofiltered limit of schemes with affine transition morphisms is the filtered colimit of the residue fields of its images.

theorem residueField_isColimit
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)]
    (c : Cone D) (hc : IsLimit c) (s : c.pt)
    (K : Iᵒᵖ ⥤ CommRingCat.{u})
    (e : ∀ i : I,
      K.obj (Opposite.op i) ≅ (D.obj i).residueField (c.π.app i s))
    (hK : ∀ {i j : I} (f : i ⟶ j),
      K.map f.op =
        (e j).hom ≫
          ((D.obj j).residueFieldCongr (by
            symm
            change (c.π.app i ≫ D.map f) s = _
            rw [c.w f])).hom ≫
          (D.map f).residueFieldMap (c.π.app i s) ≫ (e i).inv) :
    ∀ (T : CommRingCat.{u})
      (φ : ∀ i : I, K.obj (Opposite.op i) ⟶ T),
      (∀ {i j : I} (f : i ⟶ j), K.map f.op ≫ φ i = φ j) →
      ∃! ψ : c.pt.residueField s ⟶ T,
        ∀ i : I, (e i).hom ≫ (c.π.app i).residueFieldMap s ≫ ψ = φ i

Tag 086P, a situation

Tag 086P in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.DescentSituation, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Limits/Descending/DescentSituation.lean, line 48 (StacksFrontier).

Tag 01YY, a lemma

Tag 01YY in the Stacks Project.

AlgebraicGeometry.nonempty_isLimit_forget_mapCone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/DescentSituation.lean, line 109. The attribute's comment: “part (1)”.

Stacks Project, Tag 01YY, part (1). The underlying-set cone of the chosen limit in the descent situation is a limit cone.

theorem nonempty_isLimit_forget_mapCone
    {I : Type v} [Small.{u} I] [Preorder I] [IsDirected I (· ≤ ·)]
    (D : DescentSituation.{v, u} I) :
    Nonempty (IsLimit (Scheme.forget.mapCone D.limitCone))

AlgebraicGeometry.nonempty_isLimit_forgetToTop_mapCone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/DescentSituation.lean, line 119. The attribute's comment: “part (2)”.

Stacks Project, Tag 01YY, part (2). The underlying topological-space cone of the chosen limit in the descent situation is a limit cone.

theorem nonempty_isLimit_forgetToTop_mapCone
    {I : Type v} [Small.{u} I] [Preorder I] [IsDirected I (· ≤ ·)]
    (D : DescentSituation.{v, u} I) :
    Nonempty (IsLimit (Scheme.forgetToTop.mapCone D.limitCone))

AlgebraicGeometry.exists_not_specializes_map_of_not_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/DescentSituation.lean, line 130. The attribute's comment: “part (3)”.

Stacks Project, Tag 01YY, part (3). If one point of the limiting scheme does not specialize to another, this failure is detected after projection to one of the schemes in the inverse system.

theorem exists_not_specializes_map_of_not_specializes
    {I : Type v} [Small.{u} I] [Preorder I] [IsDirected I (· ≤ ·)]
    (D : DescentSituation.{v, u} I)
    (s s' : D.limitCone.pt) (h : ¬Specializes s s') :
    ∃ i : I, ¬Specializes
      (D.limitCone.π.app (Opposite.op i) s)
      (D.limitCone.π.app (Opposite.op i) s')

Tag 01Z0, a lemma

Tag 01Z0 in the Stacks Project.

AlgebraicGeometry.isStagesColimit_stagePullbackSection_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ModuleLimits/SectionsColimitFinitePresentation.lean, line 184. The attribute's comment: “for a module of finite presentation on the base stage, with the index set in the universe of the schemes”. References: EGA IV (8.5.2), “(i), special case”; EGA IV (8.5.4), “special case”.

[Stacks Project, Tag 01Z0] for a module of finite presentation on the base stage. Let E be a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms, let c be a limit cone on it, let 0 be a chosen index and let ℱ₀ be a module of finite presentation on S₀ = E.obj (op 0). Setting ℱᵢ = f_{i0}⁺ℱ₀ for i ≥ 0 and ℱ = f_0⁺ℱ₀, the group Γ(S, ℱ) is the filtered colimit of the Γ(Sᵢ, ℱᵢ), in the elementwise form Stacks.IsStagesColimit: the maps to Γ(S, ℱ) are compatible with the transition maps, every global section at the limit comes from a stage, and two global sections at one stage with the same image at the limit already agree at a later stage.

The three clauses are, in order, Stacks.AlgebraicGeometry.ModuleLimits.sectionsMap_canHom_modulePullbackSection_comp, Stacks.AlgebraicGeometry.ModuleLimits.exists_canonical_section_eq_of_isLimit and ...ModuleLimits.exists_canonical_section_eq_of_canonical_section_eq_of_isLimit — the cocone law for the canonical identification of an iterated pullback with the pullback along the composite, and the surjectivity and injectivity halves, both of which read a global section of a module as a morphism out of the structure sheaf and then apply [Stacks Project, Tag 01ZR], (2) and (3) respectively. That is why the coefficients are restricted to a module of finite presentation: Tag 01ZR is a statement about finitely presented modules.

The tag is keyed because this is only part of Stacks 01Z0: the coefficient module is of finite presentation and not merely quasi-coherent. The whole tag is AlgebraicGeometry.isStagesColimit_stagePullbackSection_of_isQuasicoherent in StacksFrontier/AlgebraicGeometry/ModuleLimits/SectionsColimitQuasiCoherent.lean, which is this statement interchanged with [Stacks Project, Tag 01PJ]. The index set lies in the universe of the schemes, which is not a restriction that may be dropped — Stacks.LimitSectionsIdentification.not_card_01Z0 refutes the statement over an index set one universe up.

theorem isStagesColimit_stagePullbackSection_of_isFinitePresentation
    [∀ {i j : αᵒᵖ} (f : i ⟶ j), IsAffineHom (E.map f)]
    [∀ i : αᵒᵖ, CompactSpace (E.obj i)] [∀ i : αᵒᵖ, QuasiSeparatedSpace (E.obj i)]
    (c : Cone E) (hc : IsLimit c) (a₀ : α) (F₀ : (E.obj (op a₀)).Modules)
    (hF₀ : F₀.IsFinitePresentation) :
    Stacks.IsStagesColimit
      (fun (a b : {a : α // a₀ ≤ a}) (h : a ≤ b) =>
        stagePullbackSectionTransition E a.2 b.2 (Subtype.coe_le_coe.mpr h) F₀)
      (fun a : {a : α // a₀ ≤ a} => stagePullbackSectionProjection E a.2 F₀ c)

AlgebraicGeometry.isStagesColimit_stagePullbackSection_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ModuleLimits/SectionsColimitQuasiCoherent.lean, line 198. References: EGA IV (8.5.4).

[Stacks Project, Tag 01Z0]. Let E be a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms, let c be a limit cone on it, let 0 be a chosen index and let ℱ₀ be a quasi-coherent module on S₀ = E.obj (op 0). Setting ℱᵢ = f_{i0}⁺ℱ₀ for i ≥ 0 and ℱ = f_0⁺ℱ₀, the group Γ(S, ℱ) is the filtered colimit of the Γ(Sᵢ, ℱᵢ), in the elementwise form Stacks.IsStagesColimit: the maps to Γ(S, ℱ) are compatible with the transition maps, every global section at the limit comes from a stage, and two global sections at one stage with the same image at the limit already agree at a later stage.

The finite-presentation case is AlgebraicGeometry.isStagesColimit_stagePullbackSection_of_isFinitePresentation, and this is it interchanged with the presentation of a quasi-coherent module as a filtered colimit of finitely presented ones, [Stacks Project, Tag 01PJ]; see the file's implementation notes.

The index set lies in the universe of the schemes, which is not a restriction that may be dropped — Stacks.LimitSectionsIdentification.not_card_01Z0 refutes the statement over an index set one universe up, so a u-small directed index set is exactly the source's "directed set".

theorem isStagesColimit_stagePullbackSection_of_isQuasicoherent
    [∀ {i j : αᵒᵖ} (f : i ⟶ j), IsAffineHom (E.map f)]
    [∀ i : αᵒᵖ, CompactSpace (E.obj i)] [∀ i : αᵒᵖ, QuasiSeparatedSpace (E.obj i)]
    (c : Cone E) (hc : IsLimit c) (a₀ : α) (F₀ : (E.obj (op a₀)).Modules)
    (hF₀ : F₀.IsQuasicoherent) :
    Stacks.IsStagesColimit
      (fun (a b : {a : α // a₀ ≤ a}) (h : a ≤ b) =>
        stagePullbackSectionTransition E a.2 b.2 (Subtype.coe_le_coe.mpr h) F₀)
      (fun a : {a : α // a₀ ≤ a} => stagePullbackSectionProjection E a.2 F₀ c)

AlgebraicGeometry.isStagesColimit_appTop_of_isAffine_of_isLimit_of_directed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/SectionsColimitDescent.lean, line 254. The attribute's comment: “for the structure sheaf over a directed inverse system of affine schemes, with the index set in the universe of the schemes”. References: EGA IV (8.5.4), “special case”; SGA 3 VIB (10.0), “(i), special case”.

The ring of global sections of a limit of affine schemes is the filtered colimit of the rings of global sections of the stages, in the elementwise form Stacks.IsStagesColimit: the transition maps are the pullbacks of global sections along the morphisms of the inverse system and the maps to the vertex are the pullbacks along the projections of the limiting cone.

theorem isStagesColimit_appTop_of_isAffine_of_isLimit_of_directed :
    Stacks.IsStagesColimit (G := fun a : α => (Γ(E.obj (op a), ⊤) : Type u))
      (T := (Γ(c.pt, ⊤) : Type u))
      (fun (a b : α) (h : a ≤ b) x => (E.map (homOfLE h).op).appTop.hom x)
      (fun (a : α) x => (c.π.app (op a)).appTop.hom x)

AlgebraicGeometry.isStagesColimit_appTop_of_isLimit_of_directed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/SectionsColimitDescent.lean, line 284. The attribute's comment: “for the structure sheaf over a directed inverse system of quasi-compact quasi-separated schemes with affine transition morphisms, with the index set in the universe of the schemes”. References: EGA IV (8.5.4), “structure sheaf”.

The ring of global sections of a limit of quasi-compact quasi-separated schemes with affine transition morphisms is the filtered colimit of the rings of global sections of the stages, in the elementwise form Stacks.IsStagesColimit: the transition maps are the pullbacks of global sections along the morphisms of the inverse system and the maps to the vertex are the pullbacks along the projections of the limiting cone.

theorem isStagesColimit_appTop_of_isLimit_of_directed :
    Stacks.IsStagesColimit (G := fun a : α => (Γ(E.obj (op a), ⊤) : Type u))
      (T := (Γ(c.pt, ⊤) : Type u))
      (fun (a b : α) (h : a ≤ b) x => (E.map (homOfLE h).op).appTop.hom x)
      (fun (a : α) x => (c.π.app (op a)).appTop.hom x)

Tag 05F3, a lemma

Tag 05F3 in the Stacks Project.

AlgebraicGeometry.eventually_isEmpty_pullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/ConstructibleImage.lean, line 56. References: EGA IV (8.3.6), “Nontrivial direction”.

Stacks Project, Tag 05F3. If the base change of a quasi-compact scheme to the limit of a directed inverse system is empty, then its base change to every sufficiently late stage is empty.

lemma eventually_isEmpty_pullback
    {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)]
    (D : DescentSituation.{u, u} I)
    (T : Scheme.{u}) [CompactSpace T]
    (t : T ⟶ D.system.obj (Opposite.op D.base))
    (hT : IsEmpty
      (pullback t (D.limitCone.π.app (Opposite.op D.base)) : Scheme)) :
    ∀ᶠ i in Filter.atTop, ∀ h : D.base ≤ i,
      IsEmpty (pullback t (D.system.map (homOfLE h).op) : Scheme)

Tag 05F4, a lemma

Tag 05F4 in the Stacks Project.

AlgebraicGeometry.eventually_range_transition_subset_of_isLocallyConstructible, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/ConstructibleImage.lean, line 123.

Stacks Project, Tag 05F4. A locally constructible subset of a stage in a directed inverse system contains the images of all sufficiently large stages if it contains the image of the limit.

lemma eventually_range_transition_subset_of_isLocallyConstructible
    {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)]
    (D : DescentSituation.{u, u} I)
    (E : Set (D.system.obj (op D.base)))
    (hE : Topology.IsLocallyConstructible E)
    (hlim : Set.range (D.limitCone.π.app (op D.base)).base ⊆ E) :
    ∀ᶠ i in atTop, ∃ h : D.base ≤ i,
      Set.range (D.system.map (homOfLE h).op).base ⊆ E

Tag 01Z4, a lemma

Tag 01Z4 in the Stacks Project.

AlgebraicGeometry.exists_iSup_map_preimage_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LimitSituation.lean, line 175. The attribute's comment: “(3)”.

Stacks 01Z4, part (3). Let X = lim X_i be the limit of a cofiltered inverse system of quasi-compact schemes with affine transition morphisms. If a family of opens of a stage X_i has inverse images in X covering X, then for some transition morphism X_j ⟶ X_i the inverse images of the family in X_j cover X_j.

The source states this for a finite family of quasi-compact opens. Neither hypothesis is used: a preimage of opens commutes with arbitrary suprema, so the statement for the single open ⨆ k, V k is the statement for the family. What the proof does use, and what Situation 086P provides, is that every stage is quasi-compact.

The single-open case is Mathlib's AlgebraicGeometry.exists_map_eq_top, used here through AlgebraicGeometry.exists_map_eq_top', its index-morphism-universe-free form, and the step from one open to a family is AlgebraicGeometry.Scheme.Hom.preimage_iSup. Mathlib records the tag for parts (1) and (2) only, on AlgebraicGeometry.exists_preimage_eq and AlgebraicGeometry.exists_map_preimage_eq_map_preimage; its exists_map_eq_top carries no tag, so part (3) is recorded here.

theorem exists_iSup_map_preimage_eq_top {I : Type u} [Category.{v} I] [IsCofiltered I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] [∀ i : I, CompactSpace (D.obj i)]
    {i : I} {ι : Type*} (V : ι → (D.obj i).Opens)
    (hV : (⨆ k, c.π.app i ⁻¹ᵁ V k) = ⊤) :
    ∃ (j : I) (f : j ⟶ i), (⨆ k, D.map f ⁻¹ᵁ V k) = ⊤

Tag 01Z6, a lemma

Tag 01Z6 in the Stacks Project.

AlgebraicGeometry.eventually_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/Affine.lean, line 64. The attribute's comment: “for an index preorder essentially small in the scheme universe”. References: SGA 4 VII (5.4), “partial”.

Stacks Project, Tag 01Z6. In a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms, if the limit is affine then every sufficiently late stage is affine.

theorem eventually_isAffine
    {I : Type v} [Preorder I] [IsDirected I (· ≤ ·)]
    [EssentiallySmall.{u} I]
    (d : DescentSituation.{v, u} I)
    [IsAffine d.limitCone.pt] :
    ∃ i₀ : I, ∀ i : I, i₀ ≤ i → IsAffine (d.system.obj (op i))

Tag 086Q, a lemma

Tag 086Q in the Stacks Project.

AlgebraicGeometry.eventually_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/Descending/Separated.lean, line 579.

Stacks Project, Tag 086Q. In a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms, if the limit is separated then every sufficiently late stage is separated.

theorem eventually_isSeparated
    {I : Type v} [Preorder I] [IsDirected I (· ≤ ·)]
    [EssentiallySmall.{u} I]
    (d : DescentSituation.{v, u} I)
    [d.limitCone.pt.IsSeparated] :
    ∃ i₀ : I, ∀ i : I, i₀ ≤ i → (d.system.obj (Opposite.op i)).IsSeparated

Tag 09MT, a lemma

Tag 09MT in the Stacks Project.

Stacks.AlgebraicGeometry.AmpleLimit.exists_isAmple_pullback_map_of_isLimit_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleLimit/Unconditional.lean, line 511.

[Stacks Project, Tag 09MT]. Let c be a limit cone on a cofiltered diagram D of quasi-compact quasi-separated schemes with affine transition morphisms and let M be an invertible module on the stage D.obj j. If the pullback of M to c.pt is ample, then the pullback of M to some stage over j is ample.

This is exists_isAmple_pullback_map_of_isLimit with its hypothesis hdesc discharged by nonvanishingLocusDescent_of_isLimit, which derives it from [Stacks Project, Tag 01ZR] (2).

theorem exists_isAmple_pullback_map_of_isLimit_of_qcqs (hc : IsLimit c) (j : I)
    (M : (D.obj j).Modules)
    [_root_.AlgebraicGeometry.SheafOfModules.IsInvertible (D.obj j).toRingedSpace.presheaf
      (structureSheafRing (D.obj j).toRingedSpace).property M]
    (hample : Scheme.Modules.IsAmple c.pt ((Scheme.Modules.pullback (c.π.app j)).obj M)) :
    ∃ (j' : I) (g : j' ⟶ j),
      Scheme.Modules.IsAmple (D.obj j') ((Scheme.Modules.pullback (D.map g)).obj M)

Tag 081B, a lemma

Tag 081B in the Stacks Project.

AlgebraicGeometry.EventualLimit.eventually_isClosedImmersion_comp_π_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EventualLimitProperties/ClosedImmersion.lean, line 309. The attribute's comment: “part (1)”.

Stacks 081B (1). Let X = lim Xᵢ be the limit of a directed inverse system of quasi-compact schemes over S whose transition morphisms are affine. If f : Y ⟶ X is a closed immersion and Y is locally of finite type over S, then the composite Y ⟶ Xᵢ is a closed immersion for all sufficiently large i.

theorem eventually_isClosedImmersion_comp_π_app
    (hcomm : c.π ≫ t = (Functor.const Iᵒᵖ).map s)
    [∀ i : I, CompactSpace (D.obj (op i))]
    [∀ ⦃i j : I⦄ (h : i ≤ j), IsAffineHom (D.map (homOfLE h).op)]
    [LocallyOfFiniteType (f ≫ s)] [IsClosedImmersion f] :
    ∀ᶠ i in atTop, IsClosedImmersion (f ≫ c.π.app (op i))

AlgebraicGeometry.EventualLimit.eventually_isImmersion_comp_π_app_of_quasiSeparatedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EventualLimitProperties/Immersion.lean, line 465. The attribute's comment: “part (2)”.

Stacks 081B (2). Let X = lim Xᵢ be the limit of a directed inverse system of schemes over S whose transition morphisms are affine and whose stages are quasi-separated. If f : Y ⟶ X is an immersion, Y is locally of finite type over S, and Y is quasi-compact, then the composite Y ⟶ Xᵢ is an immersion for all sufficiently large i.

These are exactly the source's hypotheses, and the index type I is in a universe unrelated to that of the schemes. AlgebraicGeometry.EventualLimit.eventually_isImmersion_comp_π_app drops the quasi-separatedness of the stages but ties I to the universe of the schemes, which is where Mathlib's AlgebraicGeometry.exists_preimage_eq applies.

theorem eventually_isImmersion_comp_π_app_of_quasiSeparatedSpace
    (hcomm : c.π ≫ t = (Functor.const Iᵒᵖ).map s)
    [∀ i : I, QuasiSeparatedSpace (D.obj (op i))]
    [∀ ⦃i j : I⦄ (h : i ≤ j), IsAffineHom (D.map (homOfLE h).op)]
    [LocallyOfFiniteType (f ≫ s)] [IsImmersion f] [CompactSpace Y] :
    ∀ᶠ i in atTop, IsImmersion (f ≫ c.π.app (op i))

AlgebraicGeometry.EventualLimit.eventually_isIso_comp_π_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EventualLimitProperties/Isomorphism.lean, line 258. The attribute's comment: “eventually_isomorphism”.

Stacks 081B (3), in the form in which the limit is presented through an isomorphism f : Y ≅ lim Xᵢ: the composites Y ⟶ Xᵢ are isomorphisms for all sufficiently large i.

theorem eventually_isIso_comp_π_app (hp : c.π ≫ t = (Functor.const Iᵒᵖ).map p)
    {Y : Scheme.{u}} (f : Y ⟶ c.pt) [IsIso f]
    [∀ i : I, CompactSpace (D.obj (op i))]
    [∀ i : I, LocallyOfFiniteType (t.app (op i))]
    [∀ ⦃i j : I⦄ (h : i ≤ j), IsClosedImmersion (D.map (homOfLE h).op)]
    [LocallyOfFinitePresentation (f ≫ p)] :
    ∀ᶠ i in atTop, IsIso (f ≫ c.π.app (op i))

Tag 01ZH, a lemma

Tag 01ZH in the Stacks Project.

AlgebraicGeometry.eventually_isSeparated_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/EventuallySeparatedOverBase.lean, line 240.

Stacks Project, Tag 01ZH. Let S be a quasi-separated scheme and let X = lim X_i be a directed inverse limit of quasi-compact and quasi-separated schemes over S with affine transition morphisms. If X ⟶ S is separated, then X_i ⟶ S is separated for all sufficiently large i.

theorem eventually_isSeparated_app {I : Type v} [Preorder I] [IsDirected I (· ≤ ·)]
    [EssentiallySmall.{u} I] (d : DescentSituation.{v, u} I) {S : Scheme.{u}}
    [QuasiSeparatedSpace S] (t : d.system ⟶ (Functor.const Iᵒᵖ).obj S)
    (hsep : IsSeparated (d.limitCone.π.app (op d.base) ≫ t.app (op d.base))) :
    ∃ i₀ : I, ∀ i : I, i₀ ≤ i → IsSeparated (t.app (op i))

Tag 09ZM, a lemma

Tag 09ZM in the Stacks Project.

AlgebraicGeometry.eventually_isAffineHom_of_isLimit_of_initiallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/EventuallyAffine.lean, line 240.

AlgebraicGeometry.eventually_isAffineHom_of_isLimit with the index universes independent of the scheme universe, at the cost of CategoryTheory.LocallySmall.{u} and CategoryTheory.InitiallySmall.{u} on the index category. See the module documentation for why some such condition is necessary.

theorem eventually_isAffineHom_of_isLimit_of_initiallySmall (D : I ⥤ Scheme.{u})
    (t : D ⟶ (Functor.const I).obj S) (c : Cone D) (hc : IsLimit c) (f : c.pt ⟶ S)
    (hf : c.π ≫ t = (Functor.const I).map f)
    [∀ i, CompactSpace (D.obj i)] [∀ i, QuasiSeparatedSpace (D.obj i)]
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)] [IsAffineHom f] :
    ∃ i : I, ∀ {j : I} (_ : j ⟶ i), IsAffineHom (t.app j)

Tag 09ZN, a lemma

Tag 09ZN in the Stacks Project.

AlgebraicGeometry.eventually_isFinite_of_isLimit_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EventualFiniteness/Basic.lean, line 371.

Stacks 09ZN for a directed preorder. In a directed inverse system of qcqs schemes over a qcqs scheme, if the transition morphisms are finite, the stages are locally of finite type over the base, and the limit is integral over the base, then the stages are eventually finite over the base.

The index type is taken in the same universe as the schemes; see the module docstring.

theorem eventually_isFinite_of_isLimit_of_isIntegral
    {I : Type u} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    {S : Scheme.{u}} [CompactSpace S] [QuasiSeparatedSpace S]
    (F : Iᵒᵖ ⥤ Scheme.{u}) (p : F ⟶ (Functor.const Iᵒᵖ).obj S)
    (c : Cone F) (hc : IsLimit c) (f : c.pt ⟶ S)
    (hf : ∀ i, f = c.π.app (Opposite.op i) ≫ p.app (Opposite.op i))
    [IsIntegralHom f]
    [∀ i, CompactSpace (F.obj (Opposite.op i))]
    [∀ i, QuasiSeparatedSpace (F.obj (Opposite.op i))]
    (haffine : ∀ {i j : I} (h : i ≤ j),
      IsAffineHom (F.map (homOfLE h).op))
    (hfinite : ∀ {i j : I} (h : i ≤ j),
      IsFinite (F.map (homOfLE h).op))
    [∀ i, LocallyOfFiniteType (p.app (Opposite.op i))] :
    ∀ᶠ i in Filter.atTop, IsFinite (p.app (Opposite.op i))

Tag 0A0N, a lemma

Tag 0A0N in the Stacks Project.

AlgebraicGeometry.eventually_isClosedImmersion_app_of_isLimit_of_initiallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/EventuallyClosedImmersion.lean, line 427.

AlgebraicGeometry.eventually_isClosedImmersion_app_of_isLimit with the index universes independent of the scheme universe, at the cost of CategoryTheory.LocallySmall.{u} and CategoryTheory.InitiallySmall.{u} on the index category.

This is the faithful rendering of Tag 0A0N: the source's limit is indexed by a directed set, so the index is small relative to the schemes and the smallness is part of the statement rather than an addition to it. See the module documentation, and compare AlgebraicGeometry.eventually_isAffineHom_of_isLimit_of_initiallySmall (Tag 09ZM), which carries the condition for the same reason and whose counterexample shows it cannot be dropped.

theorem eventually_isClosedImmersion_app_of_isLimit_of_initiallySmall (D : I ⥤ Scheme.{u})
    (t : D ⟶ (Functor.const I).obj S) (c : Cone D) (hc : IsLimit c) (f : c.pt ⟶ S)
    (hf : c.π ≫ t = (Functor.const I).map f)
    [CompactSpace S] [QuasiSeparatedSpace S]
    [∀ i, CompactSpace (D.obj i)] [∀ i, QuasiSeparatedSpace (D.obj i)]
    [∀ {i j : I} (g : i ⟶ j), IsClosedImmersion (D.map g)]
    [∀ i, LocallyOfFiniteType (t.app i : D.obj i ⟶ S)] [IsClosedImmersion f] :
    ∃ i : I, ∀ {j : I} (_ : j ⟶ i), IsClosedImmersion (t.app j : D.obj j ⟶ S)

Tag 0GIH, a lemma

Tag 0GIH in the Stacks Project.

AlgebraicGeometry.eventually_isImmersion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/RelativeApproximation/ClosedImmersionDescent.lean, line 797.

Stacks Project, Tag 0GIH. In a directed inverse system of quasi-compact and quasi-separated schemes whose transition morphisms are closed immersions, if all the structure morphisms to a quasi-separated base are locally of finite type and the morphism induced on the limit is an immersion, then the structure morphisms are immersions for all sufficiently large indices. Nonempty I is not a weakening: it is what makes Filter.atTop on the index a PROPER filter. Over an empty index atTop = ⊥ and the conclusion would be vacuously true, so this hypothesis is what rules vacuity out. The source assumes it too — a directed limit is indexed by a directed set, which is nonempty by convention.

lemma eventually_isImmersion {I : Type v} [Preorder I]
    [IsDirected I (· ≤ ·)] [Small.{u} I]
    {S : Scheme.{u}} (D : Iᵒᵖ ⥤ Scheme.{u})
    (t : D ⟶ (Functor.const Iᵒᵖ).obj S) (c : Cone D) (hc : IsLimit c)
    (f : c.pt ⟶ S)
    [QuasiSeparatedSpace S]
    [∀ i, CompactSpace (D.obj (op i))]
    [∀ i, QuasiSeparatedSpace (D.obj (op i))]
    [∀ ⦃i j : I⦄ (h : i ≤ j), IsClosedImmersion (D.map (homOfLE h).op)]
    [∀ i, LocallyOfFiniteType (t.app (op i))]
    (hcomm : c.π ≫ t = (Functor.const Iᵒᵖ).map f)
    [IsImmersion f] :
    ∀ᶠ i in atTop, IsImmersion (t.app (op i))

Sources

LeanAlgebraicGeometry.preservesLimit_forget_of_isCofiltered_of_isAffineHom · AlgebraicGeometry.preservesLimit_forgetToTop_of_isCofiltered_of_isAffineHom · AlgebraicGeometry.existsUnique_mem_closure_singleton_of_compatible · AlgebraicGeometry.exists_isLimit_reducedClosures · AlgebraicGeometry.residueField_isColimit · AlgebraicGeometry.DescentSituation · AlgebraicGeometry.nonempty_isLimit_forget_mapCone · AlgebraicGeometry.nonempty_isLimit_forgetToTop_mapCone

Section32.5 Absolute Noetherian Approximation #

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

Tag 01Z7, a lemma

Tag 01Z7 in the Stacks Project.

Stacks.FiniteTypeOpenModel.exists_openModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/FiniteTypeOpenModel.lean, line 521. The attribute's comment: “existence of a finite-type open model”. References: EGA II (5.1.9), “base Spec ℤ, affine”.

An open immersion of a finite-type scheme into an affine scheme descends to a finite-type subalgebra.

public theorem exists_openModel {R : Type u} [CommRing R] {W : Scheme.{u}}
    (f : W ⟶ Spec (.of R))
    [LocallyOfFiniteType (terminal.from W)]
    [QuasiCompact (terminal.from W)] [IsOpenImmersion f] :
    ∃ A : Subalgebra ℤ R, IsOpenModel f A

Stacks.FiniteTypeOpenModel.openModel_directed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/FiniteTypeOpenModel.lean, line 530. The attribute's comment: “directedness of the finite-type open models”.

Finite-type subalgebras admitting the open model are directed by inclusion.

public theorem openModel_directed {R : Type u} [CommRing R] {W : Scheme.{u}}
    (f : W ⟶ Spec (.of R))
    [LocallyOfFiniteType (terminal.from W)]
    [QuasiCompact (terminal.from W)] [IsOpenImmersion f] :
    ∀ A B : Subalgebra ℤ R, IsOpenModel f A → IsOpenModel f B →
      ∃ C : Subalgebra ℤ R, IsOpenModel f C ∧ A ≤ C ∧ B ≤ C

Stacks.FiniteTypeOpenModel.openModelCocone_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/FiniteTypeOpenModel.lean, line 548. The attribute's comment: “colimit of the finite-type open models”.

The canonical cocone of finite-type open models is a colimit cocone.

public theorem openModelCocone_isColimit {R : Type u} [CommRing R] {W : Scheme.{u}}
    (f : W ⟶ Spec (.of R))
    [LocallyOfFiniteType (terminal.from W)]
    [QuasiCompact (terminal.from W)] [IsOpenImmersion f] :
    Nonempty (IsColimit (openModelCocone f))

Tag 01Z9, a lemma

Tag 01Z9 in the Stacks Project.

AlgebraicGeometry.isOpenImmersion_iSup_basicOpen_comp_SpecMap_of_isPullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NoetherianApproximation/FibreProductOpenImmersion.lean, line 104.

In a cartesian square of rings, a finite union of standard opens which descend from the other side of the square and on which that side becomes an isomorphism maps by an open immersion to the spectrum of the remaining corner.

lemma isOpenImmersion_iSup_basicOpen_comp_SpecMap_of_isPullback
    {B R B' R' : Type u} [CommRing B] [CommRing R] [CommRing B'] [CommRing R']
    (s : B →+* R) (p : B' →+* B) (r : B' →+* R') (t : R' →+* R)
    (hcart : IsPullback (CommRingCat.ofHom p) (CommRingCat.ofHom r)
      (CommRingCat.ofHom s) (CommRingCat.ofHom t))
    {n : ℕ} (f : Fin n → R') (g : Fin n → B)
    (hfg : ∀ i, t (f i) = s (g i))
    (hloc : ∀ i, Function.Bijective (Localization.awayMap s (g i))) :
    IsOpenImmersion
      ((⨆ i, PrimeSpectrum.basicOpen (f i) : (Spec (.of R')).Opens).ι ≫
        Spec.map (CommRingCat.ofHom r))

Tag 07RN, a lemma

Tag 07RN in the Stacks Project.

AlgebraicGeometry.finiteTypeApproximationOfIsLimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LimitApproxClose/Induction.lean, line 64.

Stacks Project, Tag 07RN, as data: the extended system itself. It is AlgebraicGeometry.exists_finiteTypeApproximation together with the choice of a witness, so it is noncomputable; the construction is propositional throughout, every stage of it being chosen from an existential statement.

noncomputable def finiteTypeApproximationOfIsLimit {I : Type u} [Preorder I] [Nonempty I]
    [IsDirected I (· ≤ ·)] (D : Iᵒᵈ ⥤ Scheme.{u})
    [∀ {i j : Iᵒᵈ} (v : i ⟶ j), IsAffineHom (D.map v)]
    [∀ i, LocallyOfFiniteType (terminal.from (D.obj i))]
    [∀ i, QuasiCompact (terminal.from (D.obj i))]
    (S : Scheme.{u}) [CompactSpace S] [QuasiSeparatedSpace S] (U : S.Opens)
    [CompactSpace (U : Scheme.{u})]
    (p : (Functor.const Iᵒᵈ).obj (U : Scheme.{u}) ⟶ D)
    (hp : IsLimit (Cone.mk (U : Scheme.{u}) p)) :
    Scheme.FiniteTypeApproximation D S U p

Tag 01ZA, a proposition

Tag 01ZA in the Stacks Project.

AlgebraicGeometry.Scheme.exists_isLimit_affine_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/FiniteTypeApproximation/Absolute.lean, line 62.

Absolute Noetherian approximation. A quasi-compact and quasi-separated scheme S is the inverse limit of an inverse system of schemes over a directed set whose transition morphisms are affine and whose every stage is of finite type over the integers.

theorem exists_isLimit_affine_locallyOfFiniteType (S : Scheme.{u}) [CompactSpace S]
    [QuasiSeparatedSpace S] :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (F : Iᵒᵈ ⥤ Scheme.{u}) (c : (Functor.const Iᵒᵈ).obj S ⟶ F),
      (∀ {i j : Iᵒᵈ} (f : i ⟶ j), IsAffineHom (F.map f)) ∧
      (∀ i, LocallyOfFiniteType (terminal.from (F.obj i))) ∧
      (∀ i, QuasiCompact (terminal.from (F.obj i))) ∧
      Nonempty (IsLimit (Cone.mk S c))

AlgebraicGeometry.exists_isLimit_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/NoetherianApproximation/Absolute.lean, line 79.

Stacks Project, Tag 01ZA. A quasi-compact and quasi-separated scheme is the inverse limit of a directed system of schemes of finite type over the integers with affine transition morphisms.

public theorem exists_isLimit_finiteType (S : Scheme.{u}) [CompactSpace S]
    [QuasiSeparatedSpace S] :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (D : Iᵒᵖ ⥤ Scheme.{u}) (c : Cone D),
      (∀ {i j : Iᵒᵖ} (v : i ⟶ j), IsAffineHom (D.map v)) ∧
      (∀ i, LocallyOfFiniteType (terminal.from (D.obj i))) ∧
      (∀ i, QuasiCompact (terminal.from (D.obj i))) ∧
      Nonempty (IsLimit c) ∧ c.pt = S

Declarations registered for the tag:

AlgebraicGeometry.LimitFPObjectDescent.finiteTypeSchemeApproximation, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Approximation/Basic.lean, line 43 (StacksFrontier).

Sources

LeanStacks.FiniteTypeOpenModel.exists_openModel · Stacks.FiniteTypeOpenModel.openModel_directed · Stacks.FiniteTypeOpenModel.openModelCocone_isColimit · AlgebraicGeometry.isOpenImmersion_iSup_basicOpen_comp_SpecMap_of_isPullback · AlgebraicGeometry.finiteTypeApproximationOfIsLimit · AlgebraicGeometry.Scheme.exists_isLimit_affine_locallyOfFiniteType · AlgebraicGeometry.exists_isLimit_finiteType · AlgebraicGeometry.LimitFPObjectDescent.finiteTypeSchemeApproximation

Section32.6 Limits and morphisms of finite presentation #

Section 32.6 of the Stacks Project, Tag 01ZB. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01ZC, a proposition

Tag 01ZC in the Stacks Project.

AlgebraicGeometry.Scheme.locallyOfFinitePresentation_iff_isLimitPreservingOnAffineTransitions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/LimitPreservingFunctorOfPoints.lean, line 139. The attribute's comment: “parts (1) and (3), with the inverse systems indexed by cofiltered categories rather than by directed sets”. References: EGA IV (8.14.2), “a ⇔ b”.

A scheme X over S is locally of finite presentation over S if and only if its functor of points h_X = Mor_S(-, X) turns every cofiltered inverse limit of quasi-compact and quasi-separated S-schemes with affine transition morphisms into a filtered colimit.

The same characterization with the inverse systems restricted to affine schemes is locallyOfFinitePresentation_iff_isLimitPreserving_yoneda.

theorem locallyOfFinitePresentation_iff_isLimitPreservingOnAffineTransitions
    {X S : Scheme.{u}} (f : X ⟶ S) :
    LocallyOfFinitePresentation f ↔
      IsLimitPreservingOnAffineTransitions S (yoneda.obj (Over.mk f))

AlgebraicGeometry.Scheme.locallyOfFinitePresentation_tfae_directed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/LimitPreservingFunctorOfPoints.lean, line 177. References: EGA IV (17.3.2), “more general”; SGA 3 XI (3.2), “partial”.

Stacks 01ZC. For a morphism of schemes f : X ⟶ S the following are equivalent:

f is locally of finite presentation;

for every directed set Λ and every inverse system (T_i) of affine S-schemes over Λ, the canonical map colim_i Mor_S(T_i, X) → Mor_S(lim_i T_i, X) is bijective;

for every directed set Λ and every inverse system (T_i) of S-schemes over Λ whose transition morphisms are affine and whose members are quasi-compact and quasi-separated, the canonical map colim_i Mor_S(T_i, X) → Mor_S(lim_i T_i, X) is bijective.

A directed set is a nonempty preordered type in which any two elements have an upper bound, as in the source, taken in the universe of the schemes; an inverse system over it is a functor out of Λᵒᵖ. Bijectivity of the canonical map is PreservesColimit of the functor of points Mor_S(-, X) for the opposite diagram.

The cofiltered readings of conditions (2) and (3) are locallyOfFinitePresentation_iff_isLimitPreserving_yoneda and locallyOfFinitePresentation_iff_isLimitPreservingOnAffineTransitions; condition (1) implies the directed forms by specializing them along Λᵒᵖ, and the directed form of condition (2) implies condition (1) by the directed criterion AlgebraicGeometry.locallyOfFinitePresentation_of_directedAffineLimit_surjective.

theorem locallyOfFinitePresentation_tfae_directed {X S : Scheme.{u}} (f : X ⟶ S) :
    List.TFAE
      [ LocallyOfFinitePresentation f,
        ∀ (Λ : Type u) [Preorder Λ] [Nonempty Λ] [IsDirectedOrder Λ] (D : Λᵒᵖ ⥤ Over S),
          (∀ i, IsAffine (D.obj i).left) → PreservesColimit D.op (yoneda.obj (Over.mk f)),
        ∀ (Λ : Type u) [Preorder Λ] [Nonempty Λ] [IsDirectedOrder Λ] (D : Λᵒᵖ ⥤ Over S),
          (∀ (i j : Λᵒᵖ) (g : i ⟶ j), IsAffineHom (D.map g).left) →
          (∀ i, CompactSpace (D.obj i).left) →
          (∀ i, QuasiSeparatedSpace (D.obj i).left) →
            PreservesColimit D.op (yoneda.obj (Over.mk f)) ]

Declarations registered for the tag:

locallyOfFinitePresentation_iff_isLimitPreserving_yoneda registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Limits/LimitPreservingFunctorOfPoints.lean, line 116 (StacksFrontier): “parts (1) and (2), with the inverse systems indexed by cofiltered categories rather than by directed sets”.

Tag 05LX, a remark

Tag 05LX in the Stacks Project.

AlgebraicGeometry.Scheme.IsLimitPreserving, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/LimitPreservingFunctorOfPoints.lean, line 78. The attribute's comment: “limit preserving functors”. References: SGA 3 XI (3.2), “definition of (*)”.

Stacks 05LX. A functor on schemes over S is limit preserving when for every cofiltered inverse system {T_i} of affine schemes over S with limit T the canonical map colim_i F(T_i) → F(T) is bijective.

def IsLimitPreserving (S : Scheme.{u}) (F : (Over S)ᵒᵖ ⥤ Type v) : Prop

AlgebraicGeometry.Scheme.locallyOfFinitePresentation_iff_isLimitPreserving_yoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/LimitPreservingFunctorOfPoints.lean, line 109. The attribute's comment: “locally of finite presentation iff the functor of points is limit preserving”. References: SGA 3 XI (3.2), “representable case”.

Stacks 01ZC in the terminology of limit preserving functors. A scheme X over S is locally of finite presentation over S if and only if its functor of points h_X = Mor_S(-, X) is limit preserving.

theorem locallyOfFinitePresentation_iff_isLimitPreserving_yoneda {X S : Scheme.{u}} (f : X ⟶ S) :
    LocallyOfFinitePresentation f ↔ IsLimitPreserving S (yoneda.obj (Over.mk f))

Tag 0CM0, a lemma

Tag 0CM0 in the Stacks Project.

AlgebraicGeometry.locallyOfFinitePresentation_of_affineLimit_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/SurjectiveFinitePresentationCriterion.lean, line 227. References: SGA 3 XI (3.2), “partial”.

If every map from a cofiltered limit of affine schemes over S to X descends to a finite stage, then X ⟶ S is locally of finite presentation.

public theorem locallyOfFinitePresentation_of_affineLimit_surjective
    {X S : Scheme.{u}} (f : X ⟶ S)
    (hsurj : ∀ (I : Type u) [Category.{u} I] [IsCofiltered I]
      (D : I ⥤ Over S) (c : Cone D), IsLimit c →
      (∀ i, IsAffine (D.obj i).left) →
      ∀ g : c.pt ⟶ Over.mk f,
        ∃ (i : I) (gᵢ : D.obj i ⟶ Over.mk f), c.π.app i ≫ gᵢ = g) :
    LocallyOfFinitePresentation f

Tag 0GWT, a lemma

Tag 0GWT in the Stacks Project.

AlgebraicGeometry.existsUnique_hom_of_punctured_and_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/GluingAtClosedPoint.lean, line 118.

Morphisms from a scheme are glued uniquely from its punctured complement and the local scheme at a closed point, when the target is locally of finite presentation over the base.

theorem existsUnique_hom_of_punctured_and_stalk
    {S X Y : Scheme.{u}} (fX : X ⟶ S) (fY : Y ⟶ S)
    [LocallyOfFinitePresentation fY] (x : X) (hx : IsClosed ({x} : Set X)) :
    let U : X.Opens := ⟨({x} : Set X)ᶜ, hx.isOpen_compl⟩
    ∀ (_hU : QuasiCompact U.ι)
      (a : U.toScheme ⟶ Y) (b : Spec (X.presheaf.stalk x) ⟶ Y),
      a ≫ fY = U.ι ≫ fX →
      b ≫ fY = X.fromSpecStalk x ≫ fX →
      pullback.fst U.ι (X.fromSpecStalk x) ≫ a =
        pullback.snd U.ι (X.fromSpecStalk x) ≫ b →
      ∃! f : X ⟶ Y,
        (f ≫ fY = fX) ∧ (U.ι ≫ f = a) ∧ (X.fromSpecStalk x ≫ f = b)

Sources

LeanAlgebraicGeometry.Scheme.locallyOfFinitePresentation_iff_isLimitPreservingOnAffineTransitions · AlgebraicGeometry.Scheme.locallyOfFinitePresentation_tfae_directed · locallyOfFinitePresentation_iff_isLimitPreserving_yoneda · AlgebraicGeometry.Scheme.IsLimitPreserving · AlgebraicGeometry.Scheme.locallyOfFinitePresentation_iff_isLimitPreserving_yoneda · AlgebraicGeometry.locallyOfFinitePresentation_of_affineLimit_surjective · AlgebraicGeometry.existsUnique_hom_of_punctured_and_stalk

Section32.7 Relative approximation #

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

Tag 0GS1, a lemma

Tag 0GS1 in the Stacks Project.

AlgebraicGeometry.LimitFPObjectDescent.exists_isLimit_finiteType_arrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LimitFPObjectDescent/Approximation.lean, line 459.

A morphism between quasi-compact and quasi-separated schemes is a limit of morphisms between schemes of finite type over ℤ, with affine transition morphisms on sources and targets.

theorem exists_isLimit_finiteType_arrow
    {X S : Scheme.{u}} (f : X ⟶ S)
    [CompactSpace X] [QuasiSeparatedSpace X]
    [CompactSpace S] [QuasiSeparatedSpace S] :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirectedOrder I)
      (D : Iᵒᵖ ⥤ Arrow Scheme.{u}) (c : Cone D),
      (∀ i,
        LocallyOfFiniteType (terminal.from (D.obj i).left) ∧
          QuasiCompact (terminal.from (D.obj i).left)) ∧
      (∀ i,
        LocallyOfFiniteType (terminal.from (D.obj i).right) ∧
          QuasiCompact (terminal.from (D.obj i).right)) ∧
      (∀ {i j : Iᵒᵖ} (g : i ⟶ j),
        IsAffineHom (D.map g).left ∧ IsAffineHom (D.map g).right) ∧
      Nonempty (IsLimit c) ∧ Nonempty (c.pt ≅ Arrow.mk f)

Tag 09MV, a lemma

Tag 09MV in the Stacks Project.

AlgebraicGeometry.exists_isLimit_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/RelativeApproximation/Basic.lean, line 475.

Stacks Project, Tag 09MV. A quasi-compact and quasi-separated scheme over a quasi-separated base is a directed inverse limit of quasi-compact and quasi-separated schemes of finite presentation over that base, with affine transition morphisms over the base.

theorem exists_isLimit_finitePresentation
    {X S : Scheme.{u}} (f : X ⟶ S)
    [CompactSpace X] [QuasiSeparatedSpace X] [QuasiSeparatedSpace S] :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I)
      (_ : IsDirectedOrder I) (D : Iᵒᵖ ⥤ Scheme.{u})
      (t : D ⟶ (Functor.const Iᵒᵖ).obj S)
      (p : (Functor.const Iᵒᵖ).obj X ⟶ D) (_ : IsLimit (Cone.mk X p)),
      p ≫ t = (Functor.const Iᵒᵖ).map f ∧
        (∀ i, FinitePresentation (t.app i)) ∧
        (∀ i, CompactSpace (D.obj i) ∧ QuasiSeparatedSpace (D.obj i)) ∧
        ∀ {i j : Iᵒᵖ} (g : i ⟶ j), IsAffineHom (D.map g)

Tag 09YZ, a lemma

Tag 09YZ in the Stacks Project.

Stacks.AlgebraicGeometry.Tag0817PartTwo.nonempty_integralLimitPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PartTwoResidue/Complete.lean, line 164. The attribute's comment: “an integral morphism over a quasi-compact and quasi-separated base is the limit of a directed inverse system of schemes finite and of finite presentation over that base”.

Stacks Project, Tag 09YZ. An integral morphism to a quasi-compact and quasi-separated scheme exhibits its source as the limit of a directed inverse system of schemes finite and of finite presentation over that target.

This is the tag's own proof. The quasi-coherent algebra f_* 𝒪_X ([Stacks, Tag 01LC], here Stacks.AffineAlgebraEquivalence.isQuasicoherent_pushforwardAlgebra) is integral, part (2) of [Stacks, Tag 0817] — exists_small_index_finite_finitePresentation above, packaged as integralAlgebraHasFiniteFinitePresentationColimit — writes it as a filtered colimit of finite, finitely presented quasi-coherent 𝒪_S-algebras, and the relative spectrum turns that colimit into the required limit of schemes, with the finiteness and the finite presentation of each stage read off its algebra. That last passage is Stacks.IntegralLimit.nonempty_integralLimitPresentation_of_algebraColimit, whose only hypothesis was part (2).

The base is quasi-compact and quasi-separated, as the tag asks; the affine-base case AlgebraicGeometry.nonempty_integralLimitPresentation_of_isAffine is strictly weaker and is subsumed by this.

theorem nonempty_integralLimitPresentation {X S : Scheme.{u}} (f : X ⟶ S) [IsIntegralHom f]
    [CompactSpace S] [QuasiSeparatedSpace S] :
    Nonempty (_root_.AlgebraicGeometry.IntegralLimitPresentation f)

Sources

LeanAlgebraicGeometry.LimitFPObjectDescent.exists_isLimit_finiteType_arrow · AlgebraicGeometry.exists_isLimit_finitePresentation · Stacks.AlgebraicGeometry.Tag0817PartTwo.nonempty_integralLimitPresentation

Section32.8 Descending properties of morphisms #

Section 32.8 of the Stacks Project, Tag 081C. 16 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 081D, a situation

Tag 081D in the Stacks Project.

AlgebraicGeometry.MorphismDescentSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Situation.lean, line 42.

A directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms, equipped with a chosen limit cone and a chosen index, together with a morphism of quasi-compact and quasi-separated schemes over the scheme at that index.

structure MorphismDescentSituation (I : Type v) [Preorder I] [IsDirected I (· ≤ ·)]
    extends DescentSituation.{v, u} I

Tag 01ZN, a lemma

Tag 01ZN in the Stacks Project.

AlgebraicGeometry.exists_isAffineHom_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Affine.lean, line 177.

If a morphism over one stage of a cofiltered inverse system becomes affine after base change to the limit, it becomes affine at some later stage.

theorem exists_isAffineHom_of_isLimit
    {I : Type v} [Category.{w} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    (c : Cone D) (hc : IsLimit c) (i₀ : I)
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [IsAffineHom ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (hi : i ⟶ i₀),
      IsAffineHom ((Over.pullback (D.map hi)).map f₀).left

Tag 01ZO, a lemma

Tag 01ZO in the Stacks Project.

AlgebraicGeometry.exists_isFinite_baseChange_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Finite.lean, line 327.

Stacks Project, Tag 01ZO. If a morphism over a stage of a cofiltered inverse system is locally of finite type and its base change to the limit is finite, then its base change to some later stage is finite.

theorem exists_isFinite_baseChange_of_isLimit
    {I : Type v} [Category.{w} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    (c : Cone D) (hc : IsLimit c) (i₀ : I)
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFiniteType f₀.left]
    [IsFinite ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (hi : i ⟶ i₀), IsFinite ((Over.pullback (D.map hi)).map f₀).left

Tag 0C4W, a lemma

Tag 0C4W in the Stacks Project.

AlgebraicGeometry.exists_unramified_baseChange_of_unramified_limitBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Unramified.lean, line 107.

If a morphism over a stage of a cofiltered inverse system is locally of finite type and its base change to the limit is unramified, then its base change to some later stage is unramified.

theorem exists_unramified_baseChange_of_unramified_limitBaseChange
    {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D) (i₀ : I)
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [IsCofiltered I]
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFiniteType f₀.left]
    (hc : IsLimit c)
    [Unramified ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (g : i ⟶ i₀),
      Unramified ((Over.pullback (D.map g)).map f₀).left

Tag 01ZP, a lemma

Tag 01ZP in the Stacks Project.

AlgebraicGeometry.exists_isClosedImmersion_baseChange_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/ClosedImmersion.lean, line 406.

If a morphism over a stage is locally of finite type and becomes a closed immersion over the inverse limit, it becomes a closed immersion at a later stage.

theorem exists_isClosedImmersion_baseChange_of_isLimit
    {I : Type v} [Category.{w} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    (c : Cone D) (hc : IsLimit c) (i₀ : I)
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFiniteType f₀.left]
    [IsClosedImmersion ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (hi : i ⟶ i₀),
      IsClosedImmersion ((Over.pullback (D.map hi)).map f₀).left

Tag 01ZQ, a lemma

Tag 01ZQ in the Stacks Project.

AlgebraicGeometry.exists_isSeparated_baseChange_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Diagonal.lean, line 129.

Stacks Project, Tag 01ZQ. If a morphism over a stage of a cofiltered inverse system is separated after base change to the limit, then it is separated after base change to some later stage.

theorem exists_isSeparated_baseChange_of_isLimit
    {I : Type v} [Category.{v} I] (D : I ⥤ Scheme.{u}) (c : Cone D) (i₀ : I)
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [IsCofiltered I] [EssentiallySmall.{u} I]
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    (hc : IsLimit c)
    [IsSeparated ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (g : i ⟶ i₀), IsSeparated ((Over.pullback (D.map g)).map f₀).left

Tag 04AI, a lemma

Tag 04AI in the Stacks Project.

AlgebraicGeometry.exists_flat_baseChange_of_limitBaseChange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Flat.lean, line 242.

Stacks Project, Tag 04AI. A locally finitely presented morphism over a stage which becomes flat over the inverse limit is flat at some later stage.

lemma exists_flat_baseChange_of_limitBaseChange
    {I : Type v} [Category.{w} I] [EssentiallySmall.{u} I]
    (D : Functor I Scheme.{u}) (c : Cone D) (i₀ : I)
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [IsCofiltered I]
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFinitePresentation f₀.left]
    (hc : IsLimit c)
    [Flat ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (g : i ⟶ i₀), Flat ((Over.pullback (D.map g)).map f₀).left

Tag 06AC, a lemma

Tag 06AC in the Stacks Project.

AlgebraicGeometry.exists_isFiniteLocallyFree_baseChange_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/FiniteLocallyFree.lean, line 68. The attribute's comment: “the plain statement; the degree-d refinement is exists_isFiniteLocallyFreeOfRank_baseChange_of_isLimit. Carries the essential smallness of the index category, a hypothesis of the inputs without which the statement is false and which the source, having no universe hierarchy, states implicitly by indexing on a directed set”.

A morphism over a stage of a cofiltered inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms, essentially small in the universe of the schemes, which is locally of finite presentation and whose base change to the limit is finite locally free, is finite locally free after base change to some later stage.

theorem exists_isFiniteLocallyFree_baseChange_of_isLimit
    {I : Type v} [Category.{w} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    (c : Cone D) (hc : IsLimit c) (i₀ : I)
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFinitePresentation f₀.left]
    [Stacks.Morphisms.IsFiniteLocallyFree ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (g : i ⟶ i₀),
      Stacks.Morphisms.IsFiniteLocallyFree ((Over.pullback (D.map g)).map f₀).left

AlgebraicGeometry.exists_isFiniteLocallyFreeOfRank_baseChange_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/FiniteLocallyFree.lean, line 106. The attribute's comment: “the degree-d refinement. Narrower than the plain statement in the index universes: the objects and the morphisms of the index category are both in the universe of the schemes, which is the form in which the cofiltered Tag 05F4 used to descend the degree stratum along the system of base changes of Y₀ is available, that system being indexed by the over category, which inherits both universes. The plain statement's essential smallness is implied by this narrowing rather than assumed”.

A morphism over a stage of a cofiltered inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms, indexed in the universe of the schemes, which is locally of finite presentation and whose base change to the limit is finite locally free of degree d, is finite locally free of degree d after base change to some later stage.

theorem exists_isFiniteLocallyFreeOfRank_baseChange_of_isLimit
    {I : Type u} [Category.{u} I] [IsCofiltered I] (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    (c : Cone D) (hc : IsLimit c) (i₀ : I)
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀) (d : ℕ)
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFinitePresentation f₀.left]
    [Stacks.Morphisms.IsFiniteLocallyFreeOfRank
      ((Over.pullback (c.π.app i₀)).map f₀).left d] :
    ∃ (i : I) (g : i ⟶ i₀),
      Stacks.Morphisms.IsFiniteLocallyFreeOfRank
        ((Over.pullback (D.map g)).map f₀).left d

AlgebraicGeometry.exists_isFiniteLocallyFreeOfRank_overPullbackObj_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/FiniteLocallyFreeRank.lean, line 142. The attribute's comment: “the fixed-degree refinement, for a morphism whose target is the stage itself”.

Stacks Project, Tag 06AC, fixed-degree form, for the structure morphism of an object over a stage. Let D be a cofiltered inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms and limit cone c, and let Z be of finite presentation over the stage D.obj i₀. If the base change of Z to the limit is finite locally free of degree d over the limit, then its base change to D.obj i is finite locally free of degree d over D.obj i for some later stage i.

theorem exists_isFiniteLocallyFreeOfRank_overPullbackObj_of_isLimit
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ Scheme.{u}) [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    [∀ i : I, CompactSpace (D.obj i)] [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    (c : Cone D) (hc : IsLimit c) (i₀ : I) (Z : Over (D.obj i₀))
    (hZ : FinitePresentation Z.hom) (d : ℕ)
    [Stacks.Morphisms.IsFiniteLocallyFreeOfRank ((Over.pullback (c.π.app i₀)).obj Z).hom d] :
    ∃ (i : I) (g : i ⟶ i₀),
      Stacks.Morphisms.IsFiniteLocallyFreeOfRank ((Over.pullback (D.map g)).obj Z).hom d

Tag 0C0C, a lemma

Tag 0C0C in the Stacks Project.

AlgebraicGeometry.exists_smooth_baseChange_of_smooth_limitBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Smooth.lean, line 350. References: EGA IV (17.7.8), “(ii) smooth”; EGA IV (17.12.6), “f smooth ⇒ ∃λ”.

Stacks Project, Tag 0C0C. If a locally finitely presented morphism over a stage of a cofiltered inverse system becomes smooth over the limit, it becomes smooth at some later stage.

theorem exists_smooth_baseChange_of_smooth_limitBaseChange
    {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D) (i₀ : I)
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [IsCofiltered I]
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFinitePresentation f₀.left]
    (hc : IsLimit c)
    [Smooth ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (g : i ⟶ i₀),
      Smooth ((Over.pullback (D.map g)).map f₀).left

Tag 07RP, a lemma

Tag 07RP in the Stacks Project.

AlgebraicGeometry.exists_etale_pullback_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Etale.lean, line 63. References: EGA IV (17.7.8), “(ii) étale”.

Stacks 07RP. If a locally finitely presented morphism at one stage of a cofiltered inverse system becomes étale over the limit, then it is étale at some later stage.

theorem exists_etale_pullback_of_isLimit
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c) (i₀ : I)
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFinitePresentation f₀.left]
    [Etale ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ i : Over i₀, Etale ((Over.pullback (D.map i.hom)).map f₀).left

Tag 081E, a lemma

Tag 081E in the Stacks Project.

AlgebraicGeometry.exists_isIso_baseChange_of_isIso_limitBaseChange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Isomorphism.lean, line 173.

If the base change of a finitely presented morphism to the inverse limit is an isomorphism, then its base change to some stage is already an isomorphism.

lemma exists_isIso_baseChange_of_isIso_limitBaseChange
    {I : Type v} [Category.{w} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (S : I ⥤ Scheme.{u})
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (S.map g)]
    (c : Cone S) (hc : IsLimit c) (i₀ : I)
    (X₀ Y₀ : Over (S.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace (S.obj i₀)] [QuasiSeparatedSpace (S.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFinitePresentation f₀.left]
    [IsIso ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (g : i ⟶ i₀), IsIso ((Over.pullback (S.map g)).map f₀).left

Tag 0EUU, a lemma

Tag 0EUU in the Stacks Project.

AlgebraicGeometry.exists_isOpenImmersion_pullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Etale.lean, line 100.

Stacks 0EUU. An open immersion obtained by base change to the inverse limit of an affine-transition inverse system descends to some stage of the system.

lemma exists_isOpenImmersion_pullback
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (S : I ⥤ Scheme.{u}) (c : Cone S) (hc : IsLimit c)
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (S.map g)]
    (i₀ : I) [CompactSpace (S.obj i₀)] [QuasiSeparatedSpace (S.obj i₀)]
    (X₀ Y₀ : Over (S.obj i₀))
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    (f₀ : X₀ ⟶ Y₀) [LocallyOfFinitePresentation f₀.left]
    (hf : IsOpenImmersion ((Over.pullback (c.π.app i₀)).map f₀).left) :
    ∃ (i : I) (g : i ⟶ i₀), IsOpenImmersion ((Over.pullback (S.map g)).map f₀).left

Tag 0GTB, a lemma

Tag 0GTB in the Stacks Project.

AlgebraicGeometry.exists_isImmersion_baseChange_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Immersion.lean, line 249.

If a locally finite type morphism becomes an immersion over the inverse limit, it becomes an immersion at a later stage.

theorem exists_isImmersion_baseChange_of_isLimit
    {I : Type v} [Category.{w} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    (c : Cone D) (hc : IsLimit c) (i₀ : I)
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFiniteType f₀.left]
    [IsImmersion ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (hi : i ⟶ i₀),
      IsImmersion ((Over.pullback (D.map hi)).map f₀).left

Tag 07RQ, a lemma

Tag 07RQ in the Stacks Project.

AlgebraicGeometry.exists_mono_baseChange_of_mono_limitBaseChange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Monomorphism.lean, line 78.

Stacks 07RQ. A locally finite type morphism which becomes a monomorphism over the inverse limit is a monomorphism at some later stage.

lemma exists_mono_baseChange_of_mono_limitBaseChange
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (S : I ⥤ Scheme.{u})
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (S.map g)]
    (c : Cone S) (hc : IsLimit c) (i₀ : I)
    (X₀ Y₀ : Over (S.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace (S.obj i₀)] [QuasiSeparatedSpace (S.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFiniteType f₀.left]
    [Mono ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (g : i ⟶ i₀), Mono ((Over.pullback (S.map g)).map f₀).left

Tag 07RR, a lemma

Tag 07RR in the Stacks Project.

AlgebraicGeometry.exists_surjective_baseChange_of_surjective_limitBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Surjective.lean, line 90.

Stacks Project, Tag 07RR. If a locally finitely presented morphism over a stage of a cofiltered inverse system becomes surjective over the inverse limit, then it is surjective at some later stage.

theorem exists_surjective_baseChange_of_surjective_limitBaseChange
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (S : I ⥤ Scheme.{u})
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (S.map g)]
    (c : Cone S) (hc : IsLimit c) (i₀ : I)
    (X₀ Y₀ : Over (S.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace (S.obj i₀)] [QuasiSeparatedSpace (S.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFinitePresentation f₀.left]
    [Surjective ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (g : i ⟶ i₀),
      Surjective ((Over.pullback (S.map g)).map f₀).left

Tag 0C3L, a lemma

Tag 0C3L in the Stacks Project.

AlgebraicGeometry.exists_syntomic_baseChange_of_syntomic_limitBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Finiteness/SyntomicDescentAlongLimit.lean, line 234.

Stacks Project, Tag 0C3L. If a locally finitely presented morphism over a stage of a cofiltered inverse system with affine transition morphisms becomes syntomic over the limit, it becomes syntomic at some later stage.

theorem exists_syntomic_baseChange_of_syntomic_limitBaseChange {I : Type u} [Category.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (i₀ : I) (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [IsCofiltered I] [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFinitePresentation f₀.left] (hc : IsLimit c)
    (hf₀ : Syntomic ((Over.pullback (c.π.app i₀)).map f₀).left) :
    ∃ (i : I) (g : i ⟶ i₀), Syntomic ((Over.pullback (D.map g)).map f₀).left

Sources

LeanAlgebraicGeometry.MorphismDescentSituation · AlgebraicGeometry.exists_isAffineHom_of_isLimit · AlgebraicGeometry.exists_isFinite_baseChange_of_isLimit · AlgebraicGeometry.exists_unramified_baseChange_of_unramified_limitBaseChange · AlgebraicGeometry.exists_isClosedImmersion_baseChange_of_isLimit · AlgebraicGeometry.exists_isSeparated_baseChange_of_isLimit · AlgebraicGeometry.exists_flat_baseChange_of_limitBaseChange · AlgebraicGeometry.exists_isFiniteLocallyFree_baseChange_of_isLimit

Section32.9 Finite type closed in finite presentation #

Section 32.9 of the Stacks Project, Tag 01ZD. 7 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01ZE, a lemma

Tag 01ZE in the Stacks Project.

AlgebraicGeometry.exists_finitePresentation_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Finiteness/ImmersionIntoFinitePresentation.lean, line 221.

Stacks Project, Tag 01ZE. A quasi-compact, quasi-separated scheme locally of finite type over S immerses over S into a scheme of finite presentation over S.

theorem exists_finitePresentation_isImmersion {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [CompactSpace X] [QuasiSeparatedSpace X] :
    ∃ (X' : Scheme.{u}) (f' : X' ⟶ S) (i : X ⟶ X'),
      FinitePresentation f' ∧ IsImmersion i ∧ i ≫ f' = f

Tag 01ZG, a lemma

Tag 01ZG in the Stacks Project.

AlgebraicGeometry.exists_finitePresentation_closedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Finiteness/ClosedImmersionIntoFinitePresentation.lean, line 57.

Stacks Project, Tag 01ZG. A morphism locally of finite type from a quasi-compact, quasi-separated scheme to a quasi-separated scheme factors as a closed immersion into a scheme of finite presentation over the target.

theorem exists_finitePresentation_closedImmersion {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [CompactSpace X] [QuasiSeparatedSpace X] [QuasiSeparatedSpace S] :
    ∃ (X' : Scheme.{u}) (p : X' ⟶ S) (i : X ⟶ X'),
      FinitePresentation p ∧ IsClosedImmersion i ∧ i ≫ p = f

Tag 09ZP, a lemma

Tag 09ZP in the Stacks Project.

AlgebraicGeometry.exists_isLimit_closedImmersion_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Finiteness/ClosedImmersionLimit.lean, line 281.

A closed immersion into a quasi-compact and quasi-separated scheme Y is a directed inverse limit, over Y, of closed immersions of finite presentation into Y.

The system is the system of closed subschemes of Y cut out by the ideal sheaf data below f.ker whose closed immersion is of finite presentation. Those are directed and have supremum f.ker ([Stacks, Tag 01PG] for ideal sheaf data), and a cone of closed subschemes whose ideal sheaves have supremum f.ker has X as its limit.

theorem exists_isLimit_closedImmersion_finitePresentation {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsClosedImmersion f] [CompactSpace Y] [QuasiSeparatedSpace Y] :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (D : Functor Iᵒᵖ Scheme.{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, IsClosedImmersion (t.app i) ∧ FinitePresentation (t.app i)

AlgebraicGeometry.isLimit_finitePresentationCone_of_qcqs, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealSheafFiniteType/Basic.lean, line 493.

Limits, Tag 09ZP. The source of a closed immersion into a quasi-compact and quasi-separated scheme Y is the limit, in Over Y, of the inverse system of finite-presentation closed subschemes of Y containing it.

The index of that system is Stacks.Flatness.FinitePresentationSubscheme f.ker, whose every member is by definition a closed subscheme of Y of finite presentation, so the tag's assertion about the stages is carried by the statement itself; the directedness of the system is the unconditional AlgebraicGeometry.isCofiltered_finitePresentationSubscheme_op, which is the other half of the covering set and is left untagged where it stands.

def isLimit_finitePresentationCone_of_qcqs {X : Scheme.{u}} [CompactSpace Y]
    [QuasiSeparatedSpace Y] (f : X ⟶ Y) [IsClosedImmersion f] :
    IsLimit (finitePresentationCone f (le_refl f.ker))

Tag 09ZQ, a lemma

Tag 09ZQ in the Stacks Project.

AlgebraicGeometry.exists_isLimit_finitePresentation_closedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Finiteness/FiniteLimitPresentation.lean, line 104.

A quasi-compact and quasi-separated scheme locally of finite type over a quasi-separated base is a directed inverse limit of quasi-compact and quasi-separated schemes of finite presentation over that base, with closed immersions as the transition maps and as the limit projections.

theorem exists_isLimit_finitePresentation_closedImmersion {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [CompactSpace X] [QuasiSeparatedSpace X] [QuasiSeparatedSpace S] :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (D : Functor Iᵒᵖ Scheme.{u}) (t : D ⟶ (Functor.const Iᵒᵖ).obj S)
      (p : (Functor.const Iᵒᵖ).obj X ⟶ D) (_ : IsLimit (Cone.mk X p)),
      p ≫ t = (Functor.const Iᵒᵖ).map f ∧
        (∀ i, FinitePresentation (t.app i) ∧
          CompactSpace (D.obj i) ∧ QuasiSeparatedSpace (D.obj i)) ∧
        (∀ {i j : Iᵒᵖ} (g : i ⟶ j), IsClosedImmersion (D.map g)) ∧
        ∀ i, IsClosedImmersion (p.app i)

AlgebraicGeometry.exists_isLimit_finitePresentation_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteTypeLimitFinitePresentation/Basic.lean, line 204.

Stacks, Tag 09ZQ. A morphism f : X ⟶ S locally of finite type, with X quasi-compact and quasi-separated and S quasi-separated, presents X as the limit of a directed inverse system of quasi-compact quasi-separated schemes of finite presentation over S whose transition morphisms, and whose projections from X, are closed immersions.

[Stacks, Tag 01ZE] immerses X over S into a scheme of finite presentation over S, and AlgebraicGeometry.exists_qcqs_finitePresentation_isClosedImmersion_of_exists_immersion converts that immersion into a closed immersion j : X ⟶ Y with Y quasi-compact, quasi-separated and of finite presentation over S. [Stacks, Tag 09ZP] then writes X as the directed inverse limit over Y of those closed subschemes of Y containing X whose closed immersion into Y is of finite presentation. Composing the structure morphisms of that system with Y ⟶ S leaves them of finite presentation; every stage, being a closed subscheme of Y, inherits quasi-compactness and quasi-separatedness from Y; and both the transition morphisms and the projections from X are closed immersions because their composites with the closed immersions into Y are.

theorem exists_isLimit_finitePresentation_isClosedImmersion (f : X ⟶ S) [LocallyOfFiniteType f]
    [CompactSpace X] [QuasiSeparatedSpace X] [QuasiSeparatedSpace S] :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (D : Iᵒᵖ ⥤ Scheme.{u}) (t : D ⟶ (Functor.const Iᵒᵖ).obj S)
      (p : (Functor.const Iᵒᵖ).obj X ⟶ D) (_ : IsLimit (Cone.mk X p)),
      p ≫ t = (Functor.const Iᵒᵖ).map f ∧
        (∀ i, FinitePresentation (t.app i) ∧ CompactSpace (D.obj i) ∧
          QuasiSeparatedSpace (D.obj i)) ∧
        (∀ (i i' : Iᵒᵖ) (g : i ⟶ i'), IsClosedImmersion (D.map g)) ∧
        ∀ i, IsClosedImmersion (p.app i)

Tag 01ZJ, a proposition

Tag 01ZJ in the Stacks Project.

AlgebraicGeometry.exists_isClosedImmersion_into_isSeparated_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/SeparatedFinitePresentationEmbedding.lean, line 51.

A separated morphism of finite type onto a quasi-compact, quasi-separated scheme factors as a closed immersion followed by a separated morphism of finite presentation.

theorem exists_isClosedImmersion_into_isSeparated_finitePresentation
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f]
    [CompactSpace S] [QuasiSeparatedSpace S] :
    ∃ (X' : Scheme.{u}) (f' : X' ⟶ S) (i : X ⟶ X'),
      IsSeparated f' ∧ FinitePresentation f' ∧ IsClosedImmersion i ∧ i ≫ f' = f

Tag 01ZK, a lemma

Tag 01ZK in the Stacks Project.

AlgebraicGeometry.exists_isFinite_finitePresentation_closedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Finiteness/FiniteIntoFinitePresentation.lean, line 37.

A finite morphism f : X ⟶ S of schemes whose target is quasi-compact and quasi-separated factors as a closed immersion X ⟶ X' followed by a morphism X' ⟶ S which is finite and of finite presentation.

theorem exists_isFinite_finitePresentation_closedImmersion {X S : Scheme.{u}} (f : X ⟶ S)
    [IsFinite f] [CompactSpace S] [QuasiSeparatedSpace S] :
    ∃ (X' : Scheme.{u}) (f' : X' ⟶ S) (i : X ⟶ X'),
      IsFinite f' ∧ FinitePresentation f' ∧ IsClosedImmersion i ∧ i ≫ f' = f

Tag 09YY, a lemma

Tag 09YY in the Stacks Project.

Stacks.FiniteAlgebraLimitPresentation.finiteLimitPresentationOfIsFinite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteAlgebraLimitPresentation/Basic.lean, line 559.

[Stacks, Tag 09YY]. A finite morphism over a quasi-compact and quasi-separated base is the inverse limit of a directed system of morphisms to that base which are finite and of finite presentation, with closed immersions as transition maps.

[Stacks, Tag 09ZQ] supplies such a system of morphisms of finite presentation, finiteness of the stages failing only below some index; [Stacks, Tag 09ZN] produces that index, and the cofinal tail above it is an initial subcategory, so the restricted system has the same limit.

noncomputable def finiteLimitPresentationOfIsFinite {X S : Scheme.{u}} (f : X ⟶ S) [IsFinite f]
    [CompactSpace S] [QuasiSeparatedSpace S] : FiniteLimitPresentation f

Sources

LeanAlgebraicGeometry.exists_finitePresentation_isImmersion · AlgebraicGeometry.exists_finitePresentation_closedImmersion · AlgebraicGeometry.exists_isLimit_closedImmersion_finitePresentation · AlgebraicGeometry.isLimit_finitePresentationCone_of_qcqs · AlgebraicGeometry.exists_isLimit_finitePresentation_closedImmersion · AlgebraicGeometry.exists_isLimit_finitePresentation_isClosedImmersion · AlgebraicGeometry.exists_isClosedImmersion_into_isSeparated_finitePresentation · AlgebraicGeometry.exists_isFinite_finitePresentation_closedImmersion

Section32.10 Descending relative objects #

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

Tag 01ZM, a lemma

Tag 01ZM in the Stacks Project.

AlgebraicGeometry.LimitDescent.exists_model_of_finitePresentation_of_essentiallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LimitDescentGlueing/Glueing.lean, line 626. The attribute's comment: “part (1)”. References: EGA IV (8.1.1), “more general”; EGA IV (8.8.3), “essential surjectivity”; SGA 3 VIB (10.0), “(ii)”; SGA 4 VII (5.2), “(b)”; SGA 4 VII (5.3), “essential surjectivity”.

Let S = lim Sᵢ be a cofiltered limit of quasi-compact, quasi-separated schemes with affine transition morphisms. Every scheme of finite presentation over S is isomorphic, over S, to the base change of a scheme of finite presentation over one of the stages Sᵢ.

This is AlgebraicGeometry.LimitDescent.exists_isPullback_of_finitePresentation_of_essentiallySmall stated with CategoryTheory.Over.pullback. The index hypothesis CategoryTheory.EssentiallySmall.{u} I is relative to the universe of the schemes.

public theorem exists_model_of_finitePresentation_of_essentiallySmall {I : Type v}
    [Category.{w} I] [IsCofiltered I] [EssentiallySmall.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
    (hc : IsLimit c) [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    [∀ i : I, CompactSpace (D.obj i)] [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    (X : Over c.pt) (hX : FinitePresentation X.hom) :
    ∃ (i : I) (Xᵢ : Over (D.obj i)), FinitePresentation Xᵢ.hom ∧
      Nonempty (X ≅ (Over.pullback (c.π.app i)).obj Xᵢ)

AlgebraicGeometry.exists_morphism_after_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Relative.lean, line 302. The attribute's comment: “part (2)”.

A morphism between the base changes of two schemes of finite presentation descends after passing to a later stage of a cofiltered inverse system.

theorem exists_morphism_after_baseChange
    {I : Type v} [Category.{w} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [∀ {i j : I} (e : i ⟶ j), IsAffineHom (D.map e)]
    [∀ i : I, CompactSpace (D.obj i)]
    [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    (i : I) (X Y : Over (D.obj i))
    (hX : FinitePresentation X.hom) (hY : FinitePresentation Y.hom)
    (f : (Over.pullback (c.π.app i)).obj X ⟶ (Over.pullback (c.π.app i)).obj Y) :
    ∃ (j : I) (e : j ⟶ i)
      (g : (Over.pullback (D.map e)).obj X ⟶ (Over.pullback (D.map e)).obj Y)
      (α : (Over.pullback (c.π.app j)).obj ((Over.pullback (D.map e)).obj X) ≅
        (Over.pullback (c.π.app i)).obj X)
      (β : (Over.pullback (c.π.app j)).obj ((Over.pullback (D.map e)).obj Y) ≅
        (Over.pullback (c.π.app i)).obj Y),
      α.hom.left ≫ pullback.fst X.hom (c.π.app i) =
          pullback.fst ((Over.pullback (D.map e)).obj X).hom (c.π.app j) ≫
            pullback.fst X.hom (D.map e) ∧
        β.hom.left ≫ pullback.fst Y.hom (c.π.app i) =
          pullback.fst ((Over.pullback (D.map e)).obj Y).hom (c.π.app j) ≫
            pullback.fst Y.hom (D.map e) ∧
        α.hom ≫ f = (Over.pullback (c.π.app j)).map g ≫ β.hom

AlgebraicGeometry.eventually_eq_of_baseChange_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/Relative.lean, line 329. The attribute's comment: “part (3)”.

Two morphisms at one stage which become equal after base change to the inverse limit are equal after passing to a later stage.

theorem eventually_eq_of_baseChange_eq
    {I : Type v} [Category.{w} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [∀ {i j : I} (e : i ⟶ j), IsAffineHom (D.map e)]
    [∀ i : I, CompactSpace (D.obj i)]
    [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    (i : I) (X Y : Over (D.obj i))
    (hX : FinitePresentation X.hom) (hY : FinitePresentation Y.hom) (f g : X ⟶ Y)
    (hfg : (Over.pullback (c.π.app i)).map f = (Over.pullback (c.π.app i)).map g) :
    ∃ (j : I) (e : j ⟶ i),
      (Over.pullback (D.map e)).map f = (Over.pullback (D.map e)).map g

AlgebraicGeometry.Scheme.eventually_eq_of_baseChange_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/FinitePresentationDescent.lean, line 346. The attribute's comment: “part (3)”. References: EGA IV (8.13.1), “special case, uniqueness”; SGA 3 VIB (10.0), “(i) injectivity”; SGA 4 VII (5.2), “(a) injectivity”; SGA 4 VII (5.3), “faithfulness”.

Stacks Project, Tag 01ZM, part (3). Two morphisms between schemes of finite presentation at one stage of a cofiltered inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms, which become equal after base change to the limit, are equal after passing to a later stage.

theorem eventually_eq_of_baseChange_eq
    [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [∀ {i j : I} (e : i ⟶ j), IsAffineHom (D.map e)]
    [∀ i : I, CompactSpace (D.obj i)]
    [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    (i : I) (X Y : Over (D.obj i))
    (hX : FinitePresentation X.hom) (hY : FinitePresentation Y.hom) (f g : X ⟶ Y)
    (hfg : (Over.pullback (c.π.app i)).map f = (Over.pullback (c.π.app i)).map g) :
    ∃ (j : I) (e : j ⟶ i),
      (Over.pullback (D.map e)).map f = (Over.pullback (D.map e)).map g

AlgebraicGeometry.LimitFPObjectDescent.exists_model_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ObjectDescent/Basic.lean, line 367. The attribute's comment: “part (1)”. References: SGA 3 VIB (10.0), “(ii)”; SGA 4 VII (5.2), “(b)”; SGA 4 VII (5.3), “essential surjectivity”.

Stacks Project, Tag 01ZM, part (1). A scheme of finite presentation over the limit of a cofiltered system of quasi-compact and quasi-separated schemes with affine transition morphisms is obtained by base change from some stage.

theorem exists_model_of_finitePresentation {I : Type v} [Category.{w} I] [IsCofiltered I]
    [EssentiallySmall.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] [∀ i : I, CompactSpace (D.obj i)]
    [∀ i : I, QuasiSeparatedSpace (D.obj i)] (X : Over c.pt) (hX : FinitePresentation X.hom) :
    ∃ (i : I) (Xᵢ : Over (D.obj i)),
      FinitePresentation Xᵢ.hom ∧ Nonempty (X ≅ (Over.pullback (c.π.app i)).obj Xᵢ)

Tag 01ZR, a lemma

Tag 01ZR in the Stacks Project.

Stacks.AlgebraicGeometry.ModuleLimits.exists_pullback_map_eq_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ModuleLimits/EventualMapEq.lean, line 178. The attribute's comment: “eventual_equality”.

Let c be a limit cone on a cofiltered diagram D of schemes with affine transition morphisms and let ψ₁, ψ₂ : F ⟶ G be morphisms of sheaves of modules of finite presentation on a quasi-compact stage D.obj i. If the pullbacks of ψ₁ and ψ₂ to c.pt agree, then their pullbacks to D.obj j agree for some j over i.

theorem exists_pullback_map_eq_of_isLimit (hc : IsLimit c) (i : I) [CompactSpace (D.obj i)]
    (F G : (D.obj i).Modules) [F.IsFinitePresentation] [G.IsFinitePresentation]
    (ψ₁ ψ₂ : F ⟶ G)
    (h : (Scheme.Modules.pullback (c.π.app i)).map ψ₁ =
      (Scheme.Modules.pullback (c.π.app i)).map ψ₂) :
    ∃ (j : I) (e : j ⟶ i),
      (Scheme.Modules.pullback (D.map e)).map ψ₁ =
        (Scheme.Modules.pullback (D.map e)).map ψ₂

Stacks.AlgebraicGeometry.ModuleLimits.exists_map_of_pullback_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ModuleLimits/MorphismDescentGlue.lean, line 503. The attribute's comment: “descend_morphisms”.

[Stacks Project, Tag 01ZR] (2), with the canonical identifications written out. This is the statement of the clause of the tag verbatim, obtained from exists_map_of_pullback_canonical_of_isLimit' by unfolding the canonical identification.

theorem exists_map_of_pullback_of_isLimit (hc : IsLimit c) (i : I)
    [CompactSpace (D.obj i)] [QuasiSeparatedSpace (D.obj i)]
    (F G : (D.obj i).Modules) [F.IsFinitePresentation] [G.IsFinitePresentation]
    (φ : (Scheme.Modules.pullback (c.π.app i)).obj F ⟶
      (Scheme.Modules.pullback (c.π.app i)).obj G) :
    ∃ (j : I) (e : j ⟶ i)
      (φj : (Scheme.Modules.pullback (D.map e)).obj F ⟶
        (Scheme.Modules.pullback (D.map e)).obj G),
      (Scheme.Modules.pullback (c.π.app j)).map φj ≫
          (Scheme.Modules.pullbackComp (c.π.app j) (D.map e)).hom.app G ≫
            (Scheme.Modules.pullbackCongr (c.w e)).hom.app G =
        (Scheme.Modules.pullbackComp (c.π.app j) (D.map e)).hom.app F ≫
          (Scheme.Modules.pullbackCongr (c.w e)).hom.app F ≫ φ

Stacks.AlgebraicGeometry.ModuleLimits.exists_isFinitePresentation_pullback_iso_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ModuleLimits/MorphismDescentGlue.lean, line 528. The attribute's comment: “descend_modules”.

[Stacks Project, Tag 01ZR] (1) for a cofiltered limit of quasi-compact quasi-separated schemes with affine transition morphisms. A sheaf of modules of finite presentation on the limit is the pullback of one on a stage. This is Stacks.AlgebraicGeometry.ModuleLimits.exists_isFinitePresentation_pullback_iso_of_map with its hypothesis hmap discharged by exists_map_of_pullback_of_isLimit, and it is the statement [Stacks Project, Tag 0ASY] calls.

theorem exists_isFinitePresentation_pullback_iso_of_qcqs (hc : IsLimit c)
    [∀ j : I, CompactSpace (D.obj j)] [∀ j : I, QuasiSeparatedSpace (D.obj j)]
    (F : c.pt.Modules) [F.IsFinitePresentation] :
    ∃ (i : I) (Fᵢ : (D.obj i).Modules),
      Fᵢ.IsFinitePresentation ∧
        Nonempty (F ≅ (Scheme.Modules.pullback (c.π.app i)).obj Fᵢ)

Tag 0B8W, a lemma

Tag 0B8W in the Stacks Project.

Stacks.AlgebraicGeometry.ModuleLimits.exists_isFiniteLocallyFree_pullback_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ModuleLimits/FiniteLocallyFreeUnconditional.lean, line 216. The attribute's comment: “(1)”.

Stacks Project, Tag 0B8W (1). Let S = lim Sᵢ be the limit of a cofiltered system of quasi-compact quasi-separated schemes with affine transition morphisms. Then every finite locally free 𝒪_S-module is the pullback of a finite locally free 𝒪_{Sᵢ}-module for some i.

This is exists_isFiniteLocallyFree_pullback_iso_of_eventually with its remaining hypothesis — the conjunction of Algebra, Lemmas 02JO and 00NX in the form the source's proof uses them — supplied by exists_isFiniteLocallyFree_pullback_of_isLimit_qcqs'.

theorem exists_isFiniteLocallyFree_pullback_iso (hc : IsLimit c)
    [∀ i : I, CompactSpace (D.obj i)] [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    (E : c.pt.Modules) (hE : SheafOfModules.IsFiniteLocallyFree.{u, u, u} E) :
    ∃ (i : I) (Eᵢ : (D.obj i).Modules),
      SheafOfModules.IsFiniteLocallyFree.{u, u, u} Eᵢ ∧
        Nonempty (E ≅ (Scheme.Modules.pullback (c.π.app i)).obj Eᵢ)

Stacks.AlgebraicGeometry.ModuleLimits.exists_ideal_pullback_epi_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ModuleLimits/FiniteTypeIdealDescent.lean, line 332. The attribute's comment: “finite_type_ideal_descent”.

Stacks Project, Tag 0B8W. A finite type quasi-coherent ideal of the structure sheaf of the limit of a cofiltered system of quasi-compact and quasi-separated schemes with affine transition morphisms is the image of the pullback of such an ideal at some stage.

An ideal is given as a quasi-coherent module I of finite type together with a monomorphism inclusion : I ⟶ 𝒪. The epimorphism descend of the conclusion is compatible with the two inclusions; it need not be invertible, because the pullback of a monomorphism of modules need not be one.

theorem exists_ideal_pullback_epi_of_isLimit (hc : IsLimit c) (I : c.pt.Modules)
    [I.IsQuasicoherent] [I.IsFiniteType]
    (inclusion : I ⟶ SheafOfModules.unit c.pt.ringCatSheaf) [Mono inclusion] :
    ∃ i : J,
      letI : (SheafOfModules.pushforward
        (c.π.app i).toRingCatSheafHom).IsRightAdjoint :=
        Scheme.Modules.instIsRightAdjointPushforward (c.π.app i)
      ∃ Iᵢ : (D.obj i).Modules,
        Iᵢ.IsQuasicoherent ∧ Iᵢ.IsFiniteType ∧
          ∃ inclusionᵢ : Iᵢ ⟶ SheafOfModules.unit (D.obj i).ringCatSheaf,
            Mono inclusionᵢ ∧
              ∃ descend : (Scheme.Modules.pullback (c.π.app i)).obj Iᵢ ⟶ I,
                Epi descend ∧
                  descend ≫ inclusion =
                    (Scheme.Modules.pullback (c.π.app i)).map inclusionᵢ ≫
                      SheafOfModules.pullbackObjUnitToUnit
                        (c.π.app i).toRingCatSheafHom

Stacks.AlgebraicGeometry.ModuleLimits.exists_isInvertible_pullback_iso_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ModuleLimits/InvertibleUnconditional.lean, line 191. The attribute's comment: “(2)”.

Stacks Project, Tag 0B8W (2). Let S = lim Sᵢ be the limit of a cofiltered system of quasi-compact quasi-separated schemes with affine transition morphisms. Then every invertible 𝒪_S-module is the pullback of an invertible 𝒪_{Sᵢ}-module for some i.

This is exists_isInvertible_pullback_iso_of_isLimit_of_descent with its two hypotheses discharged: hDescend by Tag 01ZR (1), hFullyFaithful by exists_iso_pullback_of_isLimit, which rests on Tag 01ZR (2) and (3).

theorem exists_isInvertible_pullback_iso_of_isLimit
    [∀ i : I, CompactSpace (D.obj i)] [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    (hc : IsLimit c)
    (L : c.pt.Modules)
    (hL : IsInvertible c.pt.sheaf.obj c.pt.ringCatSheaf.property L) :
    ∃ (i : I) (Lᵢ : (D.obj i).Modules),
      IsInvertible (D.obj i).sheaf.obj (D.obj i).ringCatSheaf.property Lᵢ ∧
        Nonempty (L ≅ (Scheme.Modules.pullback (c.π.app i)).obj Lᵢ)

Tag 05LY, a lemma

Tag 05LY in the Stacks Project.

AlgebraicGeometry.eventually_isFlatOver_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/RelativeApproximation/FlatDescent.lean, line 903. References: EGA IV (11.2.6), “(ii)”.

If a finitely presented quasi-coherent module at one stage of a cofiltered inverse system becomes flat over the base-changed target at the limit, it is flat over that target after passing to some later stage.

theorem eventually_isFlatOver_modulePullback
    {I : Type v} [Category.{w} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [∀ {i j : I} (e : i ⟶ j), IsAffineHom (D.map e)]
    [∀ i : I, CompactSpace (D.obj i)]
    [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    (i : I) (X Y : Over (D.obj i))
    (hX : FinitePresentation X.hom) (hY : FinitePresentation Y.hom)
    (f : X ⟶ Y)
    (F : SheafOfModules.{u} (structureSheafRing X.left.toRingedSpace))
    [F.IsQuasicoherent] [F.IsFinitePresentation]
    (hflat : IsFlatOver
      ((Over.pullback (c.π.app i)).map f).left.toLRSHom.toShHom
      ((modulePullback
        (pullback.fst X.hom (c.π.app i)).toLRSHom.toShHom).obj F)) :
    ∃ (j : I) (e : j ⟶ i), IsFlatOver
      ((Over.pullback (D.map e)).map f).left.toLRSHom.toShHom
      ((modulePullback
        (pullback.fst X.hom (D.map e)).toLRSHom.toShHom).obj F)

Tag 0EY1, a lemma

Tag 0EY1 in the Stacks Project.

AlgebraicGeometry.LimitDescent.exists_model_of_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LimitDescentGlueing/GeneralStages.lean, line 351. The attribute's comment: “essential surjectivity, arbitrary stages”. References: EGA IV (8.1.1), “more general”; EGA IV (8.8.2), “more general”; EGA IV (8.8.3), “essential surjectivity”; SGA 4 VII (5.3), “essential surjectivity”; SGA 3 VIB (10.0), “more general”; SGA 4 VII (5.2), “more general”.

Essential surjectivity in Stacks Tag 0EY1, at the generality the source states.

Let S = lim Sᵢ be a directed inverse limit of schemes with affine transition morphisms — no finiteness hypothesis whatsoever is made on the stages Sᵢ — and let X be a quasi-compact, quasi-separated scheme locally of finite presentation over S. Then X is isomorphic, over S, to the base change of a quasi-compact, quasi-separated scheme locally of finite presentation over one of the stages Sᵢ.

This is AlgebraicGeometry.LimitDescent.exists_model_of_finitePresentation with the stage hypotheses CompactSpace (D.obj i) and QuasiSeparatedSpace (D.obj i) removed, so that that result is the special case of this one in which the stages are quasi-compact and quasi-separated; over such a stage the conclusion is AlgebraicGeometry.FinitePresentation of the model, by AlgebraicGeometry.finitePresentation_of_compactSpace. The source assumes nothing about the stages, which is why the statement is in terms of a quasi-compact, quasi-separated source and a morphism locally of finite presentation rather than in terms of finite presentation.

The index hypothesis CategoryTheory.FinallySmall.{u} I asks that I have a u-small cofinal set of objects; it is automatic for the directed set of the source, and is needed because the comparison of the sections of the limit with the sections at the stages is a statement about an index category at the scheme universe.

public theorem exists_model_of_locallyOfFinitePresentation
    {I : Type v} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)] [FinallySmall.{u} I]
    (D : Iᵒᵖ ⥤ Scheme.{u}) [∀ {i j : Iᵒᵖ} (a : i ⟶ j), IsAffineHom (D.map a)]
    (c : Cone D) (hc : IsLimit c) (X : Over c.pt)
    (hXqc : CompactSpace X.left) (hXqs : QuasiSeparatedSpace X.left)
    (hX : LocallyOfFinitePresentation X.hom) :
    ∃ (i : I) (Xᵢ : Over (D.obj (.op i))),
      CompactSpace Xᵢ.left ∧ QuasiSeparatedSpace Xᵢ.left ∧
        LocallyOfFinitePresentation Xᵢ.hom ∧
        Nonempty (X ≅ (Over.pullback (c.π.app (.op i))).obj Xᵢ)

AlgebraicGeometry.LimitDescent.isEquivalence_baseChangeComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LimitDescentGlueing/GeneralStagesEquivalence.lean, line 925. References: EGA IV (8.1.1), “more general”; EGA IV (8.8.3), “more general”; SGA 3 VIB (10.0), “more general”; SGA 4 VII (5.2), “more general”; SGA 4 VII (5.3), “more general”.

For a scheme T let C_T be the full subcategory of schemes W over T such that W is quasi-compact and quasi-separated and such that the structure morphism W ⟶ T is locally of finite presentation. Let S = lim Sᵢ be a directed inverse limit of schemes with affine transition morphisms, indexed by a finally u-small I, with no finiteness hypothesis on the stages Sᵢ. Then the base change functors induce an equivalence of categories colim C_{Sᵢ} ⥤ C_S.

The colimit is the colimit in CategoryTheory.Cat of the strict model AlgebraicGeometry.LimitDescent.stageDiagram of the diagram i ↦ C_{Sᵢ}, and the functor is AlgebraicGeometry.LimitDescent.baseChangeComparison, the colimit descent of the base change functors C_{Sᵢ} ⥤ C_S.

public theorem isEquivalence_baseChangeComparison :
    (baseChangeComparison D c hc).IsEquivalence

AlgebraicGeometry.LimitDescent.isEquivalence_baseChangeComparison_of_directedSet, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LimitDescentGlueing/GeneralStagesEquivalence.lean, line 946. References: EGA IV (8.8.3), “more general”; SGA 3 VIB (10.0), “more general”; SGA 4 VII (5.3), “more general”.

Let S = lim Sᵢ be the limit of an inverse system of schemes indexed by a directed set I in the universe of the schemes, with affine transition morphisms. Then the base change functors induce an equivalence of categories colim C_{Sᵢ} ⥤ C_S, where C_T is the category of quasi-compact, quasi-separated schemes locally of finite presentation over T.

public theorem isEquivalence_baseChangeComparison_of_directedSet
    {I : Type u} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (D : Iᵒᵖ ⥤ Scheme.{u}) [∀ {a b : Iᵒᵖ} (t : a ⟶ b), IsAffineHom (D.map t)]
    (c : Cone D) (hc : IsLimit c) :
    (baseChangeComparison D c hc).IsEquivalence

Sources

LeanAlgebraicGeometry.LimitDescent.exists_model_of_finitePresentation_of_essentiallySmall · AlgebraicGeometry.exists_morphism_after_baseChange · AlgebraicGeometry.eventually_eq_of_baseChange_eq · AlgebraicGeometry.Scheme.eventually_eq_of_baseChange_eq · AlgebraicGeometry.LimitFPObjectDescent.exists_model_of_finitePresentation · Stacks.AlgebraicGeometry.ModuleLimits.exists_pullback_map_eq_of_isLimit · Stacks.AlgebraicGeometry.ModuleLimits.exists_map_of_pullback_of_isLimit · Stacks.AlgebraicGeometry.ModuleLimits.exists_isFinitePresentation_pullback_iso_of_qcqs

Section32.11 Characterizing affine schemes #

Section 32.11 of the Stacks Project, Tag 01ZS. 6 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01ZT, a lemma

Tag 01ZT in the Stacks Project.

Stacks.AffineFromFiniteSurjective.isAffine_of_finite_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/AffineFromFiniteSurjective.lean, line 133.

The target of a finite surjective morphism of schemes is affine when its source is affine.

theorem isAffine_of_finite_surjective {X S : Scheme.{u}} (f : X ⟶ S)
    [IsFinite f] [Surjective f] [IsAffine X] : IsAffine S

Tag 05YU, a proposition

Tag 05YU in the Stacks Project.

Stacks.AffineFromUniversallyClosed.isAffine_of_surjective_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/AffineFromSurjectiveUniversallyClosed.lean, line 220.

[Stacks, Tag 05YU]. A scheme admitting a surjective universally closed morphism from an affine scheme is affine.

By the reduction above the morphism is integral over a separated, quasi-compact and quasi-separated base, so f_* 𝒪_X is an integral quasi-coherent sheaf of 𝒪_S-algebras. Part (1) of [Stacks, Tag 0817] presents it as a directed colimit of finite quasi-coherent subalgebras, indexed in the universe of the scheme, and the relative spectrum turns that colimit into an inverse system of schemes finite over S whose limit is X. One stage of that system is affine by [Stacks, Tag 01Z6], and is surjective over S because f factors through it, so [Stacks, Tag 01ZT] applies to it.

theorem isAffine_of_surjective_universallyClosed [IsAffine X] [Surjective f]
    [UniversallyClosed f] : IsAffine S

Tag 09NL, a lemma

Tag 09NL in the Stacks Project.

Stacks.AffineClosedUnion.isAffine_of_isClosedImmersion_iUnion_of_surjective_appTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineClosedUnion/Reduction.lean, line 131.

[Stacks, Tag 09NL], granted that global functions lift to the ambient scheme. A scheme which is set theoretically the union of finitely many affine closed subschemes is affine, provided every global function on its reduced induced closed subscheme is the restriction of a global function on it.

The hypothesis hlift is the only thing assumed, it concerns the single morphism X.nilradical.subschemeι, and it is the cohomological content of [Stacks, Tag 06AD] for that thickening: see the module docstring. Everything else — that the reduced induced closed subscheme is affine — is Stacks.AffineClosedUnion.isAffine_nilradical_subscheme_of_isClosedImmersion_iUnion.

theorem isAffine_of_isClosedImmersion_iUnion_of_surjective_appTop {ι : Type*} [Finite ι]
    {Z : ι → Scheme.{u}} (f : ∀ i, Z i ⟶ X) [∀ i, IsClosedImmersion (f i)]
    [∀ i, IsAffine (Z i)] (hcov : ⋃ i, Set.range (f i).base = Set.univ)
    (hlift : Function.Surjective X.nilradical.subschemeι.appTop.hom) : IsAffine X

Stacks.AffineClosedUnion.isAffine_of_surjective_sigmaDesc_of_surjective_appTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineClosedUnion/Reduction.lean, line 147.

[Stacks, Tag 09NL] in the tag's own vocabulary, granted that global functions lift to the ambient scheme. The covering hypothesis is surjectivity of the morphism from the coproduct, as in the tag; it is the same hypothesis by Stacks.AffineClosedUnion.surjective_sigmaDesc_iff.

The hypothesis hlift is as in Stacks.AffineClosedUnion.isAffine_of_isClosedImmersion_iUnion_of_surjective_appTop.

theorem isAffine_of_surjective_sigmaDesc_of_surjective_appTop {ι : Type v} [Finite ι]
    {Z : ι → Scheme.{u}} (f : ∀ i, Z i ⟶ X) [∀ i, IsAffine (Z i)]
    [∀ i, IsClosedImmersion (f i)] [hsurj : Surjective (Sigma.desc f)]
    (hlift : Function.Surjective X.nilradical.subschemeι.appTop.hom) : IsAffine X

Stacks.AffineClosedUnion.isAffine_of_isClosedImmersion_iUnion_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineClosedUnion/Unconditional.lean, line 61.

[Stacks, Tag 09NL]. A scheme which is set theoretically the union of finitely many affine closed subschemes is affine. Nothing is assumed about the ambient scheme.

Its reduced induced closed subscheme is affine by Stacks.AffineClosedUnion.isAffine_nilradical_subscheme_of_isClosedImmersion_iUnion, and X is a thickening of that subscheme by Stacks.AffineClosedUnion.isThickening_subschemeι_nilradical, so [Stacks, Tag 06AD] in the form Stacks.Thickenings.isAffine_of_isThickening gives affineness of X itself.

theorem isAffine_of_isClosedImmersion_iUnion_unconditional {ι : Type*} [Finite ι]
    {Z : ι → Scheme.{u}} (f : ∀ i, Z i ⟶ X) [∀ i, IsClosedImmersion (f i)]
    [∀ i, IsAffine (Z i)] (hcov : ⋃ i, Set.range (f i).base = Set.univ) : IsAffine X

Stacks.AffineClosedUnion.isAffine_of_surjective_sigmaDesc_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineClosedUnion/Unconditional.lean, line 72.

[Stacks, Tag 09NL] in the tag's own vocabulary. The covering is surjectivity of the morphism from the coproduct of the affine closed subschemes, as the tag states it; it is the same hypothesis as a union of ranges by Stacks.AffineClosedUnion.surjective_sigmaDesc_iff.

theorem isAffine_of_surjective_sigmaDesc_unconditional {ι : Type v} [Finite ι]
    {Z : ι → Scheme.{u}} (f : ∀ i, Z i ⟶ X) [∀ i, IsAffine (Z i)]
    [∀ i, IsClosedImmersion (f i)] [hsurj : Surjective (Sigma.desc f)] : IsAffine X

Tag 09MW, a lemma

Tag 09MW in the Stacks Project.

Stacks.AmpleThickeningAscent.isAmple_modulePullback_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleThickeningAscent/Basic.lean, line 66.

[Stacks, Tag 09MW]. Let i : Z ⟶ X be a closed immersion of schemes inducing a homeomorphism of underlying topological spaces, and 𝓛 an invertible 𝒪_X-module. Then i^* 𝓛 is ample on Z if and only if 𝓛 is ample on X. No Noetherian hypothesis.

The implication 𝓛 ample ⟹ i^* 𝓛 ample is Stacks.AmpleThickeningLimit.isAmple_modulePullback; the converse is Stacks.AmpleThickeningAscent.isAmple_of_isAmple_pullback_of_isThickening.

theorem isAmple_modulePullback_iff {Z X : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
    (hi : IsHomeomorph i.base) (L : X.Modules) [IsInvertibleModule X L] :
    IsAmple Z ((modulePullback i.toLRSHom.toShHom).obj L) ↔ IsAmple X L

Stacks.AmpleThickeningLimit.isAmple_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleThickeningLimit/Basic.lean, line 121. The attribute's comment: “the implication L ample ⟹ i^* L ample”.

The implication L ample ⟹ i^* L ample of [Stacks, Tag 09MW]. For a closed immersion i : Z ⟶ X inducing a homeomorphism of underlying spaces and an invertible 𝒪_X-module L, ampleness of L gives ampleness of i^* L. No Noetherian hypothesis.

The homeomorphism hypothesis is not used — hence its binder is named _hi: the proof needs only that i is an affine morphism. It is carried so that this is literally one half of the source statement rather than a more general lemma wearing the tag of [Stacks, Tag 09MW]. Neither is this half of the source any harder than part (2) of [Stacks, Tag 0892] for a quasi-affine morphism, which Stacks.SectionRatioNoAmple.isAmple_modulePullback_of_isQuasiAffineHom proves with no premise; a closed immersion is affine, and an affine morphism is quasi-affine because the inverse image of an affine open is affine.

This is Stacks.AmpleSurjectiveThickening.isAmple_modulePullback — the same half of [Stacks, Tag 09MS] — with its [Surjective i] and [IsNoetherian X] hypotheses dropped, which is exactly the difference between the two tags on this side of the biconditional.

theorem isAmple_modulePullback [IsClosedImmersion i] (_hi : IsHomeomorph i.base)
    (hL : IsAmple X L) :
    IsAmple Z ((modulePullback i.toLRSHom.toShHom).obj L)

Stacks.AmpleThickeningLimit.isAmple_modulePullback_iff_of_isHomeomorph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleThickeningLimit/Unconditional.lean, line 213.

[Stacks, Tag 09MW]. Let i : Z ⟶ X be a closed immersion of schemes inducing a homeomorphism of underlying topological spaces, and let L be an invertible 𝒪_X-module. Then i^* L is ample on Z if and only if L is ample on X.

No hypothesis beyond the source's: neither Noetherianness nor separatedness nor quasi-compactness of either scheme is assumed. The mpr half is Stacks.AmpleThickeningLimit.isAmple_modulePullback; the mp half is Stacks.AmpleThickeningLimit.isAmple_of_isAmple_modulePullback_of_isHomeomorph.

theorem isAmple_modulePullback_iff_of_isHomeomorph [IsClosedImmersion i]
    (hi : IsHomeomorph i.base) :
    IsAmple Z ((modulePullback i.toLRSHom.toShHom).obj L) ↔ IsAmple X L

Tag 0B7L, a lemma

Tag 0B7L in the Stacks Project.

Stacks.Thickenings.isQuasiAffine_of_isQuasiAffine_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Affine.lean, line 292. The attribute's comment: “the implication: ambient quasi-affine ⟹ closed subscheme quasi-affine”.

The implication ambient quasi-affine ⟹ closed subscheme quasi-affine of [Stacks Project, Tag 0B7L]. If the ambient scheme of a thickening i : X ⟶ X' is quasi-affine, then so is the closed subscheme.

This is the implication the source calls elementary, and it is: a closed immersion is an affine morphism, and AlgebraicGeometry.Scheme.IsQuasiAffine.of_isAffineHom says the source of an affine morphism into a quasi-affine scheme is quasi-affine. Surjectivity of i is not used; it is carried because it is half of the source's hypothesis, so that this is literally one implication of the source statement.

The source's hypothesis that i is a closed immersion inducing a homeomorphism of underlying spaces is Stacks.Thickenings.IsThickening: for a closed immersion, being a homeomorphism on points is being surjective, which is Stacks.Thickenings.IsThickening.isHomeomorph.

The reverse implication is the one part (9) of [Stacks Project, Tag 09ZV] needs. It is isolated as Stacks.Thickenings.QuasiAffineAscendsAlongThickening, and it is proved for every finite-order thickening in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/QuasiAffineAscent.lean (Stacks.Thickenings.isQuasiAffine_of_isFiniteOrderThickening), hence for every thickening of a locally Noetherian scheme, and for an arbitrary thickening in Stacks.Thickenings.isQuasiAffine_of_isThickening of StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/QuasiAffineLimit.lean.

theorem isQuasiAffine_of_isQuasiAffine_ambient {X X' : Scheme.{u}} {i : X ⟶ X'}
    (hi : IsThickening i) (hX' : Scheme.IsQuasiAffine X') : Scheme.IsQuasiAffine X

Stacks.Thickenings.isQuasiAffine_iff_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/QuasiAffineLimit.lean, line 315.

[Stacks Project, Tag 0B7L]. For a closed immersion inducing a homeomorphism of underlying spaces — equivalently, a surjective closed immersion — the ambient scheme is quasi-affine if and only if the closed subscheme is. No Noetherian hypothesis.

Ambient ⟹ closed subscheme is the elementary implication, a closed immersion being affine (Stacks.Thickenings.isQuasiAffine_of_isQuasiAffine_ambient); closed subscheme ⟹ ambient is Stacks.Thickenings.isQuasiAffine_of_isThickening. This supersedes the Noetherian Stacks.Thickenings.isQuasiAffine_iff_of_isNoetherian, which is [Stacks Project, Tag 0B7K].

theorem isQuasiAffine_iff_of_isThickening {Y Y' : Scheme.{u}} {k : Y ⟶ Y'}
    (hk : IsThickening k) : Scheme.IsQuasiAffine Y' ↔ Scheme.IsQuasiAffine Y

Tag 0E21, a lemma

Tag 0E21 in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.exists_affine_nonvanishingOpen_factorsThrough, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/CommonStage.lean, line 285.

[Stacks, Tag 0E21].

Let L be an ample invertible sheaf on a scheme X, let W ⊆ X be open and let Spec A ⟶ W be a family of points of W parametrised by an integral algebra A over a field k. Then there is an n > 0 and a global section s of L ^ ⊗ n whose nonvanishing open X_s is affine, is contained in W, and is such that Spec A ⟶ W factors through X_s.

This is exists_affine_nonvanishingOpen_factorsThrough_of_isOneAffineOpenStep with its one remaining hypothesis discharged by AlgebraicGeometry.Scheme.FiniteTypeApproximation.isOneAffineOpenStep, the single-affine step of Noetherian approximation relative to a quasi-compact open ([Stacks, Tag 07RN]).

theorem exists_affine_nonvanishingOpen_factorsThrough
    (k : Type v) (A : Type u) [Field k] [CommRing A] [Algebra k A] [Algebra.IsIntegral k A]
    (X : Scheme.{u}) (L : X.Modules)
    [hLinv : AlgebraicGeometry.SheafOfModules.IsInvertible X.toRingedSpace.presheaf
      (structureSheafRing X.toRingedSpace).property L]
    (hL : IsAmple X L)
    (W : X.Opens) (f : Spec (CommRingCat.of A) ⟶ (W : Scheme.{u})) :
    ∃ n : ℕ, 0 < n ∧
      ∃ s : (tensorPower X.toRingedSpace.presheaf
        (structureSheafRing X.toRingedSpace).property L (n : ℤ)).sections,
      ∃ U : X.Opens,
        U = nonvanishingOpen
          (tensorPower X.toRingedSpace.presheaf
            (structureSheafRing X.toRingedSpace).property L (n : ℤ)) s ∧
        IsAffineOpen U ∧ U ≤ W ∧
        ∃ g : Spec (CommRingCat.of A) ⟶ (U : Scheme.{u}), g ≫ U.ι = f ≫ W.ι

Sources

LeanStacks.AffineFromFiniteSurjective.isAffine_of_finite_surjective · Stacks.AffineFromUniversallyClosed.isAffine_of_surjective_universallyClosed · Stacks.AffineClosedUnion.isAffine_of_isClosedImmersion_iUnion_of_surjective_appTop · Stacks.AffineClosedUnion.isAffine_of_surjective_sigmaDesc_of_surjective_appTop · Stacks.AffineClosedUnion.isAffine_of_isClosedImmersion_iUnion_unconditional · Stacks.AffineClosedUnion.isAffine_of_surjective_sigmaDesc_unconditional · Stacks.AmpleThickeningAscent.isAmple_modulePullback_iff · Stacks.AmpleThickeningLimit.isAmple_modulePullback

Section32.12 Variants of Chow's Lemma #

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

Tag 0202, a lemma

Tag 0202 in the Stacks Project.

AlgebraicGeometry.hasChowModification_of_compactSpace_quasiSeparatedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ChowQcqs/Basic.lean, line 266. References: SGA 4 XVII (7.0.6), “(i), (iii)”; SGA 4 XII (7.1), “Chow diagram”.

Chow's lemma over a quasi-compact quasi-separated base. A separated morphism of finite type onto a quasi-compact quasi-separated scheme admits a proper surjective modification immersed in a projective space over the base.

theorem hasChowModification_of_compactSpace_quasiSeparatedSpace {X S : Scheme.{u}} (f : X ⟶ S)
    [CompactSpace S] [QuasiSeparatedSpace S] [IsSeparated f] [LocallyOfFiniteType f]
    [QuasiCompact f] : HasChowModification f

Tag 0203, a lemma

Tag 0203 in the Stacks Project.

AlgebraicGeometry.hasDenseChowModification_of_finite_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ChowQcqs/Basic.lean, line 302. References: EGA II (5.6.1), “(b); (i),(ii)”; SGA 4 XVII (7.0.6), “finite irred. components”; SGA 4 XII (7.1), “finite irred. components”.

[Stacks, Tag 0203]: the variant of Chow's lemma with a dense open. Let S be quasi-compact and quasi-separated, let f : X ⟶ S be separated and of finite type, and suppose X has only finitely many irreducible components. Then there are n, a scheme X', a proper surjective π : X' ⟶ X and an immersion X' ⟶ ℙⁿ_S making the triangle over S commute, such that π is an isomorphism over a dense open subscheme of X.

The dense open does not survive base change, so unlike [Stacks, Tag 0202] this cannot be had by descending X to a stage and pulling the modification back. Instead the whole inverse system Yⱼ = Sⱼ ×_{S_{i₁}} Y₁ is kept, Chow's lemma over a Noetherian base is applied to the scheme-theoretic image of X in a stage chosen so that the finitely many generic points of X have pairwise non-specializing images, and the dense open of that image then pulls back to a dense open of X because it contains every generic point.

theorem hasDenseChowModification_of_finite_irreducibleComponents {X S : Scheme.{u}} (f : X ⟶ S)
    [CompactSpace S] [QuasiSeparatedSpace S] [IsSeparated f] [LocallyOfFiniteType f]
    [QuasiCompact f] (hX : (irreducibleComponents X).Finite) :
    HasDenseChowModification f

Sources

LeanAlgebraicGeometry.hasChowModification_of_compactSpace_quasiSeparatedSpace · AlgebraicGeometry.hasDenseChowModification_of_finite_irreducibleComponents

Section32.13 Applications of Chow's lemma #

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

Tag 081F, a lemma

Tag 081F in the Stacks Project.

AlgebraicGeometry.exists_isProper_baseChange_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ChowFiniteType/ModuleSupport.lean, line 202.

Stacks 081F. Assumptions and notation as in Situation 081D: D is a cofiltered inverse system of schemes with affine transition morphisms and limit cone c, and f₀ : X₀ ⟶ Y₀ is a morphism of quasi-compact quasi-separated schemes over the quasi-compact quasi-separated stage D.obj i₀. If f₀ is locally of finite type and its base change to the limit is proper, then its base change to some later stage is proper.

Chow's lemma over the quasi-compact quasi-separated Y₀ needs f₀ to be separated, which is not assumed; following the Stacks proof, Stacks 01ZQ supplies separatedness at some stage i₁ and the situation is re-indexed there before AlgebraicGeometry.exists_isProper_baseChange_of_isLimit_of_isOneAffineOpenStep is applied.

theorem exists_isProper_baseChange_of_isLimit
    (hc : IsLimit c) (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFiniteType f₀.left]
    [IsProper ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (hi : i ⟶ i₀), IsProper ((Over.pullback (D.map hi)).map f₀).left

Tag 09ZR, a lemma

Tag 09ZR in the Stacks Project.

AlgebraicGeometry.exists_isLimit_isProper_finitePresentation_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/ProperFinitePresentationLimit.lean, line 66.

Stacks 09ZR. A proper morphism onto a quasi-compact, quasi-separated scheme is a directed inverse limit, over that scheme, of proper morphisms of finite presentation whose transition morphisms and limit projections are all closed immersions.

theorem exists_isLimit_isProper_finitePresentation_isClosedImmersion
    {X S : Scheme.{u}} (f : X ⟶ S) [IsProper f]
    [CompactSpace S] [QuasiSeparatedSpace S] :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (D : Iᵒᵖ ⥤ Scheme.{u}) (t : D ⟶ (Functor.const Iᵒᵖ).obj S)
      (p : (Functor.const Iᵒᵖ).obj X ⟶ D) (_ : IsLimit (Cone.mk X p)),
      p ≫ t = (Functor.const Iᵒᵖ).map f ∧
        (∀ i, IsProper (t.app i) ∧ FinitePresentation (t.app i)) ∧
        (∀ (i j : Iᵒᵖ) (g : i ⟶ j), IsClosedImmersion (D.map g)) ∧
        (∀ i, IsClosedImmersion (p.app i))

Tag 0A0P, a lemma

Tag 0A0P in the Stacks Project.

AlgebraicGeometry.exists_isLimit_isProper_finiteType_arrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/ProperLimitOfFiniteTypeOverZ.lean, line 230.

Stacks 0A0P. A proper morphism onto a quasi-compact and quasi-separated scheme is the inverse limit, over a directed set, of an inverse system of proper morphisms whose targets are of finite type over ℤ and whose transition morphisms are affine on both sources and targets.

theorem exists_isLimit_isProper_finiteType_arrow
    {X S : Scheme.{u}} (f : X ⟶ S) [IsProper f]
    [CompactSpace S] [QuasiSeparatedSpace S] :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirectedOrder I)
      (D : Iᵒᵖ ⥤ Arrow Scheme.{u}) (c : Cone D),
      (∀ i, IsProper (D.obj i).hom) ∧
      (∀ i,
        LocallyOfFiniteType (terminal.from (D.obj i).right) ∧
          QuasiCompact (terminal.from (D.obj i).right)) ∧
      (∀ {i j : Iᵒᵖ} (g : i ⟶ j),
        IsAffineHom (D.map g).left ∧ IsAffineHom (D.map g).right) ∧
      Nonempty (IsLimit c) ∧ Nonempty (c.pt ≅ Arrow.mk f)

Tag 0EX1, a lemma

Tag 0EX1 in the Stacks Project.

AlgebraicGeometry.eventually_isProper_comp_π_app_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/EventuallyProperOverLimit.lean, line 307.

Stacks 0EX1. Let X = lim Xᵢ be the limit of a cofiltered inverse system of quasi-compact and quasi-separated schemes over S with affine transition morphisms. A proper morphism f : Y ⟶ X whose source is locally of finite type over S is proper over some stage of the system and over every later stage.

theorem eventually_isProper_comp_π_app_of_isLimit
    {I : Type v} [Category.{v} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    {S : Scheme.{u}} (D : I ⥤ Scheme.{u}) (t : D ⟶ (Functor.const I).obj S)
    (c : Cone D) (hc : IsLimit c) (pX : c.pt ⟶ S)
    (hpX : c.π ≫ t = (Functor.const I).map pX)
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    [∀ i : I, CompactSpace (D.obj i)] [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    {Y : Scheme.{u}} (pY : Y ⟶ S) (f : Y ⟶ c.pt) (hf : f ≫ pX = pY)
    [LocallyOfFiniteType pY] [IsProper f] :
    ∃ i : I, ∀ (j : I) (_ : j ⟶ i), IsProper (f ≫ c.π.app j)

Tag 081G, a lemma

Tag 081G in the Stacks Project.

AlgebraicGeometry.exists_isProper_schemeTheoreticSupport_baseChange_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ChowFiniteType/ModuleSupport.lean, line 250.

Stacks 081G. Assumptions and notation as in Situation 081D, and let F₀ be a quasi-coherent O_{X₀}-module, with F and F_i its pullbacks to the base changes X and X_i of X₀. Assume f₀ is locally of finite type, F₀ is 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.

The base change of X₀ to a stage is the fibre product of X₀.hom with the transition morphism, so the pullback of F₀ to it is its pullback along CategoryTheory.Limits.pullback.fst. The proof applies Stacks 081F to the restriction of f₀ to the scheme-theoretic support of F₀.

theorem exists_isProper_schemeTheoreticSupport_baseChange_of_isLimit
    (hc : IsLimit c) (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀) (F₀ : X₀.left.Modules)
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFiniteType f₀.left] [F₀.IsQuasicoherent] [F₀.IsFiniteType]
    (hlim : IsProper ((Scheme.Modules.schemeTheoreticSupport
        ((Scheme.Modules.pullback (pullback.fst X₀.hom (c.π.app i₀))).obj F₀)).subschemeι ≫
        ((Over.pullback (c.π.app i₀)).map f₀).left)) :
    ∃ (i : I) (hi : i ⟶ i₀), IsProper ((Scheme.Modules.schemeTheoreticSupport
        ((Scheme.Modules.pullback (pullback.fst X₀.hom (D.map hi))).obj F₀)).subschemeι ≫
        ((Over.pullback (D.map hi)).map f₀).left)

Sources

LeanAlgebraicGeometry.exists_isProper_baseChange_of_isLimit · AlgebraicGeometry.exists_isLimit_isProper_finitePresentation_isClosedImmersion · AlgebraicGeometry.exists_isLimit_isProper_finiteType_arrow · AlgebraicGeometry.eventually_isProper_comp_π_app_of_isLimit · AlgebraicGeometry.exists_isProper_schemeTheoreticSupport_baseChange_of_isLimit

Section32.14 Universally closed morphisms #

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

Tag 05BD, a lemma

Tag 05BD in the Stacks Project.

AlgebraicGeometry.exists_affine_locallyFinitePresentation_separation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreSeparation/Basic.lean, line 64.

Stacks Project, Tag 05BD. A closed subscheme of a base change X ×_S T avoiding the fibre of X ×_S T ⟶ T over a point t, for f : X ⟶ S quasi-compact, can be separated from that fibre already over an affine base locally of finite presentation over S: there is an affine open V ∋ t, an affine T' locally of finite presentation over S with a factorization of V ⟶ T through it, and a closed subscheme of X ×_S T' containing the restriction of the given one and still avoiding the fibre over the image of t.

theorem exists_affine_locallyFinitePresentation_separation
    {X S T : Scheme.{u}} (f : X ⟶ S) [QuasiCompact f] (g : T ⟶ S)
    (t : T) (I : (pullback f g).IdealSheafData)
    (ht : t ∉ Set.image (pullback.snd f g) I.support.1) :
    ∃ (V : T.affineOpens) (htV : t ∈ V.1)
      (T' : Scheme.{u}) (_ : IsAffine T') (b : T' ⟶ S)
      (_ : LocallyOfFinitePresentation b) (a : V.1.toScheme ⟶ T')
      (_ : V.1.ι ≫ g = a ≫ b)
      (I' : (pullback f b).IdealSheafData)
      (p : pullback f (V.1.ι ≫ g) ⟶ pullback f g)
      (q : pullback f (V.1.ι ≫ g) ⟶ pullback f b),
      (p ≫ pullback.fst f g = pullback.fst f (V.1.ι ≫ g)) ∧
      (p ≫ pullback.snd f g = pullback.snd f (V.1.ι ≫ g) ≫ V.1.ι) ∧
      (q ≫ pullback.fst f b = pullback.fst f (V.1.ι ≫ g)) ∧
      (q ≫ pullback.snd f b = pullback.snd f (V.1.ι ≫ g) ≫ a) ∧
      (a ⟨t, htV⟩ ∉ Set.image (pullback.snd f b) I'.support.1) ∧
      (I'.comap q ≤ I.comap p)

Tag 05JX, a lemma

Tag 05JX in the Stacks Project.

AlgebraicGeometry.universallyClosed_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/UniversallyClosedTest.lean, line 62.

Stacks 05JX. A quasi-compact morphism is universally closed precisely when all of its locally finitely presented base changes are closed, or equivalently when its base changes to all finite-dimensional affine spaces are closed.

theorem universallyClosed_tfae {X S : Scheme.{u}} (f : X ⟶ S)
    [QuasiCompact f] :
    List.TFAE
      [UniversallyClosed f,
       ∀ (S' : Scheme.{u}) (g : S' ⟶ S),
         LocallyOfFinitePresentation g → IsClosedMap (pullback.snd f g),
       ∀ n : ℕ, IsClosedMap (AffineSpace.map (ULift.{u} (Fin n)) f)]

Tag 0205, a lemma

Tag 0205 in the Stacks Project.

AlgebraicGeometry.isProper_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/ProperTest.lean, line 42.

A separated morphism of finite type is proper precisely when all of its base changes along morphisms locally of finite type are closed, or equivalently when its base changes to all finite-dimensional affine spaces are closed.

The second condition is the hypothesis that X ×_S S' ⟶ S' is a closed map for every S' ⟶ S locally of finite type, and the third that 𝔸(n; X) ⟶ 𝔸(n; S), the base change of f along 𝔸(n; S) ↘ S, is a closed map for every n.

theorem isProper_tfae {X S : Scheme.{u}} (f : X ⟶ S)
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f] :
    List.TFAE
      [IsProper f,
       ∀ (S' : Scheme.{u}) (g : S' ⟶ S),
         LocallyOfFiniteType g → IsClosedMap (pullback.snd f g),
       ∀ n : ℕ, IsClosedMap (AffineSpace.map (ULift.{u} (Fin n)) f)]

Tag 05LZ, an equation

Tag 05LZ in the Stacks Project.

AlgebraicGeometry.exists_surjective_isClosedImmersion_projectiveSpace_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/ProperCheckSquare.lean, line 139.

The square of [Stacks, Tag 05LZ]. Let f : X ⟶ S be proper and admit a Chow modification. Then there are an n, a scheme X', a proper surjective morphism π : X' ⟶ X and a closed immersion i : X' ⟶ ℙⁿ_S with π ≫ f = i ≫ (ℙⁿ_S ↘ S), that is, a commutative square
X' ---i---> ℙⁿ_S
|            |
π            |
v            v
X ----f----> S
over S whose left vertical morphism is surjective and whose top morphism is a closed immersion into projective space over S.

Chow's lemma supplies the square with i merely an immersion; properness of f upgrades it to a closed immersion.

theorem exists_surjective_isClosedImmersion_projectiveSpace_of_isProper (f : X ⟶ S) [IsProper f]
    (hf : HasChowModification f) :
    ∃ (n : ℕ) (X' : Scheme.{u}) (π : X' ⟶ X) (i : X' ⟶ ProjectiveSpace n S),
      IsProper π ∧ Surjective π ∧ IsClosedImmersion i ∧
        π ≫ f = i ≫ (ProjectiveSpace n S ↘ S)

AlgebraicGeometry.exists_projectiveSpace_square_isProper_iff_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/ProperCheckSquareChow.lean, line 50.

Let S be quasi-compact and quasi-separated and let f : X ⟶ S be separated and of finite type. Then there are an n, a scheme X', a proper surjective morphism π : X' ⟶ X and an immersion i : X' ⟶ ℙⁿ_S with π ≫ f = i ≫ (ℙⁿ_S ↘ S). Moreover f is proper if and only if i is a closed immersion.

theorem exists_projectiveSpace_square_isProper_iff_isClosedImmersion {X S : Scheme.{u}}
    (f : X ⟶ S) [CompactSpace S] [QuasiSeparatedSpace S] [IsSeparated f] [LocallyOfFiniteType f]
    [QuasiCompact f] :
    ∃ (n : ℕ) (X' : Scheme.{u}) (π : X' ⟶ X) (i : X' ⟶ ProjectiveSpace n S),
      IsProper π ∧ Surjective π ∧ IsImmersion i ∧ π ≫ f = i ≫ (ProjectiveSpace n S ↘ S) ∧
        (IsProper f ↔ IsClosedImmersion i)

Declarations registered for the tag:

AlgebraicGeometry.HasChowModification, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/ChowFiniteType/Basic.lean, line 92 (StacksFrontier): “the displayed diagram, as the predicate HasChowModification”.

Sources

LeanAlgebraicGeometry.exists_affine_locallyFinitePresentation_separation · AlgebraicGeometry.universallyClosed_tfae · AlgebraicGeometry.isProper_tfae · AlgebraicGeometry.exists_surjective_isClosedImmersion_projectiveSpace_of_isProper · AlgebraicGeometry.exists_projectiveSpace_square_isProper_iff_isClosedImmersion · AlgebraicGeometry.HasChowModification

Section32.15 Noetherian valuative criterion #

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

Tag 0CM2, a lemma

Tag 0CM2 in the Stacks Project.

AlgebraicGeometry.nonempty_discreteValuationSpecialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/NoetherianValuativeCriterion/DiscreteValuationSpecialization.lean, line 356.

A point in the closure of the image of a finite-type morphism into a locally Noetherian scheme is reached by a discrete valuation ring, with generic point on a generic component of the source.

theorem nonempty_discreteValuationSpecialization {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] [QuasiCompact f] [IsLocallyNoetherian Y] (y : Y)
    (y_mem_closure : y ∈ closure (Set.range f.base)) :
    Nonempty (DiscreteValuationSpecialization f y)

Tag 0206, an equation

Tag 0206 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.ValuativeCommSq registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch32.lean, line 13 (StacksFrontier).

Tag 0207, a lemma

Tag 0207 in the Stacks Project.

AlgebraicGeometry.isSeparated_tfae_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/NoetherianValuativeCriterion/Separatedness.lean, line 626. References: EGA II (7.2.3), “Noetherian/DVR case”.

Stacks Project, Tag 0207. For a morphism locally of finite type over a locally Noetherian scheme, separatedness is equivalent to uniqueness in the valuative criterion; it suffices to use discrete valuation rings, and even the discrete valuation subrings of the function fields of the irreducible components of the source.

theorem isSeparated_tfae_of_locallyOfFiniteType {X S : Scheme.{u}} (f : X ⟶ S)
    [IsLocallyNoetherian S] [LocallyOfFiniteType f] :
    List.TFAE
      [ IsSeparated f,
        ValuativeCriterion.Uniqueness f,
        ∀ (D : ValuativeCommSq f),
          IsDiscreteValuationRing D.R → Subsingleton D.commSq.LiftStruct,
        ∀ (η : X), η ∈ genericPoints X →
          ∀ (A : Subring (X.residueField η)),
            IsDiscreteValuationRing A →
              IsFractionRing A (X.residueField η) →
                ∀ (i₂ : Spec (.of A) ⟶ S)
                  (sq : CommSq (X.fromSpecResidueField η)
                    (Spec.map (CommRingCat.ofHom A.subtype)) f i₂),
                  Subsingleton sq.LiftStruct ]

Tag 0208, a lemma

Tag 0208 in the Stacks Project.

AlgebraicGeometry.isProper_of_genericDiscreteValuativeCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/NoetherianValuativeCriterion/GenericProperness.lean, line 289. The attribute's comment: “condition (4) implies condition (1)”. References: EGA II (7.3.8), “(b)⇒(a)”; EGA IV (15.7.5), “c⇒a”; EGA IV (18.10.20), “partial”.

[Stacks, Tag 0208], condition (4) implies condition (1). A morphism of finite type to a locally Noetherian scheme is proper as soon as every valuative diagram whose valuation ring is a discrete valuation subring of the residue field at a generic point of an irreducible component of the source, with that residue field as its fraction field, and whose generic arrow is the canonical one, has exactly one dotted arrow.

theorem isProper_of_genericDiscreteValuativeCriterion (p : V ⟶ W)
    [IsLocallyNoetherian W] [LocallyOfFiniteType p] [QuasiCompact p]
    (h : GenericDiscreteValuativeCriterion p) : IsProper p

AlgebraicGeometry.isProper_tfae_genericDiscreteValuativeCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/NoetherianValuativeCriterion/GenericProperness.lean, line 342. References: EGA II (7.3.8); EGA IV (15.7.5), “a⇔c”.

[Stacks, Tag 0208]. Let S be locally Noetherian and f : X ⟶ S of finite type. The following are equivalent:

f is proper;

every valuative diagram for f has exactly one dotted arrow;

every valuative diagram for f whose valuation ring is a discrete valuation ring has exactly one dotted arrow;

for every generic point η of an irreducible component of X and every discrete valuation subring A of κ(η) with fraction field κ(η), every valuative diagram whose generic arrow is the canonical Spec κ(η) ⟶ X has exactly one dotted arrow, that is, AlgebraicGeometry.GenericDiscreteValuativeCriterion f.

Conditions (1) to (3) are AlgebraicGeometry.isProper_tfae_of_isFiniteType; (3) implies (4) because such a diagram is a valuative diagram over a discrete valuation ring, and (4) implies (1) is AlgebraicGeometry.isProper_of_genericDiscreteValuativeCriterion.

theorem isProper_tfae_genericDiscreteValuativeCriterion {X S : Scheme.{u}} (f : X ⟶ S)
    [IsLocallyNoetherian S] [LocallyOfFiniteType f] [QuasiCompact f] :
    List.TFAE
      [ IsProper f,
        ValuativeCriterion f,
        ∀ D : ValuativeCommSq f,
          IsDiscreteValuationRing D.R → Nonempty (Unique D.commSq.LiftStruct),
        GenericDiscreteValuativeCriterion f ]

AlgebraicGeometry.isProper_tfae_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/NoetherianValuativeCriterion/Properness.lean, line 58. The attribute's comment: “conditions (1), (2) and (3)”. References: EGA II (7.3.3), “Noetherian, finite type”; EGA II (7.3.8), “proper/DVR case”; EGA I (3.7.3), “more general”.

Stacks Project, Tag 0208, conditions (1), (2) and (3). For a morphism of finite type to a locally Noetherian scheme, properness, the existence of exactly one dotted arrow in every valuative square, and the existence of exactly one dotted arrow in every valuative square over a discrete valuation ring are equivalent.

theorem isProper_tfae_of_isFiniteType {X S : Scheme.{u}} (f : X ⟶ S)
    [IsLocallyNoetherian S] [LocallyOfFiniteType f] [QuasiCompact f] :
    List.TFAE
      [ IsProper f,
        ValuativeCriterion f,
        ∀ D : ValuativeCommSq f,
          IsDiscreteValuationRing D.R → Nonempty (Unique D.commSq.LiftStruct) ]

Tag 05JY, a lemma

Tag 05JY in the Stacks Project.

AlgebraicGeometry.universallyClosed_tfae_valuative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/UniversallyClosedValuative/Basic.lean, line 166. References: EGA II (7.3.8), “fin. type, Noeth. base”.

For a finite type morphism to a locally Noetherian scheme, universal closedness, closedness after adjoining any finite number of affine coordinates, the existence part of the valuative criterion, and its restriction to discrete valuation rings are equivalent.

theorem universallyClosed_tfae_valuative {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] [IsLocallyNoetherian S] :
    List.TFAE
      [ UniversallyClosed f,
        ∀ n : ℕ, IsClosedMap (AffineSpace.map (ULift.{u} (Fin n)) f),
        ValuativeCriterion.Existence f,
        ∀ (D : ValuativeCommSq f), IsDiscreteValuationRing D.R → D.commSq.HasLift ]

Sources

LeanAlgebraicGeometry.nonempty_discreteValuationSpecialization · AlgebraicGeometry.ValuativeCommSq · AlgebraicGeometry.isSeparated_tfae_of_locallyOfFiniteType · AlgebraicGeometry.isProper_of_genericDiscreteValuativeCriterion · AlgebraicGeometry.isProper_tfae_genericDiscreteValuativeCriterion · AlgebraicGeometry.isProper_tfae_of_isFiniteType · AlgebraicGeometry.universallyClosed_tfae_valuative

Section32.16 Refined Noetherian valuative criteria #

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

Tag 0CM3, a lemma

Tag 0CM3 in the Stacks Project.

AlgebraicGeometry.isProper_of_denseRange_of_exists_discreteLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/NoetherianValuativeCriterion/RefinedProperness.lean, line 369. References: EGA II (7.3.8), “(b)⇒(a)”; EGA IV (15.7.5), “c⇒a”; EGA IV (18.10.20), “partial”.

Stacks Project, Tag 0CM3. Let f : X ⟶ S and h : U ⟶ X be morphisms of schemes with S locally Noetherian, f and h of finite type, f separated and h(U) dense in X. If every commutative solid diagram with Spec(K) ⟶ U ⟶ X along the top and Spec(A) ⟶ S along the bottom, where A is a discrete valuation ring with field of fractions K, admits a dotted arrow Spec(A) ⟶ X making it commute, then f is proper.

This is isProper_of_exists_discreteLift_of_denseRange with its hypothesis h0208 discharged by isProper_of_genericDiscreteValuativeCriterion'.

theorem isProper_of_denseRange_of_exists_discreteLift
    {U X S : Scheme.{u}} (h : U ⟶ X) (f : X ⟶ S)
    [IsLocallyNoetherian S]
    [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f]
    [LocallyOfFiniteType h] [QuasiCompact h] (hdense : DenseRange h)
    (hvaluative : ∀ (D : ValuativeCommSq f) (_ : IsDiscreteValuationRing D.R)
      (g : Spec (.of D.K) ⟶ U), g ≫ h = D.i₁ → D.commSq.HasLift) :
    IsProper f

Tag 0CM4, a lemma

Tag 0CM4 in the Stacks Project.

AlgebraicGeometry.isSeparated_of_denseRange_of_subsingleton_discreteLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/NoetherianValuativeCriterion/RefinedProperness.lean, line 450.

Stacks Project, Tag 0CM4. Let f : X ⟶ S be locally of finite type with S locally Noetherian, and let h : U ⟶ X be of finite type with h(U) dense in X. If every valuative diagram for f over a discrete valuation ring whose generic arrow factors through h has at most one dotted arrow, then f is separated.

theorem isSeparated_of_denseRange_of_subsingleton_discreteLift
    {U X S : Scheme.{u}} (h : U ⟶ X) (f : X ⟶ S)
    [IsLocallyNoetherian S] [LocallyOfFiniteType f]
    [LocallyOfFiniteType h] [QuasiCompact h] (hdense : DenseRange h)
    (hvaluative : ∀ (D : ValuativeCommSq f) (_ : IsDiscreteValuationRing D.R)
      (g : Spec (.of D.K) ⟶ U), g ≫ h = D.i₁ → Subsingleton D.commSq.LiftStruct) :
    IsSeparated f

Tag 0CM5, a lemma

Tag 0CM5 in the Stacks Project.

AlgebraicGeometry.isProper_of_denseRange_of_unique_discreteLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/NoetherianValuativeCriterion/RefinedProperness.lean, line 572. References: EGA II (7.3.8), “(b)⇒(a)”.

Stacks Project, Tag 0CM5. Let f : X ⟶ S and h : U ⟶ X be of finite type with S locally Noetherian and h(U) dense in X. If every valuative diagram for f over a discrete valuation ring whose generic arrow factors through h has a unique dotted arrow, then f is proper.

There is no separatedness hypothesis on f: separatedness is what the uniqueness of the dotted arrow buys, through Stacks 0CM4.

theorem isProper_of_denseRange_of_unique_discreteLift
    {U X S : Scheme.{u}} (h : U ⟶ X) (f : X ⟶ S)
    [IsLocallyNoetherian S] [LocallyOfFiniteType f] [QuasiCompact f]
    [LocallyOfFiniteType h] [QuasiCompact h] (hdense : DenseRange h)
    (hvaluative : ∀ (D : ValuativeCommSq f) (_ : IsDiscreteValuationRing D.R)
      (g : Spec (.of D.K) ⟶ U), g ≫ h = D.i₁ → Nonempty (Unique D.commSq.LiftStruct)) :
    IsProper f

Sources

LeanAlgebraicGeometry.isProper_of_denseRange_of_exists_discreteLift · AlgebraicGeometry.isSeparated_of_denseRange_of_subsingleton_discreteLift · AlgebraicGeometry.isProper_of_denseRange_of_unique_discreteLift

Section32.17 Valuative criteria over a Nagata base #

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

Tag 0GWV, a lemma

Tag 0GWV in the Stacks Project.

Stacks.AlgebraicGeometry.Tag05JXGeneral.universallyClosed_tfae_essentiallyFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/General/Nagata.lean, line 64.

Stacks Project, Tag 0GWV. Over a Nagata base S, for a quasi-compact f : X ⟶ Y with X and Y locally of finite type over S, universal closedness, closedness of every finite-dimensional affine-space base change, and the essentially-finite-type one-dimensional extension test are equivalent.

Three of the four edges come from the Nagata files; the fourth, 2 ⇒ 1, is Stacks 05JX (3) ⇒ (1), proved in Basic.lean for an arbitrary quasi-compact morphism.

theorem universallyClosed_tfae_essentiallyFiniteType
    {S X Y : Scheme.{u}} (hX : X ⟶ S) (hY : Y ⟶ S) (f : X ⟶ Y)
    (hf : f ≫ hY = hX) (hS : IsNagataScheme S)
    [LocallyOfFiniteType hX] [LocallyOfFiniteType hY] [QuasiCompact f] :
    List.TFAE
      [UniversallyClosed f,
       ∀ n : ℕ, IsClosedMap (AffineSpace.map (ULift.{u} (Fin n)) f),
       HasEssentiallyFiniteTypeValuativeExtension f hY]

Tag 0GWW, a lemma

Tag 0GWW in the Stacks Project.

Stacks.AlgebraicGeometry.NagataValuativeCriterion.isSeparated_iff_hasEssentiallyFiniteTypeValuativeUniqueness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataValuativeCriterion/SeparatedAndProper.lean, line 168.

Stacks Project, Tag 0GWW. Over a Nagata base S, a morphism f : X ⟶ Y between schemes locally of finite type over S is separated if and only if the lift in every one-dimensional finite-type test diagram is unique.

Uniqueness for a separated morphism holds because Spec (Frac 𝒪_{C,c}) ⟶ Spec 𝒪_{C,c} is dominant and Spec 𝒪_{C,c} is reduced. Conversely the extension condition for the diagonal of f follows from the assumed uniqueness, and tag 0GWV turns it into universal closedness of the diagonal, which for an immersion means that it is a closed immersion.

theorem isSeparated_iff_hasEssentiallyFiniteTypeValuativeUniqueness
    {S X Y : Scheme.{u}} (hX : X ⟶ S) (hY : Y ⟶ S) (f : X ⟶ Y)
    (hf : f ≫ hY = hX) (hS : IsNagataScheme S)
    [LocallyOfFiniteType hX] [LocallyOfFiniteType hY] :
    IsSeparated f ↔ HasEssentiallyFiniteTypeValuativeUniqueness f hY

Stacks.AlgebraicGeometry.NagataValuativeCriterion.isSeparated_iff_hasAtMostOneLiftOverPuncturedCurves, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataValuativeCriterion/SeparatedPunctured.lean, line 148.

Stacks Project, Tag 0GWW. Let S be a Nagata scheme and let f : X ⟶ Y be a morphism of schemes locally of finite type over S. Then f is separated if and only if, for every normal integral scheme C of finite type over S, every closed point c ∈ C with dim 𝒪_{C,c} = 1, and every commutative square over S with C \ {c} ⟶ X along the top and C ⟶ Y along the bottom, at most one Spec 𝒪_{C,c} ⟶ X makes the induced square from Spec (Frac 𝒪_{C,c}) ⟶ Spec 𝒪_{C,c} to f commute.

This is isSeparated_iff_hasEssentiallyFiniteTypeValuativeUniqueness, whose condition is equivalent to this one by hasAtMostOneLiftOverPuncturedCurves_iff.

theorem isSeparated_iff_hasAtMostOneLiftOverPuncturedCurves
    {S X Y : Scheme.{u}} (hX : X ⟶ S) (hY : Y ⟶ S) (f : X ⟶ Y)
    (hf : f ≫ hY = hX) (hS : IsNagataScheme S)
    [LocallyOfFiniteType hX] [LocallyOfFiniteType hY] :
    IsSeparated f ↔ HasAtMostOneLiftOverPuncturedCurves hX hY f

Tag 0GWX, a lemma

Tag 0GWX in the Stacks Project.

Stacks.AlgebraicGeometry.NagataValuativeCriterion.isProper_iff_hasEssentiallyFiniteTypeValuativeLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataValuativeCriterion/SeparatedAndProper.lean, line 223.

Stacks Project, Tag 0GWX. Over a Nagata base S, a quasi-compact morphism f : X ⟶ Y between schemes locally of finite type over S is proper if and only if every one-dimensional finite-type test diagram admits exactly one lift.

This is formal from tags 0GWV and 0GWW and the definition of a proper morphism as one that is locally of finite type, separated and universally closed.

theorem isProper_iff_hasEssentiallyFiniteTypeValuativeLift
    {S X Y : Scheme.{u}} (hX : X ⟶ S) (hY : Y ⟶ S) (f : X ⟶ Y)
    (hf : f ≫ hY = hX) (hS : IsNagataScheme S)
    [LocallyOfFiniteType hX] [LocallyOfFiniteType hY] [QuasiCompact f] :
    IsProper f ↔ HasEssentiallyFiniteTypeValuativeLift f hY

Sources

LeanStacks.AlgebraicGeometry.Tag05JXGeneral.universallyClosed_tfae_essentiallyFiniteType · Stacks.AlgebraicGeometry.NagataValuativeCriterion.isSeparated_iff_hasEssentiallyFiniteTypeValuativeUniqueness · Stacks.AlgebraicGeometry.NagataValuativeCriterion.isSeparated_iff_hasAtMostOneLiftOverPuncturedCurves · Stacks.AlgebraicGeometry.NagataValuativeCriterion.isProper_iff_hasEssentiallyFiniteTypeValuativeLift

Section32.18 Limits and dimensions of fibres #

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

Tag 05M5, a lemma

Tag 05M5 in the Stacks Project.

AlgebraicGeometry.exists_forall_topologicalKrullDim_fiber_le_of_isLimit_of_essentiallySmall, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/FibreDimensionBound.lean, line 824.

Stacks Project, Tag 05M5, for an index category that is essentially small relative to the universe of the schemes: a uniform bound on the dimensions of the fibres of a morphism between inverse limits already holds at some stage.

public lemma exists_forall_topologicalKrullDim_fiber_le_of_isLimit_of_essentiallySmall
    {I : Type v} [Category.{w} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (X S : I ⥤ Scheme.{u}) (f : X ⟶ S)
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (S.map g)]
    [∀ i : I, CompactSpace (S.obj i)] [∀ i : I, QuasiSeparatedSpace (S.obj i)]
    [∀ i : I, LocallyOfFiniteType (f.app i)] [∀ i : I, QuasiCompact (f.app i)]
    [∀ {i j : I} (g : i ⟶ j),
      IsClosedImmersion (pullback.lift (X.map g) (f.app i) (f.naturality g))]
    (cX : Cone X) (hcX : IsLimit cX) (cS : Cone S) (hcS : IsLimit cS) (d : ℕ)
    (hdim : ∀ s : cS.pt,
      topologicalKrullDim
        ((hcS.lift ((Cone.postcompose f).obj cX)).fiber s) ≤ (d : WithBot ℕ∞)) :
    ∃ i : I, ∀ s : S.obj i,
      topologicalKrullDim ((f.app i).fiber s) ≤ (d : WithBot ℕ∞)

Tag 094M, a lemma

Tag 094M in the Stacks Project.

AlgebraicGeometry.exists_quasiFinite_baseChange_of_quasiFinite_limitBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/QuasiFinite.lean, line 91.

Let c be a limit cone of a cofiltered diagram D of schemes with affine transition morphisms, and let f₀ : X₀ ⟶ Y₀ be a morphism locally of finite type of quasi-compact and quasi-separated schemes over the quasi-compact and quasi-separated stage D.obj i₀. If the base change of f₀ to the limit is quasi-finite, then the base change of f₀ to some later stage is quasi-finite.

theorem exists_quasiFinite_baseChange_of_quasiFinite_limitBaseChange
    {I : Type u} [Category.{u} I] [IsCofiltered I] (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    (c : Cone D) (hc : IsLimit c) (i₀ : I)
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFiniteType f₀.left]
    [LocallyOfFiniteType ((Over.pullback (c.π.app i₀)).map f₀).left]
    [QuasiCompact ((Over.pullback (c.π.app i₀)).map f₀).left]
    [LocallyQuasiFinite ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (g : i ⟶ i₀),
      (LocallyOfFiniteType ((Over.pullback (D.map g)).map f₀).left ∧
          QuasiCompact ((Over.pullback (D.map g)).map f₀).left) ∧
        LocallyQuasiFinite ((Over.pullback (D.map g)).map f₀).left

Tag 0H3V, a lemma

Tag 0H3V in the Stacks Project.

AlgebraicGeometry.exists_relativeDimensionLE_baseChange_of_limitBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/RelativeDimension.lean, line 431.

In the situation of Tag 081D, if the base change of f₀ to the limit has relative dimension at most d and f₀ is locally of finite type, then the base change of f₀ to some later stage has relative dimension at most d.

theorem exists_relativeDimensionLE_baseChange_of_limitBaseChange
    (D : DescentSituation.{u, u} I)
    (X₀ Y₀ : Over (D.system.obj (op D.base))) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFiniteType f₀.left] (d : ℕ)
    (h : RelativeDimensionLE (baseChangeMap (D.limitCone.π.app (op D.base)) X₀ Y₀ f₀) d) :
    ∃ (i : I) (hi : D.base ≤ i),
      RelativeDimensionLE (baseChangeMap (D.system.map (homOfLE hi).op) X₀ Y₀ f₀) d

Tag 0EY2, a lemma

Tag 0EY2 in the Stacks Project.

AlgebraicGeometry.exists_relativeDimension_baseChange_of_relativeDimension_limitBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/RelativeDimension.lean, line 348.

In the situation of Tag 081D, if the base change of f₀ to the limit has relative dimension d and f₀ is locally of finite presentation, then the base change of f₀ to some later stage has relative dimension d.

theorem exists_relativeDimension_baseChange_of_relativeDimension_limitBaseChange
    (D : DescentSituation.{u, u} I)
    (X₀ Y₀ : Over (D.system.obj (op D.base))) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFinitePresentation f₀.left] (d : ℕ)
    (h : RelativeDimension (baseChangeMap (D.limitCone.π.app (op D.base)) X₀ Y₀ f₀) d) :
    ∃ (i : I) (hi : D.base ≤ i),
      RelativeDimension (baseChangeMap (D.system.map (homOfLE hi).op) X₀ Y₀ f₀) d

Tag 05M6, a lemma

Tag 05M6 in the Stacks Project.

AlgebraicGeometry.exists_finitePresentation_closedImmersion_of_forall_topologicalKrullDim_fiber_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/FibreDimensionEnlargement.lean, line 79.

Stacks Project, Tag 05M6. Let S be a quasi-compact and quasi-separated scheme, let f : X ⟶ S be a morphism of finite presentation and let d be a natural number. A closed subscheme Z ⊆ X, given by the closed immersion i, all of whose fibres over S have dimension at most d, is contained in a closed subscheme Z' ⊆ X, given by the closed immersion j, such that j is of finite presentation and all fibres of Z' over S still have dimension at most d.

theorem exists_finitePresentation_closedImmersion_of_forall_topologicalKrullDim_fiber_le
    {S X Z : Scheme.{u}} [CompactSpace S] [QuasiSeparatedSpace S]
    (f : X ⟶ S) (hf : FinitePresentation f) (i : Z ⟶ X) [IsClosedImmersion i] (d : ℕ)
    (hdim : ∀ s : S, topologicalKrullDim ((i ≫ f).fiber s) ≤ (d : WithBot ℕ∞)) :
    ∃ (Z' : Scheme.{u}) (j : Z' ⟶ X) (h : Z ⟶ Z'),
      IsClosedImmersion j ∧ IsClosedImmersion h ∧ i = h ≫ j ∧ FinitePresentation j ∧
        ∀ s : S, topologicalKrullDim ((j ≫ f).fiber s) ≤ (d : WithBot ℕ∞)

Sources

LeanAlgebraicGeometry.exists_forall_topologicalKrullDim_fiber_le_of_isLimit_of_essentiallySmall · AlgebraicGeometry.exists_quasiFinite_baseChange_of_quasiFinite_limitBaseChange · AlgebraicGeometry.exists_relativeDimensionLE_baseChange_of_limitBaseChange · AlgebraicGeometry.exists_relativeDimension_baseChange_of_relativeDimension_limitBaseChange · AlgebraicGeometry.exists_finitePresentation_closedImmersion_of_forall_topologicalKrullDim_fiber_le

Section32.19 Base change in top degree #

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

Tag 0EX3, a lemma

Tag 0EX3 in the Stacks Project.

Stacks.AlgebraicGeometry.TopDegreeBaseChange.affineTopDegreeTensorBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/AffineBaseChangeQuasicoherent.lean, line 203. The attribute's comment: “(c) for an affine base change over an affine base, at an arbitrary quasi-coherent module; the comparison is proved linear over the base ring and not over the base-changed ring, and no canonical base-change map is constructed”.

Conclusion (c) of [Stacks, Tag 0EX3] for an affine base change over an affine base, at an arbitrary quasi-coherent module: Hᵈ(X, F) ⊗_R B ≅ Hᵈ(X_B, q^* F).

Over an affine base the source obtains (c) from (b), and over an affine base (b) is the Eilenberg-Watts identity affineTopDegreeTensorCohomologyIso: M ↦ Hᵈ(X, F ⊗ p^* M~) is tensoring with Hᵈ(X, F). Reading it at M = B and composing with affineTopDegreeFunctorObjBaseRingIso gives the displayed identification, with no base-change morphism constructed and no invertibility to prove.

def affineTopDegreeTensorBaseChangeIso
    (F : (_root_.SheafOfModules.isQuasicoherent W.left.ringCatSheaf).FullSubcategory)
    (hvan : ∀ G : W.left.Modules, G.IsQuasicoherent →
      IsZero (((moduleGlobalSections W.left).rightDerivedPlus ((d : ℤ) + 1)).obj G))
    {B : CommRingCat.{u}} (φ : CommRingCat.of R ⟶ B) {ZB : Scheme.{u}}
    (q : ZB ⟶ W.left) (pB : ZB ⟶ Spec B)
    (sq : IsPullback pB q (Spec.map φ) W.hom) :
    (MonoidalCategory.tensorLeft
        ((ModuleCat.restrictScalars (algebraMap R Γ(W.left, ⊤))).obj
          ((qcohCohomology W.left d).obj F))).obj
        ((ModuleCat.restrictScalars φ.hom).obj (ModuleCat.of B B)) ≅
      (ModuleCat.restrictScalars (algebraMap R Γ(W.left, ⊤))).obj
        ((ModuleCat.restrictScalars q.appTop.hom).obj
          (((moduleGlobalSections ZB).rightDerived d).obj
            ((Scheme.Modules.pullback q).obj (show W.left.Modules from F.obj))))

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isIso_topDirectImageBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/BaseChangeTopDegreeConclusion.lean, line 68. The attribute's comment: “(c)”.

Conclusion (c) of [Stacks, Tag 0EX3]: formation of R^d f'_* 𝓕' commutes with arbitrary further base change. For a top-degree base-change situation S (a morphism f : X ⟶ Y of quasi-compact quasi-separated schemes whose higher direct images of quasi-coherent modules vanish above d, and a base change f' : X' ⟶ Y' of it), every further cartesian square X'' --h'--> X', X'' --f''--> Y'', Y'' --h--> Y' and every quasi-coherent 𝒪_{X'}-module 𝓕', the canonical map γ : h^* R^d f'_* 𝓕' ⟶ R^d f''_* (h')^* 𝓕' is an isomorphism.

theorem isIso_topDirectImageBaseChangeMap
    (S : Stacks.AlgebraicGeometry.TopDegreeBaseChangeSituation.{u})
    (F' : S.X'.Modules) [F'.IsQuasicoherent]
    (h' : X'' ⟶ S.X') (f'' : X'' ⟶ Y'') (h : Y'' ⟶ S.Y') (sq : IsPullback h' f'' S.f' h) :
    IsIso (topDirectImageBaseChangeMap S F' h' f'' h (toShHom_comm_of_isPullback h' f'' h sq))

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_rightDerivedPlus_pushforward_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/BaseChangeVanishing.lean, line 202. The attribute's comment: “(a)”.

Conclusion (a) of [Stacks, Tag 0EX3]. In a top-degree base-change situation the higher direct images along the base-changed morphism f' of a quasi-coherent module vanish above the degree d.

isZero_rightDerivedPlus_pushforward_of_affineCase reduces this to the case of a cartesian square whose two bases are affine, which it carried as the hypothesis haffine; that case is isZero_rightDerivedPlus_pushforward_baseChange_of_isAffine, so the conclusion is now unconditional.

The degree d of a situation is a natural number, so d < j makes j nonnegative and the integer-to-natural crossing the affine case asks for is available.

theorem isZero_rightDerivedPlus_pushforward_baseChange
    (S : Stacks.AlgebraicGeometry.TopDegreeBaseChangeSituation.{u})
    (i : ℤ) (hi : (S.d : ℤ) < i) (F' : S.X'.Modules) [F'.IsQuasicoherent] :
    IsZero (((Scheme.Modules.pushforward S.f').rightDerivedPlus i).obj F')

Stacks.AlgebraicGeometry.TopDegreeBaseChangeSituation.topDegreeTensorCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/EilenbergWattsUnitor.lean, line 269. The attribute's comment: “(b) over an affine base, as an isomorphism of functors”.

The affine case of [Stacks, Tag 0EX3] (b) in the source's own form. For a top-degree base-change situation whose base Y' is affine and a quasi-coherent module F on X', the endofunctor M ↦ H^d(X', F ⊗ (f')^* M~) of Γ(Y', ⊤)-modules is tensoring with H^d(X', F).

This strengthens topDegreeTensorIso, which names the module only as Φ(Γ(Y', ⊤)); the two are interchanged by topDegreeFunctorObjSelfIso.

def topDegreeTensorCohomologyIso :
    MonoidalCategory.tensorLeft (S.topDegreeCohomology F) ≅ S.topDegreeFunctor F

Stacks.AlgebraicGeometry.TopDegreeBaseChangeSituation.topDegreeTensorCohomologyLinearEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/EilenbergWattsUnitor.lean, line 279. The attribute's comment: “(b) over an affine base, the displayed tensor identity”.

The affine case of [Stacks, Tag 0EX3] (b), module by module, in the source's own form: a Γ(Y', ⊤)-linear equivalence H^d(X', F) ⊗_{R'} M ≃ₗ H^d(X', F ⊗ (f')^* M~), natural in M by topDegreeTensorCohomologyIso. This is the displayed equation of the source.

def topDegreeTensorCohomologyLinearEquiv (M : ModuleCat.{u} S.affineBaseRing) :
    (S.topDegreeCohomology F) ⊗[S.affineBaseRing] M ≃ₗ[S.affineBaseRing]
      (S.topDegreeFunctor F).obj M

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isIso_higherDirectImageTensorMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/TensorComparisonBase.lean, line 267. The attribute's comment: “(b)”.

Conclusion (b) of [Stacks, Tag 0EX3]. For a top-degree base-change situation, a quasi-coherent module F' on X' and a quasi-coherent module G on the base Y', the canonical map

R^d f'_* F' ⊗_{𝒪_{Y'}} G ⟶ R^d f'_*(F' ⊗_{𝒪_{X'}} (f')^* G)

is an isomorphism. The base carries no hypothesis: invertibility is local on it, the affine opens cover it, and over an affine open the Eilenberg-Watts argument of TensorComparisonAffineRigidity.lean applies to the restricted canonical map.

theorem isIso_higherDirectImageTensorMap (G : S.Y'.Modules) [G.IsQuasicoherent] :
    IsIso (higherDirectImageTensorMap S.f' F' G S.d)

Stacks.AlgebraicGeometry.TopDegreeBaseChange.topDirectImageTensorComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/TensorComparisonBase.lean, line 285. The attribute's comment: “(b)”.

Conclusion (b) of [Stacks, Tag 0EX3], as the isomorphism the tag asserts. For a top-degree base-change situation and quasi-coherent modules F' on X' and G on the base,

R^d f'_*(F' ⊗_{𝒪_{X'}} (f')^* G) ≅ R^d f'_* F' ⊗_{𝒪_{Y'}} G,

whose inverse satisfies the canonicity condition Stacks.AlgebraicGeometry.TopDegreeBaseChange.IsHigherDirectImageTensorMap of the tag, so by eq_of_isHigherDirectImageTensorMap it is the only candidate.

def topDirectImageTensorComparison (G : S.Y'.Modules) [G.IsQuasicoherent] :
    { e : ((Scheme.Modules.pushforward S.f').rightDerivedPlus (S.d : ℤ)).obj
        ((((Stacks.SheafOfModules.Tensor.sheafTensor
            ⟨S.X'.toRingedSpace.presheaf, S.X'.toRingedSpace.IsSheaf⟩).obj F').obj
              ((Scheme.Modules.pullback S.f').obj G))) ≅
      (((Stacks.SheafOfModules.Tensor.sheafTensor
          ⟨S.Y'.toRingedSpace.presheaf, S.Y'.toRingedSpace.IsSheaf⟩).obj
            (((Scheme.Modules.pushforward S.f').rightDerivedPlus (S.d : ℤ)).obj F')).obj G) //
      IsHigherDirectImageTensorMap S.f' F' G S.d e.inv }

Stacks.AlgebraicGeometry.TopDegreeBaseChangeSituation.topDegreeTensorSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/TopDegreeTensorProjection.lean, line 402. The attribute's comment: “(b)”.

Conclusion (b) of [Stacks, Tag 0EX3]. In a top-degree base-change situation, for F' quasi-coherent on X' and G' quasi-coherent on Y',

Rᵈ f'_*(F' ⊗_{𝒪_{X'}} (f')^* G') ≅ Rᵈ f'_* F' ⊗_{𝒪_{Y'}} G'.

No hypothesis is placed on Y': the base-changed morphism f' is quasi-compact and quasi-separated (quasiCompact_f', quasiSeparated_f') and its higher direct images vanish above d by conclusion (a), isZero_rightDerivedPlus_pushforward_baseChange, so this is Stacks.AlgebraicGeometry.TopDegreeBaseChange.topDegreeTensorIso for f'. Over an affine Y' the same conclusion is read on global sections by TopDegreeBaseChangeSituation.topDegreeTensorIso (EilenbergWattsSituation.lean).

def topDegreeTensorSheafIso
    (F' : SheafOfModules.{u} (structureSheafRing S.X'.toRingedSpace)) [F'.IsQuasicoherent]
    (G' : SheafOfModules.{u} (structureSheafRing S.Y'.toRingedSpace)) [G'.IsQuasicoherent] :
    (homologyFunctor (SheafOfModules.{u} (structureSheafRing S.Y'.toRingedSpace)) (S.d : ℤ)).obj
        ((derivedPushforward S.f'.toLRSHom.toShHom).obj
          ((singleFunctor (SheafOfModules.{u} (structureSheafRing S.X'.toRingedSpace)) 0).obj
            (((Stacks.SheafOfModules.Tensor.sheafTensor S.X'.toRingedSpace.sheaf).obj F').obj
              ((RingedSpaceModuleAdjunction.modulePullback S.f'.toLRSHom.toShHom).obj G')))) ≅
      ((Stacks.SheafOfModules.Tensor.sheafTensor S.Y'.toRingedSpace.sheaf).obj
        ((homologyFunctor (SheafOfModules.{u} (structureSheafRing S.Y'.toRingedSpace))
            (S.d : ℤ)).obj
          ((derivedPushforward S.f'.toLRSHom.toShHom).obj
            ((singleFunctor (SheafOfModules.{u} (structureSheafRing S.X'.toRingedSpace)) 0).obj
              F')))).obj
        G'

Tag 0E7D, a lemma

Tag 0E7D in the Stacks Project.

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_stalk_rightDerivedPlus_of_topologicalKrullDim_fiber_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/FibreDimensionStalkVanishing.lean, line 65. The attribute's comment: “part (1)”.

[Stacks, Tag 0E7D] part (1). For f : X ⟶ Y proper, y ∈ Y whose fibre has topological Krull dimension at most d, and F quasi-coherent, the stalk at y of Rⁱ f_* F vanishes for every i > d.

This is isZero_stalk_rightDerivedPlus_of_cohomology_vanishing with its hypothesis supplied by cohomology_vanishing_of_forall_topologicalKrullDim_fiber_le.

theorem isZero_stalk_rightDerivedPlus_of_topologicalKrullDim_fiber_le
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f] (y : Y) (d : ℕ)
    (hdim : topologicalKrullDim (f.fiber y) ≤ (d : WithBot ℕ∞))
    (F : X.Modules) [F.IsQuasicoherent] (i : ℤ) (hi : (d : ℤ) < i) :
    IsZero ((((Scheme.Modules.pushforward f).rightDerivedPlus i).obj F).presheaf.stalk y)

Stacks.AlgebraicGeometry.TopDegreeBaseChange.exists_isAffineOpen_topDegreeBaseChange_of_topologicalKrullDim_fiber_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/FibreDimensionStalkVanishing.lean, line 86. The attribute's comment: “part (2): the hypotheses of Tag 0EX3 and its conclusions (a) and (b)”.

[Stacks, Tag 0E7D] part (2). For f : X ⟶ Y proper and y ∈ Y whose fibre has topological Krull dimension at most d, the point y has an affine open neighbourhood V such that f ∣_ V : f ⁻¹ V ⟶ V and d satisfy

the hypotheses of [Stacks, Tag 0EX3]: f ⁻¹ V and V are quasi-compact and quasi-separated, and Rⁱ (f ∣_ V)_* F = 0 for i > d and every quasi-coherent F;

conclusion (a) of [Stacks, Tag 0EX3]: for every cartesian square X' ⟶ f ⁻¹ V, f' : X' ⟶ Y', Y' ⟶ V, Rⁱ f'_* F' = 0 for i > d and every quasi-coherent F' on X';

conclusion (b) of [Stacks, Tag 0EX3]: for every such square and quasi-coherent F' on X' and G' on Y', Rᵈ f'_*(F' ⊗ (f')^* G') ≅ Rᵈ f'_* F' ⊗ G', with Rᵈ f'_* read as the degree-d cohomology of the derived direct image of a module placed in degree 0.

theorem exists_isAffineOpen_topDegreeBaseChange_of_topologicalKrullDim_fiber_le
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f] (y : Y) (d : ℕ)
    (hdim : topologicalKrullDim (f.fiber y) ≤ (d : WithBot ℕ∞)) :
    ∃ V : Y.Opens,
      y ∈ V ∧ IsAffineOpen V ∧
      CompactSpace (f ⁻¹ᵁ V).toScheme ∧
      QuasiSeparatedSpace (f ⁻¹ᵁ V).toScheme ∧
      CompactSpace V.toScheme ∧ QuasiSeparatedSpace V.toScheme ∧
      (∀ (i : ℤ), (d : ℤ) < i →
        ∀ (F : (f ⁻¹ᵁ V).toScheme.Modules), F.IsQuasicoherent →
          IsZero (((Scheme.Modules.pushforward (f ∣_ V)).rightDerivedPlus i).obj F)) ∧
      (∀ {X' Y' : Scheme.{u}} (g' : X' ⟶ (f ⁻¹ᵁ V).toScheme) (f' : X' ⟶ Y')
          (g : Y' ⟶ V.toScheme), IsPullback g' f' (f ∣_ V) g →
        ∀ (i : ℤ), (d : ℤ) < i → ∀ (F' : X'.Modules), F'.IsQuasicoherent →
          IsZero (((Scheme.Modules.pushforward f').rightDerivedPlus i).obj F')) ∧
      (∀ {X' Y' : Scheme.{u}} (g' : X' ⟶ (f ⁻¹ᵁ V).toScheme) (f' : X' ⟶ Y')
          (g : Y' ⟶ V.toScheme), IsPullback g' f' (f ∣_ V) g →
        ∀ (F' : SheafOfModules.{u} (structureSheafRing X'.toRingedSpace)), F'.IsQuasicoherent →
        ∀ (G' : SheafOfModules.{u} (structureSheafRing Y'.toRingedSpace)), G'.IsQuasicoherent →
          Nonempty ((DerivedCategory.homologyFunctor
              (SheafOfModules.{u} (structureSheafRing Y'.toRingedSpace)) (d : ℤ)).obj
              ((derivedPushforward f'.toLRSHom.toShHom).obj
                ((DerivedCategory.singleFunctor
                  (SheafOfModules.{u} (structureSheafRing X'.toRingedSpace)) 0).obj
                  (((Stacks.SheafOfModules.Tensor.sheafTensor X'.toRingedSpace.sheaf).obj F').obj
                    ((RingedSpaceModuleAdjunction.modulePullback f'.toLRSHom.toShHom).obj
                      G')))) ≅
            ((Stacks.SheafOfModules.Tensor.sheafTensor Y'.toRingedSpace.sheaf).obj
              ((DerivedCategory.homologyFunctor
                (SheafOfModules.{u} (structureSheafRing Y'.toRingedSpace)) (d : ℤ)).obj
                ((derivedPushforward f'.toLRSHom.toShHom).obj
                  ((DerivedCategory.singleFunctor
                    (SheafOfModules.{u} (structureSheafRing X'.toRingedSpace)) 0).obj F')))).obj
              G'))

Stacks.AlgebraicGeometry.TopDegreeBaseChange.exists_isAffineOpen_topDegreeBaseChangeConclusions_of_topologicalKrullDim_fiber_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/FibreDimensionTopDegreeConclusions.lean, line 85. The attribute's comment: “part (2), with all conclusions of Tag 0EX3”.

[Stacks, Tag 0E7D] part (2), with every conclusion of Tag 0EX3. For f : X ⟶ Y proper and y ∈ Y whose fibre has topological Krull dimension at most d, the point y has an affine open neighbourhood V such that f ∣_ V : f ⁻¹ V ⟶ V and d satisfy the hypotheses of [Stacks, Tag 0EX3] (f ⁻¹ V and V quasi-compact and quasi-separated, Rⁱ (f ∣_ V)_* F = 0 for i > d and quasi-coherent F) and, for every cartesian square X' ⟶ f ⁻¹ V, f' : X' ⟶ Y', Y' ⟶ V, its conclusions:

(a) Rⁱ f'_* F' = 0 for i > d and every quasi-coherent F' on X';

(b) Rᵈ f'_*(F' ⊗ (f')^* G') ≅ Rᵈ f'_* F' ⊗ G' for quasi-coherent F' on X' and G' on Y';

(c) for every further cartesian square X'' ⟶ X', f'' : X'' ⟶ Y'', h : Y'' ⟶ Y' and every quasi-coherent F' on X', the canonical map h^* Rᵈ f'_* F' ⟶ Rᵈ f''_* (h')^* F' is an isomorphism.

theorem exists_isAffineOpen_topDegreeBaseChangeConclusions_of_topologicalKrullDim_fiber_le
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f] (y : Y) (d : ℕ)
    (hdim : topologicalKrullDim (f.fiber y) ≤ (d : WithBot ℕ∞)) :
    letI : ∀ (C : Type (u + 1)) [Category.{u} C] [Abelian C], HasDerivedCategory.{u + 1} C :=
      fun C _ _ => HasDerivedCategory.standard C
    ∃ (V : Y.Opens) (_ : y ∈ V) (_ : IsAffineOpen V)
      (hcX : CompactSpace (f ⁻¹ᵁ V).toScheme) (hqX : QuasiSeparatedSpace (f ⁻¹ᵁ V).toScheme)
      (hcY : CompactSpace V.toScheme) (hqY : QuasiSeparatedSpace V.toScheme)
      (hvan : ∀ (i : ℤ), (d : ℤ) < i →
        ∀ (F : (f ⁻¹ᵁ V).toScheme.Modules), F.IsQuasicoherent →
          IsZero (((Scheme.Modules.pushforward (f ∣_ V)).rightDerivedPlus i).obj F)),
      (∀ {X' Y' : Scheme.{u}} (g' : X' ⟶ (f ⁻¹ᵁ V).toScheme) (f' : X' ⟶ Y')
          (g : Y' ⟶ V.toScheme), IsPullback g' f' (f ∣_ V) g →
        ∀ (i : ℤ), (d : ℤ) < i → ∀ (F' : X'.Modules), F'.IsQuasicoherent →
          IsZero (((Scheme.Modules.pushforward f').rightDerivedPlus i).obj F')) ∧
      (∀ {X' Y' : Scheme.{u}} (g' : X' ⟶ (f ⁻¹ᵁ V).toScheme) (f' : X' ⟶ Y')
          (g : Y' ⟶ V.toScheme), IsPullback g' f' (f ∣_ V) g →
        ∀ (F' : SheafOfModules.{u} (structureSheafRing X'.toRingedSpace)), F'.IsQuasicoherent →
        ∀ (G' : SheafOfModules.{u} (structureSheafRing Y'.toRingedSpace)), G'.IsQuasicoherent →
          Nonempty ((DerivedCategory.homologyFunctor
              (SheafOfModules.{u} (structureSheafRing Y'.toRingedSpace)) (d : ℤ)).obj
              ((derivedPushforward f'.toLRSHom.toShHom).obj
                ((DerivedCategory.singleFunctor
                  (SheafOfModules.{u} (structureSheafRing X'.toRingedSpace)) 0).obj
                  (((Stacks.SheafOfModules.Tensor.sheafTensor X'.toRingedSpace.sheaf).obj F').obj
                    ((RingedSpaceModuleAdjunction.modulePullback f'.toLRSHom.toShHom).obj
                      G')))) ≅
            ((Stacks.SheafOfModules.Tensor.sheafTensor Y'.toRingedSpace.sheaf).obj
              ((DerivedCategory.homologyFunctor
                (SheafOfModules.{u} (structureSheafRing Y'.toRingedSpace)) (d : ℤ)).obj
                ((derivedPushforward f'.toLRSHom.toShHom).obj
                  ((DerivedCategory.singleFunctor
                    (SheafOfModules.{u} (structureSheafRing X'.toRingedSpace)) 0).obj F')))).obj
              G')) ∧
      (∀ {X' Y' : Scheme.{u}} (g' : X' ⟶ (f ⁻¹ᵁ V).toScheme) (f' : X' ⟶ Y')
          (g : Y' ⟶ V.toScheme) (sq : IsPullback g' f' (f ∣_ V) g),
        let S : Stacks.AlgebraicGeometry.TopDegreeBaseChangeSituation.{u} :=
          { X := (f ⁻¹ᵁ V).toScheme, Y := V.toScheme, f := f ∣_ V, d := d
            isCompact_X := hcX, isQuasiSeparated_X := hqX
            isCompact_Y := hcY, isQuasiSeparated_Y := hqY
            vanishes_above := hvan
            X' := X', Y' := Y', g' := g', f' := f', g := g, isPullback := sq }
        ∀ (F' : X'.Modules) [F'.IsQuasicoherent]
          {X'' Y'' : Scheme.{u}} (h' : X'' ⟶ X') (f'' : X'' ⟶ Y'') (h : Y'' ⟶ Y')
          (sq' : IsPullback h' f'' f' h),
        IsIso (topDirectImageBaseChangeMap S F' h' f'' h
          (toShHom_comm_of_isPullback (S := S) h' f'' h sq')))

Stacks.AlgebraicGeometry.TopDegreeBaseChange.stalkVanishing_and_topDegreeBaseChange_of_topologicalKrullDim_fiber_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/FibreDimensionTopDegreeConclusions.lean, line 144.

[Stacks, Tag 0E7D]. For f : X ⟶ Y proper and y ∈ Y whose fibre has topological Krull dimension at most d: (1) the stalk at y of Rⁱ f_* F vanishes for every i > d and every quasi-coherent F; (2) y has an affine open neighbourhood V such that f ∣_ V and d satisfy the hypotheses and all three conclusions of [Stacks, Tag 0EX3], as in exists_isAffineOpen_topDegreeBaseChangeConclusions_of_topologicalKrullDim_fiber_le.

theorem stalkVanishing_and_topDegreeBaseChange_of_topologicalKrullDim_fiber_le
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f] (y : Y) (d : ℕ)
    (hdim : topologicalKrullDim (f.fiber y) ≤ (d : WithBot ℕ∞)) :
    letI : ∀ (C : Type (u + 1)) [Category.{u} C] [Abelian C], HasDerivedCategory.{u + 1} C :=
      fun C _ _ => HasDerivedCategory.standard C
    (∀ (F : X.Modules), F.IsQuasicoherent → ∀ (i : ℤ), (d : ℤ) < i →
      IsZero ((((Scheme.Modules.pushforward f).rightDerivedPlus i).obj F).presheaf.stalk y)) ∧
    ∃ (V : Y.Opens) (_ : y ∈ V) (_ : IsAffineOpen V)
      (hcX : CompactSpace (f ⁻¹ᵁ V).toScheme) (hqX : QuasiSeparatedSpace (f ⁻¹ᵁ V).toScheme)
      (hcY : CompactSpace V.toScheme) (hqY : QuasiSeparatedSpace V.toScheme)
      (hvan : ∀ (i : ℤ), (d : ℤ) < i →
        ∀ (F : (f ⁻¹ᵁ V).toScheme.Modules), F.IsQuasicoherent →
          IsZero (((Scheme.Modules.pushforward (f ∣_ V)).rightDerivedPlus i).obj F)),
      (∀ {X' Y' : Scheme.{u}} (g' : X' ⟶ (f ⁻¹ᵁ V).toScheme) (f' : X' ⟶ Y')
          (g : Y' ⟶ V.toScheme), IsPullback g' f' (f ∣_ V) g →
        ∀ (i : ℤ), (d : ℤ) < i → ∀ (F' : X'.Modules), F'.IsQuasicoherent →
          IsZero (((Scheme.Modules.pushforward f').rightDerivedPlus i).obj F')) ∧
      (∀ {X' Y' : Scheme.{u}} (g' : X' ⟶ (f ⁻¹ᵁ V).toScheme) (f' : X' ⟶ Y')
          (g : Y' ⟶ V.toScheme), IsPullback g' f' (f ∣_ V) g →
        ∀ (F' : SheafOfModules.{u} (structureSheafRing X'.toRingedSpace)), F'.IsQuasicoherent →
        ∀ (G' : SheafOfModules.{u} (structureSheafRing Y'.toRingedSpace)), G'.IsQuasicoherent →
          Nonempty ((DerivedCategory.homologyFunctor
              (SheafOfModules.{u} (structureSheafRing Y'.toRingedSpace)) (d : ℤ)).obj
              ((derivedPushforward f'.toLRSHom.toShHom).obj
                ((DerivedCategory.singleFunctor
                  (SheafOfModules.{u} (structureSheafRing X'.toRingedSpace)) 0).obj
                  (((Stacks.SheafOfModules.Tensor.sheafTensor X'.toRingedSpace.sheaf).obj F').obj
                    ((RingedSpaceModuleAdjunction.modulePullback f'.toLRSHom.toShHom).obj
                      G')))) ≅
            ((Stacks.SheafOfModules.Tensor.sheafTensor Y'.toRingedSpace.sheaf).obj
              ((DerivedCategory.homologyFunctor
                (SheafOfModules.{u} (structureSheafRing Y'.toRingedSpace)) (d : ℤ)).obj
                ((derivedPushforward f'.toLRSHom.toShHom).obj
                  ((DerivedCategory.singleFunctor
                    (SheafOfModules.{u} (structureSheafRing X'.toRingedSpace)) 0).obj F')))).obj
              G')) ∧
      (∀ {X' Y' : Scheme.{u}} (g' : X' ⟶ (f ⁻¹ᵁ V).toScheme) (f' : X' ⟶ Y')
          (g : Y' ⟶ V.toScheme) (sq : IsPullback g' f' (f ∣_ V) g),
        let S : Stacks.AlgebraicGeometry.TopDegreeBaseChangeSituation.{u} :=
          { X := (f ⁻¹ᵁ V).toScheme, Y := V.toScheme, f := f ∣_ V, d := d
            isCompact_X := hcX, isQuasiSeparated_X := hqX
            isCompact_Y := hcY, isQuasiSeparated_Y := hqY
            vanishes_above := hvan
            X' := X', Y' := Y', g' := g', f' := f', g := g, isPullback := sq }
        ∀ (F' : X'.Modules) [F'.IsQuasicoherent]
          {X'' Y'' : Scheme.{u}} (h' : X'' ⟶ X') (f'' : X'' ⟶ Y'') (h : Y'' ⟶ Y')
          (sq' : IsPullback h' f'' f' h),
        IsIso (topDirectImageBaseChangeMap S F' h' f'' h
          (toShHom_comm_of_isPullback (S := S) h' f'' h sq')))

Stacks.AlgebraicGeometry.TopDegreeBaseChange.exists_isAffineOpen_vanishing_of_fiber_dimension_le_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/ZeroDimensionalFibres.lean, line 138. The attribute's comment: “part (2) for fibre dimension at most 0, with no further hypothesis”.

[Stacks, Tag 0E7D] part (2) for a proper morphism with zero-dimensional fibres, with no hypothesis beyond the tag's own. The point y has an affine open neighbourhood V such that f ∣_ V and 0 satisfy the hypotheses of [Stacks, Tag 0EX3] — the two finiteness conditions and the vanishing of the higher direct images above the degree — whose conclusions are then available unconditionally from StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/SituationBaseChange.lean.

This is exists_isAffineOpen_vanishing_of_cohomology_vanishing at d = 0, with its hypothesis hcoh discharged by cohomology_vanishing_of_forall_topologicalKrullDim_fiber_le_zero.

The part string records that the fibre bound is 0, not an arbitrary d.

theorem exists_isAffineOpen_vanishing_of_fiber_dimension_le_zero
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f] (y : Y)
    (hdim : topologicalKrullDim (f.fiber y) ≤ ((0 : ℕ) : WithBot ℕ∞)) :
    ∃ V : Y.Opens,
      y ∈ V ∧ IsAffineOpen V ∧
      CompactSpace (f ⁻¹ᵁ V).toScheme ∧
      QuasiSeparatedSpace (f ⁻¹ᵁ V).toScheme ∧
      CompactSpace V.toScheme ∧ QuasiSeparatedSpace V.toScheme ∧
      (∀ (i : ℤ), ((0 : ℕ) : ℤ) < i →
        ∀ (F : (f ⁻¹ᵁ V).toScheme.Modules), F.IsQuasicoherent →
          IsZero (((Scheme.Modules.pushforward (f ∣_ V)).rightDerivedPlus i).obj F))

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_stalk_rightDerivedPlus_of_fiber_dimension_le_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/ZeroDimensionalFibres.lean, line 162. The attribute's comment: “part (1) for fibre dimension at most 0, with no further hypothesis”.

[Stacks, Tag 0E7D] part (1) for a proper morphism with zero-dimensional fibres, with no hypothesis beyond the tag's own: the stalk at y of Rⁱ f_* F vanishes in every positive degree, for every quasi-coherent F.

This is isZero_stalk_rightDerivedPlus_of_cohomology_vanishing at d = 0, with its hypothesis hcoh discharged by cohomology_vanishing_of_forall_topologicalKrullDim_fiber_le_zero.

The part string records that the fibre bound is 0, not an arbitrary d.

theorem isZero_stalk_rightDerivedPlus_of_fiber_dimension_le_zero
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f] (y : Y)
    (hdim : topologicalKrullDim (f.fiber y) ≤ ((0 : ℕ) : WithBot ℕ∞))
    (F : X.Modules) [F.IsQuasicoherent] (i : ℤ) (hi : 0 < i) :
    IsZero ((((Scheme.Modules.pushforward f).rightDerivedPlus i).obj F).presheaf.stalk y)

Tag 0EX4, a lemma

Tag 0EX4 in the Stacks Project.

Stacks.AlgebraicGeometry.HigherDirectImageQcoh.isQuasicoherent_rightDerived_of_isProper, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HigherDirectImageQcqs/Qcqs.lean, line 505. The attribute's comment: “quasi-coherence”.

Stacks Project, Tag 0EX4 (quasi-coherence). Higher direct images of a quasi-coherent module under a proper morphism are quasi-coherent: a proper morphism is quasi-compact and quasi-separated, and properness is used for nothing else.

instance isQuasicoherent_rightDerived_of_isProper {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f]
    (F : X.Modules) [F.IsQuasicoherent] (i : ℕ) :
    (((Scheme.Modules.pushforward f).rightDerived i).obj F).IsQuasicoherent

Stacks.AlgebraicGeometry.Tag0EX4ProperQcoh.isQuasicoherent_rightDerived_of_isProper, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperQcoh/Basic.lean, line 90. The attribute's comment: “quasi-coherence”.

Stacks Project, Tag 0EX4 (quasi-coherence). Let f : X ⟶ Y be a proper morphism of schemes and let F be a quasi-coherent 𝒪_X-module. Then the higher direct image R ⁱ f_* F is a quasi-coherent 𝒪_Y-module, in every degree i : ℕ.

A proper morphism is quasi-compact and quasi-separated, so this is isQuasicoherent_rightDerived; properness is not otherwise used, and neither is any bound on the degree or on the dimension of the fibres.

instance isQuasicoherent_rightDerived_of_isProper [IsProper f] [F.IsQuasicoherent] :
    (((Scheme.Modules.pushforward f).rightDerived i).obj F).IsQuasicoherent

Stacks.AlgebraicGeometry.TopDegreeFiniteType.isFiniteType_rightDerived_of_isProper_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeFiniteType/NoetherianBaseUnconditional.lean, line 72. The attribute's comment: “finite-type clause only, and only over a locally Noetherian base; there in every degree and with no hypothesis on the fibres. An arbitrary base is not covered.”.

The finite-type clause of [Stacks, Tag 0EX4] over a locally Noetherian base. For f : X ⟶ Y proper with Y locally Noetherian and F quasi-coherent of finite type, the 𝒪_Y-module R ᵈ f_* F is of finite type in every degree d, with no bound on the fibres of f.

theorem isFiniteType_rightDerived_of_isProper_of_isLocallyNoetherian {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsProper f] [IsLocallyNoetherian Y] (F : X.Modules) [F.IsQuasicoherent]
    [F.IsFiniteType] (d : ℕ) :
    (((Scheme.Modules.pushforward f).rightDerived d).obj F).IsFiniteType

Stacks.AlgebraicGeometry.TopDegreeFiniteType.isQuasicoherent_isFiniteType_rightDerived_of_isProper_of_forall_topologicalKrullDim_fiber_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeFiniteType/Unconditional.lean, line 238. The attribute's comment: “both clauses at an ARBITRARY base, every d; the conclusion read as the 𝒪_Y-module R ᵈ f_* F, the source's 𝒪_X being a typo”.

[Stacks, Tag 0EX4]. For f : X ⟶ Y proper all of whose fibres have dimension at most d, and F a quasi-coherent 𝒪_X-module of finite type, the 𝒪_Y-module R ᵈ f_* F is quasi-coherent of finite type. The base is arbitrary.

The source prints the conclusion as an 𝒪_X-module; R ᵈ f_* F is a sheaf on Y, and the 𝒪_Y-reading is the one the source's own proof uses.

Both clauses of the tag in one statement: quasi-coherence is …ProperQcoh.isQuasicoherent_rightDerived_of_isProper, found by instance search because a proper morphism is quasi-compact and quasi-separated, and finite type is isFiniteType_rightDerived_of_isProper_of_forall_topologicalKrullDim_fiber_le.

theorem isQuasicoherent_isFiniteType_rightDerived_of_isProper_of_forall_topologicalKrullDim_fiber_le
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f] (d : ℕ)
    (hdim : ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ (d : WithBot ℕ∞))
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] :
    (((Scheme.Modules.pushforward f).rightDerived d).obj F).IsQuasicoherent ∧
      (((Scheme.Modules.pushforward f).rightDerived d).obj F).IsFiniteType

Tag 0EX5, a lemma

Tag 0EX5 in the Stacks Project.

Stacks.AlgebraicGeometry.TopDegreeFiniteType.isFinitePresentation_rightDerived_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeFiniteType/FinitePresentationModelDischarge.lean, line 220. The attribute's comment: “conclusion read as the 𝒪_Y-module R ᵈ f_* F, the source's 𝒪_X being a typo”. References: EGA III (2.4.1), “Clause (i), special case”.

[Stacks, Tag 0EX5]. Let f : X ⟶ Y be proper and of finite presentation with every fibre of dimension at most d, and let F be an 𝒪_X-module of finite presentation. Then the 𝒪_Y-module R ᵈ f_* F is of finite presentation.

No hypothesis is carried: Y is an arbitrary scheme, in particular not assumed locally Noetherian, and nothing about Noetherian models or about base change is assumed.

The proof is the source's, which is the proof of [Stacks, Tag 0EX4] with the third paragraph skipped, and it is now assembled from three pieces that are each unconditional:

the conclusion is local on Y, so Y may be taken affine, and over an affine base the situation descends to an affine Noetherian stage together with the fibre bound and the module, over which the higher direct images vanish above d — this is isFinitePresentation_rightDerived_of_topDegreeBaseChange above;

over that stage the top higher direct image of the base change is of finite presentation — …AffineBaseChangeProjection.isFinitePresentation_rightDerived_pullback_of_noetherianModel, the Eilenberg–Watts argument of [Stacks, Tag 0EX3] (b) applied at Γ(Y, ⊤).

The conclusion is read as the statement about the 𝒪_Y-module R ᵈ f_* F; the source prints 𝒪_X, which is a typo, the higher direct image being a sheaf on Y.

theorem isFinitePresentation_rightDerived_of_finitePresentation
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f] (hfp : AlgebraicGeometry.FinitePresentation f)
    (d : ℕ) (hdim : ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ (d : WithBot ℕ∞))
    (F : X.Modules) [F.IsFinitePresentation] :
    (((Scheme.Modules.pushforward f).rightDerived d).obj F).IsFinitePresentation

Sources

Section32.20 Glueing in closed fibres #

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

Tag 0BPA, a lemma

Tag 0BPA in the Stacks Project.

AlgebraicGeometry.GlueingNearPoint.restrictionFunctorAtPoint_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Germ.lean, line 4310.

Stacks Project, Tag 0BPA. Let s be a closed point of a scheme S whose open complement U = S \ {s} has quasi-compact inclusion. Restricting a scheme of finite presentation over S to U and to Spec 𝒪_{S, s}, together with the canonical comparison of the two induced restrictions to V = Spec 𝒪_{S, s} ∩ U, is an equivalence onto the category of such glueing data.

public theorem restrictionFunctorAtPoint_isEquivalence (S : Scheme.{u}) (s : S)
    (hs : IsClosed ({s} : Set S)) (hqc : QuasiCompact (puncturedOpen hs).ι) :
    (restrictionFunctorAtPoint S (puncturedOpen hs) s).IsEquivalence

Tag 0F21, a lemma

Tag 0F21 in the Stacks Project.

AlgebraicGeometry.GlueingNearPoint.moduleRestrictionFunctorAtPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/FinitePresentationModules.lean, line 365. The attribute's comment: “the canonical functor”.

Stacks 0F21, the canonical functor. A module of finite presentation on S goes to its restriction to U, its restriction to Spec 𝒪_{S, s}, and the canonical identification of the two restrictions to the punctured local scheme.

noncomputable def moduleRestrictionFunctorAtPoint (S : Scheme.{u}) (U : S.Opens) (s : S) :
    FinitePresentationModules S ⥤ moduleGlueingDataNearPoint S U s

AlgebraicGeometry.GlueingNearPoint.moduleGlueingEquivalenceNearClosedPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/FinitePresentationModules.lean, line 661.

Stacks 0F21. Let s be a closed point of a scheme S whose open complement U = S \ {s} has quasi-compact inclusion, and let V = Spec 𝒪_{S, s} ∖ {s}. Restricting a module of finite presentation on S to U and to Spec 𝒪_{S, s}, together with the canonical identification α of the two induced restrictions to V, is an equivalence onto the category of triples (𝒢, ℋ, α).

noncomputable def moduleGlueingEquivalenceNearClosedPoint (S : Scheme.{u}) (s : S)
    (hs : IsClosed ({s} : Set S)) (hqc : QuasiCompact (puncturedOpen hs).ι) :
    FinitePresentationModules S ≌ moduleGlueingDataNearPoint S (puncturedOpen hs) s

Tag 0BQ5, a lemma

Tag 0BQ5 in the Stacks Project.

AlgebraicGeometry.GlueingNearPoint.glueingEquivalenceNearPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Germ.lean, line 4045.

Stacks Project, Tag 0BQ5. Finite-presentation schemes on open neighbourhoods of a retrocompact open together with a point are equivalent, as a germ, to compatible finite-presentation schemes on the open and on the local scheme at the point. The natural identifications with base change intertwine the gluing comparison with the canonical iterated-pullback comparison on the overlap.

public noncomputable def glueingEquivalenceNearPoint
    (S : Scheme.{u}) (U : S.Opens) (s : S) (hs : s ∉ U)
    (hU : IsRetrocompact (U : Set S)) :
    { e : FinitePresentationGerm S U s ≌ glueingDataNearPoint S U s //
      ∃ a : (((FinitePresentationNeighborhoodModel.restrictionMorphisms
        (S := S) (U := U) (s := s)).Q ⋙ e.functor ⋙ openComponent S U s) ≅
        (neighborhoodModelToAmbient S U s ⋙ Over.pullback U.ι)),
      ∃ b : (((FinitePresentationNeighborhoodModel.restrictionMorphisms
        (S := S) (U := U) (s := s)).Q ⋙ e.functor ⋙ localComponent S U s) ≅
        (neighborhoodModelToAmbient S U s ⋙ Over.pullback (S.fromSpecStalk s))),
      overlapComparisonCompatible S U s e a b }

Tag 0EY3, a lemma

Tag 0EY3 in the Stacks Project.

AlgebraicGeometry.GlueingNearPoint.exists_open_isSeparated_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Properties.lean, line 348. The attribute's comment: “properties_of_relative_morphism”.

Let U ⊆ S be a retrocompact open, let s be a point of S outside U and let a be a morphism of schemes of finite presentation over an open neighbourhood U' of U ∪ {s}. If a is separated over U and over Spec 𝒪_{S, s}, then it is separated over some open neighbourhood of U ∪ {s} contained in U'.

theorem exists_open_isSeparated_baseChange
    (S : Scheme.{u}) (U U' : S.Opens) (s : S) (_hsU : s ∉ U) (hsU' : s ∈ U')
    (_hU : IsRetrocompact (U : Set S)) (hUU' : U ≤ U')
    (X₁ X₂ : Over U'.toScheme) (a : X₁ ⟶ X₂)
    (hX₁ : FinitePresentation X₁.hom) (hX₂ : FinitePresentation X₂.hom)
    (hsepU : IsSeparated (baseChangeMap U.ι ((Over.map U'.ι).obj X₁)
      ((Over.map U'.ι).obj X₂) ((Over.map U'.ι).map a)))
    (hsepS : IsSeparated (baseChangeMap (S.fromSpecStalk s) ((Over.map U'.ι).obj X₁)
      ((Over.map U'.ι).obj X₂) ((Over.map U'.ι).map a))) :
    ∃ V : S.Opens, U ≤ V ∧ V ≤ U' ∧ s ∈ V ∧
      IsSeparated (baseChangeMap V.ι ((Over.map U'.ι).obj X₁)
        ((Over.map U'.ι).obj X₂) ((Over.map U'.ι).map a))

AlgebraicGeometry.GlueingNearPoint.exists_open_isProper_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Properties.lean, line 371. The attribute's comment: “properties_of_relative_morphism”. References: EGA IV (8.1.2), “partial”.

Let U ⊆ S be a retrocompact open, let s be a point of S outside U and let a be a morphism of schemes of finite presentation over an open neighbourhood U' of U ∪ {s}. If a is proper over U and over Spec 𝒪_{S, s}, then it is proper over some open neighbourhood of U ∪ {s} contained in U'.

theorem exists_open_isProper_baseChange
    (S : Scheme.{u}) (U U' : S.Opens) (s : S) (_hsU : s ∉ U) (hsU' : s ∈ U')
    (_hU : IsRetrocompact (U : Set S)) (hUU' : U ≤ U')
    (X₁ X₂ : Over U'.toScheme) (a : X₁ ⟶ X₂)
    (hX₁ : FinitePresentation X₁.hom) (hX₂ : FinitePresentation X₂.hom)
    (hproperU : IsProper (baseChangeMap U.ι ((Over.map U'.ι).obj X₁)
      ((Over.map U'.ι).obj X₂) ((Over.map U'.ι).map a)))
    (hproperS : IsProper (baseChangeMap (S.fromSpecStalk s) ((Over.map U'.ι).obj X₁)
      ((Over.map U'.ι).obj X₂) ((Over.map U'.ι).map a))) :
    ∃ V : S.Opens, U ≤ V ∧ V ≤ U' ∧ s ∈ V ∧
      IsProper (baseChangeMap V.ι ((Over.map U'.ι).obj X₁)
        ((Over.map U'.ι).obj X₂) ((Over.map U'.ι).map a))

AlgebraicGeometry.GlueingNearPoint.exists_open_isFinite_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Properties.lean, line 394. The attribute's comment: “properties_of_relative_morphism”.

Let U ⊆ S be a retrocompact open, let s be a point of S outside U and let a be a morphism of schemes of finite presentation over an open neighbourhood U' of U ∪ {s}. If a is finite over U and over Spec 𝒪_{S, s}, then it is finite over some open neighbourhood of U ∪ {s} contained in U'.

theorem exists_open_isFinite_baseChange
    (S : Scheme.{u}) (U U' : S.Opens) (s : S) (_hsU : s ∉ U) (hsU' : s ∈ U')
    (_hU : IsRetrocompact (U : Set S)) (hUU' : U ≤ U')
    (X₁ X₂ : Over U'.toScheme) (a : X₁ ⟶ X₂)
    (hX₁ : FinitePresentation X₁.hom) (hX₂ : FinitePresentation X₂.hom)
    (hfiniteU : IsFinite (baseChangeMap U.ι ((Over.map U'.ι).obj X₁)
      ((Over.map U'.ι).obj X₂) ((Over.map U'.ι).map a)))
    (hfiniteS : IsFinite (baseChangeMap (S.fromSpecStalk s) ((Over.map U'.ι).obj X₁)
      ((Over.map U'.ι).obj X₂) ((Over.map U'.ι).map a))) :
    ∃ V : S.Opens, U ≤ V ∧ V ≤ U' ∧ s ∈ V ∧
      IsFinite (baseChangeMap V.ι ((Over.map U'.ι).obj X₁)
        ((Over.map U'.ι).obj X₂) ((Over.map U'.ι).map a))

AlgebraicGeometry.GlueingNearPoint.exists_open_etale_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Properties.lean, line 419. The attribute's comment: “properties_of_relative_morphism”.

Let U ⊆ S be a retrocompact open, let s be a point of S outside U and let a be a morphism of schemes of finite presentation over an open neighbourhood U' of U ∪ {s}. If a is étale over U and over Spec 𝒪_{S, s}, then it is étale over some open neighbourhood of U ∪ {s} contained in U'.

theorem exists_open_etale_baseChange
    (S : Scheme.{u}) (U U' : S.Opens) (s : S) (_hsU : s ∉ U) (hsU' : s ∈ U')
    (_hU : IsRetrocompact (U : Set S)) (hUU' : U ≤ U')
    (X₁ X₂ : Over U'.toScheme) (a : X₁ ⟶ X₂)
    (hX₁ : FinitePresentation X₁.hom) (hX₂ : FinitePresentation X₂.hom)
    (hetaleU : Etale (baseChangeMap U.ι ((Over.map U'.ι).obj X₁)
      ((Over.map U'.ι).obj X₂) ((Over.map U'.ι).map a)))
    (hetaleS : Etale (baseChangeMap (S.fromSpecStalk s) ((Over.map U'.ι).obj X₁)
      ((Over.map U'.ι).obj X₂) ((Over.map U'.ι).map a))) :
    ∃ V : S.Opens, U ≤ V ∧ V ≤ U' ∧ s ∈ V ∧
      Etale (baseChangeMap V.ι ((Over.map U'.ι).obj X₁)
        ((Over.map U'.ι).obj X₂) ((Over.map U'.ι).map a))

AlgebraicGeometry.GlueingNearPoint.exists_open_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Properties.lean, line 482. The attribute's comment: “properties_of_glued_morphism”.

A scheme of finite presentation over an open neighbourhood of U ∪ {s} whose restrictions to the retrocompact open U and to the local scheme Spec 𝒪_{S, s} are separated is separated over some smaller open neighbourhood of U ∪ {s}.

theorem exists_open_isSeparated
    (S : Scheme.{u}) (U : S.Opens) (s : S) (hs : s ∉ U)
    (hU : IsRetrocompact (U : Set S))
    (X : FinitePresentationNeighborhoodModel S U s)
    (hopen : IsSeparated ((Over.pullback U.ι).obj
      ((neighborhoodModelToAmbient S U s).obj X)).hom)
    (hlocal : IsSeparated ((Over.pullback (S.fromSpecStalk s)).obj
      ((neighborhoodModelToAmbient S U s).obj X)).hom) :
    ∃ V : S.Opens, U ≤ V ∧ V ≤ X.neighborhood.V ∧ s ∈ V ∧
      IsSeparated ((Over.pullback V.ι).obj
        ((neighborhoodModelToAmbient S U s).obj X)).hom

AlgebraicGeometry.GlueingNearPoint.exists_open_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Properties.lean, line 503. The attribute's comment: “properties_of_glued_morphism”.

A scheme of finite presentation over an open neighbourhood of U ∪ {s} whose restrictions to the retrocompact open U and to the local scheme Spec 𝒪_{S, s} are proper is proper over some smaller open neighbourhood of U ∪ {s}.

theorem exists_open_isProper
    (S : Scheme.{u}) (U : S.Opens) (s : S) (hs : s ∉ U)
    (hU : IsRetrocompact (U : Set S))
    (X : FinitePresentationNeighborhoodModel S U s)
    (hopen : IsProper ((Over.pullback U.ι).obj
      ((neighborhoodModelToAmbient S U s).obj X)).hom)
    (hlocal : IsProper ((Over.pullback (S.fromSpecStalk s)).obj
      ((neighborhoodModelToAmbient S U s).obj X)).hom) :
    ∃ V : S.Opens, U ≤ V ∧ V ≤ X.neighborhood.V ∧ s ∈ V ∧
      IsProper ((Over.pullback V.ι).obj
        ((neighborhoodModelToAmbient S U s).obj X)).hom

AlgebraicGeometry.GlueingNearPoint.exists_open_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Properties.lean, line 524. The attribute's comment: “properties_of_glued_morphism”.

A scheme of finite presentation over an open neighbourhood of U ∪ {s} whose restrictions to the retrocompact open U and to the local scheme Spec 𝒪_{S, s} are finite is finite over some smaller open neighbourhood of U ∪ {s}.

theorem exists_open_isFinite
    (S : Scheme.{u}) (U : S.Opens) (s : S) (hs : s ∉ U)
    (hU : IsRetrocompact (U : Set S))
    (X : FinitePresentationNeighborhoodModel S U s)
    (hopen : IsFinite ((Over.pullback U.ι).obj
      ((neighborhoodModelToAmbient S U s).obj X)).hom)
    (hlocal : IsFinite ((Over.pullback (S.fromSpecStalk s)).obj
      ((neighborhoodModelToAmbient S U s).obj X)).hom) :
    ∃ V : S.Opens, U ≤ V ∧ V ≤ X.neighborhood.V ∧ s ∈ V ∧
      IsFinite ((Over.pullback V.ι).obj
        ((neighborhoodModelToAmbient S U s).obj X)).hom

AlgebraicGeometry.GlueingNearPoint.exists_open_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Properties.lean, line 547. The attribute's comment: “properties_of_glued_morphism”.

A scheme of finite presentation over an open neighbourhood of U ∪ {s} whose restrictions to the retrocompact open U and to the local scheme Spec 𝒪_{S, s} are étale is étale over some smaller open neighbourhood of U ∪ {s}.

theorem exists_open_etale
    (S : Scheme.{u}) (U : S.Opens) (s : S) (hs : s ∉ U)
    (hU : IsRetrocompact (U : Set S))
    (X : FinitePresentationNeighborhoodModel S U s)
    (hopen : Etale ((Over.pullback U.ι).obj
      ((neighborhoodModelToAmbient S U s).obj X)).hom)
    (hlocal : Etale ((Over.pullback (S.fromSpecStalk s)).obj
      ((neighborhoodModelToAmbient S U s).obj X)).hom) :
    ∃ V : S.Opens, U ≤ V ∧ V ≤ X.neighborhood.V ∧ s ∈ V ∧
      Etale ((Over.pullback V.ι).obj
        ((neighborhoodModelToAmbient S U s).obj X)).hom

Tag 0E8Q, a lemma

Tag 0E8Q in the Stacks Project.

AlgebraicGeometry.canonicalRestrictionFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Basic.lean, line 131. The attribute's comment: “canonical functor”.

Stacks Project, Tag 0E8Q, the canonical functor. The functor taking a scheme of finite presentation over S to the gluing datum given by its restriction to the complement of the closed points, its restrictions to the local schemes at them, and the base-change associativity isomorphism between the two restrictions to each punctured local scheme.

The comparison is AlgebraicGeometry.canonicalRestrictionComparison, which is pinned by its compatibility equation, so this is the canonical functor and not merely a functor into the category of gluing data.

noncomputable def canonicalRestrictionFunctor :
    FinitePresentationOver S ⥤ glueingData s hs

AlgebraicGeometry.canonicalRestrictionFunctor_isEquivalence_of_isEmpty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Equivalence.lean, line 115. The attribute's comment: “equivalence, special case of an empty family of points”.

For an empty family of points, the canonical restriction functor from schemes of finite presentation over S to gluing data is an equivalence of categories.

theorem canonicalRestrictionFunctor_isEquivalence_of_isEmpty [IsEmpty I] :
    (canonicalRestrictionFunctor s hs).IsEquivalence

AlgebraicGeometry.canonicalRestrictionFunctor_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/EquivalenceGeneral.lean, line 153. The attribute's comment: “equivalence, general finite family of points”.

Stacks Project, Tag 0E8Q. Let s : I → S be a finite family of pairwise distinct closed points of a scheme S whose open complement has quasi-compact inclusion. Then the canonical restriction functor from schemes of finite presentation over S to glueing data near the family — a scheme of finite presentation over the open complement, a family of schemes of finite presentation over the local schemes at the points, and an isomorphism of the two restrictions to each punctured local scheme — is an equivalence of categories.

theorem canonicalRestrictionFunctor_isEquivalence {S : Scheme.{u}} {I : Type u} [Finite I]
    (s : I → S) (hs : ∀ i, s i ∈ closedPoints S) (hinj : Function.Injective s)
    (hqc : QuasiCompact (complementOfClosedPoints s hs).ι) :
    (canonicalRestrictionFunctor s hs).IsEquivalence

AlgebraicGeometry.canonicalRestrictionFunctor_isEquivalence_of_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/EquivalenceSinglePoint.lean, line 164. The attribute's comment: “equivalence, special case of a one-element family of points”.

Stacks Project, Tag 0E8Q, for a family of closed points indexed by a type with a unique element: the canonical restriction functor from schemes of finite presentation over S to gluing data near the family is an equivalence of categories.

The family is a single closed point whose open complement has quasi-compact inclusion, so this is [Stacks, Tag 0BPA] after evaluating the one-index gluing data at its unique index.

theorem canonicalRestrictionFunctor_isEquivalence_of_unique [Unique I]
    (hqc : QuasiCompact (complementOfClosedPoints s hs).ι) :
    (canonicalRestrictionFunctor s hs).IsEquivalence

AlgebraicGeometry.canonicalRestrictionComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RestrictionComparison/Basic.lean, line 219. The attribute's comment: “canonical comparison”.

Stacks Project, Tag 0E8Q, the canonical comparison. The base-change associativity isomorphism identifying the two ways of restricting a scheme of finite presentation over S to every punctured local scheme, together with the equation saying that it commutes with the projections down to the scheme being restricted.

noncomputable def canonicalRestrictionComparison {S : Scheme.{u}} {I : Type u} [Finite I]
    (s : I → S) (hs : ∀ i, s i ∈ closedPoints S) :
    { e : restrictToComplementOfClosedPoints s hs ⋙ restrictOpenToPuncturedLocals s hs ≅
        restrictToLocalSchemes s ⋙ restrictLocalsToPuncturedLocals s hs //
      ∀ (X : FinitePresentationOver S) (i : I),
        ((e.hom.app X) i).hom.left ≫
          pullback.fst
            (pullback.snd X.obj.hom (S.fromSpecStalk (s i)))
            (((S.fromSpecStalk (s i)) ⁻¹ᵁ (complementOfClosedPoints s hs)).ι) ≫
          pullback.fst X.obj.hom (S.fromSpecStalk (s i)) =
        pullback.fst
            (pullback.snd X.obj.hom (complementOfClosedPoints s hs).ι)
            ((S.fromSpecStalk (s i)) ∣_ (complementOfClosedPoints s hs)) ≫
          pullback.fst X.obj.hom (complementOfClosedPoints s hs).ι }

Sources

Section32.21 Application to modifications #

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

Tag 0B3X, a lemma

Tag 0B3X in the Stacks Project.

AlgebraicGeometry.GlueingNearPoint.finitePresentationAwayBaseChange_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GlueingNearClosedPoints/Modifications.lean, line 308.

Stacks Project, Tag 0B3X. Let s be a closed point of a scheme S whose open complement U = S ∖ {s} has quasi-compact inclusion. Base change along Spec 𝒪_{S, s} ⟶ S is an equivalence from the category of finitely presented morphisms to S which are isomorphisms over U onto the category of finitely presented morphisms to Spec 𝒪_{S, s} which are isomorphisms over the punctured spectrum.

theorem finitePresentationAwayBaseChange_isEquivalence (S : Scheme.{u}) (s : S)
    (hs : IsClosed ({s} : Set S)) (hqc : QuasiCompact (puncturedOpen hs).ι) :
    (finitePresentationAwayBaseChange S s hs).IsEquivalence

Tag 0BFN, a lemma

Tag 0BFN in the Stacks Project.

AlgebraicGeometry.GlueingNearPoint.isSeparated_iff_isSeparated_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ModificationProperties.lean, line 131. The attribute's comment: “separated”.

Stacks Project, Tag 0BFN (separated case). A morphism of finite presentation to S which is an isomorphism over the complement of a closed point s is separated exactly when its base change along Spec 𝒪_{S, s} ⟶ S is separated.

theorem isSeparated_iff_isSeparated_baseChange (S : Scheme.{u}) (s : S)
    (hs : IsClosed ({s} : Set S)) (hqc : QuasiCompact (puncturedOpen hs).ι)
    (X : FinitePresentationAway (puncturedOpen hs)) :
    IsSeparated X.obj.hom ↔
      IsSeparated ((finitePresentationAwayBaseChange S s hs).obj X).obj.hom

AlgebraicGeometry.GlueingNearPoint.isProper_iff_isProper_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ModificationProperties.lean, line 144. The attribute's comment: “proper”.

Stacks Project, Tag 0BFN (proper case). A morphism of finite presentation to S which is an isomorphism over the complement of a closed point s is proper exactly when its base change along Spec 𝒪_{S, s} ⟶ S is proper.

theorem isProper_iff_isProper_baseChange (S : Scheme.{u}) (s : S)
    (hs : IsClosed ({s} : Set S)) (hqc : QuasiCompact (puncturedOpen hs).ι)
    (X : FinitePresentationAway (puncturedOpen hs)) :
    IsProper X.obj.hom ↔
      IsProper ((finitePresentationAwayBaseChange S s hs).obj X).obj.hom

AlgebraicGeometry.GlueingNearPoint.isFinite_iff_isFinite_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ModificationProperties.lean, line 157. The attribute's comment: “finite”.

Stacks Project, Tag 0BFN (finite case). A morphism of finite presentation to S which is an isomorphism over the complement of a closed point s is finite exactly when its base change along Spec 𝒪_{S, s} ⟶ S is finite.

theorem isFinite_iff_isFinite_baseChange (S : Scheme.{u}) (s : S)
    (hs : IsClosed ({s} : Set S)) (hqc : QuasiCompact (puncturedOpen hs).ι)
    (X : FinitePresentationAway (puncturedOpen hs)) :
    IsFinite X.obj.hom ↔
      IsFinite ((finitePresentationAwayBaseChange S s hs).obj X).obj.hom

AlgebraicGeometry.GlueingNearPoint.etale_iff_etale_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ModificationProperties.lean, line 170. The attribute's comment: “etale”.

Stacks Project, Tag 0BFN (étale case). A morphism of finite presentation to S which is an isomorphism over the complement of a closed point s is étale exactly when its base change along Spec 𝒪_{S, s} ⟶ S is étale.

theorem etale_iff_etale_baseChange (S : Scheme.{u}) (s : S)
    (hs : IsClosed ({s} : Set S)) (hqc : QuasiCompact (puncturedOpen hs).ι)
    (X : FinitePresentationAway (puncturedOpen hs)) :
    Etale X.obj.hom ↔
      Etale ((finitePresentationAwayBaseChange S s hs).obj X).obj.hom

Sources

LeanAlgebraicGeometry.GlueingNearPoint.finitePresentationAwayBaseChange_isEquivalence · AlgebraicGeometry.GlueingNearPoint.isSeparated_iff_isSeparated_baseChange · AlgebraicGeometry.GlueingNearPoint.isProper_iff_isProper_baseChange · AlgebraicGeometry.GlueingNearPoint.isFinite_iff_isFinite_baseChange · AlgebraicGeometry.GlueingNearPoint.etale_iff_etale_baseChange

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

32.2 Directed limits of schemes… to 32.21 Application to…

Section32.2 Directed limits of schemes with affine transition maps#

Tag 01YV, the section

Tag 01YW, a lemma

Tag 01YX, a lemma

Tag 01YZ, a lemma

Sources

Section32.3 Infinite products#

Tag 0CNI, a lemma

Tag 0CNJ, a lemma

Tag 0CNK, a lemma

Sources

Section32.4 Descending properties#

Tag 0CUE, a lemma

Tag 0CUF, a lemma

Tag 0CUG, a lemma

Tag 086P, a situation

Tag 01YY, a lemma

Tag 01Z0, a lemma

Tag 05F3, a lemma

Tag 05F4, a lemma

Tag 01Z4, a lemma

Tag 01Z6, a lemma

Tag 086Q, a lemma

Tag 09MT, a lemma

Tag 081B, a lemma

Tag 01ZH, a lemma

Tag 09ZM, a lemma

Tag 09ZN, a lemma

Tag 0A0N, a lemma

Tag 0GIH, a lemma

Sources

Section32.5 Absolute Noetherian Approximation#

Tag 01Z7, a lemma

Tag 01Z9, a lemma

Tag 07RN, a lemma

Tag 01ZA, a proposition

Sources

Section32.6 Limits and morphisms of finite presentation#

Tag 01ZC, a proposition

Tag 05LX, a remark

Tag 0CM0, a lemma

Tag 0GWT, a lemma

Sources

Section32.7 Relative approximation#

Tag 0GS1, a lemma

Tag 09MV, a lemma

Tag 09YZ, a lemma

Sources

Section32.8 Descending properties of morphisms#

Tag 081D, a situation

Tag 01ZN, a lemma

Tag 01ZO, a lemma

Tag 0C4W, a lemma

Tag 01ZP, a lemma

Tag 01ZQ, a lemma

Tag 04AI, a lemma

Tag 06AC, a lemma

Tag 0C0C, a lemma

Tag 07RP, a lemma

Tag 081E, a lemma

Tag 0EUU, a lemma

Tag 0GTB, a lemma

Tag 07RQ, a lemma

Tag 07RR, a lemma

Tag 0C3L, a lemma

Sources

Section32.9 Finite type closed in finite presentation#

Tag 01ZE, a lemma

Tag 01ZG, a lemma

Tag 09ZP, a lemma

Tag 09ZQ, a lemma

Tag 01ZJ, a proposition

Tag 01ZK, a lemma

Tag 09YY, a lemma

Sources

Section32.10 Descending relative objects#

Tag 01ZM, a lemma

Tag 01ZR, a lemma

Tag 0B8W, a lemma

Section32.2 Directed limits of schemes with affine transition maps #

Section32.3 Infinite products #

Section32.4 Descending properties #

Section32.5 Absolute Noetherian Approximation #

Section32.6 Limits and morphisms of finite presentation #

Section32.7 Relative approximation #

Section32.8 Descending properties of morphisms #

Section32.9 Finite type closed in finite presentation #

Section32.10 Descending relative objects #

Section32.11 Characterizing affine schemes #

Section32.12 Variants of Chow's Lemma #

Section32.13 Applications of Chow's lemma #

Section32.14 Universally closed morphisms #

Section32.15 Noetherian valuative criterion #

Section32.16 Refined Noetherian valuative criteria #

Section32.17 Valuative criteria over a Nagata base #

Section32.18 Limits and dimensions of fibres #

Section32.19 Base change in top degree #

Section32.20 Glueing in closed fibres #

Section32.21 Application to modifications #