87.35 The structure sheaf to 87.38 Completion along a closed…

Section87.35 The structure sheaf#

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

Tag 0DEJ, a lemma

Tag 0DEJ in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_isStructureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/StructureSheaf/Exists.lean, line 66.

Stacks 0DEJ. Every formal algebraic space has a structure sheaf: a sheaf of topological rings 𝒪_X on its small étale site X_étale such that 𝒪_X(U_red) = lim Γ(U_λ, 𝒪_{U_λ}) as topological rings, canonically, for every affine formal algebraic space U with a morphism U ⟶ X representable by algebraic spaces and étale, and every colimit presentation U = colim U_λ of U as in Stacks 0AI7 (AlgebraicGeometry.FormalSpace.IsStructureSheaf).

theorem exists_isStructureSheaf {X : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X) :
    ∃ O : Sheaf (canonicalSmallEtaleTopology hX) TopCommRingCat.{u + 1}, IsStructureSheaf hX O
Tag 0DEK, a remark

Tag 0DEK in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_isAffineFormalAlgebraicSpace_not_enough_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/NotEnoughSections.lean, line 209.

The structure sheaf of a formal algebraic space does not always have enough sections. There is an affine formal algebraic space X which is not McQuillan (it fails condition (4) of Stacks 0AIC) and whose points are not separated by regular functions, in the sense of Stacks 0CBD: * for every presentation X = colim X_λ by affine thickenings as in Stacks 0AI7, the ring lim Γ(X_λ, O_{X_λ}) of regular functions is a field, every stage X_λ has infinitely many points (they are the points of X, see AlgebraicGeometry.FormalSpace.pointsULiftEquivStage), and each regular function vanishes either at all points of a stage or at none, so it separates no two points; * X has infinitely many points, and its reduction X_red is represented by a scheme of the site with infinitely many points.

theorem exists_isAffineFormalAlgebraicSpace_not_enough_sections :
    ∃ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) (X : FppfSheaf B S hS),
      IsAffineFormalAlgebraicSpace B S hS X ∧
      ¬ HasSomeSurjectivePresentation B S hS X ∧
      (∀ (I : Type (u + 1)) [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
        (D : I ⥤ BigAffineFppf B S hS),
        (∀ ⦃i j : I⦄ (f : i ⟶ j),
          Stacks.Thickenings.IsThickening ((BigAffineFppf.toScheme B S hS).map (D.map f))) →
        Nonempty (X ≅ colimit (D ⋙ BigAffineFppf.inclusion B S hS ⋙
          Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))) →
        IsField (sectionDiagram B S hS D ⋙ forget CommRingCat.{u}).sections ∧
        (∀ i : I, Infinite ((BigAffineFppf.toScheme B S hS).obj (D.obj i))) ∧
        ∀ (f : (sectionDiagram B S hS D ⋙ forget CommRingCat.{u}).sections) (i : I)
          (x y : (BigAffineFppf.toScheme B S hS).obj (D.obj i)),
          x ∈ ((BigAffineFppf.toScheme B S hS).obj (D.obj i)).basicOpen (f.1 (op i)) ↔
            y ∈ ((BigAffineFppf.toScheme B S hS).obj (D.obj i)).basicOpen (f.1 (op i))) ∧
      Infinite (Space.pointsULift.{u + 1} B S hS X.obj) ∧
      ∃ (T : BigFppfOver B S hS)
        (ι : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj T ⟶ X),
        IsReduction B S hS X ((Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj T) ι ∧
        Infinite ((BigFppfOver.toScheme B S hS).obj T)
Tag 0DEL, a lemma

Tag 0DEL in the Stacks Project.

AlgebraicGeometry.FormalSpace.completedCechComplex_homology_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/StructureSheafEtaleCohomology.lean, line 411. The attribute's comment: “the computation half of the proof: for a covering of X = Spf A by one affine étale chart Spf B^∧ the Čech cohomology of 𝒪_X vanishes in every positive degree. The site-theoretic half, the reduction of Hⁿ(X_étale, 𝒪_X) to these Čech complexes along Stacks 03F9, 03OZ, 0DEE and 0DEF, is not carried: this library does have the étale sites of a formal algebraic space, AlgebraicGeometry.FormalSpace.SmallEtale and its siblings of Stacks 0DEA, and Stacks 0DEE as an equivalence, AlgebraicGeometry.FormalSpace.affineEtaleEquivalence, but no structure sheaf on an étale site; Stacks 0DEF is formalized only as the ring-theoretic category of the completions B^∧. Stated for an arbitrary antitone sequence of ideals and an arbitrary faithfully flat A-algebra, which generalizes the source's weakly admissible A and étale covering A → B”.

Stacks 0DEL. Let X = Spf A be a countably indexed affine formal algebraic space, with J₀ ⊇ J₁ ⊇ ⋯ a countable fundamental system of weak ideals of definition of A, and let {Spf B^∧ ⟶ Spf A} be a covering in the affine étale site, so that A → B is faithfully flat. Then Ȟⁿ({Spf B^∧ ⟶ Spf A}, 𝒪_X) = 0 for n > 0.

theorem completedCechComplex_homology_isZero [Module.FaithfullyFlat A B] (n : ℕ) (hn : 0 < n) :
    IsZero ((completedCechComplex B J hJ).homology (n + 1))

AlgebraicGeometry.FormalSpace.exists_completedCechComplex_homology_isZero_of_isCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/StructureSheafEtaleCohomology.lean, line 495. The attribute's comment: “the covering-level content with the source's own hypotheses: a countably indexed affine formal algebraic space and a surjective affine étale chart of it, in place of the antitone sequence of ideals and the faithfully flat algebra of completedCechComplex_homology_isZero. The conclusion is still the vanishing of the Čech cohomology of the covering, not of Hⁿ(X_étale, 𝒪_X): this library has no structure sheaf on the étale site of a formal algebraic space: Stacks 0DEE is an equivalence here, AlgebraicGeometry.FormalSpace.affineEtaleEquivalence, but Stacks 0DEF is formalized only as the ring-theoretic category of the completions B^∧, so no object of the affine étale site is known to be of the form Spf B^∧ and the sections of 𝒪_X are undefined”.

Stacks 0DEL with the hypotheses of the source. A countably indexed affine formal algebraic space X is the formal spectrum of a weakly admissible topological ring A carrying a countable antitone fundamental system J₀ ⊇ J₁ ⊇ ⋯ of weak ideals of definition, and for every covering {Spf B^∧ ⟶ Spf A} of X by one affine étale chart, in the sense of Stacks 0DEF and with Spf B^∧ ⟶ Spf A surjective, the Čech complex of 𝒪_X for that covering has no cohomology in positive Čech degrees.

Affineness of X is not assumed: it is part of the conclusion, X being exhibited as a formal spectrum.

theorem exists_completedCechComplex_homology_isZero_of_isCountablyIndexed
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) {X : FppfSheaf B S hS}
    (hc : IsCountablyIndexed B S hS X) :
    ∃ (A : Type u) (_ : CommRing A) (_ : TopologicalSpace A) (_ : IsTopologicalRing A)
      (_ : IsLinearTopology A A) (hA : TopologicalRing.IsWeaklyAdmissible A)
      (Q : QuotientSystem B S hS A) (J : ℕ → Ideal A) (hJ : Antitone J),
      (∀ k, TopologicalRing.IsWeakIdealOfDefinition (J k)) ∧
        (nhds (0 : A)).HasBasis (fun _ : ℕ ↦ True) (fun k ↦ (J k : Set A)) ∧
        Nonempty (X ≅ formalSpectrum Q) ∧
        ∀ (Y : EtaleCompletion A) (E : QuotientSystem B S hS Y.completion)
          (g : ContinuousHom Q E), g.toRingHom = Y.structureMap →
          IsSurjective B S hS (formalSpectrumMap hA g) → ∀ n : ℕ, 0 < n →
            letI : Algebra A Y.carrier := Y.str.toAlgebra
            IsZero ((completedCechComplex Y.carrier J hJ).homology (n + 1))

AlgebraicGeometry.FormalSpace.subsingleton_sheafH_countablyIndexedStructureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/StructureSheafHigherVanishing.lean, line 119. The attribute's comment: “at an arbitrary reduction X_red of X, which Stacks 0DEA reads X_étale against”.

Stacks 0DEL. Let X be a countably indexed affine formal algebraic space over S, and let X_red be a reduction of X. Then the structure sheaf 𝒪_X has no higher cohomology on X_étale: Hⁿ(X_étale, 𝒪_X) = 0 for n > 0.

Only the countable presentation of X is used, not the set-theoretic condition which makes X an affine formal algebraic space, so the statement is given for a countably indexed sheaf.

theorem subsingleton_sheafH_countablyIndexedStructureSheaf (hc : IsCountablyIndexed B S hS X)
    (R : Reduction B S hS X) [HasExt.{x} (Sheaf R.smallEtaleTopology AddCommGrpCat.{u + 1})]
    (n : ℕ) (hn : 0 < n) :
    Subsingleton (Sheaf.H
      ((sheafCompose _ Space.topCommRingToAddCommGrp).obj
        (countablyIndexedStructureSheaf hc R)) n)

AlgebraicGeometry.FormalSpace.subsingleton_sheafH_canonicalStructureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/StructureSheafHigherVanishing.lean, line 131.

Stacks 0DEL. If X is a countably indexed affine formal algebraic space over S, then Hⁿ(X_étale, 𝒪_X) = 0 for n > 0, where X_étale is the small étale site of Stacks 0DEA at the reduction of X given by Stacks 0AIN, and 𝒪_X is the structure sheaf of X on it.

