88.18 Rig-smooth morphisms to 88.30 Application to…

Section88.18 Rig-smooth morphisms#

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

Tag 0GCP, a definition

Tag 0GCP in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsRigSmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmooth.lean, line 66.

Stacks 0GCP. A morphism of formal algebraic spaces over S is rig-smooth when every morphism between affine, representable, étale charts of its source and target is induced by a rig-smooth continuous homomorphism of adic Noetherian topological rings.

abbrev IsRigSmooth (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop
Tag 0GCQ, a lemma

Tag 0GCQ in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSmooth_iff_hasPropertyOnEveryAffineEtaleDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmooth.lean, line 97. The attribute's comment: “conditions (1) and (2)”.

Stacks 0GCQ, conditions (1) and (2). A morphism of formal algebraic spaces over S is rig-smooth exactly when rig-smoothness as a property of arrows of WAdm^{Noeth} holds on every affine étale diagram over it: the two conditions are the same, which is what Definition 0GCP says.

theorem isRigSmooth_iff_hasPropertyOnEveryAffineEtaleDiagram (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) {X Y : FppfSheaf B S hS} (f : X ⟶ Y) :
    IsRigSmooth B S hS f ↔
      HasPropertyOnEveryAffineEtaleDiagram B S hS
        (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R)
        (fun {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
          [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂] (φ : R₁ →+* R₂) ↦
          RingHom.IsRigSmoothArrow φ) f

AlgebraicGeometry.FormalSpace.isRigSmooth_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmoothCharacterization.lean, line 81.

Stacks 0GCQ. For a morphism f : X ⟶ Y of locally Noetherian formal algebraic spaces over S, the following are equivalent: f is rig-smooth (Definition 0GCP); every commutative square with affine formal algebraic spaces U, V and representable étale maps U ⟶ X, V ⟶ Y has U ⟶ V given by a rig-smooth arrow of WAdm^{Noeth}; there are an affine étale covering {Yⱼ ⟶ Y} and, for each j, an affine étale covering {Xⱼᵢ ⟶ Yⱼ ×_Y X} with every Xⱼᵢ ⟶ Yⱼ given by a rig-smooth arrow of WAdm^{Noeth}; and there is an affine étale covering {Xᵢ ⟶ X} with factorizations Xᵢ ⟶ Yᵢ ⟶ Y through affine formal algebraic spaces representable étale over Y with every Xᵢ ⟶ Yᵢ given by a rig-smooth arrow of WAdm^{Noeth}.

theorem isRigSmooth_tfae {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y) :
    List.TFAE
      [IsRigSmooth B S hS f,
        HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic
          (fun φ ↦ RingHom.IsRigSmoothArrow φ) f,
        HasPropertyAfterTargetCover B S hS TopologicalRing.IsNoetherianAdic
          (fun φ ↦ RingHom.IsRigSmoothArrow φ) f,
        HasPropertyAfterSourceCover B S hS TopologicalRing.IsNoetherianAdic
          (fun φ ↦ RingHom.IsRigSmoothArrow φ) f]

AlgebraicGeometry.FormalSpace.isRigSmooth_tfae_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmoothLocalCharacterization.lean, line 103.

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

  1. f is rig-smooth (Definition 0GCP);
  2. for every commutative square with U, V affine formal algebraic spaces and U ⟶ X, V ⟶ Y representable by algebraic spaces and étale, the morphism U ⟶ V corresponds to a rig-smooth map in WAdm^{Noeth};
  3. there exist a covering {Yⱼ ⟶ Y} as in Definition 0AIM and for each j a covering {Xⱼᵢ ⟶ Yⱼ ×_Y X} as in Definition 0AIM such that each Xⱼᵢ ⟶ Yⱼ corresponds to a rig-smooth map in WAdm^{Noeth};
  4. there exist a covering {Xᵢ ⟶ X} as in Definition 0AIM and for each i a factorization Xᵢ ⟶ Yᵢ ⟶ Y where Yᵢ is an affine formal algebraic space, Yᵢ ⟶ Y is representable by algebraic spaces and étale, and Xᵢ ⟶ Yᵢ corresponds to a rig-smooth map in WAdm^{Noeth}.

In (2), (3) and (4) "corresponds to a rig-smooth map in WAdm^{Noeth}" is CorrespondsToNoetherianMap for rig-smoothness: source and target are formal spectra of Noetherian adic rings and the map is the formal spectrum of a rig-smooth homomorphism.

theorem isRigSmooth_tfae_of_isLocallyNoetherian {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y) :
    List.TFAE
      [IsRigSmooth B S hS f,
        CorrespondsToNoetherianMapOnEveryAffineEtaleDiagram B S hS
          (fun φ ↦ RingHom.IsRigSmoothArrow φ) f,
        CorrespondsToNoetherianMapAfterTargetCover B S hS (fun φ ↦ RingHom.IsRigSmoothArrow φ) f,
        CorrespondsToNoetherianMapAfterSourceCover B S hS
          (fun φ ↦ RingHom.IsRigSmoothArrow φ) f]
Tag 0GCR, a lemma

Tag 0GCR in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSmooth_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmoothPullback.lean, line 60.

Stacks 0GCR. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of locally Noetherian formal algebraic spaces over S. If f is rig-smooth and g is adic, then the base change X ×_Y Z ⟶ Z is rig-smooth.

theorem isRigSmooth_pullback_snd {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hZ : IsLocallyNoetherian B S hS Z) (hf : IsRigSmooth B S hS f)
    (hg : IsAdicMorphism B S hS g) :
    IsRigSmooth B S hS (pullback.snd f g)
Tag 0GCS, a lemma

Tag 0GCS in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSmooth_comp_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmoothCompositionLocallyNoetherian.lean, line 57.

Stacks 0GCS. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of locally Noetherian formal algebraic spaces over S. If f and g are rig-smooth, then so is g ∘ f.

theorem isRigSmooth_comp_of_isLocallyNoetherian (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hZ : IsLocallyNoetherian B S hS Z)
    (hf : IsRigSmooth B S hS f) (hg : IsRigSmooth B S hS g) :
    IsRigSmooth B S hS (f ≫ g)
Tag 0GH3, a lemma

Tag 0GH3 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigFlat_of_isRigSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmoothRigFlat.lean, line 46.

Stacks 0GH3. A rig-smooth morphism of locally Noetherian formal algebraic spaces over S is rig-flat.

theorem isRigFlat_of_isRigSmooth (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hf : IsRigSmooth B S hS f) : IsRigFlat B S hS f
Sources
LeanAlgebraicGeometry.FormalSpace.IsRigSmooth · AlgebraicGeometry.FormalSpace.isRigSmooth_iff_hasPropertyOnEveryAffineEtaleDiagram · AlgebraicGeometry.FormalSpace.isRigSmooth_tfae · AlgebraicGeometry.FormalSpace.isRigSmooth_tfae_of_isLocallyNoetherian · AlgebraicGeometry.FormalSpace.isRigSmooth_pullback_snd · AlgebraicGeometry.FormalSpace.isRigSmooth_comp_of_isLocallyNoetherian · AlgebraicGeometry.FormalSpace.isRigFlat_of_isRigSmooth

Section88.19 Rig-étale homomorphisms#

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

Tag 0GCU, a lemma

Tag 0GCU in the Stacks Project.

Rig.rigEtaleOver_iff_forall_idealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmooth.lean, line 220.

Stacks Project, Tag 0GCU. For an adic morphism of topologically finite type between Noetherian adic rings, rig-étaleness over one ideal of definition is equivalent to rig-étaleness over every ideal of definition.

public theorem rigEtaleOver_iff_forall_idealOfDefinition
    {A : Type u} {B : Type v}
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [IsNoetherianRing A]
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    [IsNoetherianRing B]
    (φ : A →+* B) (_hφ : Continuous φ)
    (_hA : TopologicalRing.IsAdic A) (_hB : TopologicalRing.IsAdic B) :
    (FiniteTypeAdicAlgebraForEveryIdeal φ ∧
      ∃ I : Ideal A, TopologicalRing.IsIdealOfDefinition I ∧ IsRigEtaleOver φ I) ↔
    (FiniteTypeAdicAlgebraForEveryIdeal φ ∧
      ∀ I : Ideal A, TopologicalRing.IsIdealOfDefinition I → IsRigEtaleOver φ I)
Tag 0GCV, a definition

Tag 0GCV in the Stacks Project.

RingHom.IsRigEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmooth.lean, line 277.

Stacks Project, Tag 0GCV. A continuous homomorphism of Noetherian adic topological rings is rig-étale when it is adic of topologically finite type — condition (6) of Tag 0GBW — and makes its target rig-étale over some ideal of definition of its source. By Tag 0GCU the choice of that ideal is immaterial.

public abbrev IsRigEtale {A : Type u} {B : Type v}
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [IsNoetherianRing A]
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    [IsNoetherianRing B]
    (φ : A →+* B) : Prop
Tag 0AQL, a lemma

Tag 0AQL in the Stacks Project.

Rig.rigEtale_propertyIsLocalNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigEtaleIsLocal.lean, line 649.

Stacks 0AQL. Rig-étaleness is a local property of arrows of WAdm^Noeth, in the sense of Situation 0CBA in the Noetherian form of Remark 0ANI: it ascends along a completed étale localization diagram, descends along one whose target-side horizontal map is faithfully flat, and is preserved by finite products of targets.

public theorem rigEtale_propertyIsLocalNoetherian :
    TopologicalRing.PropertyIsLocalNoetherian.{u}
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
        RingHom.IsRigEtaleArrow φ)
Tag 0GCW, a lemma

Tag 0GCW in the Stacks Project.

TopologicalRing.rigEtale_completedTensorProduct_of_isAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmoothStability.lean, line 801.

Rig-étaleness (Tag 0GCV) is stable under base change by adic morphisms (Tag 0GBR) in the sense of Remark 0GBG: if B → A is rig-étale and B → C is adic, both arrows of WAdm^{Noeth}, then the completed tensor product A ⊗̂_B C is again Noetherian adic and rig-étale over C.

public theorem rigEtale_completedTensorProduct_of_isAdic
    {B A C : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing C] [TopologicalSpace C] [IsTopologicalRing C]
    [IsLinearTopology C C] [Algebra B A] [Algebra B C] [IsNoetherianRing B]
    [IsNoetherianRing A] [IsNoetherianRing C]
    (hB : TopologicalRing.IsAdic B) (hA : TopologicalRing.IsAdic A)
    (hC : TopologicalRing.IsAdic C)
    (hBA : Continuous (algebraMap B A)) (hBC : Continuous (algebraMap B C))
    (hP : RingHom.IsRigEtaleArrow (algebraMap B A))
    (hQ : RingHom.IsAdic (algebraMap B C)) :
    TopologicalRing.IsAdic (TopologicalRing.CompletedTensorProduct (R := B) (M := A) (N := C)) ∧
      IsNoetherianRing (TopologicalRing.CompletedTensorProduct (R := B) (M := A) (N := C)) ∧
      RingHom.IsRigEtaleArrow
        (algebraMap C (TopologicalRing.CompletedTensorProduct (R := B) (M := A) (N := C)))
Tag 0GCX, a lemma

Tag 0GCX in the Stacks Project.

Rig.rigEtale_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmoothStableUnderComposition.lean, line 615.

Stacks Project, Tag 0GCX. Rig-étaleness of arrows of WAdm^Noeth is stable under composition in the sense of Formal Spaces Remark 0GBK: if f : B →+* A and g : C →+* B are continuous rig-étale homomorphisms of Noetherian adic topological rings, then so is f ∘ g.

Condition (6) of Stacks 0GBW for the composite is Rig.finiteTypeAdicAlgebraForEveryIdeal_comp. For rig-étaleness over an ideal of definition I ⊆ C, Stacks 0GCU moves both hypotheses onto I and onto I B, Stacks 0ALM presents A over (C, I) by combining the two presentations, and the two exactness statements of its six-term sequence at the middle complex NL^∧_{A/C} multiply the two annihilating ideals of condition (3) of Stacks 0AJU.

public theorem rigEtale_comp
    {A B C : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [IsNoetherianRing A]
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    [IsNoetherianRing B]
    [CommRing C] [TopologicalSpace C] [IsTopologicalRing C] [IsLinearTopology C C]
    [IsNoetherianRing C]
    (hA : TopologicalRing.IsAdic A) (hB : TopologicalRing.IsAdic B)
    (hC : TopologicalRing.IsAdic C)
    (f : B →+* A) (g : C →+* B) (hf : Continuous f) (hg : Continuous g)
    (hPf : RingHom.IsRigEtale f) (hPg : RingHom.IsRigEtale g) :
    RingHom.IsRigEtale (f.comp g)
Tag 0GCY, a lemma

Tag 0GCY in the Stacks Project.

Rig.rigEtale_hasNoetherianCancellationProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmoothStableUnderComposition.lean, line 834.

Stacks Project, Tag 0GCY. Rig-étaleness on arrows of WAdm^Noeth has the cancellation property of Formal Spaces Remark 0GBP: for f : B →+* A and g : C →+* B continuous homomorphisms of Noetherian adic topological rings, rig-étaleness of g and of f ∘ g implies rig-étaleness of f.

Unlike the base-change bundle of Tag 0GCL and the composition bundle of Tag 0GBK, the cancellation predicate TopologicalRing.HasNoetherianCancellationProperty carries no locality field, so this bundle is exactly what Remark 0GBP defines and exactly what 0GCY asserts; the tag therefore sits on it. Its content is Rig.rigEtale_cancel.

public theorem rigEtale_hasNoetherianCancellationProperty :
    TopologicalRing.HasNoetherianCancellationProperty.{u}
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
        RingHom.IsRigEtaleArrow φ)
Sources
LeanRig.rigEtaleOver_iff_forall_idealOfDefinition · RingHom.IsRigEtale · Rig.rigEtale_propertyIsLocalNoetherian · TopologicalRing.rigEtale_completedTensorProduct_of_isAdic · Rig.rigEtale_comp · Rig.rigEtale_hasNoetherianCancellationProperty

Section88.20 Rig-étale morphisms#

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

Tag 0AQM, a definition

Tag 0AQM in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsRigEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtale.lean, line 73.

Stacks 0AQM. A morphism of formal algebraic spaces over S is rig-étale when every morphism between affine, representable, étale charts of its source and target is induced by a rig-étale continuous homomorphism of adic Noetherian topological rings.

abbrev IsRigEtale (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop
Tag 0GCZ, a lemma

Tag 0GCZ in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigEtale_tfae_of_isLocallyNoetherian', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtaleLocalCharacterizationCharts.lean, line 131.

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

  1. f is rig-étale (Definition 0AQM);
  2. for every commutative square with U, V affine formal algebraic spaces and U ⟶ X, V ⟶ Y representable by algebraic spaces and étale, the morphism U ⟶ V corresponds to a rig-étale map in WAdm^{Noeth};
  3. there exist a covering {Yⱼ ⟶ Y} as in Definition 0AIM and for each j a covering {Xⱼᵢ ⟶ Yⱼ ×_Y X} as in Definition 0AIM such that each Xⱼᵢ ⟶ Yⱼ corresponds to a rig-étale map in WAdm^{Noeth};
  4. there exist a covering {Xᵢ ⟶ X} as in Definition 0AIM and for each i a factorization Xᵢ ⟶ Yᵢ ⟶ Y where Yᵢ is an affine formal algebraic space, Yᵢ ⟶ Y is representable by algebraic spaces and étale, and Xᵢ ⟶ Yᵢ corresponds to a rig-étale map in WAdm^{Noeth};
  5. for every commutative square as in (2), every presentation of U ⟶ V by Noetherian adic rings is rig-étale.

Conditions (1) to (4) are the source's. In (2) the charts U and V are formal spectra of Noetherian adic rings and U ⟶ V is the formal spectrum of a rig-étale homomorphism. Condition (5) is the library's reading of Definition 0AQM, the form condition (2) takes in isRigEtale_tfae_of_isLocallyNoetherian; it is recorded so that this statement contains that one. Conditions (2) and (5) agree by correspondsToRigEtaleMapOnEveryAffineEtaleDiagram_iff, which uses Stacks 0AKX, and the remaining implications are those of isRigEtale_tfae_of_isLocallyNoetherian.

theorem isRigEtale_tfae_of_isLocallyNoetherian' {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y) :
    List.TFAE
      [IsRigEtale B S hS f,
        CorrespondsToRigEtaleMapOnEveryAffineEtaleDiagram B S hS f,
        CorrespondsToRigEtaleMapAfterTargetCover B S hS f,
        CorrespondsToRigEtaleMapAfterSourceCover B S hS f,
        HasPropertyOnEveryAffineEtaleDiagram B S hS IsNoetherianAdic IsRigEtaleHom f]
Tag 0AQN, a lemma

Tag 0AQN in the Stacks Project.

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_of_isRigEtale_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtaleLocallyOfFiniteTypeUnconditional.lean, line 116.

Stacks 0AQN. A rig-étale morphism of locally Noetherian formal algebraic spaces over S is locally of finite type.

By the implication (1) ⟹ (4) of Stacks 0ANW it suffices that every affine representable étale square over f has its upper map given by a taut, topologically of finite type morphism of WAdm^{count}. The two charts of such a square are Noetherian (Stacks 0AKX), so every weakly admissible ring presenting them is Noetherian and adic (Stacks 0AIC); rig-étaleness of f then says that the presenting homomorphism is rig-étale, hence taut and topologically of finite type (Stacks 0GBW).

theorem isLocallyOfFiniteType_of_isRigEtale_of_isLocallyNoetherian {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hf : IsRigEtale B S hS f) :
    IsLocallyOfFiniteType B S hS f
Tag 0GD0, a lemma

Tag 0GD0 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSmooth_of_isRigEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtale.lean, line 118.

Stacks 0GD0. A rig-étale morphism of formal algebraic spaces is rig-smooth.

theorem isRigSmooth_of_isRigEtale (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hf : IsRigEtale B S hS f) :
    IsRigSmooth B S hS f
Tag 0GD1, a lemma

Tag 0GD1 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigEtale_pullback_snd_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtaleBaseChangeCharts.lean, line 212.

Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of locally Noetherian formal algebraic spaces over S. If f is rig-étale and g is adic, then the base change X ×_Y Z ⟶ Z is rig-étale.

theorem isRigEtale_pullback_snd_of_isLocallyNoetherian {X Y Z : FppfSheaf B S hS}
    (f : X ⟶ Y) (g : Z ⟶ Y) (hX : IsLocallyNoetherian B S hS X)
    (hY : IsLocallyNoetherian B S hS Y) (hZ : IsLocallyNoetherian B S hS Z)
    (hf : IsRigEtale B S hS f) (hg : IsAdicMorphism B S hS g) :
    IsRigEtale B S hS (pullback.snd f g)

AlgebraicGeometry.FormalSpace.isRigEtale_pullback_snd_of_isAdicMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtaleStability.lean, line 163. The attribute's comment: “granting the locality of the cohomology-annihilation half of rig-étaleness, which is the hypothesis hcond and the only input of Stacks 0AQL, together with the three inputs of Remark 0GBG that the library leaves open: the covering of X ×_Y Z by fibre products of charts of Stacks 0GBD and 0AN0 (hcover), the implication (3) ⟹ (1) of Stacks 0ANG (h31), and the invariance of rig-étaleness under isomorphism of targets implied by Stacks 0ANI (hiso)”.

Stacks 0GD1. The base change of a rig-étale morphism of locally Noetherian formal algebraic spaces over S by an adic morphism is rig-étale: if f : X ⟶ Y is rig-étale and g : Z ⟶ Y is adic, then X ×_Y Z ⟶ Z is rig-étale.

theorem isRigEtale_pullback_snd_of_isAdicMorphism (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S)
    (hcond : TopologicalRing.PropertyIsLocalNoetherian.{u}
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
        Rig.RigEtaleCondition φ))
    (hiso : PropertyIsInvariantUnderTargetIso.{u}
      (fun {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂] (φ : R₁ →+* R₂) ↦
        RingHom.IsRigEtaleArrow φ))
    (h31 : SourceCoverImpliesEveryAffineEtaleDiagram B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R)
      (fun {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂] (φ : R₁ →+* R₂) ↦
        RingHom.IsRigEtaleArrow φ))
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hcover : HasBaseChangeCoverOverPullbackSnd B S hS f g)
    (_hX : IsLocallyNoetherian B S hS X) (_hY : IsLocallyNoetherian B S hS Y)
    (_hZ : IsLocallyNoetherian B S hS Z)
    (hf : IsRigEtale B S hS f)
    (hg : IsAdicOnEveryAffineEtaleDiagramNoetherian B S hS g) :
    IsRigEtale B S hS (pullback.snd f g)
Tag 0GD2, a lemma

Tag 0GD2 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigEtale_comp_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtaleCompositionCharts.lean, line 196.

Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of locally Noetherian formal algebraic spaces over S. If f and g are rig-étale, then so is g ∘ f.

theorem isRigEtale_comp_of_isLocallyNoetherian {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y)
    (g : Y ⟶ Z) (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hZ : IsLocallyNoetherian B S hS Z) (hf : IsRigEtale B S hS f)
    (hg : IsRigEtale B S hS g) :
    IsRigEtale B S hS (f ≫ g)
Tag 0GD3, a lemma

Tag 0GD3 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigEtale_of_comp_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtaleCompositionCharts.lean, line 229.

Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of locally Noetherian formal algebraic spaces over S. If g ∘ f and g are rig-étale, then so is f.

theorem isRigEtale_of_comp_of_isLocallyNoetherian {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y)
    (g : Y ⟶ Z) (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hZ : IsLocallyNoetherian B S hS Z) (hfg : IsRigEtale B S hS (f ≫ g))
    (hg : IsRigEtale B S hS g) :
    IsRigEtale B S hS f

AlgebraicGeometry.FormalSpace.isRigEtale_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtaleStability.lean, line 137. The attribute's comment: “granting the locality of the cohomology-annihilation half of rig-étaleness, which is the hypothesis hcond and the only input of Stacks 0AQL, and the transfer to formal algebraic spaces of Remark 0GBP, which is the hypothesis htransfer”.

Stacks 0GD3. Rig-étaleness of morphisms of locally Noetherian formal algebraic spaces over S cancels on the right: if g ∘ f and g are rig-étale, for f : X ⟶ Y and g : Y ⟶ Z, then f is rig-étale.

theorem isRigEtale_of_comp (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hcond : TopologicalRing.PropertyIsLocalNoetherian.{u}
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
        Rig.RigEtaleCondition φ))
    (htransfer : TransfersCancellationOnAffineEtaleDiagrams B S hS)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (_hX : IsLocallyNoetherian B S hS X) (_hY : IsLocallyNoetherian B S hS Y)
    (_hZ : IsLocallyNoetherian B S hS Z)
    (hfg : IsRigEtale B S hS (f ≫ g)) (hg : IsRigEtale B S hS g) :
    IsRigEtale B S hS f
Tag 0GH4, a lemma

Tag 0GH4 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigEtale_of_comp_of_isAdicMorphism_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtaleAdicMonomorphism.lean, line 80. The attribute's comment: “granting the locality of the cohomology-annihilation half of rig-étaleness, which is the hypothesis hcond and the only input of Stacks 0AQL, together with the three inputs of Remark 0GBG that the library leaves open and that Stacks 0GD1, the sole cited input of this tag, is itself carried with: the covering by fibre products of charts of Stacks 0GBD and 0AN0 (hcover), the implication (3) ⟹ (1) of Stacks 0ANG (h31), and the invariance of rig-étaleness under isomorphism of targets implied by Stacks 0ANI (hiso)”.

