87.11 Formal algebraic spaces to 87.16 Separation axioms for…

Section87.11 Formal algebraic spaces#

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

Tag 0AIL, the section

Tag 0AIL in the Stacks Project.

AlgebraicGeometry.FormalSpace.formalAlgebraicSpaces_discussion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalAlgebraicSpaceSanityChecks.lean, line 188. The attribute's comment: “the unnumbered discussion of Definition 0AIM in the section: an affine formal algebraic space is a formal algebraic space; the members of a family as in Definition 0AIM are representable by schemes; surjectivity of the map from the coproduct as a map of sheaves may be replaced by surjectivity (Bootstrap, Lemma 04S1). Also records that an affine formal algebraic space is quasi-compact”.

Stacks 0AIL, the discussion following Definition 0AIM in Section 87.11, "Formal algebraic spaces". Over a scheme S contained in a big fppf site:

  1. (sanity check) every affine formal algebraic space is a formal algebraic space;
  2. in the situation of Definition 0AIM — a family of maps fᵢ : Xᵢ ⟶ X of fppf sheaves whose sources are affine formal algebraic spaces and which are representable by algebraic spaces and étale — every fᵢ is representable by schemes, that is, by objects of the site (Lemma 0AIG);
  3. (Bootstrap, Lemma 04S1) Definition 0AIM is unchanged if the requirement that ∐ Xᵢ ⟶ X be surjective as a map of sheaves is replaced by the requirement that it be surjective, meaning that each of its base changes along a scheme of the site mapping to X is surjective.

The last conjunct records that an affine formal algebraic space is moreover a quasi-compact formal algebraic space (Definition 0AJA, through condition (3) of Lemma 0AJ9), its identity being a surjective representable étale chart.

theorem formalAlgebraicSpaces_discussion :
    letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) := Sheaf.instHasColimitsOfSize
    (∀ X : FppfSheaf B S hS,
      IsAffineFormalAlgebraicSpace B S hS X → IsFormalAlgebraicSpace B S hS X) ∧
    (∀ (X : FppfSheaf B S hS) (I : Type (u + 1)) (Xi : I → FppfSheaf B S hS)
      (f : ∀ i, Xi i ⟶ X), (∀ i, IsAffineFormalAlgebraicSpace B S hS (Xi i)) →
      (∀ i, ∃ hfi : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (f i).hom,
        Space.HasPropertyULift.{u + 1} B S hS
          (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) (f i).hom hfi) →
      ∀ i, uliftYoneda.{u + 1}.relativelyRepresentable (f i).hom) ∧
    (∀ X : FppfSheaf B S hS,
      IsFormalAlgebraicSpace B S hS X ↔
        SatisfiesSetTheoreticCondition B S hS X ∧
          ∃ (I : Type (u + 1)) (Xi : I → FppfSheaf B S hS) (f : ∀ i, Xi i ⟶ X),
            (∀ i, IsAffineFormalAlgebraicSpace B S hS (Xi i)) ∧
            (∀ i, ∃ hfi : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (f i).hom,
              Space.HasPropertyULift.{u + 1} B S hS
                (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) (f i).hom hfi) ∧
            IsSurjectiveOnSchemeBaseChanges B S hS (Sigma.desc f)) ∧
    (∀ X : FppfSheaf B S hS,
      IsAffineFormalAlgebraicSpace B S hS X → IsQuasiCompactSpace B S hS X)
Tag 0AIM, a definition

Tag 0AIM in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsFormalAlgebraicSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Defs.lean, line 50.

An fppf sheaf on the big fppf site of S is a formal algebraic space over S when it satisfies the set-theoretic condition of Stacks 0AIS and admits an atlas by affine formal algebraic spaces: a family of maps into it whose sources are affine formal algebraic spaces, each of which is representable by algebraic spaces and étale, and whose induced map from the coproduct is a surjection of sheaves.

abbrev IsFormalAlgebraicSpace (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : FppfSheaf B S hS) : Prop
Tag 0AIP, a lemma

Tag 0AIP in the Stacks Project.

AlgebraicGeometry.FormalSpace.relativelyRepresentable_diag_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/DiagonalRepresentable.lean, line 1010. The attribute's comment: “representable by schemes, for an arbitrary formal algebraic space”.

Stacks 0AIP, representability, for an arbitrary formal algebraic space: the absolute diagonal of a formal algebraic space over S is representable by objects of the big fppf site of S.

The diagonal is representable exactly when every morphism into the space from a sheaf represented by an object of the site is, and that is AlgebraicGeometry.FormalSpace.hasRepresentableRelativeProducts_of_isFormalAlgebraicSpace.

theorem relativelyRepresentable_diag_of_isFormalAlgebraicSpace
    {X : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X) :
    (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (diag X)

AlgebraicGeometry.FormalSpace.relative_locallyOfFiniteType_diag_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/DiagonalRepresentable.lean, line 1164. The attribute's comment: “locally of finite type, for an arbitrary formal algebraic space”.

Stacks 0AIP, local finite type, for an arbitrary formal algebraic space: every represented base change of the absolute diagonal of a formal algebraic space over S is a locally of finite type morphism of objects of the big fppf site of S.

This is the assertion on underlying presheaves, …relative_locallyOfFiniteType_diag_hom_of_isFormalAlgebraicSpace, transported to the sheaf category, which is where Stacks 0AIP and Stacks 0AN2 are stated.

theorem relative_locallyOfFiniteType_diag_of_isFormalAlgebraicSpace
    {X : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (diag X)

AlgebraicGeometry.FormalSpace.relative_locallyQuasiFinite_diag_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/DiagonalRepresentable.lean, line 1182. The attribute's comment: “locally quasi-finite, for an arbitrary formal algebraic space”.

Stacks 0AIP, local quasi-finiteness, for an arbitrary formal algebraic space: every represented base change of the absolute diagonal of a formal algebraic space over S is a locally quasi-finite, locally of finite type morphism of schemes.

The base change is locally of finite type by …relative_locallyOfFiniteType_diag_of_isFormalAlgebraicSpace and a monomorphism because the diagonal is, and a monomorphism of schemes locally of finite type is locally quasi-finite, which is Stacks 0CT8.

theorem relative_locallyQuasiFinite_diag_of_isFormalAlgebraicSpace
    {X : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X) :
    (MorphismProperty.inverseImage
      ((@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) ⊓
        (@AlgebraicGeometry.LocallyQuasiFinite.{u} : MorphismProperty Scheme.{u}))
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (diag X)

AlgebraicGeometry.FormalSpace.relative_isSeparated_diag_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/DiagonalRepresentable.lean, line 1205. The attribute's comment: “separated, for an arbitrary formal algebraic space”.

Stacks 0AIP, separatedness, for an arbitrary formal algebraic space: every represented base change of the absolute diagonal of a formal algebraic space over S is a separated morphism of schemes.

This one needs only the representability assertion: the base change is a monomorphism because the diagonal is, and a monomorphism of schemes is separated.

theorem relative_isSeparated_diag_of_isFormalAlgebraicSpace
    {X : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.IsSeparated.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (diag X)

AlgebraicGeometry.FormalSpace.relativelyRepresentable_diag_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RelativeDiagonal.lean, line 199. The attribute's comment: “representable by schemes, for an affine formal algebraic space”.

The absolute diagonal of an affine formal algebraic space is representable by objects of the site.

theorem relativelyRepresentable_diag_of_isAffineFormal {X : FppfSheaf B S hS}
    (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable (diag X)

AlgebraicGeometry.FormalSpace.relative_locallyQuasiFinite_diag_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RelativeDiagonal.lean, line 207. The attribute's comment: “locally quasi-finite, for an affine formal algebraic space”.

Every represented base change of the absolute diagonal of an affine formal algebraic space is a locally quasi-finite, locally of finite type morphism of schemes.

theorem relative_locallyQuasiFinite_diag_of_isAffineFormal {X : FppfSheaf B S hS}
    (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    (MorphismProperty.inverseImage
      ((@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) ⊓
        (@AlgebraicGeometry.LocallyQuasiFinite.{u} : MorphismProperty Scheme.{u}))
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (diag X)

AlgebraicGeometry.FormalSpace.relative_locallyOfFiniteType_diag_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RelativeDiagonal.lean, line 222. The attribute's comment: “locally of finite type, for an affine formal algebraic space”.

Every represented base change of the absolute diagonal of an affine formal algebraic space is a locally of finite type morphism of schemes.

theorem relative_locallyOfFiniteType_diag_of_isAffineFormal {X : FppfSheaf B S hS}
    (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (diag X)

AlgebraicGeometry.FormalSpace.relative_isSeparated_diag_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RelativeDiagonal.lean, line 234. The attribute's comment: “separated, for an affine formal algebraic space”.

Every represented base change of the absolute diagonal of an affine formal algebraic space is a separated morphism of schemes.

theorem relative_isSeparated_diag_of_isAffineFormal {X : FppfSheaf B S hS}
    (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.IsSeparated.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (diag X)

AlgebraicGeometry.FormalSpace.mono_diag_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RelativeDiagonal.lean, line 247. The attribute's comment: “monomorphism, for an arbitrary formal algebraic space”.

The absolute diagonal of a formal algebraic space over S is a monomorphism of fppf sheaves, which by Stacks 0AQB is what it is for a morphism of formal algebraic spaces to be a monomorphism.

theorem mono_diag_of_isFormalAlgebraicSpace {X : FppfSheaf B S hS}
    (_hX : IsFormalAlgebraicSpace B S hS X) : Mono (diag X)

Declarations registered for the tag:

Tag 0AIQ, a lemma

Tag 0AIQ in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRepresentableByAlgebraicSpacesULift_of_isAlgebraicSpaceULift_of_isFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/DiagonalRepresentable.lean, line 993. The attribute's comment: “for an arbitrary formal algebraic space target, carrying nothing: the representable-relative-products hypothesis is discharged by this module's own Stacks 0AIP”.

Stacks 0AIQ for an arbitrary formal algebraic space target. A morphism of fppf sheaves whose source is an algebraic space over S and whose target is a formal algebraic space over S is representable by algebraic spaces.

This carries nothing. isRepresentableByAlgebraicSpacesULift_of_isAlgebraicSpaceULift (MapsFromAlgebraicSpace) states the implication with the target's representable relative products as a hypothesis, and that hypothesis is the theorem above -- the representability assertion of Stacks 0AIP. It is stated here rather than beside that theorem because MapsFromAlgebraicSpace lies in this module's import closure and not conversely, so the discharge can only be written downstream.

theorem isRepresentableByAlgebraicSpacesULift_of_isAlgebraicSpaceULift_of_isFormal
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : Space.IsAlgebraicSpaceULift.{u + 1} B S hS X.obj)
    (hY : IsFormalAlgebraicSpace B S hS Y) :
    Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom

AlgebraicGeometry.FormalSpace.isRepresentableByAlgebraicSpacesULift_of_isAlgebraicSpaceULift_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MapsFromAlgebraicSpace.lean, line 134. The attribute's comment: “for a target which is an affine formal algebraic space, that being the case in which this library has Stacks 0AIP”.

Stacks 0AIQ when the target is an affine formal algebraic space. A morphism of fppf sheaves from an algebraic space over S to an affine formal algebraic space over S is representable by algebraic spaces, the relative products of the target being representable by Stacks 0AI8.

theorem isRepresentableByAlgebraicSpacesULift_of_isAlgebraicSpaceULift_of_isAffineFormal
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : Space.IsAlgebraicSpaceULift.{u + 1} B S hS X.obj)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y) :
    Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom
Tag 0AIR, a remark

Tag 0AIR in the Stacks Project.

AlgebraicGeometry.full_formalSchemePointsFunctor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsFullSupplement.lean, line 104. The attribute's comment: “fullness of the embedding by the functor of points, on all schemes”.

The functor of points of formal schemes on the category of all schemes is full, with no size hypothesis.

instance full_formalSchemePointsFunctor : formalSchemePointsFunctor.{u}.Full

AlgebraicGeometry.fullyFaithfulFormalSchemePointsFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsFullSupplement.lean, line 111. The attribute's comment: “the assignment 𝔛 ↦ h_𝔛 is a fully faithful embedding of formal schemes into presheaves on schemes”.

Taking the functor of points on the category of all schemes is a fully faithful embedding of the category of formal schemes into presheaves of sets on schemes.

noncomputable def fullyFaithfulFormalSchemePointsFunctor :
    formalSchemePointsFunctor.{u}.FullyFaithful

AlgebraicGeometry.faithful_formalSchemePointsFunctor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsSheaf.lean, line 81. The attribute's comment: “faithfulness of the embedding by the functor of points, on all schemes”.

The functor of points of formal schemes on the category of all schemes is faithful.

instance faithful_formalSchemePointsFunctor : formalSchemePointsFunctor.{u}.Faithful

AlgebraicGeometry.FormalSpace.relative_isOpenImmersion_openFormalSubschemePresheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeComparisonAtlas.lean, line 504. The attribute's comment: “the morphisms h_{𝔛ᵢ} ⟶ h_𝔛 of an open covering are representable and open immersions”.

Stacks 0AIR, clause (4). The morphism h_{𝔛|_𝔘} ⟶ h_𝔛 of fppf sheaves on the big fppf site of S is representable and an open immersion: it is representable by morphisms of the site, and every morphism of the site representing a base change of it is an open immersion of schemes. Nothing is assumed of 𝔛, of 𝔘 or of the base scheme S.

The base change along a point g of 𝔛 over T is the inclusion of the open subscheme g⁻¹(𝔘) of T, which is AlgebraicGeometry.FormalSpace.isPullback_chart; any other morphism of the site representing the same base change differs from it by an isomorphism, the universe-lifted Yoneda embedding being fully faithful.

theorem relative_isOpenImmersion_openFormalSubschemePresheafHom :
    (MorphismProperty.inverseImage (@AlgebraicGeometry.IsOpenImmersion.{u} :
        MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS)).relative
      (uliftYoneda.{u + 1}) (openFormalSubschemePresheafHom B S hS X V hV)

AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_openFormalSubschemePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeComparisonAtlas.lean, line 612. The attribute's comment: “the charts h_{𝔛ᵢ} of an affine open covering are affine formal algebraic spaces”.

Stacks 0AIR, clause (3). For a member 𝔛|_𝔘 of an affine open covering of 𝔛 — an open of 𝔛 whose restriction is isomorphic to the formal spectrum of an admissible topological ring A — the functor of points h_{𝔛|_𝔘} is an affine formal algebraic space over S.

This is Stacks 0AIE, AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_formalSchemePointsFppfSheaf, transported along the chart isomorphism, the functor of points being a functor of the formal scheme. The source's own hypotheses are kept: the base is terminal, as the source assumes it is Spec(ℤ), and the quotient spectra of A and their coproduct belong to the chosen big fppf site, which is the datum D and the condition hB.

theorem isAffineFormalAlgebraicSpace_openFormalSubschemePoints (hterm : IsTerminal S)
    (hA : TopologicalRing.IsAdmissible A) (D : QuotientSystem B S hS A) (hB : D.HasLargeSite)
    (e : (X.obj.restrict V).toPresheafedSpace ≅ (spfLTRS A hA.1).toPresheafedSpace) :
    IsAffineFormalAlgebraicSpace B S hS
      (formalSchemePointsFppfSheaf B S hS (openFormalSubscheme X V hV))

AlgebraicGeometry.FormalSpace.fullyFaithfulFormalSchemePointsFppfSheafFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeComparisonAtlas.lean, line 735. The attribute's comment: “the assignment 𝔛 ↦ h_𝔛 is a fully faithful embedding of formal schemes into the fppf sheaves on the big fppf site of the base”.

Stacks 0AIR, clause (2). The assignment 𝔛 ↦ h_𝔛 is a fully faithful embedding of the category of formal schemes into the category AlgebraicGeometry.FormalSpace.FppfSheaf B S hS of fppf sheaves on the big fppf site of S — the category in which formal algebraic spaces over S live, and the one the comparison of Stacks 0AIR is about.

The source's "modulo set theoretic issues" is the restriction of the source category to the formal schemes whose affine chart quotients belong to the big fppf site, which is the size condition of Stacks 0AI1 for the site's cutoff, and the source's assumption that the base is Spec(ℤ) is the hypothesis hterm. Both halves are Stacks 0AI1 read on the site: AlgebraicGeometry.FormalSpace.injective_map_formalSchemePointsFppfSheafFunctor and AlgebraicGeometry.FormalSpace.exists_map_eq_formalSchemePointsFppfSheafFunctor.

def fullyFaithfulFormalSchemePointsFppfSheafFunctor (hterm : IsTerminal S) :
    (sizeBoundedFormalSchemePointsFppfSheafFunctor B S hS).FullyFaithful

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpaceFormalSchemePoints_of_affineCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeComparisonAtlas.lean, line 811. The attribute's comment: “the functor of points of a formal scheme with an affine open covering is a formal algebraic space”.

Stacks 0AIR, clause (5). The functor of points of a formal scheme à la EGA is a formal algebraic space over S, for a formal scheme admitting an open covering 𝔛 = ⋃ 𝔘_i whose charts have affine formal algebraic space functors of points and whose own functor of points satisfies the set-theoretic condition of Stacks 0AIS.

This is the last sentence of the source's remark. The family {h_{𝔛|_{𝔘_i}} ⟶ h_𝔛} is a family as in Definition 0AIM: the sources are affine formal algebraic spaces, which is the hypothesis haff supplied by AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_openFormalSubschemePoints; the arrows are representable open immersions, hence representable étale, which is AlgebraicGeometry.FormalSpace.isRepresentableEtale_openFormalSubschemeSheafHom; and the family is jointly surjective, which is AlgebraicGeometry.FormalSpace.isLocallySurjective_sigmaDesc_openFormalSubschemeSheafHom. The conclusion is then Stacks 0AJ1, AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_etaleCover.

The hypothesis hset is the source's "modulo set theoretic issues" in the precise form of Stacks 0AIS, and it is the only thing the source leaves to the reader here.

theorem isFormalAlgebraicSpaceFormalSchemePoints_of_affineCover
    (hcov : ∀ p : X.obj, ∃ i, p ∈ U i)
    (haff : ∀ i, IsAffineFormalAlgebraicSpace B S hS
      (formalSchemePointsFppfSheaf B S hS (openFormalSubscheme X (U i) (hU i))))
    (hset : SatisfiesSetTheoreticCondition B S hS (formalSchemePointsFppfSheaf B S hS X)) :
    IsFormalAlgebraicSpaceFormalSchemePoints B S hS X

AlgebraicGeometry.FormalSpace.fullyFaithfulComparableFormalSchemePointsFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeComparisonAtlas.lean, line 864. The attribute's comment: “the category of formal schemes is equivalent to a full subcategory of the category of formal algebraic spaces”.

Stacks 0AIR, the comparison. The category of formal schemes à la EGA is equivalent to a full subcategory of the category of formal algebraic spaces over S: the functor 𝔛 ↦ h_𝔛 from the formal schemes the comparison applies to into the formal algebraic spaces over S is fully faithful, so it is an equivalence onto the full subcategory on its image.

This is the opening sentence of the source's remark. Its "modulo set theoretic issues" is the restriction of the source category to AlgebraicGeometry.FormalSpace.comparableFormalSchemes, and the source's assumption that the base is Spec(ℤ) is the hypothesis hterm. Full faithfulness is clause (2), AlgebraicGeometry.FormalSpace.fullyFaithfulFormalSchemePointsFppfSheafFunctor, and the functor lands in formal algebraic spaces by clause (5).

def fullyFaithfulComparableFormalSchemePointsFunctor (hterm : IsTerminal S) :
    (comparableFormalSchemePointsFunctor B S hS).FullyFaithful

AlgebraicGeometry.FormalSpace.isFppfSheafFormalSchemePoints_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeComparisonSheaf.lean, line 133. The attribute's comment: “the functor of points is an fppf sheaf, for a formal scheme that is a scheme”.

Stacks 0AIR, the sheaf clause, for a formal scheme isomorphic to a scheme: its functor of points satisfies the fppf sheaf condition on the big fppf site of S, with no hypothesis assumed.

The functor of points of a scheme seen as a formal scheme is the presheaf it represents and the fpqc topology is subcanonical, which is AlgebraicGeometry.isSheaf_fpqcTopology_formalSchemePoints_of_iso.

theorem isFppfSheafFormalSchemePoints_of_iso {X : FormalScheme.{u}} {Z : Scheme.{u}}
    (e : X ≅ schemeToFormalScheme.obj Z) : IsFppfSheafFormalSchemePoints B S hS X

AlgebraicGeometry.FormalSpace.isFppfSheafFormalSchemePoints_formalScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeComparisonSheaf.lean, line 164. The attribute's comment: “the functor of points of an arbitrary formal scheme is an fppf sheaf”.

Stacks 0AIR, the sheaf clause, for an arbitrary formal scheme: the functor of points of a formal scheme à la EGA satisfies the fppf sheaf condition on the big fppf site of S, with no hypothesis assumed.

This is the first sentence of the source's remark, "by Lemma 87.2.2 the functor of points h_𝔛 associated to a formal scheme 𝔛 is a sheaf in the fppf topology". It is AlgebraicGeometry.isSheaf_fpqcTopology_formalSchemePoints, the full statement of Stacks 0AI2, read on the big fppf site of S by AlgebraicGeometry.FormalSpace.isFppfSheafFormalSchemePoints_of_isSheaf_fpqcTopology.

theorem isFppfSheafFormalSchemePoints_formalScheme (X : FormalScheme.{u}) :
    IsFppfSheafFormalSchemePoints B S hS X
Tag 0AIS, a remark

Tag 0AIS in the Stacks Project.

AlgebraicGeometry.FormalSpace.SatisfiesSetTheoreticCondition, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine.lean, line 73. The attribute's comment: “the set-theoretic condition”.

An fppf sheaf satisfies the set-theoretic condition when there is a representable sheaf surjecting onto it and a representable sheaf surjecting onto the kernel pair of that surjection. Representability is recorded by an isomorphism of underlying presheaves with a universe-lifted Yoneda presheaf.

abbrev SatisfiesSetTheoreticCondition (X : FppfSheaf B S hS) : Prop

AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_of_bounded_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/BoundedColimit.lean, line 123. The attribute's comment: “bounded_colimit”.

Stacks 0AIS, bounded colimit. A directed colimit of affine fppf sheaves along thickenings satisfies the set-theoretic condition as soon as one cardinal μ below the size cutoff of the site bounds both the index and the size of every stage.

The coproduct of the stages is then an object of the site — a coproduct of at most μ schemes of size at most μ has size at most μ, by AlgebraicGeometry.schemeSize_coproduct_le — and its universe-lifted representable sheaf is the coproduct of those of the stages, which is the hypothesis of AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_of_colimit.

Nothing is asked of the cofinality of the cutoff, and the index may be uncountable: the uniform bound dominates the supremum of the stage sizes outright.

theorem satisfiesSetTheoreticCondition_of_bounded_colimit
    {I : Type (u + 1)} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (D : I ⥤ BigAffineFppf B S hS)
    (hD : ∀ ⦃i j : I⦄ (f : i ⟶ j),
      Stacks.Thickenings.IsThickening ((BigAffineFppf.toScheme B S hS).map (D.map f)))
    {μ : Cardinal.{u}} (hμ : μ < B.cutoff) (hI : #I ≤ Cardinal.lift.{u + 1, u} μ)
    (hstage : ∀ i : I, ((BigAffineFppf.toScheme B S hS).obj (D.obj i)).size ≤ μ)
    (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1)))
    (hX : Nonempty (X ≅ colimit
      (D ⋙ BigAffineFppf.inclusion B S hS ⋙
        Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)))) :
    SatisfiesSetTheoreticCondition B S hS X

AlgebraicGeometry.FormalSpace.exists_representable_epi_of_countable_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountableAtlas.lean, line 174. The attribute's comment: “observation (3), countable atlas”.

Stacks 0AIS, observation (3), first half. Let {Xᵢ ⟶ X} be a family of maps of fppf sheaves over S satisfying conditions (1), (2) and (3) of Definition 0AIM, with a countable index. Then there is an object U of the big fppf site of S and a surjection of fppf sheaves from the sheaf it represents onto X.

The surjection Uᵢ ⟶ Xᵢ from an object of the site onto each member of the family is the first half of the set-theoretic condition of Stacks 0AIS, which the hypothesis that Xᵢ is an affine formal algebraic space carries; countability makes the coproduct U = ∐ Uᵢ an object of the site, the size cutoff of a big fppf site having uncountable cofinality.

theorem exists_representable_epi_of_countable_atlas (X : FppfSheaf B S hS)
    {I : Type (u + 1)} [Countable I] (Xi : I → FppfSheaf B S hS) (f : ∀ i, Xi i ⟶ X)
    (hatlas : IsFormalAtlas B S hS X Xi f) :
    ∃ (U : BigFppfOver B S hS)
      (t : (BigFppfOver.topology B S hS).uliftYoneda.{u + 1}.obj U ⟶ X), Epi t

AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_of_countable_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountableAtlas.lean, line 405. The attribute's comment: “observation (3)”.

Stacks 0AIS, observation (3). Let {Xᵢ ⟶ X} be a family of maps of fppf sheaves over S satisfying conditions (1), (2) and (3) of Definition 0AIM with a countable index. Then X satisfies the set-theoretic condition of Stacks 0AIS.

Countability provides the object U of the site surjecting onto X (AlgebraicGeometry.FormalSpace.exists_representable_epi_of_countable_atlas). For the relation it provides the second half as well. The kernel pair U ×_X U is covered by the family of fibre products (U ×_X Xᵢ) ×_{Xᵢ} (U ×_X Xᵢ), one for each member of the atlas: that family is the base change of U ×_X U along the surjection ∐ Xᵢ ⟶ X of condition (3), decomposed along the coproduct, coproducts of sheaves of sets being stable under base change. Each member is an algebraic space over S — this is the step of Stacks 0AIP available unconditionally in this library, AlgebraicGeometry.FormalSpace.isAlgebraicSpaceULift_pullback_snd_pullback_snd — and an algebraic space over S receives a surjection of sheaves from an object of the site, that being what its étale scheme atlas is by Definition 025Y. The coproduct of those atlases, one for each index, is an object of the site because the index is countable and the size cutoff of a big fppf site has uncountable cofinality; it is the required R.

theorem satisfiesSetTheoreticCondition_of_countable_atlas (X : FppfSheaf B S hS)
    {I : Type (u + 1)} [Countable I] (Xi : I → FppfSheaf B S hS) (f : ∀ i, Xi i ⟶ X)
    (hatlas : IsFormalAtlas B S hS X Xi f) :
    SatisfiesSetTheoreticCondition B S hS X

AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_of_countable_atlas_of_hasQuasiCompactDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountableAtlas.lean, line 518. The attribute's comment: “observation (3), the source's quasi-compact diagonal”.

Stacks 0AIS, observation (3), as the source states it. Let {Xᵢ ⟶ X} be a family of maps of fppf sheaves over S satisfying conditions (1), (2) and (3) of Definition 0AIM with a countable index, and let the diagonal of X be quasi-compact, that is, let X be quasi-separated over S. Then X satisfies the set-theoretic condition of Stacks 0AIS.

Quasi-separatedness of X over S is quasi-compactness of the relative diagonal of its structure morphism in the sense of Stacks 0ARN part (2), the structure morphism being the morphism to the terminal object of the category of fppf sheaves on the big fppf site of S, whose relative self-product is therefore X ×_S X. It is the source's hypothesis, and the source is right that it suffices; it is not needed, and AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_of_countable_atlas proves the same conclusion from the countable atlas alone. The reason is that the source bounds the size of the relation R by that of U ×_S U, for which it needs the diagonal to be tame, whereas the argument here never leaves the site: the relation is assembled from the étale scheme atlases of the members of a countable cover of U ×_X U, and those are objects of the site by the definition of an algebraic space.

theorem satisfiesSetTheoreticCondition_of_countable_atlas_of_hasQuasiCompactDiagonal
    (X : FppfSheaf B S hS) {I : Type (u + 1)} [Countable I] (Xi : I → FppfSheaf B S hS)
    (f : ∀ i, Xi i ⟶ X) (hatlas : IsFormalAtlas B S hS X Xi f)
    (hdiag : HasQuasiCompactDiagonal B S hS (terminal.from X)) :
    SatisfiesSetTheoreticCondition B S hS X

AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_of_countable_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountableColimit.lean, line 264. The attribute's comment: “countable_colimit”.

Stacks 0AIS, countable colimit. A countable directed colimit of affine fppf sheaves along thickenings satisfies the set-theoretic condition.

Countability replaces the representability hypothesis on the coproduct of the stages in AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_of_colimit: a countable coproduct is itself represented by an object of the big fppf site. What the argument uses is only that a countable index is admissible for coproducts in the site, so this is the countable case of AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_of_admissible_colimit.

theorem satisfiesSetTheoreticCondition_of_countable_colimit (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) {I : Type (u + 1)} [Preorder I] [Nonempty I]
    [IsDirected I (· ≤ ·)] [Countable I] (D : I ⥤ BigAffineFppf B S hS)
    (hD : ∀ ⦃i j : I⦄ (f : i ⟶ j),
      Stacks.Thickenings.IsThickening ((BigAffineFppf.toScheme B S hS).map (D.map f)))
    (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1)))
    (hX : Nonempty (X ≅ colimit
      (D ⋙ BigAffineFppf.inclusion B S hS ⋙
        Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)))) :
    SatisfiesSetTheoreticCondition B S hS X

AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_of_representable_over_affineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableOverAffineSetCondition.lean, line 155. The attribute's comment: “the condition for the source of a morphism to an affine formal algebraic space which is representable by algebraic spaces, which is the first conjunct of the conclusion of Stacks 0AJH”.

The set-theoretic condition of Stacks 0AIS for the source of a morphism to an affine formal algebraic space representable by algebraic spaces. This is the first conjunct of the conclusion of Stacks 0AJH, discharged.

The condition on Y supplies one object U of the site with h_U ⟶ Y a surjection of sheaves. The fibre product W = h_U ×_Y X is then an algebraic space over S, and W ⟶ X is a surjection of sheaves, so the étale scheme atlas h_V ⟶ W of W composes to a surjection a : h_V ⟶ X from a representable. That atlas is representable by objects of the site and W ⟶ X is a base change of h_U ⟶ Y, which is representable by objects of the site because an affine formal algebraic space has representable relative products (Stacks 0AI8); so a is representable by algebraic spaces, h_V ×_X h_V is an algebraic space by Stacks 03XY, and the étale scheme atlas of h_V ×_X h_V is the second half of the condition.

theorem satisfiesSetTheoreticCondition_of_representable_over_affineFormal
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom) :
    SatisfiesSetTheoreticCondition B S hS X

