70.15 Characterizing affine… to 70.23 Descending finite type…

Section70.15 Characterizing affine spaces#

Section 70.15 of the Stacks Project, Tag 07VQ. 5 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07VS, a lemma

Tag 07VS in the Stacks Project.

AlgebraicGeometry.Space.isAffineSpace_of_isSurjective_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineOfUniversallyClosedSurjection.lean, line 235. The attribute's comment: “granted h07VR, the conclusion of Stacks 07VR that a finite morphism over a quasi-compact quasi-separated algebraic space is a directed limit of finite morphisms of finite presentation; h07SQ, the conclusion of Stacks 07SQ that a directed system with affine transition morphisms whose limit is affine has an affine stage; and hFinitePresentation, the strict special case of this statement in which the morphism is also of finite presentation — the third paragraph of the source proof, which runs through Stacks 07SU, 07SK, 084Z, 07SN and 07VP. The first two conclude about inverse systems and the third adds a hypothesis, so none is the universally quantified form of this conclusion”.

Stacks 07VS. Let f : X ⟶ Y be a surjective finite morphism of algebraic spaces over S. If X is affine, then so is Y.

A finite morphism is affine and universally closed by Stacks 0414 and Stacks 0415, so the target is separated by Stacks 05Z2 and quasi-compact by Stacks 040W. Writing f as a directed limit of finite morphisms of finite presentation, a late stage is affine and is surjective onto Y, which reduces the claim to the case of a morphism of finite presentation.