Stacks 0GH4. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of locally Noetherian formal algebraic spaces over S. If g ∘ f is rig-étale and g is an adic monomorphism, then f is rig-étale: as g is a monomorphism, f is the base change of g ∘ f along g, and the base change of a rig-étale morphism along an adic morphism is rig-étale.

theorem isRigEtale_of_comp_of_isAdicMorphism_of_mono (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S)
    (hcond : TopologicalRing.PropertyIsLocalNoetherian.{u}
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
        Rig.RigEtaleCondition φ))
    (hiso : PropertyIsInvariantUnderTargetIso.{u}
      (fun {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂] (φ : R₁ →+* R₂) ↦
        RingHom.IsRigEtaleArrow φ))
    (h31 : SourceCoverImpliesEveryAffineEtaleDiagram B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R)
      (fun {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂] (φ : R₁ →+* R₂) ↦
        RingHom.IsRigEtaleArrow φ))
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hcover : HasBaseChangeCoverOverPullbackSnd B S hS (f ≫ g) g)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hZ : IsLocallyNoetherian B S hS Z)
    (hfg : IsRigEtale B S hS (f ≫ g))
    (hgadic : IsAdicOnEveryAffineEtaleDiagramNoetherian B S hS g) (hgmono : Mono g) :
    IsRigEtale B S hS f

AlgebraicGeometry.FormalSpace.isRigEtale_of_comp_of_isAdicMorphism_of_mono_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtaleBaseChangeCharts.lean, line 224.

Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of locally Noetherian formal algebraic spaces over S. If g ∘ f is rig-étale and g is an adic monomorphism, then f is rig-étale.

theorem isRigEtale_of_comp_of_isAdicMorphism_of_mono_of_isLocallyNoetherian
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z) (hX : IsLocallyNoetherian B S hS X)
    (hY : IsLocallyNoetherian B S hS Y) (hZ : IsLocallyNoetherian B S hS Z)
    (hfg : IsRigEtale B S hS (f ≫ g)) (hgadic : IsAdicMorphism B S hS g) (hgmono : Mono g) :
    IsRigEtale B S hS f
Tag 0GD4, a lemma

Tag 0GD4 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSmooth_tfae_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtaleClosedImmersion.lean, line 250. The attribute's comment: “the full equivalence of the three conditions, with Stacks 0AQI (the fibre product chart map being a surjection of WAdm^Noeth which is adic of topologically finite type) and Stacks 0GCZ (rig-étaleness need only be checked on the ring maps appearing in condition (3)) carried as the hypotheses hAQI and hGCZ”.

Stacks 0GD4. For a closed immersion f : X ⟶ Y of locally Noetherian formal algebraic spaces over S, rig-smoothness of f (Definition 0GCP), rig-étaleness of f (Definition 0AQM), and the condition that on every affine representable étale chart V ⟶ Y of the target the fibre product X ×_Y V ⟶ V be given by a surjection of WAdm^{Noeth} whose kernel J has J / J² annihilated by an ideal of definition of the source, are all equivalent.

The implication (2) ⟹ (1) is Stacks 0GD0. The implications (1) ⟹ (3) and (3) ⟹ (2) rest on the computation of the completed naive cotangent complex of a surjection, for which both rigidity notions reduce to the annihilation of the conormal module. The hypotheses hAQI and hGCZ carry Stacks 0AQI — that the fibre product chart map is a surjection which is adic of topologically finite type — and Stacks 0GCZ in the form in which the source's proof uses it, that rig-étaleness need only be checked on the ring maps appearing in (3).

