87.17 Quasi-compact formal… to 87.20 Types of formal algebraic…

Section87.17 Quasi-compact formal algebraic spaces #

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

Tag 0AJ9, a lemma

Tag 0AJ9 in the Stacks Project.

AlgebraicGeometry.FormalSpace.tfae_isQuasiCompactSpace_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CoproductRepresentableEtaleConsequences.lean, line 80. The attribute's comment: “the equivalence of the three conditions, for every reduction i : Xred ⟶ X of X, a reduction existing by Stacks 0AIN (exists_isReduction_of_isFormalAlgebraicSpace); nothing is assumed beyond the source's hypotheses, the input hCoproductEtale of AlgebraicGeometry.FormalSpace.tfae_isQuasiCompactSpace_of_isReduction being the theorem AlgebraicGeometry.FormalSpace.coproductsRepresentableEtale”.

Let X be a formal algebraic space over S and let i : Xred ⟶ X be a reduction of X. Then quasi-compactness of Xred, the existence of an atlas as in Definition 0AIM indexed by a finite type, and the existence of a morphism from an affine formal algebraic space which is representable by algebraic spaces, étale and a surjection of sheaves are equivalent.

A reduction of X exists by AlgebraicGeometry.FormalSpace.exists_isReduction_of_isFormalAlgebraicSpace.

theorem tfae_isQuasiCompactSpace_unconditional
    {X Xred : FppfSheaf B S hS} {i : Xred ⟶ X}
    (hX : IsFormalAlgebraicSpace B S hS X) (hi : IsReduction B S hS X Xred i) :
    [Space.IsQuasiCompactSpaceULift.{u + 1} B S hS Xred.obj,
      HasFiniteFormalAtlas B S hS X,
      IsQuasiCompactSpace B S hS X].TFAE

AlgebraicGeometry.FormalSpace.IsQuasiCompactSpace.hasFiniteFormalAtlas', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteFormalAtlas.lean, line 184. The attribute's comment: “the implication (3) ⇒ (2)”.

Stacks 0AJ9, the implication (3) ⇒ (2). A quasi-compact formal algebraic space over S has a finite formal atlas: the one affine formal algebraic space surjecting onto it is an atlas as in Definition 0AIM indexed by a one-point type, the induced map from the coproduct over that type being the given map up to the coproduct inclusion, which is a split epimorphism.

theorem IsQuasiCompactSpace.hasFiniteFormalAtlas' {X : FppfSheaf B S hS}
    (h : IsQuasiCompactSpace B S hS X) : HasFiniteFormalAtlas' B S hS X

AlgebraicGeometry.FormalSpace.HasFiniteFormalAtlas.isQuasiCompactSpace', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteFormalAtlas.lean, line 204. The attribute's comment: “the implication (2) ⇒ (3)”.

Stacks 0AJ9, the implication (2) ⇒ (3). A sheaf with a finite formal atlas is a quasi-compact formal algebraic space over S: the coproduct of the finitely many members of the atlas is an affine formal algebraic space, and the induced morphism from it is representable by algebraic spaces, étale and a surjection of sheaves.