theorem isAffineSpace_of_isSurjective_of_isFinite (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hsurj : IsSurjective B S hS f) (hfin : IsFinite B S hS f)
    (haff : IsAffineSpace B S hS X)
    (h07VR : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsFinite B S hS g →
      IsQuasiCompactSpace B S hS Y' →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y' →
      IntegralFiniteSystem B S hS g)
    (h07SQ : ∀ {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)]
      (D : DescentSituation B S hS B.contains_terminal I),
      IsAffineSpace B S hS D.limitCone.pt →
      ∃ i : I, D.base ≤ i ∧ IsAffineSpace B S hS (D.system.obj (Opposite.op i)))
    (hFinitePresentation : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsFinite B S hS g →
      IsFinitePresentation B S hS g → IsSurjective B S hS g → IsAffineSpace B S hS X' →
      IsAffineSpace B S hS Y') :
    IsAffineSpace B S hS Y

Declarations registered for the tag:

• AlgebraicGeometry.Space.isAffineSpace_target_of_isFinite_of_isSurjective, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/AffineFiniteSurjectionTags.lean, line 31 (StacksFrontier).

Tag 07VT, a proposition

Tag 07VT in the Stacks Project.

AlgebraicGeometry.Space.isAffineSpace_of_isSurjective_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineOfUniversallyClosedSurjection.lean, line 275. The attribute's comment: “granted h09YA, the conclusion of Stacks 09YA that an integral morphism over a quasi-compact quasi-separated algebraic space is a directed limit of finite morphisms of finite presentation; h07SQ, the conclusion of Stacks 07SQ that a directed system with affine transition morphisms whose limit is affine has an affine stage; and hFinitePresentation, the strict special case of this statement in which the morphism is also finite and of finite presentation — the third paragraph of the proof of Stacks 07VS, which runs through Stacks 07SU, 07SK, 084Z, 07SN and 07VP. The first two conclude about inverse systems and the third adds two hypotheses, so none is the universally quantified form of this conclusion”.

Stacks 07VT. Let f : X ⟶ Y be a surjective universally closed morphism of algebraic spaces over S. If X is affine, then so is Y.

The target is separated by Stacks 05Z2 and quasi-compact by Stacks 040W, so f is affine by Stacks 08GB and hence integral by Stacks 0415. Writing f as a directed limit of finite morphisms of finite presentation, a late stage is affine and is surjective onto Y, which reduces the claim to the case of a morphism which is finite and of finite presentation.

theorem isAffineSpace_of_isSurjective_of_universallyClosed (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hsurj : IsSurjective B S hS f) (hclosed : UniversallyClosed B S hS f)
    (haff : IsAffineSpace B S hS X)
    (h09YA : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsIntegralHom B S hS g →
      IsQuasiCompactSpace B S hS Y' →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y' →
      IntegralFiniteSystem B S hS g)
    (h07SQ : ∀ {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)]
      (D : DescentSituation B S hS B.contains_terminal I),
      IsAffineSpace B S hS D.limitCone.pt →
      ∃ i : I, D.base ≤ i ∧ IsAffineSpace B S hS (D.system.obj (Opposite.op i)))
    (hFinitePresentation : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsFinite B S hS g →
      IsFinitePresentation B S hS g → IsSurjective B S hS g → IsAffineSpace B S hS X' →
      IsAffineSpace B S hS Y') :
    IsAffineSpace B S hS Y

Declarations registered for the tag:

• AlgebraicGeometry.Space.isAffineSpace_of_isSurjective_of_universallyClosed_of_isAffineSpace, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/AffineFiniteSurjectionTags.lean, line 33 (StacksFrontier).

Tag 07VU, a lemma

Tag 07VU in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_isRepresentable_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeOfIntegralBijection.lean, line 337. The attribute's comment: “granted the three hypotheses of Stacks 07VT: h09YA, the conclusion of Stacks 09YA that an integral morphism over a quasi-compact quasi-separated algebraic space is a directed limit of finite morphisms of finite presentation; h07SQ, the conclusion of Stacks 07SQ that a directed system with affine transition morphisms whose limit is affine has an affine stage; and hFinitePresentation, the case of Stacks 07VT in which the morphism is finite and of finite presentation. None is the universally quantified form of this conclusion: the first two conclude about inverse systems and the third about affineness of a target”.

Stacks 07VU, due to Conrad–Lieblich–Olsson 3.1.12. If the reduction of an algebraic space over S is a scheme, then the space itself is a scheme.

The inclusion of AlgebraicGeometry.Space.reduction is a closed immersion, hence integral by Stacks 081Y, it is injective on points because it is a monomorphism, and it is surjective on points by AlgebraicGeometry.Space.surjective_pointsMap_ι_reduction; Stacks 07VV applies.

theorem isRepresentable_of_isRepresentable_reduction {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hred : (reduction B S hS X hX).toFunctor.IsRepresentable)
    (h09YA : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsIntegralHom B S hS g →
      IsQuasiCompactSpace B S hS Y' →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y' →
      IntegralFiniteSystem B S hS g)
    (h07SQ : ∀ {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)]
      (D : DescentSituation B S hS B.contains_terminal I),
      IsAffineSpace B S hS D.limitCone.pt →
      ∃ i : I, D.base ≤ i ∧ IsAffineSpace B S hS (D.system.obj (Opposite.op i)))
    (hFinitePresentation : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsFinite B S hS g →
      IsFinitePresentation B S hS g → IsSurjective B S hS g → IsAffineSpace B S hS X' →
      IsAffineSpace B S hS Y') :
    X.IsRepresentable

Declarations registered for the tag:

• AlgebraicGeometry.IsAlgebraicSpace.isRepresentable_of_isRepresentable_reduction, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/ThickeningSchemeRepresentableClosedImmersion.lean, line 117 (StacksFrontier).

Tag 07VV, a lemma

Tag 07VV in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeOfIntegralBijection.lean, line 158. The attribute's comment: “the implication from the target, with no bijectivity hypothesis”.

Stacks 07VV, the implication from the target. If the target of an integral morphism of algebraic spaces over S is a scheme, then so is its source. Bijectivity on points is not needed.

An integral morphism is representable, so the base change of the morphism along an affine open of the target is an affine open subspace of the source; the affine opens of the target cover it, so every point of the source lies in a representable open subspace, hence in the schematic locus of Stacks 03JH.

theorem isRepresentable_of_isIntegralHom (hF : IsAlgebraicSpace B S hS F) (f : F ⟶ G)
    (hf : IsIntegralHom B S hS f) (hGrep : G.IsRepresentable) :
    F.IsRepresentable

AlgebraicGeometry.Space.isRepresentable_of_isIntegralHom_of_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeOfIntegralBijection.lean, line 194. The attribute's comment: “the implication from the source, granted the three hypotheses of Stacks 07VT: h09YA, the conclusion of Stacks 09YA that an integral morphism over a quasi-compact quasi-separated algebraic space is a directed limit of finite morphisms of finite presentation; h07SQ, the conclusion of Stacks 07SQ that a directed system with affine transition morphisms whose limit is affine has an affine stage; and hFinitePresentation, the case of Stacks 07VT in which the morphism is finite and of finite presentation. None is the universally quantified form of this conclusion: the first two conclude about inverse systems and the third about affineness of a target”.

Stacks 07VV, the implication from the source. If the source of an integral morphism of algebraic spaces over S which is bijective on points is a scheme, then so is its target.

Let α : h_V ⟶ X be an affine open of the source through a given point. The morphism is universally closed by Stacks 0415, hence closed on points, so the image of |V| is open and cuts out an open subspace W of the target by part (1) of Tag 03BZ. Bijectivity identifies the point set of X ×_Y W with |V|, so the two open subspaces of X agree and X ×_Y W is affine; its projection to W is integral and surjective, so W is affine by Stacks 07VT and the given point lies in the schematic locus of Stacks 03JH.

theorem isRepresentable_of_isIntegralHom_of_bijective (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (hf : IsIntegralHom B S hS f)
    (hbij : Function.Bijective (pointsMap B S hS F f)) (hFrep : F.IsRepresentable)
    (h09YA : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsIntegralHom B S hS g →
      IsQuasiCompactSpace B S hS Y' →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y' →
      IntegralFiniteSystem B S hS g)
    (h07SQ : ∀ {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)]
      (D : DescentSituation B S hS B.contains_terminal I),
      IsAffineSpace B S hS D.limitCone.pt →
      ∃ i : I, D.base ≤ i ∧ IsAffineSpace B S hS (D.system.obj (Opposite.op i)))
    (hFinitePresentation : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsFinite B S hS g →
      IsFinitePresentation B S hS g → IsSurjective B S hS g → IsAffineSpace B S hS X' →
      IsAffineSpace B S hS Y') :
    G.IsRepresentable

AlgebraicGeometry.Space.isRepresentable_iff_of_isIntegralHom_of_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeOfIntegralBijection.lean, line 301. The attribute's comment: “granted the three hypotheses of Stacks 07VT: h09YA, the conclusion of Stacks 09YA that an integral morphism over a quasi-compact quasi-separated algebraic space is a directed limit of finite morphisms of finite presentation; h07SQ, the conclusion of Stacks 07SQ that a directed system with affine transition morphisms whose limit is affine has an affine stage; and hFinitePresentation, the case of Stacks 07VT in which the morphism is finite and of finite presentation. None is the universally quantified form of this conclusion: the first two conclude about inverse systems and the third about affineness of a target”.

Stacks 07VV. Let f : X ⟶ Y be an integral morphism of algebraic spaces over S which induces a bijection |X| → |Y| on points. Then X is a scheme if and only if Y is a scheme.

The two implications are AlgebraicGeometry.Space.isRepresentable_of_isIntegralHom_of_bijective and AlgebraicGeometry.Space.isRepresentable_of_isIntegralHom; only the first uses bijectivity, and only the first uses the three hypotheses of Stacks 07VT.

theorem isRepresentable_iff_of_isIntegralHom_of_bijective (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (hf : IsIntegralHom B S hS f)
    (hbij : Function.Bijective (pointsMap B S hS F f))
    (h09YA : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsIntegralHom B S hS g →
      IsQuasiCompactSpace B S hS Y' →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y' →
      IntegralFiniteSystem B S hS g)
    (h07SQ : ∀ {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)]
      (D : DescentSituation B S hS B.contains_terminal I),
      IsAffineSpace B S hS D.limitCone.pt →
      ∃ i : I, D.base ≤ i ∧ IsAffineSpace B S hS (D.system.obj (Opposite.op i)))
    (hFinitePresentation : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsFinite B S hS g →
      IsFinitePresentation B S hS g → IsSurjective B S hS g → IsAffineSpace B S hS X' →
      IsAffineSpace B S hS Y') :
    F.IsRepresentable ↔ G.IsRepresentable

AlgebraicGeometry.Space.isRepresentable_iff_isRepresentable_of_isIntegralHom_of_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeOfIntegralBijectionUnconditional.lean, line 68.

Stacks 07VV. Let S be a scheme and let f : X ⟶ Y be a morphism of algebraic spaces over S. Assume f is integral and induces a bijection |X| → |Y|. Then X is a scheme if and only if Y is a scheme.

The implication from the source is AlgebraicGeometry.Space.isRepresentable_target_of_isIntegralHom_of_bijective, through Stacks 07VT, and the implication from the target is AlgebraicGeometry.Space.isRepresentable_of_isIntegralHom, which needs no bijectivity.

theorem isRepresentable_iff_isRepresentable_of_isIntegralHom_of_bijective
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G)
    (hf : IsIntegralHom B S hS f) (hbij : Function.Bijective (pointsMap B S hS F f)) :
    F.IsRepresentable ↔ G.IsRepresentable

Tag 08B2, a lemma

Tag 08B2 in the Stacks Project.

AlgebraicGeometry.Space.isClosedImmersion_of_infinitesimal_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionInfinitesimal.lean, line 183. The attribute's comment: “granted the three hypotheses of Stacks 07VT, carried unchanged from Stacks 07VV: h09YA, h07SQ and hFinitePresentation. None is the universally quantified form of this conclusion, which is about closed immersions”.

Stacks 08B2. Let f : X ⟶ Y and i : Y' ⟶ Y be morphisms of algebraic spaces over S. If i is a closed immersion, bijective on points, if the base change of f along i is a closed immersion, and if either f is of finite type or i is of finite presentation, then f is a closed immersion.

theorem isClosedImmersion_of_infinitesimal_baseChange
    {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (i : Y' ⟶ Y) (hi : IsClosedImmersion B S hS i)
    (hbij : Function.Bijective (pointsMap B S hS Y' i))
    (hbc : IsClosedImmersion B S hS (pullback.snd f i))
    (hfin : IsFiniteType B S hS f ∨ IsFinitePresentation B S hS i)
    (h09YA : ∀ {Z Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : Z ⟶ Z'),
      IsAlgebraicSpace B S hS Z → IsAlgebraicSpace B S hS Z' → IsIntegralHom B S hS g →
      IsQuasiCompactSpace B S hS Z' →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Z' →
      IntegralFiniteSystem B S hS g)
    (h07SQ : ∀ {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)]
      (D : DescentSituation B S hS B.contains_terminal I),
      IsAffineSpace B S hS D.limitCone.pt →
      ∃ i : I, D.base ≤ i ∧ IsAffineSpace B S hS (D.system.obj (Opposite.op i)))
    (hFinitePresentation : ∀ {Z Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : Z ⟶ Z'),
      IsAlgebraicSpace B S hS Z → IsAlgebraicSpace B S hS Z' → IsFinite B S hS g →
      IsFinitePresentation B S hS g → IsSurjective B S hS g → IsAffineSpace B S hS Z →
      IsAffineSpace B S hS Z') :
    IsClosedImmersion B S hS f

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

Stacks 08B2. Let f : X ⟶ Y and i : Y' ⟶ Y be morphisms of algebraic spaces over S. If i is a closed immersion, bijective on points, if the base change of f along i is a closed immersion, and if either f is of finite type or i is of finite presentation, then f is a closed immersion.

theorem isClosedImmersion_of_isClosedImmersion_pullback_snd_of_bijective
    {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (i : Y' ⟶ Y) (hi : IsClosedImmersion B S hS i)
    (hbij : Function.Bijective (pointsMap B S hS Y' i))
    (hbc : IsClosedImmersion B S hS (pullback.snd f i))
    (hfin : IsFiniteType B S hS f ∨ IsFinitePresentation B S hS i) :
    IsClosedImmersion B S hS f

Sources

• Section 70.15, Tag 07VQ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isAffineSpace_of_isSurjective_of_isFinite · AlgebraicGeometry.Space.isAffineSpace_target_of_isFinite_of_isSurjective · AlgebraicGeometry.Space.isAffineSpace_of_isSurjective_of_universallyClosed · AlgebraicGeometry.Space.isAffineSpace_of_isSurjective_of_universallyClosed_of_isAffineSpace · AlgebraicGeometry.Space.isRepresentable_of_isRepresentable_reduction · AlgebraicGeometry.IsAlgebraicSpace.isRepresentable_of_isRepresentable_reduction · AlgebraicGeometry.Space.isRepresentable_of_isIntegralHom · AlgebraicGeometry.Space.isRepresentable_of_isIntegralHom_of_bijective

Section70.16 Finite cover by a scheme#

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

Tag 09YC, a proposition

Tag 09YC in the Stacks Project.

AlgebraicGeometry.Space.existsFiniteSurjectiveSchemeCover_and_refining, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFpSchemeCoverExistence.lean, line 97.

Stacks Project, Tag 09YC. Let X be a quasi-compact and quasi-separated algebraic space over a scheme S. Then

1. there is a surjective finite morphism of finite presentation to X from the presheaf represented by an object of the big fppf site — a scheme over S — and
2. given a surjective étale morphism p : U ⟶ X from an algebraic space, such a cover can be chosen so that it factors through p on a representable open subspace neighbourhood of every one of its points.

Clause (1) is a finite surjective scheme cover refined through an affine étale chart by Stacks 0CP0 and embedded in a finite cover of finite presentation; clause (2) is clause (1) refined by Stacks 0CP0.

theorem existsFiniteSurjectiveSchemeCover_and_refining
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (hXqc : IsQuasiCompactSpace B S hS X)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X) :
    (∃ (Y : BigFppfOver B S hS) (f : yoneda.obj Y ⟶ X),
        IsSurjective B S hS f ∧ IsFinite B S hS f ∧ IsFinitePresentation B S hS f) ∧
      ∀ (U : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS U →
        ∀ p : U ⟶ X, IsSurjective B S hS p → IsEtale B S hS p →
          ∃ (Y : BigFppfOver B S hS) (f : yoneda.obj Y ⟶ X),
            IsSurjective B S hS f ∧ IsFinite B S hS f ∧ IsFinitePresentation B S hS f ∧
              FactorsZariskiLocallyThrough B S hS p Y f

Tag 0GUM, a lemma

Tag 0GUM in the Stacks Project.

AlgebraicGeometry.Space.exists_isLimit_finite_finitePresentation_fixedOnOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/IntegralLimitFinitePresentationFixedOnOpen.lean, line 83.

An integral morphism f : X ⟶ Y of algebraic spaces over S, with Y quasi-compact and quasi-separated, which is finite and of finite presentation over a quasi-compact open subspace V of Y (that is, f⁻¹(V) = X ×_Y V ⟶ V is), is the limit of a directed inverse system, indexed by a nonempty directed preorder in the universe of the schemes, of algebraic spaces D i with morphisms t i : D i ⟶ Y finite and of finite presentation, the limiting cone p having vertex X and lying over Y; and for every i the square formed by X ×_Y V ⟶ X ⟶ D i, X ×_Y V ⟶ V, t i and V ⟶ Y is cartesian, that is f⁻¹(V) ⟶ f_i⁻¹(V) is an isomorphism.

theorem exists_isLimit_finite_finitePresentation_fixedOnOpen
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsIntegralHom B S hS f)
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y)
    (V : Subfunctor Y) (hV : IsOpenSubspace B S hS V)
    (hVqc : IsQuasiCompactSpace B S hS V.toFunctor)
    (hfVfinite : IsFinite B S hS (pullback.snd f V.ι))
    (hfVfp : IsFinitePresentation B S hS (pullback.snd f V.ι)) :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirectedOrder I)
      (D : Iᵒᵖ ⥤ ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
      (p : (Functor.const Iᵒᵖ).obj X ⟶ D) (t : D ⟶ (Functor.const Iᵒᵖ).obj Y),
      (∀ i, IsAlgebraicSpace B S hS (D.obj i)) ∧
      (∀ i, IsFinite B S hS (t.app i)) ∧
      (∀ i, IsFinitePresentation B S hS (t.app i)) ∧
      (p ≫ t = (Functor.const Iᵒᵖ).map f) ∧
      Nonempty (IsLimit (Cone.mk X p)) ∧
      (∀ i, IsPullback (pullback.fst f V.ι ≫ p.app i) (pullback.snd f V.ι) (t.app i) V.ι)

Tag 0GUN, a lemma

Tag 0GUN in the Stacks Project.

AlgebraicGeometry.Space.exists_finiteSchemeCover_finiteEtaleOverDenseOpen_and_refining, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteSchemeCoverExistence.lean, line 156.

Stacks Project, Tag 0GUN. Let X be a quasi-compact and quasi-separated algebraic space over a scheme S such that |X| has finitely many irreducible components. Then

1. there is a surjective, finite and finitely presented morphism f : h_Y ⟶ X from the presheaf represented by an object Y of the big fppf site — a scheme over S — and a quasi-compact open subspace U ⊆ X with dense point set over which f is finite étale, and
2. given a surjective étale morphism p : V ⟶ X from an algebraic space, such a cover can be chosen so that it factors through p on a representable open subspace neighbourhood of every one of its points.

Clause (2) for p is reduced to an affine chart h_A ⟶ V, where it is AlgebraicGeometry.Space.exists_finiteSchemeCover_refining_of_isAffine; clause (1) is clause (2) at the identity of X.

theorem exists_finiteSchemeCover_finiteEtaleOverDenseOpen_and_refining
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (hXqc : IsQuasiCompactSpace B S hS X) (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X)
    (hcomp : (irreducibleComponents (points B S hS X)).Finite) :
    (∃ (Y : BigFppfOver B S hS) (f : yoneda.obj Y ⟶ X) (U : Subfunctor X),
      IsFiniteSchemeCoverFiniteEtaleOverDenseOpen B S hS Y f U) ∧
    ∀ (V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS V →
      ∀ p : V ⟶ X, IsSurjective B S hS p → IsEtale B S hS p →
        ∃ (Y : BigFppfOver B S hS) (f : yoneda.obj Y ⟶ X) (U : Subfunctor X),
          IsFiniteSchemeCoverFiniteEtaleOverDenseOpen B S hS Y f U ∧
            FactorsZariskiLocallyThrough B S hS p Y f

Tag 0GUP, a lemma

Tag 0GUP in the Stacks Project.

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

Stacks 0GUP. Let X be a quasi-compact and quasi-separated algebraic space. There are t ≥ 0 and closed subspaces X ⊇ Z₀ ⊇ Z₁ ⊇ ⋯ ⊇ Z_t = ∅ with each Z_i ⟶ X of finite presentation and Z₀ ⊆ X a thickening, such that for each i < t there is a scheme Y_i and a surjective, finite and finitely presented morphism Y_i ⟶ Z_i which is finite étale over the open subspace Z_i ∖ Z_{i+1} (AlgebraicGeometry.Space.IsFiniteEtaleCoverStep).

theorem exists_finiteEtaleCoverStratification (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (hXqc : IsQuasiCompactSpace B S hS X) (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X) :
    ∃ (t : ℕ) (Z : ℕ → Subfunctor X),
      (∀ i, IsClosedSubspace B S hS (Z i)) ∧ (∀ i, IsFinitePresentation B S hS (Z i).ι) ∧
      (∀ i, Z (i + 1) ≤ Z i) ∧ IsThickening B S hS ⟨X, hX⟩ (Z 0) ∧
      IsEmpty (points B S hS (Z t).toFunctor) ∧
      ∀ i < t, IsFiniteEtaleCoverStep B S hS (Z i) (Z (i + 1))

Sources

• Section 70.16, Tag 0ACX
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.existsFiniteSurjectiveSchemeCover_and_refining · AlgebraicGeometry.Space.exists_isLimit_finite_finitePresentation_fixedOnOpen · AlgebraicGeometry.Space.exists_finiteSchemeCover_finiteEtaleOverDenseOpen_and_refining · AlgebraicGeometry.Space.exists_finiteEtaleCoverStratification

Section70.17 Obtaining schemes#

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

Tag 0B7Y, a lemma

Tag 0B7Y in the Stacks Project.

AlgebraicGeometry.Space.exists_isClosedSubspace_minimal_not_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MinimalNonSchematicClosedSubspaceExistence.lean, line 209.

Stacks 0B7Y. Let X be a quasi-compact and quasi-separated algebraic space over S which is not a scheme. Then there is a closed subspace Z of X which is not a scheme but every closed subspace of Z other than Z itself — every proper closed subspace of Z — is a scheme.

This is the source's proof, by Zorn's lemma applied to the closed subspaces of X which are not schemes, ordered by inclusion: ⊤ is one of them, and the infimum of a chain of them is one of them because it is the inverse limit of the chain, which is AlgebraicGeometry.Space.not_isRepresentable_sInf_of_isChain. A minimal one is the required Z, and minimality becomes the inner clause by pushing a proper closed subspace of Z forward to a closed subspace of X contained in Z.

Nothing is assumed beyond the tag's own hypotheses. In particular no condition is imposed on the size of the chain and none on the site's size cutoff: the chain step is discharged by AlgebraicGeometry.Space.DescentSituation.exists_isRepresentable_system_obj_of_isSiteSmall, the library's Stacks 07SR, whose smallness hypothesis is met through AlgebraicGeometry.Space.IsSiteSmall.of_mono because the transition morphisms of the chain are closed immersions, hence monomorphisms.

theorem exists_isClosedSubspace_minimal_not_isRepresentable (hT : B.Contains (⊤_ Scheme.{u}))
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hqc : IsQuasiCompactSpace B S hS X)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hT X)
    (hXnotScheme : ¬ X.IsRepresentable) :
    ∃ Z : Subfunctor X, IsClosedSubspace B S hS Z ∧ ¬ Z.toFunctor.IsRepresentable ∧
      ∀ Z' : Subfunctor Z.toFunctor, IsClosedSubspace B S hS Z' → Z' ≠ ⊤ →
        Z'.toFunctor.IsRepresentable

Tag 0B7Z, a lemma

Tag 0B7Z in the Stacks Project.

AlgebraicGeometry.Space.hasEtaleLocalProperty_isReduced_and_irreducibleSpace_of_forall_ne_top_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MinimalNonSchematicSpaceReducedIrreducible.lean, line 233.

Stacks 0B7Z. Let X be an algebraic space over S which is not a scheme, and assume that every closed subspace Z of X with Z ≠ ⊤ — that is, every proper closed subspace of X — is a scheme. Then X is reduced and |X| is irreducible.

A closed subspace with every point of X cannot be a scheme, by the closed-immersion form of Stacks 07VU. Applied to the reduction of X this makes the reduction the whole of X, which is therefore reduced. Applied to the scheme-theoretic union of the reduced induced subspaces on two proper closed subsets covering |X|, which is a scheme by Stacks 0CZ1 and Stacks 0EDP, it shows that no such cover exists; and |X| is nonempty since a space without points is a scheme.

The source also assumes X quasi-compact and quasi-separated; the proof does not use either assumption, so they are omitted.

theorem hasEtaleLocalProperty_isReduced_and_irreducibleSpace_of_forall_ne_top_isRepresentable
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hproper : ∀ Z : Subfunctor X, IsClosedSubspace B S hS Z → Z ≠ ⊤ →
      Z.toFunctor.IsRepresentable)
    (hXnotScheme : ¬ X.IsRepresentable) :
    HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} => IsReduced Y) ∧
      IrreducibleSpace (points B S hS X)

Tag 0B80, a lemma

Tag 0B80 in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_isRepresentable_baseChange_specStalkSiteObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/LocalRingSchemeCriterion.lean, line 510.

Stacks 0B80. Let X be an algebraic space over a scheme S whose structure morphism f is quasi-compact and quasi-separated. If for every point of X, with image s in S, the base change X ×_S Spec(𝒪_{S, s}) is a scheme, then X is a scheme.

This is the same statement as AlgebraicGeometry.Space.isRepresentable_of_isRepresentable_baseChange_specStalk with the object of the site no longer quantified over: Spec(𝒪_{S, s}) is an object of the big fppf site of S whenever S is, by AlgebraicGeometry.BigFppfSite.contains_spec_stalk_of_contains, so the base change of the tag is formed inside the site with nothing assumed.

Nothing is assumed beyond the tag's own hypotheses: no condition on the size of the system of affine open neighbourhoods of s and none on the site's size cutoff. See the module documentation for how Stacks 07SR is met.

theorem isRepresentable_of_isRepresentable_baseChange_specStalkSiteObject
    (hX : IsAlgebraicSpace B S hS X) (hqc : IsQuasiCompact B S hS f)
    (hqs : IsQuasiSeparated B S hS f)
    (hloc : ∀ p : FieldValuedPoint B S hS X,
      ((baseChangeSiteFunctor f).obj (specStalkSiteObject B S hS
        (p.toBase (IsLocalRing.closedPoint p.carrier)))).IsRepresentable) :
    X.IsRepresentable

Tag 0B81, a lemma

Tag 0B81 in the Stacks Project.

AlgebraicGeometry.Space.exists_maximal_not_isRepresentable_quotientSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MaximalNonSchematicQuotient.lean, line 805.

Stacks 0B81. Let φ : X ⟶ Spec A be a quasi-compact and quasi-separated morphism from an algebraic space to an affine scheme. If X is not a scheme then there is an ideal I ⊂ A such that the base change X_{A/I} is not a scheme while X_{A/I'} is a scheme for every ideal I' with I ⊊ I'.

By Zorn's lemma applied to the set of ideals I with X_{A/I} not a scheme. It contains (0) because X_{A/0} ≅ X, and the supremum of a chain of such ideals is again one of them because X_{A/⨆ K} is the limit of the X_{A/K i} (AlgebraicGeometry.Space.quotientDescentSituation), so Stacks 07SR makes one member of the chain a scheme. A maximal element is the required ideal.

Nothing is assumed beyond the tag's own hypotheses, and in particular no bound on the chain and no condition on the site's size cutoff. Stacks 07SR is AlgebraicGeometry.Space.DescentSituation.exists_isRepresentable_system_obj_of_isSiteSmall, whose smallness hypothesis is met by AlgebraicGeometry.Space.IsSiteSmall.of_mono: the transition morphisms of this system are closed immersions, by AlgebraicGeometry.Space.isClosedImmersion_quotientSpaceDiagram_map, because A/K i ↠ A/K j is surjective, hence monomorphisms, and for such a system nothing is asked of the index.

theorem exists_maximal_not_isRepresentable_quotientSpace
    (hX : IsAlgebraicSpace B (Spec (.of A)) hA X)
    (hqc : IsQuasiCompact B (Spec (.of A)) hA φ)
    (hqs : IsQuasiSeparated B (Spec (.of A)) hA φ)
    (hnot : ¬ X.IsRepresentable) :
    ∃ I : Ideal A, ¬ (quotientSpace A B hA φ I).IsRepresentable ∧
      ∀ I' : Ideal A, I < I' → (quotientSpace A B hA φ I').IsRepresentable

Sources

• Section 70.17, Tag 0B7X
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.exists_isClosedSubspace_minimal_not_isRepresentable · AlgebraicGeometry.Space.hasEtaleLocalProperty_isReduced_and_irreducibleSpace_of_forall_ne_top_isRepresentable · AlgebraicGeometry.Space.isRepresentable_of_isRepresentable_baseChange_specStalkSiteObject · AlgebraicGeometry.Space.exists_maximal_not_isRepresentable_quotientSpace

Section70.18 Glueing in closed fibres#

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

Tag 0E8Z, a lemma

Tag 0E8Z in the Stacks Project.

AlgebraicGeometry.isAlgebraicSpace_iff_forall_isAlgebraicSpace_relocalizeRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlgebraicityOnBaseCover.lean, line 141. The attribute's comment: “algebraicity is detected on an open covering of the base”.

Stacks 0E8Z, the algebraicity criterion. Let {jᵢ : Tᵢ ⟶ S} be a finite family of open immersions of a big fppf site whose images cover S. An fppf sheaf on the big fppf site of S is an algebraic space over S exactly when its restriction along each jᵢ is an algebraic space over Tᵢ.

theorem isAlgebraicSpace_iff_forall_isAlgebraicSpace_relocalizeRestrict [Finite I]
    (hj : ∀ i, IsOpenImmersion (B.inclusion.map (j i)))
    (hcov : ∀ x : S, ∃ i, x ∈ Set.range (B.inclusion.map (j i)))
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F) :
    IsAlgebraicSpace B S hS F ↔
      ∀ i, IsAlgebraicSpace B (T i) (hT i) ((OverShriek.relocalizeRestrict (j i)).obj F)

AlgebraicGeometry.FinitePresentationSpacesOver.isEquivalence_glueingFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentationSliceGlueing.lean, line 64. The attribute's comment: “the equivalence clause: for an open covering of the base, base change is an equivalence onto the 2-fibre product of the categories of finite-presentation algebraic spaces over the two members. The criterion clause, that algebraicity is detected on such a covering, is AlgebraicGeometry.isAlgebraicSpace_iff_forall_isAlgebraicSpace_relocalizeRestrict in StacksFrontier.AlgebraicGeometry.Spaces.AlgebraicityOnBaseCover, which this module imports, so the two clauses cannot live in one file”.

The algebraic spaces of finite presentation over a base covered by two opens U and W with intersection V are the 2-fibre product FP_U ×_{FP_V} FP_W. The comparison functor taking a space to its two restrictions together with their canonical identification over V is an equivalence: it is faithful and full by the sheaf condition at the Mayer--Vietoris squares of the covering, and essentially surjective because the space glued from a datum restricts back to it.

theorem isEquivalence_glueingFunctor : (glueingFunctor B S hS hV.w).IsEquivalence

Tag 0E90, a lemma

Tag 0E90 in the Stacks Project.

AlgebraicGeometry.FinitePresentationSpacesOver.isEquivalence_glueingFunctor_of_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationClosedFibreGlueing.lean, line 909. The attribute's comment: “the equivalence, granted the two colimit identifications. The theorem is stated for an arbitrary object M of the site equipped with a cofiltered system of open neighbourhoods W i of the point complementary to U, and an object N over their intersections with U, such that base change exhibits FP_M as the cofiltered 2-colimit of the FP_{W i} and FP_N as that of the FP_{W i ∩ U}; these two statements are the hypotheses hloc and hoverlap. For M = Spec O_{S,s} they are what Stacks 07SK gives once the affine open neighbourhoods of s are known to have Spec O_{S,s} as their limit and the W i ∩ U to have its puncture as theirs — neither limit identification is available in this library, which is why the two colimit statements are carried as hypotheses rather than proved”.

The algebraic spaces of finite presentation over the base are the 2-fibre product FP_U ×_{FP_N} FP_M, when M is a cofiltered limit of open neighbourhoods of the point complementary to U and N is the corresponding limit of their intersections with U.

This is Stacks 0E90 for M = Spec O_{S,s} and N = Spec O_{S,s} ∖ {s}, granted the two colimit identifications carried as the hypotheses hloc and hoverlap: what the theorem proves is the formal combination, namely that the comparison functor is faithful, full and essentially surjective. Faithfulness and fullness come from the equivalence of Stacks 0E8Z at a single neighbourhood, which applies because the complement of the point and any neighbourhood of it cover the base; essential surjectivity needs in addition that a glueing datum descends to a neighbourhood.

theorem isEquivalence_glueingFunctor_of_colimit :
    (glueingFunctor B S hS hsq.w).IsEquivalence

AlgebraicGeometry.FinitePresentationSpacesOver.isEquivalence_glueingFunctor_specStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationSpecStalkGlueing.lean, line 198. The attribute's comment: “the equivalence, unconditionally: for a point s of S whose complement is an open U with quasi-compact inclusion — the tag's closed point and quasi-compact U → S — the comparison functor FP_S ⥤ FP_U ×_{FP_V} FP_{Spec O_{S,s}} is an equivalence, with V = Spec O_{S,s} ∖ {s} the complement of the closed point, which the vertex of the system of overlaps is by toScheme_obj_opensSpecStalkSiteObj_eq_compl_closedPoint. The two colimit identifications that the general theorem isEquivalence_glueingFunctor_of_colimit carries as hypotheses are discharged here from Stacks 07SK and the identification of Spec O_{S,s} and of its puncture as the limits of the affine open neighbourhoods of s and of their intersections with U”.

Stacks 0E90. Let S be a scheme, let s be a point of S and let U be an open of S whose underlying set is the complement of s — so s is a closed point of S — with quasi-compact inclusion morphism. Then for every affine open neighbourhood W₀ of s the comparison functor FP_S ⥤ FP_U ×_{FP_V} FP_{Spec 𝒪_{S, s}} is an equivalence, where FP_T is the category of algebraic spaces of finite presentation over T and V is the vertex of the system of overlaps, whose underlying scheme is the complement of the closed point of Spec 𝒪_{S, s} — the tag's V — by AlgebraicGeometry.toScheme_obj_opensSpecStalkSiteObj_eq_compl_closedPoint.

Every input is unconditional. The two cartesian squares are AlgebraicGeometry.isPullback_opensSpecStalkApex and AlgebraicGeometry.isPullback_opensSpecStalkStage; the four compatibilities hold by terminality; the colimit identification over the neighbourhoods is FinitePresentationSpacesOver.isFinitePresentationColimit_restrictedSpecStalkSiteCone, which has no hypothesis, and the one over the overlaps is AlgebraicGeometry.FinitePresentationSpacesOver.isFinitePresentationColimit_opensSpecStalkSiteCone, whose single hypothesis is retrocompactness of U — the form the tag's quasi-compactness of U → S takes, by AlgebraicGeometry.isRetrocompact_of_quasiCompact_ι. Quasi-compactness of U → S is used in that one place, exactly as in the tag's proof.

theorem isEquivalence_glueingFunctor_specStalk (hUc : (U : Set S) = {s}ᶜ)
    (hqc : QuasiCompact U.ι) :
    (glueingFunctor B S hS (isPullback_opensSpecStalkApex B S hS s W₀ U).w).IsEquivalence

Tag 0E91, a lemma

Tag 0E91 in the Stacks Project.

AlgebraicGeometry.FinitePresentationSpacesOver.isGlueingColimitEquivalence_of_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationLocalRingGlueing.lean, line 591. The attribute's comment: “the equivalence out of the filtered 2-colimit, in the concrete form: the comparison functors out of the stages are jointly essentially surjective, full and faithful. The 2-colimit category itself is not constructed. The theorem is stated for an arbitrary object M of the site equipped with a cofiltered system of opens W i under it, an object N over the system of the Wn i, and a system of stages Z i covered by U and W i, such that base change exhibits FP_M as the cofiltered 2-colimit of the FP_{W i} and FP_N as that of the FP_{Wn i} — the hypotheses hloc and hoverlap. For M = Spec O_{S,s}, W i the affine open neighbourhoods of s, Wn i = W i ∩ U and Z i = U ∪ W i these two are what Stacks 07SK gives once the W i are known to have Spec O_{S,s} as their limit and the Wn i to have V = Spec O_{S,s} ∩ U as theirs — the Wn i being quasi-compact because U is retrocompact in S. Neither limit identification is available in this library, which is why the two colimit statements are carried as hypotheses rather than proved; hstage is Stacks 0E8Z at the stage Z i, which this library proves only for a base that is terminal in the site”.

The algebraic spaces of finite presentation over the opens between U and S containing the point s have the 2-fibre product FP_U ×_{FP_V} FP_{Spec 𝒪_{S,s}} as their filtered 2-colimit, when M is a cofiltered limit of the stages W i and N the corresponding limit of the Wn i = U ∩ W i, and the stages Z i = U ∪ W i are covered by U and W i.

This is Stacks 0E91. What the theorem proves is the formal combination: the comparison functors FP_{Z i} ⥤ FP_U ×_{FP_N} FP_M are jointly essentially surjective, full and faithful in the sense of an equivalence out of a filtered 2-colimit, which is the content of AlgebraicGeometry.FinitePresentationSpacesOver.IsGlueingColimitEquivalence.

theorem isGlueingColimitEquivalence_of_colimit :
    IsGlueingColimitEquivalence B S hS Z jU jM
      (glueingSquare B S hS hsqW hjMW hpNU hpNW) hjUZ
      (glueingCone B S hS hjWZ hjMW hpM)

AlgebraicGeometry.FinitePresentationSpacesOver.isEquivalence_specStalkStageColimitFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationLocalRingGlueingRealised.lean, line 259. The attribute's comment: “the equivalence of categories out of the filtered 2-colimit. The colimit of the categories FP_{U ∪ W} is the category StageColimit — objects the spaces over a stage, morphisms the germs — and the comparison functor specStalkStageColimitFunctor out of it to FP_U ×_{FP_V} FP_{Spec O_{S,s}} is full, faithful and essentially surjective, which is the fifth clause. The colimit runs over the stages U ∪ W, W an affine open neighbourhood of s inside a fixed one; the first two clauses say these are a cofinal family among the tag's opens U' with U ⊆ U' and s ∈ U', so the colimit is the tag's. The third and fourth clauses pin the other two vertices: Spec O_{S,s}, and V as the preimage of U in it. The sole hypothesis is the tag's, that U is retrocompact in S; the tag's s ∉ U is unused, so the statement covers it”.

Let S be a scheme, U a retrocompact open of S and s a point of S, and put V = Spec 𝒪_{S, s} ∩ U. Then the comparison functor colim_{s ∈ U' ⊇ U open} FP_{U'} ⟶ FP_U ×_{FP_V} FP_{Spec 𝒪_{S, s}} is an equivalence of categories.

The colimit is the category StageColimit over the stages U ∪ W, W running over the affine open neighbourhoods of s contained in W₀. The first two clauses say that the stages are cofinal among the opens U' of S with U ⊆ U' and s ∈ U'; the third and fourth identify the remaining vertices of the 2-fibre product as Spec 𝒪_{S, s} and as V, the preimage of U in Spec 𝒪_{S, s}; the fifth is the equivalence.

theorem isEquivalence_specStalkStageColimitFunctor (hU : IsRetrocompact (U : Set S)) :
    (∀ j : Over W₀, U ≤ U ⊔ j.left.obj.1 ∧ s ∈ U ⊔ j.left.obj.1) ∧
      (∀ U' : S.Opens, U ≤ U' → s ∈ U' → ∃ j : Over W₀, U ⊔ j.left.obj.1 ≤ U') ∧
        (BigFppfOver.toScheme B S hS).obj (restrictedSpecStalkSiteCone B S hS s W₀).pt =
            Spec (S.presheaf.stalk s) ∧
          (BigFppfOver.toScheme B S hS).obj (opensSpecStalkSiteObj B S hS s W₀ U) =
              (S.fromSpecStalk s ⁻¹ᵁ U).toScheme ∧
            (specStalkStageColimitFunctor B S hS s W₀ U).IsEquivalence

Tag 0E92, a lemma

Tag 0E92 in the Stacks Project.

AlgebraicGeometry.FinitePresentationSpacesOver.ClosedPointsGlueingData.essSurj_comparisonFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationClosedPointsGlueing.lean, line 526. The attribute's comment: “the comparison functor, and its essential surjectivity granted the case n = 1 of the lemma — that is, Stacks 0E90 — at each step of a tower of intermediate bases, carried as the hypothesis Solvable. The target is the iso-comma category of the two functors into ∀ i, FP_{Uᵢ} assembled from the base changes, which is the 2-fibre product the lemma names. Full faithfulness, and hence that the functor is an equivalence, is NOT proved: the proof of Stacks 0E92 omits it”.

Stacks 0E92, essential surjectivity of the comparison functor, granted the case n = 1. Every object of the n-fold 2-fibre product — an algebraic space of finite presentation over the open part, a family of such over the local parts, and a family of identifications over the overlaps — is, up to isomorphism, the image of an algebraic space of finite presentation over the base, as soon as the glueing data admits a tower of splittings whose binary comparison functors are essentially surjective. The induction splits off the last point by one such comparison functor and applies the induction hypothesis to the remaining points.

theorem essSurj_comparisonFunctor :
    ∀ (n : ℕ) (D : ClosedPointsGlueingData B S hS n), Solvable n D →
      D.comparisonFunctor.EssSurj

AlgebraicGeometry.FinitePresentationSpacesOver.isEquivalence_comparisonFunctor_closedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FinitePresentationClosedPointsGlueingEquivalence.lean, line 463.

Stacks 0E92. Let S be a scheme of a big fppf site and let s₁, …, sₙ be pairwise distinct closed points of S such that U = S ∖ {s₁, …, sₙ} ⟶ S is quasi-compact. With Sᵢ = Spec 𝒪_{S,sᵢ} and Uᵢ = Sᵢ ∖ {sᵢ}, the comparison functor FP_S ⥤ FP_U ×_{(FP_{U₁} × ⋯ × FP_{Uₙ})} (FP_{S₁} × ⋯ × FP_{Sₙ}), taking an algebraic space of finite presentation over S to its base change to U, the family of its base changes to the Sᵢ and the family of the canonical identifications of their base changes to the Uᵢ, is an equivalence of categories. Here FP_T is the category of algebraic spaces of finite presentation over T, and the 2-fibre product is the iso-comma category of the two functors into ∀ i, FP_{Uᵢ} assembled from the base changes.

theorem isEquivalence_comparisonFunctor_closedPoints {n : ℕ} (s : Fin n → S)
    (hinj : Function.Injective s) (hs : ∀ i, IsClosed ({s i} : Set S)) (U : S.Opens)
    (hU : (U : Set S) = (Set.range s)ᶜ) (hqc : QuasiCompact U.ι) :
    (closedPointsGlueingData B S hS s hs U hU).comparisonFunctor.IsEquivalence

Sources

• Section 70.18, Tag 0E8Y
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isAlgebraicSpace_iff_forall_isAlgebraicSpace_relocalizeRestrict · AlgebraicGeometry.FinitePresentationSpacesOver.isEquivalence_glueingFunctor · AlgebraicGeometry.FinitePresentationSpacesOver.isEquivalence_glueingFunctor_of_colimit · AlgebraicGeometry.FinitePresentationSpacesOver.isEquivalence_glueingFunctor_specStalk · AlgebraicGeometry.FinitePresentationSpacesOver.isGlueingColimitEquivalence_of_colimit · AlgebraicGeometry.FinitePresentationSpacesOver.isEquivalence_specStalkStageColimitFunctor · AlgebraicGeometry.FinitePresentationSpacesOver.ClosedPointsGlueingData.essSurj_comparisonFunctor · AlgebraicGeometry.FinitePresentationSpacesOver.isEquivalence_comparisonFunctor_closedPoints

Section70.19 Application to modifications#

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

Tag 0BGY, a lemma

Tag 0BGY in the Stacks Project.

AlgebraicGeometry.Space.essSurj_baseChangeFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionEquivalence.lean, line 138. The attribute's comment: “the base-change functor is essentially surjective”.

Stacks 0BGY, essential surjectivity of the base-change functor. Let f : V ⟶ W be a separated étale morphism of algebraic spaces over S and let T be a closed subspace of W whose preimage is carried isomorphically onto T. Then every modification of V outside f⁻¹W⁰ is isomorphic to the base change of a modification of W outside W⁰, namely of the dependent product Π_f Y, the isomorphism being the counit.

theorem essSurj_baseChangeFunctor (f : V ⟶ W) (T : Subfunctor W.obj)
    (hT : IsClosedSubspace B S hS T) (hfT : IsIso (T.fromPreimage f.hom))
    (hf : IsEtale B S hS f.hom) (hsep : IsSeparated B S hS f.hom) :
    (baseChangeFunctor B S hS f (openComplement B S hS T)).1.EssSurj

AlgebraicGeometry.Space.isEquivalence_baseChangeFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionEquivalence.lean, line 159. The attribute's comment: “equivalence of categories”.

Stacks 0BGY. Let f : V ⟶ W be a separated étale morphism of algebraic spaces over a scheme S and let T ⊂ W be a closed subspace such that f⁻¹T → T is an isomorphism. Write W⁰ for the complement of T and V⁰ = f⁻¹W⁰. Then base change along f is an equivalence from the category of morphisms g : X ⟶ W of algebraic spaces with g⁻¹W⁰ → W⁰ an isomorphism to the category of morphisms h : Y ⟶ V of algebraic spaces with h⁻¹V⁰ → V⁰ an isomorphism.

Faithfulness is AlgebraicGeometry.Space.faithful_baseChangeFunctor, fullness is AlgebraicGeometry.Space.full_baseChangeFunctor and essential surjectivity is AlgebraicGeometry.Space.essSurj_baseChangeFunctor.

theorem isEquivalence_baseChangeFunctor (f : V ⟶ W) (T : Subfunctor W.obj)
    (hT : IsClosedSubspace B S hS T) (hfT : IsIso (T.fromPreimage f.hom))
    (hf : IsEtale B S hS f.hom) (hsep : IsSeparated B S hS f.hom) :
    (baseChangeFunctor B S hS f (openComplement B S hS T)).1.IsEquivalence

AlgebraicGeometry.Space.faithful_baseChangeFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionFaithful.lean, line 199. The attribute's comment: “the base-change functor is faithful”.

Stacks 0BGY, faithfulness of the base-change functor. Let f : V ⟶ W be an étale morphism of algebraic spaces over S and let T be a closed subspace of W whose preimage is carried isomorphically onto T. Then the functor of Stacks 0BGY, base change along f from the modifications of W outside the open complement W⁰ of T to the modifications of V outside f⁻¹W⁰, is faithful.

Two morphisms of modifications which agree after base change agree on X ×_W V, and they agree over W⁰ because the target is an isomorphism there; those two parts cover the source locally, which is a sheaf, so the morphisms are equal.

theorem faithful_baseChangeFunctor (f : V ⟶ W) (T : Subfunctor W.obj)
    (hT : IsClosedSubspace B S hS T) (hfT : IsIso (T.fromPreimage f.hom))
    (hf : IsEtale B S hS f.hom) :
    (baseChangeFunctor B S hS f (openComplement B S hS T)).1.Faithful

AlgebraicGeometry.Space.full_baseChangeFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionFull.lean, line 315. The attribute's comment: “the base-change functor is full”.

Stacks 0BGY, fullness of the base-change functor. Let f : V ⟶ W be a separated étale morphism of algebraic spaces over S and let T be a closed subspace of W whose preimage is carried isomorphically onto T. Then the functor of Stacks 0BGY, base change along f from the modifications of W outside the open complement W⁰ of T to the modifications of V outside f⁻¹W⁰, is full.

theorem full_baseChangeFunctor (f : V ⟶ W') (T : Subfunctor W'.obj)
    (hT : IsClosedSubspace B S hS T) (hfT : IsIso (T.fromPreimage f.hom))
    (hf : IsEtale B S hS f.hom) (hsep : IsSeparated B S hS f.hom) :
    (baseChangeFunctor B S hS f (openComplement B S hS T)).1.Full

AlgebraicGeometry.Space.fullyFaithful_baseChangeFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionFull.lean, line 326. The attribute's comment: “the base-change functor is fully faithful”.

Stacks 0BGY, full faithfulness of the base-change functor.

noncomputable def fullyFaithful_baseChangeFunctor (f : V ⟶ W') (T : Subfunctor W'.obj)
    (hT : IsClosedSubspace B S hS T) (hfT : IsIso (T.fromPreimage f.hom))
    (hf : IsEtale B S hS f.hom) (hsep : IsSeparated B S hS f.hom) :
    (baseChangeFunctor B S hS f (openComplement B S hS T)).1.FullyFaithful

AlgebraicGeometry.Space.baseChangeFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Modifications.lean, line 198. The attribute's comment: “the base-change functor”.

Stacks 0BGY. Pullback of modifications, canonically identified with pullback of their underlying presheaves over the base.

noncomputable def baseChangeFunctor {V W : AlgebraicSpaces B S hS}
    (f : V ⟶ W) (W₀ : Subfunctor W.obj) :
    Σ F : Modification B S hS W₀ ⥤ Modification B S hS (W₀.preimage f.hom),
      F ⋙ ObjectProperty.ι (IsModification B S hS (W₀.preimage f.hom)) ≅
        ObjectProperty.ι (IsModification B S hS W₀) ⋙ Over.pullback f.hom

Tag 0BGZ, a lemma

Tag 0BGZ in the Stacks Project.

AlgebraicGeometry.Space.isQuasiCompact_iff_baseChangeFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionProperties.lean, line 207. The attribute's comment: “quasi-compactness”.

A modification of W outside the complement of T is quasi-compact exactly when its base change to V is.

theorem isQuasiCompact_iff_baseChangeFunctor_obj :
    IsQuasiCompact B S hS g.obj.hom ↔
      IsQuasiCompact B S hS
        ((baseChangeFunctor B S hS f (openComplement B S hS T)).1.obj g).obj.hom

AlgebraicGeometry.Space.isQuasiSeparated_iff_baseChangeFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionProperties.lean, line 229. The attribute's comment: “quasi-separatedness”.

A modification of W outside the complement of T is quasi-separated exactly when its base change to V is.

theorem isQuasiSeparated_iff_baseChangeFunctor_obj :
    IsQuasiSeparated B S hS g.obj.hom ↔
      IsQuasiSeparated B S hS
        ((baseChangeFunctor B S hS f (openComplement B S hS T)).1.obj g).obj.hom

AlgebraicGeometry.Space.isSeparated_iff_baseChangeFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionProperties.lean, line 252. The attribute's comment: “separatedness”.

A modification of W outside the complement of T is separated exactly when its base change to V is.

theorem isSeparated_iff_baseChangeFunctor_obj :
    IsSeparated B S hS g.obj.hom ↔
      IsSeparated B S hS
        ((baseChangeFunctor B S hS f (openComplement B S hS T)).1.obj g).obj.hom

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_iff_baseChangeFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionProperties.lean, line 279. The attribute's comment: “local finite presentation”.

A modification of W outside the complement of T is locally of finite presentation exactly when its base change to V is.

theorem isLocallyOfFinitePresentation_iff_baseChangeFunctor_obj :
    IsLocallyOfFinitePresentation B S hS g.obj.hom ↔
      IsLocallyOfFinitePresentation B S hS
        ((baseChangeFunctor B S hS f (openComplement B S hS T)).1.obj g).obj.hom

AlgebraicGeometry.Space.isLocallyOfFiniteType_iff_baseChangeFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionProperties.lean, line 309. The attribute's comment: “local finite type”.

A modification of W outside the complement of T is locally of finite type exactly when its base change to V is.

theorem isLocallyOfFiniteType_iff_baseChangeFunctor_obj :
    IsLocallyOfFiniteType B S hS g.obj.hom ↔
      IsLocallyOfFiniteType B S hS
        ((baseChangeFunctor B S hS f (openComplement B S hS T)).1.obj g).obj.hom

AlgebraicGeometry.Space.isFiniteType_iff_baseChangeFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionProperties.lean, line 341. The attribute's comment: “finite type”.

A modification of W outside the complement of T is of finite type exactly when its base change to V is.

theorem isFiniteType_iff_baseChangeFunctor_obj :
    IsFiniteType B S hS g.obj.hom ↔
      IsFiniteType B S hS
        ((baseChangeFunctor B S hS f (openComplement B S hS T)).1.obj g).obj.hom

AlgebraicGeometry.Space.isFinitePresentation_iff_baseChangeFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionProperties.lean, line 352. The attribute's comment: “finite presentation”.

A modification of W outside the complement of T is of finite presentation exactly when its base change to V is.

theorem isFinitePresentation_iff_baseChangeFunctor_obj :
    IsFinitePresentation B S hS g.obj.hom ↔
      IsFinitePresentation B S hS
        ((baseChangeFunctor B S hS f (openComplement B S hS T)).1.obj g).obj.hom

AlgebraicGeometry.Space.isProper_iff_baseChangeFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionProperties.lean, line 365. The attribute's comment: “properness”.

A modification of W outside the complement of T is proper exactly when its base change to V is.

theorem isProper_iff_baseChangeFunctor_obj :
    IsProper B S hS g.obj.hom ↔
      IsProper B S hS
        ((baseChangeFunctor B S hS f (openComplement B S hS T)).1.obj g).obj.hom

AlgebraicGeometry.Space.isIntegralHom_iff_baseChangeFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionProperties.lean, line 387. The attribute's comment: “integrality”.

A modification of W outside the complement of T is integral exactly when its base change to V is.

theorem isIntegralHom_iff_baseChangeFunctor_obj :
    IsIntegralHom B S hS g.obj.hom ↔
      IsIntegralHom B S hS
        ((baseChangeFunctor B S hS f (openComplement B S hS T)).1.obj g).obj.hom

AlgebraicGeometry.Space.isFinite_iff_baseChangeFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationExcisionProperties.lean, line 405. The attribute's comment: “finiteness”.

A modification of W outside the complement of T is finite exactly when its base change to V is.

theorem isFinite_iff_baseChangeFunctor_obj :
    IsFinite B S hS g.obj.hom ↔
      IsFinite B S hS
        ((baseChangeFunctor B S hS f (openComplement B S hS T)).1.obj g).obj.hom

Tag 0BH0, a lemma

Tag 0BH0 in the Stacks Project.

AlgebraicGeometry.Space.ClosedPointNeighborhood.isEquivalence_henselianBaseChangeFunctor_of_isHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationsHenselianLocalRingEquivalence.lean, line 957.

Stacks 0BH0. Let X be a decent algebraic space over S and x ∈ |X| a closed point such that U = X ∖ {x} ⟶ X is quasi-compact; let (W, w) → (X, x) be an affine elementary étale neighbourhood with w the only point above x (Stacks 0BBP) and let R be a henselization of 𝒪_{W, w}, so that R = 𝒪^h_{X, x} (Stacks 0EMY). With V = Spec(𝒪^h_{X, x}) ∖ {𝔪^h_x}, the base change functor from the morphisms f : Y ⟶ X of finite presentation with f⁻¹(U) ⟶ U an isomorphism to the morphisms g : Y ⟶ Spec(𝒪^h_{X, x}) of finite presentation with g⁻¹(V) ⟶ V an isomorphism is an equivalence of categories.

theorem isEquivalence_henselianBaseChangeFunctor_of_isHenselization :
    (D.henselianBaseChangeFunctor R (D.contains_spec_of_isHenselization R)).IsEquivalence

Sources

• Section 70.19, Tag 0BGX
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.essSurj_baseChangeFunctor · AlgebraicGeometry.Space.isEquivalence_baseChangeFunctor · AlgebraicGeometry.Space.faithful_baseChangeFunctor · AlgebraicGeometry.Space.full_baseChangeFunctor · AlgebraicGeometry.Space.fullyFaithful_baseChangeFunctor · AlgebraicGeometry.Space.baseChangeFunctor · AlgebraicGeometry.Space.isQuasiCompact_iff_baseChangeFunctor_obj · AlgebraicGeometry.Space.isQuasiSeparated_iff_baseChangeFunctor_obj

Section70.20 Universally closed morphisms#

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

Tag 0CM8, a lemma

Tag 0CM8 in the Stacks Project.

AlgebraicGeometry.Space.exists_affine_etale_isLocallyOfFinitePresentation_separation_of_isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/AffineFinitePresentationFactorizationQuasiSeparated.lean, line 372. The attribute's comment: “the whole lemma, including the refinement for Z a scheme (V an affine open neighbourhood of z), under the extra hypothesis that Y is quasi-separated. For an arbitrary Y the refinement is open: it is equivalent to Z -> Y factoring Zariski locally through an affine scheme locally of finite presentation over Y, which is proved here only for Y quasi-separated”.

Stacks 0CM8, for Y quasi-separated. Let f : X ⟶ Y be a quasi-compact morphism of algebraic spaces over S with Y quasi-separated.

1. For every morphism g : Z ⟶ Y of algebraic spaces, point z of |Z| and closed subset T of |X ×_Y Z| whose image in |Z| misses z, there are an affine étale neighbourhood (V, v) of z, an affine Z' and a factorization V ⟶ Z' ⟶ Y of V ⟶ Y whose second leg b is locally of finite presentation, and a closed subset T' of |X ×_Y Z'| whose image in |Z'| misses the image of v and which receives the inverse image of T along the comparison morphisms r and q of the three fibre products.
2. If moreover Z is a scheme, represented by an object Z₀ of the site, then V may be taken to be an affine open neighbourhood of z: the étale neighbourhood is an open immersion V ⟶ Z₀ sending v to z, with all the conclusions of the first part.

The first part is exists_affine_etale_isLocallyOfFinitePresentation_separation, which needs no hypothesis on Y. The second part is exists_affineOpen_isLocallyOfFinitePresentation_separation_of_factorization, whose input — a Zariski-local factorization of Z₀ ⟶ Y through an affine scheme locally of finite presentation over Y — is supplied for quasi-separated Y by exists_affine_isLocallyOfFinitePresentation_factorization_of_isAbsolutelyQuasiSeparated.

theorem exists_affine_etale_isLocallyOfFinitePresentation_separation_of_isAbsolutelyQuasiSeparated
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y) (f : X ⟶ Y)
    (hf : IsQuasiCompact B S hS f) :
    (∀ {Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (_ : IsAlgebraicSpace B S hS Z) (g : Z ⟶ Y)
      (z : points B S hS Z) (T : Set (points B S hS (pullback f g))), IsClosed T →
      z ∉ pointsMap B S hS (pullback f g) (pullback.snd f g) '' T →
      ∃ (V Z' : BigFppfOver B S hS) (p : yoneda.obj V ⟶ Z)
        (v : points B S hS (yoneda.obj V)) (a : yoneda.obj V ⟶ yoneda.obj Z')
        (b : yoneda.obj Z' ⟶ Y) (T' : Set (points B S hS (pullback f b)))
        (r : pullback f (p ≫ g) ⟶ pullback f g) (q : pullback f (p ≫ g) ⟶ pullback f b),
        IsAffine ((BigFppfOver.toScheme B S hS).obj V) ∧
        IsAffine ((BigFppfOver.toScheme B S hS).obj Z') ∧
        IsEtale B S hS p ∧
        pointsMap B S hS (yoneda.obj V) p v = z ∧
        p ≫ g = a ≫ b ∧
        IsLocallyOfFinitePresentation B S hS b ∧
        IsClosed T' ∧
        pointsMap B S hS (yoneda.obj V) a v ∉
          pointsMap B S hS (pullback f b) (pullback.snd f b) '' T' ∧
        r ≫ pullback.fst f g = pullback.fst f (p ≫ g) ∧
        r ≫ pullback.snd f g = pullback.snd f (p ≫ g) ≫ p ∧
        IsPullback r (pullback.snd f (p ≫ g)) (pullback.snd f g) p ∧
        q ≫ pullback.fst f b = pullback.fst f (p ≫ g) ∧
        q ≫ pullback.snd f b = pullback.snd f (p ≫ g) ≫ a ∧
        pointsMap B S hS (pullback f (p ≫ g)) q ''
          (pointsMap B S hS (pullback f (p ≫ g)) r ⁻¹' T) ⊆ T') ∧
    (∀ {Z₀ : BigFppfOver B S hS} (g : yoneda.obj Z₀ ⟶ Y) (z : points B S hS (yoneda.obj Z₀))
      (T : Set (points B S hS (pullback f g))), IsClosed T →
      z ∉ pointsMap B S hS (pullback f g) (pullback.snd f g) '' T →
      ∃ (V Z' : BigFppfOver B S hS) (p : yoneda.obj V ⟶ yoneda.obj Z₀) (pV : V ⟶ Z₀)
        (v : points B S hS (yoneda.obj V)) (a : yoneda.obj V ⟶ yoneda.obj Z')
        (b : yoneda.obj Z' ⟶ Y) (T' : Set (points B S hS (pullback f b)))
        (r : pullback f (p ≫ g) ⟶ pullback f g) (q : pullback f (p ≫ g) ⟶ pullback f b),
        p = yoneda.map pV ∧
        AlgebraicGeometry.IsOpenImmersion ((BigFppfOver.toScheme B S hS).map pV) ∧
        (BigFppfOver.toScheme B S hS).map pV (pointsToScheme B S hS V v) =
          pointsToScheme B S hS Z₀ z ∧
        IsAffine ((BigFppfOver.toScheme B S hS).obj V) ∧
        IsAffine ((BigFppfOver.toScheme B S hS).obj Z') ∧
        IsEtale B S hS p ∧
        pointsMap B S hS (yoneda.obj V) p v = z ∧
        p ≫ g = a ≫ b ∧
        IsLocallyOfFinitePresentation B S hS b ∧
        IsClosed T' ∧
        pointsMap B S hS (yoneda.obj V) a v ∉
          pointsMap B S hS (pullback f b) (pullback.snd f b) '' T' ∧
        r ≫ pullback.fst f g = pullback.fst f (p ≫ g) ∧
        r ≫ pullback.snd f g = pullback.snd f (p ≫ g) ≫ p ∧
        IsPullback r (pullback.snd f (p ≫ g)) (pullback.snd f g) p ∧
        q ≫ pullback.fst f b = pullback.fst f (p ≫ g) ∧
        q ≫ pullback.snd f b = pullback.snd f (p ≫ g) ≫ a ∧
        pointsMap B S hS (pullback f (p ≫ g)) q ''
          (pointsMap B S hS (pullback f (p ≫ g)) r ⁻¹' T) ⊆ T')

AlgebraicGeometry.Space.exists_affine_elementary_etale_separation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ElementaryEtaleSeparation.lean, line 162. The attribute's comment: “the separation statement for Z a scheme, with V and Z' affine and the etale neighbourhood of z elementary -- the canonical morphism Spec kappa(z) -> Z factors through it -- and with clauses (1), (2) and (3) unchanged”.

Stacks 0CM8 for Z a scheme, with an elementary étale neighbourhood. Let f : X ⟶ Y be a quasi-compact morphism of algebraic spaces over S with Z represented by an object Z₀ of the site, let z be a point of |Z₀|, and let T be a closed subset of |X ×_Y Z₀| whose image in |Z₀| misses z. Then the conclusion of Tag 0CM8 holds with V and Z' affine and with the étale neighbourhood p : V ⟶ Z₀ elementary: the canonical morphism Spec κ(z) ⟶ Z₀ factors through it, so v and z have the same residue field.

The source asks only for an étale neighbourhood. The elementary refinement holds for an arbitrary algebraic space Y, because the chart of Y can be chosen to receive the field-valued point of z.

theorem exists_affine_elementary_etale_separation
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {Z₀ : BigFppfOver B S hS}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (g : yoneda.obj Z₀ ⟶ Y) (hf : IsQuasiCompact B S hS f)
    (z : points B S hS (yoneda.obj Z₀))
    (T : Set (points B S hS (pullback f g))) (hT : IsClosed T)
    (hz : z ∉ pointsMap B S hS (pullback f g) (pullback.snd f g) '' T) :
    ∃ (V Z' : BigFppfOver B S hS) (p : yoneda.obj V ⟶ yoneda.obj Z₀) (pV : V ⟶ Z₀)
      (v : points B S hS (yoneda.obj V)) (a : yoneda.obj V ⟶ yoneda.obj Z')
      (b : yoneda.obj Z' ⟶ Y) (T' : Set (points B S hS (pullback f b)))
      (r : pullback f (p ≫ g) ⟶ pullback f g) (q : pullback f (p ≫ g) ⟶ pullback f b)
      (s : FieldValuedPoint.siteObject B S hS (yoneda.obj Z₀)
        (schemePointRepresentative B S hS Z₀ (pointsToScheme B S hS Z₀ z)) ⟶ V),
      p = yoneda.map pV ∧
      s ≫ pV = (schemePointRepresentative B S hS Z₀ (pointsToScheme B S hS Z₀ z)).siteHom ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj V) ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj Z') ∧
      IsEtale B S hS p ∧
      pointsMap B S hS (yoneda.obj V) p v = z ∧
      p ≫ g = a ≫ b ∧
      IsLocallyOfFinitePresentation B S hS b ∧
      IsClosed T' ∧
      pointsMap B S hS (yoneda.obj V) a v ∉
        pointsMap B S hS (pullback f b) (pullback.snd f b) '' T' ∧
      r ≫ pullback.fst f g = pullback.fst f (p ≫ g) ∧
      r ≫ pullback.snd f g = pullback.snd f (p ≫ g) ≫ p ∧
      IsPullback r (pullback.snd f (p ≫ g)) (pullback.snd f g) p ∧
      q ≫ pullback.fst f b = pullback.fst f (p ≫ g) ∧
      q ≫ pullback.snd f b = pullback.snd f (p ≫ g) ≫ a ∧
      pointsMap B S hS (pullback f (p ≫ g)) q ''
        (pointsMap B S hS (pullback f (p ≫ g)) r ⁻¹' T) ⊆ T'

AlgebraicGeometry.Space.exists_isClosed_separation_of_etale_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/UniversallyClosedSeparation.lean, line 203. The attribute's comment: “etale-descent step of the proof: clauses (2) and (3) descend along a cover of X whose represented base changes are etale and which is surjective on points; the reduction to the case of affine schemes and the appeal to Tag 05BD are not included”.

Stacks 0CM8, the étale-descent step of the proof. Let f : X ⟶ Y, b : Z' ⟶ Y and a : V ⟶ Z' be morphisms of presheaves on the big fppf site of S, and let c : W ⟶ X be a morphism whose represented base changes are étale and which is surjective on points. There are comparison morphisms γ, α₁, α₂, κ filling the square

W ×_Y V --α₁--> W ×_Y Z'
   |               |
   γ               κ
   ↓               ↓
X ×_Y V --α₂--> X ×_Y Z'

along which clauses (2) and (3) of Tag 0CM8 descend: given a closed subset T₀ of |W ×_Y Z'| receiving the inverse image of T ⊆ |X ×_Y V| and whose image in |Z'| misses r, there is a closed T' ⊆ |X ×_Y Z'| receiving T and whose image in |Z'| misses r. Clause (1), that b is locally of finite presentation, is a property of b alone and is untouched by the descent.

theorem exists_isClosed_separation_of_etale_cover
    (f : X ⟶ Y) (b : Z' ⟶ Y) (a : V ⟶ Z') (c : W ⟶ X)
    (hc : (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf c)
    (hcsurj : Function.Surjective (pointsMap B S hS W c)) :
    ∃ (γ : pullback (c ≫ f) (a ≫ b) ⟶ pullback f (a ≫ b))
      (α₁ : pullback (c ≫ f) (a ≫ b) ⟶ pullback (c ≫ f) b)
      (α₂ : pullback f (a ≫ b) ⟶ pullback f b)
      (κ : pullback (c ≫ f) b ⟶ pullback f b),
      γ ≫ pullback.fst f (a ≫ b) = pullback.fst (c ≫ f) (a ≫ b) ≫ c ∧
        γ ≫ pullback.snd f (a ≫ b) = pullback.snd (c ≫ f) (a ≫ b) ∧
        α₁ ≫ pullback.fst (c ≫ f) b = pullback.fst (c ≫ f) (a ≫ b) ∧
        α₁ ≫ pullback.snd (c ≫ f) b = pullback.snd (c ≫ f) (a ≫ b) ≫ a ∧
        α₂ ≫ pullback.fst f b = pullback.fst f (a ≫ b) ∧
        α₂ ≫ pullback.snd f b = pullback.snd f (a ≫ b) ≫ a ∧
        κ ≫ pullback.fst f b = pullback.fst (c ≫ f) b ≫ c ∧
        κ ≫ pullback.snd f b = pullback.snd (c ≫ f) b ∧
        ∀ (T : Set (points B S hS (pullback f (a ≫ b))))
          (T₀ : Set (points B S hS (pullback (c ≫ f) b))),
          @IsClosed _ (pointTopology B S hS (pullback (c ≫ f) b)) T₀ →
          pointsMap B S hS _ α₁ '' (pointsMap B S hS _ γ ⁻¹' T) ⊆ T₀ →
          ∀ r : points B S hS Z',
            r ∉ pointsMap B S hS _ (pullback.snd (c ≫ f) b) '' T₀ →
            ∃ T' : Set (points B S hS (pullback f b)),
              @IsClosed _ (pointTopology B S hS (pullback f b)) T' ∧
                T ⊆ pointsMap B S hS _ α₂ ⁻¹' T' ∧
                  r ∉ pointsMap B S hS _ (pullback.snd f b) '' T'

AlgebraicGeometry.Space.exists_affine_etale_isLocallyOfFinitePresentation_separation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/UniversallyClosedSeparation.lean, line 829. The attribute's comment: “the separation statement, with V and Z' affine; the refinement for Z a scheme, where V may be taken to be an affine open neighbourhood of z, is not included”.

Stacks 0CM8. Let f : X ⟶ Y be a quasi-compact morphism of algebraic spaces over S, let g : Z ⟶ Y be a morphism of algebraic spaces, let z be a point of |Z|, and let T be a closed subset of |X ×_Y Z| whose image in |Z| misses z. Then there are an affine étale neighbourhood (V, v) of z, an affine Z' and a factorization V ⟶ Z' ⟶ Y of V ⟶ Y whose second leg b is locally of finite presentation, and a closed subset T' of |X ×_Y Z'| whose image in |Z'| misses the image of v and which receives the inverse image of T along the two comparison morphisms r and q of the three fibre products.

theorem exists_affine_etale_isLocallyOfFinitePresentation_separation
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Z ⟶ Y)
    (hf : IsQuasiCompact B S hS f)
    (z : points B S hS Z) (T : Set (points B S hS (pullback f g))) (hT : IsClosed T)
    (hz : z ∉ pointsMap B S hS (pullback f g) (pullback.snd f g) '' T) :
    ∃ (V Z' : BigFppfOver B S hS) (p : yoneda.obj V ⟶ Z)
      (v : points B S hS (yoneda.obj V)) (a : yoneda.obj V ⟶ yoneda.obj Z')
      (b : yoneda.obj Z' ⟶ Y) (T' : Set (points B S hS (pullback f b)))
      (r : pullback f (p ≫ g) ⟶ pullback f g) (q : pullback f (p ≫ g) ⟶ pullback f b),
      IsAffine ((BigFppfOver.toScheme B S hS).obj V) ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj Z') ∧
      IsEtale B S hS p ∧
      pointsMap B S hS (yoneda.obj V) p v = z ∧
      p ≫ g = a ≫ b ∧
      IsLocallyOfFinitePresentation B S hS b ∧
      IsClosed T' ∧
      pointsMap B S hS (yoneda.obj V) a v ∉
        pointsMap B S hS (pullback f b) (pullback.snd f b) '' T' ∧
      r ≫ pullback.fst f g = pullback.fst f (p ≫ g) ∧
      r ≫ pullback.snd f g = pullback.snd f (p ≫ g) ≫ p ∧
      IsPullback r (pullback.snd f (p ≫ g)) (pullback.snd f g) p ∧
      q ≫ pullback.fst f b = pullback.fst f (p ≫ g) ∧
      q ≫ pullback.snd f b = pullback.snd f (p ≫ g) ≫ a ∧
      pointsMap B S hS (pullback f (p ≫ g)) q ''
        (pointsMap B S hS (pullback f (p ≫ g)) r ⁻¹' T) ⊆ T'

AlgebraicGeometry.Space.exists_affineOpen_isLocallyOfFinitePresentation_separation_of_lfp_morphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/UniversallyClosedSeparation.lean, line 1099. The attribute's comment: “the refinement for Z a scheme with Y an arbitrary algebraic space over S, for g : Z -> Y locally of finite presentation: the etale neighbourhood p : V -> Z is an open immersion onto an affine open neighbourhood of z, Z' is affine, and clauses (1), (2) and (3) hold -- b locally of finite presentation, the image of T' in |Z'| missing a(v), and T' receiving the inverse image of T. An affine open neighbourhood of z is then itself an affine scheme locally of finite presentation over Y, which is the factorization the refinement amounts to”.

Stacks 0CM8, the refinement for Z a scheme and Y an arbitrary algebraic space, for a morphism g : Z ⟶ Y which is locally of finite presentation. Let f : X ⟶ Y be a quasi-compact morphism of algebraic spaces over S with Z represented by an object Z₀ of the site, let g : yoneda.obj Z₀ ⟶ Y be locally of finite presentation, let z be a point of |Z₀|, and let T be a closed subset of |X ×_Y Z₀| whose image in |Z₀| misses z. Then the conclusion of Tag 0CM8 holds with the étale neighbourhood p an open immersion out of an affine V sending v to z: that is, V is an affine open neighbourhood of z, Z' is affine, and clauses (1), (2) and (3) — b locally of finite presentation, the image of T' in |Z'| missing the image of v, and T' receiving the inverse image of T — all hold, as does étaleness of p.

Nothing is assumed of Y beyond being an algebraic space over S.

theorem exists_affineOpen_isLocallyOfFinitePresentation_separation_of_lfp_morphism
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {Z₀ : BigFppfOver B S hS}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (g : yoneda.obj Z₀ ⟶ Y)
    (hf : IsQuasiCompact B S hS f) (hg : IsLocallyOfFinitePresentation B S hS g)
    (z : points B S hS (yoneda.obj Z₀))
    (T : Set (points B S hS (pullback f g))) (hT : IsClosed T)
    (hz : z ∉ pointsMap B S hS (pullback f g) (pullback.snd f g) '' T) :
    ∃ (V Z' : BigFppfOver B S hS) (p : yoneda.obj V ⟶ yoneda.obj Z₀) (pV : V ⟶ Z₀)
      (v : points B S hS (yoneda.obj V)) (a : yoneda.obj V ⟶ yoneda.obj Z')
      (b : yoneda.obj Z' ⟶ Y) (T' : Set (points B S hS (pullback f b)))
      (r : pullback f (p ≫ g) ⟶ pullback f g) (q : pullback f (p ≫ g) ⟶ pullback f b),
      p = yoneda.map pV ∧
      AlgebraicGeometry.IsOpenImmersion ((BigFppfOver.toScheme B S hS).map pV) ∧
      (BigFppfOver.toScheme B S hS).map pV (pointsToScheme B S hS V v) =
        pointsToScheme B S hS Z₀ z ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj V) ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj Z') ∧
      IsEtale B S hS p ∧
      pointsMap B S hS (yoneda.obj V) p v = z ∧
      p ≫ g = a ≫ b ∧
      IsLocallyOfFinitePresentation B S hS b ∧
      IsClosed T' ∧
      pointsMap B S hS (yoneda.obj V) a v ∉
        pointsMap B S hS (pullback f b) (pullback.snd f b) '' T' ∧
      r ≫ pullback.fst f g = pullback.fst f (p ≫ g) ∧
      r ≫ pullback.snd f g = pullback.snd f (p ≫ g) ≫ p ∧
      IsPullback r (pullback.snd f (p ≫ g)) (pullback.snd f g) p ∧
      q ≫ pullback.fst f b = pullback.fst f (p ≫ g) ∧
      q ≫ pullback.snd f b = pullback.snd f (p ≫ g) ≫ a ∧
      pointsMap B S hS (pullback f (p ≫ g)) q ''
        (pointsMap B S hS (pullback f (p ≫ g)) r ⁻¹' T) ⊆ T'

AlgebraicGeometry.Space.exists_affineOpen_isLocallyOfFinitePresentation_separation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/UniversallyClosedSeparation.lean, line 1254. The attribute's comment: “the refinement for Z a scheme with no hypothesis on g, for Y represented by an object of the site as well -- the situation the source's own proof reduces to before it produces the affine open neighbourhood: the etale neighbourhood p : V -> Z is an open immersion onto an affine open neighbourhood of z, Z' is affine, and clauses (1), (2) and (3) hold -- b locally of finite presentation, the image of T' in |Z'| missing a(v), and T' receiving the inverse image of T. The affine opens of Y supply the factorization of an affine open neighbourhood of z through an affine scheme locally of finite presentation over Y that the refinement amounts to”.

Stacks 0CM8, the refinement for Z a scheme, with no hypothesis on g, in the situation the source's own proof reduces to, where Y is represented by an object of the site as well. Let f : X ⟶ Y be a quasi-compact morphism with X an algebraic space over S and Y and Z represented by objects Y₀ and Z₀ of the site, let z be a point of |Z₀|, and let T be a closed subset of |X ×_Y Z₀| whose image in |Z₀| misses z. Then the conclusion of Tag 0CM8 holds with V an affine open neighbourhood of z: the morphism p : V ⟶ Z₀ is an open immersion sending v to z, V and Z' are affine, and clauses (1), (2) and (3) of the source hold unchanged.

For Y an arbitrary algebraic space the refinement holds whenever g is locally of finite presentation, by exists_affineOpen_isLocallyOfFinitePresentation_separation_of_lfp_morphism, and in general from a Zariski-local factorization, by exists_affineOpen_isLocallyOfFinitePresentation_separation_of_factorization, which asks for the input in its sharpest form — an affine open neighbourhood of z whose morphism to Y factors through an affine scheme locally of finite presentation over Y. That input cannot be dispensed with: it is part of the refinement's own conclusion, by AlgebraicGeometry.Space.exists_affine_isLocallyOfFinitePresentation_factorization_of_separation. What Y being a scheme supplies is a Zariski-local factorization: for a general algebraic space the affine opens of Y are replaced by affine étale charts, and pulling a chart back along Z₀ ⟶ Y gives an étale morphism to Z₀, of which one needs a section near z. A point above z with the same residue field as z is not enough for that and is in any case always available, by AlgebraicGeometry.Space.exists_affine_etale_chart_of_fieldValuedPoint, for an arbitrary algebraic space and with no decency hypothesis; an étale morphism with trivial residue extension at a point has a section near it exactly when the map of local rings there is an isomorphism, by AlgebraicGeometry.exists_isOpenImmersion_of_etale_of_isIso_stalkMap, and that is the Henselian property of 𝒪_{Z₀, z} rather than anything about Y. What does supply the factorization for an arbitrary Y and an arbitrary g, and which step of it this development is missing, is recorded in the note opening this section.

theorem exists_affineOpen_isLocallyOfFinitePresentation_separation
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {Y₀ Z₀ : BigFppfOver B S hS}
    (hX : IsAlgebraicSpace B S hS X)
    (f : X ⟶ yoneda.obj Y₀) (g : yoneda.obj Z₀ ⟶ yoneda.obj Y₀)
    (hf : IsQuasiCompact B S hS f)
    (z : points B S hS (yoneda.obj Z₀))
    (T : Set (points B S hS (pullback f g))) (hT : IsClosed T)
    (hz : z ∉ pointsMap B S hS (pullback f g) (pullback.snd f g) '' T) :
    ∃ (V Z' : BigFppfOver B S hS) (p : yoneda.obj V ⟶ yoneda.obj Z₀) (pV : V ⟶ Z₀)
      (v : points B S hS (yoneda.obj V)) (a : yoneda.obj V ⟶ yoneda.obj Z')
      (b : yoneda.obj Z' ⟶ yoneda.obj Y₀) (T' : Set (points B S hS (pullback f b)))
      (r : pullback f (p ≫ g) ⟶ pullback f g) (q : pullback f (p ≫ g) ⟶ pullback f b),
      p = yoneda.map pV ∧
      AlgebraicGeometry.IsOpenImmersion ((BigFppfOver.toScheme B S hS).map pV) ∧
      (BigFppfOver.toScheme B S hS).map pV (pointsToScheme B S hS V v) =
        pointsToScheme B S hS Z₀ z ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj V) ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj Z') ∧
      IsEtale B S hS p ∧
      pointsMap B S hS (yoneda.obj V) p v = z ∧
      p ≫ g = a ≫ b ∧
      IsLocallyOfFinitePresentation B S hS b ∧
      IsClosed T' ∧
      pointsMap B S hS (yoneda.obj V) a v ∉
        pointsMap B S hS (pullback f b) (pullback.snd f b) '' T' ∧
      r ≫ pullback.fst f g = pullback.fst f (p ≫ g) ∧
      r ≫ pullback.snd f g = pullback.snd f (p ≫ g) ≫ p ∧
      IsPullback r (pullback.snd f (p ≫ g)) (pullback.snd f g) p ∧
      q ≫ pullback.fst f b = pullback.fst f (p ≫ g) ∧
      q ≫ pullback.snd f b = pullback.snd f (p ≫ g) ≫ a ∧
      pointsMap B S hS (pullback f (p ≫ g)) q ''
        (pointsMap B S hS (pullback f (p ≫ g)) r ⁻¹' T) ⊆ T'

Tag 0CM9, a lemma

Tag 0CM9 in the Stacks Project.

AlgebraicGeometry.Space.isClosedMorphism_pullback_fst_of_affineSpaceTest, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/UniversallyClosedAffineSpaceTest.lean, line 295. The attribute's comment: “(3) implies (2)”.

Stacks 0CM9, (3) implies (2). If f : X ⟶ Y passes the affine-space test over one surjective étale scheme atlas V ⟶ Y of the target, then the base change of f along every morphism to Y which is locally of finite presentation is closed.

Closedness of |Z ×_Y X| → |Z| may be checked after the base change along the composite of an étale atlas of Z ×_Y V with the projection to Z, which is open and surjective on points; that composite exhibits the test object as a morphism of the site into V locally of finite presentation, where the previous statement applies.

Quasi-compactness of f is not needed: it enters Tag 0CM9 only through the implication from the finitely presented tests back to universal closedness.

theorem isClosedMorphism_pullback_fst_of_affineSpaceTest
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y)
    (hgsurj : IsSurjective B S hS g) (hgetale : IsEtale B S hS g)
    (htest : ∀ n : ℕ, ∃ (W : BigFppfOver B S hS) (a : W ⟶ V), IsAffineSpaceOver B S hS V W n a ∧
      IsClosedMorphism B S hS (pullback.fst (yoneda.map a ≫ g) f))
    {Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hZ : IsAlgebraicSpace B S hS Z) (h : Z ⟶ Y)
    (hh : IsLocallyOfFinitePresentation B S hS h) :
    IsClosedMorphism B S hS (pullback.fst h f)

AlgebraicGeometry.Space.isClosedMorphism_pullback_fst_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/UniversallyClosedAffineSpaceTest.lean, line 355. The attribute's comment: “(1) implies (2)”.

Stacks 0CM9, (1) implies (2). The base change of a universally closed morphism of algebraic spaces over S along a morphism which is locally of finite presentation is closed.

theorem isClosedMorphism_pullback_fst_of_universallyClosed (f : X ⟶ Y)
    (hf : UniversallyClosed B S hS f) {Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hZ : IsAlgebraicSpace B S hS Z) (h : Z ⟶ Y)
    (_hh : IsLocallyOfFinitePresentation B S hS h) :
    IsClosedMorphism B S hS (pullback.fst h f)

AlgebraicGeometry.Space.exists_affineSpaceTest_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/UniversallyClosedAffineSpaceTest.lean, line 367. The attribute's comment: “(1) implies (3)”.

Stacks 0CM9, (1) implies (3). A universally closed morphism of algebraic spaces over S passes the affine-space test over every surjective étale scheme atlas of its target: each affine space over the atlas is an object of the site mapping to the target, so the base change of f along it is closed.

theorem exists_affineSpaceTest_of_universallyClosed (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : UniversallyClosed B S hS f) :
    ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
      IsSurjective B S hS g ∧ IsEtale B S hS g ∧
        ∀ n : ℕ, ∃ (W : BigFppfOver B S hS) (a : W ⟶ V), IsAffineSpaceOver B S hS V W n a ∧
          IsClosedMorphism B S hS (pullback.fst (yoneda.map a ≫ g) f)

AlgebraicGeometry.Space.universallyClosed_of_isClosedMorphism_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/UniversallyClosedAffineSpaceTest.lean, line 410. The attribute's comment: “(2) implies (1)”.

Stacks 0CM9, (2) implies (1). A quasi-compact morphism of algebraic spaces over S whose base changes along the morphisms locally of finite presentation are closed is universally closed.

Let T ⊆ |X ×_Y Z| be closed and let z be a point of |Z| outside the image of T. The separation statement of Tag 0CM8 produces an étale neighbourhood (V, v) of z, a factorization V ⟶ Z' ⟶ Y with Z' ⟶ Y locally of finite presentation, and a closed T' ⊆ |X ×_Y Z'| receiving the inverse image of T and missing the image of v. Since |V| → |Z| is open, v lies in the closure of the inverse image of the image of T, which by Tag 03H4 is the image of the inverse image of T in |X ×_Y V|; that image lands in the inverse image along V ⟶ Z' of the image of T', a closed set by hypothesis. Hence the image of v lies in the image of T' after all, so z is not in the closure of the image of T.

theorem universallyClosed_of_isClosedMorphism_of_isLocallyOfFinitePresentation
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsQuasiCompact B S hS f)
    (htest : ∀ (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS Z →
      ∀ h : Z ⟶ Y, IsLocallyOfFinitePresentation B S hS h →
        IsClosedMorphism B S hS (pullback.fst h f)) :
    UniversallyClosed B S hS f

AlgebraicGeometry.Space.universallyClosed_tfae_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/UniversallyClosedAffineSpaceTest.lean, line 463.

Stacks 0CM9. For a quasi-compact morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent: f is universally closed; the base change of f along every morphism to Y which is locally of finite presentation is closed; and there is a surjective étale morphism to Y from a presheaf represented by an object V of the site such that for every n the base change of f along affine n-space over V is closed.

The implication from the second condition to the first is the one using quasi-compactness of f, through the separation statement of Tag 0CM8.

theorem universallyClosed_tfae_of_isQuasiCompact (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsQuasiCompact B S hS f) :
    List.TFAE
      [UniversallyClosed B S hS f,
        ∀ (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS Z →
          ∀ h : Z ⟶ Y, IsLocallyOfFinitePresentation B S hS h →
            IsClosedMorphism B S hS (pullback.fst h f),
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
          IsSurjective B S hS g ∧ IsEtale B S hS g ∧
            ∀ n : ℕ, ∃ (W : BigFppfOver B S hS) (a : W ⟶ V),
              IsAffineSpaceOver B S hS V W n a ∧
                IsClosedMorphism B S hS (pullback.fst (yoneda.map a ≫ g) f)]

Tag 0CMA, a lemma

Tag 0CMA in the Stacks Project.

AlgebraicGeometry.Space.isClosedMorphism_pullback_fst_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ProperAffineSpaceTest.lean, line 90. The attribute's comment: “(1) implies (2)”.

Stacks 0CMA, (1) implies (2). The base change of a proper morphism of algebraic spaces over S along a morphism which is locally of finite presentation is closed.

A proper morphism is universally closed, so this is the corresponding implication of Tag 0CM9.

theorem isClosedMorphism_pullback_fst_of_isProper (f : X ⟶ Y) (hf : IsProper B S hS f)
    {Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hZ : IsAlgebraicSpace B S hS Z) (h : Z ⟶ Y)
    (hh : IsLocallyOfFinitePresentation B S hS h) :
    IsClosedMorphism B S hS (pullback.fst h f)

AlgebraicGeometry.Space.exists_affineSpaceTest_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ProperAffineSpaceTest.lean, line 103. The attribute's comment: “(1) implies (3)”.

Stacks 0CMA, (1) implies (3). A proper morphism of algebraic spaces over S passes the affine-space test over a surjective étale scheme atlas of its target: for every n the base change of f along affine n-space over the atlas is closed.

A proper morphism is universally closed, so this is the corresponding implication of Tag 0CM9.

theorem exists_affineSpaceTest_of_isProper (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsProper B S hS f) :
    ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
      IsSurjective B S hS g ∧ IsEtale B S hS g ∧
        ∀ n : ℕ, ∃ (W : BigFppfOver B S hS) (a : W ⟶ V), IsAffineSpaceOver B S hS V W n a ∧
          IsClosedMorphism B S hS (pullback.fst (yoneda.map a ≫ g) f)

AlgebraicGeometry.Space.isProper_of_isClosedMorphism_pullback_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ProperAffineSpaceTest.lean, line 121. The attribute's comment: “(2) implies (1)”.

Stacks 0CMA, (2) implies (1). A separated morphism of finite type between algebraic spaces over S whose base changes along the morphisms locally of finite presentation are closed is proper.

Properness is separatedness, finite type and universal closedness; the first two are the standing hypotheses and the third is supplied by Tag 0CM9, whose quasi-compactness hypothesis is the second conjunct of finite type.

theorem isProper_of_isClosedMorphism_pullback_fst (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hsep : IsSeparated B S hS f)
    (hft : IsFiniteType B S hS f)
    (htest : ∀ (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS Z →
      ∀ h : Z ⟶ Y, IsLocallyOfFinitePresentation B S hS h →
        IsClosedMorphism B S hS (pullback.fst h f)) :
    IsProper B S hS f

AlgebraicGeometry.Space.isProper_of_affineSpaceTest, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ProperAffineSpaceTest.lean, line 138. The attribute's comment: “(3) implies (1)”. References: EGA II (5.6.3), “more general”.

Stacks 0CMA, (3) implies (1). A separated morphism of finite type between algebraic spaces over S which passes the affine-space test over one surjective étale scheme atlas of its target is proper.

The affine-space test gives closedness of the base changes along the morphisms locally of finite presentation, by Tag 0CM9, and that in turn gives universal closedness.

theorem isProper_of_affineSpaceTest (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hsep : IsSeparated B S hS f)
    (hft : IsFiniteType B S hS f) (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y)
    (hgsurj : IsSurjective B S hS g) (hgetale : IsEtale B S hS g)
    (htest : ∀ n : ℕ, ∃ (W : BigFppfOver B S hS) (a : W ⟶ V), IsAffineSpaceOver B S hS V W n a ∧
      IsClosedMorphism B S hS (pullback.fst (yoneda.map a ≫ g) f)) :
    IsProper B S hS f

AlgebraicGeometry.Space.isProper_tfae_of_isSeparated_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ProperAffineSpaceTest.lean, line 160.

Stacks 0CMA. For a separated morphism f : X ⟶ Y of finite type between algebraic spaces over S the following are equivalent: f is proper; the base change of f along every morphism to Y which is locally of finite presentation is closed; and there is a surjective étale morphism to Y from a presheaf represented by an object V of the site such that for every n the base change of f along affine n-space over V is closed.

This is the special case of Tag 0CM9 obtained by unfolding properness into separatedness, finite type and universal closedness.

theorem isProper_tfae_of_isSeparated_of_isFiniteType (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hsep : IsSeparated B S hS f)
    (hft : IsFiniteType B S hS f) :
    List.TFAE
      [IsProper B S hS f,
        ∀ (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS Z →
          ∀ h : Z ⟶ Y, IsLocallyOfFinitePresentation B S hS h →
            IsClosedMorphism B S hS (pullback.fst h f),
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
          IsSurjective B S hS g ∧ IsEtale B S hS g ∧
            ∀ n : ℕ, ∃ (W : BigFppfOver B S hS) (a : W ⟶ V),
              IsAffineSpaceOver B S hS V W n a ∧
                IsClosedMorphism B S hS (pullback.fst (yoneda.map a ≫ g) f)]

Sources

• Section 70.20, Tag 0CM7
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.exists_affine_etale_isLocallyOfFinitePresentation_separation_of_isAbsolutelyQuasiSeparated · AlgebraicGeometry.Space.exists_affine_elementary_etale_separation · AlgebraicGeometry.Space.exists_isClosed_separation_of_etale_cover · AlgebraicGeometry.Space.exists_affine_etale_isLocallyOfFinitePresentation_separation · AlgebraicGeometry.Space.exists_affineOpen_isLocallyOfFinitePresentation_separation_of_lfp_morphism · AlgebraicGeometry.Space.exists_affineOpen_isLocallyOfFinitePresentation_separation · AlgebraicGeometry.Space.isClosedMorphism_pullback_fst_of_affineSpaceTest · AlgebraicGeometry.Space.isClosedMorphism_pullback_fst_of_universallyClosed

Section70.21 Noetherian valuative criterion#

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

Tag 0CMC, a lemma

Tag 0CMC in the Stacks Project.

AlgebraicGeometry.Space.exists_discreteValuationSpecialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeCriterion.lean, line 604.

Stacks 0CMC. Let f : X ⟶ Y be a morphism of finite type of algebraic spaces over S, with Y locally Noetherian, and let y be a point of Y in the closure of the image of the points of X. Then there are a discrete valuation ring A, a field-valued point of X over its fraction field K, a morphism Spec K ⟶ Spec A over S given by the inclusion A → K, and an A-valued point of Y forming a commutative square with f, the closed point of Spec A mapping to y. Moreover the point x of X given by Spec K ⟶ X is a codimension zero point; it satisfies f x ≠ y as soon as y is in the closure of the set of f x' for the codimension zero points x' of X with f x' ≠ y; and, when f x ≠ y, the morphism Spec K ⟶ X factors as Spec K ≅ Spec κ(u) ⟶ U ⟶ X for a point u of a scheme U étale over X, so that K is the residue field of u. The condition for f x ≠ y is also necessary: the square makes y a specialization of f x, so an x with f x ≠ y is itself such an x'.

The residue-field clause is stated under f x ≠ y because the source's unconditional clause is false. This is AlgebraicGeometry.Space.not_forall_exists_discreteValuationSpecialization_residueField (in StacksFrontier.AlgebraicGeometry.Spaces.NoetherianValuativeCriterionCounterexample), whose statement is the conclusion of this theorem with the guard f x ≠ y → removed from the residue-field clause (the clause guaranteeing f x ≠ y is left out, which only strengthens the refutation):

¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : X ⟶ Y), IsAlgebraicSpace B S hS X →
    IsAlgebraicSpace B S hS Y → IsFiniteType B S hS f →
    HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T) →
    ∀ y : points B S hS Y, y ∈ closure (Set.range (pointsMap B S hS X f)) →
      ∃ (A : Type u) (_ : CommRing A) (_ : IsDomain A) (_ : IsDiscreteValuationRing A)
        (K : FieldValuedPoint B S hS X) (_ : Algebra A K.carrier)
        (_ : IsFractionRing A K.carrier) (A_contained : B.Contains (Spec (.of A)))
        (s : Spec (.of A) ⟶ S) (j : K.siteObject ⟶ valuationObject B S hS A A_contained s)
        (g : yoneda.obj (valuationObject B S hS A A_contained s) ⟶ Y),
        j.left.1 = Scheme.Spec.map (CommRingCat.ofHom (algebraMap A K.carrier)).op ∧
        yoneda.map j ≫ g = yonedaEquiv.symm K.value ≫ f ∧
        pointsMap B S hS (yoneda.obj (valuationObject B S hS A A_contained s)) g
            ((schemePointRepresentative B S hS (valuationObject B S hS A A_contained s)
                (⟨IsLocalRing.maximalIdeal A, inferInstance⟩ : PrimeSpectrum A)).class B S hS
              (yoneda.obj (valuationObject B S hS A A_contained s))) = y ∧
        localRingDimension B S hS (K.class B S hS X) = 0 ∧
        ∃ (U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X)
          (u : (BigFppfOver.toScheme B S hS).obj U)
          (e : K.carrier ≃+* ((BigFppfOver.toScheme B S hS).obj U).residueField u)
          (t : K.siteObject ⟶ U),
          IsEtale B S hS a ∧
            t.left.1 = Scheme.Spec.map (CommRingCat.ofHom e.symm.toRingHom).op ≫
                ((BigFppfOver.toScheme B S hS).obj U).fromSpecResidueField u ∧
              a.app (Opposite.op K.siteObject) t = K.value

The witness is the identity of X = Y = S = Spec k for k the algebraic closure of ℚ: every residue field of a scheme étale over Spec k is algebraically closed, being a separable extension of k, while the fraction field of a discrete valuation ring is not, since a uniformizer has no square root in it. The same proof gives the stronger AlgebraicGeometry.Space.not_forall_exists_etale_residueFieldEquiv, in which K is only asked to be abstractly isomorphic to such a residue field.

theorem exists_discreteValuationSpecialization {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (X_isAlgebraicSpace : IsAlgebraicSpace B S hS X)
    (Y_isAlgebraicSpace : IsAlgebraicSpace B S hS Y) (f_finiteType : IsFiniteType B S hS f)
    (Y_locallyNoetherian :
      HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (y : points B S hS Y) (y_mem_closure : y ∈ closure (Set.range (pointsMap B S hS X f))) :
    ∃ (A : Type u) (_ : CommRing A) (_ : IsDomain A) (_ : IsDiscreteValuationRing A)
      (K : FieldValuedPoint B S hS X) (_ : Algebra A K.carrier) (_ : IsFractionRing A K.carrier)
      (A_contained : B.Contains (Spec (.of A))) (s : Spec (.of A) ⟶ S)
      (j : K.siteObject ⟶ valuationObject B S hS A A_contained s)
      (g : yoneda.obj (valuationObject B S hS A A_contained s) ⟶ Y),
      j.left.1 = Scheme.Spec.map (CommRingCat.ofHom (algebraMap A K.carrier)).op ∧
      yoneda.map j ≫ g = yonedaEquiv.symm K.value ≫ f ∧
      pointsMap B S hS (yoneda.obj (valuationObject B S hS A A_contained s)) g
          ((schemePointRepresentative B S hS (valuationObject B S hS A A_contained s)
              (⟨IsLocalRing.maximalIdeal A, inferInstance⟩ : PrimeSpectrum A)).class B S hS
            (yoneda.obj (valuationObject B S hS A A_contained s))) = y ∧
      localRingDimension B S hS (K.class B S hS X) = 0 ∧
      (y ∈ closure (pointsMap B S hS X f ''
          {x' | localRingDimension B S hS x' = 0 ∧ pointsMap B S hS X f x' ≠ y}) →
        pointsMap B S hS X f (K.class B S hS X) ≠ y) ∧
      (pointsMap B S hS X f (K.class B S hS X) ≠ y →
        ∃ (U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X)
          (u : (BigFppfOver.toScheme B S hS).obj U)
          (e : K.carrier ≃+* ((BigFppfOver.toScheme B S hS).obj U).residueField u)
          (t : K.siteObject ⟶ U),
          IsEtale B S hS a ∧
            t.left.1 = Scheme.Spec.map (CommRingCat.ofHom e.symm.toRingHom).op ≫
                ((BigFppfOver.toScheme B S hS).obj U).fromSpecResidueField u ∧
              a.app (Opposite.op K.siteObject) t = K.value)

Tag 0H1V, an equation

Tag 0H1V in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Space.ValuativeSquare, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/Criterion.lean, line 201 (StacksFrontier): “solid square”.
• AlgebraicGeometry.Space.ValuativeSquare.Lift, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/Criterion.lean, line 202 (StacksFrontier): “dotted arrow”.

Tag 0H1W, a lemma

Tag 0H1W in the Stacks Project.

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

Stacks 0H1W, (2) implies (3). Testing uniqueness of dotted arrows on all valuation rings is stronger than testing it on the discrete ones.

theorem discreteUniqueness_of_uniqueness {f : X ⟶ Y}
    (hu : ValuativeCriterion.Uniqueness f) : ValuativeCriterion.DiscreteUniqueness f

AlgebraicGeometry.Space.codimensionZeroUniqueness_of_discreteUniqueness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeSeparatedness.lean, line 140. The attribute's comment: “(3) implies (4)”.

Stacks 0H1W, (3) implies (4). Testing uniqueness of dotted arrows on all discrete valuation rings is stronger than testing it only on the diagrams whose generic arrow picks out a point of codimension zero.

theorem codimensionZeroUniqueness_of_discreteUniqueness {f : X ⟶ Y}
    (hu : ValuativeCriterion.DiscreteUniqueness f) :
    ValuativeCriterion.CodimensionZeroUniqueness f

AlgebraicGeometry.Space.discreteUniqueness_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeSeparatedness.lean, line 148. The attribute's comment: “(1) implies (3)”.

Stacks 0H1W, (1) implies (3). A separated morphism of algebraic spaces has at most one dotted arrow in every valuative diagram with a discrete valuation ring.

theorem discreteUniqueness_of_isSeparated (f : X ⟶ Y) (hf : IsSeparated B S hS f) :
    ValuativeCriterion.DiscreteUniqueness f

AlgebraicGeometry.Space.codimensionZeroUniqueness_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeSeparatedness.lean, line 156. The attribute's comment: “(1) implies (4)”.

Stacks 0H1W, (1) implies (4). A separated morphism of algebraic spaces has at most one dotted arrow in every valuative diagram with a discrete valuation ring whose generic arrow picks out a point of codimension zero.

theorem codimensionZeroUniqueness_of_isSeparated (f : X ⟶ Y) (hf : IsSeparated B S hS f) :
    ValuativeCriterion.CodimensionZeroUniqueness f

AlgebraicGeometry.Space.isSeparated_iff_valuativeCriterion_uniqueness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeSeparatedness.lean, line 163. The attribute's comment: “(1) is equivalent to (2)”.

Stacks 0H1W, (1) is equivalent to (2). A quasi-separated morphism of algebraic spaces is separated exactly when it satisfies the uniqueness part of the valuative criterion.

theorem isSeparated_iff_valuativeCriterion_uniqueness
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hqs : IsQuasiSeparated B S hS f) :
    IsSeparated B S hS f ↔ ValuativeCriterion.Uniqueness f

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

Stacks 0H1W. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is quasi-separated and locally of finite type, with Y locally Noetherian. The following are equivalent:

1. f is separated;
2. every valuative diagram for f has at most one dotted arrow;
3. every valuative diagram for f whose valuation ring is a discrete valuation ring has at most one dotted arrow;
4. every valuative diagram for f whose valuation ring is a discrete valuation ring and whose generic arrow picks out a point of codimension zero of X has at most one dotted arrow.

theorem isSeparated_tfae_of_isLocallyOfFiniteType
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hqs : IsQuasiSeparated B S hS f) (hlft : IsLocallyOfFiniteType B S hS f)
    (hnoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T)) :
    List.TFAE
      [ IsSeparated B S hS f,
        ValuativeCriterion.Uniqueness f,
        ValuativeCriterion.DiscreteUniqueness f,
        ValuativeCriterion.CodimensionZeroUniqueness f ]

Tag 0H1X, a lemma

Tag 0H1X in the Stacks Project.

AlgebraicGeometry.Space.isProper_tfae_of_isQuasiSeparated_of_codimensionZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeProperCodimensionZero.lean, line 496.

Stacks 0H1X. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is quasi-separated and of finite type, with Y locally Noetherian. The following are equivalent: 1. f is proper; 2. f satisfies the valuative criterion (Stacks 03IX); 3. every valuative diagram (Stacks 0H1V) for f has exactly one dotted arrow; 4. every valuative diagram for f whose valuation ring is a discrete valuation ring has exactly one dotted arrow; 5. every valuative diagram for f whose valuation ring is a discrete valuation ring and whose generic arrow Spec K ⟶ X picks out a point of codimension zero of X has exactly one dotted arrow.

Conditions (1) to (3) are equivalent by Stacks 0A40, and (3) implies (4) implies (5) trivially. Given (5), f is separated by Stacks 0H1W (AlgebraicGeometry.Space.isSeparated_of_isLocallyOfFiniteType_of_codimensionZeroUniqueness) and universally closed by AlgebraicGeometry.Space.universallyClosed_of_codimensionZeroValuativeExistence.

theorem isProper_tfae_of_isQuasiSeparated_of_codimensionZero
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hqs : IsQuasiSeparated B S hS f) (hft : IsFiniteType B S hS f)
    (hNoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T)) :
    List.TFAE
      [ IsProper B S hS f,
        ValuativeCriterion f,
        ∀ q : ValuativeSquare f, Nonempty q.Lift ∧ Subsingleton q.Lift,
        ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          Nonempty q.Lift ∧ Subsingleton q.Lift,
        ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          localRingDimension B S hS q.genericPoint = 0 →
            Nonempty q.Lift ∧ Subsingleton q.Lift ]

Tag 0H1Y, a lemma

Tag 0H1Y in the Stacks Project.

AlgebraicGeometry.Space.universallyClosed_tfae_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianUniversallyClosed.lean, line 417. The attribute's comment: “for f decent (e.g. quasi-separated); without decency the statement is false, see not_forall_universallyClosed_tfae_of_isLocallyNoetherian”.

Stacks 0H1Y. Let f : X ⟶ Y be a decent morphism of finite type of algebraic spaces over S, with Y locally Noetherian; for instance f quasi-separated. The following are equivalent:

1. f is universally closed;
2. f satisfies the existence part of the valuative criterion;
3. there are an object V of the site and a surjective étale morphism V ⟶ Y such that for every n the base change of f to affine n-space over V is closed;
4. every valuative square for f whose valuation ring is a discrete valuation ring acquires a dotted arrow after a finite separable extension of the fraction field and passage to a dominating discrete valuation ring;
5. every valuative square for f whose valuation ring is a discrete valuation ring acquires a dotted arrow after an extension of the fraction field and passage to a dominating valuation ring.

The source omits decency, and without it the statement is false. This is AlgebraicGeometry.Space.not_forall_universallyClosed_tfae_of_isLocallyNoetherian (in StacksFrontier.AlgebraicGeometry.Spaces.NoetherianUniversallyClosedCounterexample), whose statement is this theorem with the hypothesis IsDecent B S hS f removed:

¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS X →
    IsAlgebraicSpace B S hS Y → ∀ f : X ⟶ Y, IsFiniteType B S hS f →
    HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T) →
    List.TFAE
      [UniversallyClosed B S hS f,
        ValuativeCriterion.Existence f,
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
          IsSurjective B S hS g ∧ IsEtale B S hS g ∧
            ∀ n : ℕ, ∃ (W : BigFppfOver B S hS) (a : W ⟶ V),
              IsAffineSpaceOver B S hS V W n a ∧
                IsClosedMorphism B S hS (pullback.fst (yoneda.map a ≫ g) f),
        ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          ∃ e : q.DominatingExtension,
            IsDiscreteValuationRing e.square.R ∧
              (letI := e.fieldMap.toAlgebra
               Module.Finite q.K e.square.K ∧ Algebra.IsSeparable q.K e.square.K) ∧
              Nonempty e.square.Lift,
        ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          ∃ e : q.DominatingExtension, Nonempty e.square.Lift]

The witness is the structure morphism 𝔸¹_ℚ/ℤ ⟶ Spec ℚ of the quotient of the affine line by the integer translations: it is of finite type over the Noetherian scheme Spec ℚ and universally closed (Stacks 03IV), but the ℚ((t))-point 1/t extends to no valuation ring dominating ℚ[[t]], so (1) holds and (2) fails. With decency, (1) implies (2) by Stacks 03M6, f being quasi-compact as it is of finite type.

theorem universallyClosed_tfae_of_isLocallyNoetherian {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X_alg : IsAlgebraicSpace B S hS X) (Y_alg : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (decent : IsDecent B S hS f) (ft : IsFiniteType B S hS f)
    (noeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T)) :
    List.TFAE
      [UniversallyClosed B S hS f,
        ValuativeCriterion.Existence f,
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
          IsSurjective B S hS g ∧ IsEtale B S hS g ∧
            ∀ n : ℕ, ∃ (W : BigFppfOver B S hS) (a : W ⟶ V),
              IsAffineSpaceOver B S hS V W n a ∧
                IsClosedMorphism B S hS (pullback.fst (yoneda.map a ≫ g) f),
        ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          ∃ e : q.DominatingExtension,
            IsDiscreteValuationRing e.square.R ∧
              (letI := e.fieldMap.toAlgebra
               Module.Finite q.K e.square.K ∧ Algebra.IsSeparable q.K e.square.K) ∧
              Nonempty e.square.Lift,
        ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          ∃ e : q.DominatingExtension, Nonempty e.square.Lift]

AlgebraicGeometry.Space.universallyClosed_implications_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianUniversallyClosedImplications.lean, line 107. References: EGA II (7.3.8), “(b) ⇒ (a)”.

Stacks 0H1Y, the implications that hold without decency. Let f : X ⟶ Y be a morphism of finite type of algebraic spaces over S, with Y locally Noetherian. Number the conditions of Stacks 0H1Y as follows:

1. f is universally closed;
2. f satisfies the existence part of the valuative criterion;
3. there are an object V of the site and a surjective étale morphism V ⟶ Y such that for every n the base change of f to affine n-space over V is closed;
4. every valuative square for f whose valuation ring is a discrete valuation ring acquires a dotted arrow after a finite separable extension of the fraction field and passage to a dominating discrete valuation ring;
5. every valuative square for f whose valuation ring is a discrete valuation ring acquires a dotted arrow after an extension of the fraction field and passage to a dominating valuation ring.

Then (2) ⇒ (4), (4) ⇒ (5), (5) ⇒ (1) and (1) ⇔ (3); in particular (2) ⇒ (1).

Correction. The source asserts that the five conditions are equivalent under these hypotheses alone, which is false: (1) ⇒ (2) fails for the structure morphism 𝔸¹_ℚ/ℤ ⟶ Spec ℚ, which is of finite type and universally closed (Stacks 03IV) but does not satisfy the existence part of the valuative criterion (Stacks section 03K9); see not_forall_universallyClosed_tfae_of_isLocallyNoetherian. The source's proof derives (1) ⇔ (2) from Stacks 03KA, which only gives (2) ⇒ (1). Every other implication of the source holds as stated, and they are the ones asserted here. The equivalence of all five conditions for f decent is universallyClosed_implications_and_tfae_of_isLocallyNoetherian.

The proof follows the source: (1) ⇔ (3) is Stacks 0CM9 (f is quasi-compact, being of finite type), (2) ⇒ (4) is Stacks 03KH with Krull–Akizuki (Stacks 00PG), (4) ⇒ (5) is immediate, and (5) ⇒ (1) reduces to closedness over a Noetherian affine base by Stacks 0CMC.

theorem universallyClosed_implications_of_isLocallyNoetherian
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X_alg : IsAlgebraicSpace B S hS X) (Y_alg : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (ft : IsFiniteType B S hS f)
    (noeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T)) :
    (ValuativeCriterion.Existence f →
        ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          ∃ e : q.DominatingExtension,
            IsDiscreteValuationRing e.square.R ∧
              (letI := e.fieldMap.toAlgebra
               Module.Finite q.K e.square.K ∧ Algebra.IsSeparable q.K e.square.K) ∧
              Nonempty e.square.Lift) ∧
      ((∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          ∃ e : q.DominatingExtension,
            IsDiscreteValuationRing e.square.R ∧
              (letI := e.fieldMap.toAlgebra
               Module.Finite q.K e.square.K ∧ Algebra.IsSeparable q.K e.square.K) ∧
              Nonempty e.square.Lift) →
        ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          ∃ e : q.DominatingExtension, Nonempty e.square.Lift) ∧
      ((∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          ∃ e : q.DominatingExtension, Nonempty e.square.Lift) →
        UniversallyClosed B S hS f) ∧
      (UniversallyClosed B S hS f ↔
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
          IsSurjective B S hS g ∧ IsEtale B S hS g ∧
            ∀ n : ℕ, ∃ (W : BigFppfOver B S hS) (a : W ⟶ V),
              IsAffineSpaceOver B S hS V W n a ∧
                IsClosedMorphism B S hS (pullback.fst (yoneda.map a ≫ g) f))

AlgebraicGeometry.Space.universallyClosed_implications_and_tfae_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianUniversallyClosedImplications.lean, line 172.

Stacks 0H1Y, corrected. Let f : X ⟶ Y be a morphism of finite type of algebraic spaces over S, with Y locally Noetherian, and number the conditions of Stacks 0H1Y as in universallyClosed_implications_of_isLocallyNoetherian:

1. f is universally closed;
2. f satisfies the existence part of the valuative criterion;
3. there are an object V of the site and a surjective étale morphism V ⟶ Y such that for every n the base change of f to affine n-space over V is closed;
4. every valuative square for f whose valuation ring is a discrete valuation ring acquires a dotted arrow after a finite separable extension of the fraction field and passage to a dominating discrete valuation ring;
5. every valuative square for f whose valuation ring is a discrete valuation ring acquires a dotted arrow after an extension of the fraction field and passage to a dominating valuation ring.

Then (2) ⇒ (4) ⇒ (5) ⇒ (1) ⇔ (3), and if f is decent (for instance quasi-separated) the five conditions are equivalent.

Correction. The source asserts the equivalence of the five conditions with no hypothesis on f beyond finite type. That is false, by not_forall_universallyClosed_tfae_of_isLocallyNoetherian: the structure morphism 𝔸¹_ℚ/ℤ ⟶ Spec ℚ of the quotient of the affine line by the integer translations is of finite type over a Noetherian scheme and universally closed (Stacks 03IV), but the ℚ((t))-point 1/t extends to no valuation ring dominating ℚ[[t]], so (1) holds and (2) fails; that morphism is not decent. The faulty step is the source's appeal to Stacks 03KA for (1) ⇔ (2): Stacks 03KA only gives (2) ⇒ (1), and the converse needs decency (Stacks 03M6, f being quasi-compact as it is of finite type) or quasi-separatedness (Stacks 0A3X). So decency is assumed exactly for the full equivalence, which is universallyClosed_tfae_of_isLocallyNoetherian, and the remaining implications are stated without it, as in universallyClosed_implications_of_isLocallyNoetherian.

theorem universallyClosed_implications_and_tfae_of_isLocallyNoetherian
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X_alg : IsAlgebraicSpace B S hS X) (Y_alg : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (ft : IsFiniteType B S hS f)
    (noeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T)) :
    ((ValuativeCriterion.Existence f →
        ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          ∃ e : q.DominatingExtension,
            IsDiscreteValuationRing e.square.R ∧
              (letI := e.fieldMap.toAlgebra
               Module.Finite q.K e.square.K ∧ Algebra.IsSeparable q.K e.square.K) ∧
              Nonempty e.square.Lift) ∧
      ((∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          ∃ e : q.DominatingExtension,
            IsDiscreteValuationRing e.square.R ∧
              (letI := e.fieldMap.toAlgebra
               Module.Finite q.K e.square.K ∧ Algebra.IsSeparable q.K e.square.K) ∧
              Nonempty e.square.Lift) →
        ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          ∃ e : q.DominatingExtension, Nonempty e.square.Lift) ∧
      ((∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
          ∃ e : q.DominatingExtension, Nonempty e.square.Lift) →
        UniversallyClosed B S hS f) ∧
      (UniversallyClosed B S hS f ↔
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
          IsSurjective B S hS g ∧ IsEtale B S hS g ∧
            ∀ n : ℕ, ∃ (W : BigFppfOver B S hS) (a : W ⟶ V),
              IsAffineSpaceOver B S hS V W n a ∧
                IsClosedMorphism B S hS (pullback.fst (yoneda.map a ≫ g) f))) ∧
    (IsDecent B S hS f →
      List.TFAE
        [UniversallyClosed B S hS f,
          ValuativeCriterion.Existence f,
          ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
            IsSurjective B S hS g ∧ IsEtale B S hS g ∧
              ∀ n : ℕ, ∃ (W : BigFppfOver B S hS) (a : W ⟶ V),
                IsAffineSpaceOver B S hS V W n a ∧
                  IsClosedMorphism B S hS (pullback.fst (yoneda.map a ≫ g) f),
          ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
            ∃ e : q.DominatingExtension,
              IsDiscreteValuationRing e.square.R ∧
                (letI := e.fieldMap.toAlgebra
                 Module.Finite q.K e.square.K ∧ Algebra.IsSeparable q.K e.square.K) ∧
                Nonempty e.square.Lift,
          ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
            ∃ e : q.DominatingExtension, Nonempty e.square.Lift])

Sources

• Section 70.21, Tag 0CMB
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.exists_discreteValuationSpecialization · AlgebraicGeometry.Space.ValuativeSquare · AlgebraicGeometry.Space.ValuativeSquare.Lift · AlgebraicGeometry.Space.discreteUniqueness_of_uniqueness · AlgebraicGeometry.Space.codimensionZeroUniqueness_of_discreteUniqueness · AlgebraicGeometry.Space.discreteUniqueness_of_isSeparated · AlgebraicGeometry.Space.codimensionZeroUniqueness_of_isSeparated · AlgebraicGeometry.Space.isSeparated_iff_valuativeCriterion_uniqueness

Section70.22 Refined Noetherian valuative criteria#

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

Tag 0CMD, a lemma

Tag 0CMD in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Space.isProper_of_denseRange_of_exists_discreteLift, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/NoetherianRefinedValuativeCriterion.lean, line 499 (StacksFrontier): “Let f : X ⟶ Y and h : U ⟶ X be morphisms of algebraic spaces over S, with Y locally Noetherian, f and h of finite type, f separated and the image of |h| : |U| → |X| dense in |X|. If every commutative valuative diagram for f over a discrete valuation ring whose generic arrow factors through h has a dotted arrow, then f is proper.”.

Tag 0CME, a lemma

Tag 0CME in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_of_denseRange_of_subsingleton_discreteLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RefinedValuativeSeparatedness.lean, line 416.

Stacks 0CME. Let f : X ⟶ Y and h : U ⟶ X be morphisms of algebraic spaces over S with Y locally Noetherian, f locally of finite type and quasi-separated, h of finite type and the image of |h| : |U| → |X| dense in |X|. If every commutative valuative diagram for f over a discrete valuation ring A with fraction field K whose generic arrow Spec K ⟶ X factors through h has at most one dotted arrow Spec A ⟶ X, then f is separated.

The relative diagonal of f is representable, a monomorphism, separated, locally of finite type, and quasi-compact because f is quasi-separated. Its base change V ⟶ C along an étale chart C of the locally Noetherian algebraic space X ×_Y X (Stacks 04ZK) is therefore a quasi-compact monomorphism of schemes locally of finite type over a locally Noetherian scheme, and it satisfies condition (4) of Stacks 0208: at a generic point of V a dotted arrow exists by nonempty_liftStruct_of_denseRange, and it is unique since V ⟶ C is a monomorphism. So V ⟶ C is proper (Stacks 0208), hence a closed immersion (Stacks 04XV), and being a closed immersion descends from the chart to the diagonal (Stacks 02L6, 02WZ).

theorem isSeparated_of_denseRange_of_subsingleton_discreteLift
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hU : IsAlgebraicSpace B S hS U) (f : X ⟶ Y) (h : U ⟶ X)
    (hnoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hlft : IsLocallyOfFiniteType B S hS f) (hqs : IsQuasiSeparated B S hS f)
    (hh : IsFiniteType B S hS h)
    (hdense : @DenseRange _ (pointTopology B S hS X) _ (pointsMap B S hS U h))
    (hvaluative : ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
      ∀ g : yoneda.obj (siteObject B S hS q.field_mem
          (Spec.map (CommRingCat.ofHom (algebraMap q.R q.K)) ≫ q.base)) ⟶ U,
        g ≫ h = q.generic → Subsingleton q.Lift) :
    IsSeparated B S hS f

Tag 0CMF, a lemma

Tag 0CMF in the Stacks Project.

AlgebraicGeometry.Space.isProper_of_denseRange_of_unique_discreteLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RefinedValuativeProperness.lean, line 540.

Stacks 0CMF. Let f : X ⟶ Y and h : U ⟶ X be morphisms of algebraic spaces over S with Y locally Noetherian, f and h of finite type, f quasi-separated and the image of |h| : |U| → |X| dense in |X|. If every commutative valuative diagram for f over a discrete valuation ring A with fraction field K whose generic arrow Spec K ⟶ X factors through h has exactly one dotted arrow Spec A ⟶ X, then f is proper.

As in the source this combines Stacks 0CME, which gives separatedness of f from the uniqueness of the dotted arrows, with Stacks 0CMD, which gives properness from their existence.

theorem isProper_of_denseRange_of_unique_discreteLift
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hU : IsAlgebraicSpace B S hS U) (f : X ⟶ Y) (h : U ⟶ X)
    (hnoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hft : IsFiniteType B S hS f) (hh : IsFiniteType B S hS h) (hqs : IsQuasiSeparated B S hS f)
    (hdense : @DenseRange _ (pointTopology B S hS X) _ (pointsMap B S hS U h))
    (hvaluative : ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
      ∀ g : yoneda.obj (siteObject B S hS q.field_mem
          (Spec.map (CommRingCat.ofHom (algebraMap q.R q.K)) ≫ q.base)) ⟶ U,
        g ≫ h = q.generic → Nonempty q.Lift ∧ Subsingleton q.Lift) :
    IsProper B S hS f

Sources

• Section 70.22, Tag 0H1Z
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isProper_of_denseRange_of_exists_discreteLift · AlgebraicGeometry.Space.isSeparated_of_denseRange_of_subsingleton_discreteLift · AlgebraicGeometry.Space.isProper_of_denseRange_of_unique_discreteLift

Section70.23 Descending finite type spaces#

Section 70.23 of the Stacks Project, Tag 0CP5. 11 tags here are carried by 13 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CP5, the section

Tag 0CP5 in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Space.NoetherianLimitSystem, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeSection.lean, line 43 (StacksFrontier): “the situation”.
• AlgebraicGeometry.Space.GoodDiagram, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeSection.lean, line 44 (StacksFrontier): “the diagram”.
• AlgebraicGeometry.Space.GoodDiagram.isLimit_imageCone, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeSection.lean, line 45 (StacksFrontier): “X is the limit of its scheme-theoretic images”.
• AlgebraicGeometry.Space.GoodDiagram.exists_systemMorphism, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeSection.lean, line 47 (StacksFrontier): “morphisms descend to the systems of images”.
• AlgebraicGeometry.Space.GoodDiagram.eventually_eq_systemMorphism, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeSection.lean, line 49 (StacksFrontier): “eventual uniqueness of the descended morphisms”.
• AlgebraicGeometry.Space.GoodDiagram.SystemMorphism.exists_isFlat_isPullback, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeSection.lean, line 51 (StacksFrontier): “flatness descends”.
• AlgebraicGeometry.Space.GoodDiagram.SystemMorphism.exists_isSmooth, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeSection.lean, line 53 (StacksFrontier): “smoothness descends”.

Tag 0CP6, a situation

Tag 0CP6 in the Stacks Project.

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

Stacks 0CP6. A directed inverse system (B_i)_{i ∈ I} of Noetherian algebraic spaces over a scheme S with affine transition morphisms B_{i'} ⟶ B_i for i ≤ i'. Its limit B = lim_i B_i is AlgebraicGeometry.Space.NoetherianSpaceSystem.limit, an algebraic space by AlgebraicGeometry.Space.NoetherianSpaceSystem.isAlgebraicSpace_limit (Stacks 07SF).

The field indexSize is the chapter's standing convention (Stacks 07SD) that the rings it considers have their spectra in the site, stated for the fixed size cutoff of the site.

structure NoetherianSpaceSystem (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hZ : B.Contains (⊤_ Scheme.{u})) (I : Type u) [Preorder I] [Nonempty I]
    [IsDirected I (· ≤ ·)]

AlgebraicGeometry.Space.NoetherianLimitSystem, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/NoetherianSystem.lean, line 55.

Stacks 0CP6. A directed inverse system of Noetherian algebraic spaces over a scheme S with affine transition morphisms, equipped with a chosen limiting cone whose point is again an algebraic space.

structure NoetherianLimitSystem (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hZ : B.Contains (⊤_ Scheme.{u})) (I : Type v) [Preorder I] [Nonempty I]
    [IsDirected I (· ≤ ·)]

Tag 0CP7, a lemma

Tag 0CP7 in the Stacks Project.

AlgebraicGeometry.Space.NoetherianLimitSystem.nonempty_goodDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/GoodDiagramExistenceUnconditional.lean, line 69.

Stacks 0CP7. In Situation 0CP6, let f : X ⟶ B be a quasi-separated morphism of finite type of algebraic spaces over S. Then there are a stage i, an algebraic space W with a morphism W ⟶ B_i of finite type, and a morphism X ⟶ W over B ⟶ B_i, such that the induced morphism X ⟶ B ×_{B_i} W is a closed immersion: a diagram as in Stacks 0CP8.

theorem nonempty_goodDiagram (D : NoetherianLimitSystem B S hS hZ I)
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ D.limitCone.pt)
    (hX : IsAlgebraicSpace B S hS X) (hfqs : IsQuasiSeparated B S hS f)
    (hfft : IsFiniteType B S hS f) :
    Nonempty (GoodDiagram B S hS hZ D f)

Tag 0CP8, an equation

Tag 0CP8 in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Space.GoodDiagram, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeSection.lean, line 40 (StacksFrontier): “the diagram: X ⟶ W over B ⟶ B_i, W ⟶ B_i of finite type and X ⟶ B ×_{B_i} W a closed immersion”.

Tag 0CP9, a lemma

Tag 0CP9 in the Stacks Project.

AlgebraicGeometry.Space.GoodDiagram.mono_lift_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeLimit.lean, line 381. The attribute's comment: “X is a subspace of the limit: the cone to the images is jointly monic”.

The monomorphism half of Stacks 0CP9. In Situation 0CP6, for a diagram as in Stacks 0CP8, the space X is a subspace of the limit of the inverse system of the scheme-theoretic images X_{i'} of X ⟶ B_{i'} ×_{B_i} W: the comparison morphism from X to the vertex of any limiting cone on that system is a monomorphism.

The remaining half, that the comparison morphism is an isomorphism, is not proved; by AlgebraicGeometry.Space.GoodDiagram.nonempty_isLimit_imageCone_iff it is equivalent to the inclusion imageInter G ≤ Subfunctor.range G.induced of subfunctors of B ×_{B_i} W.

theorem mono_lift_of_isLimit (G : GoodDiagram B S hS hZ D f) {c : Cone (imageSystem G)}
    (hc : IsLimit c) : Mono (hc.lift (imageCone G))

AlgebraicGeometry.Space.GoodDiagram.isLimit_imageCone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeLimitImage.lean, line 765. The attribute's comment: “X = lim X_{i'}, for an index type small for the site”.

Stacks 0CP9. In Situation 0CP6, for a diagram as in Stacks 0CP8, the canonical cone from X to the inverse system of the scheme-theoretic images X_{i'} of X ⟶ B_{i'} ×_{B_i} W is a limit cone: X = lim_{i' ≥ i} X_{i'}.

By AlgebraicGeometry.Space.GoodDiagram.nonempty_isLimit_imageCone_iff this is the single inclusion AlgebraicGeometry.Space.GoodDiagram.imageInter_le_range_induced of subfunctors of B ×_{B_i} W. The hypothesis that the index type of the system be small for the site is what produces the limit of the system of affine charts used there; it is not a hypothesis of the source.

noncomputable def isLimit_imageCone (hX : IsAlgebraicSpace B S hS X)
    (hSize : Cardinal.mk I < B.cutoff.ord.cof) : IsLimit (imageCone G)

Tag 0CPA, a lemma

Tag 0CPA in the Stacks Project.

AlgebraicGeometry.Space.GoodDiagram.exists_systemMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeMorphism.lean, line 335. The attribute's comment: “existence”.

Stacks 0CPA, existence. In Situation 0CP6, let f : X ⟶ Y be a morphism of algebraic spaces over B with X quasi-separated over B, and let GX and GY be diagrams as in Stacks 0CP8 for X and for Y. Then some stage i₀ above the indices of both diagrams carries a morphism of the inverse systems of scheme-theoretic images on the tail above i₀, over the system (B_i)_{i ≥ i₀}, whose limit is f.

The model V ⟶ B_{i₂} of GY is locally of finite presentation, so the composite X ⟶ Y ⟶ V is defined over a stage X_{i₀} ⟶ V by the surjectivity half of the limit criterion for morphisms out of an inverse limit; the components of the system morphism are the factorizations through the scheme-theoretic images Y_i supplied by AlgebraicGeometry.Space.GoodDiagram.exists_comp_stageImage_ι. The two hypotheses hX and hSize are those of the library's Stacks 0CP9.

theorem exists_systemMorphism (hX : IsAlgebraicSpace B S hS X)
    (hXqs : IsQuasiSeparated B S hS pX) (hSize : Cardinal.mk I < B.cutoff.ord.cof)
    (f : X ⟶ Y) (hf : f ≫ pY = pX) (GX : GoodDiagram B S hS hZ D pX)
    (GY : GoodDiagram B S hS hZ D pY) :
    ∃ (i₀ : I) (hiX : GX.index ≤ i₀) (hiY : GY.index ≤ i₀),
      Nonempty (SystemMorphism GX GY f i₀ hiX hiY)

AlgebraicGeometry.Space.GoodDiagram.eventually_eq_systemMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeMorphism.lean, line 419. The attribute's comment: “eventual uniqueness”.

Stacks 0CPA, eventual uniqueness. Two morphisms of the inverse systems of scheme-theoretic images on the tail above a stage i₀, both inducing the same morphism f : X ⟶ Y in the limit, have the same component at every sufficiently late stage.

Their components at the initial stage agree after composing with the projection X ⟶ X_{i₀}, by the two compatibilities with the canonical cones, and after composing with the model V ⟶ B_{i₂}, by the two equations over the base; so the injectivity half of the limit criterion for morphisms out of an inverse limit makes them agree after one transition morphism, and naturality propagates that to all later stages. The source's equalizer argument is not used.

theorem eventually_eq_systemMorphism (hX : IsAlgebraicSpace B S hS X)
    (hXqs : IsQuasiSeparated B S hS pX) (hSize : Cardinal.mk I < B.cutoff.ord.cof)
    {GX : GoodDiagram B S hS hZ D pX} {GY : GoodDiagram B S hS hZ D pY} {f : X ⟶ Y}
    {i₀ : I} {hiX : GX.index ≤ i₀} {hiY : GY.index ≤ i₀}
    (F G : SystemMorphism GX GY f i₀ hiX hiY) :
    ∃ i₃ : I, i₀ ≤ i₃ ∧ ∀ j : Over (op i₀), i₃ ≤ j.left.unop →
      F.maps.app j = G.maps.app j

Tag 0CPB, a remark

Tag 0CPB in the Stacks Project.

AlgebraicGeometry.Space.NoetherianLimitSystem.isEquivalence_limitFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeEquivalence.lean, line 464. The attribute's comment: “the category of algebraic spaces quasi-separated and of finite type over B is equivalent to the category of the inverse systems over (B_i) that 0CP9 produces from the diagrams (0CP8), up to shrinking the index set”.

Stacks 0CPB. In Situation 0CP6, the category of algebraic spaces quasi-separated and of finite type over B = lim B_i is equivalent to the category of the inverse systems of algebraic spaces over (B_i) produced by Stacks 0CP9 from a diagram as in Stacks 0CP8, whose morphisms are the morphisms of inverse systems over (B_i) on a tail of the index set, up to shrinking the index set. The equivalence takes a system to its limit: it is essentially surjective by Stacks 0CP7, full by the existence half and faithful by the uniqueness half of Stacks 0CPA.

theorem isEquivalence_limitFunctor : (limitFunctor D).IsEquivalence

AlgebraicGeometry.Space.NoetherianLimitSystem.exists_iso_imageSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeEquivalence.lean, line 500. The attribute's comment: “the example: two limit descriptions of X are canonically isomorphic, after shrinking the index set”.

Stacks 0CPB, the example. Let X be an algebraic space quasi-separated and of finite type over B, and let X ⟶ W₁ ⟶ B_{i₁} and X ⟶ W₂ ⟶ B_{i₂} be two diagrams as in Stacks 0CP8. Then, up to shrinking the index set to the stages above some i₀, the corresponding limit descriptions X = lim X_{1,i} and X = lim X_{2,i} of Stacks 0CP9 are isomorphic: there is an isomorphism of inverse systems (X_{1,i})_{i ≥ i₀} ≅ (X_{2,i})_{i ≥ i₀} over (B_i)_{i ≥ i₀}, compatible in both directions with the maps from X, that is, with limit id_X. The isomorphism is canonical: every morphism of the two systems over (B_i) on any tail whose limit is id_X agrees with it at all sufficiently late stages.

It is obtained by applying Stacks 0CPA to id_X in both directions: existence gives the two morphisms of systems, and uniqueness shows that their composites agree with the identities at late stages.

theorem exists_iso_imageSystem (U : FiniteTypeSpaces D)
    (G₁ G₂ : GoodDiagram B S hS hZ D U.obj.hom) :
    ∃ (i₀ : I) (h₁ : G₁.index ≤ i₀) (h₂ : G₂.index ≤ i₀)
      (e : Over.map (homOfLE h₁).op ⋙ GoodDiagram.imageSystem G₁ ≅
        Over.map (homOfLE h₂).op ⋙ GoodDiagram.imageSystem G₂),
      (∀ j : Over (op i₀),
        e.hom.app j ≫ (GoodDiagram.stageImage G₂ ((Over.map (homOfLE h₂).op).obj j)).ι ≫
            pullback.fst _ _ =
          (GoodDiagram.stageImage G₁ ((Over.map (homOfLE h₁).op).obj j)).ι ≫ pullback.fst _ _) ∧
      (∀ j : Over (op i₀),
        e.inv.app j ≫ (GoodDiagram.stageImage G₁ ((Over.map (homOfLE h₁).op).obj j)).ι ≫
            pullback.fst _ _ =
          (GoodDiagram.stageImage G₂ ((Over.map (homOfLE h₂).op).obj j)).ι ≫ pullback.fst _ _) ∧
      (∀ j : Over (op i₀),
        (GoodDiagram.imageCone G₁).π.app ((Over.map (homOfLE h₁).op).obj j) ≫ e.hom.app j =
          (GoodDiagram.imageCone G₂).π.app ((Over.map (homOfLE h₂).op).obj j)) ∧
      (∀ j : Over (op i₀),
        (GoodDiagram.imageCone G₂).π.app ((Over.map (homOfLE h₂).op).obj j) ≫ e.inv.app j =
          (GoodDiagram.imageCone G₁).π.app ((Over.map (homOfLE h₁).op).obj j)) ∧
      ∀ (i₁ : I) (k₁ : G₁.index ≤ i₁) (k₂ : G₂.index ≤ i₁)
        (F : GoodDiagram.SystemMorphism G₁ G₂ (𝟙 U.obj.left) i₁ k₁ k₂),
        ∃ (i₃ : I) (hi₀ : i₀ ≤ i₃) (hi₁ : i₁ ≤ i₃), ∀ (i : I) (hi : i₃ ≤ i),
          F.maps.app (Over.mk (homOfLE (hi₁.trans hi)).op) =
            e.hom.app (Over.mk (homOfLE (hi₀.trans hi)).op)

Tag 0CPC, a lemma

Tag 0CPC in the Stacks Project.

AlgebraicGeometry.Space.GoodDiagram.SystemMorphism.exists_isFlat_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/FlatImageSystem.lean, line 994.

In Situation 0CP6, let f : X ⟶ Y be a morphism of algebraic spaces quasi-separated over B, let GX and GY be diagrams as in Stacks 0CP8 for X and Y, and let (f_i)_{i ≥ i₀} be a morphism of the inverse systems of scheme-theoretic images X = lim X_i and Y = lim Y_i whose limit is f, as in Stacks 0CPA. If f is flat and of finite presentation, then there is a stage i₃ ≥ i₀ such that for every k ≥ i₃ the morphism f_k is flat, X = Y ×_{Y_k} X_k, and X_i = Y_i ×_{Y_k} X_k for every i ≥ k.

theorem exists_isFlat_isPullback (algX : IsAlgebraicSpace B S hS X)
    (algY : IsAlgebraicSpace B S hS Y) (qsX : IsQuasiSeparated B S hS pX)
    (qsY : IsQuasiSeparated B S hS pY) (small : Cardinal.mk I < B.cutoff.ord.cof)
    {GX : GoodDiagram B S hS hZ D pX} {GY : GoodDiagram B S hS hZ D pY} {f : X ⟶ Y}
    {i₀ : I} {leX : GX.index ≤ i₀} {leY : GY.index ≤ i₀}
    (F : SystemMorphism GX GY f i₀ leX leY)
    (flat : IsFlat B S hS f) (fp : IsFinitePresentation B S hS f) :
    ∃ i₃ : I, i₀ ≤ i₃ ∧ ∀ k : Over (op i₀), i₃ ≤ k.left.unop →
      IsFlat B S hS (F.maps.app k) ∧
      IsPullback ((imageCone GX).π.app ((Over.map (homOfLE leX).op).obj k)) f
        (F.maps.app k) ((imageCone GY).π.app ((Over.map (homOfLE leY).op).obj k)) ∧
      ∀ (j : Over (op i₀)) (a : j ⟶ k),
        IsPullback ((imageSystem GX).map ((Over.map (homOfLE leX).op).map a)) (F.maps.app j)
          (F.maps.app k) ((imageSystem GY).map ((Over.map (homOfLE leY).op).map a))

Tag 0CPD, a lemma

Tag 0CPD in the Stacks Project.

AlgebraicGeometry.Space.GoodDiagram.SystemMorphism.exists_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeSmooth.lean, line 203.

Stacks 0CPD. In Situation 0CP6, let f : X ⟶ Y be a morphism of algebraic spaces quasi-separated over B, let GX and GY be diagrams as in Stacks 0CP8 for X and Y, and let (f_i)_{i ≥ i₀} be a morphism of the inverse systems of scheme-theoretic images X = lim X_i and Y = lim Y_i whose limit is f, as in Stacks 0CPA. If f is smooth, then there is a stage i₃ ≥ i₀ such that f_i is smooth for every i ≥ i₃.

theorem exists_isSmooth (algX : IsAlgebraicSpace B S hS X)
    (algY : IsAlgebraicSpace B S hS Y) (qsX : IsQuasiSeparated B S hS pX)
    (qsY : IsQuasiSeparated B S hS pY) (small : Cardinal.mk I < B.cutoff.ord.cof)
    {GX : GoodDiagram B S hS hZ D pX} {GY : GoodDiagram B S hS hZ D pY} {f : X ⟶ Y}
    {i₀ : I} {leX : GX.index ≤ i₀} {leY : GY.index ≤ i₀}
    (F : SystemMorphism GX GY f i₀ leX leY) (smooth : IsSmooth B S hS f) :
    ∃ i₃ : I, i₀ ≤ i₃ ∧ ∀ k : Over (op i₀), i₃ ≤ k.left.unop →
      IsSmooth B S hS (F.maps.app k)

Tag 0CPE, a lemma

Tag 0CPE in the Stacks Project.

AlgebraicGeometry.Space.GoodDiagram.SystemMorphism.exists_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeProper.lean, line 395.

Stacks 0CPE. In Situation 0CP6, let f : X ⟶ Y be a morphism of algebraic spaces quasi-separated over B, let GX and GY be diagrams as in Stacks 0CP8 for X and Y, and let (f_i)_{i ≥ i₀} be a morphism of the inverse systems of scheme-theoretic images X = lim X_i and Y = lim Y_i whose limit is f, as in Stacks 0CPA. If f is proper, then there is a stage i₃ ≥ i₀ such that f_i is proper for every i ≥ i₃.

theorem exists_isProper (algX : IsAlgebraicSpace B S hS X)
    (algY : IsAlgebraicSpace B S hS Y) (qsX : IsQuasiSeparated B S hS pX)
    (qsY : IsQuasiSeparated B S hS pY) (small : Cardinal.mk I < B.cutoff.ord.cof)
    (F : SystemMorphism GX GY f i₀ leX leY) (proper : IsProper B S hS f) :
    ∃ i₃ : I, i₀ ≤ i₃ ∧ ∀ k : Over (op i₀), i₃ ≤ k.left.unop →
      IsProper B S hS (F.maps.app k)

Tag 0CPF, a lemma

Tag 0CPF in the Stacks Project.

AlgebraicGeometry.Space.GoodDiagram.exists_isClosedImmersion_lift_and_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/DescendingFiniteTypeCartesian.lean, line 905.

Stacks 0CPF. In Situation 0CP6, let

X₁ --p--> X₃
|q        |a
X₂ --b--> X₄

be a cartesian diagram of algebraic spaces over B, quasi-separated over B. For each j = 1, 2, 3, 4 let G_j be a diagram X_j ⟶ W_j ⟶ B_{i_j} as in Stacks 0CP8, with limit description X_j = lim_{i ≥ i_j} X^j_i (Stacks 0CP9), and let (a_i)_{i ≥ i₅}, (b_i)_{i ≥ i₆}, (p_i)_{i ≥ i₇}, (q_i)_{i ≥ i₈} be morphisms of these inverse systems inducing a, b, p, q, as in Stacks 0CPA. Then there is an i₉ ≥ i₅, i₆, i₇, i₈ such that for i ≥ i₉ we have a_i ∘ p_i = b_i ∘ q_i and (q_i, p_i) : X¹_i ⟶ X²_i ×_{b_i, X⁴_i, a_i} X³_i is a closed immersion. If a is flat and of finite presentation (the source asks this of a and of b), there is an i₁₀ ≥ i₉ such that for i ≥ i₁₀ this morphism is an isomorphism.

theorem exists_isClosedImmersion_lift_and_isIso (alg₁ : IsAlgebraicSpace B S hS X₁)
    (alg₂ : IsAlgebraicSpace B S hS X₂) (alg₃ : IsAlgebraicSpace B S hS X₃)
    (alg₄ : IsAlgebraicSpace B S hS X₄) (qs₁ : IsQuasiSeparated B S hS pX₁)
    (qs₃ : IsQuasiSeparated B S hS pX₃) (qs₄ : IsQuasiSeparated B S hS pX₄)
    (small : Cardinal.mk I < B.cutoff.ord.cof)
    (cart : IsPullback p q a b) (overA : a ≫ pX₄ = pX₃) (overB : b ≫ pX₄ = pX₂)
    (overQ : q ≫ pX₂ = pX₁)
    (Fa : SystemMorphism G₃ G₄ a i₅ h₃₅ h₄₅) (Fb : SystemMorphism G₂ G₄ b i₆ h₂₆ h₄₆)
    (Fp : SystemMorphism G₁ G₃ p i₇ h₁₇ h₃₇) (Fq : SystemMorphism G₁ G₂ q i₈ h₁₈ h₂₈) :
    ∃ (i₉ : I) (le₅ : i₅ ≤ i₉) (le₆ : i₆ ≤ i₉) (le₇ : i₇ ≤ i₉) (le₈ : i₈ ≤ i₉)
      (comm : ∀ (i : I) (le : i₉ ≤ i),
        Fp.app i (le₇.trans le) ≫ Fa.app i (le₅.trans le) =
          Fq.app i (le₈.trans le) ≫ Fb.app i (le₆.trans le)),
      (∀ (i : I) (le : i₉ ≤ i),
        IsClosedImmersion B S hS (pullback.lift _ _ (comm i le).symm)) ∧
      (IsFlat B S hS a → IsFinitePresentation B S hS a →
        ∃ i₁₀ : I, ∃ le₁₀ : i₉ ≤ i₁₀, ∀ (i : I) (le : i₁₀ ≤ i),
          IsIso (pullback.lift _ _ (comm i (le₁₀.trans le)).symm))

Sources

• Section 70.23, Tag 0CP5
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.NoetherianLimitSystem · AlgebraicGeometry.Space.GoodDiagram · AlgebraicGeometry.Space.GoodDiagram.isLimit_imageCone · AlgebraicGeometry.Space.GoodDiagram.exists_systemMorphism · AlgebraicGeometry.Space.GoodDiagram.eventually_eq_systemMorphism · AlgebraicGeometry.Space.GoodDiagram.SystemMorphism.exists_isFlat_isPullback · AlgebraicGeometry.Space.GoodDiagram.SystemMorphism.exists_isSmooth · AlgebraicGeometry.Space.NoetherianSpaceSystem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.