theorem isRigSmooth_tfae_of_isClosedImmersion {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (_hX : IsLocallyNoetherian B S hS X) (_hY : IsLocallyNoetherian B S hS Y)
    (hf : IsClosedImmersion B S hS f)
    (hAQI : HasAdicQuotientOnPullbackCharts B S hS f)
    (hGCZ : HasRigEtaleOnPullbackCharts B S hS f → IsRigEtale B S hS f) :
    List.TFAE
      [IsRigSmooth B S hS f, IsRigEtale B S hS f,
        HasAnnihilatedConormalOnPullbackCharts B S hS f]

AlgebraicGeometry.FormalSpace.isRigSmooth_tfae_of_isClosedImmersion', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigEtaleClosedImmersionCharts.lean, line 401.

Stacks 0GD4. For a closed immersion f : X ⟶ Y of locally Noetherian formal algebraic spaces over S, rig-smoothness of f (Definition 0GCP), rig-étaleness of f (Definition 0AQM), and the condition that on every affine representable étale chart V ⟶ Y of the target the fibre product X ×_Y V ⟶ V be given by a surjection of WAdm^{Noeth} whose kernel J has J / J² annihilated by an ideal of definition of the source, are all equivalent.

The implication (2) ⟹ (1) is Stacks 0GD0. The implication (1) ⟹ (3) uses the surjectivity of the fibre product chart homomorphism, surjective_of_isClosedImmersion_chart, and the computation of the completed naive cotangent complex of a surjection. The implication (3) ⟹ (2) is isRigEtale_of_hasAnnihilatedConormalOnPullbackCharts.

theorem isRigSmooth_tfae_of_isClosedImmersion' {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (_hX : IsLocallyNoetherian B S hS X) (_hY : IsLocallyNoetherian B S hS Y)
    (hf : IsClosedImmersion B S hS f) :
    List.TFAE
      [IsRigSmooth B S hS f, IsRigEtale B S hS f,
        HasAnnihilatedConormalOnPullbackCharts B S hS f]
Sources
LeanAlgebraicGeometry.FormalSpace.IsRigEtale · AlgebraicGeometry.FormalSpace.isRigEtale_tfae_of_isLocallyNoetherian' · AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_of_isRigEtale_of_isLocallyNoetherian · AlgebraicGeometry.FormalSpace.isRigSmooth_of_isRigEtale · AlgebraicGeometry.FormalSpace.isRigEtale_pullback_snd_of_isLocallyNoetherian · AlgebraicGeometry.FormalSpace.isRigEtale_pullback_snd_of_isAdicMorphism · AlgebraicGeometry.FormalSpace.isRigEtale_comp_of_isLocallyNoetherian · AlgebraicGeometry.FormalSpace.isRigEtale_of_comp_of_isLocallyNoetherian

Section88.21 Rig-surjective morphisms#

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

Tag 0AQQ, a definition

Tag 0AQQ in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsRigSurjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjective.lean, line 116.

Stacks 0AQQ. A morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S is rig-surjective when every adic morphism p : Spf R ⟶ Y out of the formal spectrum of a complete discrete valuation ring R lifts to X along the formal spectrum of an extension R ⊂ R' of complete discrete valuation rings. Adic means representable by algebraic spaces, which is the definition of an adic morphism, Stacks 0AQ3.

The source defines the notion for a morphism of locally Noetherian formal algebraic spaces that is locally of finite type. The predicate drops those standing hypotheses and asks for the same lifting condition for any morphism of fppf sheaves. Under them it is the source's definition.

abbrev IsRigSurjective (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop
Tag 0AQZ, a remark

Tag 0AQZ in the Stacks Project.

AlgebraicGeometry.FormalSpace.FractionalPowers.not_isAdic_toDiscreteValuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/NoAdicDiscreteValuationPoints.lean, line 225.

Stacks 0AQZ. No ring map from A = (⋃_{n ≥ 1} k[t^{1/n}])^∧, carrying its t-adic topology, to a complete discrete valuation ring R, carrying its maximal-adic topology, is adic. Since a morphism Spf R ⟶ Spf A of affine formal algebraic spaces is Spf of a continuous ring map A → R by Stacks 0AN0, there are therefore no adic morphisms Spf R ⟶ Spf A, and every morphism X ⟶ Spf A satisfies the lifting condition of Stacks 0AQQ vacuously, although t is a nonzero element of A.

theorem not_isAdic_toDiscreteValuationRing [TopologicalSpace (Completion k)]
    [IsTopologicalRing (Completion k)]
    (hA : _root_.IsAdic (Ideal.span {completionGenerator k})) (R : Type*) [CommRing R]
    [IsDomain R] [IsDiscreteValuationRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    (hR : _root_.IsAdic (IsLocalRing.maximalIdeal R)) (φ : Completion k →+* R) : ¬ φ.IsAdic
Tag 0AQR, a lemma

Tag 0AQR in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsRigSurjective.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjective.lean, line 171. The attribute's comment: “assuming Stacks 0AN5 and, for the second factor, Stacks 0AQ0”.

Stacks 0AQR, carrying two hypotheses. A composite of rig-surjective morphisms of formal algebraic spaces over S which are locally of finite type is locally of finite type and rig-surjective: an adic point of the final target lifts through the second factor over an extension of complete discrete valuation rings, that lift is again adic, and so lifts through the first factor over a further extension; the two extensions compose to one.

Adicness of the intermediate lift is hcancel, which is Stacks 0AQ0 for the second factor, applied to the composite made representable by hformalSpectrumMap, which is Stacks 0AN5, (3) implies (1); neither is available in this library.

theorem IsRigSurjective.comp (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsLocallyOfFiniteType B S hS f) (hg : IsLocallyOfFiniteType B S hS g)
    (hformalSpectrumMap : ∀ (A₁ A₂ : Type u) [CommRing A₁] [TopologicalSpace A₁]
      [IsTopologicalRing A₁] [IsLinearTopology A₁ A₁] [CommRing A₂] [TopologicalSpace A₂]
      [IsTopologicalRing A₂] (hA₁ : TopologicalRing.IsWeaklyAdmissible A₁)
      (D₁ : QuotientSystem B S hS A₁) (D₂ : QuotientSystem B S hS A₂)
      (φ : ContinuousHom D₁ D₂), RingHom.IsTaut φ.toRingHom →
      Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (formalSpectrumMap hA₁ φ).hom)
    (hcancel : ∀ {W : FppfSheaf B S hS} (q : W ⟶ Y),
      Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (q.hom ≫ g.hom) →
      Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS q.hom)
    (hsf : IsRigSurjective B S hS f) (hsg : IsRigSurjective B S hS g) :
    IsLocallyOfFiniteType B S hS (f ≫ g) ∧ IsRigSurjective B S hS (f ≫ g)

AlgebraicGeometry.FormalSpace.IsRigSurjective.comp_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveComposition.lean, line 150.

Stacks 0AQR. A composite of rig-surjective morphisms of formal algebraic spaces over S which are locally of finite type is locally of finite type and rig-surjective: an adic point of the final target lifts through the second factor over an extension of complete discrete valuation rings, that lift is again adic, and so lifts through the first factor over a further extension; the two extensions compose to one.

Adicness of the intermediate lift is Stacks 0AQ0 for the second factor, applied to the composite made representable by the implication (3) ⟹ (1) of Stacks 0AN5. The hypothesis hY is what Stacks 0AQ0 asks of the source of the second factor, and the source of Stacks 0AQR assumes it of Y in the stronger form of a locally Noetherian formal algebraic space.

theorem IsRigSurjective.comp_of_isFormalAlgebraicSpace
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hY : IsFormalAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) (hg : IsLocallyOfFiniteType B S hS g)
    (hsf : IsRigSurjective B S hS f) (hsg : IsRigSurjective B S hS g) :
    IsLocallyOfFiniteType B S hS (f ≫ g) ∧ IsRigSurjective B S hS (f ≫ g)
Tag 0AQS, a lemma

Tag 0AQS in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsRigSurjective.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveBaseChange.lean, line 80.

Stacks 0AQS. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of formal algebraic spaces over S which are locally of finite type. A base change p : W ⟶ Z of f along g is locally of finite type, and is rig-surjective as soon as f is.

An adic point of Z out of the formal spectrum of a complete discrete valuation ring becomes, after composition with g, an adic point of Y, because g is representable by algebraic spaces; a lift of it to X over an extension of complete discrete valuation rings pairs with the point of Z to give a lift to W.

theorem IsRigSurjective.of_isPullback {W X Y Z : FppfSheaf B S hS}
    {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y} (sq : IsPullback p q g f)
    (hf : IsLocallyOfFiniteType B S hS f) (hg : IsLocallyOfFiniteType B S hS g)
    (hsf : IsRigSurjective B S hS f) :
    IsLocallyOfFiniteType B S hS p ∧ IsRigSurjective B S hS p

AlgebraicGeometry.FormalSpace.hasRigSurjectiveOnPullbackCharts_of_isRigSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveClosedImmersionCharts.lean, line 612. The attribute's comment: “the chart shape in which the proof of Stacks 0GD5 uses it, carrying nothing beyond rig-surjectivity of f: a chart which is representable by algebraic spaces and etale is in particular representable, so the base change of f along it is rig-surjective, and the presenting isomorphisms of the chart are stripped off by Stacks 0AQT and its postcomposition companion. Local finite typeness of f and of the chart, which the source assumes, is used by the source only for the conclusion that the base change is locally of finite type, which is not asserted here”.

Stacks 0AQS in the chart shape in which the proof of Stacks 0GD5 uses it: a rig-surjective morphism has rig-surjective chart base changes, presented as formal spectra of the chart homomorphisms. Nothing is carried.

A chart b : V ⟶ Y which is representable by algebraic spaces and étale is in particular representable by algebraic spaces, so AlgebraicGeometry.FormalSpace.IsRigSurjective.of_isPullback_of_representable makes the chart base change t rig-surjective; local finite typeness of f, which Stacks 0AQS assumes, enters that lemma only through the conclusion that the base change is locally of finite type, which is not asserted here. The presenting isomorphisms of the chart are then stripped off by Stacks 0AQT and its postcomposition companion, which is the step the module documentation used to record as missing.

theorem hasRigSurjectiveOnPullbackCharts_of_isRigSurjective {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hf : IsRigSurjective B S hS f) :
    HasRigSurjectiveOnPullbackCharts B S hS f

AlgebraicGeometry.FormalSpace.IsRigSurjective.of_isPullback_of_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveRigEtaleDiagonal.lean, line 198. The attribute's comment: “rig-surjectivity alone, for a base change along a morphism assumed only representable by algebraic spaces rather than locally of finite type”.

Stacks 0AQS, with both hypotheses that AlgebraicGeometry.FormalSpace.IsRigSurjective.of_isPullback makes on local finite typeness dropped. A base change of a rig-surjective morphism of formal algebraic spaces over S along a morphism representable by algebraic spaces is rig-surjective.

An adic point of Z out of the formal spectrum of a complete discrete valuation ring becomes, after composition with g, an adic point of Y, because g is representable by algebraic spaces; a lift of it to X over an extension of complete discrete valuation rings pairs with the point of Z to give a lift to W. Local finite typeness of g enters Stacks 0AQS only through this use of representability, and local finite typeness of f only through the conclusion that the base change is locally of finite type, which is not asserted here.

theorem IsRigSurjective.of_isPullback_of_representable {W X Y Z : FppfSheaf B S hS}
    {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y} (sq : IsPullback p q g f)
    (hgrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS g.hom)
    (hsf : IsRigSurjective B S hS f) :
    IsRigSurjective B S hS p
Tag 0GH5, a lemma

Tag 0GH5 in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsRigSurjective.of_comp_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveMonomorphism.lean, line 75.

Stacks 0GH5. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of locally Noetherian formal algebraic spaces over S which are locally of finite type. If g ∘ f is rig-surjective and g is a monomorphism, then f is rig-surjective.

As g is a monomorphism, the square with sides 𝟙 X and f over g ∘ f and g is cartesian, so f is the base change of g ∘ f along g; and the base change of a rig-surjective morphism locally of finite type along a morphism locally of finite type is rig-surjective, by Stacks 0AQS.

theorem IsRigSurjective.of_comp_of_mono {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsLocallyOfFiniteType B S hS f) (hg : IsLocallyOfFiniteType B S hS g)
    (hsfg : IsRigSurjective B S hS (f ≫ g)) (hgmono : Mono g) :
    IsRigSurjective B S hS f
Tag 0AQT, a lemma

Tag 0AQT in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsRigSurjective.of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjective.lean, line 138.

Stacks 0AQT. If a composition of morphisms of formal algebraic spaces over S is rig-surjective, then so is its second factor: a lift of an adic point of the final target to the initial source is, after composition with the first factor, a lift to the intermediate space.

theorem IsRigSurjective.of_comp (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hgf : IsRigSurjective B S hS (f ≫ g)) :
    IsRigSurjective B S hS g
Tag 0AQU, a lemma

Tag 0AQU in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSurjective_of_isSurjective_of_isRepresentableEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleAdicPointLift.lean, line 629.

Stacks 0AQU. A morphism of fppf sheaves over S which is representable by algebraic spaces, étale and surjective is rig-surjective.

Let p : Spf R ⟶ Y be an adic morphism out of the formal spectrum of a complete discrete valuation ring. The closed point of Spf R maps to a point of Y, which by surjectivity is the image of a point of X; together they give a point of Spf R ×_Y X (AlgebraicGeometry.Space.exists_point_of_isPullbackULift), and exists_lift_of_pointsULift_pullback_of_isRepresentableEtale turns that point into the lift the definition of rig-surjectivity asks for.

The source states this for locally Noetherian formal algebraic spaces X and Y; neither hypothesis is used, so neither is assumed. Nor is adicness of p: the lift exists for every morphism out of the formal spectrum of a complete discrete valuation ring.

theorem isRigSurjective_of_isSurjective_of_isRepresentableEtale {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hf : IsRepresentableEtale B S hS f) (hsurj : IsSurjective B S hS f) :
    IsRigSurjective B S hS f

AlgebraicGeometry.FormalSpace.isRigSurjective_of_isRepresentableEtale_of_isSurjective', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveEtaleSurjectiveRefined.lean, line 59.

A morphism of locally Noetherian formal algebraic spaces over S which is representable by algebraic spaces, étale and surjective is rig-surjective.

theorem isRigSurjective_of_isRepresentableEtale_of_isSurjective'
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hf : IsRepresentableEtale B S hS f) (hsurj : IsSurjective B S hS f) :
    IsRigSurjective B S hS f
Tag 0AQV, a lemma

Tag 0AQV in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSurjective_iff_forall_pullback_snd_of_isRepresentableEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/JointlyRigSurjectiveEtale.lean, line 129.

Stacks 0AQV. Let f : X ⟶ Y be a morphism of fppf sheaves over S which is locally of finite type and let {gᵢ : Yᵢ ⟶ Y} be a family of morphisms from formal algebraic spaces which are representable by algebraic spaces and étale and which is jointly surjective on points (that is, ∐ gᵢ is surjective). Then f is rig-surjective if and only if each base change fᵢ : X ×_Y Yᵢ ⟶ Yᵢ is rig-surjective.

This is isRigSurjective_iff_forall_pullback_snd' together with joint rig-surjectivity of the family, which is the family form of Stacks 0AQU, isJointlyRigSurjective_of_isRepresentableEtale_of_isJointlySurjective: the source's proof applies Stacks 0AQU to ∐ gᵢ, and that form avoids the coproduct by catching each adic point in one member of the family.

The source states this for locally Noetherian formal algebraic spaces X, Y and Yᵢ. Only that the Yᵢ are formal algebraic spaces is used; the locally Noetherian hypotheses and the hypotheses on X and Y are omitted.

theorem isRigSurjective_iff_forall_pullback_snd_of_isRepresentableEtale (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) {I : Type v} {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (Yi : I → FppfSheaf B S hS) (g : ∀ i, Yi i ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f)
    (hYi : ∀ i, IsFormalAlgebraicSpace B S hS (Yi i))
    (hg : ∀ i, IsRepresentableEtale B S hS (g i))
    (hcover : IsJointlySurjective B S hS Yi g) :
    IsRigSurjective B S hS f ↔ ∀ i, IsRigSurjective B S hS (pullback.snd f (g i))

AlgebraicGeometry.FormalSpace.isRigSurjective_iff_forall_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveEtaleLocal.lean, line 155. The attribute's comment: “both directions, assuming that a representable étale morphism is locally of finite type (hetaleFiniteType) and that a jointly surjective family of representable étale morphisms is jointly rig-surjective, which is Stacks 0AQU for the coproduct of the family together with the factorization of an adic point of a coproduct through a summand (h0AQU)”.

Stacks 0AQV, both directions, carrying two hypotheses. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S which is locally of finite type and let {gᵢ : Yᵢ ⟶ Y} be a family of representable étale morphisms which is jointly surjective on points. Then f is rig-surjective exactly when each base change X ×_Y Yᵢ ⟶ Yᵢ is rig-surjective.

The forward direction is Stacks 0AQS. For the converse an adic point of Y out of a complete discrete valuation ring is lifted to one Yᵢ over an extension of complete discrete valuation rings, using that the family is jointly rig-surjective, and then lifted through that base change over a further extension; the projection to X makes the result a lift through f, and the two extensions compose to one.

The two hypotheses are hetaleFiniteType, that a representable étale morphism is locally of finite type (Stacks 0AJG for Definition 0AM4), and h0AQU, that a jointly surjective family of representable étale morphisms is jointly rig-surjective (Stacks 0AQU for ∐ gᵢ, together with the factorization of an adic point of a coproduct through a summand); neither is available in this library.

theorem isRigSurjective_iff_forall_pullback_snd (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {I : Type v} {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (Yi : I → FppfSheaf B S hS) (g : ∀ i, Yi i ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f)
    (hg : ∀ i, IsRepresentableEtale B S hS (g i))
    (hcover : IsJointlySurjective B S hS Yi g)
    (hetaleFiniteType : ∀ {U V : FppfSheaf B S hS} (w : U ⟶ V),
      IsRepresentableEtale B S hS w → IsLocallyOfFiniteType B S hS w)
    (h0AQU : ∀ {V : FppfSheaf B S hS} {J : Type v} (Vj : J → FppfSheaf B S hS)
      (v : ∀ j, Vj j ⟶ V), (∀ j, IsRepresentableEtale B S hS (v j)) →
      IsJointlySurjective B S hS Vj v → IsJointlyRigSurjective B S hS Vj v) :
    IsRigSurjective B S hS f ↔ ∀ i, IsRigSurjective B S hS (pullback.snd f (g i))
Tag 0AQX, a lemma

Tag 0AQX in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSurjective_formalSpectrumMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveCriterion.lean, line 191.

Let A be a Noetherian ring complete with respect to an ideal I, and let C be an I-adically complete A-algebra. If A/Iⁿ → C/IⁿC is of finite type and flat for every n, and faithfully flat for n = 1, then Spf C → Spf A is rig-surjective.

theorem isRigSurjective_formalSpectrumMap
    {A C : Type u} [CommRing A] [CommRing C] [Algebra A C]
    [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [TopologicalSpace C] [IsTopologicalRing C] [IsLinearTopology C C]
    [IsNoetherianRing A] (I : Ideal A)
    (hAadic : IsAdic I) (hAcomplete : IsAdicComplete I A)
    (hCadic : IsAdic (I.map (algebraMap A C)))
    (hCcomplete : IsAdicComplete (I.map (algebraMap A C)) C)
    (hfinite : ∀ n : ℕ,
      Algebra.FiniteType (A ⧸ I ^ n) (C ⧸ (I ^ n).map (algebraMap A C)))
    (hflat : ∀ n : ℕ, Module.Flat (A ⧸ I ^ n) (C ⧸ (I ^ n).map (algebraMap A C)))
    (hfaithful : Module.FaithfullyFlat (A ⧸ I) (C ⧸ I.map (algebraMap A C)))
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C)
    (f : ContinuousHom D E) (hf : f.toRingHom = algebraMap A C) :
    IsRigSurjective B S hS
      (formalSpectrumMap
        (TopologicalRing.isWeaklyAdmissible_of_isAdic hAadic hAcomplete) f)
Tag 0AQY, a lemma

Tag 0AQY in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSurjective_formalSpectrumMap_iff_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveFaithfullyFlat.lean, line 406. The attribute's comment: “modulo Stacks 0AN5 part (3) implies part (1) for the adic point, carried as hAdicRepresentable”.

Stacks 0AQY. Let A be a Noetherian ring complete with respect to an ideal I whose I-torsion vanishes, and let C be an I-adically complete A-algebra such that A/Iⁿ → C/IⁿC is flat and of finite type for every n. Then Spf C → Spf A is rig-surjective if and only if A/I → C/IC is faithfully flat.

Faithful flatness gives rig-surjectivity by Stacks 0AQX. Conversely, a closed point of Spec(A/I) is a maximal ideal I ⊆ 𝔪 ⊆ A, and exists_isPrime_comap_eq_of_isRigSurjective contracts a prime of C onto it; so Spec(C/IC) → Spec(A/I) meets every closed point, which for a flat map is faithful flatness (Stacks 00HQ).

theorem isRigSurjective_formalSpectrumMap_iff_faithfullyFlat (I : Ideal A)
    (hAadic : IsAdic I) (hAcomplete : IsAdicComplete I A)
    (hCadic : IsAdic (I.map (algebraMap A C)))
    (hCcomplete : IsAdicComplete (I.map (algebraMap A C)) C)
    (hTorsion : Submodule.torsionBySet A A (I : Set A) = ⊥)
    (hfinite : ∀ n : ℕ, Algebra.FiniteType (A ⧸ I ^ n) (C ⧸ (I ^ n).map (algebraMap A C)))
    (hflat : ∀ n : ℕ, Module.Flat (A ⧸ I ^ n) (C ⧸ (I ^ n).map (algebraMap A C)))
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C)
    (f : ContinuousHom D E) (hf : f.toRingHom = algebraMap A C)
    (hAdicRepresentable : ∀ (R : Type u) [CommRing R] [TopologicalSpace R]
      [IsTopologicalRing R] [IsLinearTopology R R], TopologicalRing.IsWeaklyAdmissible R →
      ∀ (DR : QuotientSystem B S hS R)
      (q : ContinuousHom D DR), RingHom.IsAdic q.toRingHom →
        Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
          (formalSpectrumMap
            (TopologicalRing.isWeaklyAdmissible_of_isAdic hAadic hAcomplete) q).hom) :
    IsRigSurjective B S hS
      (formalSpectrumMap
        (TopologicalRing.isWeaklyAdmissible_of_isAdic hAadic hAcomplete) f) ↔
      Module.FaithfullyFlat (A ⧸ I) (C ⧸ I.map (algebraMap A C))

AlgebraicGeometry.FormalSpace.isRigSurjective_formalSpectrumMap_iff_faithfullyFlat', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveFaithfullyFlatUnconditional.lean, line 226.

Stacks 0AQY. Let A be a Noetherian ring complete with respect to an ideal I whose I-torsion vanishes, and let C be an I-adically complete A-algebra such that A/Iⁿ → C/IⁿC is flat and of finite type for every n. Then Spf C → Spf A is rig-surjective if and only if A/I → C/IC is faithfully flat.

Faithful flatness gives rig-surjectivity by Stacks 0AQX. Conversely, a closed point of Spec(A/I) is a maximal ideal I ⊆ 𝔪 ⊆ A, and exists_isPrime_comap_eq_of_isRigSurjective' contracts a prime of C onto it; so Spec(C/IC) → Spec(A/I) meets every closed point, which for a flat map is faithful flatness (Stacks 00HQ).

theorem isRigSurjective_formalSpectrumMap_iff_faithfullyFlat' (I : Ideal A)
    (hAadic : IsAdic I) (hAcomplete : IsAdicComplete I A)
    (hCadic : IsAdic (I.map (algebraMap A C)))
    (hCcomplete : IsAdicComplete (I.map (algebraMap A C)) C)
    (hTorsion : Submodule.torsionBySet A A (I : Set A) = ⊥)
    (hfinite : ∀ n : ℕ, Algebra.FiniteType (A ⧸ I ^ n) (C ⧸ (I ^ n).map (algebraMap A C)))
    (hflat : ∀ n : ℕ, Module.Flat (A ⧸ I ^ n) (C ⧸ (I ^ n).map (algebraMap A C)))
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C)
    (f : ContinuousHom D E) (hf : f.toRingHom = algebraMap A C) :
    IsRigSurjective B S hS
      (formalSpectrumMap
        (TopologicalRing.isWeaklyAdmissible_of_isAdic hAadic hAcomplete) f) ↔
      Module.FaithfullyFlat (A ⧸ I) (C ⧸ I.map (algebraMap A C))
Tag 0AR0, a lemma

Tag 0AR0 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSurjective_iff_factorsAdicCompleteDvrPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveDvrCriterion.lean, line 383.

Stacks 0AR0. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S with X and Y locally Noetherian, f locally of finite type and f a monomorphism. Then f is rig-surjective if and only if every adic morphism Spf R ⟶ Y, with R a complete discrete valuation ring, factors through X.

The forward implication uses that X and Y are fpqc sheaves, Stacks 0AQD, AlgebraicGeometry.FormalSpace.isSheaf_fpqc.

theorem isRigSurjective_iff_factorsAdicCompleteDvrPoints {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hft : IsLocallyOfFiniteType B S hS f) [Mono f] :
    IsRigSurjective B S hS f ↔ FactorsAdicCompleteDvrPoints B S hS f
Tag 0GD5, a lemma

Tag 0GD5 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSurjective_iff_hasAnnihilatedKerPowOnPullbackCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveClosedImmersion.lean, line 404. The attribute's comment: “both directions, carrying three hypotheses: Stacks 0AQI in the chart form of Stacks 0GD4, that the chart homomorphism is a surjection of WAdm^Noeth which is adic of topologically finite type (hAQI); the equivalence of rig-surjectivity of f with rig-surjectivity of its chart base changes, which is Stacks 0AQS forwards and Stacks 0AQV backwards (hAQV); and Stacks 0AR0 for the chart maps, read through the full faithfulness of Spf of Stacks 0AN0, identifying rig-surjectivity of a chart map with the factorisation of its adic discrete valuation points (hAR0). The algebraic equivalence joining the factorisation criterion to the annihilation condition, which is what the source's two implications come down to and which uses Stacks 00PH, is proved”.

Stacks 0GD5, both directions, carrying three hypotheses. Let f : X ⟶ Y be a closed immersion of locally Noetherian formal algebraic spaces over S. Then f is rig-surjective exactly when on every affine representable étale chart V ⟶ Y of the target the fibre product X ×_Y V ⟶ V is given by a surjection of WAdm^{Noeth} some ideal of definition of whose source annihilates a positive power of its kernel.

The hypothesis hAQI is Stacks 0AQI in the chart form of Stacks 0GD4, hAQV is the equivalence of rig-surjectivity of f with rig-surjectivity of its chart base changes (Stacks 0AQS forwards, Stacks 0AQV backwards), and hAR0 is Stacks 0AR0 for the chart maps, read through the full faithfulness of Spf. The passage from the factorisation criterion to the annihilation condition is the algebraic equivalence proved here, which uses Stacks 00PH.

theorem isRigSurjective_iff_hasAnnihilatedKerPowOnPullbackCharts {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (_hX : IsLocallyNoetherian B S hS X) (_hY : IsLocallyNoetherian B S hS Y)
    (_hf : IsClosedImmersion B S hS f)
    (hAQI : HasAdicQuotientOnPullbackCharts B S hS f)
    (hAQV : IsRigSurjective B S hS f ↔ HasRigSurjectiveOnPullbackCharts B S hS f)
    (hAR0 : HasRigSurjectiveOnPullbackCharts B S hS f ↔
      HasDvrFactorizationOnPullbackCharts B S hS f) :
    IsRigSurjective B S hS f ↔ HasAnnihilatedKerPowOnPullbackCharts B S hS f

AlgebraicGeometry.FormalSpace.isRigSurjective_iff_hasAnnihilatedKerPow_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveClosedImmersionAtlas.lean, line 92.

Stacks 0GD5. Let f : X ⟶ Y be a closed immersion of locally Noetherian formal algebraic spaces over S. Then f is rig-surjective if and only if for every affine formal algebraic space V and every morphism V ⟶ Y which is representable by algebraic spaces and étale, the base change X ×_Y V ⟶ V corresponds to a surjection B → A of WAdm^{Noeth} whose kernel J satisfies I J ^ n = 0 for some ideal of definition I of B and some n ≥ 1.

Condition (2) is AlgebraicGeometry.FormalSpace.HasAnnihilatedKerPowOnPullbackCharts, asked of every presentation of the base change by Noetherian rings with adic topologies. The equivalence of condition (2) with rig-surjectivity of every chart map is AlgebraicGeometry.FormalSpace.hasAnnihilatedKerPow_iff_hasRigSurjective_of_isClosedImmersion (Stacks 0AQI, 0AR0 and 00PH). Rig-surjectivity of f gives that of the chart maps by Stacks 0AQS, AlgebraicGeometry.FormalSpace.hasRigSurjectiveOnPullbackCharts_of_isRigSurjective, and conversely by Stacks 0AQV, AlgebraicGeometry.FormalSpace.isRigSurjective_of_hasRigSurjectiveOnPullbackCharts.

theorem isRigSurjective_iff_hasAnnihilatedKerPow_of_isClosedImmersion {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hf : IsClosedImmersion B S hS f) :
    IsRigSurjective B S hS f ↔ HasAnnihilatedKerPowOnPullbackCharts B S hS f
Tag 0GD6, a lemma

Tag 0GD6 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSmooth_and_isRigSurjective_tfae_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmoothRigSurjectiveClosedImmersion.lean, line 253. The attribute's comment: “all three conditions and every implication between them, carrying exactly the four hypotheses which this library's Stacks 0GD4 and Stacks 0GD5 already carry and nothing more: Stacks 0AQI in the chart form of Stacks 0GD4, that the chart homomorphism is a surjection of WAdm^Noeth which is adic of topologically finite type (hAQI), whose library carrier covers only the countably indexed case, which the Noetherian charts here are not; Stacks 0GCZ read as the proof of Stacks 0GD4 reads it, that rig-etaleness of f need only be checked on the ring maps appearing in condition (3) (hGCZ); the equivalence of rig-surjectivity of f with rig-surjectivity of its chart base changes, Stacks 0AQS forwards and Stacks 0AQV backwards (hAQV), undischargeable because Tag 0AJG, IsEtaleULift implies IsLocallyOfFiniteTypeULift, has no carrier in this library; and Stacks 0AR0 for the chart maps read through the full faithfulness of Spf of Stacks 0AN0 (hAR0), undischargeable because its substantial direction rests on the EXISTENCE half of Tag 0AQD, whose carriers supply uniqueness only. No carried hypothesis is an implication of this lemma. The combination the source calls trivial is proved, including the ring-theoretic observation the source omits: I * J ^ n = 0 together with I * J <= J ^ 2 forces I ^ n * J = 0”.

Stacks 0GD6. Let f : X ⟶ Y be a closed immersion of locally Noetherian formal algebraic spaces over S. Then the following are equivalent: (1) f is rig-smooth and rig-surjective; (2) f is rig-étale and rig-surjective; (3) on every affine representable étale chart V ⟶ Y of the target the fibre product X ×_Y V ⟶ V is given by a surjection of WAdm^{Noeth} whose kernel is annihilated by some ideal of definition of the source.

The equivalence of the two rigidity notions is Stacks 0GD4, the identification of rig-surjectivity with the annihilation of a power of the kernel is Stacks 0GD5, and the passage from "a power of J is annihilated and J / J ^ 2 is annihilated" to "J is annihilated" is Rig.exists_idealOfDefinition_mul_eq_bot, the ring-theoretic step whose proof the source omits.

The hypotheses hAQI, hGCZ, hAQV and hAR0 are precisely the ones the library's Stacks 0GD4 and Stacks 0GD5 carry: Stacks 0AQI in chart form, Stacks 0GCZ as the proof of Stacks 0GD4 uses it, the equivalence of rig-surjectivity of f with rig-surjectivity of its chart base changes (Stacks 0AQS forwards, Stacks 0AQV backwards), and Stacks 0AR0 for the chart maps read through Stacks 0AN0.

theorem isRigSmooth_and_isRigSurjective_tfae_of_isClosedImmersion {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hf : IsClosedImmersion B S hS f)
    (hAQI : HasAdicQuotientOnPullbackCharts B S hS f)
    (hGCZ : HasRigEtaleOnPullbackCharts B S hS f → IsRigEtale B S hS f)
    (hAQV : IsRigSurjective B S hS f ↔ HasRigSurjectiveOnPullbackCharts B S hS f)
    (hAR0 : HasRigSurjectiveOnPullbackCharts B S hS f ↔
      HasDvrFactorizationOnPullbackCharts B S hS f) :
    List.TFAE
      [IsRigSmooth B S hS f ∧ IsRigSurjective B S hS f,
        IsRigEtale B S hS f ∧ IsRigSurjective B S hS f,
        HasAnnihilatedKerOnPullbackCharts B S hS f]

AlgebraicGeometry.FormalSpace.isRigSmooth_and_isRigSurjective_tfae_of_isClosedImmersion', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmoothRigSurjectiveClosedImmersionCharts.lean, line 65.

Stacks 0GD6. Let f : X ⟶ Y be a closed immersion of locally Noetherian formal algebraic spaces over S. Then the following are equivalent: (1) f is rig-smooth and rig-surjective; (2) f is rig-étale and rig-surjective; (3) on every affine representable étale chart V ⟶ Y of the target the fibre product X ×_Y V ⟶ V is given by a surjection of WAdm^{Noeth} whose kernel is annihilated by some ideal of definition of the source.

The equivalence of the two rigidity notions with the annihilation of the conormal module J / J ^ 2 is Stacks 0GD4, the identification of rig-surjectivity with the annihilation of a power of the kernel is Stacks 0GD5, and the passage from "a power of J is annihilated and J / J ^ 2 is annihilated" to "J is annihilated" is Rig.exists_idealOfDefinition_mul_eq_bot, applied chart by chart in hasAnnihilatedKer_of_hasAnnihilatedConormal_of_hasAnnihilatedKerPow.

theorem isRigSmooth_and_isRigSurjective_tfae_of_isClosedImmersion' {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hf : IsClosedImmersion B S hS f) :
    List.TFAE
      [IsRigSmooth B S hS f ∧ IsRigSurjective B S hS f,
        IsRigEtale B S hS f ∧ IsRigSurjective B S hS f,
        HasAnnihilatedKerOnPullbackCharts B S hS f]
Tag 0GH6, a lemma

Tag 0GH6 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSmooth_of_comp_of_isRigSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmoothRigSurjectiveDescent.lean, line 292. The attribute's comment: “the rig-smooth case, assuming Stacks 0GCK (hlocal), the transfer of Remark 0GBG to formal algebraic spaces (htransfer), that a representable étale morphism is adic and locally of finite type (hetaleAdic, hetaleFiniteType), and the chart-level argument of the source's proof (hdescent)”.

Stacks 0GH6, the rig-smooth case, carrying four hypotheses. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of formal algebraic spaces over S. If g is locally of finite type, f is rig-smooth and rig-surjective, and f ≫ g is rig-smooth, then g is rig-smooth.

Rig-smoothness of g is tested on affine étale chart squares over it, by conditions (1) and (2) of Stacks 0GCQ. At such a square the three hypotheses produce exactly the data the source's argument consumes: the chart morphism t is locally of finite type, the base change X ×_Y V ⟶ V of f along the chart of Y is rig-surjective and rig-smooth on charts, and its composite with t ≫ b — that is, its composite with g ∘ f through the projection to X — is rig-smooth on charts.

The hypotheses carried are hlocal, which is Stacks 0GCK; htransfer, the transfer of Remark 0GBG to formal algebraic spaces; hetaleAdic and hetaleFiniteType, that a representable étale morphism is adic and locally of finite type; and hdescent, the chart-level argument of the source. Local finiteness of type of f, which Definition 0AQQ presupposes, is the hypothesis hfft.

theorem isRigSmooth_of_comp_of_isRigSurjective
    (hlocal : TopologicalRing.PropertyIsLocalNoetherian.{u}
      (fun {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂] (φ : R₁ →+* R₂) ↦
        RingHom.IsRigSmoothArrow φ))
    (htransfer : TransfersBaseChangeOnAffineEtaleDiagrams B S hS)
    (hetaleAdic : ∀ {U V : FppfSheaf B S hS} (w : U ⟶ V),
      IsRepresentableEtale B S hS w →
        IsAdicOnEveryAffineEtaleDiagramNoetherian B S hS w)
    (hetaleFiniteType : ∀ {U V : FppfSheaf B S hS} (w : U ⟶ V),
      IsRepresentableEtale B S hS w → IsLocallyOfFiniteType B S hS w)
    (hdescent : HasRigSurjectiveChartDescent B S hS
      (fun {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂] (φ : R₁ →+* R₂) ↦
        RingHom.IsRigSmoothArrow φ))
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hgft : IsLocallyOfFiniteType B S hS g) (hfft : IsLocallyOfFiniteType B S hS f)
    (hf : IsRigSmooth B S hS f) (hfs : IsRigSurjective B S hS f)
    (hgf : IsRigSmooth B S hS (f ≫ g)) :
    IsRigSmooth B S hS g

AlgebraicGeometry.FormalSpace.isRigEtale_of_comp_of_isRigSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmoothRigSurjectiveDescent.lean, line 331. The attribute's comment: “the rig-étale case, assuming Stacks 0AQL (hlocal), the transfer of Remark 0GBG to formal algebraic spaces (htransfer), that a representable étale morphism is adic and locally of finite type (hetaleAdic, hetaleFiniteType), and the chart-level argument of the source's proof (hdescent)”.

Stacks 0GH6, the rig-étale case, carrying four hypotheses. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of formal algebraic spaces over S. If g is locally of finite type, f is rig-étale and rig-surjective, and f ≫ g is rig-étale, then g is rig-étale.

The proof is the proof of the rig-smooth case with rig-smoothness of arrows of WAdm^{Noeth} replaced by rig-étaleness throughout: conditions (1) and (2) of Stacks 0GCZ replace those of Stacks 0GCQ, and Stacks 0GCW replaces Stacks 0GCL as the base-change input. The hypotheses are the same four, with hlocal now Stacks 0AQL.

theorem isRigEtale_of_comp_of_isRigSurjective
    (hlocal : TopologicalRing.PropertyIsLocalNoetherian.{u}
      (fun {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂] (φ : R₁ →+* R₂) ↦
        RingHom.IsRigEtaleArrow φ))
    (htransfer : TransfersBaseChangeOnAffineEtaleDiagrams B S hS)
    (hetaleAdic : ∀ {U V : FppfSheaf B S hS} (w : U ⟶ V),
      IsRepresentableEtale B S hS w →
        IsAdicOnEveryAffineEtaleDiagramNoetherian B S hS w)
    (hetaleFiniteType : ∀ {U V : FppfSheaf B S hS} (w : U ⟶ V),
      IsRepresentableEtale B S hS w → IsLocallyOfFiniteType B S hS w)
    (hdescent : HasRigSurjectiveChartDescent B S hS
      (fun {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂] (φ : R₁ →+* R₂) ↦
        RingHom.IsRigEtaleArrow φ))
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hgft : IsLocallyOfFiniteType B S hS g) (hfft : IsLocallyOfFiniteType B S hS f)
    (hf : IsRigEtale B S hS f) (hfs : IsRigSurjective B S hS f)
    (hgf : IsRigEtale B S hS (f ≫ g)) :
    IsRigEtale B S hS g

AlgebraicGeometry.FormalSpace.isRigSmooth_of_comp_of_isRigSurjective_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmoothRigSurjectiveDescentCharts.lean, line 285. The attribute's comment: “the rig-smooth case”.

Stacks 0GH6, the rig-smooth case. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of formal algebraic spaces over S with X locally Noetherian. If g is locally of finite type, f is rig-smooth and rig-surjective, and g ∘ f is rig-smooth, then g is rig-smooth.

The source also assumes Y and Z locally Noetherian and f locally of finite type; none of these is used, see the module documentation.

theorem isRigSmooth_of_comp_of_isRigSurjective_of_isLocallyNoetherian
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z) (hX : IsLocallyNoetherian B S hS X)
    (hgft : IsLocallyOfFiniteType B S hS g) (hf : IsRigSmooth B S hS f)
    (hfs : IsRigSurjective B S hS f) (hgf : IsRigSmooth B S hS (f ≫ g)) :
    IsRigSmooth B S hS g

AlgebraicGeometry.FormalSpace.isRigEtale_of_comp_of_isRigSurjective_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSmoothRigSurjectiveDescentCharts.lean, line 301. The attribute's comment: “the rig-étale case”.

Stacks 0GH6, the rig-étale case. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of formal algebraic spaces over S with X locally Noetherian. If g is locally of finite type, f is rig-étale and rig-surjective, and g ∘ f is rig-étale, then g is rig-étale.

The source also assumes Y and Z locally Noetherian and f locally of finite type; none of these is used, see the module documentation.

theorem isRigEtale_of_comp_of_isRigSurjective_of_isLocallyNoetherian
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z) (hX : IsLocallyNoetherian B S hS X)
    (hgft : IsLocallyOfFiniteType B S hS g) (hf : IsRigEtale B S hS f)
    (hfs : IsRigSurjective B S hS f) (hgf : IsRigEtale B S hS (f ≫ g)) :
    IsRigEtale B S hS g
Sources
LeanAlgebraicGeometry.FormalSpace.IsRigSurjective · AlgebraicGeometry.FormalSpace.FractionalPowers.not_isAdic_toDiscreteValuationRing · AlgebraicGeometry.FormalSpace.IsRigSurjective.comp · AlgebraicGeometry.FormalSpace.IsRigSurjective.comp_of_isFormalAlgebraicSpace · AlgebraicGeometry.FormalSpace.IsRigSurjective.of_isPullback · AlgebraicGeometry.FormalSpace.hasRigSurjectiveOnPullbackCharts_of_isRigSurjective · AlgebraicGeometry.FormalSpace.IsRigSurjective.of_isPullback_of_representable · AlgebraicGeometry.FormalSpace.IsRigSurjective.of_comp_of_mono

Section88.22 Formal algebraic spaces over cdvrs#

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

Tag 0GD8, a lemma

Tag 0GD8 in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_flat_isClosedImmersion_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FlatPartOverCdvr.lean, line 415. The attribute's comment: “both halves of the conclusion — the closed immersion with X' flat over A, and the factorization of every locally Noetherian Y ⟶ X flat over A through it — with the five inputs this library does not carry as named hypotheses. hpart is the affine half as a statement about formal spectra: its ring-theoretic content, that the quotient of the presenting ring by its A-torsion is flat over A and receives every homomorphism into a flat A-algebra, is proved here as Algebra.exists_flat_quotient_of_isDiscreteValuationRing, while its geometric realization needs the adic Noetherian quotient topology, a QuotientSystem for the quotient, Stacks 0ANP for a closed immersion out of a surjective presenting homomorphism and Stacks 0GCD for flatness out of a flat one, none of which this library carries. hdesc is the gluing step, Stacks 02WW with Bootstrap 046J and Spaces 03KD, carried in this library only as the quotient sheaf of a relation with the étale-equivalence-relation hypothesis undischarged, 046J only conditionally on Stacks 0AMP and Stacks 0421, and 03KD only for presheaves of Type u. hfac is the descent of a factorization through a closed immersion along an affine étale covering, Stacks 03KD with the monomorphism property of Stacks 0AQB. hrefine is the covering of a test object by the charts of the fibre products with the atlas, which is Stacks 0AJ3, the refinement of Stacks 0AJ2, Stacks 0AQ8 and Stacks 0GCG. hloc bundles the four hypotheses of isFlat_tfae, this library's Stacks 0GCD, namely Stacks 0AJ3, the refinement of Stacks 0AJ2 and the locality axioms of Stacks 0GC9 read through Stacks 0AN8 and Stacks 0AN9. Completeness of A is carried for faithfulness; the source's argument uses only that A is a discrete valuation ring, and the ring-theoretic half proved here needs only that it is a Bézout domain”.