theorem subsingleton_sheafH_canonicalStructureSheaf (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hc : IsCountablyIndexed B S hS X)
    [HasExt.{x} (Sheaf (canonicalSmallEtaleTopology
      (isFormalAlgebraicSpace_of_isAffineFormalAlgebraicSpace B S hS hX)) AddCommGrpCat.{u + 1})]
    (n : ℕ) (hn : 0 < n) :
    Subsingleton (Sheaf.H
      ((sheafCompose _ Space.topCommRingToAddCommGrp).obj
        (countablyIndexedStructureSheaf hc
          (canonicalReduction
            (isFormalAlgebraicSpace_of_isAffineFormalAlgebraicSpace B S hS hX)))) n)
Tag 0DEM, a remark

Tag 0DEM in the Stacks Project.

AlgebraicGeometry.FormalSpace.not_nonempty_abelian_quasicoherentModules_completionAlongIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionQuasicoherentNotAbelian.lean, line 79. The attribute's comment: “the content of Examples, Section 0ALF: for every Noetherian domain A complete for a principal ideal (π) with π ≠ 0 not a unit, Spf(A) is a Noetherian affine formal algebraic space whose quasi-coherent modules do not form an abelian category”.

Stacks 0DEM. Let A be a Noetherian domain which is complete for a principal ideal I = (π) with π neither zero nor a unit, and let X = Spf(A) be the completion of Spec A along V(I), over any base scheme S of any big fppf site. Then X is a Noetherian affine formal algebraic space, and the category of quasi-coherent modules on X (Stacks 06WG) is not abelian: it admits no abelian structure at all.

Formal Spaces, Remark 0DEM, says that for almost any Noetherian affine formal algebraic space the natural category of quasi-coherent modules is not abelian, referring to Examples, Section 0ALF; the content of that section is the identification of these modules with the complete A-modules (AlgebraicGeometry.FormalSpace.quasicoherentModulesCompletionEquiv) together with the non-abelianness of the latter (Stacks 07JR), and this statement is that content for every such A, of which the section's ℤ_p is one.

theorem not_nonempty_abelian_quasicoherentModules_completionAlongIdeal
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) {A : Type u} [CommRing A]
    [IsNoetherianRing A] [NoZeroDivisors A] (f : Spec (.of A) ⟶ S)
    (hA : B.Contains (Spec (.of A))) (I : Ideal A) (hAc : IsAdicComplete I A) (π : A)
    (hIπ : I = Ideal.span {π}) (hπ : π ≠ 0) (hπu : ¬ IsUnit π) :
    IsAffineFormalAlgebraicSpace B S hS (completionAlongIdeal B S hS f hA I) ∧
      IsNoetherian B S hS (completionAlongIdeal B S hS f hA I) ∧
      ¬ Nonempty (Abelian (FibredSite.quasicoherentModules.{u, u + 1, u + 1, u} B S hS
        (completionFibred B S hS f hA I).p
        (isFiberedInGroupoids_completionFibred B S hS f hA I)))
Sources
LeanAlgebraicGeometry.FormalSpace.exists_isStructureSheaf · AlgebraicGeometry.FormalSpace.exists_isAffineFormalAlgebraicSpace_not_enough_sections · AlgebraicGeometry.FormalSpace.completedCechComplex_homology_isZero · AlgebraicGeometry.FormalSpace.exists_completedCechComplex_homology_isZero_of_isCountablyIndexed · AlgebraicGeometry.FormalSpace.subsingleton_sheafH_countablyIndexedStructureSheaf · AlgebraicGeometry.FormalSpace.subsingleton_sheafH_canonicalStructureSheaf · AlgebraicGeometry.FormalSpace.not_nonempty_abelian_quasicoherentModules_completionAlongIdeal

Section87.36 Colimits of formal algebraic spaces#

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

Tag 0GVM, a lemma

Tag 0GVM in the Stacks Project.

AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/DirectedColimit.lean, line 787. The attribute's comment: “granting the set-theoretic condition of Stacks 0AIS for the colimit”.

The colimit of a directed system of affine formal algebraic spaces over S whose transition morphisms are representable thickenings -- equivalently, closed immersions inducing isomorphisms on reductions -- is an affine formal algebraic space over S, provided it satisfies the set-theoretic condition of Stacks 0AIS.

theorem isAffineFormalAlgebraicSpace_colimit (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {I : Type (u + 1)} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (D : I ⥤ Sheaf (BigFppfOver.topology B S hS) (Type (u + 1)))
    (hD : ∀ i, IsAffineFormalAlgebraicSpace B S hS (D.obj i))
    (hthick : ∀ ⦃i j : I⦄ (f : i ⟶ j),
      MorphismProperty.relative (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
        (MorphismProperty.inverseImage
          (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)) (D.map f))
    (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))) (e : X ≅ colimit D)
    (hset : SatisfiesSetTheoreticCondition B S hS X) :
    IsAffineFormalAlgebraicSpace B S hS X

AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_colimit_of_cofinal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/DirectedColimitSetCondition.lean, line 114. The attribute's comment: “corrected form: the printed statement is false for an index set as large as the size cutoff of the site, the colimit then failing the set-theoretic condition of Stacks 0AIS (AlgebraicGeometry.FormalSpace.not_forall_isAffineFormalAlgebraicSpace_colimit); stated, under the source's hypotheses, for an index with a cofinal family whose index is admissible for coproducts in the site, the proviso of Stacks 0AIS observation (1) that the coproduct of the stages be representable by an object of the site (always the case for a countable index), and with the set-theoretic condition derived, not assumed”.

Stacks 0GVM. The colimit of a directed system of affine formal algebraic spaces over S whose transition morphisms are representable thickenings -- equivalently, closed immersions inducing isomorphisms on reductions -- is an affine formal algebraic space over S, provided the index set has a cofinal family ι : K → I indexed by a set K which is not too large (u-small, of cardinality below the cofinality of the size cutoff of the site; every countable K qualifies).

The size bound is the proviso of observation (1) of Remark 0AIS. For a colimit X = colim X_λ of a system as in Definition 0AI7, the source notes that U = ∐_λ X_λ ⟶ X is a surjection of fppf sheaves, and that "if U is representable by an object of (Sch/S)_fppf" then the set-theoretic condition is satisfied, which "is always the case if Λ is countable" (Sets, Lemma 000R). Being u-small of cardinality below the cofinality of the size cutoff, AlgebraicGeometry.BigFppfSite.AdmitsCoproductIndex, is what makes a coproduct of objects of the site indexed by K an object of the site; every countable K qualifies (AlgebraicGeometry.BigFppfSite.admitsCoproductIndex_of_countable). It is asked only of a cofinal family, which has the same colimit. Because the stages here are affine formal algebraic spaces rather than affine schemes, each stage X_{ι k} is replaced by an object U_k of the site surjecting onto it, as in observation (3) of Remark 0AIS, and ∐_k U_k is the object of the site that the proviso asks for. The bound cannot be dropped: see AlgebraicGeometry.FormalSpace.not_forall_isAffineFormalAlgebraicSpace_colimit.

theorem isAffineFormalAlgebraicSpace_colimit_of_cofinal (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {I : Type (u + 1)} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (D : I ⥤ Sheaf (BigFppfOver.topology B S hS) (Type (u + 1)))
    (hD : ∀ i, IsAffineFormalAlgebraicSpace B S hS (D.obj i))
    (hthick : ∀ ⦃i j : I⦄ (f : i ⟶ j),
      MorphismProperty.relative (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
        (MorphismProperty.inverseImage
          (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)) (D.map f))
    (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))) (e : X ≅ colimit D)
    {K : Type v} [Small.{u} K] [B.AdmitsCoproductIndex K] (ι : K → I)
    (hι : ∀ i, ∃ k, i ≤ ι k) :
    IsAffineFormalAlgebraicSpace B S hS X

AlgebraicGeometry.FormalSpace.not_forall_isAffineFormalAlgebraicSpace_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/DirectedColimitSetCondition.lean, line 185. The attribute's comment: “the statement as printed is false: over any nonempty S, the directed system Spec(k + k^μ) of affine schemes along thickenings, indexed by the finite subsets μ of a set as large as the size cutoff of the site, has a colimit failing the set-theoretic condition of Stacks 0AIS, the coproduct of its stages not being an object of the site as the proviso of Stacks 0AIS observation (1) requires; the corrected form is AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_colimit_of_cofinal”.

Stacks 0GVM needs a size bound on the index set. Over a nonempty scheme S of the site it is not the case that the colimit of every directed system of affine formal algebraic spaces over S along representable thickenings is an affine formal algebraic space: the colimit of AlgebraicGeometry.FormalSpace.sqZeroSheafDiagram, for a residue field of S and an index set as large as the size cutoff of the site, does not satisfy the set-theoretic condition of Remark 0AIS. This is where the proviso of observation (1) of Remark 0AIS fails: each stage has one point, so the coproduct of the stages has as many points as the index, which is as large as the size cutoff, while an object of the site has fewer points than the cutoff.

theorem not_forall_isAffineFormalAlgebraicSpace_colimit (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) [Nonempty S] :
    ¬ ∀ (I : Type (u + 1)) [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
      (D : I ⥤ Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))),
      (∀ i, IsAffineFormalAlgebraicSpace B S hS (D.obj i)) →
      (∀ ⦃i j : I⦄ (f : i ⟶ j),
        MorphismProperty.relative (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
          (MorphismProperty.inverseImage
            (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B S hS)) (D.map f)) →
      ∀ (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))), (X ≅ colimit D) →
        IsAffineFormalAlgebraicSpace B S hS X
Tag 0GVN, a lemma

Tag 0GVN in the Stacks Project.

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_colimit_closedImmersions_of_admissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ColimitOfFormalSpacesAdmissible.lean, line 374. The attribute's comment: “corrected form: the index is required to admit coproducts in the site (AlgebraicGeometry.BigFppfSite.AdmitsCoproductIndex, e.g. any countable index), the caveat of Remark 0AIS (1) and (3) that the source's proof leaves unchecked; without such a bound the statement is false, by AlgebraicGeometry.FormalSpace.not_forall_isFormalAlgebraicSpace_colimit_closedImmersions”.