AlgebraicGeometry.FormalSpace.isAlgebraicSpace_of_affineSchemeAtlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SchemeAtlas.lean, line 736. The attribute's comment: “observation (2)”.

Stacks 0AIS, observation (2), the sanity check. A family {Xᵢ ⟶ X} as in Definition 0AIM — the set-theoretic condition included — in which every Xᵢ is an affine scheme makes X an algebraic space.

The affine schemes of the family need not be objects of the chosen site; each is presented by its restricted functor of points, sheafified. The scheme atlas of the conclusion is assembled inside the chosen site rather than by descent from a larger one: the set-theoretic condition gives an object U of the site surjecting onto X, each Xᵢ is then represented by an affine object of the site of size at most that of U, and the coproduct of one such for each point of U is an object of the site because the size cutoff is a strong prelimit.

The diagonal is not a hypothesis: the atlas assembled here is representable by objects of the site, so Stacks 0BGR gives the algebraic-space condition outright.

public theorem isAlgebraicSpace_of_affineSchemeAtlas
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : Sheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) (Type (u + 1)))
    (hX : AlgebraicGeometry.FormalSpace.IsFormalAlgebraicSpace B S hS X)
    (hAtlas :
      let J := AlgebraicGeometry.BigFppfOver.topology B S hS
      letI : HasColimitsOfSize.{u + 1, u + 1} (Sheaf J (Type (u + 1))) :=
        Sheaf.instHasColimitsOfSize
      ∃ (I : Type (u + 1)) (Xi : I → Sheaf J (Type (u + 1)))
        (f : ∀ i, Xi i ⟶ X),
        (∀ i, AlgebraicGeometry.FormalSpace.IsAffineFormalAlgebraicSpace B S hS (Xi i)) ∧
        (∀ i, ∃ (U : Over S), IsAffine U.left ∧
          Nonempty (Xi i ≅
            (presheafToSheaf J (Type (u + 1))).obj
              (Stacks.Groupoids.points (Over.post B.inclusion) U ⋙
                uliftFunctor.{u + 1, u}))) ∧
        (∀ i, ∃ hfi : AlgebraicGeometry.Space.IsRepresentableByAlgebraicSpacesULift.{u + 1}
            B S hS (f i).hom,
          AlgebraicGeometry.Space.HasPropertyULift.{u + 1} B S hS
            (fun _ _ g ↦ AlgebraicGeometry.Space.IsEtaleULift.{u + 1} B S hS g.hom)
            (f i).hom hfi) ∧
        Sheaf.IsLocallySurjective (Sigma.desc f)) :
    AlgebraicGeometry.Space.IsAlgebraicSpaceULift.{u + 1} B S hS X.obj

AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_of_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SetTheoreticColimit.lean, line 213. The attribute's comment: “colimit_condition”.

A directed colimit of affine fppf sheaves along thickenings satisfies the set-theoretic condition if the coproduct of its stages is representable in the big site.

public theorem satisfiesSetTheoreticCondition_of_colimit
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type (u + 1)} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (D : I ⥤ BigAffineFppf B S hS)
    (hD : ∀ ⦃i j : I⦄ (f : i ⟶ j),
      Stacks.Thickenings.IsThickening
        ((BigAffineFppf.toScheme B S hS).map (D.map f)))
    (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1)))
    (hX : Nonempty (X ≅ colimit
      (D ⋙ BigAffineFppf.inclusion B S hS ⋙
        Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))))
    (hU : ∃ (U : BigFppfOver B S hS)
      (F : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))),
      Nonempty (F.obj ≅ (uliftYoneda.{u + 1}).obj U) ∧
        Nonempty (F ≅ ∐ fun i : I ↦
          (Sheaf.sheafifiedYoneda
            (BigFppfOver.topology B S hS)).obj
              ((BigAffineFppf.inclusion B S hS).obj (D.obj i)))) :
    SatisfiesSetTheoreticCondition B S hS X
Sources
LeanAlgebraicGeometry.FormalSpace.formalAlgebraicSpaces_discussion · AlgebraicGeometry.FormalSpace.IsFormalAlgebraicSpace · AlgebraicGeometry.FormalSpace.relativelyRepresentable_diag_of_isFormalAlgebraicSpace · AlgebraicGeometry.FormalSpace.relative_locallyOfFiniteType_diag_of_isFormalAlgebraicSpace · AlgebraicGeometry.FormalSpace.relative_locallyQuasiFinite_diag_of_isFormalAlgebraicSpace · AlgebraicGeometry.FormalSpace.relative_isSeparated_diag_of_isFormalAlgebraicSpace · AlgebraicGeometry.FormalSpace.relativelyRepresentable_diag_of_isAffineFormal · AlgebraicGeometry.FormalSpace.relative_locallyQuasiFinite_diag_of_isAffineFormal

Section87.12 The reduction#

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

Tag 0AIN, a lemma

Tag 0AIN in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_isReduction_of_isAffineFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineReduction.lean, line 317. The attribute's comment: “affine formal algebraic spaces”.

Stacks 0AIN for an affine formal algebraic space. Let X be an affine formal algebraic space over S. There is a reduced algebraic space Xred and a representable morphism Xred ⟶ X which is a thickening and through which every morphism to X from a reduced algebraic space factors uniquely.