theorem HasFiniteFormalAtlas.isQuasiCompactSpace'
    {X : FppfSheaf B S hS} (h : HasFiniteFormalAtlas' B S hS X) :
    IsQuasiCompactSpace B S hS X

AlgebraicGeometry.FormalSpace.IsQuasiCompactSpace.hasFiniteFormalAtlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactSpaceCriteria.lean, line 221. The attribute's comment: “the implication (3) ⇒ (2)”.

Stacks 0AJ9, the implication (3) ⇒ (2). A quasi-compact formal algebraic space over S has a finite formal atlas: the one affine formal algebraic space surjecting onto it is an atlas as in Definition 0AIM indexed by a one-point type, the induced map from the coproduct over that type being the given map up to the coproduct inclusion, which is a split epimorphism.

theorem IsQuasiCompactSpace.hasFiniteFormalAtlas {X : FppfSheaf B S hS}
    (h : IsQuasiCompactSpace B S hS X) : HasFiniteFormalAtlas B S hS X

AlgebraicGeometry.FormalSpace.IsQuasiCompactSpace.isQuasiCompactSpaceULift_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactSpaceCriteria.lean, line 262. The attribute's comment: “the implication (3) ⇒ (1), with a reduction of X supplied as a hypothesis in place of Stacks 0AIN, on the hypotheses hAffineReduction that a reduction of an affine formal algebraic space is quasi-compact and hReductionEtaleSurjective that the morphism of reductions induced by a representable, étale and surjective morphism is surjective and étale”.

Stacks 0AJ9, the implication (3) ⇒ (1). Let X be a quasi-compact formal algebraic space over S and let i : Xred ⟶ X be a reduction of X. Then Xred is a quasi-compact algebraic space. Indeed, the affine formal algebraic space Y surjecting onto X has a reduction iY : Yred ⟶ Y, the composite Yred ⟶ Y ⟶ X factors through i because Yred is a reduced algebraic space, and the resulting morphism Yred ⟶ Xred is surjective and étale; composing a quasi-compact surjective étale chart of Yred with it gives one of Xred.

theorem IsQuasiCompactSpace.isQuasiCompactSpaceULift_reduction
    (hAffineReduction : AffineReductionsQuasiCompact B S hS)
    (hReductionEtaleSurjective : ReductionsOfEtaleSurjectionsEtaleSurjective B S hS)
    {X Xred : FppfSheaf B S hS} {i : Xred ⟶ X} (hi : IsReduction B S hS X Xred i)
    (h : IsQuasiCompactSpace B S hS X) :
    Space.IsQuasiCompactSpaceULift.{u + 1} B S hS Xred.obj

AlgebraicGeometry.FormalSpace.tfae_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactSpaceCriteria.lean, line 291. The attribute's comment: “the equivalence of the three conditions, with a reduction of X supplied as a hypothesis in place of Stacks 0AIN, and on the hypotheses hFiniteRefinement for the implication (1) ⇒ (2), hCoproductEtale for the implication (2) ⇒ (3), and hAffineReduction and hReductionEtaleSurjective for the implication (3) ⇒ (1)”.

Stacks 0AJ9. Let X be a formal algebraic space over S and let i : Xred ⟶ X be a reduction of X. The following are equivalent:

Xred is a quasi-compact algebraic space,

X admits an atlas as in Definition 0AIM indexed by a finite type,

X receives a morphism from an affine formal algebraic space which is representable by algebraic spaces, étale and a surjection of sheaves.

theorem tfae_isQuasiCompactSpace
    (hAffineReduction : AffineReductionsQuasiCompact B S hS)
    (hReductionEtaleSurjective : ReductionsOfEtaleSurjectionsEtaleSurjective B S hS)
    (hCoproductEtale : CoproductsRepresentableEtale B S hS)
    {X Xred : FppfSheaf B S hS} {i : Xred ⟶ X}
    (_hX : IsFormalAlgebraicSpace B S hS X) (hi : IsReduction B S hS X Xred i)
    (hFiniteRefinement : Space.IsQuasiCompactSpaceULift.{u + 1} B S hS Xred.obj →
      HasFiniteFormalAtlas B S hS X) :
    [Space.IsQuasiCompactSpaceULift.{u + 1} B S hS Xred.obj,
      HasFiniteFormalAtlas B S hS X,
      IsQuasiCompactSpace B S hS X].TFAE

AlgebraicGeometry.FormalSpace.IsQuasiCompactSpace.isQuasiCompactSpaceULift_of_isReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactSpaceCriteriaReduction.lean, line 184. The attribute's comment: “the implication (3) ⇒ (1), for every reduction i : Xred ⟶ X of X, a reduction existing by Stacks 0AIN (exists_isReduction_of_isFormalAlgebraicSpace); nothing is assumed beyond the source's hypotheses”.

Stacks 0AJ9, the implication (3) ⇒ (1). Let X be a quasi-compact formal algebraic space over S and let i : Xred ⟶ X be a reduction of X. Then Xred is a quasi-compact algebraic space.

Let c : Y ⟶ X be the morphism of condition (3), with Y an affine formal algebraic space. The fibre product P = Y ×_X Xred is a reduction of Y by Stacks 0GB7, an étale morphism being smooth, so P is the sheaf of an affine object T of the site by the affine case of Stacks 0AIN. The second projection P ⟶ Xred is a base change of c, hence representable by algebraic spaces and étale, and it is surjective on points because c is; so T ⟶ Xred is a quasi-compact surjective étale chart of Xred.

theorem IsQuasiCompactSpace.isQuasiCompactSpaceULift_of_isReduction
    {X Xred : FppfSheaf B S hS} {i : Xred ⟶ X} (hi : IsReduction B S hS X Xred i)
    (h : IsQuasiCompactSpace B S hS X) :
    Space.IsQuasiCompactSpaceULift.{u + 1} B S hS Xred.obj

AlgebraicGeometry.FormalSpace.hasFiniteFormalAtlas_of_isQuasiCompactSpaceULift_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactSpaceCriteriaRefined.lean, line 155. The attribute's comment: “the implication (1) ⇒ (2), for an arbitrary reduction of X”.

Stacks 0AJ9, the implication (1) ⇒ (2). Let X be a formal algebraic space over S, let i : Xred ⟶ X be a reduction of X and suppose that Xred is a quasi-compact algebraic space. Then X has a finite formal atlas: an atlas as in Definition 0AIM indexed by a finite type.

theorem hasFiniteFormalAtlas_of_isQuasiCompactSpaceULift_reduction
    {X Xred : FppfSheaf B S hS} {i : Xred ⟶ X}
    (hX : IsFormalAlgebraicSpace B S hS X) (hi : IsReduction B S hS X Xred i)
    (hQC : Space.IsQuasiCompactSpaceULift.{u + 1} B S hS Xred.obj) :
    HasFiniteFormalAtlas B S hS X

AlgebraicGeometry.FormalSpace.hasFiniteFormalAtlas_of_isQuasiCompactSpaceULift_of_isReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactSpaceCriteriaSupplement.lean, line 75. The attribute's comment: “the implication (1) ⇒ (2)”.

Let X be a formal algebraic space over S and let i : Xred ⟶ X be a reduction of X whose source is a quasi-compact algebraic space. Then X has a finite formal atlas.

Finitely many members of the atlas as in Definition 0AIM which X carries are already jointly surjective on points, by AlgebraicGeometry.FormalSpace.exists_finite_jointly_surjective_of_isQuasiCompactSpaceULift; what remains is that such a finite subfamily is itself an atlas as in Definition 0AIM, that is that its induced morphism out of the coproduct is a surjection of sheaves. That morphism is representable by algebraic spaces and étale by AlgebraicGeometry.FormalSpace.coproductsRepresentableEtale', hence flat and locally of finite presentation; joint surjectivity on points is surjectivity on points of it, which for a morphism representable by algebraic spaces is surjectivity in the sense of Stacks 03XZ by AlgebraicGeometry.FormalSpace.hasPropertyULift_isSurjectiveULift_iff; and Stacks 05VM turns a representable surjective flat cover into a surjection of sheaves.

theorem hasFiniteFormalAtlas_of_isQuasiCompactSpaceULift_of_isReduction
    {X Xred : FppfSheaf B S hS} {i : Xred ⟶ X} (hX : IsFormalAlgebraicSpace B S hS X)
    (hi : IsReduction B S hS X Xred i)
    (h : Space.IsQuasiCompactSpaceULift.{u + 1} B S hS Xred.obj) :
    HasFiniteFormalAtlas' B S hS X

AlgebraicGeometry.FormalSpace.IsQuasiCompactSpace.isQuasiCompactSpaceULift_reduction_space, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactSpaceCriteriaSupplement.lean, line 119. The attribute's comment: “the implication (3) ⇒ (1)”.

The reduction reduction of a quasi-compact formal algebraic space over S is a quasi-compact algebraic space.

This is AlgebraicGeometry.FormalSpace.IsQuasiCompactSpace.isQuasiCompactSpaceULift_of_isReduction read at the reduction AlgebraicGeometry.FormalSpace.reduction that Stacks 0AIN produces, the formal algebraic space being the source's own hypothesis on X and being implied by condition (3). Condition (1) of the source names the reduction of X, so the statement mentions it; any other reduction is canonically isomorphic to this one by AlgebraicGeometry.FormalSpace.Reduction.iso, and the general statement applies to it directly, so nothing depends on the choice.

theorem IsQuasiCompactSpace.isQuasiCompactSpaceULift_reduction_space {X : FppfSheaf B S hS}
    (h : IsQuasiCompactSpace B S hS X) :
    Space.IsQuasiCompactSpaceULift.{u + 1} B S hS
      (liftSheaf B S hS
        (reduction B S hS X (IsQuasiCompactSpace.isFormalAlgebraicSpace B S hS h)).space).obj

AlgebraicGeometry.FormalSpace.tfae_isQuasiCompactSpace_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactSpaceCriteriaSupplement.lean, line 159. The attribute's comment: “the equivalence of the three conditions”.

Let X be a formal algebraic space over S. The following are equivalent:

the reduction reduction of X is a quasi-compact algebraic space,

X admits an atlas as in Definition 0AIM indexed by a finite type,

X receives a morphism from an affine formal algebraic space which is representable by algebraic spaces, étale and a surjection of sheaves.

Condition (1) is read at the reduction AlgebraicGeometry.FormalSpace.reduction that Stacks 0AIN produces; by AlgebraicGeometry.FormalSpace.Reduction.iso any two reductions of X are canonically isomorphic, so the condition does not depend on the choice, and AlgebraicGeometry.FormalSpace.tfae_isQuasiCompactSpace_of_isReduction_unconditional is the same equivalence at an arbitrary reduction.

theorem tfae_isQuasiCompactSpace_of_isFormalAlgebraicSpace
    {X : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X) :
    [Space.IsQuasiCompactSpaceULift.{u + 1} B S hS
        (liftSheaf B S hS (reduction B S hS X hX).space).obj,
      HasFiniteFormalAtlas' B S hS X,
      IsQuasiCompactSpace B S hS X].TFAE

Tag 0AJA, a definition

Tag 0AJA in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.FormalSpace.IsQuasiCompactSpace, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactSpaceCriteria.lean, line 316 (StacksFrontier): “the definition, realized by condition (3) of Stacks 0AJ9, AlgebraicGeometry.FormalSpace.IsQuasiCompactSpace; the equivalence with conditions (1) and (2) that makes the choice of condition immaterial is tfae_isQuasiCompactSpace, which carries the two hypotheses standing for the steps of the omitted proof of Stacks 0AJ9”.
AlgebraicGeometry.FormalSpace.IsQuasiCompactSpace, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactSpaceCriteriaSupplement.lean, line 249 (StacksFrontier): “the definition, realized by condition (3) of Stacks 0AJ9, AlgebraicGeometry.FormalSpace.IsQuasiCompactSpace; the equivalence with conditions (1) and (2) that makes the choice of condition immaterial is tfae_isQuasiCompactSpace, which is unconditional”.

Tag 0AJB, a lemma

Tag 0AJB in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsQuasiCompactOnSchemeBaseChanges.isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphism.lean, line 228. The attribute's comment: “condition (2) implies condition (3); no other implication among the four conditions is proved here”.

Stacks 0AJB, condition (2) implies condition (3). The fibre product condition over the quasi-compact schemes over S in the site restricts to the affine ones, an affine scheme being quasi-compact.

theorem IsQuasiCompactOnSchemeBaseChanges.isQuasiCompact {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (h : IsQuasiCompactOnSchemeBaseChanges B S hS f) : IsQuasiCompact B S hS f

AlgebraicGeometry.FormalSpace.isQuasiCompactOnReductions_iff_isQuasiCompactULift_chosenReductionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismChosenReduction.lean, line 126. The attribute's comment: “condition (1), in the source's own form — quasi-compactness of the morphism f_red of the chosen reductions — identified with the phrasing of the condition that quantifies over the reductions”.

Stacks 0AJB, condition (1). Let f : X ⟶ Y be a morphism of formal algebraic spaces over S. The morphism f_red : X_red ⟶ Y_red of the chosen reductions is a quasi-compact morphism of algebraic spaces if and only if every morphism between reductions of X and of Y compatible with f is one. The second condition is AlgebraicGeometry.FormalSpace.IsQuasiCompactOnReductions, the phrasing of condition (1) which quantifies over the reductions instead of choosing them.

Given reductions iX : Xred ⟶ X and iY : Yred ⟶ Y and a compatible fred, the universal properties of the chosen reductions supply comparison morphisms a : Xred ⟶ X_red and b : Yred ⟶ Y_red over X and over Y, and these are isomorphisms because two reductions of one sheaf are isomorphic over it. The inclusion of the reduction of Y is a monomorphism, so a ≫ f_red = fred ≫ b, and fred is f_red conjugated by the two isomorphisms.

theorem isQuasiCompactOnReductions_iff_isQuasiCompactULift_chosenReductionMap
    {X Y : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsQuasiCompactOnReductions B S hS f ↔
      Space.IsQuasiCompactULift.{u + 1} B S hS (chosenReductionMap B S hS hX hY f).hom

AlgebraicGeometry.FormalSpace.IsQuasiCompact.isQuasiCompactULift_chosenReductionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismChosenReduction.lean, line 169. The attribute's comment: “condition (3) implies condition (1), for the morphism f_red of the chosen reductions”.

Stacks 0AJB, condition (3) implies condition (1). Let f : X ⟶ Y be a morphism of formal algebraic spaces over S such that every fibre product of f with an affine scheme over S in the site mapping to Y is a quasi-compact formal algebraic space — that is, let f be quasi-compact in the sense of Stacks 0AJC. Then the morphism f_red : X_red ⟶ Y_red of the chosen reductions is a quasi-compact morphism of algebraic spaces.

theorem IsQuasiCompact.isQuasiCompactULift_chosenReductionMap {X Y : FppfSheaf B S hS}
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (h : IsQuasiCompact B S hS f) :
    Space.IsQuasiCompactULift.{u + 1} B S hS (chosenReductionMap B S hS hX hY f).hom

AlgebraicGeometry.FormalSpace.IsQuasiCompactOnSchemeBaseChanges.isQuasiCompactULift_chosenReductionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismChosenReduction.lean, line 181. The attribute's comment: “condition (2) implies condition (1), for the morphism f_red of the chosen reductions”.

Stacks 0AJB, condition (2) implies condition (1). The fibre product condition over the quasi-compact schemes over S in the site restricts to the affine ones, which already makes the morphism f_red of the chosen reductions a quasi-compact morphism of algebraic spaces.

theorem IsQuasiCompactOnSchemeBaseChanges.isQuasiCompactULift_chosenReductionMap
    {X Y : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (h : IsQuasiCompactOnSchemeBaseChanges B S hS f) :
    Space.IsQuasiCompactULift.{u + 1} B S hS (chosenReductionMap B S hS hX hY f).hom

AlgebraicGeometry.FormalSpace.IsQuasiCompact.isQuasiCompactOnSchemeBaseChanges, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismDecomposition.lean, line 202. The attribute's comment: “condition (3) implies condition (2)”.

Stacks 0AJB, condition (3) implies condition (2). Let f : X ⟶ Y be a morphism of fppf sheaves on the big fppf site of S every one of whose fibre products with an affine scheme over S in the site mapping to Y is a quasi-compact formal algebraic space over S. Then the same holds over every quasi-compact scheme over S in the site.

Let T be such a scheme and let W be a fibre product of f with a point T ⟶ Y. A finite affine open covering {U_i ⟶ T} of T inside the site exists because T is quasi-compact (AlgebraicGeometry.BigFppfOver.exists_finite_affine_open_cover). Each W ×_T U_i is, by pasting the two cartesian squares, a fibre product of f with the affine point U_i ⟶ Y, hence a quasi-compact formal algebraic space by the hypothesis; each projection W ×_T U_i ⟶ W is a base change of U_i ⟶ T, hence representable étale, an open immersion being étale; and the family of projections is jointly surjective because {U_i ⟶ T} generates a covering sieve and coproducts of sheaves of types are stable under base change. So AlgebraicGeometry.FormalSpace.isQuasiCompactSpace_of_finite_isRepresentableEtale_cover applies.

theorem IsQuasiCompact.isQuasiCompactOnSchemeBaseChanges {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (h : IsQuasiCompact B S hS f) : IsQuasiCompactOnSchemeBaseChanges B S hS f

AlgebraicGeometry.FormalSpace.isQuasiCompact_iff_isQuasiCompactOnSchemeBaseChanges, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismDecomposition.lean, line 265. The attribute's comment: “the equivalence of conditions (2) and (3)”.

Stacks 0AJB, the equivalence of conditions (2) and (3). For a morphism of fppf sheaves on the big fppf site of S, the fibre product condition over the quasi-compact schemes over S in the site and the fibre product condition over the affine ones are equivalent.

One implication restricts the quantifier, an affine scheme being quasi-compact, and is AlgebraicGeometry.FormalSpace.IsQuasiCompactOnSchemeBaseChanges.isQuasiCompact; the other is AlgebraicGeometry.FormalSpace.IsQuasiCompact.isQuasiCompactOnSchemeBaseChanges. This is the first cycle closed among the four conditions of Stacks 0AJB.

theorem isQuasiCompact_iff_isQuasiCompactOnSchemeBaseChanges {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) :
    IsQuasiCompact B S hS f ↔ IsQuasiCompactOnSchemeBaseChanges B S hS f

AlgebraicGeometry.FormalSpace.IsQuasiCompactOnReductions.hasQuasiCompactFormalAtlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismFormalAtlas.lean, line 269. The attribute's comment: “condition (1) implies condition (4), with the reductions quantified over in place of Stacks 0AIN and with the source's own hypothesis that X and Y be formal algebraic spaces, which is what supplies the covering of Y that condition (4) asks for”.

Stacks 0AJB, condition (1) implies condition (4). Let f : X ⟶ Y be a morphism of formal algebraic spaces over S such that every morphism between reductions of X and of Y compatible with f is a quasi-compact morphism of algebraic spaces. Then there is a covering {Yⱼ ⟶ Y} as in Definition 0AIM all of whose fibre products with f are quasi-compact formal algebraic spaces over S.

The covering is the atlas of Y that the hypothesis IsFormalAlgebraicSpace B S hS Y supplies, which is the covering Definition 0AIM provides and the one the source's hypothesis on Y names. Its members are affine formal algebraic spaces, hence quasi-compact formal algebraic spaces, and representable by algebraic spaces and étale, so IsQuasiCompactOnReductions.isQuasiCompactSpace_of_isRepresentableEtale applies to each fibre product.

theorem IsQuasiCompactOnReductions.hasQuasiCompactFormalAtlas {X Y : FppfSheaf B S hS}
    {f : X ⟶ Y} (h : IsQuasiCompactOnReductions B S hS f)
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y) :
    HasQuasiCompactFormalAtlas B S hS f

AlgebraicGeometry.FormalSpace.IsQuasiCompact.hasQuasiCompactFormalAtlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismFormalAtlas.lean, line 292. The attribute's comment: “condition (3) implies condition (4), with the source's own hypothesis that X and Y be formal algebraic spaces”.

Stacks 0AJB, condition (3) implies condition (4). A morphism of formal algebraic spaces over S which is quasi-compact in the sense of Stacks 0AJC — every fibre product of it with an affine scheme over S in the site mapping to its target is a quasi-compact formal algebraic space — admits a covering of its target as in Definition 0AIM all of whose fibre products with it are quasi-compact formal algebraic spaces.

Condition (3) implies condition (1) by AlgebraicGeometry.FormalSpace.IsQuasiCompact.isQuasiCompactOnReductions, and condition (1) implies condition (4).

theorem IsQuasiCompact.hasQuasiCompactFormalAtlas {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (h : IsQuasiCompact B S hS f) (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) : HasQuasiCompactFormalAtlas B S hS f

AlgebraicGeometry.FormalSpace.IsQuasiCompactOnSchemeBaseChanges.hasQuasiCompactFormalAtlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismFormalAtlas.lean, line 305. The attribute's comment: “condition (2) implies condition (4), with the source's own hypothesis that X and Y be formal algebraic spaces”.

Stacks 0AJB, condition (2) implies condition (4). A morphism of formal algebraic spaces over S every one of whose fibre products with a quasi-compact scheme over S in the site mapping to its target is a quasi-compact formal algebraic space admits a covering of its target as in Definition 0AIM all of whose fibre products with it are quasi-compact formal algebraic spaces: condition (2) restricts to the affine schemes, which is condition (3).

theorem IsQuasiCompactOnSchemeBaseChanges.hasQuasiCompactFormalAtlas {X Y : FppfSheaf B S hS}
    {f : X ⟶ Y} (h : IsQuasiCompactOnSchemeBaseChanges B S hS f)
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y) :
    HasQuasiCompactFormalAtlas B S hS f

AlgebraicGeometry.FormalSpace.IsQuasiCompact.isQuasiCompactOnReductions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismReductions.lean, line 183. The attribute's comment: “condition (3) implies condition (1), with the reductions quantified over in place of Stacks 0AIN”.

Stacks 0AJB, condition (3) implies condition (1). Let f : X ⟶ Y be a morphism of fppf sheaves on the big fppf site of S such that every fibre product of f with an affine scheme over S in the site mapping to Y is a quasi-compact formal algebraic space — that is, let f be quasi-compact in the sense of Stacks 0AJC. Then every morphism between reductions of X and of Y compatible with f is a quasi-compact morphism of algebraic spaces.

Quasi-compactness of the morphism of reductions is tested against the quasi-compact algebraic spaces mapping to the reduction of Y; such a space has, by Stacks 03H6, a surjective étale chart by an affine scheme of the site, along which the test descends, so it suffices to treat an affine scheme of the site, which is isQuasiCompactSpaceULift_pullback_of_affine.

theorem IsQuasiCompact.isQuasiCompactOnReductions (hf : IsQuasiCompact B S hS f) :
    IsQuasiCompactOnReductions B S hS f

AlgebraicGeometry.FormalSpace.IsQuasiCompactOnSchemeBaseChanges.isQuasiCompactOnReductions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismReductions.lean, line 197. The attribute's comment: “condition (2) implies condition (1), with the reductions quantified over in place of Stacks 0AIN”.

Stacks 0AJB, condition (2) implies condition (1). The fibre product condition over the quasi-compact schemes over S in the site restricts to the affine ones, which already implies quasi-compactness of every induced morphism of reductions.

theorem IsQuasiCompactOnSchemeBaseChanges.isQuasiCompactOnReductions
    (hf : IsQuasiCompactOnSchemeBaseChanges B S hS f) :
    IsQuasiCompactOnReductions B S hS f

AlgebraicGeometry.FormalSpace.HasQuasiCompactFormalAtlas.isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismTFAE.lean, line 172. The attribute's comment: “condition (4) implies condition (3)”.

Stacks 0AJB, condition (4) implies condition (3). Let f : X ⟶ Y be a morphism of fppf sheaves on the big fppf site of S admitting a covering {cⱼ : Yⱼ ⟶ Y} as in Definition 0AIM all of whose fibre products with f are quasi-compact formal algebraic spaces. Then every fibre product of f with an affine scheme over S in the site mapping to Y is a quasi-compact formal algebraic space; that is, f is quasi-compact in the sense of Stacks 0AJC.

Let g : T ⟶ Y with T affine. The base changes Yⱼ ×_Y T are objects Vⱼ of the site étale over T (Stacks 0AIG); an affine open of some Vⱼ through each point of T, and quasi-compactness of T, give finitely many affine objects Uₖ étale over T, covering it, each mapping to a member Yⱼ compatibly with g. The fibre product W = X ×_Y T is covered along representable étale morphisms by the finitely many W ×_T Uₖ = X ×_Y Uₖ, each of which is quasi-compact by AlgebraicGeometry.FormalSpace.isQuasiCompactSpace_of_isPullback_comp, so W is quasi-compact by AlgebraicGeometry.FormalSpace.isQuasiCompactSpace_of_finite_isRepresentableEtale_cover.

theorem HasQuasiCompactFormalAtlas.isQuasiCompact {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (h : HasQuasiCompactFormalAtlas B S hS f) : IsQuasiCompact B S hS f

AlgebraicGeometry.FormalSpace.tfae_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismTFAE.lean, line 297. The attribute's comment: “the equivalence of the four conditions”.

Stacks 0AJB. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S. The following are equivalent:

the morphism f_red : X_red ⟶ Y_red induced between the reductions (Stacks 0AIN) is a quasi-compact morphism of algebraic spaces;

for every quasi-compact scheme T over S in the site and morphism T ⟶ Y, the fibre product X ×_Y T is a quasi-compact formal algebraic space;

the same for every affine scheme T over S in the site;

there is a covering {Yⱼ ⟶ Y} as in Definition 0AIM such that every X ×_Y Yⱼ is a quasi-compact formal algebraic space.

The reductions in condition (1) are the chosen ones, AlgebraicGeometry.FormalSpace.reduction, and f_red is AlgebraicGeometry.FormalSpace.chosenReductionMap. The cycle of implications is (1) ⇒ (4) (IsQuasiCompactOnReductions.hasQuasiCompactFormalAtlas), (4) ⇒ (3) (HasQuasiCompactFormalAtlas.isQuasiCompact), (3) ⇒ (2) (IsQuasiCompact.isQuasiCompactOnSchemeBaseChanges) and (2) ⇒ (1) (IsQuasiCompactOnSchemeBaseChanges.isQuasiCompactULift_chosenReductionMap).

theorem tfae_isQuasiCompact {X Y : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE
      [Space.IsQuasiCompactULift.{u + 1} B S hS (chosenReductionMap B S hS hX hY f).hom,
        IsQuasiCompactOnSchemeBaseChanges B S hS f,
        IsQuasiCompact B S hS f,
        HasQuasiCompactFormalAtlas B S hS f]

Tag 0AJC, a definition

Tag 0AJC in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsQuasiCompact, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphism.lean, line 199. The attribute's comment: “condition (3) of Stacks 0AJB taken as the definition”.

Stacks 0AJC, in the form of Stacks 0AJB, condition (3). A morphism of formal algebraic spaces over S is quasi-compact when every fibre product of it with an affine scheme over S in the site mapping to its target is a quasi-compact formal algebraic space over S. The condition makes sense, and is stated, for an arbitrary morphism of fppf sheaves on the big fppf site of S.

abbrev IsQuasiCompact {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop

Tag 0AM2, a lemma

Tag 0AM2 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isQuasiCompact_iff_hasPropertyULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphism.lean, line 394. The attribute's comment: “both directions, for an arbitrary morphism of fppf sheaves representable by algebraic spaces, with two named hypotheses: QuasiCompactSpaceAgreesOnAlgebraicSpaces, the agreement of the quasi-compactness notions of Stacks 0AJ9 and Stacks 03E3 on an algebraic space, and the implication (3) ⇒ (2) of Stacks 0AJB for the morphism”.

Stacks 0AM2. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S which is representable by algebraic spaces. Then f is quasi-compact in the sense of Stacks 0AJC — every fibre product of it with an affine scheme over S in the site is a quasi-compact formal algebraic space — exactly when it is quasi-compact in the sense of Bootstrap, Definition 03XZ: every fibre product of it with a scheme over S in the site is quasi-compact over that scheme as a morphism of algebraic spaces.

Both directions pass through the agreement of the two notions of quasi-compactness of a space on an algebraic space, which is the hypothesis AlgebraicGeometry.FormalSpace.QuasiCompactSpaceAgreesOnAlgebraicSpaces. For the remaining direction the bootstrap condition must be tested against the quasi-compact, not only the affine, schemes over S in the site, which is the implication (3) ⇒ (2) of Stacks 0AJB and is the second hypothesis. The witnesses that the source and the target are formal algebraic spaces are not used, so the statement is for an arbitrary morphism of fppf sheaves.

theorem isQuasiCompact_iff_hasPropertyULift {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (hagree : QuasiCompactSpaceAgreesOnAlgebraicSpaces B S hS)
    (hbase : IsQuasiCompact B S hS f → IsQuasiCompactOnSchemeBaseChanges B S hS f) :
    IsQuasiCompact B S hS f ↔
      Space.HasPropertyULift.{u + 1} B S hS
        (Space.quasiCompactPropertyULift.{u + 1} B S hS) f.hom hf

AlgebraicGeometry.FormalSpace.isQuasiCompact_iff_hasPropertyULift', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismComparison.lean, line 120. The attribute's comment: “both directions, for an arbitrary morphism of fppf sheaves representable by algebraic spaces”.

Stacks 0AM2. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S which is representable by algebraic spaces. Then f is quasi-compact in the sense of Stacks 0AJC — every fibre product of it with an affine scheme over S in the site is a quasi-compact formal algebraic space — exactly when it is quasi-compact in the sense of Bootstrap, Definition 03XZ: every fibre product of it with a scheme over S in the site is quasi-compact over that scheme as a morphism of algebraic spaces.

Both directions pass through the agreement of the two notions of quasi-compactness of a space on an algebraic space, which is AlgebraicGeometry.FormalSpace.quasiCompactSpaceAgreesOnAlgebraicSpaces. For the remaining direction the bootstrap condition must be tested against the quasi-compact, not only the affine, schemes over S in the site, which is the implication (3) ⇒ (2) of Stacks 0AJB, AlgebraicGeometry.FormalSpace.IsQuasiCompact.isQuasiCompactOnSchemeBaseChanges. The witnesses that the source and the target are formal algebraic spaces are not used, so the statement is for an arbitrary morphism of fppf sheaves.

theorem isQuasiCompact_iff_hasPropertyULift' {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom) :
    IsQuasiCompact B S hS f ↔
      Space.HasPropertyULift.{u + 1} B S hS
        (Space.quasiCompactPropertyULift.{u + 1} B S hS) f.hom hf

Sources

Section87.18 Quasi-compact and quasi-separated formal algebraic spaces #

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

Tag 0AJE, a lemma

Tag 0AJE in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_colimit_presentation_of_isAffineFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactQuasiSeparatedPresentation.lean, line 114. The attribute's comment: “the conclusion for an AFFINE formal algebraic space only; the general quasi-compact quasi-separated case is not proved here, see the implementation notes”.

An affine formal algebraic space over S is a directed colimit of algebraic spaces over S along thickenings.

public theorem exists_colimit_presentation_of_isAffineFormalAlgebraicSpace
    (X : FppfSheaf B S hS) (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) := Sheaf.instHasColimitsOfSize
    ∃ (Λ : Type (u + 1)) (pre : Preorder Λ),
      letI : Preorder Λ := pre
      Nonempty Λ ∧ IsDirected Λ (· ≤ ·) ∧
        ∃ D : Λ ⥤ AlgebraicSpaces B S hS,
          (∀ ⦃i j : Λ⦄ (f : i ⟶ j), Space.IsThickeningHom B S hS (D.map f)) ∧
          Nonempty (X ≅ colimit (D ⋙ liftSheafFunctor B S hS))

AlgebraicGeometry.FormalSpace.exists_colimit_presentation_of_quasiCompact_quasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactQuasiSeparatedPresentation.lean, line 205.

Let S be a scheme contained in a big fppf site B and let X be a formal algebraic space over S which is quasi-compact and quasi-separated. Then X is a directed colimit of algebraic spaces over S all of whose transition morphisms are thickenings.

theorem exists_colimit_presentation_of_quasiCompact_quasiSeparated
    (X : FppfSheaf B S hS) (_hX : IsFormalAlgebraicSpace B S hS X)
    (hqc : IsQuasiCompactSpace B S hS X) (hqs : IsQuasiSeparated B S hS X) :
    letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) := Sheaf.instHasColimitsOfSize
    ∃ (Λ : Type (u + 1)) (pre : Preorder Λ),
      letI : Preorder Λ := pre
      Nonempty Λ ∧ IsDirected Λ (· ≤ ·) ∧
        ∃ D : Λ ⥤ AlgebraicSpaces B S hS,
          (∀ ⦃i j : Λ⦄ (f : i ⟶ j), Space.IsThickeningHom B S hS (D.map f)) ∧
          Nonempty (X ≅ colimit (D ⋙ liftSheafFunctor B S hS))

Tag 0AJF, a remark

Tag 0AJF in the Stacks Project.

AlgebraicGeometry.LocallyTopologicallyRingedSpace.exists_subfamily_isFundamentalSystemOfIdealsOfDefinitionOn_of_isFormalScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FundamentalSystemOfIdealsOfDefinition.lean, line 147. The attribute's comment: “the shrinking of a fundamental system of WEAK ideals of definition to one of ideals of definition; the weak system is a hypothesis, see the implementation notes”.

Stacks 0AJF. A quasi-compact formal scheme à la EGA carrying a fundamental system of weak ideals of definition carries a fundamental system of genuine ideals of definition, over a finite covering by affine formal open subschemes.

This is the remark's conclusion. Its hypothesis — the fundamental system of weak ideals of definition — is what the translation of Stacks 0AJE supplies, and that translation is not carried by this library, although Stacks 0AJE itself is; see the implementation notes of this file. Here the class of opens is the class of affine formal open subschemes, so the two geometric inputs of exists_subfamily_isFundamentalSystemOfIdealsOfDefinitionOn 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.

public theorem exists_subfamily_isFundamentalSystemOfIdealsOfDefinitionOn_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 𝒰 = ⊤ ∧
      ∃ 𝒮' : Set (IdealSheaf X), 𝒮' ⊆ 𝒮 ∧ 𝒮'.Nonempty ∧
        IsFundamentalSystemOfIdealsOfDefinitionOn 𝒮' (· ∈ 𝒰)

AlgebraicGeometry.exists_isFundamentalSystemOfIdealsOfDefinitionOn_of_isFormalScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FundamentalSystemOfIdealsOfDefinitionExistence.lean, line 568.

Stacks 0AJF. Every quasi-compact and quasi-separated formal scheme à la EGA has a fundamental system of ideals of definition: a nonempty family of ideal sheaves, sectionwise directed, each of which is an ideal of definition over every affine formal open subscheme, and whose ideals of sections over every affine formal open subscheme form a neighbourhood basis of zero.

The members are the intersections ⋂ᵢ ker(Spec (Aᵢ/Jᵢ) ⟶ X) over a finite covering by affine formal charts Spf Aᵢ, which is the ideal of the scheme-theoretic image that the source's induction produces; see the implementation notes. Quasi-separatedness is that of the underlying space, which for a formal scheme à la EGA is quasi-separatedness of the formal scheme.

theorem exists_isFundamentalSystemOfIdealsOfDefinitionOn_of_isFormalScheme
    {X : LTRS.{u}} [CompactSpace ↥X] [QuasiSeparatedSpace ↥X] (hX : IsFormalScheme X) :
    ∃ 𝒮 : Set (IdealSheaf X), 𝒮.Nonempty ∧
      (∀ I ∈ 𝒮, ∀ J ∈ 𝒮, ∃ K ∈ 𝒮, ∀ W : Opens X,
        K.ideal W ≤ I.ideal W ∧ K.ideal W ≤ J.ideal W) ∧
      IsFundamentalSystemOfIdealsOfDefinitionOn 𝒮 (IsAffineFormalOpen X)

Tag 0DE8, a lemma

Tag 0DE8 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_iff_isAffine_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineOfAffineReduction.lean, line 396. The attribute's comment: “affineness of the reduction rendered as its being the sheaf of an object of the site with affine underlying scheme, the shape Stacks 0AIN delivers in the affine case; stated for an arbitrary reduction i : X_red -> X, which generalizes the source's canonical one”.

Stacks 0DE8. Let S be a scheme contained in a big fppf site B and let X be a formal algebraic space over S with reduction i : X_red ⟶ X as in Stacks 0AIN. Then X is an affine formal algebraic space over S if and only if X_red is affine, that is, if and only if it is the sheaf of an object of the site with affine underlying scheme.

Nothing is granted. The converse direction uses, for one stage of the presentation of Stacks 0AJE, that an algebraic space receiving a surjective closed immersion from an affine scheme of the site is affine: AlgebraicGeometry.FormalSpace.isAffineOfSurjectiveClosedImmersion, the closed-immersion case of Stacks 07VS, proved in StacksFrontier.AlgebraicGeometry.Spaces.Thickenings.AffineOfAffineThickening.

theorem isAffineFormalAlgebraicSpace_iff_isAffine_reduction
    {X Xred : FppfSheaf B S hS} (hX : IsFormalAlgebraicSpace B S hS X)
    {i : Xred ⟶ X} (hi : IsReduction B S hS X Xred i) :
    IsAffineFormalAlgebraicSpace B S hS X ↔
      ∃ T : BigFppfOver B S hS, IsAffine ((BigFppfOver.toScheme B S hS).obj T) ∧
        Nonempty ((uliftYoneda.{u + 1}).obj T ≅ Xred.obj)

Sources

LeanAlgebraicGeometry.FormalSpace.exists_colimit_presentation_of_isAffineFormalAlgebraicSpace · AlgebraicGeometry.FormalSpace.exists_colimit_presentation_of_quasiCompact_quasiSeparated ·

AlgebraicGeometry.LocallyTopologicallyRingedSpace.exists_subfamily_isFundamentalSystemOfIdealsOfDefinitionOn_of_isFormalScheme

· AlgebraicGeometry.exists_isFundamentalSystemOfIdealsOfDefinitionOn_of_isFormalScheme · AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_iff_isAffine_reduction

Section87.19 Morphisms representable by algebraic spaces #

Section 87.19 of the Stacks Project, Tag 0AJG. 15 tags here are carried by 83 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AJG, the section

Tag 0AJG in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsLocallyOfFiniteType.of_isRepresentableEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableEtaleFiniteType.lean, line 99. The attribute's comment: “the theory of morphisms of algebraic spaces available to a morphism representable by algebraic spaces, in the instance this library uses it: a representable etale morphism is locally of finite type in the sense of Definition 0AM4”.

Stacks 0AJG. A morphism of fppf sheaves on the big fppf site of S which is representable by algebraic spaces and étale is locally of finite type in the sense of Stacks 0AM4. This is the instance of the theory of morphisms representable by algebraic spaces that the rig-surjectivity theory of Stacks 0AQS and Stacks 0AQV asks for: étaleness of the morphism of algebraic spaces cut out by a represented base change already makes it locally of finite type.

theorem IsLocallyOfFiniteType.of_isRepresentableEtale {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : IsRepresentableEtale B S hS f) :
    IsLocallyOfFiniteType B S hS f

Tag 0APY, a lemma

Tag 0APY in the Stacks Project.

AlgebraicGeometry.Space.isRepresentableByAlgebraicSpacesULift_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Representable.lean, line 380. The attribute's comment: “representable by algebraic spaces in an arbitrary value universe”.

A composition of morphisms representable by algebraic spaces is representable by algebraic spaces, for presheaves on the big fppf site of S with values in Type (max w u).

theorem isRepresentableByAlgebraicSpacesULift_comp
    {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max w u)} (a : F ⟶ G) (b : G ⟶ H)
    (ha : IsRepresentableByAlgebraicSpacesULift.{w} B S hS a)
    (hb : IsRepresentableByAlgebraicSpacesULift.{w} B S hS b) :
    IsRepresentableByAlgebraicSpacesULift.{w} B S hS (a ≫ b)

Declarations registered for the tag:

CategoryTheory.Functor.relativelyRepresentable.isMultiplicative registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/Representable.lean, line 395 (StacksFrontier): “representable by schemes”.

Tag 0APZ, a lemma

Tag 0APZ in the Stacks Project.

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

A base change of a morphism representable by algebraic spaces is representable by algebraic spaces: in a cartesian square of presheaves on the big fppf site of S with values in Type (max w u) whose right-hand column a is representable by algebraic spaces, the left-hand column a' is representable by algebraic spaces too.

theorem isRepresentableByAlgebraicSpacesULift_of_isPullback
    {F G G' H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max w u)}
    (p : H ⟶ F) (a' : H ⟶ G') (a : F ⟶ G) (g : G' ⟶ G) (h : IsPullback p a' a g)
    (ha : IsRepresentableByAlgebraicSpacesULift.{w} B S hS a) :
    IsRepresentableByAlgebraicSpacesULift.{w} B S hS a'

Declarations registered for the tag:

CategoryTheory.Functor.relativelyRepresentable.isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/Representable.lean, line 110 (StacksFrontier): “representable by schemes”.

Tag 0AQ0, a lemma

Tag 0AQ0 in the Stacks Project.

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

Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of fppf sheaves on the big fppf site of S with Y a formal algebraic space. If f ≫ g is representable by algebraic spaces then so is f.

theorem isRepresentableByAlgebraicSpacesULift_of_comp_of_isFormalAlgebraicSpace
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hY : IsFormalAlgebraicSpace B S hS Y)
    (hcomp : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (f.hom ≫ g.hom)) :
    Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom

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

Stacks 0AQ0 when the intermediate sheaf is an affine formal algebraic space. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of fppf sheaves on the big fppf site of S with Y an affine formal algebraic space. If f ≫ g is representable by algebraic spaces then so is f, the relative diagonal of g being representable by Stacks 0AN2.

theorem isRepresentableByAlgebraicSpacesULift_of_comp_of_isAffineFormal
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y)
    (hcomp : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (f.hom ≫ g.hom)) :
    Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom

AlgebraicGeometry.FormalSpace.isRepresentableByAlgebraicSpacesULift_of_comp_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableCancellation.lean, line 172. The attribute's comment: “for a second morphism which is a monomorphism of fppf sheaves”.

Stacks 0AQ0 when the second morphism is a monomorphism. Its relative diagonal is then an isomorphism, hence representable by objects of the site.

theorem isRepresentableByAlgebraicSpacesULift_of_comp_of_mono {X Y Z : FppfSheaf B S hS}
    (f : X ⟶ Y) (g : Y ⟶ Z) [Mono g]
    (hcomp : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (f.hom ≫ g.hom)) :
    Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom

Tag 0AN4, a lemma

Tag 0AN4 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRepresentable_of_isRepresentableAfterSourceCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableAfterSourceCover.lean, line 319. The attribute's comment: “condition (5) implies condition (1)”.

Stacks 0AN4, condition (5) implies condition (1). Let f : X ⟶ Y be a morphism of formal algebraic spaces over S admitting a covering {Uᵢ ⟶ X} as in Definition 0AIM whose members factor through affine formal algebraic spaces Vᵢ with Vᵢ ⟶ Y and Uᵢ ⟶ Vᵢ representable by algebraic spaces. Then f is representable by algebraic spaces.

Each composite Uᵢ ⟶ X ⟶ Y equals Uᵢ ⟶ Vᵢ ⟶ Y, which is representable by algebraic spaces by Stacks 0APY, and representability descends along the étale covering by AlgebraicGeometry.FormalSpace.isRepresentableByAlgebraicSpacesULift_of_etaleCover_comp. Of the hypothesis that X is a formal algebraic space only the set-theoretic condition of Stacks 0AIS is used, and affineness of the Vᵢ is not used.

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

AlgebraicGeometry.FormalSpace.isRepresentable_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableLocalityTFAE.lean, line 101.

Stacks 0AN4. For a morphism f : X ⟶ Y of formal algebraic spaces over S the following are equivalent: 1. f is representable by algebraic spaces; 2. there is a commutative square U ⟶ V over f with U, V formal algebraic spaces, vertical arrows representable by algebraic spaces, U ⟶ X surjective étale and U ⟶ V representable by algebraic spaces; 3. every commutative square U ⟶ V over f with U, V formal algebraic spaces and vertical arrows representable by algebraic spaces has U ⟶ V representable by algebraic spaces; 4. there is a covering {Yⱼ ⟶ Y} as in Definition 0AIM and for each j a covering {Xⱼᵢ ⟶ Yⱼ ×_Y X} as in Definition 0AIM with every Xⱼᵢ ⟶ Yⱼ representable by algebraic spaces; 5. there is a covering {Xᵢ ⟶ X} as in Definition 0AIM and for each i a factorization Xᵢ ⟶ Yᵢ ⟶ Y with Yᵢ an affine formal algebraic space, Yᵢ ⟶ Y and Xᵢ ⟶ Yᵢ representable by algebraic spaces.

The source's sixth item, add more here, is a placeholder and not a condition.

theorem isRepresentable_tfae {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y) :
    List.TFAE [Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom,
      IsRepresentableOnSomeSquare B S hS f,
      IsRepresentableOnEverySquare B S hS f,
      IsRepresentableAfterTargetCover B S hS f,
      IsRepresentableOnFactoredAtlas B S hS f]

AlgebraicGeometry.FormalSpace.isRepresentableOnSomeSquare_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableLocalOnSourceAndTarget.lean, line 171. The attribute's comment: “condition (1) implies condition (2), reading surjectivity of the source column as surjectivity of the morphism of sheaves”.

Stacks 0AN4, condition (1) implies condition (2). The square formed by the identities of X and of Y witnesses condition (2).

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

AlgebraicGeometry.FormalSpace.isRepresentableOnEverySquare_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableLocalOnSourceAndTarget.lean, line 187. The attribute's comment: “condition (1) implies condition (3), with Stacks 0AQ0 — that a morphism of formal algebraic spaces is representable by algebraic spaces as soon as its composite with a further morphism is — carried as the hypothesis h0AQ0, since this library does not have it”.

Stacks 0AN4, condition (1) implies condition (3). In a square as in condition (3) the composite U ⟶ X ⟶ Y is representable by algebraic spaces by Stacks 0APY, and it factors through V, so Stacks 0AQ0 applies to U ⟶ V ⟶ Y.

The hypothesis h0AQ0 is Stacks 0AQ0, which this library does not carry.

theorem isRepresentableOnEverySquare_of_isRepresentable {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hY : IsFormalAlgebraicSpace B S hS Y)
    (h0AQ0 : ∀ {A A' A'' : FppfSheaf B S hS} (s : A ⟶ A') (r : A' ⟶ A''),
      IsFormalAlgebraicSpace B S hS A → IsFormalAlgebraicSpace B S hS A' →
      IsFormalAlgebraicSpace B S hS A'' →
      Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (s ≫ r).hom →
      Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS s.hom)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom) :
    IsRepresentableOnEverySquare B S hS f

AlgebraicGeometry.FormalSpace.isRepresentable_of_isRepresentableOnEverySquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableLocalOnSourceAndTarget.lean, line 205. The attribute's comment: “condition (3) implies condition (1)”.

Stacks 0AN4, condition (3) implies condition (1). The square formed by the identities of X and of Y is a square as in condition (3) whose upper horizontal map is f.

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

AlgebraicGeometry.FormalSpace.isRepresentableAfterTargetCover_of_everySquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableLocalOnSourceAndTarget.lean, line 223. The attribute's comment: “condition (3) implies condition (4), with Stacks 0AJ3 — that the fibre product of a chart of the target with the morphism is a formal algebraic space — carried as the hypothesis h0AJ3, since this library does not have it”.

Stacks 0AN4, condition (3) implies condition (4). The atlas of the target and the atlases of the fibre products of its members with the source witness condition (4): a chart Uⱼᵢ of Vⱼ ×_Y X maps to X by a morphism representable by algebraic spaces, because the second projection is a base change of Vⱼ ⟶ Y, and the square it forms with f and Vⱼ ⟶ Y commutes by the universal property of the fibre product.

The hypothesis h0AJ3 is the assertion of Stacks 0AJ3 that Vⱼ ×_Y X is a formal algebraic space, which this library does not carry.

theorem isRepresentableAfterTargetCover_of_everySquare {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hY : IsFormalAlgebraicSpace B S hS Y)
    (h0AJ3 : ∀ (V : FppfSheaf B S hS) (v : V ⟶ Y), IsAffineFormalAlgebraicSpace B S hS V →
      IsRepresentableEtale B S hS v → IsFormalAlgebraicSpace B S hS (pullback v f))
    (hf : IsRepresentableOnEverySquare B S hS f) :
    IsRepresentableAfterTargetCover B S hS f

Tag 0AJH, a lemma

Tag 0AJH in the Stacks Project.

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_representable_over_affineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableOverAffine.lean, line 129. The attribute's comment: “granting Stacks 0AIU, that a directed colimit of algebraic spaces along thickenings is a formal algebraic space, which this library does not carry and which is taken as the hypothesis h0AIU; the set-theoretic condition of Stacks 0AIS on the source is the hypothesis hXset, as it is for Stacks 0AJ1”.

Stacks 0AJH, granting Stacks 0AIU. If Y is an affine formal algebraic space over S and f : X ⟶ Y is a map of fppf sheaves representable by algebraic spaces, then X is a formal algebraic space over S.

Writing Y as the directed colimit of its affine stages, each fibre product of X with a stage over Y is an algebraic space, the transition morphisms of these fibre products are representable thickenings, and X is their colimit; the hypothesis h0AIU is Stacks 0AIU, applied to that presentation.

theorem isFormalAlgebraicSpace_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)
    (hXset : SatisfiesSetTheoreticCondition B S hS X)
    (h0AIU : ∀ (Λ : Type (u + 1)) [Preorder Λ] [Nonempty Λ] [IsDirected Λ (· ≤ ·)]
      (E : Λ ⥤ FppfSheaf B S hS),
      (∀ i : Λ, Space.IsAlgebraicSpaceULift.{u + 1} B S hS (E.obj i).obj) →
      (∀ ⦃i j : Λ⦄ (g : i ⟶ j),
        Space.IsRepresentableThickeningULift.{u + 1} B S hS (E.map g).hom) →
      ∀ Z : FppfSheaf B S hS, SatisfiesSetTheoreticCondition B S hS Z →
        Nonempty (Z ≅ colimit E) → IsFormalAlgebraicSpace B S hS Z) :
    IsFormalAlgebraicSpace B S hS X

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_representable_over_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableOverAffineCharts.lean, line 585.

Stacks 0AJH. Let S be a scheme, let Y be an affine formal algebraic space over S, and let f : X ⟶ Y be a morphism of sheaves on the big fppf site of S which is representable by algebraic spaces. Then X is a formal algebraic space over S.

The affine étale charts of one stage X₀ = Y₀ ×_Y X are transported to X along the representable thickening X₀ ⟶ X; the stages of a transported chart over the stages Y_μ of Y are algebraic spaces over the affine Y_μ whose base change to Y₀ is affine, hence affine by the thickening case of Stacks 07VT (AlgebraicGeometry.Space.isAffineSpace_of_isClosedSubspace_of_isSurjective_terminal), so each transported chart is an affine formal algebraic space, and the charts cover X.

theorem isFormalAlgebraicSpace_of_representable_over_isAffineFormal
    {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) :
    IsFormalAlgebraicSpace B S hS X

Tag 0AJI, a lemma

Tag 0AJI in the Stacks Project.

AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_isRepresentableByAlgebraicSpacesULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocallyNoetherianSource.lean, line 65.

Stacks 0AJI. If Y is a formal algebraic space over S and f : X ⟶ Y is a morphism of fppf sheaves representable by algebraic spaces, then X is a formal algebraic space over S.

This is AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_of_representable_over_formal with its hypotheses proved: the set-theoretic condition of X and of the base changed atlas members by satisfiesSetTheoreticCondition_of_isRepresentableByAlgebraicSpacesULift_of_isFormalAlgebraicSpace and Stacks 0AIU by its corrected form isFormalAlgebraicSpace_of_colimit_isRepresentableThickeningULift.

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

Tag 0AKN, a lemma

Tag 0AKN in the Stacks Project.

AlgebraicGeometry.FormalSpace.relative_isAffineHom_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/AllTestObjects.lean, line 250.

Stacks 0AKN. Let S be a scheme contained in a big fppf site B and let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces. Then f is representable by schemes and affine: every base change of f along a morphism to Y from a sheaf represented by an object of the site is represented by an object of the site, and the induced morphism of underlying schemes is affine.

theorem relative_isAffineHom_of_isRepresentableByAlgebraicSpaces
    {X Y : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))} (f : X ⟶ Y)
    (hX : _root_.AlgebraicGeometry.IsAffineFormalAlgebraicSpace B S hS X)
    (hY : _root_.AlgebraicGeometry.IsAffineFormalAlgebraicSpace B S hS Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom) :
    (MorphismProperty.inverseImage (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) f

AlgebraicGeometry.FormalSpace.exists_affine_baseChange_of_isRepresentableByAlgebraicSpaces', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/MorphismOfAffines.lean, line 691. The attribute's comment: “representability by schemes together with affineness, over every test object of the site whose underlying scheme is affine”.

Stacks 0AKN over the test objects with affine underlying scheme. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces, and let g be a morphism to Y from a sheaf represented by an object U of the site with affine underlying scheme. Then the fibre product of f and g is represented by an object of the site with affine underlying scheme, and the induced morphism to U is an affine morphism of schemes: f is representable by schemes and affine over U.

Of the two sheaves only the presentations by affine thickenings are used, not the set-theoretic condition of Stacks 0AIS which together with them makes them affine formal algebraic spaces; so the conclusion is available for the formal spectrum of a weakly admissible topological ring over any site containing its quotient spectra, with no condition on the size of the site.

theorem exists_affine_baseChange_of_isRepresentableByAlgebraicSpaces'
    {X Y : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))} (f : X ⟶ Y)
    (hX : HasThickeningPresentation B S hS X)
    (hY : HasThickeningPresentation B S hS Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (U : BigFppfOver B S hS) (hU : IsAffine ((BigFppfOver.toScheme B S hS).obj U))
    (g : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj U ⟶ Y) :
    ∃ (V : BigFppfOver B S hS)
      (p : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj V ⟶ X) (q : V ⟶ U),
      IsPullback p ((Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).map q) f g ∧
        IsAffine ((BigFppfOver.toScheme B S hS).obj V) ∧
        IsAffineHom ((BigFppfOver.toScheme B S hS).map q)

AlgebraicGeometry.FormalSpace.relative_isAffineHom_of_hasThickeningPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/MorphismOfAffines.lean, line 787. The attribute's comment: “both assertions of the source -- representability by schemes and affineness -- over an arbitrary test object of the site”.

Stacks 0AKN. A morphism f : X ⟶ Y of affine formal algebraic spaces over S which is representable by algebraic spaces is representable by schemes, and the morphism of schemes underlying each of its represented base changes is affine. Nothing is assumed of the test objects: this is the source's assertion over every object of the site.

Over a test object with affine underlying scheme the conclusion is AlgebraicGeometry.FormalSpace.exists_affine_baseChange_of_isRepresentableByAlgebraicSpaces, and it carries in addition that the representing object is affine, which an arbitrary test object cannot have. The passage to an arbitrary test object U is affine-locality on the target, carried out in the value universe of the site: the fibre product X ×_Y U is an algebraic space over S, because f is representable by algebraic spaces and U is representable, hence pointwise u-small, so it is the universe lift of an algebraic space Z₀ in the value universe of the site and the projection to U descends with it. The affine form above, read over each morphism of the site into U with affine source, is exactly the affine-base-change condition of that descended projection, which relative Tag 03JH for a morphism out of an algebraic space — AlgebraicGeometry.Space.exists_representing_over_of_holdsOnAffineBaseChange_of_isAlgebraicSpace — glues into a single object of the site with affine projection to U, affineness of a morphism of schemes being Zariski-local at the target.

As in the affine form, of the two sheaves only the presentations by affine thickenings are used and not the set-theoretic condition of Stacks 0AIS.

theorem relative_isAffineHom_of_hasThickeningPresentation
    {X Y : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))} (f : X ⟶ Y)
    (hX : HasThickeningPresentation B S hS X)
    (hY : HasThickeningPresentation B S hS Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom) :
    (MorphismProperty.inverseImage
      (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative
        (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) f

Tag 0AN5, a lemma

Tag 0AN5 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isTaut_of_isRepresentableByAlgebraicSpacesULift_formalSpectrumMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableFormalSpectrumTaut.lean, line 167. The attribute's comment: “(1) implies (3), under the set-theoretic conditions AlgebraicGeometry.FormalSpace.QuotientSystem.HasLargeSite on both quotient systems, which are what make the two formal spectra affine formal algebraic spaces by Stacks 0AIF; the converse implication (3) implies (1) carries the second of them”.

The implication (1) ⟹ (3) of Stacks 0AN5, with the hypotheses this library needs. Let φ : A ⟶ C be a continuous homomorphism of weakly admissible topological rings over S whose formal spectrum Spf φ : Spf C ⟶ Spf A is representable by algebraic spaces over S. Then the underlying ring map of φ is taut.

Two hypotheses beyond those of the source are carried, the set-theoretic conditions D.HasLargeSite and E.HasLargeSite on the site; they are named in the tag. See the implementation notes of this file.

theorem isTaut_of_isRepresentableByAlgebraicSpacesULift_formalSpectrumMap
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C)
    (hD : D.HasLargeSite) (hE : E.HasLargeSite)
    (f : ContinuousHom D E)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
      (formalSpectrumMap hA f).hom) :
    RingHom.IsTaut f.toRingHom