Stacks 0GVN, in the form its proof establishes. Let E be a directed system of formal algebraic spaces over S whose transition morphisms are representable thickenings — equivalently, by Stacks 0GVL, closed immersions inducing isomorphisms on reductions — indexed by a type admitting coproducts in the site (every countable index does). Then a sheaf isomorphic to its colimit is a formal algebraic space over S.

The bound is forced: the source's proof never checks the set-theoretic condition of Definition 0AIM for the colimit, Remark 0AIS (1) and (3) give it only for an index "not too large (for example countable)", and without a bound the conclusion is false, AlgebraicGeometry.FormalSpace.not_forall_isFormalAlgebraicSpace_colimit_closedImmersions.

theorem isFormalAlgebraicSpace_of_colimit_closedImmersions_of_admissible
    (Λ : Type (u + 1)) [Preorder Λ] [Nonempty Λ] [IsDirected Λ (· ≤ ·)] [Small.{u} Λ]
    [B.AdmitsCoproductIndex Λ] (E : Λ ⥤ FppfSheaf B S hS)
    (hform : ∀ i : Λ, IsFormalAlgebraicSpace B S hS (E.obj i))
    (hthick : ∀ ⦃i j : Λ⦄ (g : i ⟶ j),
      Space.IsRepresentableThickeningULift.{u + 1} B S hS (E.map g).hom)
    (Z : FppfSheaf B S hS) (hZ : Nonempty (Z ≅ colimit E)) :
    IsFormalAlgebraicSpace B S hS Z

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_colimit_closedImmersions_of_satisfiesSetTheoreticCondition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ColimitOfFormalSpacesAdmissible.lean, line 406. The attribute's comment: “corrected form per the recorded erratum: for an arbitrary directed index, the colimit of a system of formal algebraic spaces along closed immersions inducing isomorphisms on reductions (representable thickenings, Stacks 0GVL) is a formal algebraic space provided the colimit satisfies the set-theoretic condition of Remark 0AIS; that condition cannot be dropped, AlgebraicGeometry.FormalSpace.not_forall_isFormalAlgebraicSpace_colimit_closedImmersions”.

Stacks 0GVN, corrected per the recorded erratum. Let E be a directed system of formal algebraic spaces over S, indexed by an arbitrary directed set, whose transition morphisms are representable thickenings — equivalently, by Stacks 0GVL, closed immersions inducing isomorphisms on reductions. A sheaf Z isomorphic to its colimit which satisfies the set-theoretic condition of Remark 0AIS is a formal algebraic space over S.

The set-theoretic condition is the only hypothesis beyond those of the source, and it cannot be dropped (AlgebraicGeometry.FormalSpace.not_forall_isFormalAlgebraicSpace_colimit_closedImmersions). The chart system of the source's proof is constructed from an atlas of one stage by the étale lifting of Stacks 0DEG/0DEE and its stages are affine by Stacks 0DE8 (AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_colimit_of_setTheoretic, with AlgebraicGeometry.FormalSpace.isAffineOfSurjectiveClosedImmersion); for an index admitting coproducts in the site the condition is itself a theorem, AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_colimit_closedImmersions_of_admissible.

theorem isFormalAlgebraicSpace_of_colimit_closedImmersions_of_satisfiesSetTheoreticCondition
    (Λ : Type (u + 1)) [Preorder Λ] [Nonempty Λ] [IsDirected Λ (· ≤ ·)]
    (E : Λ ⥤ FppfSheaf B S hS)
    (hform : ∀ i : Λ, IsFormalAlgebraicSpace B S hS (E.obj i))
    (hthick : ∀ ⦃i j : Λ⦄ (g : i ⟶ j),
      Space.IsRepresentableThickeningULift.{u + 1} B S hS (E.map g).hom)
    (Z : FppfSheaf B S hS) (hZset : SatisfiesSetTheoreticCondition B S hS Z)
    (hZ : Nonempty (Z ≅ colimit E)) :
    IsFormalAlgebraicSpace B S hS Z
Sources
LeanAlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_colimit · AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_colimit_of_cofinal · AlgebraicGeometry.FormalSpace.not_forall_isAffineFormalAlgebraicSpace_colimit · AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_colimit_closedImmersions_of_admissible · AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_colimit_closedImmersions_of_satisfiesSetTheoreticCondition

Section87.37 Recompletion#

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

Tag 0GVQ, a lemma

Tag 0GVQ in the Stacks Project.

AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_completionAlong', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionAffineSupplement.lean, line 992.

Stacks 0GVQ. Let S be a scheme, let X be an affine formal algebraic space over S, let i : X_red ⟶ X be a reduction of X and let T ⊆ |X_red| be a closed subset. Then the completion X_{/T} of X along T — the fppf sheaf whose sections over an object U of the big fppf site of S are the morphisms f : U ⟶ X with f(|U|) ⊆ T — is an affine formal algebraic space over S.

Nothing is assumed beyond the tag's own hypotheses. The affine presentation is exists_affinePresentation_completionSheafULift and the set-theoretic condition of Stacks 0AIS is satisfiesSetTheoreticCondition_completionSheafULift.

The two steps the source cites in general form are proved here: that a closed subset of |X_red| is a closed subset of |X| is AlgebraicGeometry.FormalSpace.IsReduction.isClosed_image_pointsMapULift, and that X_{/T} = colim (X_λ)_{/T} is AlgebraicGeometry.FormalSpace.completionSheafULiftIsoColimitCompletion.

The reduction is supplied as data satisfying AlgebraicGeometry.FormalSpace.IsReduction rather than constructed, since Stacks 0AIN — the existence of a reduction — is not available in this library; this is how Stacks 0GVT is stated here as well, and it needs no choice.

theorem isAffineFormalAlgebraicSpace_completionAlong' {X Xred : FppfSheaf B S hS}
    (hX : IsAffineFormalAlgebraicSpace B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T) :
    IsAffineFormalAlgebraicSpace B S hS (completionAlong i T)
Tag 0GVR, a lemma

Tag 0GVR in the Stacks Project.

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_completionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionFormalAlgebraicSpace.lean, line 314.

Stacks 0GVR. Let S be a scheme, let X be a formal algebraic space over S and let T ⊆ |X_red| be a closed subset, for a reduction i : X_red ⟶ X of X. Then the functor X_{/T} on the big fppf site of S sending U to the morphisms f : U ⟶ X with f(|U|) ⊆ T is a formal algebraic space: it is an fppf sheaf, and as such a formal algebraic space over S. It is the completion completionAlong i T of Stacks 0GVS, which is a formal algebraic space as well.

The functor is AlgebraicGeometry.Space.completionSubfunctorULift of X along the image of T in |X|. Nothing is assumed: the sheaf property is AlgebraicGeometry.Space.isSheaf_completionSubfunctorULift, the atlas of Definition 0AIM is AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_completionSheafULift with its affine charts from Stacks 0GVQ, and the set-theoretic condition of Stacks 0AIS is satisfiesSetTheoreticCondition_completionSheafULift_of_satisfiesSetTheoreticCondition. A reduction exists by Stacks 0AIN, and the statement holds for every one.

theorem isFormalAlgebraicSpace_completionFunctor {X Xred : FppfSheaf B S hS}
    (hX : IsFormalAlgebraicSpace B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T) :
    ∃ h : Presheaf.IsSheaf (BigFppfOver.topology B S hS)
        (Space.completionSubfunctorULift B S hS X.obj
          (Space.pointsMapULift.{u + 1} B S hS Xred.obj i.hom '' T)).toFunctor,
      IsFormalAlgebraicSpace B S hS ⟨_, h⟩ ∧
        IsFormalAlgebraicSpace B S hS (completionAlong i T)

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_completionAlong', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionFormalSpace.lean, line 217. The attribute's comment: “the whole statement for the tag's own hypotheses — X a formal algebraic space and T closed in |X_red| — from one carried hypothesis, hset, the set-theoretic condition of Stacks 0AIS for the completion, which this library carries by standing convention on the library's Stacks 0AJ1 (isFormalAlgebraicSpace_of_etaleCover, StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleCover.lean) and Stacks 0GVM (isAffineFormalAlgebraicSpace_colimit, StacksFrontier/AlgebraicGeometry/FormalSpace/DirectedColimit.lean), the condition being part of the definition of a formal algebraic space used here and not following from the conditions on the members of a covering family. Nothing else: the affine case, clause (1) of Stacks 0GVV, is proved — completionOfAffineIsAffine; and closedness of T is the tag's own, in |X_red|, the inclusion of a reduction being a homeomorphism on points (IsReduction.isHomeomorph_pointsMapULift) and hence carrying T to a closed subset of |X|, which is where the proof uses it (IsReduction.isClosed_image_pointsMapULift). hi supplies the reduction as data because Stacks 0AIN is unavailable in this library, the convention of the library's Stacks 0GVQ and 0GVT”.

Stacks 0GVR. Let S be a scheme, let X be a formal algebraic space over S with reduction i : X_red ⟶ X and let T ⊆ |X_red| be closed. The completion X_{/T} of X along T — the fppf sheaf attached to the functor sending U to the morphisms f : U ⟶ X with f(|U|) ⊆ T — is a formal algebraic space over S: the completions of the charts of X along the inverse images of T form an atlas as in Definition 0AIM, each of them affine formal by clause (1) of Stacks 0GVV, each representable étale over X_{/T} as a base change of a chart of X, and jointly surjective because the charts of X are.

The closed subset T of |X_red| enters the completion through its image in |X|, which is closed because the inclusion of a reduction is a homeomorphism on points: AlgebraicGeometry.FormalSpace.IsReduction.isClosed_image_pointsMapULift. The set-theoretic condition hset of Stacks 0AIS is the only hypothesis beyond the tag's own; see the section "What is assumed" of this file.