theorem exists_isReduction_of_isAffineFormalAlgebraicSpace
    (X : FppfSheaf B S hS) (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    ∃ (Xred : FppfSheaf B S hS) (i : Xred ⟶ X), IsReduction B S hS X Xred i

AlgebraicGeometry.FormalSpace.reduction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/GeneralReduction.lean, line 275. The attribute's comment: “general formal algebraic spaces, as a chosen datum”.

Stacks 0AIN for a general formal algebraic space, as a construction. The chosen reduction of a formal algebraic space over S, in the bundled shape the étale sites of Stacks 0DEA consume.

noncomputable def reduction (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X) :
    Reduction B S hS X

AlgebraicGeometry.FormalSpace.exists_isReduction_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ReductionExistence.lean, line 1299. The attribute's comment: “a general formal algebraic space”.

Let X be a formal algebraic space over S. There exists a reduced algebraic space X_red and a representable morphism X_red ⟶ X which is a thickening, and a morphism U ⟶ X with U a reduced algebraic space factors uniquely through X_red.

theorem exists_isReduction_of_isFormalAlgebraicSpace
    (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X) :
    ∃ (Xred : FppfSheaf B S hS) (i : Xred ⟶ X), IsReduction B S hS X Xred i
Tag 0GB6, an example

Tag 0GB6 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isReduction_formalSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSpectrumReduction.lean, line 458. The attribute's comment: “the reduction”.

Stacks 0GB6. Let A be a weakly admissible topological ring over S and let 𝔞 be its ideal of topologically nilpotent elements, the largest weak ideal of definition of A. The stage of Spf A at 𝔞 is Spec (A ⧸ 𝔞), and its morphism to Spf A exhibits it as the reduction of Spf A.

public theorem isReduction_formalSpectrum
    {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] (hA : TopologicalRing.IsWeaklyAdmissible A)
    {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    (D : QuotientSystem B S hS A) (_hB : D.HasLargeSite) :
    IsReduction B S hS (formalSpectrum D)
      ((formalSpectrumDiagram D).obj (OrderDual.toDual (TopologicalRing.nilIdx hA.1)))
      (formalSpectrumInclusion D (OrderDual.toDual (TopologicalRing.nilIdx hA.1)))

Declarations registered for the tag:

Tag 0GB7, a lemma

Tag 0GB7 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isReduction_pullback_reduction_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ReductionSmoothBaseChange.lean, line 212. The attribute's comment: “the fibre product X ×_Y Y_red is a reduction of X; read against given reductions and a given fibre product rather than chosen ones, exactly as for Stacks 0GB8. Stacks 0AIN supplies the reductions”.

Stacks 0GB7. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S which is representable by algebraic spaces and smooth, let iY : Yred ⟶ Y be a reduction of Y and let P with projections fst : P ⟶ X and snd : P ⟶ Yred be a fibre product X ×_Y Yred. Then P, with the projection fst, is a reduction of X: this is the assertion X_red = X ×_Y Y_red.

P is an algebraic space by Stacks 03XY, reduced by Stacks 0GB3 applied to the base change snd of f, and fst is a representable thickening because iY is; a morphism to X from a reduced algebraic space factors uniquely through P because its composite with f factors uniquely through Yred.

theorem isReduction_pullback_reduction_of_smooth {X Y Yred P : FppfSheaf B S hS}
    (_hX : IsFormalAlgebraicSpace B S hS X) (_hY : IsFormalAlgebraicSpace B S hS Y)
    {f : X ⟶ Y} (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (hsmooth : Space.HasPropertyULift.{u + 1} B S hS
      (Space.smoothPropertyULift.{u + 1} B S hS) f.hom hf)
    {iY : Yred ⟶ Y} (hiY : IsReduction B S hS Y Yred iY)
    {fst : P ⟶ X} {snd : P ⟶ Yred} (sq : IsPullback fst snd f iY) :
    IsReduction B S hS X P fst

AlgebraicGeometry.FormalSpace.isIso_of_isReduction_of_isPullback_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ReductionSmoothBaseChange.lean, line 258. The attribute's comment: “the comparison morphism X_red ⟶ X ×_Y Y_red over X is an isomorphism; read against given reductions and a given fibre product rather than chosen ones, exactly as for Stacks 0GB8. Stacks 0AIN supplies the reductions”.

Stacks 0GB7. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S which is representable by algebraic spaces and smooth, let iX : Xred ⟶ X and iY : Yred ⟶ Y be reductions and let P with projections fst and snd be a fibre product X ×_Y Yred. Then every morphism Xred ⟶ P over X is an isomorphism: the canonical comparison morphism X_red ⟶ X ×_Y Y_red identifies the two.

P is a reduction of X by AlgebraicGeometry.FormalSpace.isReduction_pullback_reduction_of_smooth, and two reductions of X are isomorphic over X.

theorem isIso_of_isReduction_of_isPullback_of_smooth {X Y Xred Yred P : FppfSheaf B S hS}
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    {f : X ⟶ Y} (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (hsmooth : Space.HasPropertyULift.{u + 1} B S hS
      (Space.smoothPropertyULift.{u + 1} B S hS) f.hom hf)
    {iX : Xred ⟶ X} (hiX : IsReduction B S hS X Xred iX)
    {iY : Yred ⟶ Y} (hiY : IsReduction B S hS Y Yred iY)
    {fst : P ⟶ X} {snd : P ⟶ Yred} (sq : IsPullback fst snd f iY)
    {g : Xred ⟶ P} (hg : g ≫ fst = iX) : IsIso g
Tag 0GB8, a lemma

Tag 0GB8 in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasPropertyULift_isSurjectiveULift_iff_isSurjectiveULift_red, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Reduction.lean, line 260.

Stacks 0GB8. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S which is representable by algebraic spaces, let iX : Xred ⟶ X and iY : Yred ⟶ Y be reductions and let fred : Xred ⟶ Yred be compatible with f. Then f is surjective in the sense of Stacks 03XZ if and only if fred is a surjective morphism of algebraic spaces.

theorem hasPropertyULift_isSurjectiveULift_iff_isSurjectiveULift_red
    {X Y : FppfSheaf B S hS}
    (_hX : IsFormalAlgebraicSpace B S hS X) (_hY : IsFormalAlgebraicSpace B S hS Y)
    {Xred Yred : FppfSheaf B S hS} {iX : Xred ⟶ X} {iY : Yred ⟶ Y}
    (hiX : IsReduction B S hS X Xred iX) (hiY : IsReduction B S hS Y Yred iY)
    {f : X ⟶ Y} (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    {fred : Xred ⟶ Yred} (hfred : fred ≫ iY = iX ≫ f) :
    Space.HasPropertyULift.{u + 1} B S hS
        (fun _ _ g ↦ Space.IsSurjectiveULift.{u + 1} B S hS g.hom) f.hom hf ↔
      Space.IsSurjectiveULift.{u + 1} B S hS fred.hom
Sources
LeanAlgebraicGeometry.FormalSpace.exists_isReduction_of_isAffineFormalAlgebraicSpace · AlgebraicGeometry.FormalSpace.reduction · AlgebraicGeometry.FormalSpace.exists_isReduction_of_isFormalAlgebraicSpace · AlgebraicGeometry.FormalSpace.isReduction_formalSpectrum · TopologicalRing.isWeakIdealOfDefinition_topologicalNilradical · TopologicalRing.topologicalNilradical_isRadical · AlgebraicGeometry.FormalSpace.isReduction_pullback_reduction_of_smooth · AlgebraicGeometry.FormalSpace.isIso_of_isReduction_of_isPullback_of_smooth

Section87.13 Colimits of algebraic spaces along thickenings#

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

Tag 0AIU, a lemma

Tag 0AIU in the Stacks Project.

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_colimit_thickenings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ColimitOfAlgebraicSpaces.lean, line 171. The attribute's comment: “granting the chart system that the topological invariance of the étale site (Stacks 05ZH) and the affineness of a thickening of an affine scheme (Stacks 07VT) produce from an affine étale chart of one stage, neither of which this library carries: the chart diagrams, their colimits being affine formal algebraic spaces, their being representable étale over and covering each stage, and the factorization of a scheme-valued point of the colimit through a stage — the step the source omits — are the hypotheses G, α, haff, hαet, hsq, hcov and hfac. What is proved is the passage from the stages to the colimit: that those colimits are an atlas of the colimit sheaf in the sense of Definition 0AIM. The set-theoretic condition of Stacks 0AIS on the colimit is the hypothesis hZset, as it is for Stacks 0AJ1”.

Stacks 0AIU, granting the étale charts of the system. Let E be a directed system of fppf sheaves over S whose stages are algebraic spaces and whose transition morphisms are representable thickenings. A sheaf Z isomorphic to its colimit, satisfying the set-theoretic condition of Stacks 0AIS and admitting a system of affine étale charts as in the Stacks proof, is a formal algebraic space over S.

The charts are the hypotheses G, α, haff, hαet, hsq and hcov, and hfac says that a scheme-valued point of the colimit factors through a stage. What is proved is that the colimit of each chart diagram is representable étale over Z and that these colimits cover Z, so that they form an atlas as in Definition 0AIM.

theorem isFormalAlgebraicSpace_of_colimit_thickenings
    (Λ : Type (u + 1)) [Preorder Λ] [Nonempty Λ] [IsDirected Λ (· ≤ ·)]
    (E : Λ ⥤ FppfSheaf B S hS)
    (_halg : ∀ i : Λ, Space.IsAlgebraicSpaceULift.{u + 1} B S hS (E.obj i).obj)
    (_hthick : ∀ ⦃i j : Λ⦄ (g : i ⟶ j),
      Space.IsRepresentableThickeningULift.{u + 1} B S hS (E.map g).hom)
    (I : Type (u + 1)) (G : I → (Λ ⥤ FppfSheaf B S hS)) (α : ∀ k, G k ⟶ E)
    (haff : ∀ k, IsAffineFormalAlgebraicSpace B S hS (colimit (G k)))
    (hαet : ∀ (k : I) (i : Λ), IsRepresentableEtale B S hS ((α k).app i))
    (hsq : ∀ (k : I) (i : Λ),
      IsPullback (colimit.ι (G k) i) ((α k).app i) (colimMap (α k)) (colimit.ι E i))
    (hcov : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
        Sheaf.instHasColimitsOfSize
      ∀ i : Λ, Sheaf.IsLocallySurjective (Sigma.desc (fun k ↦ (α k).app i)))
    (hfac : ∀ (U : BigFppfOver B S hS)
      (ξ : (uliftYoneda.{u + 1}).obj U ⟶ (colimit E).obj),
      ∃ (i : Λ) (ξ' : (uliftYoneda.{u + 1}).obj U ⟶ (E.obj i).obj),
        ξ = ξ' ≫ (colimit.ι E i).hom)
    (Z : FppfSheaf B S hS) (hZset : SatisfiesSetTheoreticCondition B S hS Z)
    (hZ : Nonempty (Z ≅ colimit E)) :
    IsFormalAlgebraicSpace B S hS Z

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_colimit_isRepresentableThickeningULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ColimitOfAlgebraicSpaceThickenings.lean, line 75. The attribute's comment: “corrected form: the printed statement is false, the colimit need not satisfy the set-theoretic condition of Stacks 0AIS that Definition 0AIM asks of a formal algebraic space (AlgebraicGeometry.FormalSpace.not_forall_isFormalAlgebraicSpace_colimit_thickenings); stated for a sheaf isomorphic to the colimit which satisfies that condition, under the source's hypotheses otherwise”.

Stacks 0AIU, corrected. Let E be a directed system of algebraic spaces over S whose transition morphisms are representable thickenings. A sheaf Z isomorphic to colim E which satisfies the set-theoretic condition of Stacks 0AIS is a formal algebraic space over S.

The set-theoretic condition cannot be dropped: without it the statement is false (AlgebraicGeometry.FormalSpace.not_forall_isFormalAlgebraicSpace_colimit_thickenings).

theorem isFormalAlgebraicSpace_of_colimit_isRepresentableThickeningULift
    (Λ : Type (u + 1)) [Preorder Λ] [Nonempty Λ] [IsDirected Λ (· ≤ ·)]
    (E : Λ ⥤ FppfSheaf B S hS)
    (halg : ∀ i : Λ, Space.IsAlgebraicSpaceULift.{u + 1} B S hS (E.obj i).obj)
    (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 : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
        Sheaf.instHasColimitsOfSize
      Nonempty (Z ≅ colimit E)) :
    IsFormalAlgebraicSpace B S hS Z
Tag 0CB8, an example

Tag 0CB8 in the Stacks Project.

PadicComplexInt.isWeakIdealOfDefinition_maximalIdeal_and_not_isIdealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/IdealOfDefinitionNotAllThickenings.lean, line 127. The attribute's comment: “a weak ideal of definition that is not an ideal of definition, on the ring of integers of ℂ_[p]”.

Stacks 0AIW, the negative clause on the example of Stacks 0CB8. The maximal ideal of the ring of integers of the field ℂ_[p] of p-adic complex numbers is a weak ideal of definition of that admissible topological ring, and it is not an ideal of definition. So the two notions differ, and the correspondence of Stacks 0AIV between weak ideals of definition and thickenings cannot restrict to one between ideals of definition and thickenings.

theorem isWeakIdealOfDefinition_maximalIdeal_and_not_isIdealOfDefinition :
    TopologicalRing.IsWeakIdealOfDefinition (maximalIdeal (PadicComplexInt p)) ∧
      ¬ TopologicalRing.IsIdealOfDefinition (maximalIdeal (PadicComplexInt p))

PadicComplexInt.isIdealOfDefinition_span_p, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/IdealOfDefinitionNotAllThickenings.lean, line 162. The attribute's comment: “the p-adic complex integers”.

Stacks 0CB8. The ideal (p) is an ideal of definition of the ring of integers of ℂ_[p]: its topology is the (p)-adic one.

theorem isIdealOfDefinition_span_p :
    TopologicalRing.IsIdealOfDefinition
      (Ideal.span ({(p : PadicComplexInt p)} : Set (PadicComplexInt p)))

AlgebraicGeometry.FormalSpace.WeakIdealOfDefinitionExample.isWeakIdealOfDefinition_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealOfDefinitionExample.lean, line 232. The attribute's comment: “a weak ideal of definition that is not an ideal of definition”.

Stacks 0CB8. In a local ring whose topology is (π)-adic, with the radical of (π) the maximal ideal, the maximal ideal is a weak ideal of definition: it is open, and each of its elements lies in the radical of (π), hence is topologically nilpotent.

theorem isWeakIdealOfDefinition_maximalIdeal
    (hadic : IsAdic (Ideal.span ({π} : Set A)))
    (hrad : (Ideal.span ({π} : Set A)).radical = maximalIdeal A) :
    TopologicalRing.IsWeakIdealOfDefinition (maximalIdeal A)

AlgebraicGeometry.FormalSpace.WeakIdealOfDefinitionExample.isWeaklyAdmissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealOfDefinitionExample.lean, line 244. The attribute's comment: “a weak ideal of definition that is not an ideal of definition”.

Stacks 0CB8. A complete local ring whose topology is (π)-adic, with the radical of (π) the maximal ideal, is weakly admissible: the maximal ideal is a weak ideal of definition.

theorem isWeaklyAdmissible
    (hadic : IsAdic (Ideal.span ({π} : Set A)))
    (hcomplete : TopologicalRing.IsComplete A)
    (hrad : (Ideal.span ({π} : Set A)).radical = maximalIdeal A) :
    TopologicalRing.IsWeaklyAdmissible A

AlgebraicGeometry.FormalSpace.WeakIdealOfDefinitionExample.isAffineFormalAlgebraicSpace_formalSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealOfDefinitionExample.lean, line 306. The attribute's comment: “a weak ideal of definition that is not an ideal of definition”.

Stacks 0CB8. A complete local ring whose topology is (π)-adic, with the radical of (π) the maximal ideal, has an affine formal algebraic space as formal spectrum, with no hypothesis on the chosen big fppf site beyond its containing the quotient spectra.

Completeness and the radical identity are part of the situation of the example but are not needed for this particular conclusion, which holds for any adic topology; their names are therefore prefixed by an underscore.

theorem isAffineFormalAlgebraicSpace_formalSpectrum
    (hadic : IsAdic (Ideal.span ({π} : Set A)))
    (_hcomplete : TopologicalRing.IsComplete A)
    (_hrad : (Ideal.span ({π} : Set A)).radical = maximalIdeal A)
    {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    (D : QuotientSystem B S hS A) :
    IsAffineFormalAlgebraicSpace B S hS (formalSpectrum D)

AlgebraicGeometry.FormalSpace.WeakIdealOfDefinitionExample.isRelativelyRepresentable_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealOfDefinitionExample.lean, line 377. The attribute's comment: “a weak ideal of definition that is not an ideal of definition”.

Stacks 0CB8. The residue-field stage Spec κ ⟶ Spf A of the formal spectrum, that is the colimit cocone map at the weak ideal of definition 𝔪, is representable by objects of the big fppf site.

theorem isRelativelyRepresentable_residueField
    (hadic : IsAdic (Ideal.span ({π} : Set A)))
    (hrad : (Ideal.span ({π} : Set A)).radical = maximalIdeal A)
    {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    (D : QuotientSystem B S hS A) :
    let J : { I : Ideal A // TopologicalRing.IsWeakIdealOfDefinition I } :=
      ⟨maximalIdeal A, isWeakIdealOfDefinition_maximalIdeal π hadic hrad⟩
    (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (formalSpectrumInclusion D (OrderDual.toDual J))

AlgebraicGeometry.FormalSpace.WeakIdealOfDefinitionExample.isThickening_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealOfDefinitionExample.lean, line 393. The attribute's comment: “a weak ideal of definition that is not an ideal of definition”.

Stacks 0CB8. The residue-field stage Spec κ ⟶ Spf A of the formal spectrum is a thickening: each of its base changes along a morphism from a represented sheaf is a thickening of schemes.

theorem isThickening_residueField
    (hadic : IsAdic (Ideal.span ({π} : Set A)))
    (hrad : (Ideal.span ({π} : Set A)).radical = maximalIdeal A)
    {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    (D : QuotientSystem B S hS A) :
    let J : { I : Ideal A // TopologicalRing.IsWeakIdealOfDefinition I } :=
      ⟨maximalIdeal A, isWeakIdealOfDefinition_maximalIdeal π hadic hrad⟩
    (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)))
      (formalSpectrumInclusion D (OrderDual.toDual J))

AlgebraicGeometry.FormalSpace.WeakIdealOfDefinitionExample.not_isIdealOfDefinition_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealOfDefinitionExample.lean, line 415. The attribute's comment: “a weak ideal of definition that is not an ideal of definition”.

Stacks 0CB8. In a valuation ring whose topology is (π)-adic for some π in the maximal ideal, the maximal ideal is not an ideal of definition if it is not finitely generated: it is then idempotent, so all its powers coincide and cofinality of those powers would force 𝔪 = (π) to be principal.

theorem not_isIdealOfDefinition_maximalIdeal
    [IsDomain A] (hval : IsValuationRing A) (hπm : π ∈ maximalIdeal A)
    (hadic : IsAdic (Ideal.span ({π} : Set A)))
    (hnotfg : ¬ (maximalIdeal A).FG) :
    ¬ TopologicalRing.IsIdealOfDefinition (maximalIdeal A)

rationalPolynomial, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/CoefficientRing.lean, line 62. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. Finite sums ∑ a_α t^α with α ranging over nonnegative rationals, realised as the monoid algebra of ℚ≥0 over k.

abbrev rationalPolynomial (k : Type*) [CommRing k]

polynomialT, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/CoefficientRing.lean, line 66. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The monomial t = t^1 in rationalPolynomial k.

def polynomialT (k : Type*) [CommRing k] : rationalPolynomial k

polynomialTIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/CoefficientRing.lean, line 71. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The principal ideal (t) of rationalPolynomial k.

def polynomialTIdeal (k : Type*) [CommRing k] : Ideal (rationalPolynomial k)

rationalPowerSeries, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/CoefficientRing.lean, line 77. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The ring of power series with nonnegative rational exponents over k, constructed as the (t)-adic completion of rationalPolynomial k.

abbrev rationalPowerSeries (k : Type*) [CommRing k]

CoefficientFamily, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/CoefficientRing.lean, line 83. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. Coefficient families (a_α)_{α ∈ ℚ≥0} in k having, for every natural number n, only finitely many nonzero entries with α ≤ n.

def CoefficientFamily (k : Type*) [Zero k]

coefficientRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/CoefficientRing.lean, line 90. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The subring of HahnSeries ℚ≥0 k generated by the series whose support is finite below every integer bound. RationalPowerSeries.mem_coefficientRing_iff shows that the generating set is already a subring, so this is exactly the displayed ring of series.

def coefficientRing (k : Type*) [CommRing k] : Subring (HahnSeries ℚ≥0 k)

RationalPowerSeries.t, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/CoefficientRing.lean, line 98. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The element π = t of rationalPowerSeries k, the image of the exponent-one monomial under the completion map.

def t (k : Type*) [CommRing k] : rationalPowerSeries k

RationalPowerSeries.tIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/CoefficientRing.lean, line 104. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The principal ideal (t) of rationalPowerSeries k, whose powers define the topology.

def tIdeal (k : Type*) [CommRing k] : Ideal (rationalPowerSeries k)

RationalPowerSeries.mem_coefficientRing_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/CoefficientRing.lean, line 248. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. Membership in coefficientRing k is precisely local finiteness of the support below every integer bound; in particular the generating set of coefficientRing k is already a subring.

theorem mem_coefficientRing_iff (k : Type*) [Field k] (f : HahnSeries ℚ≥0 k) :
    f ∈ coefficientRing k ↔
      ∀ n : ℕ, {q : ℚ≥0 | q ≤ n ∧ f.coeff q ≠ 0}.Finite

RationalPowerSeries.exists_equiv_coefficientFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/CompletionEquiv.lean, line 552. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. Every coefficient family (a_α) is represented by a unique element of the coefficient ring, with unchanged coefficients.

theorem exists_equiv_coefficientFamily (k : Type*) [Field k] :
    ∃ e : CoefficientFamily k ≃ coefficientRing k,
      ∀ f : CoefficientFamily k, ∀ q : ℚ≥0, ((e f).1).coeff q = f.1 q

RationalPowerSeries.exists_ringEquiv_coefficientRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/CompletionEquiv.lean, line 607. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The completed monoid algebra is the ring of locally finite coefficient series, with the usual addition and convolution multiplication; the isomorphism preserves the coefficients of polynomials.

theorem exists_ringEquiv_coefficientRing (k : Type*) [Field k] :
    ∃ e : rationalPowerSeries k ≃+* coefficientRing k,
      ∀ (p : rationalPolynomial k) (q : ℚ≥0),
        ((e (AdicCompletion.of (polynomialTIdeal k) (rationalPolynomial k) p)).1).coeff q =
          p.coeff q

RationalPowerSeries.isDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/ValuationRing.lean, line 39. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The ring of power series with nonnegative rational exponents is a domain.

theorem isDomain (k : Type*) [Field k] : IsDomain (rationalPowerSeries k)

RationalPowerSeries.instIsDomain, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/ValuationRing.lean, line 52. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The ring of power series with nonnegative rational exponents is a domain.

instance instIsDomain (k : Type*) [Field k] : IsDomain (rationalPowerSeries k)

RationalPowerSeries.isLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/ValuationRing.lean, line 58. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The ring of power series with nonnegative rational exponents is local.

theorem isLocalRing (k : Type*) [Field k] : IsLocalRing (rationalPowerSeries k)

RationalPowerSeries.instIsLocalRing, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/ValuationRing.lean, line 66. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The ring of power series with nonnegative rational exponents is local.

instance instIsLocalRing (k : Type*) [Field k] : IsLocalRing (rationalPowerSeries k)

RationalPowerSeries.isValuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/ValuationRing.lean, line 72. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. This local domain is a valuation ring: inside its fraction field it is maximal for the domination order among local subrings.

theorem isValuationRing (k : Type*) [Field k] :
    IsValuationRing (rationalPowerSeries k)

RationalPowerSeries.t_mem_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/ValuationRing.lean, line 83. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The monomial t lies in the maximal ideal; in particular it is not a unit.

theorem t_mem_maximalIdeal (k : Type*) [Field k] :
    t k ∈ IsLocalRing.maximalIdeal (rationalPowerSeries k)

RationalPowerSeries.isAdic_span_t, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/ValuationRing.lean, line 94. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The topology of rationalPowerSeries k is the (t)-adic topology.

theorem isAdic_span_t (k : Type*) [Field k] :
    IsAdic (Ideal.span ({t k} : Set (rationalPowerSeries k)))

RationalPowerSeries.isComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/ValuationRing.lean, line 100. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The ring of power series with nonnegative rational exponents is separated and complete for its (t)-adic topology.

theorem isComplete (k : Type*) [Field k] :
    TopologicalRing.IsComplete (rationalPowerSeries k)

RationalPowerSeries.radical_span_t, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/ValuationRing.lean, line 133. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The radical of (t) is the maximal ideal: every non-unit has positive order, so some power of it is divisible by t.

theorem radical_span_t (k : Type*) [Field k] :
    (Ideal.span ({t k} : Set (rationalPowerSeries k))).radical =
      IsLocalRing.maximalIdeal (rationalPowerSeries k)

RationalPowerSeries.not_fg_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/ValuationRing.lean, line 205. The attribute's comment: “the rational power series valuation ring”.

Stacks 0CB8. The maximal ideal is not finitely generated: finitely many elements of the maximal ideal have a least positive order a, and the monomial of exponent a / 2 is in the maximal ideal but not in the ideal they generate.

theorem not_fg_maximalIdeal (k : Type*) [Field k] :
    ¬ (IsLocalRing.maximalIdeal (rationalPowerSeries k)).FG

PadicComplexInt.isAdic_span_p, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/PadicComplexInt.lean, line 93. The attribute's comment: “the p-adic complex integers”.

Stacks 0CB8. The topology of the ring of integers of ℂ_[p], inherited from ℂ_[p], is the (p)-adic topology.

theorem isAdic_span_p :
    IsAdic (Ideal.span ({(p : PadicComplexInt p)} : Set (PadicComplexInt p)))

PadicComplexInt.instIsLinearTopology, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/PadicComplexInt.lean, line 131. The attribute's comment: “the p-adic complex integers”.

Stacks 0CB8. The topology of the ring of integers of ℂ_[p] is linear: the open ideals form a basis of neighbourhoods of zero.

instance instIsLinearTopology : IsLinearTopology (PadicComplexInt p) (PadicComplexInt p)

PadicComplexInt.isComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/PadicComplexInt.lean, line 138. The attribute's comment: “the p-adic complex integers”.

Stacks 0CB8. The ring of integers of ℂ_[p] is separated and complete for its topology.

theorem isComplete : TopologicalRing.IsComplete (PadicComplexInt p)

PadicComplexInt.natCast_mem_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/PadicComplexInt.lean, line 150. The attribute's comment: “the p-adic complex integers”.

Stacks 0CB8. The element p of the ring of integers of ℂ_[p] lies in its maximal ideal; in particular it is nonzero and not a unit.

theorem natCast_mem_maximalIdeal :
    (p : PadicComplexInt p) ∈ maximalIdeal (PadicComplexInt p)

PadicComplexInt.radical_span_p, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/PadicComplexInt.lean, line 162. The attribute's comment: “the p-adic complex integers”.

Stacks 0CB8. The radical of the ideal (p) of the ring of integers of ℂ_[p] is its maximal ideal.

theorem radical_span_p :
    (Ideal.span ({(p : PadicComplexInt p)} : Set (PadicComplexInt p))).radical =
      maximalIdeal (PadicComplexInt p)

PadicComplexInt.isValuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/PadicComplexInt.lean, line 193. The attribute's comment: “the p-adic complex integers”.

Stacks 0CB8. The ring of integers of ℂ_[p] is a valuation ring: inside its fraction field it is maximal for the domination order among local subrings.

theorem isValuationRing : IsValuationRing (PadicComplexInt p)

PadicComplexInt.not_fg_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/PadicComplexInt.lean, line 200. The attribute's comment: “the p-adic complex integers”.

Stacks 0CB8. The maximal ideal of the ring of integers of ℂ_[p] is not finitely generated: the valuation of ℂ_[p] takes arbitrarily small positive values, since ℂ_[p] is algebraically closed, so no element of the maximal ideal generates it.

theorem not_fg_maximalIdeal : ¬ (maximalIdeal (PadicComplexInt p)).FG
Tag 0AIV, a remark

Tag 0AIV in the Stacks Project.

AlgebraicGeometry.McQuillanFormalScheme.not_forall_isFppfColimitOfThickenings_of_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/TwistedDoubleColimit.lean, line 90. The attribute's comment: “the statement as printed is false: the if direction, for sectionwise weak ideals of definition, fails for the twisted double, a formal scheme with a fundamental system of (weak) ideals of definition whose functor of points h_𝔛 is not a colimit of schemes as in Lemma 0AIU (colimit in fppf sheaves); the corrected form is McQuillanFormalScheme.isFppfColimitOfThickenings_iff_exists_isFundamentalSystem”.

Stacks 0AIV, the "if" direction as printed, is false. There is a formal scheme 𝔛 in the sense of McQuillan (the twisted double AlgebraicGeometry.TwistedDouble.𝔛, a formal scheme à la EGA) which has a fundamental system of weak ideals of definition, in the source's sectionwise sense, but whose functor of points h_𝔛 is not a colimit of schemes along thickenings in fppf sheaves, as in Stacks 0AIU. On a formal scheme à la EGA the weak affine formal opens are the affine formal opens, and a fundamental system of ideals of definition is one of weak ideals of definition, so the fundamental system of AlgebraicGeometry.TwistedDouble.exists_isFundamentalSystemOfIdealsOfDefinitionOn serves.

The corrected form is McQuillanFormalScheme.isFppfColimitOfThickenings_iff_exists_isFundamentalSystem, where the weak ideals of definition are cut out by their sections over the affine formal opens.

theorem McQuillanFormalScheme.not_forall_isFppfColimitOfThickenings_of_exists :
    ¬ ∀ 𝔛 : McQuillanFormalScheme.{0},
      (∃ 𝒮 : Set (IdealSheaf 𝔛.obj),
        IsFundamentalSystemOfWeakIdealsOfDefinitionOn 𝒮 (IsWeakAffineFormalOpen 𝔛.obj)) →
        𝔛.IsFppfColimitOfThickenings

AlgebraicGeometry.LocallyTopologicallyRingedSpace.IdealSheaf.IsWeakIdealOfDefinitionOn, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinition.lean, line 107. The attribute's comment: “the definition, over a class 𝒜 of affine formal opens”.

An ideal sheaf on X is a weak ideal of definition over a class 𝒜 of opens — the affine formal open subschemes — when its ideal of sections over every open of 𝒜 is a weak ideal of definition of the topological ring of sections there.

def IsWeakIdealOfDefinitionOn (I : IdealSheaf X) (𝒜 : Opens X → Prop) : Prop

AlgebraicGeometry.LocallyTopologicallyRingedSpace.IsFundamentalSystemOfWeakIdealsOfDefinitionOn, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinition.lean, line 117. The attribute's comment: “the definition, over a class 𝒜 of affine formal opens”.

A family of ideal sheaves on X is a fundamental system of weak ideals of definition over a class 𝒜 of opens — the affine formal open subschemes — when each member is a weak ideal of definition and, over every open of 𝒜, their ideals of sections form a neighbourhood basis of zero in the topological ring of sections.

def IsFundamentalSystemOfWeakIdealsOfDefinitionOn {X : LTRS.{u}} (𝒮 : Set (IdealSheaf X))
    (𝒜 : Opens X → Prop) : Prop

AlgebraicGeometry.LocallyTopologicallyRingedSpace.IdealSheaf.isWeakIdealOfDefinitionOn_of_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinition.lean, line 223. The attribute's comment: “it suffices to check on an affine open covering, CORRECTED: the condition is checked on the members of the class contained in a covering member, not on the covering members themselves, which is false as the source states it; granted the quasi-compactness hcompact and the refinement hrefine of the class of affine formal opens”.

Stacks 0AIV, the locality of the weak ideal-of-definition condition. Let 𝒰 be a covering of X and let 𝒜 be a class of quasi-compact opens — the affine formal open subschemes — whose members contained in an open cover that open. Then an ideal sheaf is a weak ideal of definition over 𝒜 as soon as its ideals of sections over the members of 𝒜 contained in a member of 𝒰 are weak ideals of definition.

Checking the members of 𝒰 alone would not do: an ideal sheaf can have the zero ideal of global sections and the unit ideal on an open avoiding one point.

theorem isWeakIdealOfDefinitionOn_of_cover (I : IdealSheaf X) (𝒜 : Opens X → Prop)
    (𝒰 : Set (Opens X)) (hcover : sSup 𝒰 = ⊤)
    (hcompact : ∀ U : Opens X, 𝒜 U → IsCompact (U : Set X))
    (hrefine : ∀ V ∈ 𝒰, ∀ W : Opens X, W ≤ V → ∀ x ∈ W,
      ∃ U : Opens X, U ≤ W ∧ x ∈ U ∧ 𝒜 U)
    (hI : ∀ V ∈ 𝒰, ∀ U : Opens X, U ≤ V → 𝒜 U →
      TopologicalRing.IsWeakIdealOfDefinition (I.ideal U)) :
    I.IsWeakIdealOfDefinitionOn 𝒜

AlgebraicGeometry.LocallyTopologicallyRingedSpace.isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinition.lean, line 263. The attribute's comment: “it suffices to check the fundamental-system condition on an affine open covering, CORRECTED in the same way as the weak ideal-of-definition condition — the condition is checked on the members of the class contained in a covering member, not on the covering members themselves — and granting hbasis: the neighbourhood-basis half is a condition on each individual affine formal open and there is nothing about it to transport along a covering”.

Stacks 0AIV, the locality of the fundamental-system condition: the neighbourhood-basis half is a condition on the individual opens of 𝒜, so only the weak ideal-of-definition half has to be transported along the covering, by IdealSheaf.isWeakIdealOfDefinitionOn_of_cover.

theorem isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover {X : LTRS.{u}}
    (𝒮 : Set (IdealSheaf X)) (𝒜 : Opens X → Prop)
    (𝒰 : Set (Opens X)) (hcover : sSup 𝒰 = ⊤)
    (hcompact : ∀ U : Opens X, 𝒜 U → IsCompact (U : Set X))
    (hrefine : ∀ V ∈ 𝒰, ∀ W : Opens X, W ≤ V → ∀ x ∈ W,
      ∃ U : Opens X, U ≤ W ∧ x ∈ U ∧ 𝒜 U)
    (h𝒮 : ∀ I ∈ 𝒮, ∀ V ∈ 𝒰, ∀ U : Opens X, U ≤ V → 𝒜 U →
      TopologicalRing.IsWeakIdealOfDefinition (I.ideal U))
    (hbasis : ∀ U : Opens X, 𝒜 U →
      (nhds (0 : (X.presheaf.obj (op U)).α)).HasBasis (· ∈ 𝒮)
        fun I : IdealSheaf X => (I.ideal U : Set (X.presheaf.obj (op U)).α)) :
    IsFundamentalSystemOfWeakIdealsOfDefinitionOn 𝒮 𝒜

AlgebraicGeometry.McQuillanFormalScheme.isFppfColimitOfThickenings_iff_exists_isFundamentalSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinitionColimitIff.lean, line 130. The attribute's comment: “h_𝔛 is a colimit of schemes along thickenings as in Lemma 0AIU (colimit in fppf sheaves) if and only if there exists a fundamental system of weak ideals of definition, CORRECTED: the weak ideals of definition are those cut out by their sections over the affine formal opens, the ones to which the correspondence ℐ ↦ (𝔛, 𝒪_𝔛/ℐ) applies (it fails for an arbitrary ideal sheaf)”.

The functor of points h_𝔛 of a McQuillan formal scheme is a colimit of schemes along thickenings, as in Stacks 0AIU, in fppf sheaves if and only if 𝔛 has a fundamental system of weak ideals of definition cut out by their sections over the weakly affine formal opens.

theorem isFppfColimitOfThickenings_iff_exists_isFundamentalSystem (𝔛 : McQuillanFormalScheme.{u}) :
    𝔛.IsFppfColimitOfThickenings ↔ ∃ 𝒮 : Set (IdealSheaf 𝔛.obj),
      (∀ I ∈ 𝒮, I.IsCutOutOn (IsWeakAffineFormalOpen 𝔛.obj)) ∧
        IsFundamentalSystemOfWeakIdealsOfDefinitionOn 𝒮 (IsWeakAffineFormalOpen 𝔛.obj)

AlgebraicGeometry.McQuillanFormalScheme.exists_isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_isFppfColimitOfThickenings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinitionColimitOnlyIf.lean, line 60. The attribute's comment: “the only if direction of the last sentence, as printed and unconditional: if h_𝔛 is a colimit of schemes along thickenings as in Lemma 0AIU (colimit in fppf sheaves), then there exists a fundamental system of weak ideals of definition for 𝔛, in the sectionwise sense the source defines, with no condition on its members. The converse fails as printed (not_forall_isFppfColimitOfThickenings_of_exists) and needs the members to be cut out by their sections (isFppfColimitOfThickenings_iff_exists_isFundamentalSystem)”.

If the functor of points h_𝔛 of a formal scheme 𝔛 in the sense of McQuillan is a colimit of schemes along thickenings, then there exists a fundamental system of weak ideals of definition for 𝔛: a family of ideal sheaves each of which is a weak ideal of definition over every affine formal open, whose ideals of sections form a neighbourhood basis of zero over every affine formal open.

theorem exists_isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_isFppfColimitOfThickenings
    (𝔛 : McQuillanFormalScheme.{u}) (h : 𝔛.IsFppfColimitOfThickenings) :
    ∃ 𝒮 : Set (IdealSheaf 𝔛.obj),
      IsFundamentalSystemOfWeakIdealsOfDefinitionOn 𝒮 (IsWeakAffineFormalOpen 𝔛.obj)

AlgebraicGeometry.McQuillanFormalScheme.weakIdealOfDefinitionEquivThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinitionCorrespondence.lean, line 219. The attribute's comment: “the one-to-one correspondence between weak ideals of definition and thickenings Z → h_𝔛, CORRECTED: the weak ideals of definition are those cut out by their sections over the affine formal opens (IdealSheaf.IsCutOutOn, the formal analogue of quasi-coherence), the printed statement for an arbitrary ideal sheaf being false (exists_isWeakIdealOfDefinitionOn_forall_thickening_ideal_ne); a thickening is a scheme Z with a relatively representable morphism h_Z → h_𝔛 whose base changes are thickenings of schemes, the functors of points being presheaves on all schemes, and thickenings are taken up to isomorphism over h_𝔛”.

Stacks 0AIV, the one-to-one correspondence between weak ideals of definition and thickenings Z → h_𝔛. A weak ideal of definition ℐ (cut out by its sections over the weak affine formal opens) goes to the thickening (𝔛, 𝒪_𝔛/ℐ) → h_𝔛, and a thickening goes to its kernel ideal sheaf; the thickenings are taken up to isomorphism over h_𝔛.

noncomputable def weakIdealOfDefinitionEquivThickening :
    𝔛.WeakIdealOfDefinition ≃ Quotient (Thickening.setoid (𝔛 := 𝔛))

AlgebraicGeometry.McQuillanFormalScheme.ker_quotientPoint_and_existsUnique_factor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinitionCorrespondence.lean, line 245. The attribute's comment: “the correspondence associates to ℐ the scheme Z = (𝔛, 𝒪_𝔛/ℐ) with the obvious morphism to 𝔛: its kernel is ℐ and the points of 𝔛 killing ℐ are those factoring through it”.

Stacks 0AIV: the thickening attached to ℐ is (𝔛, 𝒪_𝔛/ℐ) with its obvious morphism to 𝔛. The morphism Z → 𝔛 of locally topologically ringed spaces underlying the thickening has kernel ideal sheaf ℐ, and a point T → 𝔛 of a scheme factors through it, uniquely, exactly when it kills ℐ: Z is the closed subspace of 𝔛 cut out by ℐ.

theorem ker_quotientPoint_and_existsUnique_factor (I : 𝔛.WeakIdealOfDefinition) :
    IdealSheaf.ker I.thickening.point = I.1 ∧
      ∀ {T : Scheme.{u}} (f : schemeToLTRSObj T ⟶ 𝔛.obj),
        I.1.Kills f ↔ ∃! k : T ⟶ I.thickening.scheme, schemeToLTRS.map k ≫ I.thickening.point = f

AlgebraicGeometry.McQuillanFormalScheme.exists_isWeakIdealOfDefinitionOn_forall_thickening_ideal_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinitionCorrespondence.lean, line 259. The attribute's comment: “the printed correspondence, for an arbitrary ideal sheaf, is false: a weak ideal of definition which is the kernel of no thickening”.

Without the cut-out condition the correspondence of Stacks 0AIV fails. There is a McQuillan formal scheme — the pseudo-discretisation of the spectrum of the dual numbers over the 2-adic integers — with a weak ideal of definition which is the kernel ideal sheaf of no thickening Z → h_𝔛: kernels of thickenings are cut out by their sections over the affine formal opens, and this ideal sheaf is not.

theorem exists_isWeakIdealOfDefinitionOn_forall_thickening_ideal_ne :
    ∃ (𝔛 : McQuillanFormalScheme.{0}) (I : IdealSheaf 𝔛.obj),
      I.IsWeakIdealOfDefinitionOn (IsWeakAffineFormalOpen 𝔛.obj) ∧
        ∀ Z : 𝔛.Thickening, Z.ideal ≠ I

AlgebraicGeometry.LocallyTopologicallyRingedSpace.IdealSheaf.exists_not_isWeakIdealOfDefinitionOn_of_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinitionCoverCounterexample.lean, line 200. The attribute's comment: “the statement as printed is false: checking the weak ideal-of-definition condition on the members of an affine open covering does not suffice, already for Spec of the dual numbers over the 2-adic integers covered by itself, with the ideal sheaf of sections vanishing at the closed point; the corrected form is IdealSheaf.isWeakIdealOfDefinitionOn_of_cover_of_isMcQuillanFormalScheme”.

Stacks 0AIV is false as printed: the weak ideal of definition condition cannot be checked on the members of an affine open covering. There is a McQuillan formal scheme X whose whole space is a weak affine formal open, with an ideal sheaf ℐ such that ℐ(X) is a weak ideal of definition, while ℐ is not a weak ideal of definition over every weak affine formal open. The witness is the spectrum of the dual numbers ℤ₂[ε] over the 2-adic integers, pseudo-discretised, with the ideal sheaf of sections vanishing at the closed point; here t = 2 lies in the maximal ideal and 2ⁿ ε ≠ 0 for every n.

theorem exists_not_isWeakIdealOfDefinitionOn_of_cover :
    ∃ (X : LTRS.{0}) (_ : IsMcQuillanFormalScheme X) (I : IdealSheaf X),
      IsWeakAffineFormalOpen X ⊤ ∧ TopologicalRing.IsWeakIdealOfDefinition (I.ideal ⊤) ∧
        ¬ I.IsWeakIdealOfDefinitionOn (IsWeakAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.not_forall_isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinitionCoverCounterexample.lean, line 248. The attribute's comment: “the statement as printed is false: checking the fundamental-system condition on the members of an affine open covering does not suffice, already for a one-member family on Spec of the dual numbers over the 2-adic integers covered by itself, with the ideal sheaf of sections vanishing at the closed point; the corrected form is isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover_of_isMcQuillanFormalScheme”.

Stacks 0AIV, the locality of the fundamental-system condition, is false as printed. It is not true that a family of ideal sheaves on a formal scheme in the sense of McQuillan is a fundamental system of weak ideals of definition as soon as, over the members of an affine open covering, its members are weak ideals of definition whose ideals of sections form a neighbourhood basis of zero, even for a nonempty family directed by inclusion. The witness is the one-member family {ℐ} of IdealSheaf.exists_not_isWeakIdealOfDefinitionOn_of_cover, on the pseudo-discretised spectrum of the dual numbers ℤ₂[ε] covered by itself: ℐ(X) = 0 is a weak ideal of definition and a neighbourhood of zero of the discrete ring 𝒪_X(X), but ℐ is not a weak ideal of definition over the affine open D(2).

The corrected statement checks the condition on the affine formal opens contained in the members of the covering: isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover_of_isMcQuillanFormalScheme.

theorem not_forall_isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover :
    ¬ ∀ (X : LTRS.{0}), IsMcQuillanFormalScheme X → ∀ (𝒮 : Set (IdealSheaf X))
      (𝒰 : Set (Opens X)), 𝒮.Nonempty →
      (∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
        K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W) →
      (∀ V ∈ 𝒰, IsWeakAffineFormalOpen X V) → sSup 𝒰 = ⊤ →
      (∀ I ∈ 𝒮, ∀ V ∈ 𝒰, TopologicalRing.IsWeakIdealOfDefinition (I.ideal V)) →
      (∀ V ∈ 𝒰, (nhds (0 : (X.presheaf.obj (op V)).α)).HasBasis (· ∈ 𝒮)
        fun I : IdealSheaf X => (I.ideal V : Set (X.presheaf.obj (op V)).α)) →
      IsFundamentalSystemOfWeakIdealsOfDefinitionOn 𝒮 (IsWeakAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.not_forall_isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_hasBasis_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinitionCoverCounterexample.lean, line 315. The attribute's comment: “the statement as printed is false, also on the reading where the members are weak ideals of definition everywhere and only the neighbourhood-basis property is checked on the members of an affine open covering: already for one weak ideal of definition on the pseudo-discretised Spec(Z[X_0, X_1, ...]/(X_k^(k+1))) covered by itself; the corrected form is isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover_of_isMcQuillanFormalScheme”.

Stacks 0AIV, the locality of the fundamental-system condition, is false as printed, also when only the neighbourhood-basis half is checked on the covering. It is not true that a family of weak ideals of definition (over every affine formal open) on a formal scheme in the sense of McQuillan is a fundamental system as soon as its ideals of sections form a neighbourhood basis of zero over the members of an affine open covering, even for a nonempty family directed by inclusion. The witness is that of not_forall_isFundamentalSystemOfIdealsOfDefinitionOn_of_hasBasis_cover for Stacks 0AIW: on the pseudo-discretisation of Spec (ℤ[X₀, X₁, …] / (X_k ^ (k + 1))), a McQuillan formal scheme, the sections whose germs are multiples of the germ of X₁, vanishing outside D(n!), form an ideal of definition, hence a weak one, over every quasi-compact open; it is zero over the whole space, which is affine and has discrete sections, but its sections over D(n!), which are discrete, contain X₁ ≠ 0.

The corrected statement checks the condition on the affine formal opens contained in the members of the covering: isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover_of_isMcQuillanFormalScheme.

theorem not_forall_isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_hasBasis_cover :
    ¬ ∀ (X : LTRS.{0}), IsMcQuillanFormalScheme X → ∀ (𝒮 : Set (IdealSheaf X))
      (𝒰 : Set (Opens X)), 𝒮.Nonempty →
      (∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
        K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W) →
      (∀ V ∈ 𝒰, IsWeakAffineFormalOpen X V) → sSup 𝒰 = ⊤ →
      (∀ I ∈ 𝒮, I.IsWeakIdealOfDefinitionOn (IsWeakAffineFormalOpen X)) →
      (∀ V ∈ 𝒰, (nhds (0 : (X.presheaf.obj (op V)).α)).HasBasis (· ∈ 𝒮)
        fun I : IdealSheaf X => (I.ideal V : Set (X.presheaf.obj (op V)).α)) →
      IsFundamentalSystemOfWeakIdealsOfDefinitionOn 𝒮 (IsWeakAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.IdealSheaf.isWeakIdealOfDefinitionOn_of_cover_of_isCutOutOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinitionCutOutLocality.lean, line 250. The attribute's comment: “it suffices to check the weak ideal-of-definition condition on the members of an affine open covering: for ideal sheaves cut out by their sections over the affine formal opens (IdealSheaf.IsCutOutOn), the class of the correspondence with thickenings and of the colimit criterion; for an arbitrary ideal sheaf it is false (IdealSheaf.exists_not_isWeakIdealOfDefinitionOn_of_cover)”.

Stacks 0AIV, the weak ideal-of-definition condition may be checked on the members of an affine open covering, for ideal sheaves cut out by their sections. Let 𝔛 be a formal scheme in the sense of McQuillan and ℐ an ideal sheaf cut out by its sections over the affine formal opens (IdealSheaf.IsCutOutOn). If ℐ(𝔙) is a weak ideal of definition for the members 𝔙 of a covering of 𝔛 by affine formal opens, then ℐ is a weak ideal of definition.

These are the ideal sheaves of the correspondence of Stacks 0AIV with thickenings (McQuillanFormalScheme.weakIdealOfDefinitionEquivThickening) and of its colimit criterion (McQuillanFormalScheme.isFppfColimitOfThickenings_iff_exists_isFundamentalSystem). For an arbitrary ideal sheaf checking the covering members is not enough (IdealSheaf.exists_not_isWeakIdealOfDefinitionOn_of_cover), and the condition must then be checked on the affine formal opens inside the covering members (IdealSheaf.isWeakIdealOfDefinitionOn_of_cover_of_isMcQuillanFormalScheme). Over an affine formal open 𝔚 inside a covering member 𝔙 ≅ Spfw A, the ideal ℐ(𝔚) is the kernel of the quotient point Spec (A/ℐ(𝔙)) → 𝔛 (IdealSheaf.isWeakIdealOfDefinition_of_le_of_isCutOutOn).

theorem IdealSheaf.isWeakIdealOfDefinitionOn_of_cover_of_isCutOutOn
    (hX : IsMcQuillanFormalScheme X) (I : IdealSheaf X)
    (hC : I.IsCutOutOn (IsWeakAffineFormalOpen X)) (𝒰 : Set (Opens X))
    (h𝒰 : ∀ V ∈ 𝒰, IsWeakAffineFormalOpen X V) (hcover : sSup 𝒰 = ⊤)
    (hI : ∀ V ∈ 𝒰, IsWeakIdealOfDefinition (I.ideal V)) :
    I.IsWeakIdealOfDefinitionOn (IsWeakAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover_of_isCutOutOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinitionCutOutLocality.lean, line 280. The attribute's comment: “it suffices to check the fundamental-system condition on the members of an affine open covering: for a family indexed by a directed set, as in the source, of ideal sheaves cut out by their sections over the affine formal opens (IdealSheaf.IsCutOutOn), the class of the colimit criterion; for arbitrary ideal sheaves it is false (not_forall_isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_hasBasis_cover)”.

Stacks 0AIV, the fundamental-system condition may be checked on the members of an affine open covering, for ideal sheaves cut out by their sections. Let 𝔛 be a formal scheme in the sense of McQuillan and {ℐ_λ} a nonempty family of ideal sheaves, directed by inclusion, each cut out by its sections over the affine formal opens. If over the members 𝔙 of a covering of 𝔛 by affine formal opens the ℐ_λ(𝔙) are weak ideals of definition forming a neighbourhood basis of zero, then {ℐ_λ} is a fundamental system of weak ideals of definition.

The family is indexed, as in the source, by a directed set (nonempty, by Stacks' definition of a directed set), with ℐ_μ ⊆ ℐ_λ for μ ≥ λ; this is the directedness asked here. Over an affine formal open inside a single covering member no directedness is used (hasBasis_of_le_of_isCutOutOn); it serves to pass to affine formal opens meeting several members. These are the families of the colimit criterion McQuillanFormalScheme.isFppfColimitOfThickenings_iff_exists_isFundamentalSystem. For arbitrary ideal sheaves checking the covering members is not enough (not_forall_isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover, not_forall_isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_hasBasis_cover).

theorem isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover_of_isCutOutOn
    (hX : IsMcQuillanFormalScheme X) (𝒮 : Set (IdealSheaf X))
    (hC : ∀ I ∈ 𝒮, I.IsCutOutOn (IsWeakAffineFormalOpen X)) (hne : 𝒮.Nonempty)
    (hdir : ∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
      K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W)
    (𝒰 : Set (Opens X)) (h𝒰 : ∀ V ∈ 𝒰, IsWeakAffineFormalOpen X V) (hcover : sSup 𝒰 = ⊤)
    (h𝒮 : ∀ I ∈ 𝒮, ∀ V ∈ 𝒰, IsWeakIdealOfDefinition (I.ideal V))
    (hbasis : ∀ V ∈ 𝒰, (nhds (0 : (X.presheaf.obj (op V)).α)).HasBasis (· ∈ 𝒮)
      fun I : IdealSheaf X => (I.ideal V : Set (X.presheaf.obj (op V)).α)) :
    IsFundamentalSystemOfWeakIdealsOfDefinitionOn 𝒮 (IsWeakAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.IdealSheaf.isWeakIdealOfDefinitionOn_of_cover_of_isMcQuillanFormalScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinitionLocalityMcQuillan.lean, line 65. The attribute's comment: “it suffices to check the weak ideal-of-definition condition on an affine open covering, CORRECTED: on the affine formal opens contained in a covering member, checking the covering members alone being insufficient (exists_not_isWeakIdealOfDefinitionOn_of_cover)”.

An ideal sheaf on a formal scheme 𝔛 in the sense of McQuillan is a weak ideal of definition as soon as its ideals of sections over the affine formal opens contained in the members of an open covering are weak ideals of definition.

theorem IdealSheaf.isWeakIdealOfDefinitionOn_of_cover_of_isMcQuillanFormalScheme
    (hX : IsMcQuillanFormalScheme X) (I : IdealSheaf X) (𝒰 : Set (Opens X)) (hcover : sSup 𝒰 = ⊤)
    (hI : ∀ V ∈ 𝒰, ∀ U : Opens X, U ≤ V → IsWeakAffineFormalOpen X U →
      TopologicalRing.IsWeakIdealOfDefinition (I.ideal U)) :
    I.IsWeakIdealOfDefinitionOn (IsWeakAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover_of_isMcQuillanFormalScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakIdealOfDefinitionLocalityMcQuillan.lean, line 81. The attribute's comment: “it suffices to check the fundamental-system condition on an affine open covering, CORRECTED: on the affine formal opens contained in a covering member, checking the covering members alone being insufficient (exists_not_isWeakIdealOfDefinitionOn_of_cover), for a nonempty system directed by inclusion”.

A nonempty family of ideal sheaves on a formal scheme 𝔛 in the sense of McQuillan, directed by inclusion, is a fundamental system of weak ideals of definition as soon as, over every affine formal open contained in a member of an open covering, its members are weak ideals of definition whose ideals of sections form a neighbourhood basis of zero.

theorem isFundamentalSystemOfWeakIdealsOfDefinitionOn_of_cover_of_isMcQuillanFormalScheme
    (hX : IsMcQuillanFormalScheme X) (𝒮 : Set (IdealSheaf X)) (hne : 𝒮.Nonempty)
    (hdir : ∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
      K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W)
    (𝒰 : Set (Opens X)) (hcover : sSup 𝒰 = ⊤)
    (h𝒮 : ∀ I ∈ 𝒮, ∀ V ∈ 𝒰, ∀ U : Opens X, U ≤ V → IsWeakAffineFormalOpen X U →
      TopologicalRing.IsWeakIdealOfDefinition (I.ideal U))
    (hbasis : ∀ V ∈ 𝒰, ∀ U : Opens X, U ≤ V → IsWeakAffineFormalOpen X U →
      (nhds (0 : (X.presheaf.obj (op U)).α)).HasBasis (· ∈ 𝒮)
        fun I : IdealSheaf X => (I.ideal U : Set (X.presheaf.obj (op U)).α)) :
    IsFundamentalSystemOfWeakIdealsOfDefinitionOn 𝒮 (IsWeakAffineFormalOpen X)
Tag 0AIW, a remark

Tag 0AIW in the Stacks Project.

AlgebraicGeometry.LocallyTopologicallyRingedSpace.IdealSheaf.IsIdealOfDefinitionOn, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinition.lean, line 180. The attribute's comment: “the definition, over a class 𝒜 of affine formal opens”.

An ideal sheaf on X is an ideal of definition over a class 𝒜 of opens — the affine formal open subschemes — when its ideal of sections over every open of 𝒜 is an ideal of definition of the topological ring of sections there.

def IsIdealOfDefinitionOn (I : IdealSheaf X) (𝒜 : Opens X → Prop) : Prop

AlgebraicGeometry.LocallyTopologicallyRingedSpace.IsFundamentalSystemOfIdealsOfDefinitionOn, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinition.lean, line 211. The attribute's comment: “the definition, over a class 𝒜 of affine formal opens”.

A family of ideal sheaves on X is a fundamental system of ideals of definition over a class 𝒜 of opens — the affine formal open subschemes — when each member is an ideal of definition and, over every open of 𝒜, their ideals of sections form a neighbourhood basis of zero in the topological ring of sections.

def IsFundamentalSystemOfIdealsOfDefinitionOn {X : LTRS.{u}} (𝒮 : Set (IdealSheaf X))
    (𝒜 : Opens X → Prop) : Prop

AlgebraicGeometry.LocallyTopologicallyRingedSpace.IdealSheaf.isIdealOfDefinitionOn_of_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinition.lean, line 333. The attribute's comment: “it suffices to check the ideal-of-definition condition on an affine open covering, CORRECTED: the condition is checked on the members of the class contained in a covering member, not on the covering members themselves, which is false as the source states it; the quasi-compactness hcompact and the refinement hrefine of the class of affine formal opens are part of the statement”.

Stacks 0AIW, the locality of the ideal-of-definition condition. Let 𝒰 be a covering of X and let 𝒜 be a class of quasi-compact opens — the affine formal open subschemes — whose members contained in an open cover that open. Then an ideal sheaf is an ideal of definition over 𝒜 as soon as its ideals of sections over the members of 𝒜 contained in a member of 𝒰 are ideals of definition.

Checking the members of 𝒰 alone would not do, for the same reason as in the weak case (IdealSheaf.isWeakIdealOfDefinitionOn_of_cover).

theorem isIdealOfDefinitionOn_of_cover (I : IdealSheaf X) (𝒜 : Opens X → Prop)
    (𝒰 : Set (Opens X)) (hcover : sSup 𝒰 = ⊤)
    (hcompact : ∀ U : Opens X, 𝒜 U → IsCompact (U : Set X))
    (hrefine : ∀ V ∈ 𝒰, ∀ W : Opens X, W ≤ V → ∀ x ∈ W,
      ∃ U : Opens X, U ≤ W ∧ x ∈ U ∧ 𝒜 U)
    (hI : ∀ V ∈ 𝒰, ∀ U : Opens X, U ≤ V → 𝒜 U →
      TopologicalRing.IsIdealOfDefinition (I.ideal U)) :
    I.IsIdealOfDefinitionOn 𝒜

AlgebraicGeometry.LocallyTopologicallyRingedSpace.isFundamentalSystemOfIdealsOfDefinitionOn_of_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinition.lean, line 356. The attribute's comment: “it suffices to check the fundamental-system condition on an affine open covering, CORRECTED in the same way as the ideal-of-definition condition, and granting hbasis: the neighbourhood-basis half is a condition on each individual affine formal open and there is nothing about it to transport along a covering”.

Stacks 0AIW, the locality of the fundamental-system condition: the neighbourhood-basis half is a condition on the individual opens of 𝒜, so only the ideal-of-definition half has to be transported along the covering, by IdealSheaf.isIdealOfDefinitionOn_of_cover.

theorem isFundamentalSystemOfIdealsOfDefinitionOn_of_cover {X : LTRS.{u}}
    (𝒮 : Set (IdealSheaf X)) (𝒜 : Opens X → Prop)
    (𝒰 : Set (Opens X)) (hcover : sSup 𝒰 = ⊤)
    (hcompact : ∀ U : Opens X, 𝒜 U → IsCompact (U : Set X))
    (hrefine : ∀ V ∈ 𝒰, ∀ W : Opens X, W ≤ V → ∀ x ∈ W,
      ∃ U : Opens X, U ≤ W ∧ x ∈ U ∧ 𝒜 U)
    (h𝒮 : ∀ I ∈ 𝒮, ∀ V ∈ 𝒰, ∀ U : Opens X, U ≤ V → 𝒜 U →
      TopologicalRing.IsIdealOfDefinition (I.ideal U))
    (hbasis : ∀ U : Opens X, 𝒜 U →
      (nhds (0 : (X.presheaf.obj (op U)).α)).HasBasis (· ∈ 𝒮)
        fun I : IdealSheaf X => (I.ideal U : Set (X.presheaf.obj (op U)).α)) :
    IsFundamentalSystemOfIdealsOfDefinitionOn 𝒮 𝒜

AlgebraicGeometry.LocallyTopologicallyRingedSpace.exists_isIdealOfDefinition_of_isFundamentalSystemOfWeakIdealsOfDefinitionOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinition.lean, line 409. The attribute's comment: “ℐ_λ is an ideal of definition for λ large, RESTRICTED to the finite affine open covering that quasi-compactness produces, as in the source's own argument; the sectionwise directedness hdir and nonemptiness hne of the system are the source's directedness of the index set Λ, and hadm is the admissibility of the rings of sections over the members of the class of affine formal opens”.

Stacks 0AIW, the eventual ideals of definition. Let X be quasi-compact and covered by the members of a class 𝒜 of opens — the affine formal open subschemes — over each of which the ring of sections has an ideal of definition, which on a formal scheme à la EGA is the admissibility of 𝒪_𝔛(𝔘). Let 𝒮 be a nonempty, sectionwise downward directed fundamental system of weak ideals of definition over 𝒜. Then there is a finite covering of X by members of 𝒜 and a member I₀ of 𝒮 such that every member of 𝒮 below I₀ has ideals of definition for its ideals of sections over the covering: an open ideal contained in an ideal of definition is an ideal of definition, and only the finitely many members of the covering have to be checked.

theorem exists_isIdealOfDefinition_of_isFundamentalSystemOfWeakIdealsOfDefinitionOn
    {X : LTRS.{u}} [CompactSpace ↥X] (𝒮 : Set (IdealSheaf X)) (𝒜 : Opens X → Prop)
    (hne : 𝒮.Nonempty)
    (hdir : ∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
      K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W)
    (hfund : IsFundamentalSystemOfWeakIdealsOfDefinitionOn 𝒮 𝒜)
    (hbase : ∀ x : X, ∃ U : Opens X, x ∈ U ∧ 𝒜 U)
    (hadm : ∀ U : Opens X, 𝒜 U →
      TopologicalRing.IsPreAdmissible (X.presheaf.obj (op U)).α) :
    ∃ 𝒰 : Set (Opens X), 𝒰.Finite ∧ (∀ V ∈ 𝒰, 𝒜 V) ∧ sSup 𝒰 = ⊤ ∧
      ∃ I₀ ∈ 𝒮, ∀ I ∈ 𝒮, (∀ W : Opens X, I.ideal W ≤ I₀.ideal W) →
        ∀ V ∈ 𝒰, TopologicalRing.IsIdealOfDefinition (I.ideal V)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.exists_isIdealOfDefinition_of_isFormalScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinition.lean, line 455. The attribute's comment: “ℐ_λ is an ideal of definition for λ large, on a quasi-compact formal scheme à la EGA and RESTRICTED to the finite affine open covering that quasi-compactness produces, as in the source's own argument; only the sectionwise directedness hdir and nonemptiness hne of the system are carried, and they are the source's directedness of the index set Λ”.

Stacks 0AIW, the eventual ideals of definition on a quasi-compact formal scheme à la EGA. Here the class of opens is the class of affine formal open subschemes, so the two geometric inputs of exists_isIdealOfDefinition_of_isFundamentalSystemOfWeakIdealsOfDefinitionOn are discharged: the affine formal opens cover X because X is a formal scheme, and the ring of sections over one of them is pre-admissible by Stacks 0AHY.

theorem exists_isIdealOfDefinition_of_isFormalScheme {X : LTRS.{u}} [CompactSpace ↥X]
    (hX : IsFormalScheme X) (𝒮 : Set (IdealSheaf X)) (hne : 𝒮.Nonempty)
    (hdir : ∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
      K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W)
    (hfund : IsFundamentalSystemOfWeakIdealsOfDefinitionOn 𝒮 (IsAffineFormalOpen X)) :
    ∃ 𝒰 : Set (Opens X), 𝒰.Finite ∧ (∀ V ∈ 𝒰, IsAffineFormalOpen X V) ∧ sSup 𝒰 = ⊤ ∧
      ∃ I₀ ∈ 𝒮, ∀ I ∈ 𝒮, (∀ W : Opens X, I.ideal W ≤ I₀.ideal W) →
        ∀ V ∈ 𝒰, TopologicalRing.IsIdealOfDefinition (I.ideal V)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.exists_isWeakIdealOfDefinitionOn_not_isIdealOfDefinitionOn_of_nilradical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinition.lean, line 572. The attribute's comment: “we do NOT get the same correspondence as in Stacks 0AIV: already on a formal scheme à la EGA the ideal-of-definition condition is strictly stronger than the weak one, witnessed by the nilradical of the pseudo-discretisation of a one-prime scheme whose nilradical is not nilpotent”.

Stacks 0AIW, the separation of the ideal-of-definition condition from the weak one of Stacks 0AIV, at the level of ideal sheaves on a formal scheme à la EGA. Let R be a nontrivial commutative ring with exactly one prime ideal whose nilradical is not nilpotent. Then the pseudo-discretisation of Spec R is a formal scheme à la EGA carrying an ideal sheaf — the nilradical — which is a weak ideal of definition over its affine formal open subschemes and is not an ideal of definition over them. This is why the correspondence of Stacks 0AIV between weak ideals of definition and thickenings cannot restrict to a correspondence between ideals of definition and thickenings.

theorem exists_isWeakIdealOfDefinitionOn_not_isIdealOfDefinitionOn_of_nilradical
    (R : Type u) [CommRing R] [Nontrivial R] [Subsingleton (PrimeSpectrum R)]
    (hnil : ∀ n : ℕ, (nilradical R) ^ n ≠ ⊥) :
    ∃ (X : LTRS.{u}) (_ : IsFormalScheme X) (I : IdealSheaf X),
      I.IsWeakIdealOfDefinitionOn (IsAffineFormalOpen X) ∧
        ¬ I.IsIdealOfDefinitionOn (IsAffineFormalOpen X)

AlgebraicGeometry.FormalScheme.exists_isFundamentalSystemOfIdealsOfDefinitionOn_of_isFppfColimitOfThickenings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinitionColimit.lean, line 192. The attribute's comment: “the only if direction: for 𝔛 quasi-compact, if h_𝔛 is a colimit of schemes as in Lemma 0AIU (colimit in fppf sheaves) then there exists a fundamental system of ideals of definition for 𝔛, for ideal sheaves in the source's generality”.

Stacks 0AIW, the "only if" direction, for arbitrary ideal sheaves. If the functor of points h_𝔛 of a quasi-compact formal scheme 𝔛 à la EGA is a colimit of schemes along thickenings in fppf sheaves, as in Stacks 0AIU, then 𝔛 has a fundamental system of ideals of definition, with the definitions of the source: ideal sheaves whose ideals of sections over every affine formal open are ideals of definition, and a neighbourhood basis of zero there.

theorem FormalScheme.exists_isFundamentalSystemOfIdealsOfDefinitionOn_of_isFppfColimitOfThickenings
    (X : FormalScheme.{u}) [CompactSpace ↥X.obj]
    (h : X.toMcQuillanFormalScheme.IsFppfColimitOfThickenings) :
    ∃ 𝒮 : Set (IdealSheaf X.obj),
      IsFundamentalSystemOfIdealsOfDefinitionOn 𝒮 (IsAffineFormalOpen X.obj)

AlgebraicGeometry.FormalScheme.isFppfColimitOfThickenings_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinitionColimit.lean, line 217. The attribute's comment: “corrected form: for 𝔛 quasi-compact, h_𝔛 is a colimit of schemes as in Lemma 0AIU (colimit in fppf sheaves) if and only if there exists a fundamental system of ideals of definition for 𝔛 cut out by their sections over the affine formal opens; the if direction as printed is false: see FormalScheme.not_forall_isFppfColimitOfThickenings_of_exists (the only if direction for arbitrary ideal sheaves is exists_isFundamentalSystemOfIdealsOfDefinitionOn_of_isFppfColimitOfThickenings)”.

Stacks 0AIW. The functor of points h_𝔛 of a quasi-compact formal scheme 𝔛 à la EGA is a colimit of schemes along thickenings in fppf sheaves, as in Stacks 0AIU, if and only if 𝔛 has a fundamental system of ideals of definition cut out by their sections over the affine formal opens.

This is the corrected form of the remark. The "only if" direction holds without the cut-out condition (FormalScheme.exists_isFundamentalSystemOfIdealsOfDefinitionOn_of_isFppfColimitOfThickenings). The source's definition of an ideal of definition is sectionwise and does not ask for the cut-out condition (the analogue of ℐ|_𝔘 = ℐ(𝔘)^Δ in EGA), and with it the "if" direction is false (FormalScheme.not_forall_isFppfColimitOfThickenings_of_exists).

theorem FormalScheme.isFppfColimitOfThickenings_iff (X : FormalScheme.{u}) [CompactSpace ↥X.obj] :
    X.toMcQuillanFormalScheme.IsFppfColimitOfThickenings ↔ ∃ 𝒮 : Set (IdealSheaf X.obj),
      (∀ I ∈ 𝒮, I.IsCutOutOn (IsAffineFormalOpen X.obj)) ∧
        IsFundamentalSystemOfIdealsOfDefinitionOn 𝒮 (IsAffineFormalOpen X.obj)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.not_forall_exists_isIdealOfDefinitionOn_of_isFundamentalSystemOfWeakIdealsOfDefinitionOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinitionCounterexample.lean, line 730. The attribute's comment: “ℐ_λ is an ideal of definition for λ large: FALSE as printed, for ideal sheaves in the source's generality, on a quasi-compact (even affine) formal scheme à la EGA and for a nonempty directed system; the true statement is over the members of a finite affine open covering, exists_isIdealOfDefinition_of_isFormalScheme”.

Stacks 0AIW, the eventual ideals of definition, is false as printed. It is not true that on every quasi-compact formal scheme à la EGA a fundamental system {ℐ_λ} of weak ideals of definition consists of ideals of definition for λ sufficiently large, even for a nonempty system directed by inclusion: in the system of exists_isFundamentalSystemOfWeakIdealsOfDefinitionOn_forall_not_isIdealOfDefinitionOn no member at all is an ideal of definition over the affine formal opens.

The source's argument shows that ℐ_λ(𝔘) is an ideal of definition for λ large on the finitely many members 𝔘 of an affine open covering, which is true (exists_isIdealOfDefinition_of_isFormalScheme), and concludes by the locality claim refuted in not_forall_isIdealOfDefinitionOn_of_cover.

theorem not_forall_exists_isIdealOfDefinitionOn_of_isFundamentalSystemOfWeakIdealsOfDefinitionOn :
    ¬ ∀ (X : LTRS.{0}), IsFormalScheme X → CompactSpace X → ∀ 𝒮 : Set (IdealSheaf X),
      𝒮.Nonempty →
      (∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
        K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W) →
      IsFundamentalSystemOfWeakIdealsOfDefinitionOn 𝒮 (IsAffineFormalOpen X) →
      ∃ I₀ ∈ 𝒮, ∀ I ∈ 𝒮, (∀ W : Opens X, I.ideal W ≤ I₀.ideal W) →
        I.IsIdealOfDefinitionOn (IsAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.not_forall_isIdealOfDefinitionOn_of_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinitionCounterexample.lean, line 763. The attribute's comment: “it suffices to check the ideal-of-definition condition on an affine open covering: FALSE as printed, for ideal sheaves in the source's generality, already for the covering of an affine formal scheme by itself”.

Stacks 0AIW, the locality of the ideal-of-definition condition, is false as printed. It is not true that an ideal sheaf on a formal scheme à la EGA is an ideal of definition as soon as its ideals of sections over the members of an affine open covering are ideals of definition: on the pseudo-discretisation of Spec (ℤ[X₀, X₁, …] / (X_k ^ (k + 1))) the sections with nilpotent germs vanishing outside D(n!) are zero over the whole space, which is affine, and are not an ideal of definition over D(n!).

The corrected statement checks the condition on the affine formal opens contained in the members of the covering: IdealSheaf.isIdealOfDefinitionOn_of_cover.

theorem not_forall_isIdealOfDefinitionOn_of_cover :
    ¬ ∀ (X : LTRS.{0}), IsFormalScheme X → ∀ (I : IdealSheaf X) (𝒰 : Set (Opens X)),
      (∀ V ∈ 𝒰, IsAffineFormalOpen X V) → sSup 𝒰 = ⊤ →
      (∀ V ∈ 𝒰, TopologicalRing.IsIdealOfDefinition (I.ideal V)) →
      I.IsIdealOfDefinitionOn (IsAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.not_forall_isFundamentalSystemOfIdealsOfDefinitionOn_of_hasBasis_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinitionCounterexample.lean, line 796. The attribute's comment: “it suffices to check the fundamental-system condition on an affine open covering: FALSE as printed, for ideal sheaves in the source's generality, already for a single ideal of definition and the covering of an affine formal scheme by itself”.

Stacks 0AIW, the locality of the fundamental-system condition, is false as printed. It is not true that a family of ideals of definition on a formal scheme à la EGA is a fundamental system as soon as its ideals of sections form a neighbourhood basis of zero over the members of an affine open covering, even for a nonempty directed family whose members are ideals of definition over every affine formal open: on the pseudo-discretisation of Spec (ℤ[X₀, X₁, …] / (X_k ^ (k + 1))) the sections whose germs are multiples of the germ of X₁, vanishing outside D(n!), form an ideal of definition which is zero over the whole space, which is affine, but whose sections over D(n!), which are discrete, contain X₁ ≠ 0.

The corrected statement checks the condition on the affine formal opens contained in the members of the covering: isFundamentalSystemOfIdealsOfDefinitionOn_of_cover_of_directed.

theorem not_forall_isFundamentalSystemOfIdealsOfDefinitionOn_of_hasBasis_cover :
    ¬ ∀ (X : LTRS.{0}), IsFormalScheme X → ∀ (𝒮 : Set (IdealSheaf X)) (𝒰 : Set (Opens X)),
      𝒮.Nonempty →
      (∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
        K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W) →
      (∀ V ∈ 𝒰, IsAffineFormalOpen X V) → sSup 𝒰 = ⊤ →
      (∀ I ∈ 𝒮, I.IsIdealOfDefinitionOn (IsAffineFormalOpen X)) →
      (∀ V ∈ 𝒰, (nhds (0 : (X.presheaf.obj (op V)).α)).HasBasis (· ∈ 𝒮)
        fun I : IdealSheaf X => (I.ideal V : Set (X.presheaf.obj (op V)).α)) →
      IsFundamentalSystemOfIdealsOfDefinitionOn 𝒮 (IsAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.exists_forall_isIdealOfDefinitionOn_of_isCutOutOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinitionCutOut.lean, line 278. The attribute's comment: “ℐ_λ is an ideal of definition for λ large, over EVERY affine formal open, for a directed system whose members are cut out by their sections over the affine formal opens (the condition of Stacks 0AIV singling out the ideal sheaves of thickenings); for arbitrary ideal sheaves the statement is false, not_forall_exists_isIdealOfDefinitionOn_of_isFundamentalSystemOfWeakIdealsOfDefinitionOn”.

Stacks 0AIW, the eventual ideals of definition, for a system cut out by its sections. On a quasi-compact formal scheme à la EGA, let 𝒮 be a nonempty, directed fundamental system of weak ideals of definition over the affine formal opens, each member cut out by its sections over the affine formal opens. Then there is a member I₀ such that every member below it is an ideal of definition over every affine formal open.

The finite affine covering produced by quasi-compactness gives I₀ with ideals of definition over the members of the covering (exists_isIdealOfDefinition_of_isFormalScheme), and IdealSheaf.pow_ideal_le_of_isCutOutOn carries the comparison of powers from the covering to an arbitrary affine formal open.

theorem exists_forall_isIdealOfDefinitionOn_of_isCutOutOn {X : LTRS.{u}} [CompactSpace ↥X]
    (hX : IsFormalScheme X) (𝒮 : Set (IdealSheaf X)) (hne : 𝒮.Nonempty)
    (hdir : ∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
      K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W)
    (hfund : IsFundamentalSystemOfWeakIdealsOfDefinitionOn 𝒮 (IsAffineFormalOpen X))
    (hcut : ∀ I ∈ 𝒮, I.IsCutOutOn (IsAffineFormalOpen X)) :
    ∃ I₀ ∈ 𝒮, ∀ I ∈ 𝒮, (∀ W : Opens X, I.ideal W ≤ I₀.ideal W) →
      I.IsIdealOfDefinitionOn (IsAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.IdealSheaf.isIdealOfDefinitionOn_of_cover_of_isCutOutOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinitionCutOutLocality.lean, line 162. The attribute's comment: “it suffices to check the ideal-of-definition condition on the members of an affine open covering: for ideal sheaves cut out by their sections over the affine formal opens (IdealSheaf.IsCutOutOn), the class of the colimit criterion FormalScheme.isFppfColimitOfThickenings_iff; for an arbitrary ideal sheaf it is false (not_forall_isIdealOfDefinitionOn_of_cover)”.

Stacks 0AIW, the ideal-of-definition condition may be checked on the members of an affine open covering, for ideal sheaves cut out by their sections. Let 𝔛 be a formal scheme à la EGA and ℐ an ideal sheaf cut out by its sections over the affine formal opens (IdealSheaf.IsCutOutOn). If ℐ(𝔙) is an ideal of definition for the members 𝔙 of a covering of 𝔛 by affine formal opens, then ℐ is an ideal of definition.

These are the ideal sheaves of the colimit criterion of Stacks 0AIW, FormalScheme.isFppfColimitOfThickenings_iff. For an arbitrary ideal sheaf checking the covering members is not enough (not_forall_isIdealOfDefinitionOn_of_cover), and the condition must then be checked on the affine formal opens inside the covering members (IdealSheaf.isIdealOfDefinitionOn_of_cover_of_isFormalScheme). Over an affine formal open inside a covering member the condition is IdealSheaf.isIdealOfDefinition_of_le_of_isCutOutOn.

theorem IdealSheaf.isIdealOfDefinitionOn_of_cover_of_isCutOutOn
    (hX : IsFormalScheme X) (I : IdealSheaf X)
    (hC : I.IsCutOutOn (IsAffineFormalOpen X)) (𝒰 : Set (Opens X))
    (h𝒰 : ∀ V ∈ 𝒰, IsAffineFormalOpen X V) (hcover : sSup 𝒰 = ⊤)
    (hI : ∀ V ∈ 𝒰, IsIdealOfDefinition (I.ideal V)) :
    I.IsIdealOfDefinitionOn (IsAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.isFundamentalSystemOfIdealsOfDefinitionOn_of_cover_of_isCutOutOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinitionCutOutLocality.lean, line 191. The attribute's comment: “it suffices to check the fundamental-system condition on the members of an affine open covering: for a family indexed by a directed set, as in the source, of ideal sheaves cut out by their sections over the affine formal opens (IdealSheaf.IsCutOutOn), the class of the colimit criterion FormalScheme.isFppfColimitOfThickenings_iff; for arbitrary ideal sheaves it is false (not_forall_isFundamentalSystemOfIdealsOfDefinitionOn_of_hasBasis_cover)”. References: EGA I (10.3.7), “more general”.

Stacks 0AIW, the fundamental-system condition may be checked on the members of an affine open covering, for ideal sheaves cut out by their sections. Let 𝔛 be a formal scheme à la EGA and {ℐ_λ} a nonempty family of ideal sheaves, directed by inclusion, each cut out by its sections over the affine formal opens. If over the members 𝔙 of a covering of 𝔛 by affine formal opens the ℐ_λ(𝔙) are ideals of definition forming a neighbourhood basis of zero, then {ℐ_λ} is a fundamental system of ideals of definition.

The family is indexed, as in the source, by a directed set (nonempty, by Stacks' definition of a directed set), with ℐ_μ ⊆ ℐ_λ for μ ≥ λ; over an affine formal open inside a single covering member no directedness is used (hasBasis_of_le_of_isCutOutOn). These are the families of the colimit criterion FormalScheme.isFppfColimitOfThickenings_iff. For arbitrary ideal sheaves checking the covering members is not enough (not_forall_isFundamentalSystemOfIdealsOfDefinitionOn_of_hasBasis_cover).

theorem isFundamentalSystemOfIdealsOfDefinitionOn_of_cover_of_isCutOutOn
    (hX : IsFormalScheme X) (𝒮 : Set (IdealSheaf X))
    (hC : ∀ I ∈ 𝒮, I.IsCutOutOn (IsAffineFormalOpen X)) (hne : 𝒮.Nonempty)
    (hdir : ∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
      K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W)
    (𝒰 : Set (Opens X)) (h𝒰 : ∀ V ∈ 𝒰, IsAffineFormalOpen X V) (hcover : sSup 𝒰 = ⊤)
    (h𝒮 : ∀ I ∈ 𝒮, ∀ V ∈ 𝒰, IsIdealOfDefinition (I.ideal V))
    (hbasis : ∀ V ∈ 𝒰, (nhds (0 : (X.presheaf.obj (op V)).α)).HasBasis (· ∈ 𝒮)
      fun I : IdealSheaf X => (I.ideal V : Set (X.presheaf.obj (op V)).α)) :
    IsFundamentalSystemOfIdealsOfDefinitionOn 𝒮 (IsAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.isFundamentalSystemOfIdealsOfDefinitionOn_of_cover_of_directed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinitionLocality.lean, line 85. The attribute's comment: “it suffices to check the fundamental-system condition on an affine open covering, CORRECTED: both halves are checked on the members of the class contained in a covering member, not on the covering members themselves, which is false as the source states it (not_forall_isFundamentalSystemOfIdealsOfDefinitionOn_of_hasBasis_cover), and the system is nonempty and directed by inclusion (hne, hdir), the source's directed index set Λ; the quasi-compactness hcompact and the refinement hrefine of the class of affine formal opens are part of the statement”.

Stacks 0AIW, the locality of the fundamental-system condition. Let 𝒰 be a covering of X and let 𝒜 be a class of quasi-compact opens — the affine formal open subschemes — whose members contained in an open cover that open. Let 𝒮 be a nonempty family of ideal sheaves, downward directed by inclusion, such that over every open of 𝒜 contained in a member of 𝒰 each member of 𝒮 has an ideal of definition for its ideal of sections and these ideals of sections form a neighbourhood basis of zero. Then 𝒮 is a fundamental system of ideals of definition over 𝒜.

Both halves of the condition are transported along the covering: the ideal-of-definition half by IdealSheaf.isIdealOfDefinitionOn_of_cover, the neighbourhood-basis half by IdealSheaf.hasBasis_ideal_of_isCompact.

theorem isFundamentalSystemOfIdealsOfDefinitionOn_of_cover_of_directed {X : LTRS.{u}}
    (𝒮 : Set (IdealSheaf X)) (𝒜 : Opens X → Prop) (hne : 𝒮.Nonempty)
    (hdir : ∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
      K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W)
    (𝒰 : Set (Opens X)) (hcover : sSup 𝒰 = ⊤)
    (hcompact : ∀ U : Opens X, 𝒜 U → IsCompact (U : Set X))
    (hrefine : ∀ V ∈ 𝒰, ∀ W : Opens X, W ≤ V → ∀ x ∈ W,
      ∃ U : Opens X, U ≤ W ∧ x ∈ U ∧ 𝒜 U)
    (h𝒮 : ∀ I ∈ 𝒮, ∀ V ∈ 𝒰, ∀ U : Opens X, U ≤ V → 𝒜 U →
      TopologicalRing.IsIdealOfDefinition (I.ideal U))
    (hbasis : ∀ V ∈ 𝒰, ∀ U : Opens X, U ≤ V → 𝒜 U →
      (nhds (0 : (X.presheaf.obj (op U)).α)).HasBasis (· ∈ 𝒮)
        fun I : IdealSheaf X => (I.ideal U : Set (X.presheaf.obj (op U)).α)) :
    IsFundamentalSystemOfIdealsOfDefinitionOn 𝒮 𝒜

AlgebraicGeometry.LocallyTopologicallyRingedSpace.IdealSheaf.isIdealOfDefinitionOn_of_cover_of_isFormalScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinitionLocality.lean, line 117. The attribute's comment: “it suffices to check the ideal-of-definition condition on an affine open covering, CORRECTED, on a formal scheme à la EGA with no further hypothesis: the condition is checked on the affine formal opens contained in a covering member, not on the covering members themselves, which is false as the source states it (not_forall_isIdealOfDefinitionOn_of_cover)”.

Stacks 0AIW, the locality of the ideal-of-definition condition on a formal scheme à la EGA. An ideal sheaf is an ideal of definition as soon as its ideals of sections over the affine formal open subschemes contained in the members of some covering are ideals of definition. The affine formal open subschemes are quasi-compact and form a basis, which are the two hypotheses IdealSheaf.isIdealOfDefinitionOn_of_cover asks of the class of opens.

theorem IdealSheaf.isIdealOfDefinitionOn_of_cover_of_isFormalScheme {X : LTRS.{u}}
    (hX : IsFormalScheme X) (I : IdealSheaf X) (𝒰 : Set (Opens X)) (hcover : sSup 𝒰 = ⊤)
    (hI : ∀ V ∈ 𝒰, ∀ U : Opens X, U ≤ V → IsAffineFormalOpen X U →
      TopologicalRing.IsIdealOfDefinition (I.ideal U)) :
    I.IsIdealOfDefinitionOn (IsAffineFormalOpen X)

AlgebraicGeometry.LocallyTopologicallyRingedSpace.isFundamentalSystemOfIdealsOfDefinitionOn_of_cover_of_isFormalScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/IdealOfDefinitionLocality.lean, line 136. The attribute's comment: “it suffices to check the fundamental-system condition on an affine open covering, CORRECTED, on a formal scheme à la EGA with no further hypothesis: both halves are checked on the affine formal opens contained in a covering member, not on the covering members themselves, which is false as the source states it (not_forall_isFundamentalSystemOfIdealsOfDefinitionOn_of_hasBasis_cover), for a nonempty system directed by inclusion (hne, hdir), the source's directed index set Λ”.

Stacks 0AIW, the locality of the fundamental-system condition on a formal scheme à la EGA, with no hypothesis on the class of opens: for a nonempty family directed by inclusion, both halves of the condition may be checked on the affine formal open subschemes contained in the members of a covering.

theorem isFundamentalSystemOfIdealsOfDefinitionOn_of_cover_of_isFormalScheme {X : LTRS.{u}}
    (hX : IsFormalScheme X) (𝒮 : Set (IdealSheaf X)) (hne : 𝒮.Nonempty)
    (hdir : ∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
      K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W)
    (𝒰 : Set (Opens X)) (hcover : sSup 𝒰 = ⊤)
    (h𝒮 : ∀ I ∈ 𝒮, ∀ V ∈ 𝒰, ∀ U : Opens X, U ≤ V → IsAffineFormalOpen X U →
      TopologicalRing.IsIdealOfDefinition (I.ideal U))
    (hbasis : ∀ V ∈ 𝒰, ∀ U : Opens X, U ≤ V → IsAffineFormalOpen X U →
      (nhds (0 : (X.presheaf.obj (op U)).α)).HasBasis (· ∈ 𝒮)
        fun I : IdealSheaf X => (I.ideal U : Set (X.presheaf.obj (op U)).α)) :
    IsFundamentalSystemOfIdealsOfDefinitionOn 𝒮 (IsAffineFormalOpen X)

AlgebraicGeometry.FormalScheme.not_forall_isFppfColimitOfThickenings_of_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/TwistedDoubleColimit.lean, line 65. The attribute's comment: “the if direction as printed (sectionwise ideals of definition) is false: a quasi-compact formal scheme with a fundamental system of ideals of definition whose functor of points h_𝔛 is not a colimit of schemes as in Lemma 0AIU (colimit in fppf sheaves); corrected form: FormalScheme.isFppfColimitOfThickenings_iff”.

Stacks 0AIW, the "if" direction as printed, is false. There is a quasi-compact formal scheme 𝔛 à la EGA (the twisted double AlgebraicGeometry.TwistedDouble.𝔛) which has a fundamental system of ideals of definition, in the source's sectionwise sense, but whose functor of points h_𝔛 is not a colimit of schemes along thickenings in fppf sheaves, as in Stacks 0AIU.

The corrected form is AlgebraicGeometry.FormalScheme.isFppfColimitOfThickenings_iff, where the ideals of definition are cut out by their sections over the affine formal opens.

theorem FormalScheme.not_forall_isFppfColimitOfThickenings_of_exists :
    ¬ ∀ (X : FormalScheme.{0}) [CompactSpace X.obj],
      (∃ 𝒮 : Set (IdealSheaf X.obj),
        IsFundamentalSystemOfIdealsOfDefinitionOn 𝒮 (IsAffineFormalOpen X.obj)) →
        X.toMcQuillanFormalScheme.IsFppfColimitOfThickenings

AlgebraicGeometry.FormalSpace.WeakIdealOfDefinitionExample.isThickening_residueField_and_not_isIdealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/IdealOfDefinitionNotAllThickenings.lean, line 91. The attribute's comment: “we do NOT get the same correspondence between ideals of definition and thickenings as in Stacks 0AIV: the residue-field stage of Spf A is a thickening while the weak ideal of definition it corresponds to is not an ideal of definition (Stacks 0CB8); the presentation D of the formal spectrum over a big fppf site is an input, as it is throughout the statements of Stacks 0CB8 combined here”.

Stacks 0AIW, the failure of the correspondence of Stacks 0AIV for ideals of definition. For a valuation ring (A, 𝔪, κ) which is (π)-adically complete for a nonzero π ∈ 𝔪 whose radical is 𝔪, and whose maximal ideal is not finitely generated, the residue-field stage Spec κ ⟶ Spf A of the formal spectrum is a thickening, while the weak ideal of definition 𝔪 to which the correspondence of Stacks 0AIV attaches it is not an ideal of definition. So the correspondence between weak ideals of definition and thickenings does not restrict to a correspondence between ideals of definition and thickenings.

theorem isThickening_residueField_and_not_isIdealOfDefinition [IsDomain A]
    (hval : IsValuationRing A) (hπm : π ∈ maximalIdeal A)
    (hadic : IsAdic (Ideal.span ({π} : Set A)))
    (hrad : (Ideal.span ({π} : Set A)).radical = maximalIdeal A)
    (hnotfg : ¬ (maximalIdeal A).FG)
    {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    (D : QuotientSystem B S hS A) :
    let J : { I : Ideal A // TopologicalRing.IsWeakIdealOfDefinition I } :=
      ⟨maximalIdeal A, isWeakIdealOfDefinition_maximalIdeal π hadic hrad⟩
    (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)))
      (formalSpectrumInclusion D (OrderDual.toDual J)) ∧
      ¬ TopologicalRing.IsIdealOfDefinition J.1

PadicComplexInt.isWeakIdealOfDefinition_maximalIdeal_and_not_isIdealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/IdealOfDefinitionNotAllThickenings.lean, line 127. The attribute's comment: “the negative clause is not vacuous: in the ring of integers of ℂ_[p] the maximal ideal is a weak ideal of definition and is not an ideal of definition”.

Stacks 0AIW, the negative clause on the example of Stacks 0CB8. The maximal ideal of the ring of integers of the field ℂ_[p] of p-adic complex numbers is a weak ideal of definition of that admissible topological ring, and it is not an ideal of definition. So the two notions differ, and the correspondence of Stacks 0AIV between weak ideals of definition and thickenings cannot restrict to one between ideals of definition and thickenings.

theorem isWeakIdealOfDefinition_maximalIdeal_and_not_isIdealOfDefinition :
    TopologicalRing.IsWeakIdealOfDefinition (maximalIdeal (PadicComplexInt p)) ∧
      ¬ TopologicalRing.IsIdealOfDefinition (maximalIdeal (PadicComplexInt p))

PadicComplexInt.isThickening_residueField_not_from_idealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/IdealOfDefinitionNotAllThickenings.lean, line 142. The attribute's comment: “the negative clause on the example of Stacks 0CB8: a thickening of the formal spectrum of the ring of integers of ℂ_[p] whose weak ideal of definition is not an ideal of definition; the presentation D of the formal spectrum over a big fppf site is an input”.

Stacks 0AIW, the negative clause on the example of Stacks 0CB8, geometrically: the residue-field stage Spec ℂ_[p]^- ⟶ Spf 𝒪_{ℂ_p} of the formal spectrum of the ring of integers of ℂ_[p] is a thickening whose weak ideal of definition, the maximal ideal, is not an ideal of definition.

theorem isThickening_residueField_not_from_idealOfDefinition
    {B : BigFppfSite.{0}} {S : Scheme.{0}} {hS : B.Contains S}
    (D : QuotientSystem B S hS (PadicComplexInt p)) :
    let J : { I : Ideal (PadicComplexInt p) // TopologicalRing.IsWeakIdealOfDefinition I } :=
      ⟨maximalIdeal (PadicComplexInt p),
        (isWeakIdealOfDefinition_maximalIdeal_and_not_isIdealOfDefinition p).1⟩
    (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{0})
        (BigFppfOver.toScheme B S hS)))
      (formalSpectrumInclusion D (OrderDual.toDual J)) ∧
      ¬ TopologicalRing.IsIdealOfDefinition J.1

PadicComplexInt.exists_isWeakIdealOfDefinitionOn_not_isIdealOfDefinitionOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/IdealOfDefinitionNotAllThickenings.lean, line 241. The attribute's comment: “the negative clause is not vacuous at the level of ideal sheaves: an explicit formal scheme à la EGA with a weak ideal of definition that is not an ideal of definition”.

Stacks 0AIW, the negative clause at the level of ideal sheaves, unconditionally. The pseudo-discretisation of Spec (𝒪_{ℂ_p}/(p)) is a formal scheme à la EGA whose nilradical is a weak ideal of definition over its affine formal open subschemes and is not an ideal of definition over them: the ring has the single prime 𝔪/(p), and no power of its nilradical vanishes because no power of 𝔪 lies inside (p).

theorem exists_isWeakIdealOfDefinitionOn_not_isIdealOfDefinitionOn
    (q : ℕ) [Fact (Nat.Prime q)] :
    ∃ (X : LTRS.{0}) (_ : IsFormalScheme X) (I : LocallyTopologicallyRingedSpace.IdealSheaf X),
      I.IsWeakIdealOfDefinitionOn (IsAffineFormalOpen X) ∧
        ¬ I.IsIdealOfDefinitionOn (IsAffineFormalOpen X)

TopologicalRing.isIdealOfDefinition_of_le_of_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/IdealOfDefinition.lean, line 106. The attribute's comment: “in an admissible topological ring all sufficiently small open ideals are ideals of definition: any open ideal contained in an ideal of definition is one”.

Stacks 0AIW. An open ideal contained in an ideal of definition is an ideal of definition: its powers lie inside the corresponding powers of the larger ideal, and those are cofinal among the neighbourhoods of zero. Since in an admissible topological ring the open ideals form a basis of neighbourhoods of zero, this is the source's observation that all sufficiently small open ideals of such a ring are ideals of definition.

public theorem isIdealOfDefinition_of_le_of_isOpen {I J : Ideal R}
    (hJ : IsIdealOfDefinition J) (hI : IsOpen (I : Set R)) (hIJ : I ≤ J) :
    IsIdealOfDefinition I
Sources
LeanAlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_colimit_thickenings · AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_colimit_isRepresentableThickeningULift · PadicComplexInt.isWeakIdealOfDefinition_maximalIdeal_and_not_isIdealOfDefinition · PadicComplexInt.isIdealOfDefinition_span_p · AlgebraicGeometry.FormalSpace.WeakIdealOfDefinitionExample.isWeakIdealOfDefinition_maximalIdeal · AlgebraicGeometry.FormalSpace.WeakIdealOfDefinitionExample.isWeaklyAdmissible · AlgebraicGeometry.FormalSpace.WeakIdealOfDefinitionExample.isAffineFormalAlgebraicSpace_formalSpectrum · AlgebraicGeometry.FormalSpace.WeakIdealOfDefinitionExample.isRelativelyRepresentable_residueField

Section87.14 Completion along a closed subset#

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

Tag 0AIY, a lemma

Tag 0AIY in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_completionSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionAffineMcQuillan.lean, line 895. The attribute's comment: “McQuillan affine formal algebraic space”.

Stacks 0AIY. Let S be a scheme, let X = Spec A be an affine scheme over S lying in the big fppf site and let T ⊆ |X| be a closed subset. The completion of X along T — the fppf sheaf attached to the functor sending U to the set of morphisms f : U ⟶ X with f(|U|) ⊆ T — is a McQuillan affine formal algebraic space: it is the directed colimit of the affine thickenings Spec (A ⧸ J) over the ideals J with V(J) = T, and the projections from the inverse limit of the section rings of that presentation onto each stage are surjective.

theorem hasSomeSurjectivePresentation_completionSheaf
    (T : Set ((BigFppfOver.toScheme B S hS).obj (affineOver B S hS hA f))) (hT : IsClosed T)
    (hatlas : HasStageAtlas B S hS hA f (PrimeSpectrum.vanishingIdeal T)) :
    HasSomeSurjectivePresentation B S hS
      (Space.completionSheaf B S hS (yoneda.obj (affineOver B S hS hA f))
        (supportedPoints B S hS (affineOver B S hS hA f) T))

AlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_completionSheaf_of_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionAffineStageAtlas.lean, line 116. The attribute's comment: “McQuillan affine formal algebraic space”.

Stacks 0AIY. Let S be a scheme, let X = Spec A be an affine scheme over S lying in the big fppf site and let T ⊆ |X| be a closed subset. The completion of X along T — the fppf sheaf attached to the functor sending U to the set of morphisms f : U ⟶ X with f(|U|) ⊆ T — is a McQuillan affine formal algebraic space.

This is AlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_completionSheaf with its atlas hypothesis discharged by AlgebraicGeometry.FormalSpace.hasStageAtlas.

theorem hasSomeSurjectivePresentation_completionSheaf_of_isClosed
    (T : Set ((BigFppfOver.toScheme B S hS).obj (affineOver B S hS hA f))) (hT : IsClosed T) :
    HasSomeSurjectivePresentation B S hS
      (Space.completionSheaf B S hS (yoneda.obj (affineOver B S hS hA f))
        (supportedPoints B S hS (affineOver B S hS hA f) T))

AlgebraicGeometry.FormalSpace.isIso_toSheafify_completionSubfunctor_affineOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSetTheoretic.lean, line 386. The attribute's comment: “the functor”.

Let X = Spec A be an affine scheme over S lying in the site and T ⊆ |X| a subset. The functor sending an object U of the big fppf site of S to the morphisms f : U ⟶ X with f(|U|) ⊆ T is an fppf sheaf: the map to its sheafification, the completion of AlgebraicGeometry.Space.completionSheaf, is an isomorphism.

theorem isIso_toSheafify_completionSubfunctor_affineOver {A : Type u} [CommRing A]
    (hA : B.Contains (Spec (.of A))) (f : Spec (.of A) ⟶ S)
    (T : Set ((BigFppfOver.toScheme B S hS).obj (affineOver B S hS hA f))) :
    IsIso (toSheafify (BigFppfOver.topology B S hS)
      (Space.completionSubfunctor B S hS (yoneda.obj (affineOver B S hS hA f))
        (supportedPoints B S hS (affineOver B S hS hA f) T)).toFunctor)
Tag 0AIZ, a lemma

Tag 0AIZ in the Stacks Project.

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_completionSheaf_of_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionAlgebraicSpaceAtlas.lean, line 512.

Stacks 0AIZ. Let S be a scheme, let X be an algebraic space over S and let T ⊆ |X| be a closed subset. 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 affine étale charts of X are those of AlgebraicGeometry.FormalSpace.exists_affine_etale_charts, the inverse image of T on each is the set of points supported in a closed subset (AlgebraicGeometry.FormalSpace.exists_isClosed_preimage_eq_supportedPoints), the stage atlas of each chart completion is AlgebraicGeometry.FormalSpace.hasStageAtlas, and the set-theoretic condition is AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_completionSheaf; with these the atlas argument of AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_completionSheaf applies.

theorem isFormalAlgebraicSpace_completionSheaf_of_isClosed
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (T : Set (Space.points B S hS X)) (hT : @IsClosed _ (Space.pointTopology B S hS X) T) :
    IsFormalAlgebraicSpace B S hS (Space.completionSheaf B S hS X T)

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_completionSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFormalAlgebraicSpace.lean, line 236. The attribute's comment: “assumes the affine étale charts of X as hA, str, a, ha, hcov, their closed point sets as hTi and hTpts, the affine case's HasStageAtlas as hstage, and the 0AIS condition as hset”.

Stacks 0AIZ. Let S be a scheme, let X be an algebraic space over S and let T ⊆ |X| be a closed subset. 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 affine charts of X along the inverse images of T form an atlas of X_{/T}, and each of them is an affine formal algebraic space by the affine case, Stacks 0AIY.

The affine étale charts of X, the description of the inverse image of T on each of them as the points supported in a closed subset, the per-chart hypothesis HasStageAtlas of the affine case and the set-theoretic condition of Stacks 0AIS are carried as hypotheses; see the section "What is assumed" of this file.

theorem isFormalAlgebraicSpace_completionSheaf
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (T : Set (Space.points B S hS X))
    {Ix : Type (u + 1)} {A : Ix → Type u} [∀ i, CommRing (A i)]
    (hA : ∀ i, B.Contains (AlgebraicGeometry.Spec (.of (A i))))
    (str : ∀ i, AlgebraicGeometry.Spec (.of (A i)) ⟶ S)
    (a : ∀ i, yoneda.obj (affineOver B S hS (hA i) (str i)) ⟶ X)
    (ha : ∀ i, ∃ hai : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
        (Space.sheafifiedULiftMap B S hS (a i)).hom,
      Space.HasPropertyULift.{u + 1} B S hS
        (fun _ _ q ↦ Space.IsEtaleULift.{u + 1} B S hS q.hom)
        (Space.sheafifiedULiftMap B S hS (a i)).hom hai)
    (hcov : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
          Sheaf.instHasColimitsOfSize
        Sheaf.IsLocallySurjective
          (Sigma.desc fun i ↦ Space.sheafifiedULiftMap B S hS (a i)))
    (Ti : ∀ i, Set ((BigFppfOver.toScheme B S hS).obj (affineOver B S hS (hA i) (str i))))
    (hTi : ∀ i, IsClosed (Ti i))
    (hTpts : ∀ i, Space.pointsMap B S hS _ (a i) ⁻¹' T =
      supportedPoints B S hS (affineOver B S hS (hA i) (str i)) (Ti i))
    (hstage : ∀ i, HasStageAtlas B S hS (hA i) (str i)
      (PrimeSpectrum.vanishingIdeal (Ti i)))
    (hset : SatisfiesSetTheoreticCondition B S hS (Space.completionSheaf B S hS X T)) :
    IsFormalAlgebraicSpace B S hS (Space.completionSheaf B S hS X T)

AlgebraicGeometry.FormalSpace.isIso_toSheafify_completionSubfunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSetTheoretic.lean, line 374. The attribute's comment: “the functor”.

Let X be an algebraic space over S and T a set of points of X. The functor sending an object U of the big fppf site of S to the morphisms f : U ⟶ X with f(|U|) ⊆ T is an fppf sheaf: the map to its sheafification, the completion X_{/T} of AlgebraicGeometry.Space.completionSheaf, is an isomorphism.

theorem isIso_toSheafify_completionSubfunctor
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (T : Set (Space.points B S hS X)) :
    IsIso (toSheafify (BigFppfOver.topology B S hS)
      (Space.completionSubfunctor B S hS X T).toFunctor)
Tag 0AMC, a definition

Tag 0AMC in the Stacks Project.

AlgebraicGeometry.Space.completionSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Completion.lean, line 125. The attribute's comment: “the completion along a closed subset; 0AIZ, formal algebraic space, not proved”.

Stacks 0AMC. The completion X_{/T} of X along T: the fppf sheafification of the subfunctor of sections with point-set image in T.

For X an algebraic space over S and T ⊆ |X| closed this is the object Stacks 0AMC names the completion of X along T, namely the formal algebraic space of Stacks 0AIZ: the fppf sheafification of the functor sending U to the morphisms f : U ⟶ X with f(|U|) ⊆ T. Stacks 0AIZ, that it is a formal algebraic space, is not proved in this library; the object named here is the sheaf itself, defined for an arbitrary presheaf X and an arbitrary set T of its points. The affine case of 0AIZ is AlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_completionSheaf (Stacks 0AIY).

def completionSheaf (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (T : Set (points B S hS X)) :
    Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))
Tag 0APV, a lemma

Tag 0APV in the Stacks Project.

AlgebraicGeometry.Space.isPullback_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Completion.lean, line 231. The attribute's comment: “cartesian square”.

Stacks 0APV. Completion is compatible with base change: for a morphism f : X' ⟶ X of presheaves on the big fppf site of S and a set T of points of X, the square formed by the completion of X' along |f|⁻¹ T, the completion of X along T and the two ambient sheaves is a cartesian square of fppf sheaves.

theorem isPullback_completionSheafMap
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X' ⟶ X)
    (T : Set (points B S hS X)) :
    IsPullback
      (completionSheafInclusion B S hS X' (pointsMap B S hS X' f ⁻¹' T))
      (completionSheafMap B S hS f T)
      (sheafifiedULiftMap B S hS f)
      (completionSheafInclusion B S hS X T)

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

Stacks 0APV. For a morphism f : X' ⟶ X of algebraic spaces over S and a set T of points of X, the induced morphism of completions X'_{/|f|⁻¹ T} ⟶ X_{/T} is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpacesULift_completionMap
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (f : X' ⟶ X) (T : Set (points B S hS X)) :
    IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
      (completionSheafMap B S hS f T).hom
Tag 0GB9, a lemma

Tag 0GB9 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isReduction_completionSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionAlongClosedSubsetReduction.lean, line 379.

Stacks 0GB9. Let X be an algebraic space over S and let T ⊆ |X| be a closed subset. The reduction of the completion X_{/T} of X along T is the reduced induced closed subspace Z of X supported on T: the canonical morphism Z ⟶ X_{/T} exhibits Z as the reduction of X_{/T}.

theorem isReduction_completionSheaf :
    IsReduction B S hS (Space.completionSheaf B S hS X T)
      (reducedClosedSubsetSheaf B S hS hX T hT)
      (reducedClosedSubsetToCompletionSheaf B S hS hX T hT)
Tag 0GBA, a lemma

Tag 0GBA in the Stacks Project.

AlgebraicGeometry.FormalSpace.isAdicStar_completionSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineCompletionTypes.lean, line 430. The attribute's comment: “adic*”.

Stacks 0GBA (1). Let X = Spec A be an affine scheme over S in the big fppf site and let T ⊆ |X| be a closed subset whose complement is quasi-compact, that is a constructible closed subset. Then the completion X_{/T} is an adic* affine formal algebraic space.

theorem isAdicStar_completionSheaf
    (T : Set (Space.points B S hS (yoneda.obj (affineOver B S hS hA f))))
    (hT : @IsClosed _
      (Space.pointTopology B S hS (yoneda.obj (affineOver B S hS hA f))) T)
    (hqc : @IsCompact _
      (Space.pointTopology B S hS (yoneda.obj (affineOver B S hS hA f))) Tᶜ) :
    IsAdicStar B S hS
      (Space.completionSheaf B S hS (yoneda.obj (affineOver B S hS hA f)) T)

AlgebraicGeometry.FormalSpace.isNoetherian_completionSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineCompletionTypes.lean, line 447. The attribute's comment: “Noetherian”.

Stacks 0GBA (3). Let X = Spec A be a Noetherian affine scheme over S in the big fppf site and let T ⊆ |X| be a closed subset. Then the completion X_{/T} is a Noetherian affine formal algebraic space.

theorem isNoetherian_completionSheaf [IsNoetherianRing A]
    (T : Set (Space.points B S hS (yoneda.obj (affineOver B S hS hA f))))
    (hT : @IsClosed _
      (Space.pointTopology B S hS (yoneda.obj (affineOver B S hS hA f))) T) :
    IsNoetherian B S hS
      (Space.completionSheaf B S hS (yoneda.obj (affineOver B S hS hA f)) T)

AlgebraicGeometry.FormalSpace.isIso_completionComparison_adicQuotientSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineRigEtaleAlgebraization.lean, line 167. The attribute's comment: “formal spectrum, for the constructed quotient-system presentation AlgebraicGeometry.FormalSpace.adicQuotientSystem of the completion”.

Let X = Spec A be an affine scheme over S in the big fppf site and let T = V(I) for a finitely generated ideal I ⊆ A. Then the canonical comparison Spf (A^∧) ⟶ X_{/T} is an isomorphism, for the presentation adicQuotientSystem of the I-adic completion A^∧.

theorem isIso_completionComparison_adicQuotientSystem (hA : B.Contains (Spec (.of A)))
    (f : Spec (.of A) ⟶ S) (I : Ideal A) (hI : I.FG) :
    IsIso (completionComparison B S hS hA f I (adicQuotientSystem B S hS hA f I hI)
      (quotientSystemCompatible_adicQuotientSystem B S hS hA f I hI))

AlgebraicGeometry.FormalSpace.isIso_completionComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFormalSpectrum.lean, line 936. The attribute's comment: “formal spectrum”. 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 0GBA (2). Let X = Spec A be an affine scheme over S in the big fppf site and let T = V(I) be the zero locus of a finitely generated ideal I ⊆ A. Then the canonical comparison from the formal spectrum of the I-adic completion of A to the completion of X along T is an isomorphism, so X_{/T} = Spf (A^∧).

theorem isIso_completionComparison
    (hI : I.FG)
    (D : AdicQuotientSystem B S hS I)
    (hD : QuotientSystemCompatible B S hS f I D) :
    IsIso (completionComparison B S hS hA f I D hD)
Tag 0APW, a lemma

Tag 0APW in the Stacks Project.

AlgebraicGeometry.FormalSpace.isAdicStar_countableCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedAdicStar.lean, line 1219. The attribute's comment: “clause (1): a countably indexed completion whose closed set is cut out by countably many equations is adic star”.

Stacks 0APW (1). Let T ⊆ Spec A be a closed set cut out by countably many equations e : ℕ → A, and suppose the completion X_{/T} of X = Spec A along T is countably indexed, in the sense that some decreasing sequence J of ideals cutting out T is cofinal among all ideals cutting out T. Then X_{/T}, which is the colimit of the quotient spectra Spec (A ⧸ J n), is adic*. The presenting ring is the inverse limit lim A ⧸ J' n along a square-cofinal reindexing J' = J ∘ idx of J; passing to that subsequence does not change the colimit, since the reindexing functor is final.

theorem isAdicStar_countableCompletion (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (f : Spec (.of A) ⟶ S) (hA : B.Contains (Spec (.of A)))
    {T : Set (PrimeSpectrum A)} (J : ℕ → Ideal A) (hJ : IsCofinalVanishingSequence A T J)
    (e : ℕ → A) (heT : T = PrimeSpectrum.zeroLocus (Set.range e)) :
    IsAdicStar B S hS (countableCompletion B S hS f hA J hJ.1)

AlgebraicGeometry.FormalSpace.gabberCompletion_no_fg_isWeakIdealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedNotAdicStarExample.lean, line 695. The attribute's comment: “clause (2), the example is not adic*, at the level of the ring; the sheaf-level form of clause (2) is AlgebraicGeometry.FormalSpace.isCountablyIndexed_not_isAdicStar_gabberCompletionSheaf”.

Stacks 0APW (2). The completion lim A ⧸ J_n of Gabber's ring has no finitely generated weak ideal of definition, hence no finitely generated ideal of definition: it is not adic with a finitely generated ideal of definition.

theorem gabberCompletion_no_fg_isWeakIdealOfDefinition.{v} :
    ¬ ∃ I : Ideal GabberCompletion.{v},
      I.FG ∧ TopologicalRing.IsWeakIdealOfDefinition I

AlgebraicGeometry.FormalSpace.isCofinalVanishingSequence_gabberPowerIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedNotAdicStarExample.lean, line 729. The attribute's comment: “clause (2), the example is countably indexed, as cofinality of the ideal sequence; the sheaf-level form of clause (2) is AlgebraicGeometry.FormalSpace.isCountablyIndexed_not_isAdicStar_gabberCompletionSheaf”.

Stacks 0APW (2). The ideals J_n = (x_α^(n+1)) decrease, all cut out T = V(x_α : α ∈ ω₁), and are cofinal among the ideals cutting out T; so the completion of Spec A along T is countably indexed.

theorem isCofinalVanishingSequence_gabberPowerIdeal.{v} :
    IsCofinalVanishingSequence GabberRing.{v}
      (PrimeSpectrum.zeroLocus (gabberVanishingIdeal.{v} : Set GabberRing.{v}))
      gabberPowerIdeal.{v}

AlgebraicGeometry.FormalSpace.isCountablyIndexed_not_isAdicStar_gabberCompletionSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedNotAdicStarSheaf.lean, line 168. The attribute's comment: “clause (2) at sheaf level: Gabber's completion is countably indexed and is not adic star”.

Stacks 0APW (2). Gabber's completion is a countably indexed affine formal algebraic space which is not adic*: so the hypothesis of clause (1) that the closed set be cut out by countably many functions cannot be dropped.

Both halves are the ring-theoretic ones of StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedNotAdicStarExample.lean read at sheaf level. Countable indexedness is the cofinality of the sequence J_n, through Stacks 0AN1. For the failure of adic*-ness, every topological ring presenting the completion is isomorphic to lim A ⧸ J_n by the uniqueness of the associated ring of Stacks 0AIC, so a finitely generated ideal of definition of any of them would give one of lim A ⧸ J_n, and hence a finitely generated weak ideal of definition, which that ring has none of.

theorem isCountablyIndexed_not_isAdicStar_gabberCompletionSheaf (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) (f : Spec (.of GabberRing.{u}) ⟶ S)
    (hA : B.Contains (Spec (.of GabberRing.{u}))) :
    IsCountablyIndexed B S hS (gabberCompletionSheaf B S hS f hA) ∧
      ¬ IsAdicStar B S hS (gabberCompletionSheaf B S hS f hA)
Sources
LeanAlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_completionSheaf · AlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_completionSheaf_of_isClosed · AlgebraicGeometry.FormalSpace.isIso_toSheafify_completionSubfunctor_affineOver · AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_completionSheaf_of_isClosed · AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_completionSheaf · AlgebraicGeometry.FormalSpace.isIso_toSheafify_completionSubfunctor · AlgebraicGeometry.Space.completionSheaf · AlgebraicGeometry.Space.isPullback_completionSheafMap

Section87.15 Fibre products#

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

Tag 0AJ1, a lemma

Tag 0AJ1 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_etaleCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleCover.lean, line 237.

Stacks 0AJ1. A jointly surjective family of representable étale maps from formal algebraic spaces makes its target a formal algebraic space, provided the target satisfies the set-theoretic condition of Stacks 0AIS.

theorem isFormalAlgebraicSpace_of_etaleCover {I : Type (u + 1)}
    (X : FppfSheaf B S hS) (Xi : I → FppfSheaf B S hS) (f : ∀ i, Xi i ⟶ X)
    (hXi : ∀ i, IsFormalAlgebraicSpace B S hS (Xi i))
    (hf : ∀ i, ∃ hfi : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (f i).hom,
      Space.HasPropertyULift.{u + 1} B S hS
        (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) (f i).hom hfi)
    (hsurj : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
        Sheaf.instHasColimitsOfSize
      Sheaf.IsLocallySurjective (Sigma.desc f))
    (hXset : SatisfiesSetTheoreticCondition B S hS X) :
    IsFormalAlgebraicSpace B S hS X

AlgebraicGeometry.FormalSpace.not_forall_isFormalAlgebraicSpace_of_etaleCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleCoverCounterexample.lean, line 261. The attribute's comment: “the statement as printed is false: over any nonempty S, the sheaf of locally constant functions to a discrete set as large as the size cutoff of the site, with the family of its constant sections out of h_S, satisfies (a)-(c) but fails the set-theoretic condition of Stacks 0AIS; the corrected form is AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_etaleCover_of_admitsCoproductIndex”.

Stacks 0AJ1 is false without a bound on the index. Over a nonempty scheme S of a big fppf site, it is not the case that every fppf sheaf X with a family {Xᵢ ⟶ X} satisfying conditions (a), (b) and (c) of Stacks 0AJ1 is a formal algebraic space: the sheaf of locally constant functions with values in a discrete set as large as the cutoff of the site, with its family of constant functions out of h_S, satisfies (a)–(c) but not the set-theoretic condition of Stacks 0AIS that Definition 0AIM asks of a formal algebraic space.

theorem not_forall_isFormalAlgebraicSpace_of_etaleCover [Nonempty S] :
    letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) := Sheaf.instHasColimitsOfSize
    ¬ ∀ (I : Type (u + 1)) (X : FppfSheaf B S hS) (Xi : I → FppfSheaf B S hS)
      (f : ∀ i, Xi i ⟶ X),
      (∀ i, IsFormalAlgebraicSpace B S hS (Xi i)) →
      (∀ i, ∃ hfi : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (f i).hom,
        Space.HasPropertyULift.{u + 1} B S hS
          (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) (f i).hom hfi) →
      Sheaf.IsLocallySurjective (Sigma.desc f) →
      IsFormalAlgebraicSpace B S hS X

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_etaleCover_of_admitsCoproductIndex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleCoverSetCondition.lean, line 318. 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 target then failing the set-theoretic condition of Stacks 0AIS that Definition 0AIM asks of a formal algebraic space (AlgebraicGeometry.FormalSpace.not_forall_isFormalAlgebraicSpace_of_etaleCover); stated, under the source's hypotheses (a)-(c), for an index admissible for coproducts in the site, the proviso 'I not too large' of Stacks 0AIS observation (3), and with that condition derived, not assumed”.

Stacks 0AJ1, for an index which is not too large. Let {Xᵢ ⟶ X}_{i ∈ I} be a family of maps of fppf sheaves on the big fppf site of S, indexed by a type admissible for coproducts in the site (of cardinality below the cofinality of its size cutoff; for instance a countable one), such that (a) each Xᵢ is a formal algebraic space over S, (b) each Xᵢ ⟶ X is representable by algebraic spaces and étale, and (c) ∐ Xᵢ ⟶ X is a surjection of sheaves. Then X is a formal algebraic space over S.

The atlas is the source's: the atlases of the Xᵢ composed with the maps Xᵢ ⟶ X (AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_etaleCover). The set-theoretic condition of Stacks 0AIS, which Definition 0AIM asks of X as well, is not assumed: it is derived from (a)–(c) by AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_of_etaleCover, which is where the size of the index enters, as observation (3) of Remark 0AIS says it must. Without a bound on the index the statement is false (AlgebraicGeometry.FormalSpace.not_forall_isFormalAlgebraicSpace_of_etaleCover).

theorem isFormalAlgebraicSpace_of_etaleCover_of_admitsCoproductIndex
    {I : Type (u + 1)} [Small.{u} I] [B.AdmitsCoproductIndex I]
    (X : FppfSheaf B S hS) (Xi : I → FppfSheaf B S hS) (f : ∀ i, Xi i ⟶ X)
    (hXi : ∀ i, IsFormalAlgebraicSpace B S hS (Xi i))
    (hf : ∀ i, ∃ hfi : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (f i).hom,
      Space.HasPropertyULift.{u + 1} B S hS
        (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) (f i).hom hfi)
    (hsurj : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
        Sheaf.instHasColimitsOfSize
      Sheaf.IsLocallySurjective (Sigma.desc f)) :
    IsFormalAlgebraicSpace B S hS X
Tag 0AJ2, a lemma

Tag 0AJ2 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_pullback_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FibreProduct.lean, line 189. The attribute's comment: “the case of a base separated in the sense of clause (2) of Stacks 0AJ6, where Stacks 0AN3 clause (1) makes every fibre product of two affine formal algebraic spaces over the base an affine formal algebraic space, in place of the directed colimit argument of Stacks 0AIU that the general case needs”.

Stacks 0AJ2 for a base which is separated in the sense of clause (2) of Stacks 0AJ6. The fibre product of two formal algebraic spaces over such a base, whose relative products of representables are representable, is a formal algebraic space.

Separatedness enters only through Stacks 0AN3 clause (1): it makes the fibre product of two affine formal algebraic spaces over Z again an affine formal algebraic space, which is the hypothesis hstage of isFormalAlgebraicSpace_pullback_of_affineStages. The set-theoretic condition of Stacks 0AIS on X ×_Z Y and on the intermediate fibre products follows from hZrep alone, by satisfiesSetTheoreticCondition_pullback_of_hasRepresentableRelativeProducts over Z and, after the pasting isomorphism, over Z again.

theorem isFormalAlgebraicSpace_pullback_of_isSeparated
    {X Y Z : FppfSheaf B S hS} (p : X ⟶ Z) (q : Y ⟶ Z)
    (hZrep : HasRepresentableRelativeProducts B S hS Z)
    (hZsep : IsSeparated B S hS Z)
    (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) :
    IsFormalAlgebraicSpace B S hS (pullback p q)

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_pullback_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FibreProduct.lean, line 219. The attribute's comment: “the case of two affine formal algebraic spaces over a base separated in the sense of clause (2) of Stacks 0AJ6, where Stacks 0AN3 clause (1) makes the fibre product of the two an affine formal algebraic space”.

Stacks 0AJ2 for a separated base, on two affine formal algebraic spaces: an affine formal algebraic space is a formal algebraic space, so this is a special case of isFormalAlgebraicSpace_pullback_of_isSeparated.

theorem isFormalAlgebraicSpace_pullback_of_isAffineFormal
    {X Y Z : FppfSheaf B S hS} (p : X ⟶ Z) (q : Y ⟶ Z)
    (hZrep : HasRepresentableRelativeProducts B S hS Z)
    (hZsep : IsSeparated B S hS Z)
    (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y) :
    IsFormalAlgebraicSpace B S hS (pullback p q)

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_pullback_of_representableDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FibreProductRepresentableDiagonal.lean, line 211.

Stacks 0AJ2. Let S be a scheme, let X and Y be formal algebraic spaces over S and let Z be a sheaf on (Sch/S)_fppf whose diagonal is representable by algebraic spaces. For maps of sheaves p : X ⟶ Z and q : Y ⟶ Z, the fibre product X ×_Z Y is a formal algebraic space.

theorem isFormalAlgebraicSpace_pullback_of_representableDiagonal
    {X Y Z : FppfSheaf B S hS} (p : X ⟶ Z) (q : Y ⟶ Z)
    (hZ : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (diag Z.obj))
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y) :
    IsFormalAlgebraicSpace B S hS (pullback p q)
Tag 0AJ3, a lemma

Tag 0AJ3 in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasPullbacks_formalAlgebraicSpaces, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FibreProductFormalBase.lean, line 292.

Stacks 0AJ3. The category of formal algebraic spaces over a scheme S has fibre products.

The fibre product is the fibre product of the underlying fppf sheaves: that is again a formal algebraic space by AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_pullback_of_isFormalAlgebraicSpace, so the full inclusion into fppf sheaves creates fibre products and the subcategory inherits them.

instance hasPullbacks_formalAlgebraicSpaces : HasPullbacks (FormalAlgebraicSpaces B S hS)
Tag 0CB9, a lemma

Tag 0CB9 in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_iso_reduction_fibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FibreProductReduction.lean, line 150. The attribute's comment: “with reductions of the five spaces, and both fibre products, as hypotheses”.

Stacks 0CB9. Let X ⟶ Z and Y ⟶ Z be morphisms of formal algebraic spaces over S, let iX : Xred ⟶ X, iY : Yred ⟶ Y and iZ : Zred ⟶ Z be reductions and let Xred ⟶ Zred and Yred ⟶ Zred be compatible with the two given morphisms. Let P be a fibre product of X and Y over Z, let Q be a fibre product of Xred and Yred over Zred, and let iP : Pred ⟶ P and iQ : Qred ⟶ Q be reductions of those two fibre products. Then the inclusions of the reductions induce a morphism Q ⟶ P over which Qred and Pred are isomorphic: (X ×_Z Y)_red = (X_red ×_{Z_red} Y_red)_red.

theorem exists_iso_reduction_fibreProduct
    (_hX : IsFormalAlgebraicSpace B S hS X) (_hY : IsFormalAlgebraicSpace B S hS Y)
    (_hZ : IsFormalAlgebraicSpace B S hS Z)
    (hiX : IsReduction B S hS X Xred iX) (hiY : IsReduction B S hS Y Yred iY)
    (hiZ : IsReduction B S hS Z Zred iZ)
    (hfred : fred ≫ iZ = iX ≫ f) (hgred : gred ≫ iZ = iY ≫ g)
    (hP : IsPullback p₁ p₂ f g) (hQ : IsPullback q₁ q₂ fred gred)
    (hiP : IsReduction B S hS P Pred iP) (hiQ : IsReduction B S hS Q Qred iQ) :
    ∃ (cmp : Q ⟶ P) (e : Qred ≅ Pred),
      cmp ≫ p₁ = q₁ ≫ iX ∧ cmp ≫ p₂ = q₂ ≫ iY ∧ e.hom ≫ iP = iQ ≫ cmp
Tag 0AN2, a lemma

Tag 0AN2 in the Stacks Project.

AlgebraicGeometry.FormalSpace.relativelyRepresentable_pullback_diagonal_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/DiagonalRepresentable.lean, line 1039. The attribute's comment: “representable by schemes, for a morphism whose source is an arbitrary formal algebraic space”.

Stacks 0AN2, representability, for a morphism whose source is an arbitrary formal algebraic space: the relative diagonal of a morphism of fppf sheaves out of a formal algebraic space is representable by objects of the big fppf site of S.

This discharges the hypothesis of AlgebraicGeometry.FormalSpace.relativelyRepresentable_pullback_diagonal, the relative diagonal being a base change of the absolute one.

theorem relativelyRepresentable_pullback_diagonal_of_isFormalAlgebraicSpace
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hX : IsFormalAlgebraicSpace B S hS X) :
    (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (pullback.diagonal f)

AlgebraicGeometry.FormalSpace.relative_locallyOfFiniteType_pullback_diagonal_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/DiagonalRepresentable.lean, line 1227. The attribute's comment: “locally of finite type, for a morphism whose source is an arbitrary formal algebraic space”.

Stacks 0AN2, local finite type, for a morphism whose source is an arbitrary formal algebraic space: every represented base change of the relative diagonal of a morphism of fppf sheaves out of a formal algebraic space is a locally of finite type morphism of schemes.

This discharges the hypothesis of AlgebraicGeometry.FormalSpace.relative_pullback_diagonal for local finite type, the relative diagonal being a base change of the absolute one.

theorem relative_locallyOfFiniteType_pullback_diagonal_of_isFormalAlgebraicSpace
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hX : IsFormalAlgebraicSpace B S hS X) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (pullback.diagonal f)

AlgebraicGeometry.FormalSpace.relative_locallyQuasiFinite_pullback_diagonal_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/DiagonalRepresentable.lean, line 1241. The attribute's comment: “locally quasi-finite, for a morphism whose source is an arbitrary formal algebraic space”.

Stacks 0AN2, local quasi-finiteness, for a morphism whose source is an arbitrary formal algebraic space: every represented base change of the relative diagonal is a locally quasi-finite, locally of finite type morphism of schemes.

theorem relative_locallyQuasiFinite_pullback_diagonal_of_isFormalAlgebraicSpace
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hX : IsFormalAlgebraicSpace B S hS X) :
    (MorphismProperty.inverseImage
      ((@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) ⊓
        (@AlgebraicGeometry.LocallyQuasiFinite.{u} : MorphismProperty Scheme.{u}))
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (pullback.diagonal f)

AlgebraicGeometry.FormalSpace.relative_isSeparated_pullback_diagonal_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/DiagonalRepresentable.lean, line 1255. The attribute's comment: “separated, for a morphism whose source is an arbitrary formal algebraic space”.

Stacks 0AN2, separatedness, for a morphism whose source is an arbitrary formal algebraic space: every represented base change of the relative diagonal is a separated morphism of schemes.

theorem relative_isSeparated_pullback_diagonal_of_isFormalAlgebraicSpace
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hX : IsFormalAlgebraicSpace B S hS X) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.IsSeparated.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (pullback.diagonal f)

AlgebraicGeometry.FormalSpace.relativelyRepresentable_pullback_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RelativeDiagonal.lean, line 114. The attribute's comment: “representability, by base change from the representability assertion of Stacks 0AIP for the absolute diagonal of the source, which is available for an arbitrary formal algebraic space in StacksFrontier.AlgebraicGeometry.FormalSpace.DiagonalRepresentable, where this reduction is fed it”.

If the absolute diagonal of an fppf sheaf X on the big fppf site of S is representable by objects of the site, then so is the relative diagonal of every morphism out of X.

theorem relativelyRepresentable_pullback_diagonal {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (diag X)) :
    (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (pullback.diagonal f)

AlgebraicGeometry.FormalSpace.relative_pullback_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RelativeDiagonal.lean, line 132. The attribute's comment: “the locally quasi-finite, locally of finite type and separated assertions at once, by base change from the corresponding assertion of Stacks 0AIP for the absolute diagonal of the source, taken uniformly in the property of morphisms of the site; all three are available for an arbitrary formal algebraic space in StacksFrontier.AlgebraicGeometry.FormalSpace.DiagonalRepresentable, where this reduction is fed them”.

If every represented base change of the absolute diagonal of an fppf sheaf X on the big fppf site of S is a morphism of the site with Q, then the same holds for the relative diagonal of every morphism out of X.

theorem relative_pullback_diagonal (Q : MorphismProperty (BigFppfOver B S hS))
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : Q.relative (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (diag X)) :
    Q.relative (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (pullback.diagonal f)

AlgebraicGeometry.FormalSpace.relativelyRepresentable_pullback_diagonal_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RelativeDiagonal.lean, line 266. The attribute's comment: “representable by schemes, for a morphism whose source is an affine formal algebraic space”.

The relative diagonal of a morphism out of an affine formal algebraic space is representable by objects of the site.

theorem relativelyRepresentable_pullback_diagonal_of_isAffineFormal
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (pullback.diagonal f)

AlgebraicGeometry.FormalSpace.relative_locallyQuasiFinite_pullback_diagonal_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RelativeDiagonal.lean, line 276. The attribute's comment: “locally quasi-finite, for a morphism whose source is an affine formal algebraic space”.

Every represented base change of the relative diagonal of a morphism out of an affine formal algebraic space is a locally quasi-finite, locally of finite type morphism of schemes.

theorem relative_locallyQuasiFinite_pullback_diagonal_of_isAffineFormal
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    (MorphismProperty.inverseImage
      ((@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) ⊓
        (@AlgebraicGeometry.LocallyQuasiFinite.{u} : MorphismProperty Scheme.{u}))
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (pullback.diagonal f)

AlgebraicGeometry.FormalSpace.relative_locallyOfFiniteType_pullback_diagonal_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RelativeDiagonal.lean, line 292. The attribute's comment: “locally of finite type, for a morphism whose source is an affine formal algebraic space”.

Every represented base change of the relative diagonal of a morphism out of an affine formal algebraic space is a locally of finite type morphism of schemes.

theorem relative_locallyOfFiniteType_pullback_diagonal_of_isAffineFormal
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (pullback.diagonal f)

AlgebraicGeometry.FormalSpace.relative_isSeparated_pullback_diagonal_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RelativeDiagonal.lean, line 305. The attribute's comment: “separated, for a morphism whose source is an affine formal algebraic space”.

Every represented base change of the relative diagonal of a morphism out of an affine formal algebraic space is a separated morphism of schemes.

theorem relative_isSeparated_pullback_diagonal_of_isAffineFormal
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.IsSeparated.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (pullback.diagonal f)

AlgebraicGeometry.FormalSpace.mono_pullback_diagonal_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RelativeDiagonal.lean, line 320. The attribute's comment: “monomorphism, for a morphism whose source is an arbitrary formal algebraic space”.

The relative diagonal of a morphism of fppf sheaves out of a formal algebraic space is a monomorphism, which by Stacks 0AQB is the monomorphism condition for a morphism of formal algebraic spaces.

theorem mono_pullback_diagonal_of_isFormalAlgebraicSpace {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (_hX : IsFormalAlgebraicSpace B S hS X) : Mono (pullback.diagonal f)

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_etaleCover · AlgebraicGeometry.FormalSpace.not_forall_isFormalAlgebraicSpace_of_etaleCover · AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_etaleCover_of_admitsCoproductIndex · AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_pullback_of_isSeparated · AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_pullback_of_isAffineFormal · AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_pullback_of_representableDiagonal · AlgebraicGeometry.FormalSpace.hasPullbacks_formalAlgebraicSpaces · AlgebraicGeometry.FormalSpace.exists_iso_reduction_fibreProduct

Section87.16 Separation axioms for formal algebraic spaces#

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

Tag 0AJ5, a lemma

Tag 0AJ5 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isAbsolutelyQuasiSeparated_reduction_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ReductionQuasiSeparated.lean, line 281. The attribute's comment: “the reduction of X is a given, in the sense of AlgebraicGeometry.FormalSpace.IsReduction and supplied by Stacks 0AIN, and is presented by a presheaf of Type u together with an isomorphism from its universe lift, since an algebraic space over S is a presheaf of Type u while a formal algebraic space is a sheaf of Type (u + 1); clauses (2) and (3) quantify over the objects of the site representing the fibre product, as the carriers of Stacks 0AHR do for the identical clauses, rather than asserting that it is representable, which is Stacks 0AIP”.

Stacks 0AJ5. Let X be a formal algebraic space over S and let i : X_red ⟶ X be a reduction of X, presented by a presheaf Xred of Type u together with an isomorphism from its universe lift. The following are equivalent: Xred is a quasi-separated algebraic space; for every pair of objects of the big fppf site of S with quasi-compact underlying scheme and every pair of morphisms from their universe-lifted Yoneda presheaves into X, every object of the site representing the fibre product has quasi-compact underlying scheme; and the same for every pair of objects with affine underlying scheme.

Condition (1) is equivalent to the intersection condition for Xred, with quasi-compact or with affine test objects, by Stacks 0AHR. The intersection condition for X implies the one for Xred because the inclusion of a reduction is a monomorphism, and conversely it follows from the one for Xred by the thickening comparison of AlgebraicGeometry.FormalSpace.hasQuasiCompactIntersectionsULift_of_isReduction.

theorem isAbsolutelyQuasiSeparated_reduction_tfae
    {X Xr : FppfSheaf B S hS} (_hX : IsFormalAlgebraicSpace B S hS X)
    {i : Xr ⟶ X} (hi : IsReduction B S hS X Xr i)
    {Xred : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (e : Xred ⋙ uliftFunctor.{u + 1} ≅ Xr.obj) :
    List.TFAE
      [ Space.IsAbsolutelyQuasiSeparated B S hS hZ Xred,
        HasQuasiCompactIntersectionsULift B S hS
          (fun Z : Scheme.{u} ↦ CompactSpace (Z : Type u)) X.obj,
        HasQuasiCompactIntersectionsULift B S hS (fun Z : Scheme.{u} ↦ IsAffine Z) X.obj ]

AlgebraicGeometry.FormalSpace.isAbsolutelyQuasiSeparated_reduction_tfae_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparationAxiomsRepresentable.lean, line 255. The attribute's comment: “with clauses (2) and (3) in the source's own form, asserting that the fibre product U ×_X V is representable by an object of the site with quasi-compact underlying scheme; read against a reduction of X, in the sense of AlgebraicGeometry.FormalSpace.IsReduction and supplied by Stacks 0AIN, presented by a presheaf of Type u together with an isomorphism from its universe lift”.

Stacks 0AJ5, with clauses (2) and (3) asserting representability. Let X be a formal algebraic space over S and let i : X_red ⟶ X be a reduction of X, presented by a presheaf Xred of Type u together with an isomorphism from its universe lift. The following are equivalent: Xred is a quasi-separated algebraic space; for every pair of objects of the big fppf site of S with quasi-compact underlying scheme and every pair of morphisms from their universe-lifted Yoneda presheaves into X, the fibre product is represented by an object of the site with quasi-compact underlying scheme; and the same for every pair of objects with affine underlying scheme.

This is AlgebraicGeometry.FormalSpace.isAbsolutelyQuasiSeparated_reduction_tfae together with AlgebraicGeometry.FormalSpace.hasRepresentableQuasiCompactIntersectionsULift_iff.

theorem isAbsolutelyQuasiSeparated_reduction_tfae_representable
    {X Xr : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X)
    {i : Xr ⟶ X} (hi : IsReduction B S hS X Xr i)
    {Xred : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (e : Xred ⋙ uliftFunctor.{u + 1} ≅ Xr.obj) :
    List.TFAE
      [ Space.IsAbsolutelyQuasiSeparated B S hS hZ Xred,
        HasRepresentableQuasiCompactIntersectionsULift B S hS
          (fun Z : Scheme.{u} ↦ CompactSpace (Z : Type u)) X.obj,
        HasRepresentableQuasiCompactIntersectionsULift B S hS
          (fun Z : Scheme.{u} ↦ IsAffine Z) X.obj ]
Tag 0AJ6, a lemma

Tag 0AJ6 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isAbsolutelySeparated_reduction_of_hasAffineIntersectionsULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ReductionSeparated.lean, line 255. The attribute's comment: “(2) implies (1): the affine-intersection and surjectivity condition for X gives that the reduction of X is a separated algebraic space. The reduction is a given, in the sense of AlgebraicGeometry.FormalSpace.IsReduction and supplied by Stacks 0AIN, and is presented by a presheaf of Type u together with an isomorphism from its universe lift, since an algebraic space over S is a presheaf of Type u while a formal algebraic space is a sheaf of Type (u + 1). Clause (2) quantifies over the objects of the site representing the fibre product, as the carrier of Stacks 0AHS does for the identical clause, rather than asserting that it is representable, which is Stacks 0AIP. The converse implication (1) implies (2), the equivalence read against an arbitrary reduction, and the tag itself, whose reduction is produced from Stacks 0AIN, are AlgebraicGeometry.FormalSpace.hasAffineIntersectionsULift_of_isReduction, AlgebraicGeometry.FormalSpace.isAbsolutelySeparated_reduction_iff_hasAffineIntersectionsULift and AlgebraicGeometry.FormalSpace.exists_isReduction_and_isAbsolutelySeparated_iff_hasAffineIntersectionsULift in StacksFrontier.AlgebraicGeometry.FormalSpace.ReductionSeparatedConverse”. References: EGA I (10.15.7), “partial”.

Stacks 0AJ6, the implication (2) ⟹ (1). Let X be a formal algebraic space over S and let i : X_red ⟶ X be a reduction of X, presented by a presheaf Xred of Type u together with an isomorphism from its universe lift. If for every pair of objects of the big fppf site of S with affine underlying scheme and every pair of morphisms from their universe-lifted Yoneda presheaves into X every object of the site representing the fibre product has affine underlying scheme and the canonical map from the tensor product over ℤ of the two rings of global sections to its ring of global sections is surjective, then Xred is a separated algebraic space.

The inclusion of a reduction is a monomorphism, so a cartesian square exhibiting a fibre product over Xred also exhibits it over X; the condition therefore restricts from X to Xred, where it is separatedness by Stacks 0AHS.

theorem isAbsolutelySeparated_reduction_of_hasAffineIntersectionsULift
    {X Xr : FppfSheaf B S hS} (_hX : IsFormalAlgebraicSpace B S hS X)
    {i : Xr ⟶ X} (hi : IsReduction B S hS X Xr i)
    {Xred : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (e : Xred ⋙ uliftFunctor.{u + 1} ≅ Xr.obj)
    (h : HasAffineIntersectionsULift B S hS X.obj) :
    Space.IsAbsolutelySeparated B S hS hZ Xred

AlgebraicGeometry.FormalSpace.isAbsolutelySeparated_reduction_iff_hasAffineIntersectionsULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ReductionSeparatedConverse.lean, line 416. The attribute's comment: “both implications, read against a reduction of X, in the sense of AlgebraicGeometry.FormalSpace.IsReduction, and a presentation of it by a presheaf of Type u together with an isomorphism from its universe lift -- an algebraic space over S being a presheaf of Type u while a formal algebraic space is a sheaf of Type (u + 1). Clause (2) quantifies over the objects of the site representing the fibre product, as the carrier of Stacks 0AHS does for the identical clause, rather than asserting that it is representable, which is Stacks 0AIP. The tag itself, which produces the reduction and its presentation, is AlgebraicGeometry.FormalSpace.exists_isReduction_and_isAbsolutelySeparated_iff_hasAffineIntersectionsULift”. References: EGA I (10.15.7), “more general”.

Stacks 0AJ6. Let X be a formal algebraic space over S and let i : X_red ⟶ X be a reduction of X, presented by a presheaf Xred of Type u together with an isomorphism from its universe lift. Then Xred is a separated algebraic space if and only if for every pair of objects of the big fppf site of S with affine underlying scheme and every pair of morphisms from their universe-lifted Yoneda presheaves into X every object of the site representing the fibre product has affine underlying scheme and the canonical map from the tensor product over ℤ of the two rings of global sections to its ring of global sections is surjective.

The implication from the condition to separatedness is AlgebraicGeometry.FormalSpace.isAbsolutelySeparated_reduction_of_hasAffineIntersectionsULift: the inclusion of a reduction is a monomorphism, so the condition restricts from X to the reduction, where it is separatedness by Stacks 0AHS. The converse is AlgebraicGeometry.FormalSpace.hasAffineIntersectionsULift_of_isReduction, the argument of the source through the thickening comparison of the two fibre products.

theorem isAbsolutelySeparated_reduction_iff_hasAffineIntersectionsULift
    {X Xr : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X)
    {i : Xr ⟶ X} (hi : IsReduction B S hS X Xr i)
    {Xred : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (e : Xred ⋙ uliftFunctor.{u + 1} ≅ Xr.obj) :
    Space.IsAbsolutelySeparated B S hS hZ Xred ↔
      HasAffineIntersectionsULift B S hS X.obj

AlgebraicGeometry.FormalSpace.exists_isReduction_and_isAbsolutelySeparated_iff_hasAffineIntersectionsULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ReductionSeparatedConverse.lean, line 455. References: EGA I (10.15.7), “more general”.

Stacks 0AJ6. Let S be a scheme contained in a big fppf site B and let X be a formal algebraic space over S. The reduction of X exists — a reduced algebraic space X_red and a representable thickening i : X_red ⟶ X through which every morphism to X from a reduced algebraic space factors uniquely — it is presented by a presheaf Xred of Type u together with an isomorphism from its universe lift, and the following are equivalent:

  1. Xred is a separated algebraic space;
  2. for every pair of objects of the big fppf site of S with affine underlying scheme and every pair of morphisms from their universe-lifted Yoneda presheaves into X, every object of the site representing the fibre product has affine underlying scheme and the canonical map from the tensor product over ℤ of the two rings of global sections to its ring of global sections is surjective.

The reduction comes from Stacks 0AIN, AlgebraicGeometry.FormalSpace.exists_isReduction_of_isFormalAlgebraicSpace; its presentation by a presheaf of Type u from the pointwise u-smallness of an algebraic space, AlgebraicGeometry.Space.exists_comp_uliftFunctor_iso_of_isAlgebraicSpaceULift; and the equivalence from AlgebraicGeometry.FormalSpace.isAbsolutelySeparated_reduction_iff_hasAffineIntersectionsULift, which reads it against any reduction and any presentation of it.

theorem exists_isReduction_and_isAbsolutelySeparated_iff_hasAffineIntersectionsULift
    (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X) :
    ∃ (Xr : FppfSheaf B S hS) (i : Xr ⟶ X) (Xred : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
      (_ : Xred ⋙ uliftFunctor.{u + 1} ≅ Xr.obj),
      IsReduction B S hS X Xr i ∧
        (Space.IsAbsolutelySeparated B S hS hZ Xred ↔
          HasAffineIntersectionsULift B S hS X.obj)

AlgebraicGeometry.FormalSpace.isAbsolutelySeparated_reduction_iff_hasRepresentableAffineIntersectionsULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ReductionSeparatedRepresentable.lean, line 177. The attribute's comment: “both implications, with clause (2) in the source's own form, which asserts that the fibre product U ×_X V is representable by an object of the site and that its underlying scheme is affine, rather than quantifying over the objects of the site representing it. The two readings agree on a formal algebraic space, by AlgebraicGeometry.FormalSpace.hasRepresentableAffineIntersectionsULift_iff, whose nontrivial direction is the representability assertion of Stacks 0AIP for an arbitrary formal algebraic space. Read against a reduction of X, in the sense of AlgebraicGeometry.FormalSpace.IsReduction, and a presentation of it by a presheaf of Type u together with an isomorphism from its universe lift -- an algebraic space over S being a presheaf of Type u while a formal algebraic space is a sheaf of Type (u + 1). The tag with the reduction and its presentation produced is AlgebraicGeometry.FormalSpace.exists_isReduction_and_isAbsolutelySeparated_iff_hasRepresentableAffineIntersectionsULift”. References: EGA I (10.15.7), “more general”.

Stacks 0AJ6, with clause (2) asserting representability. Let X be a formal algebraic space over S and let i : X_red ⟶ X be a reduction of X, presented by a presheaf Xred of Type u together with an isomorphism from its universe lift. Then Xred is a separated algebraic space if and only if for every pair of objects of the big fppf site of S with affine underlying scheme and every pair of morphisms from their universe-lifted Yoneda presheaves into X the fibre product is represented by an object of the site with affine underlying scheme and the canonical map from the tensor product over ℤ of the two rings of global sections to its ring of global sections is surjective.

This is …isAbsolutelySeparated_reduction_iff_hasAffineIntersectionsULift composed with …hasRepresentableAffineIntersectionsULift_iff, which identifies clause (2) in the source's form with the form that quantifies over the representing objects.

theorem isAbsolutelySeparated_reduction_iff_hasRepresentableAffineIntersectionsULift
    {X Xr : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X)
    {i : Xr ⟶ X} (hi : IsReduction B S hS X Xr i)
    {Xred : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (e : Xred ⋙ uliftFunctor.{u + 1} ≅ Xr.obj) :
    Space.IsAbsolutelySeparated B S hS hZ Xred ↔
      HasRepresentableAffineIntersectionsULift B S hS X.obj

AlgebraicGeometry.FormalSpace.exists_isReduction_and_isAbsolutelySeparated_iff_hasRepresentableAffineIntersectionsULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ReductionSeparatedRepresentable.lean, line 213. The attribute's comment: “the reduction and its presentation by a presheaf of Type u produced, from Stacks 0AIN for an arbitrary formal algebraic space and from the pointwise u-smallness of an algebraic space, with clause (2) in the source's own form, which asserts that the fibre product U ×_X V is representable by an object of the site and that its underlying scheme is affine. The variant whose clause (2) quantifies over the objects of the site representing the fibre product instead is AlgebraicGeometry.FormalSpace.exists_isReduction_and_isAbsolutelySeparated_iff_hasAffineIntersectionsULift in StacksFrontier.AlgebraicGeometry.FormalSpace.ReductionSeparatedConverse”. References: EGA I (10.15.7), “more general”.

Stacks 0AJ6, with clause (2) asserting representability. Let S be a scheme contained in a big fppf site B and let X be a formal algebraic space over S. The reduction of X exists — a reduced algebraic space X_red and a representable thickening i : X_red ⟶ X through which every morphism to X from a reduced algebraic space factors uniquely — it is presented by a presheaf Xred of Type u together with an isomorphism from its universe lift, and the following are equivalent:

  1. Xred is a separated algebraic space;
  2. for every pair of objects of the big fppf site of S with affine underlying scheme and every pair of morphisms from their universe-lifted Yoneda presheaves into X, the fibre product is represented by an object of the site with affine underlying scheme and the canonical map from the tensor product over ℤ of the two rings of global sections to its ring of global sections is surjective.

Clause (2) is here the source's own, asserting that U ×_X V is a scheme. The reduction comes from Stacks 0AIN for an arbitrary formal algebraic space, AlgebraicGeometry.FormalSpace.exists_isReduction_of_isFormalAlgebraicSpace.

theorem exists_isReduction_and_isAbsolutelySeparated_iff_hasRepresentableAffineIntersectionsULift
    (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X) :
    ∃ (Xr : FppfSheaf B S hS) (i : Xr ⟶ X) (Xred : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
      (_ : Xred ⋙ uliftFunctor.{u + 1} ≅ Xr.obj),
      IsReduction B S hS X Xr i ∧
        (Space.IsAbsolutelySeparated B S hS hZ Xred ↔
          HasRepresentableAffineIntersectionsULift B S hS X.obj)
Tag 0AJ7, a definition

Tag 0AJ7 in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsSeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineFibreProduct.lean, line 138. The attribute's comment: “clause (2): separated, in the form of clause (2) of Stacks 0AJ6”.

An fppf sheaf X on the big fppf site of S is separated when, for every pair of morphisms to X from sheaves represented by affine schemes over S, every object of the site representing their fibre product is affine and the canonical map from the tensor product over ℤ of the two coordinate rings to its coordinate ring is surjective.

The condition quantifies over the objects of the site representing the fibre product, so on an fppf sheaf whose fibre products are not representable it holds vacuously. On a formal algebraic space it agrees with AlgebraicGeometry.FormalSpace.IsSeparatedFormalAlgebraicSpace, by AlgebraicGeometry.FormalSpace.isSeparatedFormalAlgebraicSpace_iff_isSeparated.

abbrev IsSeparated (X : FppfSheaf B S hS) : Prop

AlgebraicGeometry.FormalSpace.IsQuasiSeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparationAxioms.lean, line 88. The attribute's comment: “clause (1): quasi-separated, in the form of clause (3) of Stacks 0AJ5, whose equivalence with clause (2) of Stacks 0AJ5 and with quasi-separatedness of the reduction is not proved in this library”.

An fppf sheaf X on the big fppf site of S is quasi-separated when, for every pair of morphisms to X from sheaves represented by affine schemes over S, every object of the site representing their fibre product has quasi-compact underlying scheme.

abbrev IsQuasiSeparated (X : FppfSheaf B S hS) : Prop

AlgebraicGeometry.FormalSpace.IsAffineFormalAlgebraicSpace.isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparationAxioms.lean, line 109. The attribute's comment: “clause (2): an affine formal algebraic space is separated, in the form of clause (2) of Stacks 0AJ6, whose equivalence with clause (1) is not proved in this library”.

Every affine formal algebraic space over S is separated, in the form of clause (2) of Stacks 0AJ6.

theorem IsAffineFormalAlgebraicSpace.isSeparated {X : FppfSheaf B S hS}
    (hX : IsAffineFormalAlgebraicSpace B S hS X) : IsSeparated B S hS X

AlgebraicGeometry.FormalSpace.isQuasiSeparated_of_isAffineFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparationAxioms.lean, line 210. The attribute's comment: “clause (1): an affine formal algebraic space is quasi-separated, in the form of clause (3) of Stacks 0AJ5”.

Every affine formal algebraic space over S is quasi-separated, in the form of clause (3) of Stacks 0AJ5.

theorem isQuasiSeparated_of_isAffineFormalAlgebraicSpace {X : FppfSheaf B S hS}
    (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    IsQuasiSeparated B S hS X

AlgebraicGeometry.FormalSpace.IsQuasiSeparatedFormalAlgebraicSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparationAxiomsRepresentable.lean, line 290. The attribute's comment: “clause (1): a formal algebraic space is quasi-separated when the conditions of Stacks 0AJ5 hold, recorded as clause (3) of Stacks 0AJ5 with the fibre product asserted to be a scheme; equivalent to every condition of Stacks 0AJ5 by isQuasiSeparatedFormalAlgebraicSpace_tfae”.

Stacks 0AJ7, clause (1): quasi-separated formal algebraic spaces. A formal algebraic space X over S is quasi-separated when the equivalent conditions of Stacks 0AJ5 hold. The condition recorded is clause (3) of Stacks 0AJ5: for every pair of objects U, V of the big fppf site of S with affine underlying scheme and every pair of morphisms U ⟶ X, V ⟶ X (morphisms h_U ⟶ X, h_V ⟶ X of presheaves out of the universe-lifted Yoneda presheaves), the fibre product U ×_X V is a scheme — represented by an object of the site with a cartesian square over the two morphisms — and that scheme is quasi-compact.

The fibre product is the genuine one, and it is always representable, by Stacks 0AIP; so the condition is never vacuous. Its equivalence with the other conditions of Stacks 0AJ5 — quasi-separatedness of the reduction of X, and clause (2) with quasi-compact test objects — is AlgebraicGeometry.FormalSpace.isQuasiSeparatedFormalAlgebraicSpace_tfae. On a formal algebraic space it agrees with AlgebraicGeometry.FormalSpace.IsQuasiSeparated, by AlgebraicGeometry.FormalSpace.isQuasiSeparatedFormalAlgebraicSpace_iff_isQuasiSeparated.

def IsQuasiSeparatedFormalAlgebraicSpace (X : FppfSheaf B S hS) : Prop

AlgebraicGeometry.FormalSpace.IsSeparatedFormalAlgebraicSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparationAxiomsRepresentable.lean, line 311. The attribute's comment: “clause (2): a formal algebraic space is separated when the conditions of Stacks 0AJ6 hold, recorded as clause (2) of Stacks 0AJ6 with the fibre product asserted to be a scheme; equivalent to clause (1) of Stacks 0AJ6 by isSeparatedFormalAlgebraicSpace_tfae”.

Stacks 0AJ7, clause (2): separated formal algebraic spaces. A formal algebraic space X over S is separated when the equivalent conditions of Stacks 0AJ6 hold. The condition recorded is clause (2) of Stacks 0AJ6: for every pair of objects U, V of the big fppf site of S with affine underlying scheme and every pair of morphisms U ⟶ X, V ⟶ X (morphisms h_U ⟶ X, h_V ⟶ X of presheaves out of the universe-lifted Yoneda presheaves), the fibre product U ×_X V is a scheme — represented by an object of the site with a cartesian square over the two morphisms — that scheme is affine, and the canonical map 𝒪(U) ⊗_ℤ 𝒪(V) ⟶ 𝒪(U ×_X V) is surjective.

The fibre product is the genuine one, and it is always representable, by Stacks 0AIP; so the condition is never vacuous. Its equivalence with clause (1) of Stacks 0AJ6, separatedness of the reduction of X, is AlgebraicGeometry.FormalSpace.isSeparatedFormalAlgebraicSpace_tfae. On a formal algebraic space it agrees with AlgebraicGeometry.FormalSpace.IsSeparated, by AlgebraicGeometry.FormalSpace.isSeparatedFormalAlgebraicSpace_iff_isSeparated.

def IsSeparatedFormalAlgebraicSpace (X : FppfSheaf B S hS) : Prop

AlgebraicGeometry.FormalSpace.isQuasiSeparatedFormalAlgebraicSpace_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparationAxiomsRepresentable.lean, line 356. The attribute's comment: “clause (1): the definition is equivalent to each of the conditions of Stacks 0AJ5, read against a reduction of X presented by a presheaf of Type u, which exists by Stacks 0AIN”.

Stacks 0AJ7, clause (1), is the class of the conditions of Stacks 0AJ5. Let X be a formal algebraic space over S and let i : X_red ⟶ X be a reduction of X, presented by a presheaf Xred of Type u together with an isomorphism from its universe lift. The following are equivalent: X is quasi-separated in the sense of Stacks 0AJ7; Xred is a quasi-separated algebraic space (clause (1) of Stacks 0AJ5); for every pair of quasi-compact test objects over X the fibre product is a quasi-compact scheme (clause (2)); and the same for every pair of affine test objects (clause (3)).

theorem isQuasiSeparatedFormalAlgebraicSpace_tfae
    {X Xr : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X)
    {i : Xr ⟶ X} (hi : IsReduction B S hS X Xr i)
    {Xred : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (e : Xred ⋙ uliftFunctor.{u + 1} ≅ Xr.obj) :
    List.TFAE
      [ IsQuasiSeparatedFormalAlgebraicSpace B S hS X,
        Space.IsAbsolutelyQuasiSeparated B S hS hZ Xred,
        HasRepresentableQuasiCompactIntersectionsULift B S hS
          (fun Z : Scheme.{u} ↦ CompactSpace (Z : Type u)) X.obj,
        HasRepresentableQuasiCompactIntersectionsULift B S hS
          (fun Z : Scheme.{u} ↦ IsAffine Z) X.obj ]

AlgebraicGeometry.FormalSpace.isSeparatedFormalAlgebraicSpace_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparationAxiomsRepresentable.lean, line 381. The attribute's comment: “clause (2): the definition is equivalent to clause (1) of Stacks 0AJ6, read against a reduction of X presented by a presheaf of Type u, which exists by Stacks 0AIN”.

Stacks 0AJ7, clause (2), is the class of the conditions of Stacks 0AJ6. Let X be a formal algebraic space over S and let i : X_red ⟶ X be a reduction of X, presented by a presheaf Xred of Type u together with an isomorphism from its universe lift. Then X is separated in the sense of Stacks 0AJ7 if and only if Xred is a separated algebraic space (clause (1) of Stacks 0AJ6).

theorem isSeparatedFormalAlgebraicSpace_tfae
    {X Xr : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X)
    {i : Xr ⟶ X} (hi : IsReduction B S hS X Xr i)
    {Xred : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (e : Xred ⋙ uliftFunctor.{u + 1} ≅ Xr.obj) :
    IsSeparatedFormalAlgebraicSpace B S hS X ↔ Space.IsAbsolutelySeparated B S hS hZ Xred
Tag 0AN3, a lemma

Tag 0AN3 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineFibreProduct.lean, line 254. The attribute's comment: “the fibre product of affine formal algebraic spaces over a separated base”.

The fibre product of two affine formal algebraic spaces over a separated fppf sheaf with representable relative products is an affine formal algebraic space.

theorem isAffineFormalAlgebraicSpace_pullback
    {X Y Z : FppfSheaf B S hS} (p : X ⟶ Z) (q : Y ⟶ Z)
    (hZrep : HasRepresentableRelativeProducts B S hS Z)
    (hZsep : IsSeparated B S hS Z)
    (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y) :
    IsAffineFormalAlgebraicSpace B S hS (pullback p q)

AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_pullback_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineFibreProductFormalBase.lean, line 59. The attribute's comment: “clause (1): the fibre product of two affine formal algebraic spaces over a separated formal algebraic space, at the hypotheses of the source”.

Stacks 0AN3, clause (1). The fibre product of two affine formal algebraic spaces over a separated formal algebraic space is an affine formal algebraic space.

theorem isAffineFormalAlgebraicSpace_pullback_of_isFormalAlgebraicSpace
    {X Y Z : FppfSheaf B S hS} (p : X ⟶ Z) (q : Y ⟶ Z)
    (hZ : IsFormalAlgebraicSpace B S hS Z)
    (hZsep : IsSeparated B S hS Z)
    (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y) :
    IsAffineFormalAlgebraicSpace B S hS (pullback p q)

AlgebraicGeometry.FormalSpace.exists_quotientSystem_iso_pullback_completedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletedTensorFibreProduct.lean, line 651. The attribute's comment: “clause (3), that the fibre product of two McQuillan affine formal algebraic spaces over a third is the formal spectrum of the completed tensor product of their weakly admissible topological rings, compatibly with both projections. The quotient system on the completed tensor product and the comparison with the fibre product are proved. The one input this library does not carry is the hypothesis epres: that the fibre product is itself a formal spectrum, which is clause (2) of the same tag together with the McQuillan criterion of Stacks 0AIC. Stacks 0AN0 is full faithfulness of Spf against formal spectra only (existsUnique_continuousHom_formalSpectrumMap_eq), not a universal property against arbitrary fppf sheaves, so representability of the fibre product is not a consequence of it; separatedness of the base, which the source uses only to obtain clauses (1) and (2), is therefore not needed here and is not assumed”.

Stacks 0AN3, clause (3). Let A₀, A₁ and A be weakly admissible topological rings over S with chart systems D₀, D₁, D, and let A₀ → A₁ and A₀ → A be continuous homomorphisms over S. If the fibre product Spf A₁ ×_{Spf A₀} Spf A is itself the formal spectrum of a weakly admissible topological ring over S, then it is the formal spectrum of the completed tensor product A₁ ⊗̂_{A₀} A: that ring carries a chart system over S and an isomorphism onto the fibre product compatible with both projections, through which the two projections are the formal spectra of the two canonical maps into the completed tensor product.

theorem exists_quotientSystem_iso_pullback_completedTensorProduct
    (h₀ : TopologicalRing.IsWeaklyAdmissible A₀)
    (h₁ : TopologicalRing.IsWeaklyAdmissible A₁) (hA : TopologicalRing.IsWeaklyAdmissible A)
    (D₀ : QuotientSystem B S hS A₀) (D₁ : QuotientSystem B S hS A₁)
    (D : QuotientSystem B S hS A)
    (c₁ : ContinuousHom D₀ D₁) (c : ContinuousHom D₀ D)
    (hc₁ : c₁.toRingHom = algebraMap A₀ A₁) (hc : c.toRingHom = algebraMap A₀ A)
    {R : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [IsLinearTopology R R]
    (hR : TopologicalRing.IsWeaklyAdmissible R) (E : QuotientSystem B S hS R)
    (epres : pullback (formalSpectrumMap h₀ c₁) (formalSpectrumMap h₀ c) ≅ formalSpectrum E) :
    ∃ (DT : QuotientSystem B S hS (TopologicalRing.CompletedTensorProduct
        (R := A₀) (M := A₁) (N := A)))
        (t₁ : ContinuousHom D₁ DT) (t : ContinuousHom D DT)
        (eT : pullback (formalSpectrumMap h₀ c₁) (formalSpectrumMap h₀ c) ≅ formalSpectrum DT),
      t₁.toRingHom = algebraMap A₁ (TopologicalRing.CompletedTensorProduct
          (R := A₀) (M := A₁) (N := A)) ∧
        t.toRingHom = algebraMap A (TopologicalRing.CompletedTensorProduct
            (R := A₀) (M := A₁) (N := A)) ∧
        eT.hom ≫ formalSpectrumMap h₁ t₁ =
          pullback.fst (formalSpectrumMap h₀ c₁) (formalSpectrumMap h₀ c) ∧
        eT.hom ≫ formalSpectrumMap hA t =
          pullback.snd (formalSpectrumMap h₀ c₁) (formalSpectrumMap h₀ c)

AlgebraicGeometry.FormalSpace.exists_continuous_ringEquiv_completedTensorProduct_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletedTensorFibreProduct.lean, line 779. The attribute's comment: “clause (3) read on chart rings: the chart ring of the fibre product of two McQuillan affine formal algebraic spaces over a third is the completed tensor product of their weakly admissible topological rings, by an isomorphism of topological rings compatible with both projections. The one input this library does not carry is the hypothesis epres, that the fibre product is itself a formal spectrum, which is clause (2) of the same tag together with the McQuillan criterion of Stacks 0AIC; Stacks 0AN0 is full faithfulness of Spf against formal spectra only, so representability of the fibre product does not follow from it. Separatedness of the base, which the source uses only for clauses (1) and (2), is not needed here and is not assumed”.

Stacks 0AN3, clause (3), in the form of an isomorphism of chart rings. If the fibre product Spf A₁ ×_{Spf A₀} Spf A is the formal spectrum of a weakly admissible topological ring R over S, then R is isomorphic, as a topological ring, to the completed tensor product A₁ ⊗̂_{A₀} A, compatibly with the two projections: the isomorphism carries each of the two canonical maps into the completed tensor product to the continuous homomorphism that Stacks 0AN0 attaches to the corresponding projection.

theorem exists_continuous_ringEquiv_completedTensorProduct_pullback
    (h₀ : TopologicalRing.IsWeaklyAdmissible A₀)
    (h₁ : TopologicalRing.IsWeaklyAdmissible A₁) (hA : TopologicalRing.IsWeaklyAdmissible A)
    (D₀ : QuotientSystem B S hS A₀) (D₁ : QuotientSystem B S hS A₁)
    (D : QuotientSystem B S hS A)
    (c₁ : ContinuousHom D₀ D₁) (c : ContinuousHom D₀ D)
    (hc₁ : c₁.toRingHom = algebraMap A₀ A₁) (hc : c.toRingHom = algebraMap A₀ A)
    {R : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [IsLinearTopology R R]
    (hR : TopologicalRing.IsWeaklyAdmissible R) (E : QuotientSystem B S hS R)
    (epres : pullback (formalSpectrumMap h₀ c₁) (formalSpectrumMap h₀ c) ≅ formalSpectrum E) :
    ∃ ε : (TopologicalRing.CompletedTensorProduct (R := A₀) (M := A₁) (N := A)) ≃+* R,
      Continuous ε ∧ Continuous ε.symm ∧
        ∀ (a₁ : ContinuousHom D₁ E) (a : ContinuousHom D E),
          formalSpectrumMap h₁ a₁ = epres.inv ≫
              pullback.fst (formalSpectrumMap h₀ c₁) (formalSpectrumMap h₀ c) →
            formalSpectrumMap hA a = epres.inv ≫
              pullback.snd (formalSpectrumMap h₀ c₁) (formalSpectrumMap h₀ c) →
            ε.toRingHom.comp (algebraMap A₁ (TopologicalRing.CompletedTensorProduct
                (R := A₀) (M := A₁) (N := A))) = a₁.toRingHom ∧
              ε.toRingHom.comp (algebraMap A (TopologicalRing.CompletedTensorProduct
                  (R := A₀) (M := A₁) (N := A))) = a.toRingHom

AlgebraicGeometry.FormalSpace.exists_quotientSystem_iso_pullback_completedTensorProduct_of_isWeaklyAdmissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletedTensorFibreProduct.lean, line 1241. The attribute's comment: “clause (3), that the fibre product of two McQuillan affine formal algebraic spaces over a third is the formal spectrum of the completed tensor product of their weakly admissible topological rings, compatibly with both projections, with no hypothesis beyond the weak admissibility of the three rings: the fibre product is proved to be a formal spectrum, as the colimit of the stagewise fibre products”.

Stacks 0AN3, clause (3), with no presentation of the fibre product assumed. Let A₀, A₁ and A be weakly admissible topological rings over S with quotient systems D₀, D₁, D, and let A₀ → A₁ and A₀ → A be continuous homomorphisms over S. Then the fibre product Spf A₁ ×_{Spf A₀} Spf A is the formal spectrum of the completed tensor product A₁ ⊗̂_{A₀} A: that ring carries a quotient system over S and an isomorphism of its formal spectrum onto the fibre product, through which the two projections are the formal spectra of the two canonical maps into the completed tensor product.

This is exists_quotientSystem_iso_pullback_completedTensorProduct with its hypothesis epres discharged: the fibre product of the two formal spectra is the colimit of the stagewise fibre products, which are the stages of Spf (A₁ ⊗̂_{A₀} A) at the projection kernels, and those are cofinal among all its stages.

theorem exists_quotientSystem_iso_pullback_completedTensorProduct_of_isWeaklyAdmissible
    (h₀ : TopologicalRing.IsWeaklyAdmissible A₀)
    (h₁ : TopologicalRing.IsWeaklyAdmissible A₁) (hA : TopologicalRing.IsWeaklyAdmissible A)
    (D₀ : QuotientSystem B S hS A₀) (D₁ : QuotientSystem B S hS A₁)
    (D : QuotientSystem B S hS A)
    (c₁ : ContinuousHom D₀ D₁) (c : ContinuousHom D₀ D)
    (hc₁ : c₁.toRingHom = algebraMap A₀ A₁) (hc : c.toRingHom = algebraMap A₀ A) :
    ∃ (DT : QuotientSystem B S hS (TopologicalRing.CompletedTensorProduct
        (R := A₀) (M := A₁) (N := A)))
        (t₁ : ContinuousHom D₁ DT) (t : ContinuousHom D DT)
        (eT : pullback (formalSpectrumMap h₀ c₁) (formalSpectrumMap h₀ c) ≅ formalSpectrum DT),
      t₁.toRingHom = algebraMap A₁ (TopologicalRing.CompletedTensorProduct
          (R := A₀) (M := A₁) (N := A)) ∧
        t.toRingHom = algebraMap A (TopologicalRing.CompletedTensorProduct
            (R := A₀) (M := A₁) (N := A)) ∧
        eT.hom ≫ formalSpectrumMap h₁ t₁ =
          pullback.fst (formalSpectrumMap h₀ c₁) (formalSpectrumMap h₀ c) ∧
        eT.hom ≫ formalSpectrumMap hA t =
          pullback.snd (formalSpectrumMap h₀ c₁) (formalSpectrumMap h₀ c)

AlgebraicGeometry.FormalSpace.exists_formalSpectrum_completedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletedTensorProductFibreProduct.lean, line 1017. The attribute's comment: “clause (3): the fibre product of two McQuillan affine formal algebraic spaces over a McQuillan affine separated one is the formal spectrum of the completed tensor product of their weakly admissible topological rings, at the hypotheses of the source”.

Stacks 0AN3, clause (3). Let S be a scheme contained in a big fppf site B, let X ⟶ Z and Y ⟶ Z be morphisms of fppf sheaves over S with Z separated, and suppose that X, Y and Z are the formal spectra of weakly admissible topological rings A, B and C over S, the two morphisms being the ones induced by continuous homomorphisms C ⟶ A and C ⟶ B over S. Then the fibre product X ×_Z Y is the formal spectrum of the completed tensor product A ⊗̂_C B, which is again weakly admissible.

theorem exists_formalSpectrum_completedTensorProduct (𝔅 : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : 𝔅.Contains S) {A B C : Type u} [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [IsLinearTopology A A] [CommRing B] [TopologicalSpace B]
    [IsTopologicalRing B] [IsLinearTopology B B] [CommRing C] [TopologicalSpace C]
    [IsTopologicalRing C] [IsLinearTopology C C]
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hB : TopologicalRing.IsWeaklyAdmissible B)
    (hC : TopologicalRing.IsWeaklyAdmissible C) (DA : QuotientSystem 𝔅 S hS A)
    (DB : QuotientSystem 𝔅 S hS B) (DC : QuotientSystem 𝔅 S hS C)
    {X Y Z : FppfSheaf 𝔅 S hS} (f : X ⟶ Z) (g : Y ⟶ Z) (eX : X ≅ formalSpectrum DA)
    (eY : Y ≅ formalSpectrum DB) (eZ : Z ≅ formalSpectrum DC)
    (_hZsep : IsSeparated 𝔅 S hS Z) (cToA : ContinuousHom DC DA) (cToB : ContinuousHom DC DB)
    (hf : formalSpectrumMap hC cToA = eX.inv ≫ f ≫ eZ.hom)
    (hg : formalSpectrumMap hC cToB = eY.inv ≫ g ≫ eZ.hom) :
    letI : Algebra C A := cToA.toRingHom.toAlgebra
    letI : Algebra C B := cToB.toRingHom.toAlgebra
    ∃ DT : QuotientSystem 𝔅 S hS
        (TopologicalRing.CompletedTensorProduct (R := C) (M := A) (N := B)),
      TopologicalRing.IsWeaklyAdmissible
          (TopologicalRing.CompletedTensorProduct (R := C) (M := A) (N := B)) ∧
        Nonempty (pullback f g ≅ formalSpectrum DT)

AlgebraicGeometry.FormalSpace.exists_formalSpectrum_completedTensorProduct_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletedTensorProductFibreProductSupplement.lean, line 373. The attribute's comment: “clause (3): the fibre product of two McQuillan affine formal algebraic spaces over a separated McQuillan affine formal algebraic space is the formal spectrum of the completed tensor product of the three weakly admissible topological rings, compatibly with both projections; McQuillanness of the two factors is in the form of condition (2) of Stacks 0AIC, the form the library's clause (2) consumes”.

Let X ⟶ Z and Y ⟶ Z be morphisms of fppf sheaves on the big fppf site of S with Z a separated affine formal algebraic space, let X and Y be McQuillan affine formal algebraic spaces, and let X = Spf A, Y = Spf B, Z = Spf C for weakly admissible topological rings A, B, C over S with the two morphisms induced by continuous ring maps C → A and C → B over S. Then

X ×_Z Y = Spf (A ⊗̂_C B),

compatibly with the two projections and with the canonical maps of A and of B into the completed tensor product.

The conclusion produces the ring over S, that is the AlgebraicGeometry.FormalSpace.QuotientSystem of A ⊗̂_C B, together with the two continuous homomorphisms over S out of A and B, says that those are the canonical maps into the completion of the algebraic tensor product, and characterises the isomorphism by its compatibility with both projections of the fibre product.

theorem exists_formalSpectrum_completedTensorProduct_compatible {X Y Z : FppfSheaf 𝔅 S hS}
    (hX : HasAffineClosedImmersionCriterionMapToSpec 𝔅 S hS X)
    (hY : HasAffineClosedImmersionCriterionMapToSpec 𝔅 S hS Y)
    (hZ : IsAffineFormalAlgebraicSpace 𝔅 S hS Z)
    (hZsep : IsSeparated 𝔅 S hS Z)
    {A B C : Type u}
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    [CommRing C] [TopologicalSpace C] [IsTopologicalRing C] [IsLinearTopology C C]
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (hB : TopologicalRing.IsWeaklyAdmissible B)
    (hC : TopologicalRing.IsWeaklyAdmissible C)
    (DA : QuotientSystem 𝔅 S hS A) (DB : QuotientSystem 𝔅 S hS B)
    (DC : QuotientSystem 𝔅 S hS C)
    (eX : X ≅ formalSpectrum DA) (eY : Y ≅ formalSpectrum DB) (eZ : Z ≅ formalSpectrum DC)
    (f : X ⟶ Z) (g : Y ⟶ Z)
    (cToA : ContinuousHom DC DA) (cToB : ContinuousHom DC DB)
    (hf : formalSpectrumMap hC cToA = eX.inv ≫ f ≫ eZ.hom)
    (hg : formalSpectrumMap hC cToB = eY.inv ≫ g ≫ eZ.hom) :
    letI : Algebra C A := cToA.toRingHom.toAlgebra
    letI : Algebra C B := cToB.toRingHom.toAlgebra
    letI : TopologicalSpace (A ⊗[C] B) :=
      TopologicalRing.tensorProductTopology (R := C) (M := A) (N := B)
    letI : UniformSpace (A ⊗[C] B) :=
      TopologicalRing.tensorProductUniformSpace (R := C) (M := A) (N := B)
    ∃ (DT : QuotientSystem 𝔅 S hS
        (TopologicalRing.CompletedTensorProduct (R := C) (M := A) (N := B)))
      (aToT : ContinuousHom DA DT) (bToT : ContinuousHom DB DT)
      (e : pullback f g ≅ formalSpectrum DT),
      TopologicalRing.IsWeaklyAdmissible
          (TopologicalRing.CompletedTensorProduct (R := C) (M := A) (N := B)) ∧
        aToT.toRingHom = (UniformSpace.Completion.coeRingHom).comp
            (Algebra.TensorProduct.includeLeftRingHom : A →+* A ⊗[C] B) ∧
        bToT.toRingHom = (UniformSpace.Completion.coeRingHom).comp
            ((Algebra.TensorProduct.includeRight : B →ₐ[C] A ⊗[C] B).toRingHom) ∧
        e.hom ≫ formalSpectrumMap hA aToT = pullback.fst f g ≫ eX.hom ∧
        e.hom ≫ formalSpectrumMap hB bToT = pullback.snd f g ≫ eY.hom

AlgebraicGeometry.FormalSpace.isPullback_formalSpectrumMap_completedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSpectrumCompletedTensorProduct.lean, line 1341. The attribute's comment: “clause (3): Spf A ×_{Spf C} Spf B corresponds to the completed tensor product”.

Let A₀ → A₁ and A₀ → A₂ be continuous homomorphisms of weakly admissible topological rings over S. Then the completed tensor product T = A₁ ⊗̂_{A₀} A₂ is weakly admissible and Spf T, with the maps induced by the canonical continuous homomorphisms A₁ → T and A₂ → T, is the fibre product Spf A₁ ×_{Spf A₀} Spf A₂.

theorem isPullback_formalSpectrumMap_completedTensor :
    TopologicalRing.IsWeaklyAdmissible
        (TopologicalRing.CompletedTensorProduct (R := A₀) (M := A₁) (N := A₂)) ∧
      IsPullback (formalSpectrumMap hA₁ (completedTensorLeftHom A₀ hA₁ hA₂ D₁ D₂))
        (formalSpectrumMap hA₂ (completedTensorRightHom A₀ hA₁ hA₂ D₁ D₂ hA₀ φ₁ φ₂ hφ₁ hφ₂))
        (formalSpectrumMap hA₀ φ₁) (formalSpectrumMap hA₀ φ₂)

AlgebraicGeometry.FormalSpace.hasAffineClosedImmersionCriterion_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedFibreProduct.lean, line 247. The attribute's comment: “clause (2): the fibre product of two McQuillan affine formal algebraic spaces over a separated formal algebraic space is McQuillan affine, with McQuillanness in the form of condition (2) of Stacks 0AIC”.

Stacks 0AN3, clause (2). Let X ⟶ Z and Y ⟶ Z be morphisms of fppf sheaves on the big fppf site of S with Z a separated formal algebraic space. If X and Y are McQuillan affine formal algebraic spaces, then so is the fibre product X ×_Z Y.

McQuillanness is here condition (2) of Stacks 0AIC: an affine formal algebraic space together with a morphism to the spectrum of a ring through which every closed immersion of an affine scheme of the site composes to a closed immersion of schemes. The ring witnessing the conclusion is the tensor product over ℤ of the two rings witnessing the hypotheses, which is the ring the source's proof uses.

theorem hasAffineClosedImmersionCriterion_pullback
    {X Y Z : FppfSheaf B S hS} (p : X ⟶ Z) (q : Y ⟶ Z)
    (hZ : IsFormalAlgebraicSpace B S hS Z)
    (hZsep : IsSeparated B S hS Z)
    (hX : HasAffineClosedImmersionCriterionMapToSpec B S hS X)
    (hY : HasAffineClosedImmersionCriterionMapToSpec B S hS Y) :
    HasAffineClosedImmersionCriterionMapToSpec B S hS (pullback p q)

AlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedFibreProduct.lean, line 292. The attribute's comment: “clause (2): the fibre product of two McQuillan affine formal algebraic spaces over a separated formal algebraic space is McQuillan affine, with the conclusion in the form of condition (4) of Stacks 0AIC, the predicate Stacks 0AID names McQuillan in this library”.

Stacks 0AN3, clause (2), in the form of condition (4) of Stacks 0AIC. The fibre product of two McQuillan affine formal algebraic spaces over a separated formal algebraic space is an affine formal algebraic space some presentation of which by affine thickenings has surjective section-ring projections.

This is the predicate AlgebraicGeometry.FormalSpace.HasSomeSurjectivePresentation that Stacks 0AID names "McQuillan" in this library, and it is the hypothesis as well as the conclusion: condition (4) gives condition (2) by AlgebraicGeometry.FormalSpace.hasAffineClosedImmersionCriterion_of_hasSomeSurjectivePresentation, and condition (2) gives condition (4) back by the implications (2) ⟹ (5) ⟹ (4) of Stacks 0AIC.

theorem hasSomeSurjectivePresentation_pullback
    {X Y Z : FppfSheaf B S hS} (p : X ⟶ Z) (q : Y ⟶ Z)
    (hZ : IsFormalAlgebraicSpace B S hS Z)
    (hZsep : IsSeparated B S hS Z)
    (hX : HasSomeSurjectivePresentation B S hS X)
    (hY : HasSomeSurjectivePresentation B S hS Y) :
    HasSomeSurjectivePresentation B S hS (pullback p q)
Tag 0APX, a lemma

Tag 0APX in the Stacks Project.

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_of_isClosedImmersion_diag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparationAxioms.lean, line 228.

A morphism f : U ⟶ X of fppf sheaves over S whose source is separated over S, that is whose diagonal U ⟶ U ⨯ U is a closed immersion, is separated.

theorem isSeparatedMorphism_of_isClosedImmersion_diag {U X : FppfSheaf B S hS}
    (hU : IsClosedImmersion B S hS (diag U)) (f : U ⟶ X) :
    IsSeparatedMorphism B S hS f
Sources
LeanAlgebraicGeometry.FormalSpace.isAbsolutelyQuasiSeparated_reduction_tfae · AlgebraicGeometry.FormalSpace.isAbsolutelyQuasiSeparated_reduction_tfae_representable · AlgebraicGeometry.FormalSpace.isAbsolutelySeparated_reduction_of_hasAffineIntersectionsULift · AlgebraicGeometry.FormalSpace.isAbsolutelySeparated_reduction_iff_hasAffineIntersectionsULift · AlgebraicGeometry.FormalSpace.exists_isReduction_and_isAbsolutelySeparated_iff_hasAffineIntersectionsULift · AlgebraicGeometry.FormalSpace.isAbsolutelySeparated_reduction_iff_hasRepresentableAffineIntersectionsULift · AlgebraicGeometry.FormalSpace.exists_isReduction_and_isAbsolutelySeparated_iff_hasRepresentableAffineIntersectionsULift · AlgebraicGeometry.FormalSpace.IsSeparated

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.