AlgebraicGeometry.FormalSpace.isRepresentableByAlgebraicSpacesULift_formalSpectrumMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpectrumFullyFaithful.lean, line 667. The attribute's comment: “(2) implies (1)”.

Stacks 0AN5, the implication from its condition (2) to its condition (1): if the formal spectrum of a continuous homomorphism of weakly admissible topological rings over S is representable by objects of the site, then it is representable by algebraic spaces over S.

theorem isRepresentableByAlgebraicSpacesULift_formalSpectrumMap
    {A C : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing C] [TopologicalSpace C]
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    {D : QuotientSystem B S hS A} {E : QuotientSystem B S hS C} (φ : ContinuousHom D E)
    (hφ : (uliftYoneda.{u + 1} (C := BigFppfOver B S hS)).relativelyRepresentable
      (formalSpectrumMap hA φ).hom) :
    Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (formalSpectrumMap hA φ).hom

AlgebraicGeometry.FormalSpace.relative_isAffineHom_formalSpectrumMap_of_isTaut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautFormalSpectrumAffine.lean, line 202. The attribute's comment: “(3) implies (2)”.

Stacks 0AN5, the implication from its condition (3) to its condition (2): if a continuous homomorphism φ : A ⟶ C of weakly admissible topological rings over S is taut, then Spf φ is representable by objects of the site, and every represented base change of it is an affine morphism of schemes.

This is the source's own argument. A point of Spf A out of an affine object U of the site factors through a quotient stage Spec (A ⧸ I) by Stacks 0AIA, and tautness makes the closure K of φ(I)C a weak ideal of definition, so that Spec (C ⧸ K) = Spf C ×\_\{Spf A} Spec (A ⧸ I); the base change over U is then the affine U ×\_\{Spec (A ⧸ I)} Spec (C ⧸ K). Passing from the affine points of Spf A to arbitrary ones is the gluing of AlgebraicGeometry.FormalSpace.CartesianColimit.relative_of_affineBaseChanges — the step the source leaves at "we conclude" — and it needs the charts over the affine opens of a test object to obey a uniform size bound.

Where the source has a convention on the size of the site, this carries the single set-theoretic hypothesis hE : E.HasLargeSite, and only for that uniform bound: it says the coproduct ∐_K Spec (C ⧸ K) of all the quotient stages of C lies in the site, hence each stage has size at most that of the coproduct, which is one cardinal below the cutoff. Nothing is assumed about A — in particular not that Spf A is an affine formal algebraic space, which is what the implication (1) ⟹ (3) above needs — because the smallness of the sections of Spf C comes from Stacks 0AIA (small_sections_formalSpectrum) rather than from the set-theoretic condition of Stacks 0AIS. That substitution is what removes the finite type condition which bounds the size of the coproduct in AlgebraicGeometry.FormalSpace.CompactPullbackRepresentable.