theorem isFormalAlgebraicSpace_completionAlong' {X Xred : FppfSheaf B S hS}
    (hX : IsFormalAlgebraicSpace B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T)
    (hset : SatisfiesSetTheoreticCondition B S hS (completionAlong i T)) :
    IsFormalAlgebraicSpace B S hS (completionAlong i T)
Tag 0GVS, a definition

Tag 0GVS in the Stacks Project.

Declarations registered for the tag:

Tag 0GVT, a lemma

Tag 0GVT in the Stacks Project.

AlgebraicGeometry.FormalSpace.isClosed_preimage_pointsMapULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Recompletion.lean, line 352. The attribute's comment: “the closed subset T'”.

Stacks 0GVT. The inverse image T' = |f_red|⁻¹ T of a closed subset T ⊆ |X_red| is a closed subset of |X'_red|, since the morphism of reductions is continuous on points.

theorem isClosed_preimage_pointsMapULift {Xred' Xred : FppfSheaf B S hS}
    (fred : Xred' ⟶ Xred) (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj)) :
    letI := Space.pointTopologyULift.{u + 1} B S hS Xred.obj
    letI := Space.pointTopologyULift.{u + 1} B S hS Xred'.obj
    IsClosed T →
      IsClosed (Space.pointsMapULift.{u + 1} B S hS Xred'.obj fred.hom ⁻¹' T)

AlgebraicGeometry.FormalSpace.isPullback_completionAlongMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Recompletion.lean, line 410. The attribute's comment: “the cartesian square”. References: EGA I (10.9.9).

Stacks 0GVT. Let f : X' ⟶ X be a morphism of formal algebraic spaces over S, let T ⊆ |X_red| be a closed subset and let T' = |f_red|⁻¹ T ⊆ |X'_red|. Then the square formed by X'_{/T'} ⟶ X', X_{/T} ⟶ X, the morphism of completions and f is cartesian.

theorem isPullback_completionAlongMap {X' X Xred' Xred : FppfSheaf B S hS}
    (_hX' : IsFormalAlgebraicSpace B S hS X') (_hX : IsFormalAlgebraicSpace B S hS X)
    {i' : Xred' ⟶ X'} {i : Xred ⟶ X} (hi' : IsReduction B S hS X' Xred' i')
    (hi : IsReduction B S hS X Xred i) (f : X' ⟶ X)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (_hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T) :
    IsPullback
      (completionAlongInclusion i'
        (Space.pointsMapULift.{u + 1} B S hS Xred'.obj (reductionMap hi' hi f).hom ⁻¹' T))
      (completionAlongMap hi' hi f T)
      f
      (completionAlongInclusion i T)
Tag 0GVU, a lemma

Tag 0GVU in the Stacks Project.

AlgebraicGeometry.FormalSpace.isReduction_completionAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionReduction.lean, line 551. The attribute's comment: “with the reduction of X written as the universe lift of an algebraic space over S, the form in which the reduced induced closed subspace of Stacks 03IQ is available; that costs no generality, by Space.exists_uliftFunctor_iso_of_isAlgebraicSpaceULift”. References: EGA I (10.8.6), “more general”.

Stacks 0GVU. Let S be a scheme contained in a big fppf site B, let X be a formal algebraic space over S with reduction i : X_red ⟶ X, and let T ⊆ |X_red| be a closed subset. The reduction of the completion X_{/T} of X along T is the reduced induced closed subspace Z of X_red corresponding to T: the canonical morphism Z ⟶ X_{/T} exhibits Z as the reduction of the completion.

The conclusion contains the mapping property: every morphism to X_{/T} from a reduced algebraic space over S factors uniquely through Z.

theorem isReduction_completionAlong (_hX : IsFormalAlgebraicSpace B S hS X)
    (hi : IsReduction B S hS X (sheafOfAlgebraicSpace B S hS Xred₀ hXred₀) i)
    (T : Set (Space.points B S hS Xred₀)) (hT : IsClosed T) :
    IsReduction B S hS (completionAlong i (liftedPointSet B S hS hXred₀ T))
      (reducedSubspaceSheaf B S hS hXred₀ T hT)
      (reducedSubspaceToCompletionAlong B S hS hXred₀ T hT)
Tag 0GVV, a lemma

Tag 0GVV in the Stacks Project.

AlgebraicGeometry.FormalSpace.isCountablyIndexed_completionAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionAffineClausesTypes.lean, line 142. The attribute's comment: “clause (3): if |X_red| \ T is quasi-compact and X is countably indexed then so is X_{/T}, countably indexed being IsCountablyIndexed (Stacks 0AIJ, StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexed.lean). Carried hypotheses: hX is the tag's own countable-indexing hypothesis on X, hi supplies the reduction as data rather than choosing one from Stacks 0AIN (the convention of the library's Stacks 0GVT and 0GB8), hT is the tag's own closedness of T in |X_red|, hqc is the tag's own quasi-compactness of |X_red| \ T, stated as compactness of Tᶜ for the point topology Space.pointTopologyULift since this library has no quasi-compactness predicate for formal algebraic spaces, and hspf is the source's own step producing the weakly admissible ring lim A/J_{m,n} with a countable fundamental system of neighbourhoods of zero — condition (2) of Stacks 0AN1 — quantified over its own space, reduction and subset. The step from hspf to the conclusion is Stacks 0AN1, (2) ⇒ (1) (isCountablyIndexedAffine_of_hasCountableWeakPresentation).”.

Let S be a scheme, let X be an affine formal algebraic space over S, let i : X_red ⟶ X be a reduction of X and let T ⊆ |X_red| be closed with |X_red| \ T quasi-compact. If X is countably indexed then so is the completion X_{/T} of X along T.

It takes as hypothesis hspf : CompletionOfCountablyIndexedIsCountableSpf.

theorem isCountablyIndexed_completionAlong {X Xred : FppfSheaf B S hS}
    (hX : IsCountablyIndexed B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T)
    (hqc : @IsCompact _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) Tᶜ)
    (hspf : CompletionOfCountablyIndexedIsCountableSpf B S hS) :
    IsCountablyIndexed B S hS (completionAlong i T)

AlgebraicGeometry.FormalSpace.isAdicStar_completionAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionAffineClausesTypes.lean, line 190. The attribute's comment: “clause (4): if |X_red| \ T is quasi-compact and X is adic then so is X_{/T}, adic being IsAdicStar (Stacks 0AID (4), StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Types.lean). Carried hypotheses: hX is the tag's own adic* hypothesis on X, hi supplies the reduction as data rather than choosing one from Stacks 0AIN (the convention of the library's Stacks 0GVT and 0GB8), hT is the tag's own closedness of T in |X_red|, hqc is the tag's own quasi-compactness of |X_red| \ T, stated as compactness of Tᶜ for the point topology Space.pointTopologyULift since this library has no quasi-compactness predicate for formal algebraic spaces, hideal is the source's own step identifying X_{/T} with the completion of an affine scheme along the finitely generated ideal J = (f_1,...,f_r) + I, quantified over its own space, reduction and subset, and hset is the set-theoretic condition of Stacks 0AIS on the completion, carried where Stacks 0GVM (isAffineFormalAlgebraicSpace_colimit) carries it and needed to transport the conclusion back along the isomorphism. The step from hideal to the conclusion is Stacks 0GXX (3) (isAdicStar_completionAlongIdeal).”.

Let S be a scheme, let X be an affine formal algebraic space over S, let i : X_red ⟶ X be a reduction of X and let T ⊆ |X_red| be closed with |X_red| \ T quasi-compact. If X is adic* then so is the completion X_{/T} of X along T.

It takes as hypotheses hideal : CompletionOfAdicStarIsCompletionAlongFGIdeal and the set-theoretic condition hset on X_{/T}.

theorem isAdicStar_completionAlong {X Xred : FppfSheaf B S hS}
    (hX : IsAdicStar B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T)
    (hqc : @IsCompact _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) Tᶜ)
    (hideal : CompletionOfAdicStarIsCompletionAlongFGIdeal B S hS)
    (hset : SatisfiesSetTheoreticCondition B S hS (completionAlong i T)) :
    IsAdicStar B S hS (completionAlong i T)

AlgebraicGeometry.FormalSpace.isNoetherian_completionAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionAffineClausesTypes.lean, line 239. The attribute's comment: “clause (5): if X is Noetherian then so is X_{/T}, Noetherian being IsNoetherian (Stacks 0AID (5), StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Types.lean). Carried hypotheses: hX is the tag's own Noetherian hypothesis on X, hi supplies the reduction as data rather than choosing one from Stacks 0AIN (the convention of the library's Stacks 0GVT and 0GB8), hT is the tag's own closedness of T in |X_red|, hideal is the source's own step identifying X_{/T} with the completion of a Noetherian affine scheme along an ideal, quantified over its own space, reduction and subset, and hset is the set-theoretic condition of Stacks 0AIS on the completion, carried where Stacks 0GVM (isAffineFormalAlgebraicSpace_colimit) carries it and needed to transport the conclusion back along the isomorphism. There is deliberately NO quasi-compactness hypothesis: the source notes it is automatic here. The step from hideal to the conclusion is Stacks 0GXX (4) (isNoetherian_completionAlongIdeal).”.

Let S be a scheme, let X be an affine formal algebraic space over S, let i : X_red ⟶ X be a reduction of X and let T ⊆ |X_red| be closed. If X is Noetherian then so is the completion X_{/T} of X along T. No quasi-compactness of |X_red| \ T is assumed.

It takes as hypotheses hideal : CompletionOfNoetherianIsCompletionAlongNoetherianIdeal and the set-theoretic condition hset on X_{/T}.

theorem isNoetherian_completionAlong {X Xred : FppfSheaf B S hS}
    (hX : IsNoetherian B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T)
    (hideal : CompletionOfNoetherianIsCompletionAlongNoetherianIdeal B S hS)
    (hset : SatisfiesSetTheoreticCondition B S hS (completionAlong i T)) :
    IsNoetherian B S hS (completionAlong i T)

AlgebraicGeometry.FormalSpace.isCountablyIndexed_completionAlong', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionAffineClausesTypesSupplement.lean, line 72. The attribute's comment: “clause (3): if |X_red| \ T is quasi-compact and X is countably indexed then so is X_{/T}, countably indexed being IsCountablyIndexed (Stacks 0AIJ, StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexed.lean). Carried hypotheses: hX is the tag's own countable-indexing hypothesis on X, hi supplies the reduction as data rather than choosing one from Stacks 0AIN (the convention of Stacks 0GVT and 0GB8), hT is the tag's own closedness of T in |X_red|, hqc is the tag's own quasi-compactness of |X_red| \ T, stated as compactness of Tᶜ for the point topology Space.pointTopologyULift since this library has no quasi-compactness predicate for formal algebraic spaces. Nothing else: the source's step producing the weakly admissible ring lim A/J_{m,n} with a countable fundamental system of neighbourhoods of zero — condition (2) of Stacks 0AN1 — is not needed at all. The proof goes through condition (1) directly: isCountablyIndexed_completionSheafULift, which gets a countable directed presentation of X_{/T} from a countable one of X and turns it into a sequential one by Stacks 0AII (isCountablyIndexed_iff_exists_countable_presentation).”.

Let S be a scheme, let X be an affine formal algebraic space over S, let i : X_red ⟶ X be a reduction of X and let T ⊆ |X_red| be closed with |X_red| \ T quasi-compact. If X is countably indexed then so is the completion X_{/T} of X along T: it admits a presentation indexed by ℕ by affine schemes along thickenings.

theorem isCountablyIndexed_completionAlong' {X Xred : FppfSheaf B S hS}
    (hX : IsCountablyIndexed B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T)
    (hqc : @IsCompact _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) Tᶜ) :
    IsCountablyIndexed B S hS (completionAlong i T)

AlgebraicGeometry.FormalSpace.isAdicStar_completionAlong', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionAffineClausesTypesSupplement.lean, line 105. The attribute's comment: “clause (4): if |X_red| \ T is quasi-compact and X is adic then so is X_{/T}, adic being IsAdicStar (Stacks 0AID (4), StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Types.lean). Carried hypotheses: hX is the tag's own adic* hypothesis on X, hi supplies the reduction as data because Stacks 0AIN is unavailable in this library (the convention of Stacks 0GVT and 0GB8), hT is the tag's own closedness of T in |X_red|, and hqc is the tag's own quasi-compactness of |X_red| \ T, stated as compactness of Tᶜ for the point topology Space.pointTopologyULift since this library has no quasi-compactness predicate for formal algebraic spaces. NOTHING ELSE: the source's own step X_{/T} = Spf (lim A/J^n) for a finitely generated J is PROVED (exists_fg_quotientSystem_formalSpectrum_iso_completionSheafULift). Nothing in the chain asks anything of Spec A -- no structure morphism to S and no site-membership -- exactly as the source asks nothing: the affines of the site cutting out the powers of J are quotients of the STAGE rings A/K. The set-theoretic condition of Stacks 0AIS is not assumed. The step from X_{/T} = Spf (lim A/J^n) to the conclusion is the ring half of Stacks 0GXX (isAdic_adicCompletion, isIdealOfDefinition_map_adicCompletion, isWeaklyAdmissible_adicCompletion) together with clause (2) of this tag (hasSomeSurjectivePresentation_completionAlong').”.

Let S be a scheme, let X be an affine formal algebraic space over S, let i : X_red ⟶ X be a reduction of X and let T ⊆ |X_red| be closed with |X_red| \ T quasi-compact. If X is adic* then so is the completion X_{/T} of X along T: it is presented by an adic topological ring with a finitely generated ideal of definition.

theorem isAdicStar_completionAlong' {X Xred : FppfSheaf B S hS}
    (hX : IsAdicStar B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T)
    (hqc : @IsCompact _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) Tᶜ) :
    IsAdicStar B S hS (completionAlong i T)

AlgebraicGeometry.FormalSpace.isNoetherian_completionAlong', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionAffineClausesTypesSupplement.lean, line 150. The attribute's comment: “clause (5): if X is Noetherian then so is X_{/T}, Noetherian being IsNoetherian (Stacks 0AID (5), StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Types.lean). Carried hypotheses: hX is the tag's own Noetherian hypothesis on X, hi supplies the reduction as data because Stacks 0AIN is unavailable in this library (the convention of Stacks 0GVT and 0GB8), and hT is the tag's own closedness of T in |X_red|. NOTHING ELSE: the source's own step X_{/T} = Spf (lim A/J^n) for a Noetherian A is PROVED (exists_fg_quotientSystem_formalSpectrum_iso_completionSheafULift). Nothing in the chain asks anything of Spec A -- no structure morphism to S and no site-membership. There is deliberately NO quasi-compactness hypothesis: it is automatic here, which is isCompact_of_isNoetherianRing (the point space of X is the prime spectrum of a quotient of the Noetherian presenting ring, hence a Noetherian space). The set-theoretic condition of Stacks 0AIS is not assumed. The step from X_{/T} = Spf (lim A/J^n) to the conclusion is Stacks 0316 for the Noetherianness of the adic completion together with the ring half of Stacks 0GXX (isAdic_adicCompletion) and clause (2) of this tag (hasSomeSurjectivePresentation_completionAlong').”. References: EGA I (10.8.6), “special case”.

Let S be a scheme, let X be an affine formal algebraic space over S, let i : X_red ⟶ X be a reduction of X and let T ⊆ |X_red| be closed. If X is Noetherian then so is the completion X_{/T} of X along T: it is presented by a topological ring which is both Noetherian and adic.

theorem isNoetherian_completionAlong' {X Xred : FppfSheaf B S hS}
    (hX : IsNoetherian B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T) :
    IsNoetherian B S hS (completionAlong i T)

AlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_completionAlong', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionAffineClausesVariants.lean, line 55. The attribute's comment: “clause (2): if X is McQuillan so is X_{/T}, with McQuillan read as HasSomeSurjectivePresentation (condition (4) of Stacks 0AIC, registered for Stacks 0AID at StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Types.lean). Carried hypotheses: hX is the tag's own McQuillan hypothesis on X, hi supplies the reduction as data because Stacks 0AIN is unavailable in this library (the convention of the library's Stacks 0GVT and 0GB8), and hT is the tag's own closedness of T in |X_red|. Nothing else: the source's step producing condition (2) of Stacks 0AIC for the completion is proved — hasAffineClosedImmersionCriterion_completionSheafULift, resting on completionClosedSubscheme_of_isAffineFormalAlgebraicSpace; and the set-theoretic condition of Stacks 0AIS on the completion is proved — satisfiesSetTheoreticCondition_completionSheafULift. The step from condition (2) to the conclusion is Stacks 0AIC, (2) ⇒ (5) ⇒ (4).”.

Clause (2) of Stacks 0GVV. Let S be a scheme, let X be a McQuillan affine formal algebraic space over S, let i : X_red ⟶ X be a reduction of X and let T ⊆ |X_red| be closed. Then the completion X_{/T} of X along T is again McQuillan, that is satisfies condition (4) of Stacks 0AIC: it is an affine formal algebraic space some presentation of which by affine thickenings has all its section-ring projections surjective.

Nothing is assumed beyond the tag's own hypotheses. This is AlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_completionSheafULift in the source's spelling X_{/T} for a closed subset T of the points of a reduction; the source's step — write X = Spf(A) and observe that X_{/T} ⟶ X ⟶ Spec(A) satisfies condition (2) of Stacks 0AIC — is AlgebraicGeometry.FormalSpace.hasAffineClosedImmersionCriterion_completionSheafULift, and the geometric content it rests on is AlgebraicGeometry.FormalSpace.completionClosedSubscheme_of_isAffineFormalAlgebraicSpace: a closed immersion of an object of the site into X_{/T} is a closed immersion into X.

theorem hasSomeSurjectivePresentation_completionAlong' {X Xred : FppfSheaf B S hS}
    (hX : HasSomeSurjectivePresentation B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T) :
    HasSomeSurjectivePresentation B S hS (completionAlong i T)

AlgebraicGeometry.FormalSpace.completionOfAffineIsAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionAffineSupplement.lean, line 1038. The attribute's comment: “clause (1), in the ambient spelling CompletionOfAffineIsAffine, quantified over the affine formal algebraic space and over the closed subset of its own points. No hypotheses beyond the tag's own: the set-theoretic condition of Stacks 0AIS on the completions is proved — satisfiesSetTheoreticCondition_completionSheafULift; the commutation of completion with directed colimits of fppf sheaves is proved — completionSheafULiftIsoColimitCompletion; Stacks 0AIY at the affine stages is isAffineFormalAlgebraicSpace_completionSheafULift_affineStageSheaf. No hred is needed, the ambient spelling mentioning no reduction. Clause (1) is Stacks 0GVQ, whose registration stays on isAffineFormalAlgebraicSpace_completionAlong' above”.

Clause (1) of Stacks 0GVV, in the ambient spelling AlgebraicGeometry.FormalSpace.CompletionOfAffineIsAffine: the completion of an affine formal algebraic space over S along a closed set of its points is again an affine formal algebraic space, for every such space and every such set at once. It is AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_completionAlong' (Stacks 0GVQ) with the reduction removed from the statement: the completion is formed along a closed set of points of the space itself, which is what the consumers of clause (1) in this library — the base-changed charts of Stacks 0GVR and Stacks 0GVW — supply, and so no hred is needed.

Nothing is assumed. The affine presentation is AlgebraicGeometry.FormalSpace.exists_affinePresentation_completionSheafULift and the set-theoretic condition of Stacks 0AIS is AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_completionSheafULift.

theorem completionOfAffineIsAffine : CompletionOfAffineIsAffine' B S hS
Tag 0GVW, a lemma

Tag 0GVW in the Stacks Project.

AlgebraicGeometry.FormalSpace.isLocallyCountablyIndexed_completionAlong', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionLocalTypes.lean, line 488. The attribute's comment: “clause (1): if the complement of T is quasi-compact and X is locally countably indexed then so is X_{/T} (IsLocallyCountablyIndexed, Stacks 0AKY). Binders are exactly the source's data: T closed in |X_red|, and quasi-compactness (Stacks 03HE, Space.IsQuasiCompactULift) of the inclusion of the open subspace |X_red| \ T (the subfunctor of sections with point-set image in Tᶜ). The set-theoretic condition of 0AIS is proved (0GVR), clause (1) of 0GVV is proved (completionOfAffineIsAffine), clause (3) of 0GVV is proved (isCountablyIndexed_completionAlong').”.

Clause (1) of Stacks 0GVW. Let S be a scheme, let X be a formal algebraic space over S, let i : X_red ⟶ X be a reduction of X and let T ⊆ |X_red| be closed such that the inclusion |X_red| \ T ⟶ |X_red| of the open subspace with points |X_red| \ T is quasi-compact. If X is locally countably indexed then so is the completion X_{/T} of X along T.

The open subspace |X_red| \ T is the subfunctor of the sections of X_red with point-set image in Tᶜ, and the hypothesis hqc is quasi-compactness of its inclusion in the sense of Stacks 03HE; see the section "The source's quasi-compactness hypothesis" of this file. It is transferred to the charts by complementCompactOnCharts_of_isQuasiCompactULift, and the statement follows from isLocallyCountablyIndexed_completionAlong_of_complementCompactOnCharts. Nothing else is assumed.

theorem isLocallyCountablyIndexed_completionAlong' {X Xred : FppfSheaf B S hS}
    (hX : IsLocallyCountablyIndexed B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T)
    (hqc : Space.IsQuasiCompactULift.{u + 1} B S hS
      (Space.completionSubfunctorULift B S hS Xred.obj Tᶜ).ι) :
    IsLocallyCountablyIndexed B S hS (completionAlong i T)

AlgebraicGeometry.FormalSpace.isLocallyAdicStar_completionAlong', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionLocalTypes.lean, line 552. The attribute's comment: “clause (2): if the complement of T is quasi-compact and X is locally adic* then so is X_{/T} (IsLocallyAdicStar, Stacks 0AKY). Binders are exactly the source's data: T closed in |X_red|, and quasi-compactness (Stacks 03HE, Space.IsQuasiCompactULift) of the inclusion of the open subspace |X_red| \ T (the subfunctor of sections with point-set image in Tᶜ). The set-theoretic condition of 0AIS is proved (0GVR), clause (4) of 0GVV is proved (isAdicStar_completionAlong').”.

Clause (2) of Stacks 0GVW. Let S be a scheme, let X be a formal algebraic space over S, let i : X_red ⟶ X be a reduction of X and let T ⊆ |X_red| be closed such that the inclusion |X_red| \ T ⟶ |X_red| of the open subspace with points |X_red| \ T is quasi-compact. If X is locally adic* then so is the completion X_{/T} of X along T.

The hypothesis hqc is read as for clause (1), isLocallyCountablyIndexed_completionAlong'. Nothing else is assumed.

theorem isLocallyAdicStar_completionAlong' {X Xred : FppfSheaf B S hS}
    (hX : IsLocallyAdicStar B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T)
    (hqc : Space.IsQuasiCompactULift.{u + 1} B S hS
      (Space.completionSubfunctorULift B S hS Xred.obj Tᶜ).ι) :
    IsLocallyAdicStar B S hS (completionAlong i T)

AlgebraicGeometry.FormalSpace.isLocallyNoetherian_completionAlong', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RecompletionLocalTypes.lean, line 603. The attribute's comment: “clause (3): if X is locally Noetherian then so is X_{/T} (IsLocallyNoetherian, Stacks 0AKY); deliberately NO quasi-compactness hypothesis, as in the source. Binders are exactly the source's data: T closed in |X_red|. The set-theoretic condition of 0AIS is proved (0GVR), clause (5) of 0GVV is proved (isNoetherian_completionAlong').”.

Clause (3) of Stacks 0GVW. Let S be a scheme, let X be a formal algebraic space over S, let i : X_red ⟶ X be a reduction of X and let T ⊆ |X_red| be closed. If X is locally Noetherian then so is the completion X_{/T} of X along T: the completions of the charts of X along the inverse images of T form an atlas as in Definition 0AIM, and each of them is a Noetherian affine formal algebraic space by clause (5) of Stacks 0GVV. No quasi-compactness hypothesis is needed, the source observing that it holds automatically because |X_red| is then the spectrum of a Noetherian ring.

Nothing is assumed beyond the source's hypotheses: the set-theoretic condition of Stacks 0AIS for X_{/T} is satisfiesSetTheoreticCondition_completionAlong_of_isFormalAlgebraicSpace (Stacks 0GVR), and clause (5) of Stacks 0GVV is AlgebraicGeometry.FormalSpace.isNoetherian_completionAlong'.

theorem isLocallyNoetherian_completionAlong' {X Xred : FppfSheaf B S hS}
    (hX : IsLocallyNoetherian B S hS X) {i : Xred ⟶ X}
    (hi : IsReduction B S hS X Xred i)
    (T : Set (Space.pointsULift.{u + 1} B S hS Xred.obj))
    (hT : @IsClosed _ (Space.pointTopologyULift.{u + 1} B S hS Xred.obj) T) :
    IsLocallyNoetherian B S hS (completionAlong i T)
Sources
LeanAlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_completionAlong' · AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_completionFunctor · AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_completionAlong' · AlgebraicGeometry.FormalSpace.completionAlong · AlgebraicGeometry.FormalSpace.isClosed_preimage_pointsMapULift · AlgebraicGeometry.FormalSpace.isPullback_completionAlongMap · AlgebraicGeometry.FormalSpace.isReduction_completionAlong · AlgebraicGeometry.FormalSpace.isCountablyIndexed_completionAlong

Section87.38 Completion along a closed subspace#

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

Tag 0GXU, a definition

Tag 0GXU in the Stacks Project.

AlgebraicGeometry.Space.completionSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceBaseChange.lean, line 185. The attribute's comment: “the completion along a closed subspace”.

Stacks 0GXU. The completion X^∧_Z of an algebraic space X over S along a closed subspace Z: the fppf sheafification of the union of the infinitesimal neighbourhoods of Z in X, which is their colimit in fppf sheaves.

def completionSubspace (X : AlgebraicSpaces B S hS) (Z : Subfunctor X.1) :
    Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))