Stacks 0GD8. Let A be a complete discrete valuation ring and let X be a locally Noetherian formal algebraic space over S with a structure morphism p : X ⟶ Spf A. Then there is a closed immersion ι : X' ⟶ X of formal algebraic spaces with X' locally Noetherian and flat over A such that every morphism q : Y ⟶ X with Y a locally Noetherian formal algebraic space flat over A factors through ι.

The atlas of X supplied by the locally Noetherian hypothesis is turned into a family of affine flat parts by hpart; those are mutually compatible, since the universal property of one of them applies to any Noetherian affine formal algebraic space flat over A mapping to the corresponding chart, so they glue by hdesc to a closed immersion ι : X' ⟶ X whose sources form an affine étale covering of X'. That covering exhibits X' as locally Noetherian, and reading condition (4) of Stacks 0GCD on it gives flatness of X' over A. For the universal property, hrefine covers a test object Y by Noetherian affine formal algebraic spaces which are flat over A and map to the charts of X; each of them factors through the corresponding flat part and hence through X', and hfac glues those factorizations.

theorem exists_flat_isClosedImmersion_of_isLocallyNoetherian
    [IsDomain A] [IsDiscreteValuationRing A] [IsNoetherianRing A]
    (_hAadic : TopologicalRing.IsAdic A)
    (_hAcomplete : IsAdicComplete (IsLocalRing.maximalIdeal A) A)
    (hSpfAaffine : IsAffineFormalAlgebraicSpace B S hS (formalSpectrum D))
    (hSpfA : IsFormalAlgebraicSpace B S hS (formalSpectrum D))
    {X : FppfSheaf B S hS} (hX : IsLocallyNoetherian B S hS X) (p : X ⟶ formalSpectrum D)
    (hpart : HasAffineFlatParts B S hS D p)
    (hdesc : FlatPartsDescend B S hS D p)
    (hfac : FactorizationDescendsAlongAffineEtaleCover B S hS)
    (hrefine : HasFlatAffineCoverOfFlat B S hS D p)
    (hloc : FlatnessLocalityInputs B S hS D) :
    ∃ (X' : FppfSheaf B S hS) (ι : X' ⟶ X),
      IsClosedImmersion B S hS ι ∧ IsLocallyNoetherian B S hS X' ∧
        IsFlat B S hS (ι ≫ p) ∧
        ∀ (Y : FppfSheaf B S hS) (q : Y ⟶ X), IsLocallyNoetherian B S hS Y →
          IsFlat B S hS (q ≫ p) → ∃ r : Y ⟶ X', r ≫ ι = q

AlgebraicGeometry.FormalSpace.exists_flatPart_of_isLocallyNoetherian_of_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FlatPartOverCdvrFull.lean, line 70.

Stacks 0GD8. Let A be a complete discrete valuation ring, carrying its 𝔪-adic topology, and let X be a locally Noetherian formal algebraic space over S with a structure morphism p : X ⟶ Spf A. Then there is a closed immersion ι : X' ⟶ X of formal algebraic spaces with X' locally Noetherian and flat over A such that every morphism q : Y ⟶ X with Y a locally Noetherian formal algebraic space flat over A factors through ι.

The members Uᵢ of a Noetherian atlas of X carry affine flat parts Zᵢ ⟶ Uᵢ, the formal spectra of the quotients by the A-torsion of their presenting rings; these glue to ι, the Zᵢ forming an atlas of X', on which flatness of X' over A is read off by Remark 0ANI. A test object Y is covered by Noetherian affine charts flat over A mapping to the Uᵢ; each factors through the corresponding Zᵢ, and the factorizations descend along the covering because ι is a monomorphism.

theorem exists_flatPart_of_isLocallyNoetherian_of_isAdicComplete
    [IsDomain A] [IsDiscreteValuationRing A]
    (hA : _root_.IsAdic (IsLocalRing.maximalIdeal A))
    (hAc : IsAdicComplete (IsLocalRing.maximalIdeal A) A)
    {X : FppfSheaf B S hS} (hX : IsLocallyNoetherian B S hS X) (p : X ⟶ formalSpectrum D) :
    ∃ (X' : FppfSheaf B S hS) (ι : X' ⟶ X),
      IsClosedImmersion B S hS ι ∧ IsLocallyNoetherian B S hS X' ∧
        IsFlat B S hS (ι ≫ p) ∧
        ∀ (Y : FppfSheaf B S hS) (q : Y ⟶ X), IsLocallyNoetherian B S hS Y →
          IsFlat B S hS (q ≫ p) → ∃ r : Y ⟶ X', r ≫ ι = q
Tag 0GD9, a lemma

Tag 0GD9 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isIso_or_isInitial_flatPart_of_isRigEtale_of_isRigSurjective_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FlatPartRigEtaleDiagonalUnconditional.lean, line 103.

Stacks 0GD9. Let A be a complete discrete valuation ring, carrying its 𝔪-adic topology, let X be a locally Noetherian formal algebraic space over S with a structure morphism p : X ⟶ Spf A locally of finite type, and let ι : X' ⟶ X be as in Stacks 0GD8: a closed immersion with X' flat over A through which every morphism Y ⟶ X from a locally Noetherian formal algebraic space flat over A factors. If the relative diagonal X ⟶ X ×_{Spf A} X is rig-étale and rig-surjective, then X' = Spf A or X' = ∅: the structure morphism ι ≫ p of X' is an isomorphism, or X' is initial.

X' is locally Noetherian, being locally of finite type over X (Stacks 0AQ7). The relative diagonal of ι ≫ p is the base change of that of p along the adic comparison X' ×_{Spf A} X' ⟶ X ×_{Spf A} X, ι being a monomorphism, so it is rig-étale (Stacks 0GD1) and rig-surjective (Stacks 0AQS), and isIso_or_isInitial_of_isFlat_of_isRigEtale_of_isRigSurjective_diagonal applies to ι ≫ p.