theorem relative_isAffineHom_formalSpectrumMap_of_isTaut
    {A C : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [CommRing C] [TopologicalSpace C] [IsTopologicalRing C] [IsLinearTopology C C]
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    {D : QuotientSystem B S hS A} {E : QuotientSystem B S hS C} (hE : E.HasLargeSite)
    (φ : ContinuousHom D E) (hφ : RingHom.IsTaut φ.toRingHom) :
    (MorphismProperty.inverseImage (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (formalSpectrumMap hA φ)

AlgebraicGeometry.FormalSpace.isRepresentableByAlgebraicSpacesULift_formalSpectrumMap_of_isTaut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautFormalSpectrumRepresentable.lean, line 206. The attribute's comment: “(3) implies (1)”.

Stacks 0AN5, the implication from its condition (3) to its condition (1). Let φ : A ⟶ C be a continuous homomorphism of weakly admissible topological rings over S whose underlying ring map is taut, which is condition (3) of Stacks 0AN5. Then Spf φ : Spf C ⟶ Spf A is representable by algebraic spaces over S, which is its condition (1).

The hypothesis hE is the condition of Stacks 0AIF that the site contain the coproduct of the quotient spectra of C, under which Spf C is an affine formal algebraic space; it enters only as the uniform size bound on those quotient spectra which puts the base change over a non-quasi-compact point of Spf A back in the site. Nothing is assumed about the stages of Spf A.

theorem isRepresentableByAlgebraicSpacesULift_formalSpectrumMap_of_isTaut
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (hE : E.HasLargeSite)
    (f : ContinuousHom D E) (hf : RingHom.IsTaut f.toRingHom) :
    Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (formalSpectrumMap hA f).hom

AlgebraicGeometry.FormalSpace.formalSpectrumMap_tfae_of_isAffineFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautFormalSpectrumTfae.lean, line 271. The attribute's comment: “the equivalence of (1), (2) and (3), with Spf(B) an affine formal algebraic space as in Definition 0AIF”.

Stacks 0AN5. Let S be a scheme and φ : A ⟶ C a continuous homomorphism of weakly admissible topological rings over S, the formal spectrum Spf C being an affine formal algebraic space as in Definition 0AIF. The following are equivalent:

Spf φ : Spf C ⟶ Spf A is representable by algebraic spaces;

Spf φ is representable (by objects of the site);

φ is taut.

The hypothesis hE. Definition 0AIF of the source defines Spf(B) to be "the affine formal algebraic space colim Spec(B/I)", and an affine formal algebraic space satisfies, by Definition 0AI7, the set-theoretic condition of Remark 0AIS; the source's proof of (1) ⟺ (2) is Lemma 0AKN, a statement about morphisms of affine formal algebraic spaces. In this library formalSpectrum E is the colimit alone, and hE records that it is an affine formal algebraic space in the sense of Definition 0AI7 (AlgebraicGeometry.IsAffineFormalAlgebraicSpace). This is the source's own notion of Spf(B), not an extra condition: for weakly admissible C it is equivalent to the coproduct of the stages lying in the site (AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_formalSpectrum_iff_hasLargeSite), the proviso of Remark 0AIE. Nothing is asked of Spf A, of the cutoff of the site, or of the stages of either ring.

Why it cannot be dropped. Over a site whose cutoff is singular there are taut homomorphisms with Spf φ not representable (AlgebraicGeometry.FormalSpace.exists_isTaut_not_relativelyRepresentable_of_cof_lt), and the formal spectrum of the target of such a homomorphism is not an affine formal algebraic space (AlgebraicGeometry.FormalSpace.exists_not_isAffineFormalAlgebraicSpace_formalSpectrum_of_cof_lt).

Proof. (1) ⟹ (3) is AlgebraicGeometry.FormalSpace.isTaut_of_isRepresentableByAlgebraicSpaces_formalSpectrumMap and (2) ⟹ (1) is AlgebraicGeometry.FormalSpace.isRepresentableByAlgebraicSpacesULift_formalSpectrumMap, both with no set-theoretic input. (3) ⟹ (2) is AlgebraicGeometry.FormalSpace.relative_isAffineHom_formalSpectrumMap_of_isTaut: a point of Spf A out of an affine object factors through a stage Spec(A/I) (Stacks 0AIA), over which the base change is Spec(C/J(I)) with J(I) the closure of φ(I)C, open by tautness; the charts over the affine opens of an arbitrary test object glue inside the site because each stage of Spf C is bounded by the coproduct of all of them, an object of the site by hE.

theorem formalSpectrumMap_tfae_of_isAffineFormalAlgebraicSpace
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C)
    (hE : IsAffineFormalAlgebraicSpace B S hS (formalSpectrum E)) (f : ContinuousHom D E) :
    List.TFAE
      [Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (formalSpectrumMap hA f).hom,
        (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
          (formalSpectrumMap hA f),
        RingHom.IsTaut f.toRingHom]

AlgebraicGeometry.FormalSpace.isTaut_of_isRepresentableByAlgebraicSpaces_formalSpectrumMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautFromRepresentable.lean, line 250. The attribute's comment: “(1) implies (3)”.

Stacks 0AN5, the implication from its condition (1) to its condition (3): if the formal spectrum of a continuous homomorphism φ : A ⟶ C of weakly admissible topological rings over S is representable by algebraic spaces, then φ is taut.

Only the base changes along the quotient stages of Spf A are needed, and those stages are affine, so what carries the step from condition (1) to condition (2) is Stacks 0AKN over the test objects of the site with affine underlying scheme, AlgebraicGeometry.FormalSpace.exists_affine_baseChange_of_isRepresentableByAlgebraicSpaces. That statement consumes of each of the two formal spectra only its presentation as a directed colimit of affine objects of the site along thickenings, and for a formal spectrum that presentation is its construction (AlgebraicGeometry.FormalSpace.hasThickeningPresentation_formalSpectrum). So nothing is assumed here beyond condition (1) — in particular no bound on the size of the site, which is what asking the two formal spectra to be affine formal algebraic spaces would amount to.

theorem isTaut_of_isRepresentableByAlgebraicSpaces_formalSpectrumMap
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
      (formalSpectrumMap hA f).hom) :
    RingHom.IsTaut f.toRingHom

AlgebraicGeometry.FormalSpace.isTaut_of_isClosedImmersionInto_formalSpectrumMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautFromRepresentable.lean, line 271. The attribute's comment: “(2) implies (3), for a closed immersion”.

A closed immersion of formal spectra of weakly admissible topological rings over S comes from a taut homomorphism: a closed immersion is representable, so Stacks 0AN5 applies.

theorem isTaut_of_isClosedImmersionInto_formalSpectrumMap
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (hf : IsClosedImmersionInto B S hS (formalSpectrumMap hA f)) :
    RingHom.IsTaut f.toRingHom

AlgebraicGeometry.FormalSpace.forall_formalSpectrumMap_tfae_iff_cutoff_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautNotRepresentable.lean, line 322. The attribute's comment: “the equivalence of (1), (2) and (3) for all weakly admissible rings holds over a site exactly when its cutoff is a regular cardinal”.

Stacks 0AN5 holds over a big fppf site exactly when its cutoff is regular. For a big fppf site B the following are equivalent:

for every scheme S of the site and every continuous homomorphism φ : A ⟶ C of weakly admissible topological rings over S, the three conditions of Stacks 0AN5 — Spf φ representable by algebraic spaces, Spf φ representable by objects of the site, φ taut — are equivalent;

the size cutoff of B is a regular cardinal.

Backwards this is AlgebraicGeometry.FormalSpace.formalSpectrumMap_tfae_of_cutoff_isRegular. Forwards, a cutoff which is not regular has cofinality below it, and then AlgebraicGeometry.FormalSpace.exists_not_tfae_formalSpectrumMap_of_cof_lt produces a taut homomorphism for which the equivalence fails.

theorem forall_formalSpectrumMap_tfae_iff_cutoff_isRegular :
    (∀ (S : Scheme.{u}) (hS : B.Contains S) (A : Type u) [CommRing A] [TopologicalSpace A]
      [IsTopologicalRing A] [IsLinearTopology A A] (C : Type u) [CommRing C]
      [TopologicalSpace C] [IsTopologicalRing C] [IsLinearTopology C C]
      (hA : TopologicalRing.IsWeaklyAdmissible A) (_ : TopologicalRing.IsWeaklyAdmissible C)
      (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E),
      List.TFAE
        [Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (formalSpectrumMap hA f).hom,
          (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
            (formalSpectrumMap hA f),
          RingHom.IsTaut f.toRingHom]) ↔ B.cutoff.IsRegular

AlgebraicGeometry.FormalSpace.exists_bigFppfSite_isTaut_not_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautNotRepresentable.lean, line 354. The attribute's comment: “false as stated over a site whose cutoff is singular: (3) does not imply (2)”.

Stacks 0AN5 is false as stated for some big fppf site. There are a big fppf site, a scheme S of it, and a continuous homomorphism φ : A ⟶ C of weakly admissible topological rings over S which is taut while Spf φ is not representable by objects of the site; so the three conditions of Stacks 0AN5 are not equivalent for it.

The site is the one of AlgebraicGeometry.BigFppfSite.exists_cutoff_eq with cutoff AlgebraicGeometry.singularCutoff = ℶ_{ω₁}, a singular cardinal satisfying every cardinal axiom of AlgebraicGeometry.BigFppfSite, and the homomorphism is the one of AlgebraicGeometry.FormalSpace.exists_isTaut_not_relativelyRepresentable_of_cof_lt. The statement holds, in the form of all three equivalences, over a site whose cutoff is regular (AlgebraicGeometry.FormalSpace.formalSpectrumMap_tfae_of_cutoff_isRegular) and for a countably indexed target over any site (AlgebraicGeometry.FormalSpace.formalSpectrumMap_tfae_of_isCountablyGenerated).

theorem exists_bigFppfSite_isTaut_not_relativelyRepresentable :
    ∃ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) (A : Type u) (_ : CommRing A)
      (_ : TopologicalSpace A) (_ : IsTopologicalRing A) (_ : IsLinearTopology A A)
      (C : Type u) (_ : CommRing C) (_ : TopologicalSpace C) (_ : IsTopologicalRing C)
      (_ : IsLinearTopology C C) (hA : TopologicalRing.IsWeaklyAdmissible A)
      (_ : TopologicalRing.IsWeaklyAdmissible C) (D : QuotientSystem B S hS A)
      (E : QuotientSystem B S hS C) (f : ContinuousHom D E),
      RingHom.IsTaut f.toRingHom ∧
        ¬ (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
          (formalSpectrumMap hA f) ∧
        ¬ List.TFAE
          [Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
              (formalSpectrumMap hA f).hom,
            (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
              (formalSpectrumMap hA f),
            RingHom.IsTaut f.toRingHom]

AlgebraicGeometry.FormalSpace.isTaut_of_relativelyRepresentable_formalSpectrumMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautOfRepresentable.lean, line 183. The attribute's comment: “(2) implies (3)”.

A continuous homomorphism φ : A ⟶ C of weakly admissible topological rings over S whose formal spectrum map is representable by objects of the site is taut.

theorem isTaut_of_relativelyRepresentable_formalSpectrumMap
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (hrep : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (formalSpectrumMap hA f)) :
    RingHom.IsTaut f.toRingHom

AlgebraicGeometry.FormalSpace.relativelyRepresentable_formalSpectrumMap_of_isTaut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautRepresentableBoundedStages.lean, line 358. The attribute's comment: “(3) implies (2), assuming the stages of the target are uniformly bounded by the site cutoff”.

Stacks 0AN5, the implication (3) ⟹ (2), under a uniform bound on the stages of the target. The representability half of AlgebraicGeometry.FormalSpace.relative_isAffineHom_formalSpectrumMap_of_isTaut_of_boundedStages: for a taut φ : A ⟶ C, if one cardinal below the cutoff bounds the sizes of all the stages Spec (C ⧸ K) of Spf C, then Spf φ is representable by schemes.

The named hypothesis is not a consequence of the axioms of AlgebraicGeometry.BigFppfSite; see the module docstring. Sufficient forms of it are AlgebraicGeometry.FormalSpace.QuotientSystem.HasLargeSite for the quotient system of C, the side condition of AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_formalSpectrum; a fundamental system of weak ideals of definition of C indexed below the cofinality of the cutoff (AlgebraicGeometry.FormalSpace.iSup_stageSize_lt_cutoff_of_cofinal_lt_cof), of which a countable fundamental system is the case the cutoff's axioms always allow (AlgebraicGeometry.FormalSpace.iSup_stageSize_lt_cutoff_of_isCountablyGenerated); and (Spec (.of C)).size < B.cutoff, since every stage is a quotient of C. The last of these is the hypothesis AlgebraicGeometry.FormalSpace.hasLargeSite_of_mk_lt_cutoff consumes and it constrains #C, which the bound on the stages does not: if the weak ideals of definition of C have a smallest member K₀ then that supremum is (Spec (.of (C ⧸ K₀))).size whatever #C may be, by AlgebraicGeometry.FormalSpace.iSup_stageSize_lt_cutoff_of_cofinal_lt_cof at a one-point index type.

Dropping the hypothesis altogether is possible at the price of one on the site instead of on the rings; see AlgebraicGeometry.FormalSpace.relativelyRepresentable_formalSpectrumMap_of_cutoff_isRegular.

theorem relativelyRepresentable_formalSpectrumMap_of_isTaut
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (hf : RingHom.IsTaut f.toRingHom)
    (hstages : ⨆ K : { K : Ideal C // TopologicalRing.IsWeakIdealOfDefinition K },
      (Spec (.of (C ⧸ K.1))).size < B.cutoff) :
    (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (formalSpectrumMap hA f)

AlgebraicGeometry.FormalSpace.relativelyRepresentable_formalSpectrumMap_of_cutoff_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautRepresentableBoundedStages.lean, line 395. The attribute's comment: “(3) implies (2), over a site whose cutoff is a regular cardinal”.

Stacks 0AN5, the implication (3) ⟹ (2), over a site whose cutoff is a regular cardinal. Let φ : A ⟶ C be a taut continuous homomorphism of weakly admissible topological rings over S. If the size cutoff of the site is a regular cardinal then Spf φ is representable by schemes, with no hypothesis on A or C beyond the ones Stacks 0AN5 states.

What the glueing of the charts over the affine opens of a test object T needs is that the scheme they glue to lie in the site. There are at most size T affine opens (AlgebraicGeometry.Scheme.mk_affineOpens_le_size), so a regular cutoff, being its own cofinality, makes the cofinality hypothesis of AlgebraicGeometry.BigFppfSite.contains_of_openCover automatic and asks nothing of the charts beyond their lying in the site, which they do — this is AlgebraicGeometry.BigFppfSite.contains_of_openCover_affineOpens_of_isRegular. So the stages of C may be of unbounded size.

Regularity is exactly the containment at stake, not merely one sufficient condition for it, and at the very index shape used here: the containment of every scheme covered by the images of open immersions from objects of the site indexed by the affine opens of an object of the site holds for all such coverings if and only if the cutoff is regular (AlgebraicGeometry.BigFppfSite.isRegular_cutoff_iff_contains_of_openCover_affineOpens). The same is true of the coproducts of the families of objects of the site indexed below the cutoff (AlgebraicGeometry.BigFppfSite.isRegular_cutoff_iff_contains_sigma), and such a cutoff is inaccessible (AlgebraicGeometry.BigFppfSite.isInaccessible_cutoff_of_contains_sigma). It is therefore not available from the axioms of AlgebraicGeometry.BigFppfSite, which a singular cutoff satisfies (AlgebraicGeometry.exists_cutoff_isSingular, AlgebraicGeometry.exists_bigFppfSite_family_not_contains_sigma).

theorem relativelyRepresentable_formalSpectrumMap_of_cutoff_isRegular
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (hf : RingHom.IsTaut f.toRingHom) (hreg : B.cutoff.IsRegular) :
    (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (formalSpectrumMap hA f)

AlgebraicGeometry.FormalSpace.formalSpectrumMap_tfae_of_cutoff_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautRepresentableBoundedStages.lean, line 459. The attribute's comment: “the equivalence of (1), (2) and (3), over a site whose cutoff is a regular cardinal”.

Stacks 0AN5 over a site whose cutoff is a regular cardinal: conditions (1), (2) and (3) are equivalent. Let φ : A ⟶ C be a continuous homomorphism of weakly admissible topological rings over S and suppose the size cutoff of the site is a regular cardinal. Then the following are equivalent:

Spf φ is representable by algebraic spaces over S;

Spf φ is representable by objects of the site;

φ is taut.

This is Stacks 0AN5 at its own hypotheses on the rings — two weakly admissible topological rings and a continuous homomorphism, no countability and no bound on the stages. The regularity of the cutoff is a condition on the ambient site, which the tag does not speak of; it is the exact containment the glueing of the charts of condition (2) needs (AlgebraicGeometry.BigFppfSite.isRegular_cutoff_iff_contains_of_openCover_affineOpens) and it is not implied by the axioms of AlgebraicGeometry.BigFppfSite. Only the step (3) ⟹ (2), AlgebraicGeometry.FormalSpace.relativelyRepresentable_formalSpectrumMap_of_cutoff_isRegular, uses it.

theorem formalSpectrumMap_tfae_of_cutoff_isRegular
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (hreg : B.cutoff.IsRegular) :
    List.TFAE
      [Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (formalSpectrumMap hA f).hom,
        (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
          (formalSpectrumMap hA f),
        RingHom.IsTaut f.toRingHom]

AlgebraicGeometry.FormalSpace.relativelyRepresentable_formalSpectrumMap_of_isCountablyGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautRepresentableBoundedStages.lean, line 538. The attribute's comment: “(3) implies (2), for a countably indexed target”.

Stacks 0AN5, the implication (3) ⟹ (2) for a countably indexed target, with no side condition. If the neighbourhood filter of 0 in C is countably generated and φ : A ⟶ C is taut, then Spf φ is representable by schemes.

The side condition of AlgebraicGeometry.FormalSpace.relativelyRepresentable_formalSpectrumMap_of_isTaut is discharged by AlgebraicGeometry.FormalSpace.iSup_stageSize_lt_cutoff_of_isCountablyGenerated. Nothing is assumed about A, and nothing about the site.

theorem relativelyRepresentable_formalSpectrumMap_of_isCountablyGenerated
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (hf : RingHom.IsTaut f.toRingHom) (hc : (nhds (0 : C)).IsCountablyGenerated) :
    (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (formalSpectrumMap hA f)

AlgebraicGeometry.FormalSpace.formalSpectrumMap_tfae_of_isCountablyGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautRepresentableBoundedStages.lean, line 561. The attribute's comment: “the equivalence of (1), (2) and (3), for a countably indexed target”.

Stacks 0AN5 for a countably indexed target: conditions (1), (2) and (3) are equivalent. Let φ : A ⟶ C be a continuous homomorphism of weakly admissible topological rings over S and suppose the neighbourhood filter of 0 in C is countably generated. Then the following are equivalent:

Spf φ is representable by algebraic spaces over S;

Spf φ is representable by objects of the site;

φ is taut.

Only the step (3) ⟹ (2), AlgebraicGeometry.FormalSpace.relativelyRepresentable_formalSpectrumMap_of_isCountablyGenerated, uses the countability hypothesis; the other two arrows are the unconditional ones of AlgebraicGeometry.FormalSpace.formalSpectrumMap_tfae_of_imp_relativelyRepresentable.

theorem formalSpectrumMap_tfae_of_isCountablyGenerated
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (hc : (nhds (0 : C)).IsCountablyGenerated) :
    List.TFAE
      [Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (formalSpectrumMap hA f).hom,
        (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
          (formalSpectrumMap hA f),
        RingHom.IsTaut f.toRingHom]

Tag 0AKP, a lemma

Tag 0AKP in the Stacks Project.

AlgebraicGeometry.isAffineFormalAlgebraicSpace_of_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/RepresentableAffine.lean, line 99. The attribute's comment: “affine_source”.

The source of a representable affine map of fppf sheaves to an affine formal algebraic space is an affine formal algebraic space.

theorem isAffineFormalAlgebraicSpace_of_affine
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))}
    (f : X ⟶ Y)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y)
    (hf : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda
        (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) f) :
    IsAffineFormalAlgebraicSpace B S hS X

AlgebraicGeometry.isCountablyIndexed_of_affine', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/RepresentableAffine.lean, line 204. The attribute's comment: “countably_indexed_source”.

The source of a representable affine map to a countably indexed sheaf is countably indexed.

theorem isCountablyIndexed_of_affine'
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))}
    (f : X ⟶ Y)
    (hf : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda
        (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (hY_countable : FormalSpace.IsCountablyIndexed B S hS Y) :
    FormalSpace.IsCountablyIndexed B S hS X

AlgebraicGeometry.FormalSpace.isCountablyIndexed_of_relative_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffinePullbackPresentation.lean, line 295. The attribute's comment: “countably_indexed_source”.

The source of a representable affine morphism of fppf sheaves whose target is countably indexed is itself countably indexed.

theorem isCountablyIndexed_of_relative_isAffineHom
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (hY : IsCountablyIndexed B S hS Y) :
    IsCountablyIndexed B S hS X

AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_of_relative_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineSource.lean, line 165. The attribute's comment: “affine_source”.

Stacks 0AKP, part (1). The source of a representable affine morphism of fppf sheaves whose target is an affine formal algebraic space is itself an affine formal algebraic space.

theorem isAffineFormalAlgebraicSpace_of_relative_isAffineHom
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y) :
    IsAffineFormalAlgebraicSpace B S hS X

AlgebraicGeometry.FormalSpace.isCountablyIndexedAndClassical_of_relative_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineSourceTypes.lean, line 194. The attribute's comment: “classical_source”.

Stacks 0AKP, part (3). The source of a representable affine morphism of fppf sheaves whose target is a countably indexed and classical affine formal algebraic space is itself countably indexed and classical.

Countable indexing of the source is part (2) of the same tag. For the classical half the morphism is the formal spectrum of a continuous taut homomorphism of presenting rings, and pre-admissibility ascends along such a homomorphism by Stacks 0GX8; the presenting ring of the source is complete and separated, being weakly admissible.

theorem isCountablyIndexedAndClassical_of_relative_isAffineHom
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (hY : IsCountablyIndexed B S hS Y ∧ IsClassical B S hS Y) :
    IsCountablyIndexed B S hS X ∧ IsClassical B S hS X

AlgebraicGeometry.FormalSpace.isWeaklyAdic_of_relative_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineSourceTypes.lean, line 220. The attribute's comment: “weakly_adic_source”.

Stacks 0AKP, part (4). The source of a representable affine morphism of fppf sheaves whose target is a weakly adic affine formal algebraic space is itself weakly adic.

A weakly adic affine formal algebraic space is countably indexed by item (5) of Stacks 0AIK, so the morphism is the formal spectrum of a continuous taut homomorphism of presenting rings; weak pre-adicness ascends along such a homomorphism by Stacks 0GXI, and the presenting ring of the source is complete and separated, being weakly admissible.

theorem isWeaklyAdic_of_relative_isAffineHom
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (hY : IsWeaklyAdic B S hS Y) :
    IsWeaklyAdic B S hS X

AlgebraicGeometry.FormalSpace.isAdicStar_of_relative_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineSourceTypes.lean, line 252. The attribute's comment: “adic_star_source”.

Stacks 0AKP, part (5). The source of a representable affine morphism of fppf sheaves whose target is an adic* affine formal algebraic space is itself adic*.

An adic* affine formal algebraic space is countably indexed by items (2) and (3) and (5) of Stacks 0AIK, so the morphism is the formal spectrum of a continuous taut homomorphism of presenting rings; Stacks 0APU makes the target of such a homomorphism adic with a finitely generated ideal of definition as soon as its source is and the target is complete and separated, which the presenting ring of the source is, being weakly admissible. The finitely generated ideal of definition the hypothesis supplies defines the topology adically because the ring is pre-adic.

theorem isAdicStar_of_relative_isAffineHom
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (hY : IsAdicStar B S hS Y) :
    IsAdicStar B S hS X

AlgebraicGeometry.FormalSpace.isNoetherian_of_relative_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineSourceTypes.lean, line 291. The attribute's comment: “noetherian_source”.

Stacks 0AKP, part (6). The source of a representable affine morphism of fppf sheaves which is locally of finite type and whose target is a Noetherian affine formal algebraic space is itself Noetherian.

A Noetherian affine formal algebraic space is countably indexed by items (1), (2), (3) and (5) of Stacks 0AIK, so the morphism is the formal spectrum of a continuous taut homomorphism φ : A → C of presenting rings. An ideal of definition of the Noetherian ring A is finitely generated, so Stacks 0APU produces a finitely generated ideal J ⊆ C defining the topology of C adically; C is then J-adically complete, and Stacks 05GH reduces Noetherianness of C to that of C ⧸ J. The closed extended ideals form a fundamental system of neighbourhoods of zero by tautness, so J contains the closure J(I) of I C for a weak ideal of definition I ⊆ A; the stage half of Stacks 0ANT makes A ⧸ I → C ⧸ J(I) of finite type, hence C ⧸ J(I) Noetherian, and C ⧸ J is a quotient of it.

theorem isNoetherian_of_relative_isAffineHom
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hY : IsNoetherian B S hS Y) :
    IsNoetherian B S hS X

AlgebraicGeometry.FormalSpace.isCountablyIndexed_and_isClassical_of_relative_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeDescentAlongAffine.lean, line 148. The attribute's comment: “classical_source”.

Stacks 0AKP, part (3). The source of a representable affine morphism of fppf sheaves whose target is a countably indexed classical affine formal algebraic space is itself countably indexed and classical.

Countable indexing passes to the source by part (2) of Stacks 0AKP, and admissibility of the presenting ring ascends along the taut homomorphism inducing the morphism, by Stacks 0GX8.

theorem isCountablyIndexed_and_isClassical_of_relative_isAffineHom
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (hYc : IsCountablyIndexed B S hS Y) (hYcl : IsClassical B S hS Y) :
    IsCountablyIndexed B S hS X ∧ IsClassical B S hS X

AlgebraicGeometry.FormalSpace.isNoetherian_of_relative_isAffineHom', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeDescentAlongAffine.lean, line 175. The attribute's comment: “noetherian_source”. References: EGA I (10.13.2), “special case”.

Stacks 0AKP, part (6). The source of a representable affine morphism of fppf sheaves which is locally of finite type and whose target is a Noetherian affine formal algebraic space is itself Noetherian.

By the equivalence of conditions (1) and (3) of Stacks 0AKM a Noetherian affine formal algebraic space is an adic* one with a presentation by Noetherian affine schemes. Part (5) above gives the first half for the source, and the presentation pulls back to a Noetherian one because each stage of the source is of finite type over the corresponding Noetherian stage of the target.

theorem isNoetherian_of_relative_isAffineHom'
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hYn : IsNoetherian B S hS Y) :
    IsNoetherian B S hS X

AlgebraicGeometry.FormalSpace.isAdicStar_of_relative_isAffineHom', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeDescentAlongAffine.lean, line 200. The attribute's comment: “adic_star_source”.

Stacks 0AKP, part (5). The source of a representable affine morphism of fppf sheaves whose target is an adic* affine formal algebraic space is itself adic*.

The powers of an ideal of definition of an adic ring are a fundamental system of open ideals, so the target is countably indexed and part (2) of Stacks 0AKP carries that to the source. The presenting ring of the source is complete and separated, so by Stacks 0APU the taut homomorphism inducing the morphism makes it adic with a finitely generated ideal of definition.

theorem isAdicStar_of_relative_isAffineHom'
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (hYa : IsAdicStar B S hS Y) :
    IsAdicStar B S hS X

AlgebraicGeometry.FormalSpace.isWeaklyAdic_of_relative_isAffineHom', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeDescentAlongAffine.lean, line 231. The attribute's comment: “weakly_adic_source”.

Stacks 0AKP, part (4). The source of a representable affine morphism of fppf sheaves whose target is a weakly adic affine formal algebraic space is itself weakly adic.

A weakly adic ring has the closed powers of a single ideal as a fundamental system of open ideals, so the target is countably indexed and part (2) of Stacks 0AKP carries that to the source; weak pre-adicness of the presenting ring then ascends along the taut homomorphism inducing the morphism, by Stacks 0GXI.

theorem isWeaklyAdic_of_relative_isAffineHom'
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (hYw : IsWeaklyAdic B S hS Y) :
    IsWeaklyAdic B S hS X

Tag 0AKQ, a lemma

Tag 0AKQ in the Stacks Project.

AlgebraicGeometry.FormalSpace.isCountablyIndexed_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransfer.lean, line 341. The attribute's comment: “clause (1); Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces and parts (1) and (2) of Stacks 0AKP are the library's isAffineFormalAlgebraicSpace_of_relative_isAffineHom and isCountablyIndexed_of_relative_isAffineHom”.

Stacks 0AKQ, clause (1). Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces. If Y is countably indexed then so is X.

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

AlgebraicGeometry.FormalSpace.isCountablyIndexedAndClassical_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransfer.lean, line 356. The attribute's comment: “clause (2); Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces and clause (3) of Stacks 0AKP is the library's isCountablyIndexedAndClassical_of_relative_isAffineHom”.

Stacks 0AKQ, clause (2). Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces. If Y is countably indexed and classical then so is X.

theorem isCountablyIndexedAndClassical_of_isRepresentable {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (hYc : IsCountablyIndexed B S hS Y ∧ IsClassical B S hS Y) :
    IsCountablyIndexed B S hS X ∧ IsClassical B S hS X

AlgebraicGeometry.FormalSpace.isWeaklyAdic_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransfer.lean, line 371. The attribute's comment: “clause (3); Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces and clause (4) of Stacks 0AKP is the library's isWeaklyAdic_of_relative_isAffineHom”.

Stacks 0AKQ, clause (3). Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces. If Y is weakly adic then so is X.

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

AlgebraicGeometry.FormalSpace.isAdicStar_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransfer.lean, line 386. The attribute's comment: “clause (4); Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces and clause (5) of Stacks 0AKP is the library's isAdicStar_of_relative_isAffineHom”.

Stacks 0AKQ, clause (4). Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces. If Y is adic* then so is X.

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

AlgebraicGeometry.FormalSpace.isNoetherian_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransfer.lean, line 401. The attribute's comment: “clause (5); Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces and clause (6) of Stacks 0AKP is the library's isNoetherian_of_relative_isAffineHom”.

Stacks 0AKQ, clause (5). Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces and locally of finite type. If Y is Noetherian then so is X.

theorem isNoetherian_of_isRepresentable {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hYc : IsNoetherian B S hS Y) :
    IsNoetherian B S hS X

AlgebraicGeometry.FormalSpace.isCountablyIndexed_of_isRepresentable', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransferRefined.lean, line 74. The attribute's comment: “clause (1); Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces and parts (1) and (2) of Stacks 0AKP are the library's isAffineFormalAlgebraicSpace_of_relative_isAffineHom and isCountablyIndexed_of_relative_isAffineHom”.

Stacks 0AKQ, clause (1). Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces. If Y is countably indexed then so is X.

alias isCountablyIndexed_of_isRepresentable'

AlgebraicGeometry.FormalSpace.isCountablyIndexedAndClassical_of_isRepresentable', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransferRefined.lean, line 82. The attribute's comment: “clause (2); Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces and clause (3) of Stacks 0AKP is the library's isCountablyIndexedAndClassical_of_relative_isAffineHom”.

Stacks 0AKQ, clause (2). Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces. If Y is countably indexed and classical then so is X.

alias isCountablyIndexedAndClassical_of_isRepresentable'

AlgebraicGeometry.FormalSpace.isWeaklyAdic_of_isRepresentable', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransferRefined.lean, line 91. The attribute's comment: “clause (3); Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces and clause (4) of Stacks 0AKP is the library's isWeaklyAdic_of_relative_isAffineHom”.

Stacks 0AKQ, clause (3). Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces. If Y is weakly adic then so is X.

alias isWeaklyAdic_of_isRepresentable'

AlgebraicGeometry.FormalSpace.isAdicStar_of_isRepresentable', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransferRefined.lean, line 99. The attribute's comment: “clause (4); Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces and clause (5) of Stacks 0AKP is the library's isAdicStar_of_relative_isAffineHom”.

Stacks 0AKQ, clause (4). Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces. If Y is adic* then so is X.

alias isAdicStar_of_isRepresentable'

AlgebraicGeometry.FormalSpace.isNoetherian_of_isRepresentable', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransferRefined.lean, line 107. The attribute's comment: “clause (5); Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces and clause (6) of Stacks 0AKP is the library's isNoetherian_of_relative_isAffineHom”.

Stacks 0AKQ, clause (5). Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces and locally of finite type. If Y is Noetherian then so is X.

alias isNoetherian_of_isRepresentable'

Tag 0AN6, an example

Tag 0AN6 in the Stacks Project.

TopologicalRing.CompletionOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 74. The attribute's comment: “completion_over”.

The completion of A over B is the inverse limit, over the weak ideals of definition J of B, of the rings A / JA.

public def CompletionOver {B : Type u} {A : Type v} [CommRing B] [CommRing A]
    [TopologicalSpace B] (f : B →+* A) :
    Subring (∀ J : WeakIdealOfDefinitionIndex B, A ⧸ extendedIdeal f J)

TopologicalRing.CompletionOver.limitTopology, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 90. The attribute's comment: “completion_over”.

The inverse-limit topology on the completion over B, with every quotient ring in the defining inverse system carrying the discrete topology.

public noncomputable instance limitTopology {B : Type u} {A : Type v} [CommRing B]
    [CommRing A] [TopologicalSpace B] (f : B →+* A) :
    TopologicalSpace (CompletionOver f)

TopologicalRing.CompletionOver.canonicalMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 114. The attribute's comment: “completion_over”.

The canonical ring homomorphism from B to the completion of A over B.

public def canonicalMap {B : Type u} {A : Type v} [CommRing B] [CommRing A]
    [TopologicalSpace B] (f : B →+* A) : B →+* CompletionOver f

TopologicalRing.CompletionOver.projection_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 211. The attribute's comment: “kernel_closure”.

Every projection from the relative completion to a defining quotient is surjective.

public theorem projection_surjective {B : Type u} {A : Type v} [CommRing B] [CommRing A]
    [TopologicalSpace B] (f : B →+* A) (J : WeakIdealOfDefinitionIndex B) :
    Function.Surjective (projection f J)

TopologicalRing.CompletionOver.isOpen_ker_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 220. The attribute's comment: “kernel_closure”.

The kernel of a projection from the relative completion is open.

public theorem isOpen_ker_projection {B : Type u} {A : Type v} [CommRing B] [CommRing A]
    [TopologicalSpace B] (f : B →+* A) (J : WeakIdealOfDefinitionIndex B) :
    IsOpen (RingHom.ker (projection f J) : Set (CompletionOver f))

TopologicalRing.CompletionOver.ker_projection_eq_closure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 233. The attribute's comment: “kernel_closure”.

The kernel of a projection from the relative completion is the closure of the ideal extended from the corresponding weak ideal of definition of the base ring.

public theorem ker_projection_eq_closure {B : Type u} {A : Type v} [CommRing B] [CommRing A]
    [TopologicalSpace B] (f : B →+* A) (J : WeakIdealOfDefinitionIndex B) :
    RingHom.ker (projection f J) = Ideal.closure (J.1.map (canonicalMap f))

TopologicalRing.projection_ker_isWeakIdealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 340. The attribute's comment: “weakly_admissible”.

The kernel of every projection to A / JA is a weak ideal of definition of the completion.

public theorem projection_ker_isWeakIdealOfDefinition (f : B →+* A)
    (J : WeakIdealOfDefinitionIndex B) :
    TopologicalRing.IsWeakIdealOfDefinition (RingHom.ker (projection f J))

TopologicalRing.completionOver_isWeaklyAdmissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 382. The attribute's comment: “weakly_admissible”.

Completion over a weakly admissible topological ring is weakly admissible.

public theorem completionOver_isWeaklyAdmissible (f : B →+* A)
    (hB : TopologicalRing.IsWeaklyAdmissible B) :
    TopologicalRing.IsWeaklyAdmissible (CompletionOver f)

TopologicalRing.completeSpace_completionOver, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 414. The attribute's comment: “complete_linearly_topologized”.

The completion over a ring is complete for its canonical additive uniformity.

public noncomputable instance completeSpace_completionOver (f : B →+* A) :
    @CompleteSpace (CompletionOver f)
      (IsTopologicalAddGroup.rightUniformSpace (CompletionOver f))

TopologicalRing.t2Space_completionOver, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 441. The attribute's comment: “complete_linearly_topologized”.

The inverse-limit topology on the completion is separated.

public noncomputable instance t2Space_completionOver (f : B →+* A) :
    T2Space (CompletionOver f)

TopologicalRing.continuous_canonicalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 462. The attribute's comment: “taut”.

The canonical map to the completion over a topological ring is continuous.

public theorem continuous_canonicalMap {B : Type u} {A : Type v}
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [CommRing A]
    (f : B →+* A) : Continuous (canonicalMap f)

TopologicalRing.isTaut_canonicalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 492. The attribute's comment: “taut”.

The canonical map to the completion over a weakly preadmissible ring is taut.

public theorem isTaut_canonicalMap {B : Type u} {A : Type v}
    [CommRing B] [TopologicalSpace B] [CommRing A]
    (f : B →+* A) (hB : TopologicalRing.IsWeaklyPreAdmissible B) :
    RingHom.IsTaut (canonicalMap f)

Declarations registered for the tag:

TopologicalRing.completionOverIsLinearTopology, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 408 (StacksFrontier): “complete_linearly_topologized”.

Tag 0AN7, a remark

Tag 0AN7 in the Stacks Project.

TopologicalRing.not_isTaut_constantsToTAdicPowerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SharpnessOfRepresentability.lean, line 186. The attribute's comment: “first sense, the example only: for A = k a field with the discrete topology and B = k⟦t⟧ with the t-adic topology, the inclusion of constants is a continuous homomorphism of weakly admissible topological rings (isWeaklyAdmissible_discreteTopology, isWeaklyAdmissible_tAdicPowerSeries, continuous_constantsToTAdicPowerSeries) which is not taut. That Spf of it is therefore not representable is the implication (1) ⟹ (3) of Stacks 0AN5, which this library does not prove; it is an explicit hypothesis of AlgebraicGeometry.FormalSpace.not_isRepresentableByAlgebraicSpaces_formalSpectrumMap_constants”.

Stacks 0AN7, the example for its first sense, at the level of rings. Let k be a field with the discrete topology and let k⟦t⟧ carry the t-adic topology. The inclusion of constants is a continuous homomorphism of weakly admissible topological rings which is not taut: the zero ideal of k is open, its extension to k⟦t⟧ is the zero ideal and is closed because k⟦t⟧ is separated, and the zero ideal of k⟦t⟧ is not open.

theorem not_isTaut_constantsToTAdicPowerSeries (k : Type u) [Field k] [TopologicalSpace k]
    [DiscreteTopology k] : ¬ RingHom.IsTaut (constantsToTAdicPowerSeries k)

AlgebraicGeometry.FormalSpace.not_isRepresentableByAlgebraicSpaces_formalSpectrumMap_constants, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SharpnessOfRepresentability.lean, line 240. The attribute's comment: “first sense, the non-representability itself, conditional on the explicit hypothesis IsTautOfRepresentableFormalSpectrumMap, which is the implication (1) ⟹ (3) of Stacks 0AN5 and is not proved in this library. The example is the one of the source: k a field with the discrete topology, k⟦t⟧ with the t-adic topology, and the inclusion of constants, whose non-tautness is TopologicalRing.not_isTaut_constantsToTAdicPowerSeries. The second sense of the remark, that the source of a representable morphism onto a McQuillan formal spectrum need not be McQuillan, is not proved here”.

Stacks 0AN7, its first sense. Let k be a field with the discrete topology, let k⟦t⟧ carry the t-adic topology, and let Spf (φ) : Spf k⟦t⟧ ⟶ Spf k be the formal spectrum of the inclusion of constants, taken over any base and any quotient systems presenting the two formal spectra. Then Spf (φ) is not representable by algebraic spaces, granted the implication (1) ⟹ (3) of Stacks 0AN5: the inclusion of constants is not taut. Both rings are weakly admissible, by TopologicalRing.isWeaklyAdmissible_discreteTopology and TopologicalRing.isWeaklyAdmissible_tAdicPowerSeries.

theorem not_isRepresentableByAlgebraicSpaces_formalSpectrumMap_constants
    (k : Type u) [Field k] [TopologicalSpace k] [DiscreteTopology k]
    (h0AN5 : IsTautOfRepresentableFormalSpectrumMap B S hS)
    (D : QuotientSystem B S hS k)
    (E : QuotientSystem B S hS (TopologicalRing.TAdicPowerSeries k))
    (f : ContinuousHom D E)
    (hf : f.toRingHom = TopologicalRing.constantsToTAdicPowerSeries k) :
    ¬ Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
      (formalSpectrumMap (TopologicalRing.isWeaklyAdmissible_discreteTopology k) f).hom

AlgebraicGeometry.FormalSpace.not_relativelyRepresentable_formalSpectrumMap_constants, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SharpnessOfRepresentabilityExamples.lean, line 115. The attribute's comment: “first sense, the non-representability itself in the reading of condition (2) of Stacks 0AN5 — representable, i.e. every base change along a point of Spf k out of an object of the site is again such an object — and with no hypothesis whatever: the implication (2) ⟹ (3) of Stacks 0AN5, AlgebraicGeometry.FormalSpace.isTaut_of_relativelyRepresentable_formalSpectrumMap, carries no side condition, so the non-tautness of the example (TopologicalRing.not_isTaut_constantsToTAdicPowerSeries) rules condition (2) out directly. The reading on condition (1), representability by algebraic spaces, is AlgebraicGeometry.FormalSpace.not_isRepresentableByAlgebraicSpaces_formalSpectrumMap_constants', which is unconditional as well. The concrete instance and the second sense of the remark are AlgebraicGeometry.FormalSpace.exists_formalSpectrumMap_constants_not_representable and AlgebraicGeometry.FormalSpace.exists_representable_formalSpectrum_not_mcQuillan”.

Stacks 0AN7, its first sense, read on condition (2) of Stacks 0AN5 and with no hypothesis whatever. Let k be a field with the discrete topology, let k⟦t⟧ carry the t-adic topology and let Spf (φ) : Spf k⟦t⟧ ⟶ Spf k be the formal spectrum of the inclusion of constants. Then Spf (φ) is not representable: some base change of it along a point of Spf k coming from an object of the site is not again such an object.

The implication (2) ⟹ (3) of Stacks 0AN5, AlgebraicGeometry.FormalSpace.isTaut_of_relativelyRepresentable_formalSpectrumMap, carries no side condition at all — only the base changes along the quotient stages are used, and condition (2) supplies those directly — so the non-tautness of the example rules out condition (2) outright. Ruling out the weaker condition (1), representability by algebraic spaces, needs the step from (1) to (2), which is Stacks 0AKN; that is AlgebraicGeometry.FormalSpace.not_isRepresentableByAlgebraicSpaces_formalSpectrumMap_constants', and it is unconditional too, the library's Stacks 0AKN consuming of a formal spectrum only its presentation by affine thickenings.

theorem not_relativelyRepresentable_formalSpectrumMap_constants
    (k : Type u) [Field k] [TopologicalSpace k] [DiscreteTopology k]
    (D : QuotientSystem B S hS k)
    (E : QuotientSystem B S hS (TopologicalRing.TAdicPowerSeries k))
    (f : ContinuousHom D E)
    (hf : f.toRingHom = TopologicalRing.constantsToTAdicPowerSeries k) :
    ¬ (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (formalSpectrumMap (TopologicalRing.isWeaklyAdmissible_discreteTopology k) f)

AlgebraicGeometry.FormalSpace.exists_formalSpectrumMap_constants_not_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SharpnessOfRepresentabilityExamples.lean, line 140. The attribute's comment: “(1): for A = k a field with the discrete topology and B = k⟦t⟧ with the t-adic topology, Spf (φ) : Spf(k⟦t⟧) → Spf(k) of the inclusion of constants is a morphism of affine formal algebraic spaces which is not representable, and not even representable by algebraic spaces”.

Stacks 0AN7 (1). Let k be a field with the discrete topology and let k⟦t⟧ carry the t-adic topology; both are weakly admissible and the inclusion of constants φ : k → k⟦t⟧ is continuous. Then, over the base S = Spec k of a suitable big fppf site, the formal spectra Spf k and Spf k⟦t⟧ are affine formal algebraic spaces and Spf (φ) : Spf k⟦t⟧ ⟶ Spf k is neither representable nor representable by algebraic spaces.

theorem exists_formalSpectrumMap_constants_not_representable
    (k : Type u) [Field k] [TopologicalSpace k] [DiscreteTopology k] :
    ∃ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
      (D : QuotientSystem B S hS k)
      (E : QuotientSystem B S hS (TopologicalRing.TAdicPowerSeries k))
      (f : ContinuousHom D E),
      f.toRingHom = TopologicalRing.constantsToTAdicPowerSeries k ∧
      IsAffineFormalAlgebraicSpace B S hS (formalSpectrum D) ∧
      IsAffineFormalAlgebraicSpace B S hS (formalSpectrum E) ∧
      ¬ (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
        (formalSpectrumMap (TopologicalRing.isWeaklyAdmissible_discreteTopology k) f) ∧
      ¬ Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
        (formalSpectrumMap (TopologicalRing.isWeaklyAdmissible_discreteTopology k) f).hom

AlgebraicGeometry.FormalSpace.exists_representable_formalSpectrum_not_mcQuillan, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SharpnessOfRepresentabilityExamples.lean, line 192. The attribute's comment: “(2): a representable morphism f : Y → X of affine formal algebraic spaces with X = Spf(A) McQuillan and Y not McQuillan, the example of Examples, Section 0ANY”.

Stacks 0AN7 (2). There are a weakly admissible topological ring A over a base S and a representable morphism f : Y ⟶ Spf A of affine formal algebraic spaces such that the target Spf A is McQuillan but the source Y is not. This is the example of Examples, Section 0ANY, i.e. Stacks 0CBE, with its McQuillan target identified with a formal spectrum. The source is not McQuillan in the sense of condition (4) of Stacks 0AIC, and not in the sense of condition (1) either: it is isomorphic to the formal spectrum of no weakly admissible topological ring.

theorem exists_representable_formalSpectrum_not_mcQuillan :
    ∃ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
      (A : Type u) (_ : CommRing A) (_ : TopologicalSpace A) (_ : IsTopologicalRing A)
      (_ : IsLinearTopology A A) (D : QuotientSystem B S hS A) (Y : FppfSheaf B S hS)
      (f : Y ⟶ formalSpectrum D),
      TopologicalRing.IsWeaklyAdmissible A ∧
      IsAffineFormalAlgebraicSpace B S hS Y ∧
      IsAffineFormalAlgebraicSpace B S hS (formalSpectrum D) ∧
      HasSomeSurjectivePresentation B S hS (formalSpectrum D) ∧
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable f ∧
      ¬ HasSomeSurjectivePresentation B S hS Y ∧
      ¬ ∃ (A' : Type u) (_ : CommRing A') (_ : TopologicalSpace A') (_ : IsTopologicalRing A')
        (_ : IsLinearTopology A' A') (D' : QuotientSystem B S hS A'),
        TopologicalRing.IsWeaklyAdmissible A' ∧ Nonempty (Y ≅ formalSpectrum D')

AlgebraicGeometry.FormalSpace.not_isRepresentableByAlgebraicSpaces_formalSpectrumMap_constants', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SharpnessOfRepresentabilityFirstSense.lean, line 82. The attribute's comment: “first sense, the non-representability itself. The example is the one of the source: k a field with the discrete topology, k⟦t⟧ with the t-adic topology, and the inclusion of constants, whose non-tautness is TopologicalRing.not_isTaut_constantsToTAdicPowerSeries. The second sense of the remark, that the source of a representable morphism onto a McQuillan formal spectrum need not be McQuillan, is not proved here”.

Stacks 0AN7, its first sense. Let k be a field with the discrete topology, let k⟦t⟧ carry the t-adic topology, and let Spf (φ) : Spf k⟦t⟧ ⟶ Spf k be the formal spectrum of the inclusion of constants, taken over any base and any quotient systems presenting the two formal spectra. Then Spf (φ) is not representable by algebraic spaces: by the implication (1) ⟹ (3) of Stacks 0AN5 it would be taut, and the inclusion of constants is not. Both rings are weakly admissible, by TopologicalRing.isWeaklyAdmissible_discreteTopology and TopologicalRing.isWeaklyAdmissible_tAdicPowerSeries, and both carry a countable fundamental system of neighbourhoods of 0 — the discrete one trivially, the t-adic one by the powers of (t) — which is what gives the two quotient systems the set-theoretic condition that the implication (1) ⟹ (3) asks for. This is AlgebraicGeometry.FormalSpace.not_isRepresentableByAlgebraicSpaces_formalSpectrumMap_constants with its hypothesis h0AN5 discharged at the two quotient systems of the example.

theorem not_isRepresentableByAlgebraicSpaces_formalSpectrumMap_constants'
    (k : Type u) [Field k] [TopologicalSpace k] [DiscreteTopology k]
    (D : QuotientSystem B S hS k)
    (E : QuotientSystem B S hS (TopologicalRing.TAdicPowerSeries k))
    (f : ContinuousHom D E)
    (hf : f.toRingHom = TopologicalRing.constantsToTAdicPowerSeries k) :
    ¬ Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
      (formalSpectrumMap (TopologicalRing.isWeaklyAdmissible_discreteTopology k) f).hom

Tag 0AN8, a lemma

Tag 0AN8 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isEssentiallySurjectiveSpf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EssentiallySurjectiveSpf.lean, line 178. The attribute's comment: “essential surjectivity, and only for a quotient system satisfying the site condition of Stacks 0AIF, that the site hold the atlas of quotient spectra: the source leaves that condition implicit, its sites being indexed by a cutoff it may enlarge, and a quotient system by itself places only the individual quotient spectra in the site, not their coproduct. Nothing is asked of the coefficient ring beyond the source's own hypotheses”.

Essential surjectivity of Spf on étale algebras. For a McQuillan affine formal algebraic space Spf R over S, every affine formal algebraic space V over S carrying a morphism V ⟶ Spf R which is representable by algebraic spaces and étale is Spf of the completion A^∧ of an étale R-algebra A, compatibly with the morphisms to Spf R.

theorem isEssentiallySurjectiveSpf : IsEssentiallySurjectiveSpf' 𝔅 S hS

AlgebraicGeometry.FormalSpace.etaleFormalSpectrum_correspondence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleCompletionSpectrum.lean, line 899.

Stacks 0AN8. Let Y = Spf R be a McQuillan affine formal algebraic space over S, for a weakly admissible topological ring R. Sending the completion A^∧ = lim A ⧸ JA of an étale R-algebra A to Spf A^∧ ⟶ Y is an equivalence between the opposite of the category of such completions and the category of morphisms X ⟶ Y of affine formal algebraic spaces which are representable by algebraic spaces and étale:

the functor is well defined: Spf A^∧ ⟶ Spf R is representable by algebraic spaces and étale;

it is fully faithful: a morphism Spf A₁^∧ ⟶ Spf A₂^∧ over Spf R is Spf of a unique continuous R-algebra map A₂^∧ → A₁^∧;

it is essentially surjective: every affine formal algebraic space X with a morphism X ⟶ Spf R representable by algebraic spaces and étale is, over Spf R, the formal spectrum of the completion of an étale R-algebra; in particular X is McQuillan.

The hypothesis that Spf R is an affine formal algebraic space is part of Y being a McQuillan affine formal algebraic space; only the third clause uses it.

theorem etaleFormalSpectrum_correspondence (hR : TopologicalRing.IsWeaklyAdmissible R)
    (D : QuotientSystem 𝔅 S hS R)
    (hY : IsAffineFormalAlgebraicSpace 𝔅 S hS (formalSpectrum D)) :
    (∀ {A : Type u} [CommRing A] (f : R →+* A), f.Etale →
      ∀ (E : QuotientSystem 𝔅 S hS (TopologicalRing.CompletionOver f)) (g : ContinuousHom D E),
        g.toRingHom = TopologicalRing.CompletionOver.canonicalMap f →
          IsRepresentableEtale 𝔅 S hS (formalSpectrumMap hR g)) ∧
    (∀ {A₁ A₂ : Type u} [CommRing A₁] [CommRing A₂] {f₁ : R →+* A₁} {f₂ : R →+* A₂}
      {E₁ : QuotientSystem 𝔅 S hS (TopologicalRing.CompletionOver f₁)}
      {E₂ : QuotientSystem 𝔅 S hS (TopologicalRing.CompletionOver f₂)}
      (g₁ : ContinuousHom D E₁) (g₂ : ContinuousHom D E₂)
      (φ : formalSpectrum E₁ ⟶ formalSpectrum E₂),
        φ ≫ formalSpectrumMap hR g₂ = formalSpectrumMap hR g₁ →
          ∃! h : ContinuousHom E₂ E₁, formalSpectrumMap
            (TopologicalRing.completionOver_isWeaklyAdmissible f₂ hR) h = φ ∧
              h.toRingHom.comp g₂.toRingHom = g₁.toRingHom) ∧
    (∀ {X : FppfSheaf 𝔅 S hS}, IsAffineFormalAlgebraicSpace 𝔅 S hS X →
      ∀ p : X ⟶ formalSpectrum D, IsRepresentableEtale 𝔅 S hS p →
        ∃ (A : Type u) (_ : CommRing A) (f : R →+* A), f.Etale ∧
          ∃ (E : QuotientSystem 𝔅 S hS (TopologicalRing.CompletionOver f))
            (g : ContinuousHom D E), g.toRingHom = TopologicalRing.CompletionOver.canonicalMap f ∧
              ∃ i : X ≅ formalSpectrum E, p = i.hom ≫ formalSpectrumMap hR g)

AlgebraicGeometry.FormalSpace.etale_stageMap_canonicalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleCompletionStageBaseChange.lean, line 104. The attribute's comment: “the first step of the proof read in the site: for an étale ring map B → A and a weak ideal of definition J of B, the morphism Spec (A^∧ ⧸ K) ⟶ Spec (B ⧸ J) of quotient stages of Spf A^∧ ⟶ Spf B induced by the canonical map B → A^∧ is étale. The assertions about the morphism of formal spectra itself — representability, étaleness, full faithfulness, essential surjectivity, the equivalence of categories and the McQuillan conclusion — are not included”.

Stacks 0AN8, the first step of the proof read in the site. For an étale ring map f : B →+* A and a weak ideal of definition J of B, the morphism of quotient stages Spec (A^∧ ⧸ K) ⟶ Spec (B ⧸ J) induced by the canonical map B → A^∧ is étale, where K is the closure of the ideal extended along the canonical map — equivalently the kernel of the projection A^∧ → A ⧸ JA. These are the stages of Spf A^∧ ⟶ Spf B.

theorem etale_stageMap_canonicalMap (f : B →+* A) (hf : f.Etale)
    (D : QuotientSystem 𝔅 S hS B)
    (E : QuotientSystem 𝔅 S hS (TopologicalRing.CompletionOver f))
    (g : ContinuousHom D E)
    (hg : g.toRingHom = TopologicalRing.CompletionOver.canonicalMap f)
    (J : { J : Ideal B // TopologicalRing.IsWeakIdealOfDefinition J })
    (K : { K : Ideal (TopologicalRing.CompletionOver f) //
      TopologicalRing.IsWeakIdealOfDefinition K })
    (hK : K.1 = (J.1.map g.toRingHom).closure)
    (hJK : J.1 ≤ Ideal.comap g.toRingHom K.1) :
    AlgebraicGeometry.Etale ((BigFppfOver.toScheme 𝔅 S hS).map
      ((BigAffineFppf.inclusion 𝔅 S hS).map (g.stageMap J K hJK)))

AlgebraicGeometry.FormalSpace.exists_isPullback_etale_formalSpectrumMap_completionOver_of_compactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleCompletionStageBaseChange.lean, line 193. The attribute's comment: “the base change identification of the proof: for an étale ring map B → A and a point of Spf B out of a quasi-compact object T of the site, T ×_{Spf B} Spf A^∧ is represented by the object T ×_{Spec (B ⧸ J)} Spec (A ⧸ JA) of the site and its projection to T is étale. The assertions about the morphism Spf A^∧ ⟶ Spf B itself — étaleness at an arbitrary scheme-valued point, full faithfulness, essential surjectivity, the equivalence of categories and the McQuillan conclusion — are not included”.

Stacks 0AN8, the base change identification of its proof. For an étale ring map f : B →+* A over a weakly admissible B and every point T ⟶ Spf B whose source is a quasi-compact object of the site, the base change T ×_{Spf B} Spf A^∧ is represented by an object V of the site, namely T ×_{Spec (B ⧸ J)} Spec (A ⧸ JA), and the projection V ⟶ T is étale.

The point factors through a stage Spec (B ⧸ J) ⟶ Spf B by Stacks 0AIA, in the form exists_factorsThroughStage_of_compactSpace, and the base change along the factorisation is exists_isPullback_etale_formalSpectrumMap_completionOver_of_factorsThroughStage.

theorem exists_isPullback_etale_formalSpectrumMap_completionOver_of_compactSpace
    (f : B →+* A) (hf : f.Etale) (hB : TopologicalRing.IsWeaklyAdmissible B)
    (D : QuotientSystem 𝔅 S hS B)
    (E : QuotientSystem 𝔅 S hS (TopologicalRing.CompletionOver f))
    (g : ContinuousHom D E)
    (hg : g.toRingHom = TopologicalRing.CompletionOver.canonicalMap f)
    (U : BigFppfOver 𝔅 S hS) (hU : CompactSpace ((BigFppfOver.toScheme 𝔅 S hS).obj U))
    (a : (Sheaf.sheafifiedYoneda (BigFppfOver.topology 𝔅 S hS)).obj U ⟶ formalSpectrum D) :
    ∃ (V : BigFppfOver 𝔅 S hS) (q : V ⟶ U)
      (r : (Sheaf.sheafifiedYoneda (BigFppfOver.topology 𝔅 S hS)).obj V ⟶ formalSpectrum E),
      IsPullback r ((Sheaf.sheafifiedYoneda (BigFppfOver.topology 𝔅 S hS)).map q)
        (formalSpectrumMap hB g) a ∧
      AlgebraicGeometry.Etale ((BigFppfOver.toScheme 𝔅 S hS).map q)

AlgebraicGeometry.FormalSpace.isEquivalence_etaleCompletionCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SmallEtaleSite/EtaleCompletionEquivalence.lean, line 412. The attribute's comment: “the equivalence of categories, with the functor A^∧ ↦ Spf (A^∧) and the McQuillan conclusion. The equivalence is realized on the opposite of the category of the algebras A^∧, a morphism of that category being a continuous R-algebra homomorphism and Spf being contravariant; Stacks 0DEF writes the same identification with the opposite taken on the geometric side, and mcQuillanAffineEtaleEquivalence moves it there. The quotient system D is how this library says that R is a topological S-algebra, the structure morphisms of the quotient spectra being data here, and without it Spf R is not defined; its large-site condition QuotientSystem.HasLargeSite says that the chosen big fppf site contains the atlas of Spf R, which is what Stacks 0AIF consumes to make Spf R an affine formal algebraic space, so it is part of the source's hypothesis that Y is one, and is a condition on the site rather than on R. It passes to every A^∧ through Stacks 0ANM. No bound on the cardinality of R is assumed”.

Stacks 0AN8. Let S be a scheme contained in a big fppf site B and let R be a weakly admissible topological ring presented over S by a quotient system D whose atlas ∐_J Spec (R ⧸ J) lies in the site, so that Y = Spf R is a McQuillan affine formal algebraic space over S. Then the functor sending an étale R-algebra A to the morphism Spf (A^∧) ⟶ Spf R is an equivalence between the opposite of the category of the topological R-algebras A^∧ = lim A/JA and the category of the morphisms X ⟶ Spf R of affine formal algebraic spaces which are representable by algebraic spaces and étale; in particular every such X is McQuillan, being Spf of the weakly admissible topological ring A^∧.

The hypotheses are the source's. The quotient system D is how this library says that R is a topological S-algebra — the structure morphisms Spec (R ⧸ J) ⟶ S are data here, where the source has them from R being a topological S-algebra — and without it Spf R is not defined. Its large-site condition D.HasLargeSite says that the chosen big fppf site contains the atlas of Spf R, which is what Stacks 0AIF needs to make Spf R an affine formal algebraic space at all; so it is part of the hypothesis that Y is one, and it is a condition on the site rather than on R. Through Stacks 0ANM it passes to every A^∧ with nothing further assumed.

theorem isEquivalence_etaleCompletionCharts :
    (etaleCompletionCharts hR D hD).IsEquivalence ∧
      ∀ W : AffineEtaleFormalCharts B S hS (formalSpectrum D),
        ∃ Y : EtaleCompletion R,
          TopologicalRing.IsWeaklyAdmissible Y.completion ∧
            Nonempty (W.obj.left ≅ formalSpectrum (Y.quotientSystem hR D hD))

TopologicalRing.existsUnique_algEquiv_of_isWeakIdealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/EtaleLiftRigidity.lean, line 97. The attribute's comment: “the rigidity step of the essential surjectivity half: for a weak ideal of definition J₀ and an open ideal J, two étale R ⧸ J-algebras with identified reductions modulo the image of J₀ are uniquely isomorphic compatibly with that identification. This is the uniqueness that produces the family φ_J of the source's proof; the construction of the étale lift, the identification of the stagewise base changes of a representable étale morphism with the spectra of étale algebras, the equivalence of categories and the McQuillan conclusion are not included”.

Stacks 0AN8, the rigidity step φ_J of the essential surjectivity half. Let J₀ be a weak ideal of definition of a topologized commutative ring R and let J be an open ideal of R. Two étale R ⧸ J-algebras whose reductions modulo the image of J₀ are identified are uniquely isomorphic over R ⧸ J compatibly with that identification.

The image of J₀ in R ⧸ J consists of nilpotent elements, a power of a topologically nilpotent element lying in the open ideal J, so this is rigidity of étale lifts along a locally nilpotent ideal. In the source's proof J ⊆ J₀ and the two étale R ⧸ J-algebras both reduce to the fixed étale R ⧸ J₀-algebra A₀.

theorem existsUnique_algEquiv_of_isWeakIdealOfDefinition {J₀ J : Ideal R}
    (hJ₀ : IsWeakIdealOfDefinition J₀) (hJ : IsOpen (J : Set R))
    (S T : Type*) [CommRing S] [CommRing T] [Algebra (R ⧸ J) S] [Algebra (R ⧸ J) T]
    [Algebra.Etale (R ⧸ J) S] [Algebra.Etale (R ⧸ J) T]
    (e : (S ⧸ (J₀.map (Ideal.Quotient.mk J)).map (algebraMap (R ⧸ J) S)) ≃ₐ[R ⧸ J]
      T ⧸ (J₀.map (Ideal.Quotient.mk J)).map (algebraMap (R ⧸ J) T)) :
    ∃! φ : S ≃ₐ[R ⧸ J] T,
      (Ideal.Quotient.mkₐ (R ⧸ J)
          ((J₀.map (Ideal.Quotient.mk J)).map (algebraMap (R ⧸ J) T))).comp φ.toAlgHom =
        e.toAlgHom.comp (Ideal.Quotient.mkₐ (R ⧸ J)
          ((J₀.map (Ideal.Quotient.mk J)).map (algebraMap (R ⧸ J) S)))

TopologicalRing.etale_quotientMap_weakIdealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/EtaleModWeakIdeal.lean, line 92. The attribute's comment: “first step of the proof: for an étale ring map B → A and a weak ideal of definition J of B, the ring map B ⧸ J → A ⧸ JA of quotient stages is étale. The assertions about morphisms of formal spectra — representability, étaleness, full faithfulness, essential surjectivity, the equivalence of categories and the McQuillan conclusion — are not included”.

Stacks 0AN8, first step of the proof. For an étale ring map f : B →+* A and a weak ideal of definition J of B, the induced map B ⧸ J → A ⧸ JA is étale.

public theorem etale_quotientMap_weakIdealOfDefinition {f : B →+* A} (hf : f.Etale)
    (J : WeakIdealOfDefinitionIndex B) :
    (Ideal.quotientMap (extendedIdeal f J) f Ideal.le_comap_map).Etale

TopologicalRing.exists_etale_surjection_weakIdealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/EtaleModWeakIdeal.lean, line 125. The attribute's comment: “the étale-lift step of the essential surjectivity half: for a weak ideal of definition J₀ of B and an étale B ⧸ J₀-algebra A₀, there is an étale B-algebra C together with a surjection C → A₀ compatible with the structure maps whose kernel is the extended ideal J₀ C, so that A₀ is the quotient stage C ⧸ J₀ C. This is the existence of the étale lift only; the comparison family φ_J, the identification of the stagewise base changes of a representable étale morphism with the spectra of étale algebras, the colimit assembly of the essential surjectivity half, the assertions about morphisms of formal spectra — representability, étaleness, full faithfulness — the equivalence of categories and the McQuillan conclusion are not included”.

Stacks 0AN8, the étale-lift step of the essential surjectivity half. Let J₀ be a weak ideal of definition of a linearly topologized ring B and let A₀ be an étale B ⧸ J₀-algebra. Then A₀ is the quotient stage attached to J₀ of an étale B-algebra: there is an étale B-algebra C and a surjection ψ : C → A₀ of rings whose kernel is the extended ideal J₀ C and which is compatible with the two structure maps, so that A₀ ≅ C ⧸ J₀ C over B ⧸ J₀.

This is the step of the source's proof that produces the étale B-algebra from the étale B ⧸ J₀-algebra A₀ cut out by the fixed weak ideal of definition J₀; the source invokes Algebra, Lemma 10.143.10, which this library carries as Stacks 04D1 (etale_lift_along_surjection). Only the existence of the lift is asserted. The comparison family φ_J that the source obtains from uniqueness of étale lifts is TopologicalRing.existsUnique_algEquiv_of_isWeakIdealOfDefinition; the identification of the stagewise base changes of a representable étale morphism with the spectra of étale algebras, the colimit assembly X = Spf A^∧, and the equivalence of categories are not part of this statement.

The conclusion is phrased as a surjection with a named kernel rather than as an isomorphism A₀ ≅ C ⧸ J₀ C, which is the shape Stacks 04D1 is stated in here; the kernel is spelled with this module's extendedIdeal.

public theorem exists_etale_surjection_weakIdealOfDefinition
    (J₀ : WeakIdealOfDefinitionIndex B) (A₀ : Type w) [CommRing A₀]
    [Algebra (B ⧸ (J₀.1 : Ideal B)) A₀] [Algebra.Etale (B ⧸ (J₀.1 : Ideal B)) A₀] :
    ∃ (C : Type u) (_ : CommRing C) (_ : Algebra B C), Algebra.Etale B C ∧
      ∃ ψ : C →+* A₀, Function.Surjective ψ ∧
        RingHom.ker ψ = extendedIdeal (algebraMap B C) J₀ ∧
        ψ.comp (algebraMap B C) =
          (algebraMap (B ⧸ (J₀.1 : Ideal B)) A₀).comp
            (Ideal.Quotient.mk (J₀.1 : Ideal B))

TopologicalRing.CompletionOver.etale_quotientMap_canonicalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/EtaleModWeakIdeal.lean, line 167. The attribute's comment: “first step of the proof, on the stages of the completion: for an étale ring map B → A and a weak ideal of definition J of B, the map B ⧸ J → A^∧ ⧸ ker (A^∧ → A ⧸ JA) of quotient stages of the canonical map B → A^∧ is étale. The assertions about morphisms of formal spectra — representability, étaleness, full faithfulness, essential surjectivity, the equivalence of categories and the McQuillan conclusion — are not included”.

Stacks 0AN8, first step of the proof, on the stages of the completion. For an étale ring map f : B →+* A and a weak ideal of definition J of B, the map B ⧸ J → A^∧ ⧸ ker (A^∧ → A ⧸ JA) induced by the canonical map B → A^∧ is étale; the quotient stages of Spf A^∧ ⟶ Spf B are the spectra of these maps.

public theorem etale_quotientMap_canonicalMap {f : B →+* A} (hf : f.Etale)
    (J : WeakIdealOfDefinitionIndex B) :
    (Ideal.quotientMap (RingHom.ker (projection f J)) (canonicalMap f)
      (le_comap_ker_projection f J)).Etale

Tag 0AN9, a lemma

Tag 0AN9 in the Stacks Project.

AlgebraicGeometry.FormalSpace.etaleFormalSpectrumMap_surjective_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSurjective.lean, line 371.

Let R be a weakly admissible topological ring, let A be an étale R-algebra and let R → A^∧ be the canonical map to the completion of A over R, presented by quotient systems over a base scheme S of a big fppf site. The following are equivalent:

the induced morphism Spf A^∧ ⟶ Spf R of formal spectra is surjective;

R → A is faithfully flat;

R ⧸ J → A ⧸ JA is faithfully flat for every weak ideal of definition J of R;

R ⧸ J → A ⧸ JA is faithfully flat for some weak ideal of definition J of R.

public theorem etaleFormalSpectrumMap_surjective_tfae (f : R →+* A)
    (hA : letI : Algebra R A := f.toAlgebra; Algebra.Etale R A)
    (hB : TopologicalRing.IsWeaklyAdmissible R)
    (D : QuotientSystem B S hS R)
    (E : QuotientSystem B S hS (TopologicalRing.CompletionOver f))
    (g : ContinuousHom D E)
    (hg : g.toRingHom = TopologicalRing.CompletionOver.canonicalMap f) :
    List.TFAE
      [ IsSurjective B S hS (formalSpectrumMap hB g),
        f.FaithfullyFlat,
        ∀ J : TopologicalRing.WeakIdealOfDefinitionIndex R,
          (Ideal.quotientMap (J.1.map f) f Ideal.le_comap_map).FaithfullyFlat,
        ∃ J : TopologicalRing.WeakIdealOfDefinitionIndex R,
          (Ideal.quotientMap (J.1.map f) f Ideal.le_comap_map).FaithfullyFlat ]

Sources

LeanAlgebraicGeometry.FormalSpace.IsLocallyOfFiniteType.of_isRepresentableEtale · AlgebraicGeometry.Space.isRepresentableByAlgebraicSpacesULift_comp · CategoryTheory.Functor.relativelyRepresentable.isMultiplicative · AlgebraicGeometry.Space.isRepresentableByAlgebraicSpacesULift_of_isPullback · CategoryTheory.Functor.relativelyRepresentable.isStableUnderBaseChange · AlgebraicGeometry.FormalSpace.isRepresentableByAlgebraicSpacesULift_of_comp_of_isFormalAlgebraicSpace · AlgebraicGeometry.FormalSpace.isRepresentableByAlgebraicSpacesULift_of_comp_of_isAffineFormal · AlgebraicGeometry.FormalSpace.isRepresentableByAlgebraicSpacesULift_of_comp_of_mono

Section87.20 Types of formal algebraic spaces #

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

Tag 0AKS, a lemma

Tag 0AKS in the Stacks Project.

AlgebraicGeometry.FormalSpace.isCountablyIndexed_of_isCountablyIndexed_of_surjective_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedDescent.lean, line 165. The attribute's comment: “the implication from the source being countably indexed to the target being countably indexed, which is the content of the source's proof; the converse is clause (1) of Stacks 0AKQ”.

Stacks 0AKS, the forward implication. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces, surjective and flat. If X is countably indexed then so is Y.

theorem isCountablyIndexed_of_isCountablyIndexed_of_surjective_flat
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y)
    (hfrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (hsurj : IsSurjective B S hS f)
    (hflat : ∃ hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom,
      Space.HasPropertyULift.{u + 1} B S hS
        (fun _ _ g ↦ Space.HoldsOnEveryEtaleChartULift.{u + 1} B S hS
          (@AlgebraicGeometry.Flat.{u} : MorphismProperty Scheme.{u}) g.hom) f.hom hf)
    (hXc : IsCountablyIndexed B S hS X) :
    IsCountablyIndexed B S hS Y

AlgebraicGeometry.FormalSpace.isCountablyIndexed_iff_of_surjective_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransfer.lean, line 484. The attribute's comment: “the equivalence, at the source's own hypotheses. The forward implication is the source's cofinality argument, isCountablyIndexed_target_of_surjective_flat, which rests on Stacks 0AIA, on Stacks 0AKN — the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces — and on faithful flatness of a represented base change; the reverse implication is part (2) of Stacks 0AKP, the library's isCountablyIndexed_of_relative_isAffineHom”.

Stacks 0AKS. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces, surjective and flat. Then X is countably indexed if and only if Y is.

theorem isCountablyIndexed_iff_of_surjective_flat {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (hsurj : IsSurjective B S hS f) (hflat : IsRepresentableFlat B S hS f) :
    IsCountablyIndexed B S hS X ↔ IsCountablyIndexed B S hS Y

AlgebraicGeometry.FormalSpace.isCountablyIndexed_iff_of_surjective_flat', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransferRefined.lean, line 122. The attribute's comment: “the equivalence, at the source's own hypotheses. The forward implication is the source's cofinality argument, AlgebraicGeometry.FormalSpace.isCountablyIndexed_target_of_surjective_flat, which rests on Stacks 0AIA, on Stacks 0AKN — the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces — and on faithful flatness of a represented base change; the reverse implication is clause (1) of Stacks 0AKQ”.

Stacks 0AKS. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces, surjective and flat. Then X is countably indexed if and only if Y is.

alias isCountablyIndexed_iff_of_surjective_flat'

Tag 0GXR, a lemma

Tag 0GXR in the Stacks Project.

AlgebraicGeometry.FormalSpace.isCountablyIndexedAndClassical_iff_of_isSurjective_of_isRepresentableFlat, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineEtaleChartTypes.lean, line 114.

Stacks 0GXR. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces, surjective and flat. Then X is countably indexed and classical if and only if Y is.

The countably indexed half is Stacks 0AKS. For the classical half, a presenting ring A of Y with a continuous taut homomorphism A → C to a presenting ring of X whose maps on quotients by open ideals are faithfully flat is AlgebraicGeometry.FormalSpace.exists_isTaut_faithfullyFlat_presentingRing_of_surjective_flat, and pre-admissibility descends along it by Stacks 0GXN.

alias isCountablyIndexedAndClassical_iff_of_isSurjective_of_isRepresentableFlat

AlgebraicGeometry.FormalSpace.isCountablyIndexedAndClassical_iff_of_surjective_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransfer.lean, line 505. The attribute's comment: “the equivalence, at the source's own hypotheses. Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces; the countably indexed half of the forward implication is isCountablyIndexed_target_of_surjective_flat, the presenting ring of the target with its continuous taut homomorphism to that of the source is exists_isTaut_faithfullyFlat_presentingRing_of_surjective_flat, and pre-admissibility descends along it by Stacks 0GXN; the reverse implication is clause (3) of Stacks 0AKP, the library's isCountablyIndexedAndClassical_of_relative_isAffineHom”.

Stacks 0GXR. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces, surjective and flat. Then X is countably indexed and classical if and only if Y is.

theorem isCountablyIndexedAndClassical_iff_of_surjective_flat {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y)
    (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (hsurj : IsSurjective B S hS f) (hflat : IsRepresentableFlat B S hS f) :
    IsCountablyIndexed B S hS X ∧ IsClassical B S hS X ↔
      IsCountablyIndexed B S hS Y ∧ IsClassical B S hS Y

Tag 0GXS, a lemma

Tag 0GXS in the Stacks Project.

AlgebraicGeometry.FormalSpace.isWeaklyAdic_iff_of_surjective_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransfer.lean, line 535. The attribute's comment: “the equivalence, at the source's own hypotheses. Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces; the presenting ring of the target with its continuous taut homomorphism to that of the source is exists_isTaut_faithfullyFlat_presentingRing_of_surjective_flat, which takes countable indexing of the source from item (5) of Stacks 0AIK. The forward implication is the library's Stacks 0GXP and the reverse one is clause (4) of Stacks 0AKP, the library's isWeaklyAdic_of_relative_isAffineHom”.

Stacks 0GXS. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces, surjective and flat. Then X is weakly adic if and only if Y is.

theorem isWeaklyAdic_iff_of_surjective_flat {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (hsurj : IsSurjective B S hS f) (hflat : IsRepresentableFlat B S hS f) :
    IsWeaklyAdic B S hS X ↔ IsWeaklyAdic B S hS Y

AlgebraicGeometry.FormalSpace.isWeaklyAdic_iff_of_surjective_flat', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransferRefined.lean, line 160. The attribute's comment: “the equivalence, at the source's own hypotheses. The presenting ring of the target together with the continuous taut homomorphism to the source's, which is Stacks 0AN0, the implication (1) ⟹ (3) of Stacks 0AN5 and the identification of Stacks 0AMZ, is the library's AlgebraicGeometry.FormalSpace``.exists_isTaut_faithfullyFlat_presentingRing_of_surjective_flat, which takes countable indexing of the source from item (5) of Stacks 0AIK; Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces. The forward implication is the library's Stacks 0GXP and the reverse one is clause (3) of Stacks 0AKQ”.

Stacks 0GXS. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces, surjective and flat. Then X is weakly adic if and only if Y is.

alias isWeaklyAdic_iff_of_surjective_flat'

Tag 0AKT, a lemma

Tag 0AKT in the Stacks Project.

AlgebraicGeometry.FormalSpace.isAdicStar_iff_of_surjective_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransfer.lean, line 566. The attribute's comment: “the equivalence, at the source's own hypotheses. The presenting ring of the target with its continuous taut homomorphism to that of the source is exists_isTaut_faithfullyFlat_presentingRing_of_surjective_flat, which takes countable indexing of the source from items (2), (3) and (5) of Stacks 0AIK; Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces. The forward implication is the library's Stacks 0GXQ and the reverse one is clause (5) of Stacks 0AKP, the library's isAdicStar_of_relative_isAffineHom”.

Stacks 0AKT. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces, surjective and flat. Then X is adic* if and only if Y is.

theorem isAdicStar_iff_of_surjective_flat {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (hsurj : IsSurjective B S hS f) (hflat : IsRepresentableFlat B S hS f) :
    IsAdicStar B S hS X ↔ IsAdicStar B S hS Y

AlgebraicGeometry.FormalSpace.isAdicStar_iff_of_surjective_flat', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransferRefined.lean, line 173. The attribute's comment: “the equivalence, at the source's own hypotheses. The presenting ring of the target together with the continuous taut homomorphism to the source's, which is Stacks 0AN0, the implication (1) ⟹ (3) of Stacks 0AN5 and the identification of Stacks 0AMZ, is the library's AlgebraicGeometry.FormalSpace``.exists_isTaut_faithfullyFlat_presentingRing_of_surjective_flat, which takes countable indexing of the source from items (2), (3) and (5) of Stacks 0AIK; Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces. The forward implication is the library's Stacks 0GXQ and the reverse one is clause (4) of Stacks 0AKQ”.

Stacks 0AKT. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces, surjective and flat. Then X is adic* if and only if Y is.

alias isAdicStar_iff_of_surjective_flat'

Tag 0AKW, a lemma

Tag 0AKW in the Stacks Project.

AlgebraicGeometry.FormalSpace.isNoetherian_iff_of_isSurjective_of_isRepresentableFlat, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineEtaleChartTypes.lean, line 130.

Stacks 0AKW. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces, surjective, flat and locally of finite type. Then X is Noetherian if and only if Y is.

The reverse implication is clause (5) of Stacks 0AKQ. For the forward one, let C be a Noetherian adic ring presenting X. A presenting ring A of Y with a continuous taut homomorphism φ : A → C whose maps on quotients by open ideals are faithfully flat is AlgebraicGeometry.FormalSpace.exists_isTaut_faithfullyFlat_presentingRing_of_surjective_flat. By Stacks 0GXQ the ring A has a finitely generated ideal of definition J defining its topology; A ⧸ J is Noetherian by Stacks 033E, its faithfully flat extension C ⧸ (J C)‾ being a quotient of the Noetherian ring C; and A, complete for the J-adic topology, is Noetherian by Stacks 05GH.

alias isNoetherian_iff_of_isSurjective_of_isRepresentableFlat

AlgebraicGeometry.FormalSpace.isNoetherian_iff_of_surjective_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransfer.lean, line 599. The attribute's comment: “the equivalence, at the source's own hypotheses. The presenting ring of the target with its continuous taut homomorphism to that of the source is exists_isTaut_faithfullyFlat_presentingRing_of_surjective_flat; its finitely generated ideal of definition is the library's Stacks 0GXQ, the descent of the Noetherian property to the quotient by it is Stacks 033E, descent_noetherian, and the passage to the complete ring is Stacks 05GH, noetherian_of_isAdicComplete_fg; Stacks 0AKN is the library's relative_isAffineHom_of_isRepresentableByAlgebraicSpaces. The reverse implication is clause (6) of Stacks 0AKP, the library's isNoetherian_of_relative_isAffineHom”.

Stacks 0AKW. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S which is representable by algebraic spaces, surjective, flat and locally of finite type. Then X is Noetherian if and only if Y is.

theorem isNoetherian_iff_of_surjective_flat {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (hsurj : IsSurjective B S hS f) (hflat : IsRepresentableFlat B S hS f)
    (hft : IsLocallyOfFiniteType B S hS f) :
    IsNoetherian B S hS X ↔ IsNoetherian B S hS Y

Tag 0AKX, a lemma

Tag 0AKX in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasAffineEtaleChartProperty_iff_hasAffineEtaleAtlasWithProperty_of_mem, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineEtaleChartTypes.lean, line 172.

Stacks 0AKX. Let X be a formal algebraic space over S and let P be one of the properties of affine formal algebraic spaces countably indexed, countably indexed and classical, weakly adic, adic* and Noetherian. The following are equivalent:

if Y is an affine formal algebraic space and Y ⟶ X is representable by algebraic spaces and étale, then Y has property P;

for some covering {Xᵢ ⟶ X} as in Definition 0AIM each Xᵢ has property P.

For (2) ⟹ (1) the atlas is refined against the chart and cut down to a finite subfamily by quasi-compactness; its members have P by Stacks 0AKQ, their disjoint union has P, and P passes to the chart along the surjective flat morphism from that disjoint union by Stacks 0AKS, 0GXR, 0GXS, 0AKT or 0AKW.

alias hasAffineEtaleChartProperty_iff_hasAffineEtaleAtlasWithProperty_of_mem

AlgebraicGeometry.FormalSpace.hasAffineEtaleChartProperty_iff_hasAffineEtaleAtlasWithProperty_isCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AtlasChartCountablyIndexed.lean, line 99. The attribute's comment: “the equivalence of conditions (1) and (2) at the property of being countably indexed, with nothing assumed. The refinement of the atlas against a chart is the library's exists_countablyIndexed_surjective_flat_over_chart (Stacks 0AJ3 in its chart form, clause (1) of Stacks 0AKQ, the implication (1) ⟹ (2) of Stacks 0AJ9 and the coproduct stability of countable indexing), and the transfer of countable indexing along the surjective flat morphism it produces is Stacks 0AKS. The equivalence is registered at this property rather than at an arbitrary one because the refinement is false at an arbitrary property”.

Stacks 0AKX at countable indexing. Let X be a formal algebraic space over S. Then every affine formal algebraic space representable étale over X is countably indexed if and only if X admits an atlas as in Definition Stacks 0AIM all of whose members are countably indexed.

The implication (1) ⟹ (2) is the atlas of X. For (2) ⟹ (1), a chart g : Z ⟶ X receives a surjective flat morphism, representable by algebraic spaces, from a countably indexed affine formal algebraic space — the coproduct of a finite jointly surjective subfamily of the atlas refined against Z — and Stacks 0AKS transfers countable indexing along it.

theorem hasAffineEtaleChartProperty_iff_hasAffineEtaleAtlasWithProperty_isCountablyIndexed
    (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X) :
    HasAffineEtaleChartProperty B S hS X (IsCountablyIndexed B S hS) ↔
      HasAffineEtaleAtlasWithProperty B S hS X (IsCountablyIndexed B S hS)

AlgebraicGeometry.FormalSpace.hasAffineEtaleChartProperty_iff_hasAffineEtaleAtlasWithProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransfer.lean, line 786. The attribute's comment: “the equivalence of conditions (1) and (2), at the source's own hypotheses and for each of the five properties of its list. For (2) ⟹ (1) the refinement of the atlas against a chart is exists_surjective_flat_over_chart_of_hasAffineEtaleAtlasWithProperty: Stacks 0AJ3 for the fibre products, the coverings of Definition 0AIM, quasi-compactness of the chart, Stacks 0AKQ along the étale maps and the finite disjoint union of the members; the property then passes to the chart by Stacks 0AKS, 0GXR, 0GXS, 0AKT or 0AKW”.

Stacks 0AKX. Let X be a formal algebraic space over S and let P be one of the properties of affine formal algebraic spaces countably indexed, countably indexed and classical, weakly adic, adic* and Noetherian. The following are equivalent:

if Y is an affine formal algebraic space and Y ⟶ X is representable by algebraic spaces and étale, then Y has property P;

for some covering {Xᵢ ⟶ X} as in Definition 0AIM each Xᵢ has property P.

For (2) ⟹ (1) the atlas is refined against the chart and cut down to a finite subfamily by quasi-compactness; its members have P by Stacks 0AKQ, their disjoint union has P, and P passes to the chart along the surjective flat morphism from that disjoint union by Stacks 0AKS, 0GXR, 0GXS, 0AKT or 0AKW.

theorem hasAffineEtaleChartProperty_iff_hasAffineEtaleAtlasWithProperty
    (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X) (P : FppfSheaf B S hS → Prop)
    (hP : P = IsCountablyIndexed B S hS ∨
      P = (fun Z ↦ IsCountablyIndexed B S hS Z ∧ IsClassical B S hS Z) ∨
      P = IsWeaklyAdic B S hS ∨ P = IsAdicStar B S hS ∨ P = IsNoetherian B S hS) :
    HasAffineEtaleChartProperty B S hS X P ↔ HasAffineEtaleAtlasWithProperty B S hS X P

AlgebraicGeometry.FormalSpace.hasAffineEtaleChartProperty_iff_atlas_isCountablyIndexedAndClassical_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransferVariants.lean, line 224. The attribute's comment: “the equivalence of conditions (1) and (2) for the countably indexed and classical property of Stacks 0AIJ and Stacks 0AID, unconditionally. The three conditions on the property asked for by hasAffineEtaleChartProperty_iff_hasAffineEtaleAtlasWithProperty above are, in order, clause (2) of Stacks 0AKQ (isCountablyIndexedAndClassical_of_isRepresentable'), the passage to a finite disjoint union (isCountablyIndexed_sigma' and isClassical_sigma), and Stacks 0GXR (isCountablyIndexedAndClassical_iff_of_isSurjective_of_isRepresentableFlat)”.

Every affine formal algebraic space representable étale over a formal algebraic space X is countably indexed and classical if and only if X admits an atlas as in Definition 0AIM all of whose members are.

theorem hasAffineEtaleChartProperty_iff_atlas_isCountablyIndexedAndClassical_unconditional
    (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X) :
    HasAffineEtaleChartProperty B S hS X
        (fun Y ↦ IsCountablyIndexed B S hS Y ∧ IsClassical B S hS Y) ↔
      HasAffineEtaleAtlasWithProperty B S hS X
        (fun Y ↦ IsCountablyIndexed B S hS Y ∧ IsClassical B S hS Y)

AlgebraicGeometry.FormalSpace.hasAffineEtaleChartProperty_iff_atlas_isWeaklyAdic_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransferVariants.lean, line 247. The attribute's comment: “the equivalence of conditions (1) and (2) for the weakly adic property of Stacks 0AID, unconditionally. The three conditions on the property asked for by hasAffineEtaleChartProperty_iff_hasAffineEtaleAtlasWithProperty above are, in order, clause (3) of Stacks 0AKQ (isWeaklyAdic_of_isRepresentable'), the passage to a finite disjoint union (isWeaklyAdic_sigma'), and Stacks 0GXS (isWeaklyAdic_iff_of_surjective_flat')”.

Every affine formal algebraic space representable étale over a formal algebraic space X is weakly adic if and only if X admits an atlas as in Definition 0AIM all of whose members are.

theorem hasAffineEtaleChartProperty_iff_atlas_isWeaklyAdic_unconditional
    (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X) :
    HasAffineEtaleChartProperty B S hS X (IsWeaklyAdic B S hS) ↔
      HasAffineEtaleAtlasWithProperty B S hS X (IsWeaklyAdic B S hS)

AlgebraicGeometry.FormalSpace.hasAffineEtaleChartProperty_iff_atlas_isAdicStar_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransferVariants.lean, line 265. The attribute's comment: “the equivalence of conditions (1) and (2) for the adic* property of Stacks 0AID, unconditionally. The three conditions on the property asked for by hasAffineEtaleChartProperty_iff_hasAffineEtaleAtlasWithProperty above are, in order, clause (4) of Stacks 0AKQ (isAdicStar_of_isRepresentable'), the passage to a finite disjoint union (isAdicStar_sigma'), and Stacks 0AKT (isAdicStar_iff_of_surjective_flat')”.

Every affine formal algebraic space representable étale over a formal algebraic space X is adic* if and only if X admits an atlas as in Definition 0AIM all of whose members are.

theorem hasAffineEtaleChartProperty_iff_atlas_isAdicStar_unconditional
    (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X) :
    HasAffineEtaleChartProperty B S hS X (IsAdicStar B S hS) ↔
      HasAffineEtaleAtlasWithProperty B S hS X (IsAdicStar B S hS)

AlgebraicGeometry.FormalSpace.hasAffineEtaleChartProperty_iff_atlas_isNoetherian_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TypeTransferVariants.lean, line 285. The attribute's comment: “the equivalence of conditions (1) and (2) for the Noetherian property of Stacks 0AID, unconditionally. The three conditions on the property asked for by hasAffineEtaleChartProperty_iff_hasAffineEtaleAtlasWithProperty above are, in order, clause (5) of Stacks 0AKQ (isNoetherian_of_isRepresentable', which for this property also uses that a representable étale morphism is locally of finite type), the passage to a finite disjoint union (isNoetherian_sigma'), and Stacks 0AKW (isNoetherian_iff_of_isSurjective_of_isRepresentableFlat)”.

Every affine formal algebraic space representable étale over a formal algebraic space X is Noetherian if and only if X admits an atlas as in Definition 0AIM all of whose members are.

theorem hasAffineEtaleChartProperty_iff_atlas_isNoetherian_unconditional
    (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X) :
    HasAffineEtaleChartProperty B S hS X (IsNoetherian B S hS) ↔
      HasAffineEtaleAtlasWithProperty B S hS X (IsNoetherian B S hS)

Tag 0AKY, a definition

Tag 0AKY in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsLocallyCountablyIndexed, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Types.lean, line 98. The attribute's comment: “locally countably indexed”.

Stacks 0AKY, locally countably indexed. A formal algebraic space over S is locally countably indexed when it admits an atlas as in Definition 0AIM by countably indexed affine formal algebraic spaces.

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

AlgebraicGeometry.FormalSpace.IsLocallyCountablyIndexedAndClassical, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Types.lean, line 106. The attribute's comment: “locally countably indexed and classical”.

Stacks 0AKY, locally countably indexed and classical. A formal algebraic space over S is locally countably indexed and classical when it admits an atlas as in Definition 0AIM by affine formal algebraic spaces which are countably indexed and classical.

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

AlgebraicGeometry.FormalSpace.IsLocallyWeaklyAdic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Types.lean, line 115. The attribute's comment: “locally weakly adic”.

Stacks 0AKY, locally weakly adic. A formal algebraic space over S is locally weakly adic when it admits an atlas as in Definition 0AIM by weakly adic affine formal algebraic spaces.

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

AlgebraicGeometry.FormalSpace.IsLocallyAdicStar, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Types.lean, line 122. The attribute's comment: “locally adic star”.

Stacks 0AKY, locally adic*. A formal algebraic space over S is locally adic* when it admits an atlas as in Definition 0AIM by adic* affine formal algebraic spaces.

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

AlgebraicGeometry.FormalSpace.IsLocallyNoetherian, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Types.lean, line 131. The attribute's comment: “locally Noetherian”.

Stacks 0AKY, locally Noetherian. A formal algebraic space over S is locally Noetherian when it admits an atlas as in Definition 0AIM by Noetherian affine formal algebraic spaces, that is by affine formal algebraic spaces whose associated weakly admissible topological ring is Noetherian and adic.

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

Tag 0AQ1, a lemma

Tag 0AQ1 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isLocallyNoetherian_completionSheaf_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionAlgebraicSpaceAtlas.lean, line 538. The attribute's comment: “part (2)”.

Stacks 0AQ1, part (2). Let S be a scheme, let X be a locally Noetherian algebraic space over S and let T ⊆ |X| be a closed subset. The completion X_{/T} of X along T is locally Noetherian.

The affine étale charts Spec A_k ⟶ X of AlgebraicGeometry.FormalSpace.exists_affine_etale_charts are étale over the locally Noetherian X, so each Spec A_k is locally Noetherian and each A_k is a Noetherian ring; the set-theoretic condition is AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_completionSheaf. With these the atlas argument of AlgebraicGeometry.FormalSpace.isLocallyNoetherian_completionSheaf applies.

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

AlgebraicGeometry.FormalSpace.isLocallyAdicStar_completionSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFormalAlgebraicSpace.lean, line 321. The attribute's comment: “part (1): locally adic star; assumes the affine étale charts of X as hA, str, a, ha, hcov, chartwise quasi-compactness of the complement as hqc, and the 0AIS condition as hset”.

Stacks 0AQ1, part (1). Let S be a scheme, let X be an algebraic space over S and let T ⊆ |X| be a closed subset such that X \ T ⟶ X is quasi-compact. The completion X_{/T} of X along T is locally adic*: 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 adic* affine formal algebraic space by the affine case, Stacks 0GBA (1), the complement of the inverse image of T on a chart being quasi-compact.

The affine étale charts of X and the set-theoretic condition of Stacks 0AIS are carried as hypotheses, as in AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_completionSheaf (Stacks 0AIZ); quasi-compactness of X \ T ⟶ X is carried in the form it is used in, namely chartwise quasi-compactness of the complement hqc, which is the source's step transferring the hypothesis from X to the charts. The hypothesis HasStageAtlas of Stacks 0AIY is not needed here: being adic* already contains being an affine formal algebraic space.

theorem isLocallyAdicStar_completionSheaf
    {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)
    {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)))
    (hqc : ∀ i, @IsCompact _
      (Space.pointTopology B S hS (yoneda.obj (affineOver B S hS (hA i) (str i))))
      (Space.pointsMap B S hS _ (a i) ⁻¹' T)ᶜ)
    (hset : SatisfiesSetTheoreticCondition B S hS (Space.completionSheaf B S hS X T)) :
    IsLocallyAdicStar B S hS (Space.completionSheaf B S hS X T)

AlgebraicGeometry.FormalSpace.isLocallyNoetherian_completionSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFormalAlgebraicSpace.lean, line 371. The attribute's comment: “part (2): locally Noetherian; assumes the affine étale charts of X as hA, str, a, ha, hcov, Noetherianness of the chart rings as hNoeth, and the 0AIS condition as hset”.

Stacks 0AQ1, part (2). Let S be a scheme, let X be a locally Noetherian algebraic space over S and let T ⊆ |X| be a closed subset. The completion X_{/T} of X along T is locally Noetherian: 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 a Noetherian affine formal algebraic space by the affine case, Stacks 0GBA (3), the chart rings being Noetherian.

The affine étale charts of X and the set-theoretic condition of Stacks 0AIS are carried as hypotheses, as in AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_completionSheaf (Stacks 0AIZ); local Noetherianness of X is carried in the form it is used in, namely Noetherianness of the chart rings hNoeth, which is the source's step transferring the hypothesis from X to the charts. The hypothesis HasStageAtlas of Stacks 0AIY is not needed here: being Noetherian already contains being an affine formal algebraic space.

theorem isLocallyNoetherian_completionSheaf
    {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)
    {Ix : Type (u + 1)} {A : Ix → Type u} [∀ i, CommRing (A i)]
    (hNoeth : ∀ i, IsNoetherianRing (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)))
    (hset : SatisfiesSetTheoreticCondition B S hS (Space.completionSheaf B S hS X T)) :
    IsLocallyNoetherian B S hS (Space.completionSheaf B S hS X T)

AlgebraicGeometry.FormalSpace.isLocallyAdicStar_completionSheaf_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionLocallyAdicStar.lean, line 130. The attribute's comment: “part (1)”.

Stacks 0AQ1, part (1). Let S be a scheme, let X be an algebraic space over S and let T ⊆ |X| be a closed subset such that the inclusion X ∖ T ⟶ X of the open complement is quasi-compact. Then the completion X_{/T} of X along T is locally adic*.

The affine étale charts Spec A_k ⟶ X are those of AlgebraicGeometry.FormalSpace.exists_affine_etale_charts; on each, the complement of the inverse image of T is quasi-compact (AlgebraicGeometry.Space.isCompact_compl_preimage_pointsMap_of_isQuasiCompact_ι), and the set-theoretic condition of Stacks 0AIS is AlgebraicGeometry.FormalSpace.satisfiesSetTheoreticCondition_completionSheaf. With these the atlas argument of AlgebraicGeometry.FormalSpace.isLocallyAdicStar_completionSheaf applies.

theorem isLocallyAdicStar_completionSheaf_of_isQuasiCompact
    {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)
    (hqc : Space.IsQuasiCompact B S hS (Space.openSubspaceOfPoints B S hS X Tᶜ).ι) :
    IsLocallyAdicStar B S hS (Space.completionSheaf B S hS X T)

AlgebraicGeometry.FormalSpace.isLocallyAdicStar_completionSheaf_and_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionLocallyAdicStar.lean, line 156.

Stacks 0AQ1. Let S be a scheme, let X be an algebraic space over S, let T ⊆ |X| be a closed subset and let X_{/T} be the completion of X along T.

If X ∖ T ⟶ X is quasi-compact, then X_{/T} is locally adic*.

If X is locally Noetherian, then X_{/T} is locally Noetherian.

The two parts are AlgebraicGeometry.FormalSpace.isLocallyAdicStar_completionSheaf_of_isQuasiCompact and AlgebraicGeometry.FormalSpace.isLocallyNoetherian_completionSheaf_of_isLocallyNoetherian.

theorem isLocallyAdicStar_completionSheaf_and_isLocallyNoetherian
    {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) :
    (Space.IsQuasiCompact B S hS (Space.openSubspaceOfPoints B S hS X Tᶜ).ι →
        IsLocallyAdicStar B S hS (Space.completionSheaf B S hS X T)) ∧
      (Space.IsLocallyNoetherian B S hS X →
        IsLocallyNoetherian B S hS (Space.completionSheaf B S hS X T))

Tag 0CKX, a remark

Tag 0CKX in the Stacks Project.

RationalPowerSeries.mem_radical_polynomialTIdeal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/RadicalCompletion.lean, line 138. The attribute's comment: “the radical of (t) in the monoid algebra”.

Stacks 0CKX. The radical of (t) in k[t^(ℚ≥0)] is the ideal of polynomials with vanishing constant coefficient: a positive exponent becomes at least one after enough multiplications.

theorem mem_radical_polynomialTIdeal_iff (k : Type*) [Field k] (p : rationalPolynomial k) :
    p ∈ (polynomialTIdeal k).radical ↔ p.coeff 0 = 0

RationalPowerSeries.isMaximal_radical_polynomialTIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/RadicalCompletion.lean, line 177. The attribute's comment: “the radical of (t) is the maximal ideal”.

Stacks 0CKX. The radical of (t) is a maximal ideal of k[t^(ℚ≥0)], being the kernel of the constant-coefficient map onto the field k.

theorem isMaximal_radical_polynomialTIdeal (k : Type*) [Field k] :
    ((polynomialTIdeal k).radical).IsMaximal

RationalPowerSeries.radicalQuotientEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/RadicalCompletion.lean, line 184. The attribute's comment: “the residue field at the radical of (t)”.

Stacks 0CKX. The residue field of k[t^(ℚ≥0)] at the radical of (t) is k.

def radicalQuotientEquiv (k : Type*) [Field k] :
    rationalPolynomial k ⧸ (polynomialTIdeal k).radical ≃+* k

RationalPowerSeries.radical_polynomialTIdeal_sq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/RadicalCompletion.lean, line 192. The attribute's comment: “J ^ 2 = J for J the radical of (t)”.

Stacks 0CKX. The radical of (t) is idempotent: a monomial of positive exponent is the square of the monomial of half that exponent.

theorem radical_polynomialTIdeal_sq (k : Type*) [Field k] :
    (polynomialTIdeal k).radical ^ 2 = (polynomialTIdeal k).radical

RationalPowerSeries.radical_polynomialTIdeal_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/RadicalCompletion.lean, line 223. The attribute's comment: “J ^ n = J for J the radical of (t)”.

Stacks 0CKX. Every positive power of the radical of (t) equals it, so the tower defining its adic completion is constant.

theorem radical_polynomialTIdeal_pow (k : Type*) [Field k] {n : ℕ} (hn : n ≠ 0) :
    (polynomialTIdeal k).radical ^ n = (polynomialTIdeal k).radical

RationalPowerSeries.radicalAdicCompletionEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/RadicalCompletion.lean, line 267. The attribute's comment: “the radical-adic completion of the monoid algebra is k”.

Stacks 0CKX. The completion of k[t^(ℚ≥0)] at the radical of (t) is k itself, because that radical is idempotent.

def radicalAdicCompletionEquiv (k : Type*) [Field k] :
    AdicCompletion (polynomialTIdeal k).radical (rationalPolynomial k) ≃+* k

RationalPowerSeries.injective_of_rationalPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/RadicalCompletion.lean, line 282. The attribute's comment: “the monoid algebra sits inside its (t)-adic completion”.

Stacks 0CKX. The monoid algebra is contained in its (t)-adic completion: a polynomial whose class vanishes modulo every power of (t) has all coefficients zero.

theorem injective_of_rationalPolynomial (k : Type*) [CommRing k] :
    Function.Injective
      (AdicCompletion.of (polynomialTIdeal k) (rationalPolynomial k))

RationalPowerSeries.not_injective_compareAlgHom_radical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/RadicalCompletion.lean, line 314. The attribute's comment: “the comparison map is not injective”.

Stacks 0CKX. The comparison map from the (t)-adic completion of k[t^(ℚ≥0)] to the completion at the radical of (t) is not injective: it kills the nonzero element t.

theorem not_injective_compareAlgHom_radical (k : Type*) [Field k] :
    ¬ Function.Injective
      (AdicCompletion.compareAlgHom k (polynomialTIdeal_pow_one_le_radical k))

RationalPowerSeries.not_bijective_compareAlgHom_radical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/RadicalCompletion.lean, line 324. The attribute's comment: “the comparison map is not a ring isomorphism”.

Stacks 0CKX. The natural map from the I-adic completion to the √I-adic completion of a ring can fail to be an isomorphism: for I = (t) in k[t^(ℚ≥0)] it is not bijective.

theorem not_bijective_compareAlgHom_radical (k : Type*) [Field k] :
    ¬ Function.Bijective
      (AdicCompletion.compareAlgHom k (polynomialTIdeal_pow_one_le_radical k))

RationalPowerSeries.isEmpty_ringEquiv_adicCompletion_radical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/RationalPowerSeries/RadicalCompletion.lean, line 333. The attribute's comment: “the two completions are not isomorphic”.

Stacks 0CKX. The two completions are not isomorphic by any ring map at all: the completion at the radical is the field k, while t is a nonzero non-unit of the (t)-adic completion.

theorem isEmpty_ringEquiv_adicCompletion_radical (k : Type*) [Field k] :
    IsEmpty (rationalPowerSeries k ≃+*
      AdicCompletion (polynomialTIdeal k).radical (rationalPolynomial k))

Tag 0GBB, a lemma

Tag 0GBB in the Stacks Project.

AlgebraicGeometry.FormalSpace.isLocallyCountablyIndexed_pullback', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FibreProductTypesRefined.lean, line 133. The attribute's comment: “clause (1), locally countably indexed; the affine case (0AN3 with 0GB4) and the 0AIM covering condition for the chart cover are named hypotheses”.

Stacks 0GBB, clause (1). If X and Z are locally countably indexed, then so is X ×_Y Z. The hypotheses hPaff and hcover are the inputs of the source which the library does not carry; the implication (2) ⟹ (1) of Stacks 0AKX, which the other four clauses carry as h0AKX, is a theorem at countable indexing and is discharged here, as is separatedness of the chart.

theorem isLocallyCountablyIndexed_pullback' {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    (hZ : IsLocallyCountablyIndexed B S hS Z)
    (hPaff : AffineChartFibreProductStable B S hS (IsCountablyIndexed B S hS))
    (hcover : HasChartPullbackCover B S hS f g) :
    IsLocallyCountablyIndexed B S hS (pullback f g)

AlgebraicGeometry.FormalSpace.isLocallyCountablyIndexed_pullback_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FibreProductTypesSupplement.lean, line 286. The attribute's comment: “clause (1), locally countably indexed, in full under the source's hypotheses. The affine case (0AN3 with 0GB4) is affineChartFibreProductStable_isCountablyIndexed; the 0AIS set-theoretic condition for X ×_Y Z is satisfiesSetTheoreticCondition_pullback_of_isFormalAlgebraicSpace', from 0AIP; the 0AIM covering condition for the chart cover is isLocallySurjective_sigmaDesc_chartPullbackMap; Stacks 0AKX (2) implies (1) is AlgebraicGeometry.FormalSpace.hasAffineEtaleChartProperty_iff_hasAffineEtaleAtlasWithProperty_isCountablyIndexed; and the étale case of Stacks 0AJ3 is isFormalAlgebraicSpace_pullback_of_isRepresentableEtale”.

Stacks 0GBB, clause (1). If X and Z are locally countably indexed, then so is X ×_Y Z. The hypotheses are exactly the source's.

theorem isLocallyCountablyIndexed_pullback_unconditional {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y)
    (g : Z ⟶ Y)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    (hZ : IsLocallyCountablyIndexed B S hS Z) :
    IsLocallyCountablyIndexed B S hS (pullback f g)

AlgebraicGeometry.FormalSpace.isLocallyCountablyIndexedAndClassical_pullback_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FibreProductTypesSupplement.lean, line 311. The attribute's comment: “clause (2), locally countably indexed and classical, in full under the source's hypotheses. The affine case (0AN3 with 0GB4) is affineChartFibreProductStable_isCountablyIndexedAndClassical; the 0AIS set-theoretic condition for X ×_Y Z is satisfiesSetTheoreticCondition_pullback_of_isFormalAlgebraicSpace', from 0AIP; the 0AIM covering condition for the chart cover is isLocallySurjective_sigmaDesc_chartPullbackMap; Stacks 0AKX (2) implies (1) is hasAffineEtaleChartProperty_iff_atlas_isCountablyIndexedAndClassical_unconditional; and the étale case of Stacks 0AJ3 is isFormalAlgebraicSpace_pullback_of_isRepresentableEtale”.

Stacks 0GBB, clause (2). If X and Z are locally countably indexed and classical, then so is X ×_Y Z. The hypotheses are exactly the source's.

theorem isLocallyCountablyIndexedAndClassical_pullback_unconditional {X Y Z : FppfSheaf B S hS}
    (f : X ⟶ Y) (g : Z ⟶ Y) (hX : IsLocallyCountablyIndexedAndClassical B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y)
    (hZ : IsLocallyCountablyIndexedAndClassical B S hS Z) :
    IsLocallyCountablyIndexedAndClassical B S hS (pullback f g)

AlgebraicGeometry.FormalSpace.isLocallyWeaklyAdic_pullback_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FibreProductTypesSupplement.lean, line 335. The attribute's comment: “clause (3), locally weakly adic, in full under the source's hypotheses. The affine case (0AN3 with 0GXJ) is affineChartFibreProductStable_isWeaklyAdic; the 0AIS set-theoretic condition for X ×_Y Z is satisfiesSetTheoreticCondition_pullback_of_isFormalAlgebraicSpace', from 0AIP; the 0AIM covering condition for the chart cover is isLocallySurjective_sigmaDesc_chartPullbackMap; Stacks 0AKX (2) implies (1) is hasAffineEtaleChartProperty_iff_atlas_isWeaklyAdic_unconditional; and the étale case of Stacks 0AJ3 is isFormalAlgebraicSpace_pullback_of_isRepresentableEtale”.

Stacks 0GBB, clause (3). If X and Z are locally weakly adic, then so is X ×_Y Z. The hypotheses are exactly the source's.

theorem isLocallyWeaklyAdic_pullback_unconditional {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y)
    (g : Z ⟶ Y)
    (hX : IsLocallyWeaklyAdic B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    (hZ : IsLocallyWeaklyAdic B S hS Z) :
    IsLocallyWeaklyAdic B S hS (pullback f g)

AlgebraicGeometry.FormalSpace.isLocallyAdicStar_pullback_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FibreProductTypesSupplement.lean, line 357. The attribute's comment: “clause (4), locally adic*, in full under the source's hypotheses. The affine case (0AN3 with 0GB4) is affineChartFibreProductStable_isAdicStar; the 0AIS set-theoretic condition for X ×_Y Z is satisfiesSetTheoreticCondition_pullback_of_isFormalAlgebraicSpace', from 0AIP; the 0AIM covering condition for the chart cover is isLocallySurjective_sigmaDesc_chartPullbackMap; Stacks 0AKX (2) implies (1) is hasAffineEtaleChartProperty_iff_atlas_isAdicStar_unconditional; and the étale case of Stacks 0AJ3 is isFormalAlgebraicSpace_pullback_of_isRepresentableEtale”.

Stacks 0GBB, clause (4). If X and Z are locally adic*, then so is X ×_Y Z. The hypotheses are exactly the source's.

theorem isLocallyAdicStar_pullback_unconditional {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hX : IsLocallyAdicStar B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    (hZ : IsLocallyAdicStar B S hS Z) :
    IsLocallyAdicStar B S hS (pullback f g)

AlgebraicGeometry.FormalSpace.isLocallyNoetherian_pullback_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FibreProductTypesSupplement.lean, line 410. The attribute's comment: “clause (5), locally Noetherian, in full under the source's hypotheses. The affine case (0AN3 with 0GB4) is affineChartFibreProductStable_isNoetherian, the affine case RELATIVE TO THE CHART MAP: the map-blind form is unsatisfiable at IsNoetherian -- it quantifies over all affine U, V, W with no condition on the maps, which is false for Spec K over Spec k with K/k of infinite transcendence degree, the presenting ring of the fibre product being the non-Noetherian K tensor K -- so a registration on it would have been vacuous. The docstring gives that witness. The source's finite type condition on the reductions, hfin, is carried to the chart maps by hasLocallyOfFiniteTypeReduction_chart and from there to algebraMap C A by the affine dictionary chartPropertyIsFiniteTypeOnReductions. The 0AIS set-theoretic condition for X ×_Y Z is satisfiesSetTheoreticCondition_pullback_of_isFormalAlgebraicSpace', from 0AIP; the 0AIM covering condition for the chart cover is isLocallySurjective_sigmaDesc_chartPullbackMap; Stacks 0AKX (2) implies (1) is hasAffineEtaleChartProperty_iff_atlas_isNoetherian_unconditional; and the étale case of Stacks 0AJ3 is isFormalAlgebraicSpace_pullback_of_isRepresentableEtale”.

Stacks 0GBB, clause (5). If X and Z are locally Noetherian and X_red ⟶ Y_red is locally of finite type, then X ×_Y Z is locally Noetherian.

hfin is the source's own hypothesis on the reduction morphism, and the hypotheses are exactly the source's.

The affine case is relative to the chart map, AlgebraicGeometry.FormalSpace.AffineChartFibreProductStableRel: the map-blind AlgebraicGeometry.FormalSpace.AffineChartFibreProductStable, which the other four clauses prove, is unsatisfiable at P := IsNoetherian: it asserts that every fibre product of Noetherian affine formal algebraic spaces over an affine formal algebraic space is Noetherian, which is false in every big fppf site over a nonempty base. Take a point of S with residue field k and K = k(x₁, x₂, …); then Spec k and Spec K are affine objects of the site, hence affine formal algebraic spaces by AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_sheafifiedYoneda', and Spec K is Noetherian — its presenting ring K is discrete, hence Noetherian, complete and adic with ideal of definition (0). The sheafified Yoneda embedding preserves fibre products on this subcanonical site, so Spec K ×_{Spec k} Spec K = Spec (K ⊗_k K), whose presenting ring is K ⊗_k K; that ring is not Noetherian, and by AlgebraicGeometry.FormalSpace.exists_continuous_ringEquiv_of_isPresentingRing the presenting ring is unique up to isomorphism of topological rings, so no Noetherian one presents it. A registration of this clause on the map-blind affine case would be vacuously true.

The passage from the chart map to the morphism into the shrunk base of the affine case transports nothing along the monomorphism of the shrink: reduction is not invariant along an arbitrary monomorphism, AlgebraicGeometry.FormalSpace.isReduction_completionSheaf being a counterexample.

theorem isLocallyNoetherian_pullback_unconditional {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y)
    (g : Z ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    (hZ : IsLocallyNoetherian B S hS Z)
    (hfin : HasLocallyOfFiniteTypeReduction B S hS f) :
    IsLocallyNoetherian B S hS (pullback f g)

Tag 0GHM, a lemma

Tag 0GHM in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_finiteOrderThickening_presentation_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocallyNoetherianColimitPresentation.lean, line 317.

Stacks 0GHM. Let X be a locally Noetherian formal algebraic space over S. Then X = colim X_n for a system X_0 ⟶ X_1 ⟶ X_2 ⟶ ⋯ of finite-order thickenings of locally Noetherian algebraic spaces over S, where X_0 = X_red and X_n is the nth infinitesimal neighbourhood of X_0 in X_m for all m ≥ n.

The stages are indexed from zero, so the stage n is the source's X_{n+1}. In detail: every X_n is an algebraic space whose étale atlases are locally Noetherian; every transition morphism X_n ⟶ X_m is representable and an mth-order thickening on every represented base change; on every represented base change along a section of X_m, the ideal sheaf of X_n is the (n + 1)st power of the ideal sheaf of X_0; and X is the colimit of the X_n, its colimit leg at 0 exhibiting X_0 as the reduction of X.

theorem exists_finiteOrderThickening_presentation_of_isLocallyNoetherian
    (X : FppfSheaf B S hS) (hX : IsLocallyNoetherian B S hS X) :
    ∃ E : ℕ ⥤ FppfSheaf B S hS,
      (∀ n, Space.IsAlgebraicSpaceULift.{u + 1} B S hS (E.obj n).obj) ∧
      (∀ n, Space.HasEtaleLocalPropertyULift.{u + 1} B S hS (E.obj n).obj
        (fun T : Scheme.{u} ↦ AlgebraicGeometry.IsLocallyNoetherian T)) ∧
      (∀ ⦃n m : ℕ⦄ (f : n ⟶ m), Space.HasSchemePropertyULift.{u + 1} B S hS
        (fun _ _ k ↦ Stacks.Thickenings.IsNthOrderThickening m k) (E.map f).hom) ∧
      (∀ (n m : ℕ) (hnm : n ≤ m) {a b c : BigFppfOver B S hS}
        (g : uliftYoneda.{u + 1}.obj a ⟶ (E.obj m).obj)
        {fst₀ : uliftYoneda.{u + 1}.obj b ⟶ (E.obj 0).obj} {snd₀ : b ⟶ a}
        (_ : IsPullback fst₀ (uliftYoneda.{u + 1}.map snd₀)
          (E.map (homOfLE (Nat.zero_le m))).hom g)
        {fstₙ : uliftYoneda.{u + 1}.obj c ⟶ (E.obj n).obj} {sndₙ : c ⟶ a}
        (_ : IsPullback fstₙ (uliftYoneda.{u + 1}.map sndₙ) (E.map (homOfLE hnm)).hom g),
        ((BigFppfOver.toScheme B S hS).map snd₀).ker ^ (n + 1) =
          ((BigFppfOver.toScheme B S hS).map sndₙ).ker) ∧
      ∃ e : X ≅ colimit E, IsReduction B S hS X (E.obj 0) (colimit.ι E 0 ≫ e.inv)

AlgebraicGeometry.FormalSpace.exists_finiteOrderThickening_presentation_formalSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/NoetherianColimitPresentation.lean, line 174. The attribute's comment: “Noetherian affine formal algebraic space”.

Stacks 0GHM, for a Noetherian affine formal algebraic space. Let A be a Noetherian topological ring whose topology is adic. Then the formal spectrum of A is the colimit of a sequence X_0 → X_1 → X_2 → ⋯ of affine schemes over S whose transition morphisms are finite-order thickenings, whose terms are all locally Noetherian, whose first term X_0 is reduced, and in which X_n is the nth infinitesimal neighbourhood of X_0 inside X_m for every m ≥ n — the last clause in the form of the equality (X_0 ⟶ X_m).ker ^ (n + 1) = (X_n ⟶ X_m).ker of ideal sheaves on X_m.

theorem exists_finiteOrderThickening_presentation_formalSpectrum
    [IsTopologicalRing A] [IsLinearTopology A A] [IsNoetherianRing A]
    {I : Ideal A} (hI : _root_.IsAdic I) (D : QuotientSystem B S hS A) :
    ∃ E : ℕ ⥤ BigAffineFppf B S hS,
      IsReduced ((BigAffineFppf.toScheme B S hS).obj (E.obj 0)) ∧
      (∀ n, IsLocallyNoetherian ((BigAffineFppf.toScheme B S hS).obj (E.obj n))) ∧
      (∀ ⦃n m : ℕ⦄ (f : n ⟶ m), Stacks.Thickenings.IsFiniteOrderThickening
        ((BigAffineFppf.toScheme B S hS).map (E.map f))) ∧
      (∀ (n m : ℕ) (hnm : n ≤ m),
        ((BigAffineFppf.toScheme B S hS).map (E.map (homOfLE (Nat.zero_le m)))).ker ^ (n + 1) =
          ((BigAffineFppf.toScheme B S hS).map (E.map (homOfLE hnm))).ker) ∧
      Nonempty (formalSpectrum D ≅ colimit (E ⋙ BigAffineFppf.inclusion B S hS ⋙
        Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)))

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

87.17 Quasi-compact formal… to 87.20 Types of formal algebraic…

Section87.17 Quasi-compact formal algebraic spaces#

Tag 0AJ9, a lemma

Tag 0AJA, a definition

Tag 0AJB, a lemma

Tag 0AJC, a definition

Tag 0AM2, a lemma

Sources

Section87.18 Quasi-compact and quasi-separated formal algebraic spaces#

Tag 0AJE, a lemma

Tag 0AJF, a remark

Tag 0DE8, a lemma

Sources

Section87.19 Morphisms representable by algebraic spaces#

Tag 0AJG, the section

Tag 0APY, a lemma

Tag 0APZ, a lemma

Tag 0AQ0, a lemma

Tag 0AN4, a lemma

Tag 0AJH, a lemma

Tag 0AJI, a lemma

Tag 0AKN, a lemma

Tag 0AN5, a lemma

Tag 0AKP, a lemma

Tag 0AKQ, a lemma

Tag 0AN6, an example

Tag 0AN7, a remark

Tag 0AN8, a lemma

Tag 0AN9, a lemma

Sources

Section87.20 Types of formal algebraic spaces#

Tag 0AKS, a lemma

Tag 0GXR, a lemma

Tag 0GXS, a lemma

Tag 0AKT, a lemma

Tag 0AKW, a lemma

Tag 0AKX, a lemma

Tag 0AKY, a definition

Tag 0AQ1, a lemma

Tag 0CKX, a remark

Tag 0GBB, a lemma

Tag 0GHM, a lemma

Sources

Section87.17 Quasi-compact formal algebraic spaces #

Section87.18 Quasi-compact and quasi-separated formal algebraic spaces #

Section87.19 Morphisms representable by algebraic spaces #

Section87.20 Types of formal algebraic spaces #