Tag 0GXV, a lemma

Tag 0GXV in the Stacks Project.

AlgebraicGeometry.Space.isPullback_completionSubspaceMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceBaseChange.lean, line 270. The attribute's comment: “the square is cartesian”.

Stacks 0GXV. Completion along a closed subspace is compatible with base change: for a morphism f : X' ⟶ X of algebraic spaces over S and a subfunctor Z of X, in the source a closed subspace, the square formed by the completion of X' along Z' = f⁻¹(Z) = X' ×_X Z, the completion of X along Z and the two ambient sheaves is a cartesian square of fppf sheaves.

theorem isPullback_completionSubspaceMap {X' X : AlgebraicSpaces B S hS} (f : X' ⟶ X)
    (Z : Subfunctor X.1) :
    IsPullback
      (completionSubspaceToAmbient B S hS X' (Z.preimage f.hom))
      (completionSubspaceMap B S hS f Z)
      (sheafifiedULiftMap B S hS f.hom)
      (completionSubspaceToAmbient B S hS X Z)

AlgebraicGeometry.Space.isRepresentableByAlgebraicSpacesULift_completionSubspaceMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceBaseChange.lean, line 284. The attribute's comment: “representable by algebraic spaces”.

Stacks 0GXV. For a morphism f : X' ⟶ X of algebraic spaces over S and a subfunctor Z of X, in the source a closed subspace, the induced morphism of completions (X')^∧_{f⁻¹(Z)} ⟶ X^∧_Z is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpacesULift_completionSubspaceMap
    {X' X : AlgebraicSpaces B S hS} (f : X' ⟶ X) (Z : Subfunctor X.1) :
    IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
      (completionSubspaceMap B S hS f Z).hom