theorem isIso_or_isInitial_flatPart_of_isRigEtale_of_isRigSurjective_diagonal
    [IsDomain A] [IsDiscreteValuationRing A]
    (hAadic : _root_.IsAdic (IsLocalRing.maximalIdeal A))
    (hAc : IsAdicComplete (IsLocalRing.maximalIdeal A) A)
    {X X' : FppfSheaf B S hS} (hX : IsLocallyNoetherian B S hS X) (p : X ⟶ formalSpectrum D)
    (hp : IsLocallyOfFiniteType B S hS p) (ι : X' ⟶ X) (hιclosed : IsClosedImmersion B S hS ι)
    (hX'flat : IsFlat B S hS (ι ≫ p))
    (_hX'univ : ∀ (Y : FppfSheaf B S hS) (q : Y ⟶ X), IsLocallyNoetherian B S hS Y →
      IsFlat B S hS (q ≫ p) → ∃ r : Y ⟶ X', r ≫ ι = q)
    (hdiagE : IsRigEtale B S hS (pullback.diagonal p))
    (hdiagS : IsRigSurjective B S hS (pullback.diagonal p)) :
    IsIso (ι ≫ p) ∨ Nonempty (IsInitial X')
Tag 0GDA, a lemma

Tag 0GDA in the Stacks Project.

AlgebraicGeometry.FormalSpace.factorsAdicCompleteDvrPoints_of_rigEtaleDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveRigEtaleDiagonal.lean, line 318. The attribute's comment: “the complete discrete valuation ring lifting criterion is necessary for rig-surjectivity, granting Stacks 0AQ8, Stacks 0GD1 read through Stacks 0AQ3, Stacks 0AKY for the formal spectrum of a complete discrete valuation ring, Stacks 0GCD for an extension of such rings, and Stacks 0GD9 with Stacks 0GD8; see the module docstring for each”.

Stacks 0GDA, the substantial direction, carrying five hypotheses. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S with X locally Noetherian, f locally of finite type and Δ_f : X ⟶ X ×_Y X rig-étale and rig-surjective. If f is rig-surjective then every adic morphism Spf R ⟶ Y, with R a complete discrete valuation ring, lifts to X over R itself.

Rig-surjectivity provides an extension R ⊂ R' of complete discrete valuation rings and a lift Spf R' ⟶ X of the point p. In the fibre product W = Spf R ×_Y X the projection p₁ : W ⟶ Spf R is locally of finite type by Stacks 0AQ5 and W is locally Noetherian by h0AQ8, which is Stacks 0AQ8; the relative diagonal Δ_{p₁} is a base change of Δ_f along the comparison morphism W ×_{Spf R} W ⟶ X ×_Y X, which is a base change of p and hence representable by algebraic spaces, so Δ_{p₁} is rig-étale by h0GD1, which is Stacks 0GD1, and rig-surjective by Stacks 0AQS. Hence h0GD9, which is Stacks 0GD9 together with Stacks 0GD8, gives the flat part ι : W' ⟶ W of W over R and the dichotomy. The lift Spf R' ⟶ W is flat over R by hextFlat, which is Stacks 0GCD, and Spf R' is locally Noetherian by hSpfNoeth, which is Stacks 0AKY, so the lift factors through W' and the second alternative of the dichotomy is impossible. Therefore ι ≫ p₁ is an isomorphism and inv (ι ≫ p₁) ≫ ι ≫ p₂ is the factorisation wanted.

Local Noetherianity of Y is a hypothesis of Stacks 0GDA and is kept as _hY; the proof does not use it, obtaining local Noetherianity of X ×_Y X from that of X instead.

theorem factorsAdicCompleteDvrPoints_of_rigEtaleDiagonal
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (_hY : IsLocallyNoetherian B S hS Y)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hdiagEtale : IsRigEtale B S hS (pullback.diagonal f))
    (hdiagSurj : IsRigSurjective B S hS (pullback.diagonal f))
    (h0AQ8 : FibreProductIsLocallyNoetherian B S hS)
    (h0GD1 : RigEtaleIsStableUnderRepresentableBaseChange B S hS)
    (hSpfNoeth : FormalSpectrumOfCompleteDvrIsLocallyNoetherian B S hS)
    (hextFlat : FormalSpectrumMapOfDvrExtensionIsFlat B S hS)
    (h0GD9 : FlatPartOfRigEtaleDiagonalIsBaseOrPointless B S hS)
    (hrig : IsRigSurjective B S hS f) :
    FactorsAdicCompleteDvrPoints B S hS f

AlgebraicGeometry.FormalSpace.isRigSurjective_iff_factorsAdicCompleteDvrPoints_of_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveRigEtaleDiagonal.lean, line 408. The attribute's comment: “granting Stacks 0AQ8, Stacks 0GD1 read through Stacks 0AQ3, Stacks 0AKY for the formal spectrum of a complete discrete valuation ring, Stacks 0GCD for an extension of such rings, and Stacks 0GD9 with Stacks 0GD8, all five used by the forward implication only; see the module docstring for each”.

Stacks 0GDA, carrying five hypotheses. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S with X and Y locally Noetherian, f locally of finite type and the relative diagonal Δ_f : X ⟶ X ×_Y X rig-étale and rig-surjective. Then f is rig-surjective if and only if every adic morphism Spf R ⟶ Y, with R a complete discrete valuation ring, lifts to a morphism Spf R ⟶ X.

The direction the source calls trivial is AlgebraicGeometry.FormalSpace.isRigSurjective_of_factorsAdicCompleteDvrPoints, which needs none of the hypotheses. The five carried hypotheses are used by the other direction only; see the module docstring.

theorem isRigSurjective_iff_factorsAdicCompleteDvrPoints_of_diagonal
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hdiagEtale : IsRigEtale B S hS (pullback.diagonal f))
    (hdiagSurj : IsRigSurjective B S hS (pullback.diagonal f))
    (h0AQ8 : FibreProductIsLocallyNoetherian B S hS)
    (h0GD1 : RigEtaleIsStableUnderRepresentableBaseChange B S hS)
    (hSpfNoeth : FormalSpectrumOfCompleteDvrIsLocallyNoetherian B S hS)
    (hextFlat : FormalSpectrumMapOfDvrExtensionIsFlat B S hS)
    (h0GD9 : FlatPartOfRigEtaleDiagonalIsBaseOrPointless B S hS) :
    IsRigSurjective B S hS f ↔ FactorsAdicCompleteDvrPoints B S hS f

AlgebraicGeometry.FormalSpace.isRigSurjective_iff_factorsAdicCompleteDvrPoints_of_rigEtale_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveRigEtaleDiagonalCriterion.lean, line 162.

Stacks 0GDA. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S with X and Y locally Noetherian, f locally of finite type, and the relative diagonal Δ_f : X ⟶ X ×_Y X rig-étale and rig-surjective. Then f is rig-surjective if and only if every adic morphism Spf R ⟶ Y, with R a complete discrete valuation ring, lifts to a morphism Spf R ⟶ X.

theorem isRigSurjective_iff_factorsAdicCompleteDvrPoints_of_rigEtale_diagonal
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hdiagEtale : IsRigEtale B S hS (pullback.diagonal f))
    (hdiagSurj : IsRigSurjective B S hS (pullback.diagonal f)) :
    IsRigSurjective B S hS f ↔ FactorsAdicCompleteDvrPoints B S hS f
Sources
LeanAlgebraicGeometry.FormalSpace.exists_flat_isClosedImmersion_of_isLocallyNoetherian · AlgebraicGeometry.FormalSpace.exists_flatPart_of_isLocallyNoetherian_of_isAdicComplete · AlgebraicGeometry.FormalSpace.isIso_or_isInitial_flatPart_of_isRigEtale_of_isRigSurjective_diagonal · AlgebraicGeometry.FormalSpace.factorsAdicCompleteDvrPoints_of_rigEtaleDiagonal · AlgebraicGeometry.FormalSpace.isRigSurjective_iff_factorsAdicCompleteDvrPoints_of_diagonal · AlgebraicGeometry.FormalSpace.isRigSurjective_iff_factorsAdicCompleteDvrPoints_of_rigEtale_diagonal

Section88.23 The completion functor#

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

Tag 0AQ9, a lemma

Tag 0AQ9 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionLocallyFiniteType.lean, line 114.

Stacks 0AQ9. Let f : X' ⟶ X be a morphism of algebraic spaces over S and let T be a set of points of X. If f is locally of finite type, then the induced morphism of completions X'_{/|f|⁻¹ T} ⟶ X_{/T} is locally of finite type.

theorem isLocallyOfFiniteType_completionSheafMap
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (f : X' ⟶ X) (T : Set (Space.points B S hS X))
    (hf : Space.IsLocallyOfFiniteType B S hS f) :
    IsLocallyOfFiniteType B S hS (Space.completionSheafMap B S hS f T)
Tag 0GI0, a lemma

Tag 0GI0 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isEtale_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionEtale.lean, line 208.

Let f : X' ⟶ X be a morphism of algebraic spaces over S and let T be a set of points of X. If f is étale, then the induced morphism of completions X'_{/|f|⁻¹ T} ⟶ X_{/T} is étale: it is representable by algebraic spaces and each of its base changes along a scheme-valued point of its target is étale.

theorem isEtale_completionSheafMap
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (f : X' ⟶ X) (T : Set (Space.points B S hS X))
    (hf : Space.IsEtale B S hS f) :
    ∃ hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
        (Space.completionSheafMap B S hS f T).hom,
      Space.HasPropertyULift.{u + 1} B S hS
        (fun ⦃A C : Space.AlgebraicSpacesULift.{u + 1} B S hS⦄ (g : A ⟶ C) ↦
          Space.IsEtaleULift.{u + 1} B S hS g.hom)
        (Space.completionSheafMap B S hS f T).hom hrep
Tag 0GDC, a lemma

Tag 0GDC in the Stacks Project.

AlgebraicGeometry.FormalSpace.isClosedImmersion_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionClosedImmersion.lean, line 98.

Stacks 0GDC. Let f : X' ⟶ X be a morphism of algebraic spaces over S and let T be a set of points of X. If f is a closed immersion, then the induced morphism of completions X'_{/|f|⁻¹ T} ⟶ X_{/T} is a closed immersion of formal algebraic spaces: it is representable by algebraic spaces and each of its base changes along a scheme-valued point of its target is a closed immersion.

theorem isClosedImmersion_completionSheafMap
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (f : X' ⟶ X) (T : Set (Space.points B S hS X))
    (hf : Space.IsClosedImmersion B S hS f) :
    IsClosedImmersion B S hS (Space.completionSheafMap B S hS f T)
Tag 0GDD, a lemma

Tag 0GDD in the Stacks Project.

AlgebraicGeometry.FormalSpace.isProper_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionProper.lean, line 282.

Let f : X' ⟶ X be a morphism of algebraic spaces over S and let T be a set of points of X. If f is proper, then the induced morphism of completions X'_{/|f|⁻¹ T} ⟶ X_{/T} is proper.

theorem isProper_completionSheafMap
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (f : X' ⟶ X) (T : Set (Space.points B S hS X))
    (hf : Space.IsProper B S hS f) :
    IsProper B S hS (Space.completionSheafMap B S hS f T)
Tag 0GDE, a lemma

Tag 0GDE in the Stacks Project.

AlgebraicGeometry.FormalSpace.isQuasiCompact_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionQuasiCompact.lean, line 146. The attribute's comment: “quasi-compactness of f_{/T} in the form of Bootstrap, Definition 03XZ: f_{/T} is representable by algebraic spaces and each of its base changes along a scheme-valued point of its target is a quasi-compact morphism of algebraic spaces. For a morphism representable by algebraic spaces this is the quasi-compactness of Stacks 0AJC by Stacks 0AM2, whose proof needs the agreement of the two notions of a quasi-compact space on an algebraic space, QuasiCompactSpaceAgreesOnAlgebraicSpaces, which this library does not carry; isQuasiCompact_completionSheafMap_of_agreesOnAlgebraicSpaces is the conclusion in the form of Stacks 0AJC granted that agreement”.

Stacks 0GDE. Let f : X' ⟶ X be a morphism of algebraic spaces over S and let T be a set of points of X. If f is quasi-compact, then the induced morphism of completions f_{/T} : X'_{/|f|⁻¹ T} ⟶ X_{/T} is quasi-compact: it is representable by algebraic spaces and each of its base changes along a scheme-valued point of its target is a quasi-compact morphism of algebraic spaces.

theorem isQuasiCompact_completionSheafMap
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (f : X' ⟶ X) (T : Set (Space.points B S hS X))
    (hf : Space.IsQuasiCompact B S hS f) :
    ∃ hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
        (Space.completionSheafMap B S hS f T).hom,
      Space.HasPropertyULift.{u + 1} B S hS
        (Space.quasiCompactPropertyULift.{u + 1} B S hS)
        (Space.completionSheafMap B S hS f T).hom hrep
Tag 0GDF, a remark

Tag 0GDF in the Stacks Project.

AlgebraicGeometry.Space.isPullback_completionSheafPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionDiagonal.lean, line 248. The attribute's comment: “fibre product of completions”.

Stacks 0GDF. The completion of a fibre product is the fibre product of the completions: for morphisms f : X' ⟶ X and g : Y ⟶ X of presheaves on the big fppf site of S and a set T of points of X, the square formed by (X' ×_X Y)_{/T''}, the two completions X'_{/T'} and Y_{/T₂} and X_{/T} is cartesian, so that X'_{/T'} ×_{X_{/T}} Y_{/T₂} = (X' ×_X Y)_{/T''} as subobjects of the ambient sheaf of X' ×_X Y.

theorem isPullback_completionSheafPullback (f : X' ⟶ X) (g : Y ⟶ X)
    (T : Set (points B S hS X)) :
    IsPullback (completionSheafPullbackFst B S hS f g T)
      (completionSheafPullbackSnd B S hS f g T)
      (completionSheafMap B S hS f T) (completionSheafMap B S hS g T)

AlgebraicGeometry.Space.completionSheafDiagonal_comp_completionSheafInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionDiagonal.lean, line 300. The attribute's comment: “diagonals agree over the fibre product”.

Stacks 0GDF. The diagonal of the completed morphism is the diagonal of the original morphism, read inside the ambient sheaf of X' ×_X X': this is the equality Δ_{f_{/T}} = (Δ_f)_{/T''} of morphisms of subobjects of X' ×_X X', the inclusion of a completion into the ambient sheaf being a monomorphism.

theorem completionSheafDiagonal_comp_completionSheafInclusion (f : X' ⟶ X)
    (T : Set (points B S hS X)) :
    completionSheafDiagonal B S hS f T ≫
        completionSheafInclusion B S hS (pullback f f) (pullbackPoints B S hS f f T) =
      completionSheafInclusion B S hS X' (pointsMap B S hS X' f ⁻¹' T) ≫
        sheafifiedULiftMap B S hS (pullback.diagonal f)

AlgebraicGeometry.Space.completionSheafDiagonal_eq_completionSheafMap_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionDiagonal.lean, line 337. The attribute's comment: “equality of diagonals”.

Stacks 0GDF. The diagonal of the completed morphism is the completion of the diagonal: Δ_{f_{/T}} = (Δ_f)_{/T''} as morphisms X'_{/T'} ⟶ (X' ×_X X')_{/T''}. The eqToHom transports the source of (Δ_f)_{/T''}, the completion of X' along the inverse image of T'' under the diagonal, to the completion of X' along T'; the two sets of points are equal by AlgebraicGeometry.Space.pointsMap_diagonal_preimage_pullbackPoints.

theorem completionSheafDiagonal_eq_completionSheafMap_diagonal (f : X' ⟶ X)
    (T : Set (points B S hS X)) :
    completionSheafDiagonal B S hS f T =
      eqToHom (congrArg (completionSheaf B S hS X')
          (pointsMap_diagonal_preimage_pullbackPoints B S hS f T).symm) ≫
        completionSheafMap B S hS (pullback.diagonal f) (pullbackPoints B S hS f f T)
Tag 0GDG, a lemma

Tag 0GDG in the Stacks Project.

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSeparated.lean, line 130. The attribute's comment: “separated: the completion of a separated morphism of algebraic spaces along a set of points of its target is a separated morphism of formal algebraic spaces, separatedness of the completion read as the separatedness axiom of Stacks 0ARN”.

Stacks 0GDG, the separatedness clause. Let f : X' ⟶ X be a morphism of algebraic spaces over S and let T be a set of points of X. If f is separated, then the induced morphism of completions f_{/T} : X'_{/|f|⁻¹ T} ⟶ X_{/T} is separated: its relative diagonal is the completion of the relative diagonal of f, which is a closed immersion by Stacks 0GDC.

theorem isSeparatedMorphism_completionSheafMap
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (f : X' ⟶ X) (T : Set (Space.points B S hS X))
    (hf : Space.IsSeparated B S hS f) :
    IsSeparatedMorphism B S hS (Space.completionSheafMap B S hS f T)

AlgebraicGeometry.FormalSpace.isQuasiSeparatedMorphism_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionSeparated.lean, line 162. The attribute's comment: “quasi-separated: the completion of a quasi-separated morphism of algebraic spaces along a set of points of its target has quasi-compact relative diagonal. Quasi-compactness of the diagonal is read as IsQuasiSeparatedMorphism, that is, as Space.IsQuasiCompactULift: every base change of the diagonal along a morphism from a quasi-compact algebraic space has quasi-compact source. The implementation notes of StacksFrontier.AlgebraicGeometry.FormalSpace.SeparatedMorphism record that condition as a priori stronger than the source's quasi-compactness of a morphism of formal algebraic spaces, so the conclusion delivered is a priori stronger than the source's; the hypothesis is the source's quasi-separatedness of Stacks 03HL, part (3)”.

Stacks 0GDG, the quasi-separatedness clause. Let f : X' ⟶ X be a morphism of algebraic spaces over S and let T be a set of points of X. If f is quasi-separated, then the induced morphism of completions f_{/T} : X'_{/|f|⁻¹ T} ⟶ X_{/T} has quasi-compact relative diagonal: that relative diagonal is the completion of the relative diagonal of f, which is quasi-compact by Stacks 0GDE.

theorem isQuasiSeparatedMorphism_completionSheafMap
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (f : X' ⟶ X) (T : Set (Space.points B S hS X))
    (hf : Space.IsQuasiSeparated B S hS f) :
    IsQuasiSeparatedMorphism B S hS (Space.completionSheafMap B S hS f T)
Tag 0GDH, a lemma

Tag 0GDH in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSmooth_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionRigEtale.lean, line 307. The attribute's comment: “the affine case, which is part (1) of Stacks 0GAK (Rig.isRigSmooth_adicCompletionObj_of_smoothAwayFrom), applied through the reduction to the affine case carried as the hypothesis hred: granted the three hypotheses of the lemma it produces, for each affine representable étale square over f_{/T}, the Noetherian ring A₀, the ideal I₀ and the finite type A₀-algebra C₀ smooth over Spec A₀ minus V(I₀) of the source's proof, together with the comparison of rig-smoothness of C₀ completed with rig-smoothness of the arrow of WAdm^{Noeth} presenting the square. The source assembles that reduction from Properties of Spaces, Lemma 03FX, the cartesian completion squares of Stacks 0APV, the identification of a chart of the completion with a formal spectrum in the proof of Stacks 0AQ1, and the étale locality of local finite type, of smoothness and of local Noetherianity, none of which this library carries in that combination”.

Stacks 0GDH. In the situation of Stacks 0GDB, if X is locally Noetherian, f is locally of finite type and U' → U is smooth, then f_{/T} is rig-smooth.

Granted the reduction to the affine case, the lemma is part (1) of Stacks 0GAK applied to the affine data that reduction produces, exactly as in the source.

theorem isRigSmooth_completionSheafMap {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X' ⟶ X)
    (T : Set (Space.points B S hS X))
    (hX : Space.IsLocallyNoetherian B S hS X)
    (hf : Space.IsLocallyOfFiniteType B S hS f)
    (hsm : Space.IsSmooth B S hS (Space.openComplementRestriction B S hS f T))
    (hred : ChartSquareReducesToSmoothAwayFrom B S hS f T) :
    IsRigSmooth B S hS (Space.completionSheafMap B S hS f T)

AlgebraicGeometry.FormalSpace.isRigSmooth_completionSheafMap_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionRigSmoothCover.lean, line 329.

Stacks 0GDH. Let f : X' ⟶ X be a morphism of algebraic spaces over S, let T ⊆ |X| be closed, and let U ⊆ X be the open complement of T and U' = f⁻¹U (the situation of Stacks 0GDB). If X is locally Noetherian, f is locally of finite type and U' → U is smooth, then the completion f_{/T} : X'_{/T'} ⟶ X_{/T} is rig-smooth.

The proof is the source's: compatible étale atlases of X and X' by spectra of rings (Properties of Spaces, Lemma 03FX; exists_compatible_affineOver_atlases), condition (4) of Stacks 0GCQ for f_{/T} from them (correspondsToNoetherianMapAfterSourceCover_isRigSmoothArrow_completionSheafMap: the reduction to the affine case and the affine case by Stacks 0GAK and Stacks 0GAM), and the implication (4) ⟹ (1) of Stacks 0GCQ.

theorem isRigSmooth_completionSheafMap_of_isLocallyNoetherian
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX' : IsAlgebraicSpace B S hS X')
    (hX : IsAlgebraicSpace B S hS X) (f : X' ⟶ X) (T : Set (Space.points B S hS X))
    (hT : @IsClosed _ (Space.pointTopology B S hS X) T)
    (hXN : Space.IsLocallyNoetherian B S hS X)
    (hf : Space.IsLocallyOfFiniteType B S hS f)
    (hsm : Space.IsSmooth B S hS (Space.openComplementRestriction B S hS f T)) :
    IsRigSmooth B S hS (Space.completionSheafMap B S hS f T)
Tag 0AR2, a lemma

Tag 0AR2 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigEtale_completionSheafMap_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionAtlasCompatible.lean, line 386.

Stacks 0AR2. Let f : X' ⟶ X be a morphism of algebraic spaces over S, let T ⊆ |X| be closed, and let U ⊆ X be the open complement of T and U' = f⁻¹U (the situation of Stacks 0GDB). If X is locally Noetherian, f is locally of finite type and U' → U is étale, then the completion f_{/T} : X'_{/T'} ⟶ X_{/T} is rig-étale.

The proof is the source's: compatible étale atlases of X and X' by spectra of rings (Properties of Spaces, Lemma 03FX; exists_compatible_affineOver_atlases), condition (4) of Stacks 0GCZ for f_{/T} from them (correspondsToRigEtaleMapAfterSourceCover_completionSheafMap: the reduction to the affine case and the affine case by part (1) of Stacks 0ALQ), and the implication (4) ⟹ (1) of Stacks 0GCZ.

theorem isRigEtale_completionSheafMap_of_isLocallyNoetherian
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX' : IsAlgebraicSpace B S hS X')
    (hX : IsAlgebraicSpace B S hS X) (f : X' ⟶ X) (T : Set (Space.points B S hS X))
    (hT : @IsClosed _ (Space.pointTopology B S hS X) T)
    (hXN : Space.IsLocallyNoetherian B S hS X)
    (hf : Space.IsLocallyOfFiniteType B S hS f)
    (het : Space.IsEtale B S hS (Space.openComplementRestriction B S hS f T)) :
    IsRigEtale B S hS (Space.completionSheafMap B S hS f T)

AlgebraicGeometry.FormalSpace.isRigEtale_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionRigEtale.lean, line 339. The attribute's comment: “the affine case, which is part (1) of Stacks 0ALQ (Rig.isRigEtale_adicCompletionObj_of_isEtaleOutside), applied through the reduction to the affine case carried as the hypothesis hred: granted the three hypotheses of the lemma it produces, for each affine representable étale square over f_{/T}, the Noetherian ring A₀, the ideal I₀ and the finite type A₀-algebra C₀ étale over Spec A₀ minus V(I₀) of the source's proof, together with the comparison of rig-étaleness of C₀ completed with rig-étaleness of the arrow of WAdm^{Noeth} presenting the square. This is the substitution of Lemmas 0ALQ and 0GCZ for Lemmas 0GAK and 0GCQ that the source's proof prescribes; the reduction itself is assembled in the source from Properties of Spaces, Lemma 03FX, the cartesian completion squares of Stacks 0APV, the identification of a chart of the completion with a formal spectrum in the proof of Stacks 0AQ1, and the étale locality of local finite type, of étaleness and of local Noetherianity, none of which this library carries in that combination”.

Stacks 0AR2. In the situation of Stacks 0GDB, if X is locally Noetherian, f is locally of finite type and U' → U is étale, then f_{/T} is rig-étale.

Granted the reduction to the affine case, the lemma is part (1) of Stacks 0ALQ applied to the affine data that reduction produces; this is the proof of Stacks 0GDH with Lemmas 0GAK and 0GCQ replaced by Lemmas 0ALQ and 0GCZ, as the source says.

theorem isRigEtale_completionSheafMap {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X' ⟶ X)
    (T : Set (Space.points B S hS X))
    (hX : Space.IsLocallyNoetherian B S hS X)
    (hf : Space.IsLocallyOfFiniteType B S hS f)
    (het : Space.IsEtale B S hS (Space.openComplementRestriction B S hS f T))
    (hred : ChartSquareReducesToIsEtaleOutside B S hS f T) :
    IsRigEtale B S hS (Space.completionSheafMap B S hS f T)

AlgebraicGeometry.FormalSpace.isRigEtale_completionSheafMap_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionRigEtaleCharts.lean, line 692.

Stacks 0AR2. Let f : X' ⟶ X be a morphism of algebraic spaces over S, let T ⊆ |X| be closed and let U' ⟶ U be the restriction of f to the open complements of T' = |f|⁻¹T and T. If X is locally Noetherian, f is locally of finite type and U' ⟶ U is étale, then f_{/T} : X'_{/T'} ⟶ X_{/T} is rig-étale.

The proof is the source's, through condition (4) of Stacks 0GCZ. Cover X by affine étale charts Spec A_k ⟶ X (exists_affine_etale_charts) and each Spec A_k ×_X X' by affine étale charts Spec C_kl; the completions (Spec C_kl)_{/T} cover X'_{/T'} (Stacks 0APV), each factors through the chart (Spec A_k)_{/T} of X_{/T} by the completion of Spec C_kl ⟶ Spec A_k, and that completion corresponds to a rig-étale map by the affine case (correspondsToRigEtaleMap_completionSheafMap_of_etaleAt, which is part (1) of Stacks 0ALQ): the chart map Spec C_kl ⟶ Spec A_k is locally of finite type, A_k is Noetherian, and the chart map is étale over the complement of T because U' ⟶ U is.

theorem isRigEtale_completionSheafMap_of_isEtale {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X) (f : X' ⟶ X)
    (T : Set (Space.points B S hS X)) (hT : IsClosed T)
    (hXN : Space.IsLocallyNoetherian B S hS X) (hf : Space.IsLocallyOfFiniteType B S hS f)
    (het : Space.IsEtale B S hS (Space.openComplementRestriction B S hS f T)) :
    IsRigEtale B S hS (Space.completionSheafMap B S hS f T)
Tag 0AQW, a lemma

Tag 0AQW in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSurjective_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ProperValuativeLifting.lean, line 789.

Stacks 0AQW. In the situation of Stacks 0GDB, let f : X' ⟶ X be a proper morphism of algebraic spaces over S, let T be a closed set of points of X, and let the restriction U' ⟶ U of f to the open complements of T and of T' = |f|⁻¹ T be surjective. Then the morphism of completions f_{/T} : X'_{/T'} ⟶ X_{/T} is rig-surjective.

An adic morphism p : Spf R ⟶ X_{/T} out of a complete discrete valuation ring R algebraizes by Stacks 0GBU to a morphism Spec R ⟶ X whose fibre over T is the closed point, so its generic point lies over U. The valuative step AlgebraicGeometry.Space.exists_isExtension_lift_of_isProper_of_isSurjective (Stacks 00PH, 0A40 and 0AP1) produces an extension R ⊂ R' of complete discrete valuation rings and a point Spec R' ⟶ X' over Spec R' ⟶ Spec R ⟶ X. Restricted to Spf R' and paired with Spf R' ⟶ Spf R ⟶ X_{/T}, it lands in X'_{/T'} because the completion square of Stacks 0APV is cartesian, and this is the lift.

The source also assumes X locally Noetherian, so that f_{/T} is a morphism of locally Noetherian formal algebraic spaces and the algebraization of Stacks 0GBU is available as stated; neither use is needed here, and the statement is proved without that hypothesis.

theorem isRigSurjective_completionSheafMap {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (f : X' ⟶ X) (T : Set (Space.points B S hS X))
    (hT : @IsClosed _ (Space.pointTopology B S hS X) T) (hf : Space.IsProper B S hS f)
    (hsurj : Space.IsSurjective B S hS
      ((Space.openSubspaceOfPoints B S hS X Tᶜ).fromPreimage f)) :
    IsRigSurjective B S hS (Space.completionSheafMap B S hS f T)
Tag 0GDI, a lemma

Tag 0GDI in the Stacks Project.

AlgebraicGeometry.FormalSpace.isRigSurjective_diagonal_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionDiagonalRigSurjective.lean, line 170.

Stacks 0GDI. In the situation of Stacks 0GDB, let f : X' ⟶ X be a separated morphism of algebraic spaces over S, let T be a closed set of points of X, and let the restriction U' ⟶ U of f to the open complements of T and of T' = |f|⁻¹ T be a monomorphism. Then the diagonal Δ_{f_{/T}} : X'_{/T'} ⟶ X'_{/T'} ×_{X_{/T}} X'_{/T'} of the completed morphism is rig-surjective.

By Stacks 0GDF it is the completion of Δ_f : X' ⟶ X' ×_X X' along the set of points over T, up to isomorphisms; Δ_f is a closed immersion, hence proper, and is surjective over the complement of T, so Stacks 0AQW applies. The source's hypotheses that X be locally Noetherian and f locally of finite type are not needed.

theorem isRigSurjective_diagonal_completionSheafMap {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (f : X' ⟶ X) (T : Set (Space.points B S hS X))
    (hT : @IsClosed _ (Space.pointTopology B S hS X) T) (hf : Space.IsSeparated B S hS f)
    (hmono : Mono ((Space.openSubspaceOfPoints B S hS X Tᶜ).fromPreimage f)) :
    IsRigSurjective B S hS (pullback.diagonal (Space.completionSheafMap B S hS f T))
Sources
LeanAlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_completionSheafMap · AlgebraicGeometry.FormalSpace.isEtale_completionSheafMap · AlgebraicGeometry.FormalSpace.isClosedImmersion_completionSheafMap · AlgebraicGeometry.FormalSpace.isProper_completionSheafMap · AlgebraicGeometry.FormalSpace.isQuasiCompact_completionSheafMap · AlgebraicGeometry.Space.isPullback_completionSheafPullback · AlgebraicGeometry.Space.completionSheafDiagonal_comp_completionSheafInclusion · AlgebraicGeometry.Space.completionSheafDiagonal_eq_completionSheafMap_diagonal

Section88.24 Formal modifications#

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

Tag 0GDK, a definition

Tag 0GDK in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsFormalModification, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Proper.lean, line 323.

Stacks 0GDK. A morphism f : X ⟶ Y of locally Noetherian formal algebraic spaces over S is a formal modification when (1) f is proper, (2) f is rig-étale, (3) f is rig-surjective, and (4) the relative diagonal Δ_f : X ⟶ X ×_Y X is rig-surjective. The hypothesis that X and Y be locally Noetherian formal algebraic spaces is recorded in the first two fields, so the condition is stated for an arbitrary morphism of fppf sheaves on the big fppf site of S.

structure IsFormalModification {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop
Tag 0GDL, a remark

Tag 0GDL in the Stacks Project.

AlgebraicGeometry.FormalSpace.artinConditions_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalModificationArtinComparison.lean, line 249.

Stacks 0GDL. Let f : X ⟶ Y be a proper morphism of locally Noetherian formal algebraic spaces over S, and compare the conditions of Artin's Definition 1.7 of a formal modification — (i) the Jacobian and the Cramer ideal of f each contain an ideal of definition of X, (ii) the ideal of the relative diagonal Δ_f : X ⟶ X ×_Y X is annihilated by an ideal of definition of X ×_Y X, (iii) every adic morphism Spf R ⟶ Y with R a complete discrete valuation ring lifts to X — with those of Definition 0GDK:

  • Ad (i): condition (i) holds if and only if f is rig-étale;
  • Ad (ii): if f is rig-étale, then Δ_f is rig-étale, and condition (ii) holds if and only if Δ_f is rig-surjective;
  • Ad (iii): if conditions (i) and (ii) hold, condition (iii) holds if and only if f is rig-surjective.

Conditions (i) and (ii) are read on the affine étale charts of f and of X ×_Y X, as AlgebraicGeometry.FormalSpace.HasJacobianCramerIdealOfDefinition and AlgebraicGeometry.FormalSpace.HasAnnihilatedKerOnPullbackCharts.

theorem artinConditions_comparison {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hproper : IsProper B S hS f) :
    (HasJacobianCramerIdealOfDefinition B S hS f ↔ IsRigEtale B S hS f) ∧
      (IsRigEtale B S hS f →
        IsRigEtale B S hS (pullback.diagonal f) ∧
          (HasAnnihilatedKerOnPullbackCharts B S hS (pullback.diagonal f) ↔
            IsRigSurjective B S hS (pullback.diagonal f))) ∧
      (HasJacobianCramerIdealOfDefinition B S hS f →
        HasAnnihilatedKerOnPullbackCharts B S hS (pullback.diagonal f) →
          (FactorsAdicCompleteDvrPoints B S hS f ↔ IsRigSurjective B S hS f))

AlgebraicGeometry.FormalSpace.isFormalModification_of_factorsAdicCompleteDvrPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalModificationArtinConditions.lean, line 114. The attribute's comment: “the implication of Ad (iii) that needs no further input: Artin's condition (iii), a lift of every adic point over the complete discrete valuation ring itself, implies rig-surjectivity, which asks only for a lift over an extension of that ring. Together with the remaining conditions of Artin's Definition 1.7 in the translated form the remark gives them — properness, rig-étaleness for condition (i) by Ad (i), and rig-surjectivity of the relative diagonal for condition (ii) by Ad (ii) — this is the comparison with Definition 0GDK. Not covered: the converse implication of Ad (iii), which the remark obtains from Stacks 0GDA; the two implications of Ad (ii), which it obtains from Stacks 0GD1, Stacks 0GD3 and Stacks 0GD6; and Ad (i), whose equivalence of condition (i) with rig-étaleness is part (7) of Lemma 0AJU, that is Stacks 0AJY, and whose Cramer and Jacobian ideals of a morphism of formal algebraic spaces this library does not have”.

Stacks 0GDL. Let f : X ⟶ Y be a proper rig-étale morphism of locally Noetherian formal algebraic spaces over S whose relative diagonal Δ_f : X ⟶ X ×_Y X is rig-surjective. If every adic morphism Spf R ⟶ Y with R a complete discrete valuation ring factors through f over R itself, then f is a formal modification in the sense of Definition 0GDK: such a factorisation is in particular one over the trivial extension of R, so f is rig-surjective.

theorem isFormalModification_of_factorsAdicCompleteDvrPoints {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hproper : IsProper B S hS f) (hetale : IsRigEtale B S hS f)
    (hdiagSurj : IsRigSurjective B S hS (pullback.diagonal f))
    (hlift : FactorsAdicCompleteDvrPoints B S hS f) :
    IsFormalModification B S hS f
Tag 0GDM, a lemma

Tag 0GDM in the Stacks Project.

AlgebraicGeometry.FormalSpace.isFormalModification_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFormalModification.lean, line 52.

Stacks 0GDM. Let f : X' ⟶ X be a morphism of algebraic spaces over S, let T ⊆ |X| be closed and let U ⊆ X be the open subspace with |U| = |X| ∖ T. If X is locally Noetherian, f is proper and U' = f⁻¹U ⟶ U is an isomorphism, then f_{/T} : X'_{/T'} ⟶ X_{/T} is a formal modification.

theorem isFormalModification_completionSheafMap {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hXN : Space.IsLocallyNoetherian B S hS X) (f : X' ⟶ X)
    (T : Set (Space.points B S hS X)) (hT : IsClosed T) (hf : Space.IsProper B S hS f)
    (hfU : IsIso (pullback.snd f (Space.openSubspaceOfPoints B S hS X Tᶜ).ι)) :
    IsFormalModification B S hS (Space.completionSheafMap B S hS f T)
Tag 0GDN, a lemma

Tag 0GDN in the Stacks Project.

AlgebraicGeometry.FormalSpace.isFormalModification_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalModificationBaseChange.lean, line 222. The attribute's comment: “granting Stacks 0AQ8 as h0AQ8 and the four open inputs of Stacks 0GD1 as hcond, hiso, h31, hcover; see the module docstring for these and for hgft, hdiag”.

Stacks 0GDN. Let f : X ⟶ Y be a formal modification of locally Noetherian formal algebraic spaces over S and let g : Z ⟶ Y be an adic morphism, Z locally Noetherian. Then the base change X ×_Y Z ⟶ Z of f along g is a formal modification.

theorem isFormalModification_pullback_snd
    (hcond : TopologicalRing.PropertyIsLocalNoetherian.{u}
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
        Rig.RigEtaleCondition φ))
    (hiso : PropertyIsInvariantUnderTargetIso.{u}
      (fun {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂] (φ : R₁ →+* R₂) ↦
        RingHom.IsRigEtaleArrow φ))
    (h31 : SourceCoverImpliesEveryAffineEtaleDiagram B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R)
      (fun {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂] (φ : R₁ →+* R₂) ↦
        RingHom.IsRigEtaleArrow φ))
    (hcover : ∀ {X₀ Y₀ Z₀ : FppfSheaf B S hS} (f₀ : X₀ ⟶ Y₀) (g₀ : Z₀ ⟶ Y₀),
      HasBaseChangeCoverOverPullbackSnd B S hS f₀ g₀)
    (h0AQ8 : FibreProductIsLocallyNoetherian B S hS)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hZ : IsLocallyNoetherian B S hS Z)
    (hg : IsAdicOnEveryAffineEtaleDiagramNoetherian B S hS g)
    (hgft : IsLocallyOfFiniteType B S hS g)
    (hdiag : IsLocallyOfFiniteType B S hS (pullback.diagonal f))
    (hf : IsFormalModification B S hS f) :
    IsFormalModification B S hS (pullback.snd f g)

AlgebraicGeometry.FormalSpace.isFormalModification_pullback_snd_of_isAdicMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalModificationBaseChangeAdic.lean, line 122.

Stacks 0GDN. Let f : X ⟶ Y be a morphism of locally Noetherian formal algebraic spaces over S which is a formal modification. Then for any adic morphism g : Z ⟶ Y of locally Noetherian formal algebraic spaces, the base change X ×_Y Z ⟶ Z is a formal modification.

theorem isFormalModification_pullback_snd_of_isAdicMorphism {X Y Z : FppfSheaf B S hS}
    (f : X ⟶ Y) (g : Z ⟶ Y) (hZ : IsLocallyNoetherian B S hS Z)
    (hg : IsAdicMorphism B S hS g) (hf : IsFormalModification B S hS f) :
    IsFormalModification B S hS (pullback.snd f g)
Sources
LeanAlgebraicGeometry.FormalSpace.IsFormalModification · AlgebraicGeometry.FormalSpace.artinConditions_comparison · AlgebraicGeometry.FormalSpace.isFormalModification_of_factorsAdicCompleteDvrPoints · AlgebraicGeometry.FormalSpace.isFormalModification_completionSheafMap · AlgebraicGeometry.FormalSpace.isFormalModification_pullback_snd · AlgebraicGeometry.FormalSpace.isFormalModification_pullback_snd_of_isAdicMorphism

Section88.25 Completions and morphisms, I#

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

Tag 0AR4, a lemma

Tag 0AR4 in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_affine_algebraization_of_isRigEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineRigEtaleAlgebraization.lean, line 320.

Let X = Spec R be a Noetherian affine scheme over S in the big fppf site, let T ⊆ |X| be closed, let W be a Noetherian affine formal algebraic space and let g : W ⟶ X_{/T} be rig-étale. Then there are an affine scheme X' and a morphism f : X' ⟶ X of finite type (locally of finite type and quasi-compact), étale at every point lying over X ∖ T, and an isomorphism X'_{/f⁻¹T} ≅ W compatible with f_{/T} and g. Moreover, if g is étale, that is representable by algebraic spaces and étale, then f is étale.

theorem exists_affine_algebraization_of_isRigEtale
    {R : Type u} [CommRing R] [IsNoetherianRing R] (hR : B.Contains (Spec (.of R)))
    (s : Spec (.of R) ⟶ S)
    (T : Set (Space.points B S hS (yoneda.obj (affineOver B S hS hR s)))) (hT : IsClosed T)
    {W : FppfSheaf B S hS} (hWaff : IsAffineFormalAlgebraicSpace B S hS W)
    (hWnoeth : IsNoetherian B S hS W)
    (g : W ⟶ Space.completionSheaf B S hS (yoneda.obj (affineOver B S hS hR s)) T)
    (hg : IsRigEtale B S hS g) :
    ∃ (X' : BigFppfOver B S hS) (_ : IsAffine ((BigFppfOver.toScheme B S hS).obj X'))
      (f : X' ⟶ affineOver B S hS hR s)
      (e : Space.completionSheaf B S hS (yoneda.obj X')
          (Space.pointsMap B S hS (yoneda.obj X') (yoneda.map f) ⁻¹' T) ≅ W),
      LocallyOfFiniteType ((BigFppfOver.toScheme B S hS).map f) ∧
      QuasiCompact ((BigFppfOver.toScheme B S hS).map f) ∧
      (∀ p : Space.points B S hS (yoneda.obj X'),
        Space.pointsMap B S hS (yoneda.obj X') (yoneda.map f) p ∉ T →
          EtaleAt ((BigFppfOver.toScheme B S hS).map f) (Space.pointsToScheme B S hS X' p)) ∧
      e.hom ≫ g = Space.completionSheafMap B S hS (yoneda.map f) T ∧
      (IsRepresentableEtale B S hS g → Etale ((BigFppfOver.toScheme B S hS).map f))

AlgebraicGeometry.FormalSpace.isEtale_of_isEtale_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionEtale.lean, line 546. The attribute's comment: “the étale clause: a morphism locally of finite type which is étale away from T and whose completion f_{/T} is étale is étale everywhere, by Tag 0A43 (AlgebraicGeometry.etaleAt_of_etale_infinitesimalNeighbourhoods) above the closed subscheme cut out by T. Stated for f locally of finite type over a locally Noetherian X, where the source has f of finite type over an affine Noetherian X. The existence clause of the tag is not stated”.

Let f : X' ⟶ X be a morphism of the big fppf site over S which is locally of finite type, let X be locally Noetherian, let T be a set of points of X and let i : Z ⟶ X be a closed subscheme whose set of points is T. If f is étale at every point of X' outside |f|⁻¹ T and the morphism of completions f_{/T} is étale, then f is étale.

theorem isEtale_of_isEtale_completionSheafMap
    {X' X : BigFppfOver B S hS} (f : X' ⟶ X)
    (T : Set (Space.points B S hS (yoneda.obj X)))
    {Z : Scheme.{u}} (i : Z ⟶ (BigFppfOver.toScheme B S hS).obj X)
    [IsClosedImmersion i]
    [_root_.AlgebraicGeometry.IsLocallyNoetherian ((BigFppfOver.toScheme B S hS).obj X)]
    (hiT : Set.range i = Space.pointsToScheme B S hS X '' T)
    (hf : Space.IsLocallyOfFiniteType B S hS (yoneda.map f))
    (haway : ∀ p : Space.points B S hS (yoneda.obj X'),
      Space.pointsMap B S hS (yoneda.obj X') (yoneda.map f) p ∉ T →
        AlgebraicGeometry.EtaleAt ((BigFppfOver.toScheme B S hS).map f)
          (Space.pointsToScheme B S hS X' p))
    (hetale : ∃ hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
        (Space.completionSheafMap B S hS (yoneda.map f) T).hom,
      Space.HasPropertyULift.{u + 1} B S hS
        (fun ⦃A C : Space.AlgebraicSpacesULift.{u + 1} B S hS⦄ (g : A ⟶ C) ↦
          Space.IsEtaleULift.{u + 1} B S hS g.hom)
        (Space.completionSheafMap B S hS (yoneda.map f) T).hom hrep) :
    Space.IsEtale B S hS (yoneda.map f)
Tag 0AR3, a lemma

Tag 0AR3 in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_etale_completion_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionMorphismsAffine.lean, line 1355.

Let X, X', Y be Noetherian affine schemes of the big fppf site over S, let T ⊆ |X| be closed, let f : X' ⟶ X be locally of finite type and étale over X ∖ T, let h : Y ⟶ X be a morphism and let α : Y_{/T} ⟶ X'_{/T} be a morphism over X_{/T}. Then there are an étale morphism b : Y' ⟶ Y of affine schemes inducing an isomorphism b_{/T} : Y'_{/T} ⟶ Y_{/T} and a morphism a : Y' ⟶ X' over X such that α = a_{/T} ∘ b_{/T}⁻¹.

Here g_{/T} is the completion along T, Space.completionOverFunctor, which sends g : V ⟶ X to V_{/g⁻¹T} ⟶ X_{/T}.

theorem exists_etale_completion_factorization {X X' Y : BigFppfOver B S hS}
    [IsAffine ((BigFppfOver.toScheme B S hS).obj X)]
    [IsNoetherian ((BigFppfOver.toScheme B S hS).obj X)]
    [IsAffine ((BigFppfOver.toScheme B S hS).obj X')]
    [IsNoetherian ((BigFppfOver.toScheme B S hS).obj X')]
    [IsAffine ((BigFppfOver.toScheme B S hS).obj Y)]
    [IsNoetherian ((BigFppfOver.toScheme B S hS).obj Y)]
    (T : Set (Space.points B S hS (yoneda.obj X))) (T_closed : IsClosed T)
    (f : X' ⟶ X) [LocallyOfFiniteType ((BigFppfOver.toScheme B S hS).map f)]
    (hf : ∀ p : Space.points B S hS (yoneda.obj X'),
      Space.pointsMap B S hS (yoneda.obj X') (yoneda.map f) p ∉ T →
        EtaleAt ((BigFppfOver.toScheme B S hS).map f) (Space.pointsToScheme B S hS X' p))
    (h : Y ⟶ X)
    (α : (Space.completionOverFunctor B S hS T).obj (Over.mk (yoneda.map h)) ⟶
      (Space.completionOverFunctor B S hS T).obj (Over.mk (yoneda.map f))) :
    ∃ (Y' : BigFppfOver B S hS) (_ : IsAffine ((BigFppfOver.toScheme B S hS).obj Y'))
      (b : Y' ⟶ Y) (_ : Etale ((BigFppfOver.toScheme B S hS).map b))
      (a : Y' ⟶ X') (comm_ab : a ≫ f = b ≫ h)
      (_ : IsIso ((Space.completionOverFunctor B S hS T).map
        (Over.homMk (yoneda.map b) : Over.mk (yoneda.map b ≫ yoneda.map h) ⟶
          Over.mk (yoneda.map h)))),
      α = inv ((Space.completionOverFunctor B S hS T).map
          (Over.homMk (yoneda.map b) : Over.mk (yoneda.map b ≫ yoneda.map h) ⟶
            Over.mk (yoneda.map h))) ≫
        (Space.completionOverFunctor B S hS T).map
          (Over.homMk (yoneda.map a) (by simp only [Over.mk_hom, ← Functor.map_comp, comm_ab]) :
            Over.mk (yoneda.map b ≫ yoneda.map h) ⟶ Over.mk (yoneda.map f))
Tag 0AR6, a lemma

Tag 0AR6 in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_factorization_of_openComplement_and_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFactorization.lean, line 184. The attribute's comment: “the completion hypothesis is stated on the unsheafified subfunctor of sections with point-set image in T (AlgebraicGeometry.Space.completionSubfunctor), whose sheafification is the completion X_{/T} of Tag 0AMC by Tag 0AIZ, because the completion lands one universe above Y and so admits no morphism to Y in this library; no other hypothesis is carried”.

Stacks 0AR6. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of algebraic spaces over S and let T ⊆ |X| be closed. Assume that X is locally Noetherian, that g is a monomorphism and locally of finite type, that f restricted to the open complement of T factors through g, and that f factors through g on the subfunctor of sections with point-set image in T. Then f factors through g.

The last hypothesis is the factorization on the completion X_{/T} of Stacks 0AMC, stated on the subfunctor whose sheafification that completion is by Stacks 0AIZ; see the module documentation.

theorem exists_factorization_of_openComplement_and_completion
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Z ⟶ Y)
    (T : Set (Space.points B S hS X)) (hT : IsClosed T)
    (hXnoeth : Space.HasEtaleLocalProperty B S hS X
      (fun V : Scheme.{u} => IsLocallyNoetherian V))
    (hgmono : Mono g) (hgft : Space.IsLocallyOfFiniteType B S hS g)
    (hopen : ∃ v : ((Space.openSubspacesOrderIso B S hS X hX).symm
        ⟨Tᶜ, hT.isOpen_compl⟩).1.toFunctor ⟶ Z,
      v ≫ g = ((Space.openSubspacesOrderIso B S hS X hX).symm
        ⟨Tᶜ, hT.isOpen_compl⟩).1.ι ≫ f)
    (hcompletion : ∃ v : (Space.completionSubfunctor B S hS X T).toFunctor ⟶
        Z ⋙ uliftFunctor.{u + 1},
      v ≫ Functor.whiskerRight g uliftFunctor.{u + 1} =
        (Space.completionSubfunctor B S hS X T).ι ≫
          Functor.whiskerRight f uliftFunctor.{u + 1}) :
    ∃ v : X ⟶ Z, v ≫ g = f
Tag 0GI1, a lemma

Tag 0GI1 in the Stacks Project.

AlgebraicGeometry.FormalSpace.eq_of_eq_on_openComplement_of_eq_on_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MorphismEqualityFromCompletion.lean, line 504.

Stacks 0GI1. Let X and W be algebraic spaces over S with X locally Noetherian, let T ⊆ |X| be a closed subset and let a, b : X ⟶ W be morphisms over S which agree on the open subspace X ∖ T and whose completions along T agree. Then a = b.

The equalizer E of a and b is an algebraic space whose projection g : E ⟶ X is a monomorphism locally of finite type — Stacks 03HK — and the two hypotheses factor X ∖ T ⟶ X and X_{/T} ⟶ X through g, so Stacks 0AR6 applied to 𝟙 X and g gives a section v of g. Since g ≫ a = g ≫ b by construction, a = v ≫ g ≫ a = v ≫ g ≫ b = b.

theorem eq_of_eq_on_openComplement_of_eq_on_completion
    (hX : IsAlgebraicSpace B S hS X) (hW : IsAlgebraicSpace B S hS W)
    (hXnoeth : Space.HasEtaleLocalProperty B S hS X
      (fun V : Scheme.{u} => IsLocallyNoetherian V))
    (T : Set (Space.points B S hS X)) (hT : IsClosed T) (a b : X ⟶ W)
    (hopen : (Space.openSubspaceOfPoints B S hS X Tᶜ).ι ≫ a =
      (Space.openSubspaceOfPoints B S hS X Tᶜ).ι ≫ b)
    (hcompletion :
      completionOfAlgebraicSpaceInclusion B S hS hX T ≫ upliftedMap B S hS hX hW a =
        completionOfAlgebraicSpaceInclusion B S hS hX T ≫ upliftedMap B S hS hX hW b) :
    a = b
Tag 0AR7, a lemma

Tag 0AR7 in the Stacks Project.

AlgebraicGeometry.Space.eq_of_eq_on_compl_of_completionSubfunctorMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MorphismUniquenessAlongClosedSubset.lean, line 367.

Stacks 0AR7. Let X and Y be locally Noetherian algebraic spaces over S, let T ⊆ |X| and T' ⊆ |Y| be closed subsets and let a, b : X ⟶ Y be morphisms with |a| (T) ⊆ T' and |b| (T) ⊆ T'. If a and b agree on the open subspace X ∖ T and the induced morphisms of completions a_{/T}, b_{/T} : X_{/T} ⟶ Y_{/T'} agree, then a = b.

theorem eq_of_eq_on_compl_of_completionSubfunctorMap_eq
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hXnoeth : HasEtaleLocalProperty B S hS X (fun V : Scheme.{u} => IsLocallyNoetherian V))
    (_hYnoeth : HasEtaleLocalProperty B S hS Y (fun V : Scheme.{u} => IsLocallyNoetherian V))
    {T : Set (points B S hS X)} (hT : IsClosed T)
    {T' : Set (points B S hS Y)} (_hT' : IsClosed T')
    (a b : X ⟶ Y)
    (ha : pointsMap B S hS X a '' T ⊆ T') (hb : pointsMap B S hS X b '' T ⊆ T')
    (hcompl :
      (openSubspaceOfPoints B S hS X Tᶜ).ι ≫ a = (openSubspaceOfPoints B S hS X Tᶜ).ι ≫ b)
    (hcompletion : completionSubfunctorMap B S hS a T T' ha =
      completionSubfunctorMap B S hS b T T' hb) :
    a = b
Tag 0AR8, a lemma

Tag 0AR8 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isEtaleEquivalenceRelation_of_openComplement_and_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EquivalenceRelationFromCompletion.lean, line 1157. The attribute's comment: “WHAT IS FORMALIZED: hypothesis (3) is read as saying that the formal completion (t_{/T}, s_{/T}) is an étale equivalence relation — an equivalence relation whose two maps s_{/T} and t_{/T} are étale — and not merely an equivalence relation. THE LITERAL READING OF (3) IS FALSE: take X = Spec k and T = |X|, so that X ∖ T is empty and (2) is vacuous, and U = 𝔸¹, R = U ×_X U, t = pr₀, s = pr₁; then X_{/T} = X, U_{/T} = U, R_{/T} = R, so (3) says that the identity is an equivalence relation, (1) and (2) hold, and yet s = pr₁ : 𝔸¹ × 𝔸¹ ⟶ 𝔸¹ is not étale, so the conclusion fails. THE ÉTALE READING IS THE ONE THE SOURCE'S OWN PROOF USES: "Since the formal completions of the maps s, t are étale, we see that s and t are étale for example by More on Morphisms, Lemma 37.12.3". Otherwise the statement is the tag's: hypothesis (2) is read as the restrictions of s and t to the subspaces cut out by the complements of the inverse images of T, which is the base change to X ∖ T by AlgebraicGeometry.FormalSpace.isPullback_ι_openSubspaceOfPoints_compl, and (3) as the restriction morphisms of the completions of Tag 0AMC along those inverse images. No further hypothesis is added and no part of the conclusion is dropped: the conclusion carries monomorphy of (t, s), the equivalence-relation structure, and étaleness of both s and t”.

Let S be a scheme, let X be a locally Noetherian algebraic space over S, let T ⊆ |X| be a closed subset and let s, t : R ⟶ U be two morphisms of algebraic spaces over X. Assume

  1. R and U are locally of finite type over X,
  2. the base change of s and t to X ∖ T is an étale equivalence relation, and
  3. the formal completion (t_{/T}, s_{/T}) : R_{/T} ⟶ U_{/T} ×_{X_{/T}} U_{/T} is an étale equivalence relation.

Then (t, s) : R ⟶ U ×_X U is an étale equivalence relation: it is a monomorphism, t and s form an equivalence relation, and both are étale.

theorem isEtaleEquivalenceRelation_of_openComplement_and_completion
    (hX : IsAlgebraicSpace B S hS X) (hR : IsAlgebraicSpace B S hS R)
    (hU : IsAlgebraicSpace B S hS U)
    (qR : R ⟶ X) (qU : U ⟶ X) (s t : R ⟶ U)
    (hs : s ≫ qU = qR) (ht : t ≫ qU = qR)
    (T : Set (Space.points B S hS X)) (hT : IsClosed T)
    (hXnoeth : Space.HasEtaleLocalProperty B S hS X
      (fun V : Scheme.{u} => _root_.AlgebraicGeometry.IsLocallyNoetherian V))
    (hqR : Space.IsLocallyOfFiniteType B S hS qR)
    (hqU : Space.IsLocallyOfFiniteType B S hS qU)
    (hopen : IsEquivalenceRelation
      (Space.openSubspaceOfPointsRestrict B S hS t _ _
        (compl_subset_preimage_compl B S hS t qU qR ht T))
      (Space.openSubspaceOfPointsRestrict B S hS s _ _
        (compl_subset_preimage_compl B S hS s qU qR hs T)))
    (hopent : Space.IsEtale B S hS (Space.openSubspaceOfPointsRestrict B S hS t _ _
      (compl_subset_preimage_compl B S hS t qU qR ht T)))
    (hopens : Space.IsEtale B S hS (Space.openSubspaceOfPointsRestrict B S hS s _ _
      (compl_subset_preimage_compl B S hS s qU qR hs T)))
    (hcompletion : IsEquivalenceRelation
      (Space.completionSheafRestrict B S hS t _ _
        (preimage_subset_preimage_of_comp B S hS t qU qR ht T))
      (Space.completionSheafRestrict B S hS s _ _
        (preimage_subset_preimage_of_comp B S hS s qU qR hs T)))
    (hcomplt : ∃ hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
        (Space.completionSheafMap B S hS t (Space.pointsMap B S hS U qU ⁻¹' T)).hom,
      Space.HasPropertyULift.{u + 1} B S hS
        (fun ⦃A C : Space.AlgebraicSpacesULift.{u + 1} B S hS⦄ (g : A ⟶ C) ↦
          Space.IsEtaleULift.{u + 1} B S hS g.hom)
        (Space.completionSheafMap B S hS t (Space.pointsMap B S hS U qU ⁻¹' T)).hom hrep)
    (hcompls : ∃ hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS
        (Space.completionSheafMap B S hS s (Space.pointsMap B S hS U qU ⁻¹' T)).hom,
      Space.HasPropertyULift.{u + 1} B S hS
        (fun ⦃A C : Space.AlgebraicSpacesULift.{u + 1} B S hS⦄ (g : A ⟶ C) ↦
          Space.IsEtaleULift.{u + 1} B S hS g.hom)
        (Space.completionSheafMap B S hS s (Space.pointsMap B S hS U qU ⁻¹' T)).hom hrep) :
    Mono (relationMap B S hS qU s t (ht.trans hs.symm)) ∧ IsEquivalenceRelation t s ∧
      Space.IsEtale B S hS s ∧ Space.IsEtale B S hS t
Tag 0AR9, a lemma

Tag 0AR9 in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_factorization_isIso_completionSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleAwayFromClosedFactorization.lean, line 180.

Let X be an algebraic space over S, let T ⊆ |X| be closed with open complement U = X ∖ T, and let f : X' ⟶ X be a morphism of algebraic spaces which is locally of finite type and étale over U. Then f factors as X' ⟶ X'' ⟶ X where X'' ⟶ X is locally of finite type and an isomorphism over U, and X' ⟶ X'' induces an isomorphism X'_{/T} ⟶ X''_{/T} of completions.

Here U is the open subspace with point set Tᶜ, and "over U" is the base change along its inclusion.

theorem exists_factorization_isIso_completionSheafMap
    {X X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hX' : IsAlgebraicSpace B S hS X')
    (T : Set (Space.points B S hS X)) (hT : IsClosed T)
    (f : X' ⟶ X) (hf : Space.IsLocallyOfFiniteType B S hS f)
    (hfU : Space.IsEtale B S hS (pullback.snd f
      ((Space.openSubspacesOrderIso B S hS X hX).symm ⟨Tᶜ, hT.isOpen_compl⟩).1.ι)) :
    ∃ (X'' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS X'')
      (g : X' ⟶ X'') (p : X'' ⟶ X),
      g ≫ p = f ∧ Space.IsLocallyOfFiniteType B S hS p ∧
        IsIso (pullback.snd p
          ((Space.openSubspacesOrderIso B S hS X hX).symm ⟨Tᶜ, hT.isOpen_compl⟩).1.ι) ∧
        IsIso (Space.completionSheafMap B S hS g (Space.pointsMap B S hS X'' p ⁻¹' T))

AlgebraicGeometry.FormalSpace.exists_factorization_of_isEtale_openComplementRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleOutsideFactorization.lean, line 447. The attribute's comment: “stated without the hypothesis that X be locally Noetherian, which the source's proof does not use; X'' ⟶ X is an isomorphism over U in the form that its base change to the open subspace with point set |X| ∖ T is an isomorphism, and the completions are the completionSheafMap of Section 0GDB”.

Stacks 0AR9. Let S be a scheme contained in a big fppf site B, let X be an algebraic space over S and let T ⊆ |X| be closed. Let f : X' ⟶ X be a morphism of algebraic spaces which is locally of finite type and étale outside of T, i.e. whose restriction U' = f⁻¹U ⟶ U to the open subspace U with |U| = |X| ∖ T is étale. Then f factors as X' ⟶ X'' ⟶ X where

  • X'' is an algebraic space and X'' ⟶ X is locally of finite type,
  • X'' ⟶ X is an isomorphism over U: its base change to U is an isomorphism, and
  • X'_{/T} ⟶ X''_{/T} is an isomorphism, the completion of X' ⟶ X'' along the inverse image of T in the sense of Section 0GDB, AlgebraicGeometry.Space.completionSheafMap.

The source assumes moreover that X is locally Noetherian; its proof does not use that hypothesis, so it is dropped here.

theorem exists_factorization_of_isEtale_openComplementRestriction
    {X X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hX' : IsAlgebraicSpace B S hS X') (T : Set (Space.points B S hS X)) (hT : IsClosed T)
    (f : X' ⟶ X) (hft : Space.IsLocallyOfFiniteType B S hS f)
    (het : Space.IsEtale B S hS (Space.openComplementRestriction B S hS f T)) :
    ∃ (X'' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS X'')
      (g : X' ⟶ X'') (h : X'' ⟶ X), g ≫ h = f ∧ Space.IsLocallyOfFiniteType B S hS h ∧
        IsIso (pullback.snd h (Space.openSubspaceOfPoints B S hS X Tᶜ).ι) ∧
        IsIso (Space.completionSheafMap B S hS g (Space.pointsMap B S hS X'' h ⁻¹' T))
Sources
LeanAlgebraicGeometry.FormalSpace.exists_affine_algebraization_of_isRigEtale · AlgebraicGeometry.FormalSpace.isEtale_of_isEtale_completionSheafMap · AlgebraicGeometry.FormalSpace.exists_etale_completion_factorization · AlgebraicGeometry.FormalSpace.exists_factorization_of_openComplement_and_completion · AlgebraicGeometry.FormalSpace.eq_of_eq_on_openComplement_of_eq_on_completion · AlgebraicGeometry.Space.eq_of_eq_on_compl_of_completionSubfunctorMap_eq · AlgebraicGeometry.FormalSpace.isEtaleEquivalenceRelation_of_openComplement_and_completion · AlgebraicGeometry.FormalSpace.exists_factorization_isIso_completionSheafMap

Section88.26 Rig glueing of morphisms#

Section 88.26 of the Stacks Project, Tag 0GI2. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GI3, a proposition

Tag 0GI3 in the Stacks Project.

AlgebraicGeometry.Space.morToModificationCompletion_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MorphismsFromProperModification.lean, line 214. The attribute's comment: “injectivity of the comparison map”.

Stacks 0GI3, injectivity. Let X be a locally Noetherian algebraic space over S, let T ⊆ |X| be a closed subset with complementary open subspace U ⊆ X, and let f : X' ⟶ X be a proper morphism of algebraic spaces whose base change f⁻¹(U) ⟶ U is an isomorphism. For every algebraic space W over S a morphism X ⟶ W is determined by its restriction to X' together with the morphism X_{/T} ⟶ W it induces.

theorem morToModificationCompletion_injective
    {X' X W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (_hX' : IsAlgebraicSpace B S hS X')
    (hW : IsAlgebraicSpace B S hS W)
    (hXnoeth : HasEtaleLocalProperty B S hS X (fun V : Scheme.{u} => IsLocallyNoetherian V))
    {T : Set (points B S hS X)} (hT : IsClosed T)
    (f : X' ⟶ X) (_hfproper : IsProper B S hS f)
    (hfU : IsIso (pullback.snd f (openSubspaceOfPoints B S hS X Tᶜ).ι)) :
    Function.Injective (morToModificationCompletion B S hS f T W)

AlgebraicGeometry.Space.morToModificationCompletion_codRestrict_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MorphismsFromProperModificationExistence.lean, line 173.

Stacks 0GI3. Let S be a scheme, X a locally Noetherian algebraic space over S, T ⊆ |X| a closed subset with complementary open subspace U ⊆ X, and f : X' ⟶ X a proper morphism of algebraic spaces such that f⁻¹(U) ⟶ U is an isomorphism. For any algebraic space W over S the map Mor_S(X, W) ⟶ Mor_S(X', W) ×_{Mor_S(X'_{/T}, W)} Mor_S(X_{/T}, W), sending w to its restriction to X' and the morphism it induces on the completion X_{/T}, is bijective.

theorem morToModificationCompletion_codRestrict_bijective
    {X' X W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hX' : IsAlgebraicSpace B S hS X')
    (hW : IsAlgebraicSpace B S hS W)
    (hXnoeth : HasEtaleLocalProperty B S hS X (fun V : Scheme.{u} => IsLocallyNoetherian V))
    {T : Set (points B S hS X)} (hT : IsClosed T)
    (f : X' ⟶ X) (hfproper : IsProper B S hS f)
    (hfU : IsIso (pullback.snd f (openSubspaceOfPoints B S hS X Tᶜ).ι)) :
    Function.Bijective (Set.codRestrict (morToModificationCompletion B S hS f T W)
      {p | completionMap B S hS f T ≫ p.2 =
        (completionSubfunctor B S hS X' (pointsMap B S hS X' f ⁻¹' T)).ι ≫
          Functor.whiskerRight p.1 uliftFunctor.{u + 1}}
      (morToModificationCompletion_compatible B S hS f T W))
Sources
LeanAlgebraicGeometry.Space.morToModificationCompletion_injective · AlgebraicGeometry.Space.morToModificationCompletion_codRestrict_bijective

Section88.27 Algebraization of rig-étale morphisms#

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

Tag 0AR5, an equation

Tag 0AR5 in the Stacks Project.

AlgebraicGeometry.FormalSpace.completionModificationFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionModificationFunctor.lean, line 102. The attribute's comment: “the completion functor with the source's hypotheses only: X a locally Noetherian algebraic space and T closed; the three conditions placing f_{/T} in the right-hand category are proved by 0AIZ, 0AQ1 (2) and 0AR2”.

Stacks 0AR5. Let X be a locally Noetherian algebraic space over S, let T ⊆ |X| be closed and let U ⊂ X be the open subspace with |U| = |X| ∖ T. Completion along T is a functor from the morphisms f : X' ⟶ X of algebraic spaces which are locally of finite type and an isomorphism over U to the morphisms g : W ⟶ X_{/T} of formal algebraic spaces with W locally Noetherian and g rig-étale.

The arrow map is AlgebraicGeometry.Space.completionOverFunctor. The three conditions on the value are proved: X'_{/T'} is a formal algebraic space by Stacks 0AIZ, it is locally Noetherian by Stacks 0AQ1 (2) since X' is locally of finite type over the locally Noetherian X, and f_{/T} is rig-étale by Stacks 0AR2 since U' ⟶ U is an isomorphism.

This is a new object and not a copy of AlgebraicGeometry.FormalSpace.completionFiniteTypeModificationFunctor: that functor is only defined when three hypotheses (h0AIZ, hnoeth, hred) are given, and this one needs none of them. When they are given, the two functors are equal (completionFiniteTypeModificationFunctor_eq_completionModificationFunctor).

def completionModificationFunctor {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (T : Set (Space.points B S hS X)) (hT : IsClosed T) (hXsp : IsAlgebraicSpace B S hS X)
    (hX : Space.IsLocallyNoetherian B S hS X) :
    Space.FiniteTypeModification B S hS (Space.openSubspaceOfPoints B S hS X Tᶜ) ⥤
      RigEtaleOverCompletion B S hS X T

AlgebraicGeometry.FormalSpace.completionOfFiniteTypeModification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionRigEtale.lean, line 431. The attribute's comment: “the arrow of the displayed equation, that is the assignment sending a morphism locally of finite type which is an isomorphism over U to its completion along T, together with the three conditions placing the result in the right-hand collection. The rig-étaleness, which is what the source says makes the arrow well defined, is Stacks 0AR2 (AlgebraicGeometry.FormalSpace.isRigEtale_completionSheafMap) applied through the proof here that U' is the fibre product of U with f, so that the modification condition makes U' ⟶ U an isomorphism and therefore étale. The two conditions on the source X'_{/T'} are hypotheses: Stacks 0AIZ, that a completion along a closed set is a formal algebraic space, as h0AIZ, and its locally Noetherian refinement as hnoeth; neither is carried by this library, which proves only the affine case Stacks 0AIY of the first. The reduction of Stacks 0AR2 to the affine case is forwarded as hred”.

Stacks 0AR5. The arrow of the displayed equation: a morphism f : X' ⟶ X of algebraic spaces over S which is locally of finite type and an isomorphism over U is sent to f_{/T} : X'_{/T'} ⟶ X_{/T}, a rig-étale morphism with locally Noetherian source.

That f_{/T} is rig-étale is Stacks 0AR2 applied to U' ⟶ U, which is an isomorphism — and hence étale — because U' is the fibre product of U with f.

def completionOfFiniteTypeModification {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (T : Set (Space.points B S hS X)) (hT : IsClosed T)
    (hX : Space.IsLocallyNoetherian B S hS X)
    (M : Space.FiniteTypeModification B S hS (Space.openSubspaceOfPoints B S hS X Tᶜ))
    (h0AIZ : IsFormalAlgebraicSpaceCompletionSheaf B S hS X T)
    (hnoeth : IsLocallyNoetherianCompletionSheaf B S hS X T)
    (hred : ChartSquareReducesToIsEtaleOutside B S hS M.obj.hom T) :
    RigEtaleOverCompletion B S hS X T

AlgebraicGeometry.FormalSpace.completionFiniteTypeModificationFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionRigEtaleFunctor.lean, line 120. The attribute's comment: “the displayed assignment as a FUNCTOR, not only on objects: the object map is AlgebraicGeometry.FormalSpace.completionOfFiniteTypeModification, which is what this library already carried for Stacks 0AR5, and the arrow map is the completion along T of a morphism over X, which is AlgebraicGeometry.Space.completionOverFunctor and carries no hypotheses. The three conditions placing the value in the right-hand collection are the hypotheses of the object map, unchanged except that the reduction of Stacks 0AR2 to the affine case is asked of every object of the source category rather than of one, which is the only form in which a functor can carry it: Stacks 0AIZ for the algebraic spaces over X as h0AIZ, its locally Noetherian refinement from Stacks 0AQ1 as hnoeth, and the reduction of Stacks 0AR2 as hred”.

Stacks 0AR5, as a functor. Sending a finite-type modification f : X' ⟶ X of X outside U to f_{/T} : X'_{/T'} ⟶ X_{/T} is a functor to the rig-étale morphisms with locally Noetherian source over X_{/T}.

def completionFiniteTypeModificationFunctor {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (T : Set (Space.points B S hS X)) (hT : IsClosed T)
    (hX : Space.IsLocallyNoetherian B S hS X)
    (h0AIZ : IsFormalAlgebraicSpaceCompletionSheaf B S hS X T)
    (hnoeth : IsLocallyNoetherianCompletionSheaf B S hS X T)
    (hred : ChartSquareReducesToIsEtaleOutsideModifications T) :
    Space.FiniteTypeModification B S hS (Space.openSubspaceOfPoints B S hS X Tᶜ) ⥤
      RigEtaleOverCompletion B S hS X T
Tag 0GDQ, a lemma

Tag 0GDQ in the Stacks Project.

AlgebraicGeometry.FormalSpace.completionModificationFunctorBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionRigEtaleBaseChange.lean, line 111.

Stacks 0GDQ. Let X be a locally Noetherian algebraic space over S, let T ⊆ |X| be closed with open complement U, and let g : X₁ ⟶ X be a morphism of algebraic spaces with X₁ locally Noetherian; write T₁ = |g|⁻¹T and U₁ = g⁻¹U. Then the square 

  C_{X,T}   ⟶  C_{X_{/T}}
     ↓              ↓
  C_{X₁,T₁} ⟶  C_{X_{1,/T_1}}
commutes, where the horizontal arrows are the functors of Stacks 0AR5, the left vertical arrow is base change along g and the right vertical arrow is base change along X_{1, /T_1} ⟶ X_{/T}. Base change being defined by a universal property, commutativity is a natural isomorphism of the two composite functors.

The proof is the source's: the completion functor (h : Y ⟶ X) ↦ Y_{/T} commutes with fibre products.

def completionModificationFunctorBaseChangeIso {X₁ X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (g : X₁ ⟶ X) (T : Set (Space.points B S hS X)) (hT : IsClosed T)
    (hX₁sp : IsAlgebraicSpace B S hS X₁) (hXsp : IsAlgebraicSpace B S hS X)
    (hX₁ : Space.IsLocallyNoetherian B S hS X₁) (hX : Space.IsLocallyNoetherian B S hS X) :
    Space.finiteTypeBaseChangePointsFunctor hX₁sp hXsp g T ⋙
        completionModificationFunctor (Space.pointsMap B S hS X₁ g ⁻¹' T)
          (hT.preimage (Space.continuous_pointsMap B S hS g)) hX₁sp hX₁ ≅
      completionModificationFunctor T hT hXsp hX ⋙
        rigEtaleOverCompletionPullback g T hT hX₁sp hXsp hX₁ hX

AlgebraicGeometry.FormalSpace.completionFiniteTypeModificationFunctorBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionRigEtaleFunctor.lean, line 184. The attribute's comment: “the commutativity of the square, as an isomorphism of the two composite functors rather than an equality, the two completion functors being defined by a sheafification; and conditional on the right vertical arrow, which is the hypothesis D together with hD saying that D restricts base change along X_{1, /T_1} ⟶ X_{/T}: the categories of Stacks 0AS2 are realized here as full subcategories of an over-category, and base change on them is not available in this repository without the fibre products of formal algebraic spaces that Stacks 0AS2 provides”.

The square of Stacks 0GDQ, for the categories of Stacks 0AS2 and 0AR5 and conditional on its right vertical arrow. Base change along g : X₁ ⟶ X on finite-type modifications followed by the functor of Stacks 0AR5 for X₁ and T₁ = |g|⁻¹T agrees with the functor of Stacks 0AR5 for X and T followed by any functor restricting base change along X_{1, /T_1} ⟶ X_{/T}.

The commutativity is the one the source's proof gives: the completion functor (h : Y ⟶ X) ↦ Y_{/T} commutes with fibre products, which is AlgebraicGeometry.Space.completionBaseChangeIso and, after restriction to the two subcategories, AlgebraicGeometry.Space.restrictedCompletionBaseChangeSquareIso.

def completionFiniteTypeModificationFunctorBaseChangeIso
    {X₁ X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X₁ ⟶ X)
    (hX₁sp : IsAlgebraicSpace B S hS X₁) (hXsp : IsAlgebraicSpace B S hS X)
    (T : Set (Space.points B S hS X)) (hT : IsClosed T)
    (hX : Space.IsLocallyNoetherian B S hS X)
    (h0AIZ : IsFormalAlgebraicSpaceCompletionSheaf B S hS X T)
    (hnoeth : IsLocallyNoetherianCompletionSheaf B S hS X T)
    (hred : ChartSquareReducesToIsEtaleOutsideModifications T)
    (hX₁ : Space.IsLocallyNoetherian B S hS X₁)
    (h0AIZ₁ : IsFormalAlgebraicSpaceCompletionSheaf B S hS X₁
      (Space.pointsMap B S hS X₁ g ⁻¹' T))
    (hnoeth₁ : IsLocallyNoetherianCompletionSheaf B S hS X₁
      (Space.pointsMap B S hS X₁ g ⁻¹' T))
    (hred₁ : ChartSquareReducesToIsEtaleOutsideModifications
      (Space.pointsMap B S hS X₁ g ⁻¹' T))
    {D : RigEtaleOverCompletion B S hS X T ⥤
      RigEtaleOverCompletion B S hS X₁ (Space.pointsMap B S hS X₁ g ⁻¹' T)}
    (hD : D ⋙ ObjectProperty.ι (fun W : Over (Space.completionSheaf B S hS X₁
            (Space.pointsMap B S hS X₁ g ⁻¹' T)) =>
          IsFormalAlgebraicSpace B S hS W.left ∧ IsLocallyNoetherian B S hS W.left ∧
            IsRigEtale B S hS W.hom) ≅
      ObjectProperty.ι (fun W : Over (Space.completionSheaf B S hS X T) =>
          IsFormalAlgebraicSpace B S hS W.left ∧ IsLocallyNoetherian B S hS W.left ∧
            IsRigEtale B S hS W.hom) ⋙
        Over.pullback (Space.completionSheafMap B S hS g T)) :
    Space.finiteTypeBaseChangePointsFunctor hX₁sp hXsp g T ⋙
        completionFiniteTypeModificationFunctor (Space.pointsMap B S hS X₁ g ⁻¹' T)
          (hT.preimage (Space.continuous_pointsMap B S hS g)) hX₁ h0AIZ₁ hnoeth₁ hred₁ ≅
      completionFiniteTypeModificationFunctor T hT hX h0AIZ hnoeth hred ⋙ D
Tag 0GDR, a lemma

Tag 0GDR in the Stacks Project.

AlgebraicGeometry.Space.completionOverFunctor_map_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineCompletionLift.lean, line 824.

Stacks 0GDR. Let X be a locally Noetherian algebraic space over S, T ⊆ |X| closed and U ⊂ X the open subspace with |U| = |X| ∖ T. Let f : X' ⟶ X be a morphism of algebraic spaces which is locally of finite type and an isomorphism over U, and let g : Y ⟶ X be a morphism with Y a locally Noetherian algebraic space. Then completion along T (AlgebraicGeometry.Space.completionOverFunctor, the completion of Section 0GDB used in Stacks 0AR5) is a bijection from the morphisms Y ⟶ X' over X to the morphisms Y_{/T} ⟶ X'_{/T} over X_{/T}.

Injectivity is AlgebraicGeometry.Space.completionOverFunctor_map_injective; surjectivity is AlgebraicGeometry.Space.exists_completionOverFunctor_map_eq_of_affineCompletionLiftProperty applied to its affine case AlgebraicGeometry.Space.affineCompletionLiftProperty. The consequence that the functor of Stacks 0AR5 is fully faithful is AlgebraicGeometry.FormalSpace.finiteTypeModificationCompletionFullyFaithful.

theorem completionOverFunctor_map_bijective {X X' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hXnoeth : HasEtaleLocalProperty B S hS X
      (fun V : Scheme.{u} => _root_.AlgebraicGeometry.IsLocallyNoetherian V))
    {T : Set (points B S hS X)} (hT : IsClosed T) {f : X' ⟶ X}
    (hX' : IsAlgebraicSpace B S hS X') (hf : IsLocallyOfFiniteType B S hS f)
    (hfU : IsIso (pullback.snd f (openSubspaceOfPoints B S hS X Tᶜ).ι)) (g : Y ⟶ X)
    (hY : IsAlgebraicSpace B S hS Y)
    (hYnoeth : HasEtaleLocalProperty B S hS Y
      (fun V : Scheme.{u} => _root_.AlgebraicGeometry.IsLocallyNoetherian V)) :
    Function.Bijective
      (fun a : Over.mk g ⟶ Over.mk f => (completionOverFunctor B S hS T).map a)

AlgebraicGeometry.FormalSpace.finiteTypeModificationCompletionFullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineCompletionLift.lean, line 863. The attribute's comment: “in particular: the functor of Stacks 0AR5 is fully faithful”.

Stacks 0GDR, the consequence: the functor of Stacks 0AR5 is fully faithful. For a locally Noetherian algebraic space X and a closed T ⊆ |X|, completion along T is fully faithful on the morphisms X' ⟶ X locally of finite type which are an isomorphism over the open subspace with points |X| ∖ T. The functor of Stacks 0AR5, AlgebraicGeometry.FormalSpace.completionFiniteTypeModificationFunctor, is this functor with its values regarded in the full subcategory of rig-étale morphisms with locally Noetherian formal source (AlgebraicGeometry.FormalSpace.completionFiniteTypeModificationFunctor_comp_ι). Fullness and faithfulness are the two halves of the bijection AlgebraicGeometry.Space.completionOverFunctor_map_bijective, applied to a finite-type modification M as the locally Noetherian source: M is locally Noetherian because it is locally of finite type over X.

noncomputable def finiteTypeModificationCompletionFullyFaithful
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hXnoeth : Space.HasEtaleLocalProperty B S hS X
      (fun V : Scheme.{u} => _root_.AlgebraicGeometry.IsLocallyNoetherian V))
    (T : Set (Space.points B S hS X)) (hT : IsClosed T) :
    (finiteTypeModificationCompletion (B := B) (S := S) (hS := hS) T).FullyFaithful
Tag 0ARA, a lemma

Tag 0ARA in the Stacks Project.

AlgebraicGeometry.FormalSpace.isEquivalence_completionModificationFunctor_affineOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineCompletionEssentialSurjectivity.lean, line 931.

Stacks 0ARA. Let S be a scheme, let X be a locally Noetherian algebraic space over S which is affine, so X = Spec R with R Noetherian, let T ⊆ |X| be closed and let U ⊂ X be the open subspace with |U| = |X| ∖ T. Then the completion functor of Stacks 0AR5, AlgebraicGeometry.FormalSpace.completionModificationFunctor, from the morphisms f : X' ⟶ X of algebraic spaces which are locally of finite type and an isomorphism over U to the morphisms g : W ⟶ X_{/T} of formal algebraic spaces with W locally Noetherian and g rig-étale, is an equivalence.

Full faithfulness is Stacks 0GDR (AlgebraicGeometry.FormalSpace.completionModificationFunctorFullyFaithful). Essential surjectivity is exists_finiteTypeModification_completion_iso_of_isRigEtale, assembled as in the source from Step 1 (Stacks 0AR4 and 0AR9), Step 2 (a separated W: Stacks 0AR8 and 04S6 applied to the algebraizations of an affine étale covering) and Step 3 (a general W, whose Wᵢ ×_W Wⱼ are separated).

theorem isEquivalence_completionModificationFunctor_affineOver
    {R : Type u} [CommRing R] [IsNoetherianRing R] (hR : B.Contains (Spec (.of R)))
    (s : Spec (.of R) ⟶ S)
    (T : Set (Space.points B S hS (yoneda.obj (affineOver B S hS hR s)))) (hT : IsClosed T) :
    (completionModificationFunctor T hT (isAlgebraicSpace_yoneda B S hS (affineOver B S hS hR s))
      (Space.isLocallyNoetherian_yoneda_affineOver hR s)).IsEquivalence
Tag 0ARB, a theorem

Tag 0ARB in the Stacks Project.

AlgebraicGeometry.FormalSpace.isEquivalence_completionModificationFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionModificationEquivalence.lean, line 75.

Stacks 0ARB. Let X be a locally Noetherian algebraic space over S, let T ⊆ |X| be closed and let U ⊂ X be the open subspace with |U| = |X| ∖ T. The completion functor of Stacks 0AR5 sends f : X' ⟶ X to f_{/T} : X'_{/T'} ⟶ X_{/T}. Its source is the morphisms of algebraic spaces which are locally of finite type and an isomorphism over U. Its target is the morphisms g : W ⟶ X_{/T} of formal algebraic spaces with W locally Noetherian and g rig-étale. This functor is an equivalence.

Full faithfulness is Stacks 0GDR (completionModificationFunctorFullyFaithful). For essential surjectivity, the base change of W to each affine étale chart Spec R ⟶ X, R Noetherian, is an object of the right-hand category for Spec R (rigEtaleOverCompletionBaseChange, through Stacks 0GD1). By Stacks 0ARA (exists_finiteTypeModification_completion_iso_of_isRigEtale) it is the completion of a finite-type modification of Spec R. These glue (mem_essImage_completionModificationFunctor_of_affine_charts).

theorem isEquivalence_completionModificationFunctor {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (T : Set (Space.points B S hS X)) (hT : IsClosed T) (hXsp : IsAlgebraicSpace B S hS X)
    (hX : Space.IsLocallyNoetherian B S hS X) :
    (completionModificationFunctor T hT hXsp hX).IsEquivalence
Sources
LeanAlgebraicGeometry.FormalSpace.completionModificationFunctor · AlgebraicGeometry.FormalSpace.completionOfFiniteTypeModification · AlgebraicGeometry.FormalSpace.completionFiniteTypeModificationFunctor · AlgebraicGeometry.FormalSpace.completionModificationFunctorBaseChangeIso · AlgebraicGeometry.FormalSpace.completionFiniteTypeModificationFunctorBaseChangeIso · AlgebraicGeometry.Space.completionOverFunctor_map_bijective · AlgebraicGeometry.FormalSpace.finiteTypeModificationCompletionFullyFaithful · AlgebraicGeometry.FormalSpace.isEquivalence_completionModificationFunctor_affineOver

Section88.28 Completions and morphisms, II#

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

Tag 0ARU, a lemma

Tag 0ARU in the Stacks Project.

AlgebraicGeometry.FormalSpace.isQuasiCompact_iff_isQuasiCompact_of_overIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionQuasiCompactIff.lean, line 456.

Stacks 0ARU. Let X be a locally Noetherian algebraic space over S, let T ⊆ |X| be a closed subset and let U ⊂ X be the open subspace with |U| = |X| ∖ T. Let f : X' ⟶ X be a morphism of algebraic spaces which is locally of finite type and such that f⁻¹U ⟶ U is an isomorphism, and let g : W ⟶ X_{/T} correspond to f under the completion functor of Stacks 0AR5, that is, be isomorphic over X_{/T} to f_{/T} : X'_{/T'} ⟶ X_{/T}. Then f is quasi-compact if and only if g is quasi-compact.

theorem isQuasiCompact_iff_isQuasiCompact_of_overIso
    {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 T)
    (M : Space.FiniteTypeModification B S hS (Space.openSubspaceOfPoints B S hS X Tᶜ))
    {W : FppfSheaf B S hS} (g : W ⟶ Space.completionSheaf B S hS X T)
    (e : Over.mk g ≅ Over.mk (Space.completionSheafMap B S hS M.obj.hom T)) :
    Space.IsQuasiCompact B S hS M.obj.hom ↔ IsQuasiCompact B S hS g
Tag 0ARV, a lemma

Tag 0ARV in the Stacks Project.

AlgebraicGeometry.FormalSpace.isQuasiSeparated_iff_hasQuasiCompactDiagonal_of_overIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionQuasiSeparatedIff.lean, line 246.

Stacks 0ARV. Let X be a locally Noetherian algebraic space over S, let T ⊆ |X| be a closed subset and let U ⊂ X be the open subspace with |U| = |X| ∖ T. Let f : X' ⟶ X be a morphism of algebraic spaces which is locally of finite type and such that f⁻¹U ⟶ U is an isomorphism, and let g : W ⟶ X_{/T} correspond to f under the equivalence of Stacks 0ARB (isEquivalence_completionModificationFunctor), that is, be isomorphic over X_{/T} to the completion f_{/T} : X'_{/T'} ⟶ X_{/T}, the value at f of the functor completionModificationFunctor of Stacks 0AR5. Then f is quasi-separated (Stacks 03HL, part (3)) if and only if g is quasi-separated (Stacks 0ARN, part (2)).

theorem isQuasiSeparated_iff_hasQuasiCompactDiagonal_of_overIso
    {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 T)
    (M : Space.FiniteTypeModification B S hS (Space.openSubspaceOfPoints B S hS X Tᶜ))
    {W : FppfSheaf B S hS} (g : W ⟶ Space.completionSheaf B S hS X T)
    (e : Over.mk g ≅ Over.mk (Space.completionSheafMap B S hS M.obj.hom T)) :
    Space.IsQuasiSeparated B S hS M.obj.hom ↔ HasQuasiCompactDiagonal B S hS g
Tag 0ARW, a lemma

Tag 0ARW in the Stacks Project.

AlgebraicGeometry.FormalSpace.isSeparated_iff_isSeparatedMorphism_and_isRigSurjective_diagonal_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ModificationOutputSeparated.lean, line 240. The attribute's comment: “the correspondence f ↔ g of Theorem 0ARB is rendered as an isomorphism over X_{/T} between the image f_{/T} of f under the completion functor of Stacks 0AR5 and an object g of the right-hand category of Stacks 0AR5; the equivalence of Theorem 0ARB itself is not used. Separatedness of g is the separatedness axiom of Stacks 0ARN, part (1)”.

Stacks 0ARW. Let X be a locally Noetherian algebraic space over S, let T ⊆ |X| be closed with open complement U, and let f : X' ⟶ X be a finite-type modification of X outside U (Stacks 0AS2), corresponding to an object g : W ⟶ X_{/T} of the right-hand category of Stacks 0AR5 — a rig-étale morphism with W a locally Noetherian formal algebraic space — through an isomorphism over X_{/T} between f_{/T} and g. Then f is separated if and only if g is separated (Stacks 0ARN) and its relative diagonal Δ_g : W ⟶ W ×_{X_{/T}} W is rig-surjective.

theorem isSeparated_iff_isSeparatedMorphism_and_isRigSurjective_diagonal_of_iso
    {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 T)
    (M : Space.FiniteTypeModification B S hS (Space.openSubspaceOfPoints B S hS X Tᶜ))
    (P : RigEtaleOverCompletion B S hS X T)
    (e : (Space.completionOverFunctor B S hS T).obj M.obj ≅ P.obj) :
    Space.IsSeparated B S hS M.obj.hom ↔
      IsSeparatedMorphism B S hS P.obj.hom ∧
        IsRigSurjective B S hS (pullback.diagonal P.obj.hom)
Tag 0ARX, a lemma

Tag 0ARX in the Stacks Project.

AlgebraicGeometry.FormalSpace.isProper_iff_isFormalModification_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ModificationOutputProper.lean, line 820. The attribute's comment: “the correspondence f ↔ g of Theorem 0ARB is rendered as an isomorphism over X_{/T} between the image f_{/T} of f under the completion functor of Stacks 0AR5 and an object g of the right-hand category of Stacks 0AR5; the equivalence of Theorem 0ARB itself is not used”.

Let X be a locally Noetherian algebraic space over S, let T ⊆ |X| be closed with open complement U, and let f : X' ⟶ X be a finite-type modification of X outside U (Stacks 0AS2), corresponding to an object g : W ⟶ X_{/T} of the right-hand category of Stacks 0AR5 — a rig-étale morphism with W a locally Noetherian formal algebraic space — through an isomorphism over X_{/T} between f_{/T} and g. Then f is proper if and only if g is a formal modification (Definition 0GDK).

theorem isProper_iff_isFormalModification_of_iso
    {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 T)
    (M : Space.FiniteTypeModification B S hS (Space.openSubspaceOfPoints B S hS X Tᶜ))
    (P : RigEtaleOverCompletion B S hS X T)
    (e : (Space.completionOverFunctor B S hS T).obj M.obj ≅ P.obj) :
    Space.IsProper B S hS M.obj.hom ↔ IsFormalModification B S hS P.obj.hom
Tag 0GI4, a lemma

Tag 0GI4 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isEtale_iff_isRepresentableEtale_of_overIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionEtaleIff.lean, line 75.

Stacks 0GI4. Let X be a locally Noetherian algebraic space over S, let T ⊆ |X| be a closed subset and let U ⊂ X be the open subspace with |U| = |X| ∖ T. Let f : X' ⟶ X be a morphism of algebraic spaces which is locally of finite type and such that f⁻¹U ⟶ U is an isomorphism, and let g : W ⟶ X_{/T} correspond to f under the equivalence of Stacks 0ARB, that is, be isomorphic over X_{/T} to f_{/T} : X'_{/T'} ⟶ X_{/T}. Then f is étale if and only if g is étale.

theorem isEtale_iff_isRepresentableEtale_of_overIso
    {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 T)
    (M : Space.FiniteTypeModification B S hS (Space.openSubspaceOfPoints B S hS X Tᶜ))
    {W : FppfSheaf B S hS} (g : W ⟶ Space.completionSheaf B S hS X T)
    (e : Over.mk g ≅ Over.mk (Space.completionSheafMap B S hS M.obj.hom T)) :
    Space.IsEtale B S hS M.obj.hom ↔ IsRepresentableEtale B S hS g
Sources
LeanAlgebraicGeometry.FormalSpace.isQuasiCompact_iff_isQuasiCompact_of_overIso · AlgebraicGeometry.FormalSpace.isQuasiSeparated_iff_hasQuasiCompactDiagonal_of_overIso · AlgebraicGeometry.FormalSpace.isSeparated_iff_isSeparatedMorphism_and_isRigSurjective_diagonal_of_iso · AlgebraicGeometry.FormalSpace.isProper_iff_isFormalModification_of_iso · AlgebraicGeometry.FormalSpace.isEtale_iff_isRepresentableEtale_of_overIso

Section88.29 Artin's theorem on dilatations#

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

Tag 0GDU, a theorem

Tag 0GDU in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_isProper_completion_iso_of_isFormalModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionModificationEquivalence.lean, line 105. The attribute's comment: “existence: a proper f : X' ⟶ X, isomorphism over U, with f_{/T} ≅ 𝔣 over X_{/T}”.

Stacks 0GDU, existence. Let X be a locally Noetherian algebraic space over S, let T ⊆ |X| be closed, U ⊂ X the open subspace with |U| = |X| ∖ T, and let 𝔣 : 𝔛' ⟶ X_{/T} be a formal modification (Definition 0GDK). Then there is a proper morphism f : X' ⟶ X of algebraic spaces which is an isomorphism over U and whose completion f_{/T} is isomorphic to 𝔣 over X_{/T}.

By Stacks 0ARB (isEquivalence_completionModificationFunctor), 𝔣, an object of the right-hand category of Stacks 0AR5, is the completion of a finite-type modification f; by Stacks 0ARX (isProper_iff_isFormalModification_of_iso) f is proper.

theorem exists_isProper_completion_iso_of_isFormalModification
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hXsp : IsAlgebraicSpace B S hS X)
    (hX : Space.IsLocallyNoetherian B S hS X) (T : Set (Space.points B S hS X)) (hT : IsClosed T)
    {W : FppfSheaf B S hS} {𝔣 : W ⟶ Space.completionSheaf B S hS X T}
    (h𝔣 : IsFormalModification B S hS 𝔣) :
    ∃ (X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS X') (f : X' ⟶ X),
      Space.IsProper B S hS f ∧ IsIso (pullback.snd f (Space.openSubspaceOfPoints B S hS X Tᶜ).ι) ∧
        Nonempty ((Space.completionOverFunctor B S hS T).obj (Over.mk f) ≅ Over.mk 𝔣)

AlgebraicGeometry.FormalSpace.existsUnique_completionOverFunctor_map_comp_eq_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionModificationEquivalence.lean, line 141. The attribute's comment: “uniqueness: any two such proper f₁, f₂ are isomorphic over X by a unique isomorphism compatible with the identifications of f₁_{/T} and f₂_{/T} with 𝔣”.

Stacks 0GDU, uniqueness. In the situation of exists_isProper_completion_iso_of_isFormalModification, let f₁ : X₁ ⟶ X and f₂ : X₂ ⟶ X be proper morphisms of algebraic spaces which are isomorphisms over U, with isomorphisms e₁ : f₁_{/T} ≅ 𝔣 and e₂ : f₂_{/T} ≅ 𝔣 over X_{/T}. Then there is exactly one morphism φ : X₁ ⟶ X₂ over X whose completion is compatible with e₁ and e₂, and it is an isomorphism. So f is unique up to unique isomorphism.

This is Stacks 0GDR (AlgebraicGeometry.Space.completionOverFunctor_map_bijective), which holds because a proper morphism is locally of finite type.

theorem existsUnique_completionOverFunctor_map_comp_eq_of_isProper
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hXsp : IsAlgebraicSpace B S hS X)
    (hX : Space.IsLocallyNoetherian B S hS X) (T : Set (Space.points B S hS X)) (hT : IsClosed T)
    {W : FppfSheaf B S hS} (𝔣 : W ⟶ Space.completionSheaf B S hS X T)
    {X₁ X₂ : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX₁ : IsAlgebraicSpace B S hS X₁)
    (hX₂ : IsAlgebraicSpace B S hS X₂) {f₁ : X₁ ⟶ X} {f₂ : X₂ ⟶ X}
    (hf₁ : Space.IsProper B S hS f₁) (hf₂ : Space.IsProper B S hS f₂)
    (hU₁ : IsIso (pullback.snd f₁ (Space.openSubspaceOfPoints B S hS X Tᶜ).ι))
    (hU₂ : IsIso (pullback.snd f₂ (Space.openSubspaceOfPoints B S hS X Tᶜ).ι))
    (e₁ : (Space.completionOverFunctor B S hS T).obj (Over.mk f₁) ≅ Over.mk 𝔣)
    (e₂ : (Space.completionOverFunctor B S hS T).obj (Over.mk f₂) ≅ Over.mk 𝔣) :
    ∃! φ : Over.mk f₁ ⟶ Over.mk f₂,
      (Space.completionOverFunctor B S hS T).map φ ≫ e₂.hom = e₁.hom ∧ IsIso φ
Tag 0GDV, a lemma

Tag 0GDV in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_isProper_completionOverFunctor_iso_of_isFormalModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalModificationAlgebraization.lean, line 273.

Stacks 0GDV. Let f : 𝔛' ⟶ 𝔛 be a formal modification (Definition 0GDK) of locally Noetherian formal algebraic spaces over S. Let A be an adic Noetherian topological ring and let g : Spf A ⟶ 𝔛 be an adic morphism, Spf A being a formal algebraic space over S through the quotient system D. Then there are a proper morphism p : X ⟶ Spec A of algebraic spaces and an isomorphism Spf A ×_𝔛 𝔛' ≅ X_{/Z} over Spf A of the base change of f with the formal completion of X along its closed fibre Z = X ×_{Spec A} Spf(A)_red.

Algebraic spaces with no base are algebraic spaces over Spec ℤ, the terminal scheme, and the base change, a formal algebraic space over S, is viewed over Spec ℤ by the change of base of Stacks 04SG (AlgebraicGeometry.FormalSpace.smallerBaseSheafFunctor). The closed fibre is the inverse image under p of the zero locus V(I) of an ideal of definition I, which is the closed subset of Spec A underlying Spf(A)_red; the completion along it is AlgebraicGeometry.Space.completionOverFunctor, and the isomorphism is one over the completion of Spec A along V(I), which is Spf A (AlgebraicGeometry.FormalSpace.formalSpectrumCompletionIso). The statement holds for every ideal of definition I.

As in the source: the base change Spf A ×_𝔛 𝔛' ⟶ Spf A is a formal modification by Stacks 0GDN, and Theorem 0GDU applies to it.

theorem exists_isProper_completionOverFunctor_iso_of_isFormalModification
    {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    (hA : TopologicalRing.IsNoetherianAdic A) (hAB : B.Contains (Spec (.of A)))
    (I : Ideal A) (hI : TopologicalRing.IsIdealOfDefinition I)
    {X' X : FppfSheaf B S hS} (f : X' ⟶ X) (hf : IsFormalModification B S hS f)
    (D : QuotientSystem B S hS A) (g : formalSpectrum D ⟶ X) (hg : IsAdicMorphism B S hS g) :
    ∃ (Y : (BigFppfOver B (⊤_ Scheme.{u}) hZ)ᵒᵖ ⥤ Type u)
      (_ : IsAlgebraicSpace B (⊤_ Scheme.{u}) hZ Y)
      (p : Y ⟶ yoneda.obj (specOverTerminal B hZ hAB)),
      Space.IsProper B (⊤_ Scheme.{u}) hZ p ∧
        Nonempty ((Space.completionOverFunctor B (⊤_ Scheme.{u}) hZ
            (zeroLocusPoints B (⊤_ Scheme.{u}) hZ hAB (terminal.from _) I)).obj (Over.mk p) ≅
          Over.mk ((Ψ).map (pullback.snd f g) ≫
            (formalSpectrumCompletionIso B hZ S hS hAB hA I hI D).hom))
Sources
LeanAlgebraicGeometry.FormalSpace.exists_isProper_completion_iso_of_isFormalModification · AlgebraicGeometry.FormalSpace.existsUnique_completionOverFunctor_map_comp_eq_of_isProper · AlgebraicGeometry.FormalSpace.exists_isProper_completionOverFunctor_iso_of_isFormalModification

Section88.30 Application to modifications#

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

Tag 0AS2, an equation

Tag 0AS2 in the Stacks Project.

AlgebraicGeometry.Space.IsFiniteTypeModification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Modifications.lean, line 113. The attribute's comment: “the three defining conditions”.

Stacks 0AS2. An algebraic space over W, locally of finite type over W and unchanged over W₀.

def IsFiniteTypeModification {W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (W₀ : Subfunctor W)
    (X : Over W) : Prop

AlgebraicGeometry.Space.FiniteTypeModification, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Modifications.lean, line 120. The attribute's comment: “the category they form”.

Stacks 0AS2. The category of algebraic spaces over W which are locally of finite type over W and isomorphisms over W₀.

abbrev FiniteTypeModification {W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (W₀ : Subfunctor W)

AlgebraicGeometry.Space.isFiniteTypeModification_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Modifications.lean, line 130.

Stacks 0AS2. The three conditions of Stacks 0AS2: the source is an algebraic space, the structure morphism is locally of finite type, and its base change to W₀ is an isomorphism. The tag is the set-builder expression delimiting the morphisms that satisfy exactly these three conditions, so this equivalence is the whole of it.

theorem isFiniteTypeModification_iff :
    IsFiniteTypeModification B S hS W₀ X ↔
      IsAlgebraicSpace B S hS X.left ∧ IsLocallyOfFiniteType B S hS X.hom ∧
        IsIso (pullback.snd X.hom W₀.ι)
Tag 0AE5, a lemma

Tag 0AE5 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isEquivalence_affineModificationBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineModificationBaseChange.lean, line 457.

Stacks 0AE5. Let φ : A →+* R be a homomorphism of Noetherian rings inducing an isomorphism from the I-adic completion of A to the I R-adic completion of R, for an ideal I ⊆ A. Then base change along Spec R ⟶ Spec A is an equivalence from the category of Stacks 0AS2 for (A, I) to the category of Stacks 0AS2 for (R, I R).

theorem isEquivalence_affineModificationBaseChange [IsNoetherianRing A] [IsNoetherianRing R]
    (h : Function.Bijective (adicCompletionMap φ I (I.map φ) le_rfl)) :
    (affineModificationBaseChange B S hS φ I hA hR s).IsEquivalence
Tag 0BH5, a lemma

Tag 0BH5 in the Stacks Project.

AlgebraicGeometry.FormalSpace.fpqcLocalProperties_iff_of_affineModificationBaseChange_obj_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineModificationBaseChangeProperties.lean, line 416.

Let φ : A →+* R be a homomorphism of rings, A Noetherian, inducing an isomorphism from the I-adic completion of A to the I R-adic completion of R, as in Stacks 0AE5. Let f : X' ⟶ Spec A, an object of the category of Stacks 0AS2 for (A, I), correspond to g : Y' ⟶ Spec R, an object of the category for (R, I R), under the base change functor of Stacks 0AE5, that is g ≅ f ×_{Spec A} Spec R. Then f is quasi-compact, quasi-separated, separated, proper, respectively finite, if and only if g is.

theorem fpqcLocalProperties_iff_of_affineModificationBaseChange_obj_iso
    [IsNoetherianRing A] (h : Function.Bijective (adicCompletionMap φ I (I.map φ) le_rfl))
    (M : Space.FiniteTypeModification B S hS (Space.openSubspaceOfPoints B S hS
      (yoneda.obj (affineOver B S hS hA s)) (zeroLocusPoints B S hS hA s I)ᶜ))
    (N : Space.FiniteTypeModification B S hS (Space.openSubspaceOfPoints B S hS
      (yoneda.obj (affineOver B S hS hR (Spec.map (CommRingCat.ofHom φ) ≫ s)))
      (zeroLocusPoints B S hS hR (Spec.map (CommRingCat.ofHom φ) ≫ s) (I.map φ))ᶜ))
    (e : (affineModificationBaseChange B S hS φ I hA hR s).obj M ≅ N) :
    (Space.IsQuasiCompact B S hS M.obj.hom ↔ Space.IsQuasiCompact B S hS N.obj.hom) ∧
      (Space.IsQuasiSeparated B S hS M.obj.hom ↔ Space.IsQuasiSeparated B S hS N.obj.hom) ∧
      (Space.IsSeparated B S hS M.obj.hom ↔ Space.IsSeparated B S hS N.obj.hom) ∧
      (Space.IsProper B S hS M.obj.hom ↔ Space.IsProper B S hS N.obj.hom) ∧
      (Space.IsFinite B S hS M.obj.hom ↔ Space.IsFinite B S hS N.obj.hom)
Tag 0AF7, a lemma

Tag 0AF7 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isEquivalence_finiteTypeBaseChange_of_flat_localHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FlatLocalModificationEquivalence.lean, line 84.

Stacks 0AF7. Let A → R be a local homomorphism of Noetherian local rings which is flat, with 𝔪_R = 𝔪_A R and κ(𝔪_A) = κ(𝔪_R). Then the base-change functor along Spec R ⟶ Spec A, from the category (0AS2) for (A, 𝔪_A) to the category (0AS2) for (R, 𝔪_R), is an equivalence. Here Spec A lies over a base scheme S through s, and the categories are the finite-type modifications of the represented spaces outside the complements of V(𝔪_A) and V(𝔪_R).

theorem isEquivalence_finiteTypeBaseChange_of_flat_localHom {A R : Type u} [CommRing A]
    [CommRing R] [IsLocalRing A] [IsLocalRing R] [IsNoetherianRing A] [IsNoetherianRing R]
    [Algebra A R] [IsLocalHom (algebraMap A R)] [Module.Flat A R]
    (hmax : (maximalIdeal A).map (algebraMap A R) = maximalIdeal R)
    (hres : Function.Bijective (ResidueField.map (algebraMap A R)))
    (hA : B.Contains (Spec (.of A))) (hR : B.Contains (Spec (.of R)))
    (s : Spec (.of A) ⟶ S) :
    (Space.finiteTypeBaseChangeFunctorOfEq
      (isAlgebraicSpace_yoneda B S hS
        (affineOver B S hS hR (Spec.map (CommRingCat.ofHom (algebraMap A R)) ≫ s)))
      (isAlgebraicSpace_yoneda B S hS (affineOver B S hS hA s))
      (yoneda.map (affineOverMap (algebraMap A R) hA hR s))
      (Space.openSubspaceOfPoints B S hS _ (zeroLocusPoints B S hS hA s (maximalIdeal A))ᶜ)
      (Space.openSubspaceOfPoints B S hS _
        (zeroLocusPoints B S hS hR _ (maximalIdeal R))ᶜ)
      (by rw [Space.preimage_openSubspaceOfPoints_compl, preimage_zeroLocusPoints, hmax])
      ).IsEquivalence
Tag 0AE6, a lemma

Tag 0AE6 in the Stacks Project.

AlgebraicGeometry.Space.exists_isAdmissibleBlowup_dominating_of_isLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationDomination/LocalRing.lean, line 247.

Stacks 0AE6. Let (A, 𝔪, κ) be a Noetherian local ring, let U = Spec(A) ∖ V(𝔪) and let f : X ⟶ Spec(A) be an object of the category of Stacks 0AS2 for (A, 𝔪) — an algebraic space, locally of finite type over Spec(A), with f⁻¹(U) ⟶ U an isomorphism — such that f is proper. Then there exists a U-admissible blowup S' ⟶ Spec(A) which dominates X, that is, the blowup morphism factors as S' ⟶ X ⟶ Spec(A).

The algebraic spaces are those over an arbitrary base scheme S of the big fppf site, with Spec(A) an object of the site over S; the source's category is that of algebraic spaces over Spec(A), which is the case S = Spec(A). Being a U-admissible blowup is Stacks 086B, AlgebraicGeometry.Space.IsAdmissibleBlowup.

theorem exists_isAdmissibleBlowup_dominating_of_isLocalRing {A : Type u} [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] (hA : B.Contains (Spec (.of A))) (s : Spec (.of A) ⟶ S)
    (X : Over (yoneda.obj (FormalSpace.affineOver B S hS hA s)))
    (hX : IsFiniteTypeModification B S hS
      (openSubspaceOfPoints B S hS (yoneda.obj (FormalSpace.affineOver B S hS hA s))
        (FormalSpace.zeroLocusPoints B S hS hA s (IsLocalRing.maximalIdeal A))ᶜ) X)
    (hf : IsProper B S hS X.hom) :
    ∃ (S' : AlgebraicSpaces B S hS) (b : S' ⟶ schemeSpace (FormalSpace.affineOver B S hS hA s)),
      IsAdmissibleBlowup B S hS
        ⟨openSubspaceOfPoints B S hS (yoneda.obj (FormalSpace.affineOver B S hS hA s))
          (FormalSpace.zeroLocusPoints B S hS hA s (IsLocalRing.maximalIdeal A))ᶜ,
          isOpenSubspace_compl_zeroLocusPoints hA s _⟩ b ∧
        ∃ g : S'.obj ⟶ X.left, g ≫ X.hom = b.hom
Sources
LeanAlgebraicGeometry.Space.IsFiniteTypeModification · AlgebraicGeometry.Space.FiniteTypeModification · AlgebraicGeometry.Space.isFiniteTypeModification_iff · AlgebraicGeometry.FormalSpace.isEquivalence_affineModificationBaseChange · AlgebraicGeometry.FormalSpace.fpqcLocalProperties_iff_of_affineModificationBaseChange_obj_iso · AlgebraicGeometry.FormalSpace.isEquivalence_finiteTypeBaseChange_of_flat_localHom · AlgebraicGeometry.Space.exists_isAdmissibleBlowup_dominating_of_isLocalRing

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.