Tag 0GXW, a lemma

Tag 0GXW in the Stacks Project.

AlgebraicGeometry.FormalSpace.isReduction_completionSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionAlongClosedSubspaceReduction.lean, line 638. The attribute's comment: “the whole statement, under the additional hypothesis that the canonical morphism Z ⟶ X^∧_Z is a representable thickening; that is Tag 0AI9 for a colimit of algebraic spaces, which is available here only for a colimit of affine objects of the site”.

Stacks 0GXW. Let X be an algebraic space over S and let Z ⊆ X be a closed subspace. The reduction of the completion X^∧_Z of X along Z is Z_red: the composite Z_red ⟶ Z ⟶ X^∧_Z exhibits Z_red as the reduction of the completion.

The hypothesis is that the canonical morphism Z ⟶ X^∧_Z is a representable thickening. That is exactly what it is: Z = Z_0 is a stage of the colimit presentation of X^∧_Z by the infinitesimal neighbourhoods of Z, whose transition morphisms are thickenings, so Stacks 0AI9 applies. The library has Stacks 0AI9 only for a colimit of affine objects of the site, AlgebraicGeometry.FormalSpace.isThickening_colimitι, which is why the property is carried here as a hypothesis; see the module docstring.

theorem isReduction_completionSubspace
    (hc : Space.IsRepresentableThickeningULift.{u + 1} B S hS
      (closedSubspaceToCompletionSubspace B S hS hX Z hZ).hom) :
    IsReduction B S hS (Space.completionSubspace B S hS ⟨X, hX⟩ Z)
      (reductionOfClosedSubspaceSheaf B S hS hX Z hZ)
      (reductionInclusion B S hS hX Z hZ ≫
        closedSubspaceToCompletionSubspace B S hS hX Z hZ)

AlgebraicGeometry.FormalSpace.isReduction_completionSubspace', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceThickening.lean, line 240.

Stacks 0GXW. Let X be an algebraic space over S and let Z ⊆ X be a closed subspace. The reduction of the completion X^∧_Z of X along Z is Z_red: the composite Z_red ⟶ Z ⟶ X^∧_Z exhibits Z_red as the reduction of the completion.

Both morphisms are representable thickenings — the first because Z_red is a closed subspace of X contained in Z with the same point set, the second by AlgebraicGeometry.FormalSpace.isRepresentableThickeningULift_toCompletionSubspace — and Z_red is a reduced algebraic space, so the composite exhibits it as the reduction.

This is the unconditional form of AlgebraicGeometry.FormalSpace.isReduction_completionSubspace, which takes the representability of Z ⟶ X^∧_Z as a hypothesis.

theorem isReduction_completionSubspace' :
    IsReduction B S hS (Space.completionSubspace B S hS ⟨X, hX⟩ Z)
      (reductionOfClosedSubspaceSheaf B S hS hX Z hZ)
      (reductionInclusion B S hS hX Z hZ ≫
        closedSubspaceToCompletionSubspace B S hS hX Z hZ)
Tag 0GXX, a lemma

Tag 0GXX in the Stacks Project.

AlgebraicGeometry.FormalSpace.isWeaklyAdic_completionAlongIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineCompletionAlongIdeal.lean, line 849. The attribute's comment: “clause (1): weakly adic”.

Stacks 0GXX (1). For an affine scheme X = Spec A over S and the closed subscheme Z ⊆ X of an ideal I ⊆ A, the completion X^∧_Z of X along Z is a weakly adic affine formal algebraic space: it is the formal spectrum of the I-adic completion of A, whose topology is given by the closures of the powers of the ideal generated by I.

public theorem isWeaklyAdic_completionAlongIdeal (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {A : Type u} [CommRing A] (f : Spec (.of A) ⟶ S)
    (hA : B.Contains (Spec (.of A))) (I : Ideal A) :
    IsWeaklyAdic B S hS (completionAlongIdeal B S hS f hA I)

AlgebraicGeometry.FormalSpace.isAdic_and_iso_formalSpectrum_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineCompletionAlongIdeal.lean, line 930. The attribute's comment: “clause (2): formal spectrum of the adic completion”. References: EGA I (10.8.5), “affine case Spf(Â)”; EGA I (10.10.1), “Spf(A) = X_{/X}”; EGA III (5.1.1), “Spf(A) ≅ Ŷ”.

Stacks 0GXX (2). If I is finitely generated then the completion X^∧_Z of X = Spec A along the closed subscheme Z of I is Spf (A^∧) for the I-adic completion A^∧ of A: the topology of A^∧ is the adic topology of the ideal I A^∧, and X^∧_Z is the formal spectrum of A^∧.

public theorem isAdic_and_iso_formalSpectrum_adicCompletion (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) {A : Type u} [CommRing A] (f : Spec (.of A) ⟶ S)
    (hA : B.Contains (Spec (.of A))) (I : Ideal A) (hI : I.FG) :
    _root_.IsAdic (Ideal.map (algebraMap A (AdicCompletion I A)) I) ∧
      Nonempty (completionAlongIdeal B S hS f hA I ≅
        formalSpectrum (adicCompletionQuotientSystem B S hS f hA I))

AlgebraicGeometry.FormalSpace.isAdicStar_completionAlongIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineCompletionAlongIdeal.lean, line 943. The attribute's comment: “clause (3): adic star”.

Stacks 0GXX (3). If I is finitely generated — equivalently, if the closed subscheme Z ⊆ X = Spec A of I is of finite presentation over X — then the completion X^∧_Z is an adic* affine formal algebraic space: it is presented by the I-adic completion of A, which is adic with the finitely generated ideal of definition I A^∧.

public theorem isAdicStar_completionAlongIdeal (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {A : Type u} [CommRing A] (f : Spec (.of A) ⟶ S)
    (hA : B.Contains (Spec (.of A))) (I : Ideal A) (hI : I.FG) :
    IsAdicStar B S hS (completionAlongIdeal B S hS f hA I)

AlgebraicGeometry.FormalSpace.isNoetherian_completionAlongIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceLocalTypes.lean, line 410. The attribute's comment: “clause (4): Noetherian”. References: EGA I (10.8.6), “special case”.

Stacks 0GXX (4). For an affine scheme X = Spec A over S with A Noetherian and the closed subscheme Z ⊆ X of an ideal J ⊆ A, the completion X^∧_Z of X along Z is a Noetherian affine formal algebraic space: it is presented by the J-adic completion of A, which is a Noetherian ring by Stacks 0316 and which is adic with the finitely generated ideal of definition J A^∧ by Stacks 0GXX (2), the ideal J being finitely generated because A is Noetherian.

theorem isNoetherian_completionAlongIdeal {A : Type u} [CommRing A] [IsNoetherianRing A]
    (str : Spec (.of A) ⟶ S) (hA : B.Contains (Spec (.of A))) (J : Ideal A) :
    IsNoetherian B S hS (completionAlongIdeal B S hS str hA J)
Tag 0GXY, a lemma

Tag 0GXY in the Stacks Project.

AlgebraicGeometry.FormalSpace.isLocallyWeaklyAdic_completionSubspace_of_isClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceAtlas.lean, line 424. The attribute's comment: “part (1): locally weakly adic”.

Stacks 0GXY (1). Let S be a scheme, let X be an algebraic space over S and let Z ⊆ X be a closed subspace. The completion X^∧_Z of X along Z is locally weakly adic.

The completions of the affine étale charts of X along the inverse images of Z form an atlas of X^∧_Z (Stacks 0GXV), each is the completion of an affine scheme along an ideal, hence weakly adic by Stacks 0GXX (1), and X^∧_Z satisfies the set-theoretic condition of Stacks 0AIS by AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_completionSubspace.

theorem isLocallyWeaklyAdic_completionSubspace_of_isClosedSubspace {X : AlgebraicSpaces B S hS}
    (Z : Subfunctor X.1) (hZ : Space.IsClosedSubspace B S hS Z) :
    IsLocallyWeaklyAdic B S hS (Space.completionSubspace B S hS X Z)

AlgebraicGeometry.FormalSpace.isLocallyAdicStar_completionSubspace_of_isClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceAtlas.lean, line 443. The attribute's comment: “part (2): locally adic star”.

Stacks 0GXY (2). Let S be a scheme, let X be an algebraic space over S and let Z ⊆ X be a closed subspace such that Z ⟶ X is of finite presentation. The completion X^∧_Z of X along Z is locally adic*.

As in clause (1), with the members of the atlas adic* by Stacks 0GXX (3): finite presentation of Z ⟶ X makes the ideal cutting out the inverse image of Z on an affine chart finitely generated, AlgebraicGeometry.Space.fg_closedChartIdeal_of_isLocallyOfFinitePresentation.

theorem isLocallyAdicStar_completionSubspace_of_isClosedSubspace {X : AlgebraicSpaces B S hS}
    (Z : Subfunctor X.1) (hZ : Space.IsClosedSubspace B S hS Z)
    (hZfp : Space.IsFinitePresentation B S hS Z.ι) :
    IsLocallyAdicStar B S hS (Space.completionSubspace B S hS X Z)

AlgebraicGeometry.FormalSpace.isLocallyNoetherian_completionSubspace_of_isClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceAtlas.lean, line 464. The attribute's comment: “part (3): locally Noetherian”.

Stacks 0GXY (3). Let S be a scheme, let X be a locally Noetherian algebraic space over S and let Z ⊆ X be a closed subspace. The completion X^∧_Z of X along Z is locally Noetherian.

As in clause (1), with the members of the atlas Noetherian by Stacks 0GXX (4), AlgebraicGeometry.FormalSpace.isNoetherian_completionAlongIdeal: local Noetherianness of X is local in the étale topology (Stacks 03E8), so every étale chart of X is a locally Noetherian scheme and its ring of regular functions is Noetherian.

theorem isLocallyNoetherian_completionSubspace_of_isClosedSubspace {X : AlgebraicSpaces B S hS}
    (Z : Subfunctor X.1) (hZ : Space.IsClosedSubspace B S hS Z)
    (hXN : Space.HasEtaleLocalProperty B S hS X.1
      (fun T : Scheme.{u} ↦ _root_.AlgebraicGeometry.IsLocallyNoetherian T)) :
    IsLocallyNoetherian B S hS (Space.completionSubspace B S hS X Z)

AlgebraicGeometry.FormalSpace.isLocallyWeaklyAdic_completionSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceLocalTypes.lean, line 335. The attribute's comment: “part (1): locally weakly adic; charts and 0AIS condition assumed”.

Stacks 0GXY (1). Let S be a scheme, let X be an algebraic space over S and let Z ⊆ X be a closed subspace. The completion X^∧_Z of X along Z is locally weakly adic: the completions of the affine charts of X along the inverse images of Z form an atlas of X^∧_Z, and each of them is a weakly adic affine formal algebraic space by Stacks 0GXX (1).

The charts of X and the identification of their completions with completions of affine schemes along ideals are carried as hypotheses, as is the set-theoretic condition of Stacks 0AIS; see the section "What is assumed" of this file.

theorem isLocallyWeaklyAdic_completionSubspace
    {X : AlgebraicSpaces B S hS} (Z : Subfunctor X.1)
    {Ix : Type (u + 1)} (Xi : Ix → AlgebraicSpaces B S hS) (f : ∀ i, Xi i ⟶ X)
    (hf : ∀ i, ∃ hfi : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
        (Space.sheafifiedULiftMap B S hS (f i).hom).hom,
      Space.HasPropertyULift.{u + 1} B S hS
        (fun _ _ q ↦ Space.IsEtaleULift.{u + 1} B S hS q.hom)
        (Space.sheafifiedULiftMap B S hS (f i).hom).hom hfi)
    (hcov : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
          Sheaf.instHasColimitsOfSize
        Sheaf.IsLocallySurjective
          (Sigma.desc fun i ↦ Space.sheafifiedULiftMap B S hS (f i).hom))
    (hchart : ∀ i, ∃ (A : Type u) (_ : CommRing A) (str : Spec (.of A) ⟶ S)
      (hA : B.Contains (Spec (.of A))) (J : Ideal A),
      Nonempty (Space.completionSubspace B S hS (Xi i) (Z.preimage (f i).hom) ≅
        completionAlongIdeal B S hS str hA J))
    (hset : SatisfiesSetTheoreticCondition B S hS (Space.completionSubspace B S hS X Z)) :
    IsLocallyWeaklyAdic B S hS (Space.completionSubspace B S hS X Z)

AlgebraicGeometry.FormalSpace.isLocallyAdicStar_completionSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceLocalTypes.lean, line 372. The attribute's comment: “part (2): locally adic star; charts and 0AIS condition assumed”.

Stacks 0GXY (2). Let S be a scheme, let X be an algebraic space over S and let Z ⊆ X be a closed subspace with Z ⟶ X of finite presentation. The completion X^∧_Z of X along Z is locally adic*: the completions of the affine charts of X along the inverse images of Z form an atlas of X^∧_Z, and each of them is an adic* affine formal algebraic space by Stacks 0GXX (3), finite presentation of Z ⟶ X saying on an affine chart Spec A that the ideal cutting out the inverse image of Z is finitely generated.

The charts of X and the identification of their completions with completions of affine schemes along finitely generated ideals are carried as hypotheses, as is the set-theoretic condition of Stacks 0AIS; see the section "What is assumed" of this file.

theorem isLocallyAdicStar_completionSubspace
    {X : AlgebraicSpaces B S hS} (Z : Subfunctor X.1)
    {Ix : Type (u + 1)} (Xi : Ix → AlgebraicSpaces B S hS) (f : ∀ i, Xi i ⟶ X)
    (hf : ∀ i, ∃ hfi : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
        (Space.sheafifiedULiftMap B S hS (f i).hom).hom,
      Space.HasPropertyULift.{u + 1} B S hS
        (fun _ _ q ↦ Space.IsEtaleULift.{u + 1} B S hS q.hom)
        (Space.sheafifiedULiftMap B S hS (f i).hom).hom hfi)
    (hcov : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
          Sheaf.instHasColimitsOfSize
        Sheaf.IsLocallySurjective
          (Sigma.desc fun i ↦ Space.sheafifiedULiftMap B S hS (f i).hom))
    (hchart : ∀ i, ∃ (A : Type u) (_ : CommRing A) (str : Spec (.of A) ⟶ S)
      (hA : B.Contains (Spec (.of A))) (J : Ideal A), J.FG ∧
      Nonempty (Space.completionSubspace B S hS (Xi i) (Z.preimage (f i).hom) ≅
        completionAlongIdeal B S hS str hA J))
    (hset : SatisfiesSetTheoreticCondition B S hS (Space.completionSubspace B S hS X Z)) :
    IsLocallyAdicStar B S hS (Space.completionSubspace B S hS X Z)

AlgebraicGeometry.FormalSpace.isLocallyNoetherian_completionSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceLocalTypes.lean, line 435. The attribute's comment: “part (3): locally Noetherian; charts and 0AIS condition assumed”.

Stacks 0GXY (3). Let S be a scheme, let X be a locally Noetherian algebraic space over S and let Z ⊆ X be a closed subspace. The completion X^∧_Z of X along Z is locally Noetherian: the completions of the affine charts of X along the inverse images of Z form an atlas of X^∧_Z, and each of them is presented by the adic completion of the Noetherian chart ring, which is adic with a finitely generated ideal of definition by Stacks 0GXX (2).

The charts of X and the identification of their completions with completions of Noetherian affine schemes along ideals are carried as hypotheses, as is the set-theoretic condition of Stacks 0AIS; see the section "What is assumed" of this file.

theorem isLocallyNoetherian_completionSubspace
    {X : AlgebraicSpaces B S hS} (Z : Subfunctor X.1)
    {Ix : Type (u + 1)} (Xi : Ix → AlgebraicSpaces B S hS) (f : ∀ i, Xi i ⟶ X)
    (hf : ∀ i, ∃ hfi : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
        (Space.sheafifiedULiftMap B S hS (f i).hom).hom,
      Space.HasPropertyULift.{u + 1} B S hS
        (fun _ _ q ↦ Space.IsEtaleULift.{u + 1} B S hS q.hom)
        (Space.sheafifiedULiftMap B S hS (f i).hom).hom hfi)
    (hcov : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
          Sheaf.instHasColimitsOfSize
        Sheaf.IsLocallySurjective
          (Sigma.desc fun i ↦ Space.sheafifiedULiftMap B S hS (f i).hom))
    (hchart : ∀ i, ∃ (A : Type u) (_ : CommRing A) (str : Spec (.of A) ⟶ S)
      (hA : B.Contains (Spec (.of A))) (J : Ideal A) (_ : IsNoetherianRing A),
      Nonempty (Space.completionSubspace B S hS (Xi i) (Z.preimage (f i).hom) ≅
        completionAlongIdeal B S hS str hA J))
    (hset : SatisfiesSetTheoreticCondition B S hS (Space.completionSubspace B S hS X Z)) :
    IsLocallyNoetherian B S hS (Space.completionSubspace B S hS X Z)
Tag 0H8N, a lemma

Tag 0H8N in the Stacks Project.

AlgebraicGeometry.Space.isIso_completionSubspaceComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceComparison.lean, line 480. The attribute's comment: “the comparison is an isomorphism for a closed subspace of finite presentation”.

Stacks 0H8N, the positive half. Let X be an algebraic space over S and let Z ⊆ X be a closed subspace with point set T = |Z|. If Z ⟶ X is of finite presentation, the canonical morphism c : X^∧_Z ⟶ X_{/T} is an isomorphism.

Both sides are sheafifications of subfunctors of X, and c is the sheafification of the inclusion of the first into the second. That inclusion is injective on sections, hence locally injective; and it is locally surjective because the affine objects of the site generate the fppf topology (Stacks 021V) and over an affine object the two subfunctors agree, by AlgebraicGeometry.Space.mem_completionSubspaceSubfunctor_of_hasImageIn_of_isAffine. A locally bijective morphism of sheaves of types is an isomorphism.

The negative half of the source's statement — that c is not an isomorphism in general — is not formalized here; see the module documentation.

theorem isIso_completionSubspaceComparison (X : AlgebraicSpaces B S hS) (Z : Subfunctor X.1)
    (hZ : IsClosedSubspace B S hS Z) (hfp : IsFinitePresentation B S hS Z.ι) :
    IsIso (completionSubspaceComparison B S hS X Z)

AlgebraicGeometry.Space.not_isIso_completionSubspaceComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSubspaceCounterexample.lean, line 514. The attribute's comment: “the comparison is not an isomorphism in general”.

Stacks 0H8N, the negative half. There are a scheme S in a big fppf site B, an algebraic space X over S and a closed subspace Z ⊆ X for which the canonical morphism c : X^∧_Z ⟶ X_{/T}, T = |Z|, is not an isomorphism.

Take A = ℤ[x₀, x₁, x₂, …], S = X = Spec A and Z = Spec (A ⧸ I) the closed subscheme cut out by I = (x₀, x₁, x₂, …), which is not of finite presentation. The section Spec (A ⧸ (xₙ ^ (n+1) : n)) ⟶ Spec A is supported on |Z|, because every variable is nilpotent in the quotient and so dies in any field-valued point; but no infinitesimal neighbourhood of Z contains it, not even after an fppf covering, because the exponent needed to kill xₘ in the quotient grows with m while a covering supplies only finitely many exponents and detects vanishing faithfully.

theorem not_isIso_completionSubspaceComparison :
    ∃ (B : BigFppfSite.{0}) (S : Scheme.{0}) (hS : B.Contains S)
      (X : AlgebraicSpaces B S hS) (Z : Subfunctor X.1),
      IsClosedSubspace B S hS Z ∧
        ¬ IsIso (completionSubspaceComparison B S hS X Z)
Sources
LeanAlgebraicGeometry.Space.completionSubspace · AlgebraicGeometry.Space.isPullback_completionSubspaceMap · AlgebraicGeometry.Space.isRepresentableByAlgebraicSpacesULift_completionSubspaceMap · AlgebraicGeometry.FormalSpace.isReduction_completionSubspace · AlgebraicGeometry.FormalSpace.isReduction_completionSubspace' · AlgebraicGeometry.FormalSpace.isWeaklyAdic_completionAlongIdeal · AlgebraicGeometry.FormalSpace.isAdic_and_iso_formalSpectrum_adicCompletion · AlgebraicGeometry.FormalSpace.isAdicStar_completionAlongIdeal

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.