89 Resolution of Surfaces Revisited

Chapter 89 of the Stacks Project, Resolution of Surfaces Revisited, Tag 0BH6: the 8 sections of its 9 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 27 tags are carried by 77 declarations of the repository (all in StacksFrontier).

Section89.2 Modifications #

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

Tag 0AE2, an equation

Tag 0AE2 in the Stacks Project.

AlgebraicGeometry.Space.puncturedSpectrumSubfunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperModifications.lean, line 57. The attribute's comment: “the punctured spectrum as a subfunctor”.

Stacks 0AE2. The punctured spectrum of a local ring A, as a subfunctor of the functor of points of Spec A on a big fppf site: a point lies in it exactly when the corresponding morphism of schemes factors through the open immersion of the punctured spectrum.

noncomputable def puncturedSpectrumSubfunctor (A : Type u) [CommRing A] [IsLocalRing A]
    (B : BigFppfSite.{u}) (hS : B.Contains (Spec (.of A))) :
    Subfunctor (yoneda.obj (baseTerminal B (Spec (.of A)) hS))

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

Stacks 0AE2. A proper modification of a represented algebraic space T outside a subfunctor U of its functor of points: an algebraic space over T whose structure morphism is proper and whose base change to U is an isomorphism.

def IsProperModification (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (T : BigFppfOver B S hS) (U : Subfunctor (yoneda.obj T))
    (X : Over (yoneda.obj T)) : Prop

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

Stacks 0AE2. The category of proper morphisms of algebraic spaces to Spec A which are isomorphisms over the punctured spectrum of A.

abbrev ProperModification (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (B : BigFppfSite.{u}) (hS : B.Contains (Spec (.of A)))

AlgebraicGeometry.Space.isProperModification_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperModifications.lean, line 92. The attribute's comment: “the conditions spelled out”.

Stacks 0AE2. The three conditions defining a proper modification, spelled out: the source is an algebraic space, its structure morphism is proper, and the base change of that morphism to the subfunctor is an isomorphism.

theorem isProperModification_iff (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (T : BigFppfOver B S hS) (U : Subfunctor (yoneda.obj T)) (X : Over (yoneda.obj T)) :
    IsProperModification B S hS T U X ↔
      IsAlgebraicSpace B S hS X.left ∧ IsProper B S hS X.hom ∧
        IsIso (pullback.snd X.hom U.ι)

Tag 0AE3, a lemma

Tag 0AE3 in the Stacks Project.

AlgebraicGeometry.Space.isProperModification_of_isIntegralModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationNormalPuncturedSurface.lean, line 169.

Stacks 0AE3. Let (A, 𝔪, κ) be a two-dimensional Noetherian local domain whose punctured spectrum U = Spec A ∖ {𝔪} is a normal scheme. Then every modification f : X → Spec A lies in the category of Stacks 0AE2: f is proper and its base change f⁻¹(U) → U to the punctured spectrum is an isomorphism.

theorem isProperModification_of_isIntegralModification [IsDomain A] [IsNoetherianRing A]
    (hdim : ringKrullDim A = 2) [AlgebraicGeometry.IsNormal (Stacks.puncturedSpectrum A).toScheme]
    {X : (BigFppfOver B (Spec (.of A)) hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of A)) hS X)
    (f : X ⟶ yoneda.obj (baseTerminal B (Spec (.of A)) hS))
    (hf : IsIntegralModification B (Spec (.of A)) hS hX
      (isAlgebraicSpace_yoneda B (Spec (.of A)) hS _)
      (isIntegralSpace_yoneda_baseTerminal A B hS) f) :
    IsProperModification B (Spec (.of A)) hS (baseTerminal B (Spec (.of A)) hS)
      (puncturedSpectrumSubfunctor A B hS) (Over.mk f)

Tag 0AGM, a lemma

Tag 0AGM in the Stacks Project.

AlgebraicGeometry.Space.isClosedImmersion_of_isClosedImmersion_specialFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperModificationSpecialFibre.lean, line 198.

Stacks 0AGM. Let (A, 𝔪, κ) be a Noetherian local ring and let g : X ⟶ Y be a morphism of proper modifications of Spec A outside its punctured spectrum. If the induced morphism X_κ ⟶ Y_κ of special fibres — the base change of g along the closed point Spec κ → Spec A — is a closed immersion, then g is a closed immersion.

This is the case Z = Spec A of Stacks 05XA: the open subspace of Spec A that lemma produces contains the closed point, hence is the whole of Spec A.

theorem isClosedImmersion_of_isClosedImmersion_specialFibre
    {X Y : ProperModification A B hS} (g : X ⟶ Y)
    (hg : IsClosedImmersion B (Spec (.of A)) hS
      (baseChangeOverBase B (Spec (.of A)) hS g.hom.left X.1.hom Y.1.hom g.hom.w
        (yoneda.map (residueSpecToBase A B hS)))) :
    IsClosedImmersion B (Spec (.of A)) hS g.hom.left

Tag 0AYJ, a lemma

Tag 0AYJ in the Stacks Project.

AlgebraicGeometry.Space.dimension_fieldFibre_add_one_le_ringKrullDim_of_isIntegralModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationSpecialFibreDimension.lean, line 140. The attribute's comment: “case (1), f a modification”.

Stacks 0AYJ, case (1). Let (A, 𝔪, κ) be a Noetherian local domain of dimension at least one and let f : X → Spec A be a modification. Then the special fibre X_κ has dimension at most dim(A) - 1.

theorem dimension_fieldFibre_add_one_le_ringKrullDim_of_isIntegralModification [IsDomain A]
    [IsNoetherianRing A] (hdim : 1 ≤ ringKrullDim A)
    {X : (BigFppfOver B (Spec (.of A)) hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of A)) hS X)
    (f : X ⟶ yoneda.obj (baseTerminal B (Spec (.of A)) hS))
    (hf : IsIntegralModification B (Spec (.of A)) hS hX
      (isAlgebraicSpace_yoneda B (Spec (.of A)) hS _)
      (isIntegralSpace_yoneda_baseTerminal A B hS) f) :
    dimension B (Spec (.of A)) hS
        (fieldFibre B (Spec (.of A)) hS f (residueFieldPoint A B hS))
        (isAlgebraicSpace_fieldFibre hX (isAlgebraicSpace_yoneda B (Spec (.of A)) hS _) f
          (residueFieldPoint A B hS)) + 1
      ≤ ringKrullDim A

AlgebraicGeometry.Space.dimension_fieldFibre_add_one_le_ringKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpecialFibreDimension.lean, line 211. The attribute's comment: “case (4), X decent”.

Stacks 0AYJ, case (4). Let (A, 𝔪, κ) be a Noetherian local domain of dimension at least one and let f : X → Spec A be a morphism of algebraic spaces which is locally of finite type, with X decent, such that the points of |X| lying over the generic point of Spec A are exactly the generic points of the irreducible components of |X|. Then the special fibre X_κ has dimension at most dim(A) - 1.

The bound is proved one point of X_κ at a time: base change identifies the dimension of X_κ at a point with the relative dimension of f over the closed point there, an affine étale chart turns that into the dimension of the fibre of an affine scheme of finite type over Spec A, and the generic hypothesis transported to the chart is the hypothesis of the commutative-algebra bound on the special fibre.

theorem dimension_fieldFibre_add_one_le_ringKrullDim [IsDomain A] [IsNoetherianRing A]
    (hdim : 1 ≤ ringKrullDim A)
    {X : (BigFppfOver B (Spec (.of A)) hA)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of A)) hA X)
    (f : X ⟶ yoneda.obj (baseTerminal B (Spec (.of A)) hA))
    (hf : IsLocallyOfFiniteType B (Spec (.of A)) hA f)
    (hdec : IsDecentSpace B (Spec (.of A)) hA X)
    (hgen : ∀ x : points B (Spec (.of A)) hA X,
      x ∈ genericPoints (points B (Spec (.of A)) hA X) ↔
        pointsToScheme B (Spec (.of A)) hA (baseTerminal B (Spec (.of A)) hA)
            (pointsMap B (Spec (.of A)) hA X f x) = genericPoint (Spec (.of A)))
    (hfib : IsAlgebraicSpace B (Spec (.of A)) hA
      (fieldFibre B (Spec (.of A)) hA f (residueFieldPoint A B hA))) :
    dimension B (Spec (.of A)) hA
        (fieldFibre B (Spec (.of A)) hA f (residueFieldPoint A B hA)) hfib + 1
      ≤ ringKrullDim A

AlgebraicGeometry.Space.dimension_fieldFibre_add_one_le_ringKrullDim_of_isIntegralSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpecialFibreDimension.lean, line 324. The attribute's comment: “case (3), X integral”.

Stacks 0AYJ, case (3). Let (A, 𝔪, κ) be a Noetherian local domain of dimension at least one and let f : X → Spec A be a morphism of algebraic spaces which is locally of finite type, with X integral, such that exactly one point of |X| lies over the generic point of Spec A. Then the special fibre X_κ has dimension at most dim(A) - 1.

This is case (4): an integral algebraic space is decent and its space of points is irreducible, so its generic points are the points whose closure is everything, and there is one of them because the points of codimension zero are dense. The image of such a point both specialises to and generalises the generic point of Spec A, hence equals it, and uniqueness identifies it with the point lying over the generic point. Quasi-separatedness, which the source also assumes, is not needed for this reduction.

theorem dimension_fieldFibre_add_one_le_ringKrullDim_of_isIntegralSpace
    [IsDomain A] [IsNoetherianRing A] (hdim : 1 ≤ ringKrullDim A)
    {X : (BigFppfOver B (Spec (.of A)) hA)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of A)) hA X)
    (f : X ⟶ yoneda.obj (baseTerminal B (Spec (.of A)) hA))
    (hf : IsLocallyOfFiniteType B (Spec (.of A)) hA f)
    (hint : IsIntegralSpace B (Spec (.of A)) hA X)
    (hone : ∃! x : points B (Spec (.of A)) hA X,
      pointsToScheme B (Spec (.of A)) hA (baseTerminal B (Spec (.of A)) hA)
        (pointsMap B (Spec (.of A)) hA X f x) = genericPoint (Spec (.of A)))
    (hfib : IsAlgebraicSpace B (Spec (.of A)) hA
      (fieldFibre B (Spec (.of A)) hA f (residueFieldPoint A B hA))) :
    dimension B (Spec (.of A)) hA
        (fieldFibre B (Spec (.of A)) hA f (residueFieldPoint A B hA)) hfib + 1
      ≤ ringKrullDim A

AlgebraicGeometry.Space.dimension_fieldFibre_add_one_le_ringKrullDim', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpecialFibreDimensionExtensions.lean, line 63. The attribute's comment: “case (4), X decent, at the source's hypotheses”.

Stacks 0AYJ, case (4), with the algebraicity of the special fibre supplied rather than assumed: it is the base change of f along the residue-field point, so AlgebraicGeometry.Space.isAlgebraicSpace_fieldFibre_residueFieldPoint provides it and AlgebraicGeometry.Space.dimension_fieldFibre_add_one_le_ringKrullDim applies.

theorem dimension_fieldFibre_add_one_le_ringKrullDim' [IsDomain A] [IsNoetherianRing A]
    (hdim : 1 ≤ ringKrullDim A)
    {X : (BigFppfOver B (Spec (.of A)) hA)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of A)) hA X)
    (f : X ⟶ yoneda.obj (baseTerminal B (Spec (.of A)) hA))
    (hf : IsLocallyOfFiniteType B (Spec (.of A)) hA f)
    (hdec : IsDecentSpace B (Spec (.of A)) hA X)
    (hgen : ∀ x : points B (Spec (.of A)) hA X,
      x ∈ genericPoints (points B (Spec (.of A)) hA X) ↔
        pointsToScheme B (Spec (.of A)) hA (baseTerminal B (Spec (.of A)) hA)
            (pointsMap B (Spec (.of A)) hA X f x) = genericPoint (Spec (.of A))) :
    dimension B (Spec (.of A)) hA
        (fieldFibre B (Spec (.of A)) hA f (residueFieldPoint A B hA))
        (isAlgebraicSpace_fieldFibre_residueFieldPoint A B hA hX f) + 1
      ≤ ringKrullDim A

AlgebraicGeometry.Space.dimension_fieldFibre_add_one_le_ringKrullDim_of_isIntegralSpace', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpecialFibreDimensionExtensions.lean, line 86. The attribute's comment: “case (3), X integral, at the source's hypotheses”.

Stacks 0AYJ, case (3), with the algebraicity of the special fibre supplied rather than assumed, by AlgebraicGeometry.Space.isAlgebraicSpace_fieldFibre_residueFieldPoint; this is AlgebraicGeometry.Space.dimension_fieldFibre_add_one_le_ringKrullDim_of_isIntegralSpace with that witness.

theorem dimension_fieldFibre_add_one_le_ringKrullDim_of_isIntegralSpace'
    [IsDomain A] [IsNoetherianRing A] (hdim : 1 ≤ ringKrullDim A)
    {X : (BigFppfOver B (Spec (.of A)) hA)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of A)) hA X)
    (f : X ⟶ yoneda.obj (baseTerminal B (Spec (.of A)) hA))
    (hf : IsLocallyOfFiniteType B (Spec (.of A)) hA f)
    (hint : IsIntegralSpace B (Spec (.of A)) hA X)
    (hone : ∃! x : points B (Spec (.of A)) hA X,
      pointsToScheme B (Spec (.of A)) hA (baseTerminal B (Spec (.of A)) hA)
        (pointsMap B (Spec (.of A)) hA X f x) = genericPoint (Spec (.of A))) :
    dimension B (Spec (.of A)) hA
        (fieldFibre B (Spec (.of A)) hA f (residueFieldPoint A B hA))
        (isAlgebraicSpace_fieldFibre_residueFieldPoint A B hA hX f) + 1
      ≤ ringKrullDim A

AlgebraicGeometry.Space.dimension_fieldFibre_add_one_le_ringKrullDim_of_isAlteration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpecialFibreDimensionExtensions.lean, line 115. The attribute's comment: “case (2), f an alteration”.

Stacks 0AYJ, case (2). Let (A, 𝔪, κ) be a Noetherian local domain of dimension at least one and let f : X → Spec A be an alteration of algebraic spaces, Stacks 0ADA. Then the special fibre X_κ has dimension at most dim(A) - 1.

This is case (3). An alteration is proper, hence locally of finite type, and its source is integral, so all that is needed is that exactly one point of |X| lies over the generic point of Spec A. Being an alteration, f is quasi-finite at the generic point of |X| by Stacks 0ADB, and condition (5) of Stacks 0AD5 turns that into the statement that the generic point is the only point of |X| above the generic point of |Spec A|; the comparison map from the points of the representable base to Spec A is injective, so that is uniqueness of the point above genericPoint (Spec A).

theorem dimension_fieldFibre_add_one_le_ringKrullDim_of_isAlteration
    [IsDomain A] [IsNoetherianRing A] (hdim : 1 ≤ ringKrullDim A)
    {X : (BigFppfOver B (Spec (.of A)) hA)ᵒᵖ ⥤ Type u}
    (f : X ⟶ yoneda.obj (baseTerminal B (Spec (.of A)) hA))
    (halt : IsAlteration B (Spec (.of A)) hA f) :
    dimension B (Spec (.of A)) hA
        (fieldFibre B (Spec (.of A)) hA f (residueFieldPoint A B hA))
        (isAlgebraicSpace_fieldFibre_residueFieldPoint A B hA
          (halt.isAlgebraicSpace_source B (Spec (.of A)) hA) f) + 1
      ≤ ringKrullDim A

AlgebraicGeometry.Space.dimension_fieldFibre_add_one_le_ringKrullDim_of_alteration_or_generic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpecialFibreDimensionExtensions.lean, line 191.

Stacks 0AYJ. Let (A, 𝔪, κ) be a Noetherian local domain of dimension at least one and let f : X → Spec A be a morphism of algebraic spaces satisfying at least one of: (1) f is a modification, Stacks 0AD8; (2) f is an alteration, Stacks 0ADA; (3) f is locally of finite type, X is integral, and exactly one point of |X| maps to the generic point of Spec A; (4) f is locally of finite type, X is decent, and the points of |X| mapping to the generic point of Spec A are the generic points of the irreducible components of |X|. Then the special fibre X_κ has dimension at most dim(A) - 1.

The source's hypothesis is this disjunction, and the four clauses are four theorems (clause (1) is dimension_fieldFibre_add_one_le_ringKrullDim_of_isIntegralModification, the others are above), so the proof is the case distinction. Clause (1) needs no decency witness: AlgebraicGeometry.Space.IsIntegralModification derives it from the integrality it asserts. The source also assumes f quasi-separated in clause (3); that is omitted, because AlgebraicGeometry.Space.dimension_fieldFibre_add_one_le_ringKrullDim_of_isIntegralSpace does not need it.

theorem dimension_fieldFibre_add_one_le_ringKrullDim_of_alteration_or_generic
    [IsDomain A] [IsNoetherianRing A] (hdim : 1 ≤ ringKrullDim A)
    {X : (BigFppfOver B (Spec (.of A)) hA)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of A)) hA X)
    (f : X ⟶ yoneda.obj (baseTerminal B (Spec (.of A)) hA))
    (hf :
      IsIntegralModification B (Spec (.of A)) hA hX
        (isAlgebraicSpace_yoneda B (Spec (.of A)) hA _)
        (isIntegralSpace_yoneda_baseTerminal A B hA) f ∨
      IsAlteration B (Spec (.of A)) hA f ∨
      (IsLocallyOfFiniteType B (Spec (.of A)) hA f ∧
        IsIntegralSpace B (Spec (.of A)) hA X ∧
        ∃! x : points B (Spec (.of A)) hA X,
          pointsToScheme B (Spec (.of A)) hA (baseTerminal B (Spec (.of A)) hA)
            (pointsMap B (Spec (.of A)) hA X f x) = genericPoint (Spec (.of A))) ∨
      (IsLocallyOfFiniteType B (Spec (.of A)) hA f ∧
        IsDecentSpace B (Spec (.of A)) hA X ∧
        ∀ x : points B (Spec (.of A)) hA X,
          x ∈ genericPoints (points B (Spec (.of A)) hA X) ↔
            pointsToScheme B (Spec (.of A)) hA (baseTerminal B (Spec (.of A)) hA)
              (pointsMap B (Spec (.of A)) hA X f x) = genericPoint (Spec (.of A)))) :
    dimension B (Spec (.of A)) hA
        (fieldFibre B (Spec (.of A)) hA f (residueFieldPoint A B hA))
        (isAlgebraicSpace_fieldFibre_residueFieldPoint A B hA hX f) + 1
      ≤ ringKrullDim A

Tag 0AGN, a lemma

Tag 0AGN in the Stacks Project.

AlgebraicGeometry.Space.exists_iso_isProjective_of_isIntegralModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationCompleteLocalProjective.lean, line 176.

Let (A, 𝔪, κ) be a complete Noetherian local domain of dimension 2. Every modification f : X ⟶ Spec A (Stacks 0AD8) is projective over A: X is a scheme Y, in the sense that there are a projective morphism of schemes fY : Y ⟶ Spec A and an isomorphism of X with the algebraic space Y over Spec A.

theorem exists_iso_isProjective_of_isIntegralModification
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [IsDomain A]
    [IsAdicComplete (maximalIdeal A) A] (hdim : ringKrullDim A = 2)
    (B : BigFppfSite.{u}) (hS : B.Contains (Spec (.of A)))
    {X : (BigFppfOver B (Spec (.of A)) hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of A)) hS X)
    (f : X ⟶ yoneda.obj (baseObject A B hS))
    (hf : IsIntegralModification B (Spec (.of A)) hS hX
      (isAlgebraicSpace_yoneda B (Spec (.of A)) hS _)
      (isIntegralSpace_yoneda_baseTerminal A B hS) f) :
    ∃ (Y : Scheme.{u}) (hY : B.Contains Y) (fY : Y ⟶ Spec (.of A)),
      IsProjective fY ∧ IsProjectiveMorphism fY ∧
      ∃ e : X ≅ yoneda.obj (siteObject B (Spec (.of A)) hS hY fY),
        e.hom ≫ yoneda.map (siteObjectToBase A B hS hY fY) = f

Sources

Section89.3 Strategy #

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

Tag 0BHA, an equation

Tag 0BHA in the Stacks Project.

AlgebraicGeometry.Space.ClosedPointNeighborhoods.modificationsAwayFromPoints, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationsAtClosedPoints.lean, line 274. The attribute's comment: “the source category of the functor”.

Stacks 0BHA. The category C_{X, {x₁, …, xₙ}} of algebraic spaces over X which are unchanged over X ∖ {x₁, …, xₙ}.

abbrev modificationsAwayFromPoints

AlgebraicGeometry.Space.ClosedPointNeighborhoods.modificationsAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationsAtClosedPoints.lean, line 279. The attribute's comment: “the factors of the target category of the functor”.

Stacks 0BHA. The category C_{Uᵢ, uᵢ} of algebraic spaces over the ith neighborhood which are unchanged over Uᵢ ∖ {uᵢ}.

abbrev modificationsAt (i : Fin n)

AlgebraicGeometry.Space.ClosedPointNeighborhoods.restrictionFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationsAtClosedPoints.lean, line 300. The attribute's comment: “the functor given by base change”.

Stacks 0BHA. The functor F : C_{X, {x₁, …, xₙ}} ⟶ C_{U₁, u₁} × … × C_{Uₙ, uₙ} given by base change along the chosen elementary étale neighborhoods.

def restrictionFunctor :
    D.modificationsAwayFromPoints ⥤ ∀ i : Fin n, D.modificationsAt i

AlgebraicGeometry.Space.ClosedPointNeighborhoods.restrictionFunctorCompιIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationsAtClosedPoints.lean, line 306. The attribute's comment: “base change computes the functor”.

Stacks 0BHA. The ith component of F is base change along Uᵢ ⟶ X.

def restrictionFunctorCompιIso (i : Fin n) :
    D.restrictionFunctor ⋙ Pi.eval _ i ⋙
        ObjectProperty.ι (IsModification B S hS (D.openAwayFromPoint i)) ≅
      ObjectProperty.ι (IsModification B S hS D.openAwayFromPoints) ⋙
        Over.pullback (D.toSpaceHom i).hom

Tag 0BHB, a lemma

Tag 0BHB in the Stacks Project.

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

Stacks 0BHB. The functor F of Stacks 0BHA, base change of the modifications of X away from the chosen closed points to the chosen elementary étale neighborhoods, is an equivalence of categories.

theorem isEquivalence_restrictionFunctor : D.restrictionFunctor.IsEquivalence

AlgebraicGeometry.Space.ClosedPointNeighborhoods.essSurj_restrictionFunctor_of_essSurj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationsAtClosedPointsSinglePoint.lean, line 152. The attribute's comment: “essential surjectivity of the functor, granted the case n = 1 of Stacks 0BGY”.

Stacks 0BHB, the essential surjectivity of F, granted the case n = 1. If the base-change functor of Stacks 0BGY along Uᵢ ⟶ X, taken outside X ∖ {xᵢ}, is essentially surjective for every i, then the functor F of Stacks 0BHA is essentially surjective.

theorem essSurj_restrictionFunctor_of_essSurj
    (hES : ∀ i : Fin n,
      (baseChangeFunctor B S hS (D.toSpaceHom i) (D.openAwayFromSinglePoint i)).1.EssSurj) :
    D.restrictionFunctor.EssSurj

Tag 0BHC, a lemma

Tag 0BHC in the Stacks Project.

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

Stacks 0BHC, quasi-compactness. A modification of X away from {x₁, …, xₙ} is quasi-compact exactly when each of its restrictions under the functor F of Stacks 0BHA is.

theorem isQuasiCompact_iff_forall_restrictionComponent :
    IsQuasiCompact B S hS M.obj.hom ↔
      ∀ i, IsQuasiCompact B S hS ((D.restrictionComponent i).obj M).obj.hom

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

Stacks 0BHC, quasi-separatedness. A modification of X away from {x₁, …, xₙ} is quasi-separated exactly when each of its restrictions under the functor F of Stacks 0BHA is.

theorem isQuasiSeparated_iff_forall_restrictionComponent :
    IsQuasiSeparated B S hS M.obj.hom ↔
      ∀ i, IsQuasiSeparated B S hS ((D.restrictionComponent i).obj M).obj.hom

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

Stacks 0BHC, separatedness. A modification of X away from {x₁, …, xₙ} is separated exactly when each of its restrictions under the functor F of Stacks 0BHA is.

theorem isSeparated_iff_forall_restrictionComponent :
    IsSeparated B S hS M.obj.hom ↔
      ∀ i, IsSeparated B S hS ((D.restrictionComponent i).obj M).obj.hom

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

Stacks 0BHC, local finite presentation. A modification of X away from {x₁, …, xₙ} is locally of finite presentation exactly when each of its restrictions under the functor F of Stacks 0BHA is.

theorem isLocallyOfFinitePresentation_iff_forall_restrictionComponent :
    IsLocallyOfFinitePresentation B S hS M.obj.hom ↔
      ∀ i, IsLocallyOfFinitePresentation B S hS
        ((D.restrictionComponent i).obj M).obj.hom

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

Stacks 0BHC, local finite type. A modification of X away from {x₁, …, xₙ} is locally of finite type exactly when each of its restrictions under the functor F of Stacks 0BHA is.

theorem isLocallyOfFiniteType_iff_forall_restrictionComponent :
    IsLocallyOfFiniteType B S hS M.obj.hom ↔
      ∀ i, IsLocallyOfFiniteType B S hS ((D.restrictionComponent i).obj M).obj.hom

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

Stacks 0BHC, finite type. A modification of X away from {x₁, …, xₙ} is of finite type exactly when each of its restrictions under the functor F of Stacks 0BHA is.

theorem isFiniteType_iff_forall_restrictionComponent :
    IsFiniteType B S hS M.obj.hom ↔
      ∀ i, IsFiniteType B S hS ((D.restrictionComponent i).obj M).obj.hom

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

Stacks 0BHC, finite presentation. A modification of X away from {x₁, …, xₙ} is of finite presentation exactly when each of its restrictions under the functor F of Stacks 0BHA is.

theorem isFinitePresentation_iff_forall_restrictionComponent :
    IsFinitePresentation B S hS M.obj.hom ↔
      ∀ i, IsFinitePresentation B S hS ((D.restrictionComponent i).obj M).obj.hom

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

Stacks 0BHC, properness. A modification of X away from {x₁, …, xₙ} is proper exactly when each of its restrictions under the functor F of Stacks 0BHA is.

theorem isProper_iff_forall_restrictionComponent :
    IsProper B S hS M.obj.hom ↔
      ∀ i, IsProper B S hS ((D.restrictionComponent i).obj M).obj.hom

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

Stacks 0BHC, integrality. A modification of X away from {x₁, …, xₙ} is integral exactly when each of its restrictions under the functor F of Stacks 0BHA is.

theorem isIntegralHom_iff_forall_restrictionComponent :
    IsIntegralHom B S hS M.obj.hom ↔
      ∀ i, IsIntegralHom B S hS ((D.restrictionComponent i).obj M).obj.hom

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

Stacks 0BHC, finiteness. A modification of X away from {x₁, …, xₙ} is finite exactly when each of its restrictions under the functor F of Stacks 0BHA is.

theorem isFinite_iff_forall_restrictionComponent :
    IsFinite B S hS M.obj.hom ↔
      ∀ i, IsFinite B S hS ((D.restrictionComponent i).obj M).obj.hom

Tag 0BHD, a lemma

Tag 0BHD in the Stacks Project.

AlgebraicGeometry.Space.ClosedPointNeighborhoods.fibreAtPointIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModificationsAtClosedPointsProperties.lean, line 222. The attribute's comment: “the fibres agree”.

Stacks 0BHD. If f : Y ⟶ X corresponds to gᵢ : Yᵢ ⟶ Uᵢ under the functor F of Stacks 0BHA, then Y_{xᵢ} ≅ (Yᵢ)_{uᵢ} as algebraic spaces: both are the fibre product of f with the monomorphism Spec κ(uᵢ) ⟶ X.

def fibreAtPointIso (M : D.modificationsAwayFromPoints) (i : Fin n) :
    fibreAtPoint M i ≅ fibreAtNeighborhoodPoint M i

Sources

LeanAlgebraicGeometry.Space.ClosedPointNeighborhoods.modificationsAwayFromPoints · AlgebraicGeometry.Space.ClosedPointNeighborhoods.modificationsAt · AlgebraicGeometry.Space.ClosedPointNeighborhoods.restrictionFunctor · AlgebraicGeometry.Space.ClosedPointNeighborhoods.restrictionFunctorCompιIso · AlgebraicGeometry.Space.ClosedPointNeighborhoods.isEquivalence_restrictionFunctor · AlgebraicGeometry.Space.ClosedPointNeighborhoods.essSurj_restrictionFunctor_of_essSurj · AlgebraicGeometry.Space.ClosedPointNeighborhoods.isQuasiCompact_iff_forall_restrictionComponent · AlgebraicGeometry.Space.ClosedPointNeighborhoods.isQuasiSeparated_iff_forall_restrictionComponent

Section89.4 Dominating by quadratic transformations #

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

Tag 0BHE, a definition

Tag 0BHE in the Stacks Project.

AlgebraicGeometry.Space.IsBlowupAtClosedPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupsAtClosedPoints.lean, line 187.

Stacks 0BHE. A morphism f : Y ⟶ X of algebraic spaces is the blowing up of X at the closed point z when there is a blowing up of X in the reduced closed subspace supported on {z} to which f is isomorphic over X.

Being the blowing up in a closed subspace is the universal property of Stacks 085U, which is AlgebraicGeometry.Space.IsBlowupAlong; it already determines the morphism up to isomorphism over X, so asking for the isomorphism here changes nothing and makes AlgebraicGeometry.Space.IsBlowupAtClosedPoint.comp_iso available. The centre is AlgebraicGeometry.Space.closedPointSubspace, which is the i(Spec(k)) of the source by AlgebraicGeometry.Space.eq_closedPointSubspace.

def IsBlowupAtClosedPoint {X Y : AlgebraicSpaces B S hS} (z : points B S hS X.obj)
    (hz : IsClosed ({z} : Set (points B S hS X.obj))) (f : Y ⟶ X) : Prop

Tag 0BHF, a lemma

Tag 0BHF in the Stacks Project.

AlgebraicGeometry.Space.BlowupFactorization, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupsAtClosedPoints.lean, line 397. The attribute's comment: “the condition asserted on both sides of the equivalence: a factorization of the given morphism as a finite sequence of blowings up at closed points lying over the given set of points. The equivalence itself is AlgebraicGeometry.Space.ClosedPointNeighborhoods.nonempty_globalBlowupFactorization_iff.”.

A factorization of f : Y ⟶ X as a sequence of blowings up at closed points lying over the set of points T ⊆ |X|: a tower

Zₘ ⟶ Zₘ₋₁ ⟶ … ⟶ Z₁ ⟶ Z₀ = X

of blowings up at closed points, all of whose centres lie over T, together with an identification of Y with its top Zₘ under which f is the composite Zₘ ⟶ X.

This is the condition on both sides of Stacks 0BHF, taken there with T = {x₁, …, xₙ} for the morphism to X and with T = {uᵢ} for the morphism to the ith étale neighborhood.

structure BlowupFactorization (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (T : Set (points B S hS X.obj)) (f : Y ⟶ X)

AlgebraicGeometry.Space.ClosedPointNeighborhoods.GlobalBlowupFactorization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupsAtClosedPoints.lean, line 491. The attribute's comment: “the condition on the morphism to X: it factors as a finite sequence of blowings up at closed points lying over x₁, …, xₙ”.

Stacks 0BHF, the condition on the morphism to X: f : Y ⟶ X factors as

Y = Zₘ ⟶ Zₘ₋₁ ⟶ … ⟶ Z₁ ⟶ Z₀ = X

where each Z_{j+1} ⟶ Z_j is the blowing up of Z_j at a closed point z_j lying over {x₁, …, xₙ}.

abbrev GlobalBlowupFactorization {Y : AlgebraicSpaces B S hS} (f : Y ⟶ D.space)

AlgebraicGeometry.Space.ClosedPointNeighborhoods.LocalBlowupFactorization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupsAtClosedPoints.lean, line 503. The attribute's comment: “the condition on the morphism to the i-th étale neighborhood: it factors as a finite sequence of blowings up at closed points lying over uᵢ”.

Stacks 0BHF, the condition on the morphism to the ith étale neighborhood: gᵢ : Yᵢ ⟶ Uᵢ factors as

Yᵢ = Z_{i, mᵢ} ⟶ … ⟶ Z_{i, 1} ⟶ Z_{i, 0} = Uᵢ

where each Z_{i, j+1} ⟶ Z_{i, j} is the blowing up of Z_{i, j} at a closed point lying over uᵢ.

abbrev LocalBlowupFactorization (i : Fin n) {Y : AlgebraicSpaces B S hS}
    (g : Y ⟶ D.neighborhoodSpace i)

AlgebraicGeometry.Space.ClosedPointNeighborhoods.nonempty_localBlowupFactorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupTowerEtaleRestriction.lean, line 474. The attribute's comment: “the only-if direction: a factorization of f as a sequence of blowings up at closed points lying over x₁, …, xₙ gives, for each i, a factorization of its base change gᵢ as a sequence of blowings up at closed points lying over uᵢ. The if direction is AlgebraicGeometry.Space.ClosedPointNeighborhoods.nonempty_globalBlowupFactorization_of_isPullback and the equivalence itself is AlgebraicGeometry.Space.ClosedPointNeighborhoods.nonempty_globalBlowupFactorization_iff.”.

Stacks 0BHF, the "only if" direction. Let X, xᵢ, Uᵢ ⟶ X, uᵢ be as in Stacks 0BH9 and let f : Y ⟶ X be a morphism of algebraic spaces with base change gᵢ : Yᵢ ⟶ Uᵢ along Uᵢ ⟶ X. If f factors as a finite sequence of blowings up at closed points lying over {x₁, …, xₙ}, then gᵢ factors as a finite sequence of blowings up at closed points lying over uᵢ.

The sequence over Uᵢ is the base change of the given one, which is AlgebraicGeometry.Space.ClosedPointNeighborhoods.exists_blowupTower_of_isPullback. No hypothesis on f beyond the cartesian square is used; in particular f need not be an isomorphism over X ∖ {x₁, …, xₙ}, so the statement is stronger than the source's, which fixes f in C_{X, {x₁, …, xₙ}}.

theorem nonempty_localBlowupFactorization {i : Fin n} {Y Y' : AlgebraicSpaces B S hS}
    {f : Y ⟶ D.space} {a : Y' ⟶ Y} {g : Y' ⟶ D.neighborhoodSpace i}
    (sq : IsPullback a g f (D.toSpaceHom i)) (F : D.GlobalBlowupFactorization f) :
    Nonempty (D.LocalBlowupFactorization i g)

AlgebraicGeometry.Space.ClosedPointNeighborhoods.nonempty_localBlowupFactorization_restrictionComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupTowerEtaleRestriction.lean, line 501. The attribute's comment: “the only-if direction at the functor F: a factorization of f as a sequence of blowings up at closed points lying over x₁, …, xₙ gives, for each i, a factorization of gᵢ = F(f)ᵢ as a sequence of blowings up at closed points lying over uᵢ. The if direction at F is nonempty_globalBlowupFactorization_restrictionComponent and the equivalence itself is AlgebraicGeometry.Space.ClosedPointNeighborhoods.nonempty_globalBlowupFactorization_iff.”.

Stacks 0BHF, the "only if" direction, for the functor F of Stacks 0BHA. Let X, xᵢ, Uᵢ ⟶ X, uᵢ be as in Stacks 0BH9 and let f : Y ⟶ X be an object of C_{X, {x₁, …, xₙ}} corresponding to gᵢ : Yᵢ ⟶ Uᵢ under F. If f factors as a finite sequence of blowings up at closed points lying over {x₁, …, xₙ}, then for every i the morphism gᵢ factors as a finite sequence of blowings up at closed points lying over uᵢ.

This is AlgebraicGeometry.Space.ClosedPointNeighborhoods.nonempty_localBlowupFactorization at the cartesian square of AlgebraicGeometry.Space.ClosedPointNeighborhoods.isPullback_restrictionComponent_obj, which is what "corresponds under F" means.

theorem nonempty_localBlowupFactorization_restrictionComponent
    (M : D.modificationsAwayFromPoints) (i : Fin n)
    (F : D.GlobalBlowupFactorization (ObjectProperty.homMk M.obj.hom :
      (⟨M.obj.left, M.property.1⟩ : AlgebraicSpaces B S hS) ⟶ D.space)) :
    Nonempty (D.LocalBlowupFactorization i (ObjectProperty.homMk
      ((D.restrictionComponent i).obj M).obj.hom :
      (⟨((D.restrictionComponent i).obj M).obj.left,
          ((D.restrictionComponent i).obj M).property.1⟩ : AlgebraicSpaces B S hS) ⟶
        D.neighborhoodSpace i))

AlgebraicGeometry.Space.ClosedPointNeighborhoods.nonempty_globalBlowupFactorization_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupTowerGlobalConverse.lean, line 487.

Stacks 0BHF. Let X, xᵢ, Uᵢ ⟶ X, uᵢ be as in Stacks 0BH9 and let f : Y ⟶ X be an object of the category C_{X, {x₁, …, xₙ}} of Stacks 0BHA. Then f factors as a finite sequence of blowings up at closed points lying over {x₁, …, xₙ} if and only if, for every i, the morphism gᵢ = F(f)ᵢ factors as a finite sequence of blowings up at closed points lying over uᵢ.

The "only if" direction is nonempty_localBlowupFactorization_restrictionComponent and the "if" direction is nonempty_globalBlowupFactorization_restrictionComponent.

theorem nonempty_globalBlowupFactorization_iff (M : D.modificationsAwayFromPoints) :
    Nonempty (D.GlobalBlowupFactorization (ObjectProperty.homMk M.obj.hom :
        (⟨M.obj.left, M.property.1⟩ : AlgebraicSpaces B S hS) ⟶ D.space)) ↔
      ∀ i, Nonempty (D.LocalBlowupFactorization i (ObjectProperty.homMk
        ((D.restrictionComponent i).obj M).obj.hom :
        (⟨((D.restrictionComponent i).obj M).obj.left,
            ((D.restrictionComponent i).obj M).property.1⟩ : AlgebraicSpaces B S hS) ⟶
          D.neighborhoodSpace i))

Tag 0BHG, a lemma

Tag 0BHG in the Stacks Project.

AlgebraicGeometry.Space.exists_blowupFactorization_isPullbackDefined, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PrincipalizationAtClosedPoints.lean, line 159. The attribute's comment: “the induction producing the sequence of blowings up, granted the existence of the blowing up of an algebraic space at a closed point (0BHE, hence 084A/084B/085Q), the algebraic-space analogue of 0809, and the local splitting of 0AGT”.

Stacks 0BHG. Let S be a scheme, let X be a Noetherian algebraic space over S and let T ⊆ |X| be a finite set of closed points x such that X is regular at x and the local ring of X at x has dimension 2. Let ℐ ⊆ 𝒪_X be a quasi-coherent sheaf of ideals, given by the closed subspace Z ⊆ X it cuts out, such that 𝒪_X/ℐ is supported on T, that is, |Z| ⊆ T. Then there is a sequence

X_m ⟶ X_{m-1} ⟶ … ⟶ X_1 ⟶ X_0 = X

where X_{j+1} ⟶ X_j is the blowing up of X_j at a closed point x_j lying above a point of T, such that ℐ𝒪_{X_m} is an invertible ideal sheaf — that is, such that the inverse image of Z along the composite X_m ⟶ X is an effective Cartier divisor.

Along the sequence produced, every effective Cartier divisor on X also has a defined pullback; that is the form in which the induction uses its own output and it is recorded in the conclusion.

Three inputs are granted, since the library has them for schemes only: the existence of the blowing up of an algebraic space at a closed point (Stacks 0BHE, whose construction needs the relative Proj of Stacks 084A and 084B), the algebraic-space analogue of Stacks 0809, and the local splitting of Stacks 0AGT with respect to a colength function given as a parameter — the hypothesis which the scheme case, Stacks 0AHH, carries as well. See the module documentation.

theorem exists_blowupFactorization_isPullbackDefined
    (colength : ∀ Y : AlgebraicSpaces B S hS,
      ClosedSubspaces B S hS Y.1 → Set (points B S hS Y.1) → ℕ∞)
    (blowupExists : ∀ (Y : AlgebraicSpaces B S hS) (y : points B S hS Y.1)
      (hy : IsClosed ({y} : Set (points B S hS Y.1))),
      ∃ (Y' : AlgebraicSpaces B S hS) (b : Y' ⟶ Y), IsBlowupAtClosedPoint B S hS y hy b)
    (pullbackOfEffectiveCartier : ∀ (Y Y' : AlgebraicSpaces B S hS) (y : points B S hS Y.1)
      (hy : IsClosed ({y} : Set (points B S hS Y.1))) (b : Y' ⟶ Y),
      IsBlowupAtClosedPoint B S hS y hy b →
      ∀ D : ClosedSubspaces B S hS Y.1, IsEffectiveCartierDivisor B S hS Y D →
        IsPullbackDefined B S hS b D)
    (splitting : ∀ (Y : AlgebraicSpaces B S hS) (T : Set (points B S hS Y.1)), T.Finite →
      (∀ y ∈ T, IsClosed ({y} : Set (points B S hS Y.1))) →
      (∀ y ∈ T, IsRegularAt B S hS Y.1 y) →
      (∀ y ∈ T, localRingDimension B S hS y = 2) →
      ∀ Z : ClosedSubspaces B S hS Y.1, subspacePointSet B S hS Y.1 Z.1 ⊆ T →
      ∀ y ∈ subspacePointSet B S hS Y.1 Z.1,
      ∀ (hy : IsClosed ({y} : Set (points B S hS Y.1))) (Y' : AlgebraicSpaces B S hS)
        (b : Y' ⟶ Y), IsBlowupAtClosedPoint B S hS y hy b →
        ∃ (E Z' : ClosedSubspaces B S hS Y'.1) (T' : Set (points B S hS Y'.1)),
          preimageClosedSubspace b Z = sumClosedSubspaces B S hS Y' E Z' ∧
          IsEffectiveCartierDivisor B S hS Y' E ∧
          T'.Finite ∧
          (∀ z ∈ T', IsClosed ({z} : Set (points B S hS Y'.1))) ∧
          (∀ z ∈ T', IsRegularAt B S hS Y'.1 z) ∧
          (∀ z ∈ T', localRingDimension B S hS z = 2) ∧
          (∀ z ∈ T', pointsMap B S hS Y'.1 b.hom z ∈ T) ∧
          subspacePointSet B S hS Y'.1 Z'.1 ⊆ T' ∧
          colength Y' Z' T' < colength Y Z T)
    (hterm : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS) (_hX : IsNoetherian B S hS hterm X.1)
    (T : Set (points B S hS X.1)) (hTfinite : T.Finite)
    (hTclosed : ∀ x ∈ T, IsClosed ({x} : Set (points B S hS X.1)))
    (hTregular : ∀ x ∈ T, IsRegularAt B S hS X.1 x)
    (hTdim : ∀ x ∈ T, localRingDimension B S hS x = 2)
    (Z : ClosedSubspaces B S hS X.1)
    (hZsupport : subspacePointSet B S hS X.1 Z.1 ⊆ T) :
    ∃ (Y : AlgebraicSpaces B S hS) (f : Y ⟶ X),
      Nonempty (BlowupFactorization B S hS T f) ∧
        IsPullbackDefined B S hS f Z ∧
        ∀ D : ClosedSubspaces B S hS X.1, IsEffectiveCartierDivisor B S hS X D →
          IsPullbackDefined B S hS f D

AlgebraicGeometry.Space.exists_blowupFactorization_isPullbackDefined_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PrincipalizationAtClosedPointsUnconditional.lean, line 266.

Let S be a scheme, let X be a Noetherian algebraic space over S and let T ⊆ |X| be a finite set of closed points x such that X is regular at x and the local ring of X at x has dimension 2. Let ℐ ⊆ 𝒪_X be a quasi-coherent sheaf of ideals, given by the closed subspace Z ⊆ X it cuts out, such that 𝒪_X/ℐ is supported on T, that is, |Z| ⊆ T. Then there is a sequence

X_m ⟶ X_{m-1} ⟶ … ⟶ X_1 ⟶ X_0 = X

where X_{j+1} ⟶ X_j is the blowing up of X_j at a closed point x_j lying above a point of T, such that ℐ𝒪_{X_m} is an invertible ideal sheaf — that is, such that the inverse image of Z along the composite X_m ⟶ X is an effective Cartier divisor.

theorem exists_blowupFactorization_isPullbackDefined_of_isNoetherian
    (hterm : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS) (hX : IsNoetherian B S hS hterm X.1)
    (T : Set (points B S hS X.1)) (hTfinite : T.Finite)
    (hTclosed : ∀ x ∈ T, IsClosed ({x} : Set (points B S hS X.1)))
    (hTregular : ∀ x ∈ T, IsRegularAt B S hS X.1 x)
    (hTdim : ∀ x ∈ T, localRingDimension B S hS x = 2)
    (Z : ClosedSubspaces B S hS X.1)
    (hZsupport : subspacePointSet B S hS X.1 Z.1 ⊆ T) :
    ∃ (Y : AlgebraicSpaces B S hS) (f : Y ⟶ X),
      Nonempty (BlowupFactorization B S hS T f) ∧ IsPullbackDefined B S hS f Z

Tag 0BHH, a lemma

Tag 0BHH in the Stacks Project.

AlgebraicGeometry.Space.exists_blowupFactorization_factors_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DominationByPointBlowups.lean, line 91.

Dominating a modification by blowing up closed points. Let S be a scheme, let X be a Noetherian algebraic space over S and let T ⊆ |X| be a finite set of closed points x such that X is regular at x and the local ring of X at x has dimension 2. Let f : Y ⟶ X be a proper morphism of algebraic spaces which is an isomorphism over U = X ∖ T. Then there exist a sequence

X_n ⟶ X_{n-1} ⟶ … ⟶ X_1 ⟶ X_0 = X

where X_{i+1} ⟶ X_i is the blowing up of X_i at a closed point x_i lying above a point of T, and a factorization X_n ⟶ Y ⟶ X of the composition.

theorem exists_blowupFactorization_factors_of_isProper
    (hterm : B.Contains (⊤_ Scheme.{u}))
    (X : AlgebraicSpaces B S hS) (hX : IsNoetherian B S hS hterm X.1)
    (T : Set (points B S hS X.1)) (hTfinite : T.Finite)
    (hTclosed : ∀ x ∈ T, IsClosed ({x} : Set (points B S hS X.1)))
    (hTregular : ∀ x ∈ T, IsRegularAt B S hS X.1 x)
    (hTdim : ∀ x ∈ T, localRingDimension B S hS x = 2)
    (Y : AlgebraicSpaces B S hS) (f : Y ⟶ X) (hf : IsProper B S hS f.hom)
    (hfU : IsIso (pullback.snd f.hom (openSubspaceOfPoints B S hS X.1 Tᶜ).ι)) :
    ∃ (X' : AlgebraicSpaces B S hS) (b : X' ⟶ X),
      Nonempty (BlowupFactorization B S hS T b) ∧ ∃ h : X' ⟶ Y, h ≫ f = b

Sources

Section89.5 Dominating by normalized blowups #

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

Tag 0BHJ, a definition

Tag 0BHJ in the Stacks Project.

AlgebraicGeometry.Space.IsNormalizedBlowupAtClosedPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizedBlowupsAtClosedPoints.lean, line 185.

Stacks 0BHJ. A morphism f : X'' ⟶ X of algebraic spaces is the normalized blowing up of X at the closed point z when it is the composition of the normalization of a blowing up of X at z with that blowing up: there are an algebraic space X', a blowing up b : X' ⟶ X of X at z, normalization data on X', and an identification of X'' with the normalization carrying f to the normalization morphism followed by b.

The blowing up at z is AlgebraicGeometry.Space.IsBlowupAtClosedPoint, and the normalization is the datum AlgebraicGeometry.Space.NormalizationData. The decency hypothesis and the finiteness condition of Stacks 0BB1 are those of the source.

def IsNormalizedBlowupAtClosedPoint {X Y : AlgebraicSpaces B S hS}
    (_hX : IsDecentSpace B S hS X.obj)
    (_hXfin : HasLocallyFiniteIrreducibleComponents B S hS X.obj)
    (z : points B S hS X.obj) (hz : IsClosed ({z} : Set (points B S hS X.obj)))
    (f : Y ⟶ X) : Prop

Tag 0BHK, a lemma

Tag 0BHK in the Stacks Project.

AlgebraicGeometry.Space.NormalizedBlowupAtClosedPoint.isNormal_and_isNagata_and_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizedBlowupAtClosedPoint.lean, line 221. The attribute's comment: “all four assertions — the normalized blowing up is an algebraic space, it is normal, it is Nagata, and it is proper over X — with properness of the blowing up X' ⟶ X itself, which is Stacks 085Z, as the named hypothesis hproperBlowup”.

Stacks 0BHK. If X is Nagata, then the normalized blowing up of X at a closed point z is a normal Nagata algebraic space proper over X.

All four assertions of the source are listed: X'' is an algebraic space over S, it is normal, it is Nagata, and the normalized blowing up X'' ⟶ X is proper.

The hypothesis hproperBlowup is properness of the blowing up X' ⟶ X, which is Stacks 085Z; see the "what is assumed" section of the module documentation.

theorem isNormal_and_isNagata_and_isProper
    (hNagata : HasEtaleLocalProperty B S hS X.obj (fun T : Scheme.{u} => IsNagataScheme T))
    (hproperBlowup : IsProper B S hS N.proj.hom) :
    IsAlgebraicSpace B S hS N.space.obj ∧
      HasEtaleLocalProperty B S hS N.space.obj
        (fun T : Scheme.{u} => _root_.AlgebraicGeometry.IsNormal T) ∧
      HasEtaleLocalProperty B S hS N.space.obj (fun T : Scheme.{u} => IsNagataScheme T) ∧
      IsProper B S hS N.hom.hom

AlgebraicGeometry.Space.NormalizedBlowupAtClosedPoint.isNormal_and_isNagata_and_isProper_of_isNagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizedBlowupAtClosedPointProper.lean, line 133.

Stacks 0BHK. If X is Nagata, then the normalized blowing up of X at a closed point z is a normal Nagata algebraic space proper over X.

Spelled out: for every normalized blowing up X'' ⟶ X' ⟶ X of X at z (Stacks 0BHJ), X'' is an algebraic space over S, it is normal, it is Nagata, and the composite X'' ⟶ X is proper. The only hypothesis is that X is Nagata.

The proof is the source's. The blowing up X' ⟶ X is proper, AlgebraicGeometry.Space.NormalizedBlowupAtClosedPoint.isProper_proj (Stacks 085Z, X being locally Noetherian); hence X' is Nagata (Stacks 0BAU), the normalization X'' ⟶ X' is finite (Stacks 0BB5), hence proper (Stacks 04NZ), and the composite is proper (Stacks 04XY); X'' is normal by Stacks 0BB4 and Nagata by Stacks 0BAU again.

theorem isNormal_and_isNagata_and_isProper_of_isNagata
    (hNagata : HasEtaleLocalProperty B S hS X.obj (fun T : Scheme.{u} => IsNagataScheme T)) :
    IsAlgebraicSpace B S hS N.space.obj ∧
      HasEtaleLocalProperty B S hS N.space.obj
        (fun T : Scheme.{u} => _root_.AlgebraicGeometry.IsNormal T) ∧
      HasEtaleLocalProperty B S hS N.space.obj (fun T : Scheme.{u} => IsNagataScheme T) ∧
      IsProper B S hS N.hom.hom

Tag 0BHL, a lemma

Tag 0BHL in the Stacks Project.

AlgebraicGeometry.Space.NormalizedBlowupFactorization, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizedBlowupsAtClosedPoints.lean, line 427. The attribute's comment: “the condition asserted on both sides of the equivalence: a factorization of the given morphism as a finite sequence of normalized blowings up at closed points lying over the given set of points. The equivalence itself is not proved: its proof is the argument of Tag 0BHF, which this library does carry, together with a comparison of a normalization with an étale base change of it, which it does not.”.

A factorization of f : Y ⟶ X as a sequence of normalized blowings up at closed points lying over the set of points T ⊆ |X|: a tower

Zₘ ⟶ Zₘ₋₁ ⟶ … ⟶ Z₁ ⟶ Z₀ = X

of normalized blowings up at closed points, all of whose centres lie over T, together with an identification of Y with its top Zₘ under which f is the composite Zₘ ⟶ X.

This is the condition on both sides of Stacks 0BHL, taken there with T = {x₁, …, xₙ} for the morphism to X and with T = {uᵢ} for the morphism to the ith étale neighborhood.

structure NormalizedBlowupFactorization (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y : AlgebraicSpaces B S hS} (T : Set (points B S hS X.obj))
    (f : Y ⟶ X)

AlgebraicGeometry.Space.ClosedPointNeighborhoods.GlobalNormalizedBlowupFactorization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizedBlowupsAtClosedPoints.lean, line 526. The attribute's comment: “the left-hand side of the equivalence: the factorization of the morphism to X by normalized blowings up at closed points lying over {x₁, …, xₙ}”.

Stacks 0BHL, the condition on the morphism to X: f : Y ⟶ X factors as

Y = Zₘ ⟶ Zₘ₋₁ ⟶ … ⟶ Z₁ ⟶ Z₀ = X

where each Z_{j+1} ⟶ Z_j is the normalized blowing up of Z_j at a closed point z_j lying over {x₁, …, xₙ}.

abbrev GlobalNormalizedBlowupFactorization {Y : AlgebraicSpaces B S hS} (f : Y ⟶ D.space)

AlgebraicGeometry.Space.ClosedPointNeighborhoods.LocalNormalizedBlowupFactorization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizedBlowupsAtClosedPoints.lean, line 538. The attribute's comment: “the right-hand side of the equivalence: the factorization of the morphism to the i-th elementary étale neighborhood by normalized blowings up at closed points lying over uᵢ”.

Stacks 0BHL, the condition on the morphism to the ith étale neighborhood: gᵢ : Yᵢ ⟶ Uᵢ factors as

Yᵢ = Z_{i, mᵢ} ⟶ … ⟶ Z_{i, 1} ⟶ Z_{i, 0} = Uᵢ

where each Z_{i, j+1} ⟶ Z_{i, j} is the normalized blowing up of Z_{i, j} at a closed point lying over uᵢ.

abbrev LocalNormalizedBlowupFactorization (i : Fin n) {Y : AlgebraicSpaces B S hS}
    (g : Y ⟶ D.neighborhoodSpace i)

AlgebraicGeometry.Space.ClosedPointNeighborhoods.nonempty_globalNormalizedBlowupFactorization_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizedBlowupsAtClosedPointsEquivalence.lean, line 249. The attribute's comment: “corrected (erratum): with X normal; false as written without it, the normalized blowup normalizes the whole space (counterexamples to both directions in the module documentation); otherwise the full statement, under the source's hypotheses”.

Stacks 0BHL, for normal X. Let X, xᵢ, Uᵢ ⟶ X, uᵢ be as in Stacks 0BHA and let f : Y ⟶ X correspond to gᵢ : Yᵢ ⟶ Uᵢ under the functor F of Stacks 0BHA. Assume that X satisfies the equivalent conditions of Stacks 0BB1 and that X is normal. Then f factors as Y = Zₘ ⟶ … ⟶ Z₁ ⟶ Z₀ = X with each Z_{j+1} ⟶ Z_j the normalized blowing up of Z_j at a closed point over {x₁, …, xₙ} if and only if each gᵢ factors as Yᵢ = Z_{i, mᵢ} ⟶ … ⟶ Z_{i, 0} = Uᵢ with each step the normalized blowing up at a closed point over uᵢ.

The normality of X is not in the source, but the statement is false without it; see the module documentation for a counterexample to each direction.

theorem nonempty_globalNormalizedBlowupFactorization_iff
    (hXfin : HasLocallyFiniteIrreducibleComponents B S hS D.space.obj)
    (hXn : Space.IsNormal B S hS D.space.obj) (M : D.modificationsAwayFromPoints)
    (N : ∀ i, D.modificationsAt i) (e : D.restrictionFunctor.obj M ≅ N) :
    Nonempty (D.GlobalNormalizedBlowupFactorization (ObjectProperty.homMk M.obj.hom :
        (⟨M.obj.left, M.property.1⟩ : AlgebraicSpaces B S hS) ⟶ D.space)) ↔
      ∀ i, Nonempty (D.LocalNormalizedBlowupFactorization i (ObjectProperty.homMk (N i).obj.hom :
        (⟨(N i).obj.left, (N i).property.1⟩ : AlgebraicSpaces B S hS) ⟶
          D.neighborhoodSpace i))

Stacks.Examples.NormalizedBlowupsNotEtaleLocal.not_stacks0BHL, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/NormalizedBlowupsNotEtaleLocal.lean, line 555. The attribute's comment: “refutation of the published statement: false without X normal; at X = Spec(Z/36Z), two closed points with non-reduced local rings, g₁ the normalized blowing up of U₁ at u₁ and g₂ = id are sequences of normalized blowings up, but the f corresponding to them is not, a nonempty sequence having a normal source and the empty one being an isomorphism”.

Stacks 0BHL is false as published. The source asserts, for every scheme S, every decent algebraic space X over S satisfying the equivalent conditions of Stacks 0BB1, every choice of pairwise distinct closed points x₁, …, xₙ and elementary étale neighbourhoods (Uᵢ, uᵢ) ⟶ (X, xᵢ) as in Stacks 0BHA, and every f : Y ⟶ X corresponding to gᵢ : Yᵢ ⟶ Uᵢ under the functor F of Stacks 0BHA, that f is a sequence of normalized blowings up at closed points over {x₁, …, xₙ} if and only if each gᵢ is one at closed points over uᵢ. This is the negation of that assertion, with exactly its hypotheses; exists_counterexample is a counterexample to the "if" direction.

The statement holds once X is normal: this is nonempty_globalNormalizedBlowupFactorization_iff in the namespace AlgebraicGeometry.Space.ClosedPointNeighborhoods.

theorem not_stacks0BHL :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) (n : ℕ)
      (D : ClosedPointNeighborhoods B S hS n)
      (_ : HasLocallyFiniteIrreducibleComponents B S hS D.space.obj)
      (M : D.modificationsAwayFromPoints) (N : ∀ i, D.modificationsAt i)
      (_ : D.restrictionFunctor.obj M ≅ N),
      Nonempty (D.GlobalNormalizedBlowupFactorization (ObjectProperty.homMk M.obj.hom :
          (⟨M.obj.left, M.property.1⟩ : AlgebraicSpaces B S hS) ⟶ D.space)) ↔
        ∀ i, Nonempty (D.LocalNormalizedBlowupFactorization i
          (ObjectProperty.homMk (N i).obj.hom :
            (⟨(N i).obj.left, (N i).property.1⟩ : AlgebraicSpaces B S hS) ⟶
              D.neighborhoodSpace i))

Tag 0BHM, a lemma

Tag 0BHM in the Stacks Project.

AlgebraicGeometry.Space.exists_normalizedBlowUpChain_dominating, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SurfaceTransfer/DominatingNormalizedBlowups.lean, line 167.

Stacks 0BHM. Let S be a scheme, let X be a Noetherian Nagata algebraic space over S with dim(X) = 2, and let f : Y ⟶ X be a proper birational morphism. Then there is a commutative diagram
X_n ⟶ X_{n-1} ⟶ … ⟶ X_1 ⟶ X_0
 |                            |
 v                            v
 Y  ------------------------> X
where X_0 ⟶ X is the normalization and X_{i+1} ⟶ X_i is the normalized blowing up of X_i at a closed point: a sequence NormalizedBlowUpChain B S hS X A g with top A = X_n and composite g : X_n ⟶ X, and h : X_n ⟶ Y with h ≫ f = g.

Being Noetherian is Stacks 03EA (quasi-compact, quasi-separated, locally Noetherian), Nagata is the étale-local property of Stacks 03E6, dim(X) is Stacks 04N6, properness is Stacks 04XU, and birationality is Stacks 0ACV, which is defined for decent spaces with finitely many irreducible components; those witnesses are carried existentially, being consequences of the Noetherian hypothesis and of properness rather than extra assumptions.

theorem exists_normalizedBlowUpChain_dominating {X Y : AlgebraicSpaces B S hS}
    (hXN : IsNoetherian B S hS B.contains_terminal X.obj)
    (hXnag : HasEtaleLocalProperty B S hS X.obj (fun T : Scheme.{u} => IsNagataScheme T))
    (hXdim : dimension B S hS X.obj X.property = 2) (f : Y ⟶ X)
    (hf : IsProper B S hS f.hom)
    (hbir : ∃ (hDY : IsDecentSpace B S hS Y.obj) (hDX : IsDecentSpace B S hS X.obj)
      (hCY : (irreducibleComponents (points B S hS Y.obj)).Finite)
      (hCX : (irreducibleComponents (points B S hS X.obj)).Finite),
      IsBirational B S hS Y.property X.property hDY hDX hCY hCX f.hom) :
    ∃ (A : AlgebraicSpaces B S hS) (g : A ⟶ X) (h : A ⟶ Y),
      NormalizedBlowUpChain B S hS X A g ∧ h ≫ f = g

Sources

LeanAlgebraicGeometry.Space.IsNormalizedBlowupAtClosedPoint · AlgebraicGeometry.Space.NormalizedBlowupAtClosedPoint.isNormal_and_isNagata_and_isProper · AlgebraicGeometry.Space.NormalizedBlowupAtClosedPoint.isNormal_and_isNagata_and_isProper_of_isNagata · AlgebraicGeometry.Space.NormalizedBlowupFactorization · AlgebraicGeometry.Space.ClosedPointNeighborhoods.GlobalNormalizedBlowupFactorization · AlgebraicGeometry.Space.ClosedPointNeighborhoods.LocalNormalizedBlowupFactorization · AlgebraicGeometry.Space.ClosedPointNeighborhoods.nonempty_globalNormalizedBlowupFactorization_iff · Stacks.Examples.NormalizedBlowupsNotEtaleLocal.not_stacks0BHL

Section89.6 Base change to the completion #

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

Tag 0BHP, a lemma

Tag 0BHP in the Stacks Project.

AlgebraicGeometry.Space.exists_adicCompletion_ringEquiv_henselianLocalRing_completionSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/HenselianCompletionBaseChange.lean, line 210.

Let (A, 𝔪) be a local ring with finitely generated maximal ideal, let X be a decent algebraic space over Spec A and let Y = X ×_{Spec A} Spec A^ be its base change to the 𝔪-adic completion of A. For a point q of Y whose image p in X lies over the closed point of Spec A, the canonical local homomorphism 𝒪^h_{X,p} ⟶ 𝒪^h_{Y,q} — the one compatible with the local rings of a pair of corresponding elementary étale neighborhoods — induces an isomorphism on 𝔪-adic completions.

theorem exists_adicCompletion_ringEquiv_henselianLocalRing_completionSpace
    (hfg : (IsLocalRing.maximalIdeal A).FG)
    (hX : IsAlgebraicSpace B (Spec (.of A)) hA X)
    (hXdec : IsDecentSpace B (Spec (.of A)) hA X)
    (q : points B (Spec (.of A)) hA (completionSpace A B hA hAc f))
    (p : points B (Spec (.of A)) hA X)
    (hp : pointsMap B (Spec (.of A)) hA (completionSpace A B hA hAc f)
      (completionProjection A B hA hAc f) q = p)
    (hclosed : pointsToScheme B (Spec (.of A)) hA (Over.mk (𝟙 (B.obj hA)))
        (pointsMap B (Spec (.of A)) hA X f p) =
      (⟨IsLocalRing.maximalIdeal A, inferInstance⟩ : PrimeSpectrum A)) :
    letI hY := isAlgebraicSpace_completionSpace A B hA hAc f hX
    letI hYdec := isDecentSpace_completionSpace A B hA hAc f hX hXdec
    letI := isLocalRing_henselianLocalRing B (Spec (.of A)) hA hX hXdec p
    letI := isLocalRing_henselianLocalRing B (Spec (.of A)) hA hY hYdec q
    ∃ φ : (henselianLocalRing B (Spec (.of A)) hA X hX p hXdec : Type (u + 1)) →+*
        (henselianLocalRing B (Spec (.of A)) hA (completionSpace A B hA hAc f) hY q hYdec :
          Type (u + 1)),
      IsLocalHom φ ∧
      (∃ (E : ElementaryEtaleNeighborhood B (Spec (.of A)) hA X hX p)
          (N : ElementaryEtaleNeighborhood B (Spec (.of A)) hA
            (completionSpace A B hA hAc f) hY q)
          (j : N.scheme ⟶ E.scheme) (hj : j.left.1 N.point = E.point),
        yoneda.map j ≫ E.toSpace = N.toSpace ≫ completionProjection A B hA hAc f ∧
          φ.comp (stalkToHenselianLocalRing B (Spec (.of A)) hA X hX p hXdec E) =
            (stalkToHenselianLocalRing B (Spec (.of A)) hA (completionSpace A B hA hAc f) hY q
                hYdec N).comp
              ((E.scheme.left.1.presheaf.stalkCongr (Inseparable.of_eq hj.symm)).hom ≫
                j.left.1.stalkMap N.point).hom) ∧
      ∃ e : AdicCompletion (IsLocalRing.maximalIdeal
            (henselianLocalRing B (Spec (.of A)) hA X hX p hXdec : Type (u + 1)))
            (henselianLocalRing B (Spec (.of A)) hA X hX p hXdec : Type (u + 1)) ≃+*
          AdicCompletion (IsLocalRing.maximalIdeal
            (henselianLocalRing B (Spec (.of A)) hA (completionSpace A B hA hAc f) hY q hYdec :
              Type (u + 1)))
            (henselianLocalRing B (Spec (.of A)) hA (completionSpace A B hA hAc f) hY q hYdec :
              Type (u + 1)),
        e.toRingHom.comp (algebraMap _ _) = (algebraMap _ _).comp φ

Tag 0BHQ, a lemma

Tag 0BHQ in the Stacks Project.

AlgebraicGeometry.Space.isRegularLocalRing_henselianLocalRing_of_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularCompletionBaseChange.lean, line 97. The attribute's comment: “part (1)”.

Stacks 0BHQ, part (1). Let (A, 𝔪) be a Noetherian local ring, let X be a decent algebraic space locally of finite type over Spec A and let Y = X ×_{Spec A} Spec A^ be its base change to the 𝔪-adic completion. If the henselian local ring of Y at a point y is regular, then so is the henselian local ring of X at the image of y.

theorem isRegularLocalRing_henselianLocalRing_of_completion
    (hX : IsAlgebraicSpace B (Spec (.of A)) hA X)
    (hXdec : IsDecentSpace B (Spec (.of A)) hA X)
    (hf : IsLocallyOfFiniteType B (Spec (.of A)) hA f)
    (y : points B (Spec (.of A)) hA (completionSpace A B hA hAc f))
    (hy : IsRegularLocalRing
      (henselianLocalRing B (Spec (.of A)) hA (completionSpace A B hA hAc f)
        (isAlgebraicSpace_completionSpace A B hA hAc f hX) y
        (isDecentSpace_completionSpace A B hA hAc f hX hXdec) : Type (u + 1))) :
    IsRegularLocalRing
      (henselianLocalRing B (Spec (.of A)) hA X hX
        (pointsMap B (Spec (.of A)) hA (completionSpace A B hA hAc f)
          (completionProjection A B hA hAc f) y) hXdec : Type (u + 1))

AlgebraicGeometry.Space.isRegularLocalRing_henselianLocalRing_completion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularCompletionClosedFibre.lean, line 151. The attribute's comment: “part (2)”.

Let (A, 𝔪) be a Noetherian local ring, let X be a decent algebraic space locally of finite type over Spec A and let Y = X ×_{Spec A} Spec A^ be its base change to the 𝔪-adic completion. At a point y of Y lying over the closed point of Spec A^, the henselian local ring of Y at y is regular if and only if the henselian local ring of X at the image of y is regular.

theorem isRegularLocalRing_henselianLocalRing_completion_iff
    (hX : IsAlgebraicSpace B (Spec (.of A)) hA X)
    (hXdec : IsDecentSpace B (Spec (.of A)) hA X)
    (hf : IsLocallyOfFiniteType B (Spec (.of A)) hA f)
    (y : points B (Spec (.of A)) hA (completionSpace A B hA hAc f))
    (hy : pointsToScheme B (Spec (.of A)) hA (completionBase A B hA hAc)
        (pointsMap B (Spec (.of A)) hA (completionSpace A B hA hAc f)
          (pullback.snd f (completionBaseMap A B hA hAc)) y) =
      (⟨IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal A) A),
        inferInstance⟩ :
        PrimeSpectrum (AdicCompletion (IsLocalRing.maximalIdeal A) A))) :
    IsRegularLocalRing
        (henselianLocalRing B (Spec (.of A)) hA (completionSpace A B hA hAc f)
          (isAlgebraicSpace_completionSpace A B hA hAc f hX) y
          (isDecentSpace_completionSpace A B hA hAc f hX hXdec) : Type (u + 1)) ↔
      IsRegularLocalRing
        (henselianLocalRing B (Spec (.of A)) hA X hX
          (pointsMap B (Spec (.of A)) hA (completionSpace A B hA hAc f)
            (completionProjection A B hA hAc f) y) hXdec : Type (u + 1))

AlgebraicGeometry.Space.hasEtaleLocalProperty_isRegular_completionSpace_iff_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularCompletionProper.lean, line 220. The attribute's comment: “part (3)”.

Stacks 0BHQ, part (3). Let (A, 𝔪) be a Noetherian local ring and let X be a decent algebraic space proper over Spec A. Then X is regular if and only if its base change Y = X ×_{Spec A} Spec A^ to the 𝔪-adic completion of A is regular.

theorem hasEtaleLocalProperty_isRegular_completionSpace_iff_of_isProper
    (hX : IsAlgebraicSpace B (Spec (.of A)) hA X)
    (hXdec : IsDecentSpace B (Spec (.of A)) hA X)
    (hproper : IsProper B (Spec (.of A)) hA f) :
    HasEtaleLocalProperty B (Spec (.of A)) hA X (fun T : Scheme.{u} ↦ IsRegular T) ↔
      HasEtaleLocalProperty B (Spec (.of A)) hA (completionSpace A B hA hAc f)
        (fun T : Scheme.{u} ↦ IsRegular T)

Tag 0BHR, a lemma

Tag 0BHR in the Stacks Project.

AlgebraicGeometry.Space.isFinite_normalization_of_isAnalyticallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationSpaceConstruction.lean, line 322. References: SGA 3 XXV (4.2), “more general”.

Stacks 0BHR. Let (A, 𝔪) be an analytically unramified Noetherian local ring and let F be an algebraic space over S whose structure morphism goes to an object of the site with underlying scheme Spec A. If F is locally of finite type over A and its structure morphism is étale at every point of codimension zero, then the normalization morphism F^ν ⟶ F of F is a finite morphism of algebraic spaces.

The normalization is the constructed one, neither assumed nor existentially quantified: F is locally of finite type over a Noetherian ring, so its étale scheme charts are locally Noetherian and satisfy the finiteness condition of Tag 0BB1, and AlgebraicGeometry.Space.normalizationData is then the normalization of F, unique up to a unique isomorphism over F by AlgebraicGeometry.Space.NormalizationData.existsUnique_iso_hom. Finiteness of its normalization morphism is AlgebraicGeometry.Space.NormalizationData.isFinite_hom_of_isAnalyticallyUnramified, which is Stacks 0BG8 on a surjective étale chart followed by the étale-local characterisation of finiteness, condition (3) of Stacks 03ZQ.

The base is a representable presheaf with an isomorphism of its underlying scheme onto Spec A, which is the source's hypothesis with no identification of schemes imposed and with the base scheme S of the site left arbitrary.

theorem isFinite_normalization_of_isAnalyticallyUnramified {A : Type u} [CommRing A]
    [IsNoetherianRing A] [IsLocalRing A] (hA : IsAnalyticallyUnramified A)
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    {Z : BigFppfOver B S hS} (f : F ⟶ yoneda.obj Z)
    (a : (BigFppfOver.toScheme B S hS).obj Z ⟶ Spec (.of A)) [IsIso a]
    (hft : IsLocallyOfFiniteType B S hS f)
    (het : ∀ x : points B S hS F, localRingDimension B S hS x = 0 → IsEtaleAt B S hS f x) :
    IsFinite B S hS (normalizationData B S hS hF
      (hasLocallyFiniteIrreducibleComponents_of_isLocallyOfFiniteType B S hS f a hft)).hom

Sources

LeanAlgebraicGeometry.Space.exists_adicCompletion_ringEquiv_henselianLocalRing_completionSpace · AlgebraicGeometry.Space.isRegularLocalRing_henselianLocalRing_of_completion · AlgebraicGeometry.Space.isRegularLocalRing_henselianLocalRing_completion_iff · AlgebraicGeometry.Space.hasEtaleLocalProperty_isRegular_completionSpace_iff_of_isProper · AlgebraicGeometry.Space.isFinite_normalization_of_isAnalyticallyUnramified

Section89.7 Implied properties #

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

Tag 0BHT, a lemma

Tag 0BHT in the Stacks Project.

AlgebraicGeometry.Space.isFinite_normalization_of_regular_alteration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationFiniteRegularAlteration.lean, line 486. The attribute's comment: “finiteness of the normalization. The source's Noetherian hypothesis on Y is used only as quasi-compactness of its point space and local Noetherianity of its etale charts; the quasi-separatedness that Stacks 03EA also asks for is unused, which is a strengthening. Integrality of Y is part of IsAlteration. The source's Step 1 -- etale localization to a Noetherian domain, which charts of an integral space do not permit -- and its appeal to Stacks 08AR are both replaced by Chow's lemma for spaces (Stacks 089J) over an affine chart, which reduces the finiteness to the degree-zero case of Stacks 02O6 for schemes; see the module docstring”.

Stacks 0BHT, finiteness of the normalization. Let Y be an integral algebraic space over S which is quasi-compact and whose étale scheme charts are locally Noetherian, and suppose there is an alteration f : X ⟶ Y with X regular. Then the normalization morphism Y^ν ⟶ Y of Y is a finite morphism of algebraic spaces.

The normalization is the constructed one, neither assumed nor existentially quantified: the étale scheme charts of Y are locally Noetherian, so they satisfy the finiteness condition of Stacks 0BB1 by Stacks 0GMB, and AlgebraicGeometry.Space.normalizationData is then the normalization of Y, unique up to a unique isomorphism over Y by AlgebraicGeometry.Space.NormalizationData.existsUnique_iso_hom.

theorem isFinite_normalization_of_regular_alteration
    (f : X ⟶ Y) (hf : IsAlteration B S hS f)
    (hXreg : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsRegular T))
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYnoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T)) :
    IsFinite B S hS (normalizationData B S hS hf.1
      (hasLocallyFiniteIrreducibleComponents_of_isLocallyNoetherian B S hS Y hf.1 hYnoeth)).hom

AlgebraicGeometry.Space.exists_isDenseOpenSubspace_hasEtaleLocalProperty_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularAlterationImpliedProperties.lean, line 203. The attribute's comment: “the regular dense open; the source's Noetherian hypothesis on Y and the finiteness of f over a nonempty open are unused, only reducedness of Y and properness and dominance of f, which is a strengthening. The source's Stacks 07NG enters as the space-level descent Stacks 06MK, whose engine on local rings is that same statement”.

Stacks 0BHT, the dense regular open. An integral algebraic space Y over S admitting an alteration f : X ⟶ Y whose source is regular has a dense open subspace which is regular.

theorem exists_isDenseOpenSubspace_hasEtaleLocalProperty_isRegular (f : X ⟶ Y)
    (hf : IsAlteration B S hS f)
    (hXreg : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsRegular T)) :
    ∃ V : Subfunctor Y, IsDenseOpenSubspace B S hS hf.1 V ∧
      HasEtaleLocalProperty B S hS V.toFunctor (fun T : Scheme.{u} => IsRegular T)

AlgebraicGeometry.Space.NormalizationData.isFinite_hom_of_regular_alteration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularAlterationImpliedProperties.lean, line 320. The attribute's comment: “finiteness of the normalization, for a REPRESENTABLE AFFINE target: the source's Step 1, etale localization to a Noetherian domain, is invalid for algebraic spaces -- charts of an integral space are reduced but not irreducible, so Stacks 0BH3 does not apply over them. Conditional on h02O6, the degree-zero case of Stacks 02O6 for algebraic spaces, which this library lacks; see the module docstring”.

Stacks 0BHT, finiteness of the normalization, for a target represented by an affine object of the site and conditional on the degree-zero case of Stacks 02O6. Let Z be an affine object of the site whose scheme is integral and locally Noetherian, let f : X ⟶ h_Z be an alteration with X regular, and let D be normalization data for h_Z. Then the normalization morphism of D is finite.

theorem NormalizationData.isFinite_hom_of_regular_alteration {Z : BigFppfOver B S hS}
    [IsAffine ((BigFppfOver.toScheme B S hS).obj Z)]
    [_root_.AlgebraicGeometry.IsIntegral ((BigFppfOver.toScheme B S hS).obj Z)]
    [IsLocallyNoetherian ((BigFppfOver.toScheme B S hS).obj Z)]
    (f : X ⟶ yoneda.obj Z) (hf : IsAlteration B S hS f)
    (hXreg : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsRegular T))
    (h02O6 : ∃ φ : Γ((BigFppfOver.toScheme B S hS).obj Z, ⊤) →+*
        ↥(RingCat.sectionsSubring
          (structurePresheaf B S hS X ⋙ forget₂ CommRingCat.{u} RingCat.{u})),
      Function.Injective φ ∧ φ.Finite)
    (D : NormalizationData B S hS (yoneda.obj Z)) :
    IsFinite B S hS D.hom

Tag 0BHU, a lemma

Tag 0BHU in the Stacks Project.

AlgebraicGeometry.Space.exists_isRegularRing_localizationAway_of_regular_spaceAlteration, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ImpliedProperties/LocalDomainSpaceAlteration.lean, line 164. The attribute's comment: “clause (1), regular after inverting one element”.

A Noetherian local domain admitting an alteration by a regular algebraic space is regular after inverting one nonzero element. The dense regular open of [Stacks, Tag 0BHT] at the representable target Spec A contains a nonempty basic open D(a) of Spec A, and Γ(D(a)) = A_a.

public alias exists_isRegularRing_localizationAway_of_regular_spaceAlteration

AlgebraicGeometry.Space.module_finite_integralClosure_of_regular_spaceAlteration, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ImpliedProperties/LocalDomainSpaceAlteration.lean, line 172. The attribute's comment: “clause (2), finite integral closure”.

The integral closure of a Noetherian local domain admitting an alteration by a regular algebraic space is a finite module over it. The normalization of Spec A is finite by [Stacks, Tag 0BHT], and it is the spectrum of the integral closure of A in Frac(A) ([Stacks, Tag 035P]).

public alias module_finite_integralClosure_of_regular_spaceAlteration

AlgebraicGeometry.Space.isNormalRing_adicCompletion_integralClosure_of_regular_spaceAlteration, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ImpliedProperties/LocalDomainSpaceAlteration.lean, line 182. The attribute's comment: “clause (3), normal completion of the integral closure”.

The completion of the integral closure is normal. With C = Γ(X, 𝒪_X) and B the integral closure of A in Frac(A), the inclusion B ⊆ C is a map of finite A-algebras and B is a normal domain, so [Stacks, Tag 0BGH] reduces normality of Bˆ to normality of Cˆ = Aˆ ⊗_A C, which is the global functions of the regular base change X ×_{Spec A} Spec Aˆ ([Stacks, Tag 073K], [Stacks, Tag 0BHQ]). Normality here is IsNormalRing, which for a finite algebra over a Noetherian local ring is normality of the completions at the maximal ideals.

public alias isNormalRing_adicCompletion_integralClosure_of_regular_spaceAlteration

AlgebraicGeometry.Space.isRegularRing_genericFormalFibre_of_regular_spaceAlteration, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ImpliedProperties/LocalDomainSpaceAlteration.lean, line 191. The attribute's comment: “clause (4), regular generic formal fibre”.

The generic formal fibre of a Noetherian local domain admitting an alteration by a regular algebraic space is regular. For an affine étale chart V of X through the generic point the ring Aˆ ⊗_A Γ(V, 𝒪_V) is regular by [Stacks, Tag 0BHQ], and the generic formal fibre is recovered by inverting A ∖ {0} and descending along the faithfully flat Frac(A)-algebra Frac(A) ⊗_A Γ(V, 𝒪_V) by [Stacks, Tag 07NG].

public alias isRegularRing_genericFormalFibre_of_regular_spaceAlteration

AlgebraicGeometry.Space.exists_isRegularRing_localizationAway_of_isAlteration_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ImpliedProperties/RegularSpaceAlterationLocalDomain.lean, line 473. The attribute's comment: “part (1)”.

A Noetherian local domain admitting an alteration by a regular algebraic space is regular after inverting one nonzero element. The dense regular open of [Stacks, Tag 0BHT], read at the representable target Spec A by AlgebraicGeometry.Space.denseRegularOpenOfRegularAlteration, contains a nonempty basic open D(a) of Spec A, and Γ(D(a)) = A_a.

public theorem exists_isRegularRing_localizationAway_of_isAlteration_of_isRegular
    (A : Type u) [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsLocalRing A]
    (B : BigFppfSite.{u}) (hA : B.Contains (Spec (.of A)))
    (X : (BigFppfOver B (Spec (.of A)) hA)ᵒᵖ ⥤ Type u)
    (g : X ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hA))))
    (hg : IsAlteration B (Spec (.of A)) hA g)
    (hreg : HasEtaleLocalProperty B (Spec (.of A)) hA X (fun T : Scheme.{u} => IsRegular T)) :
    ∃ a : A, a ≠ 0 ∧ IsRegularRing (Localization.Away a)

AlgebraicGeometry.Space.module_finite_integralClosure_of_isAlteration_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ImpliedProperties/RegularSpaceAlterationLocalDomain.lean, line 505. The attribute's comment: “part (2)”.

The integral closure of a Noetherian local domain admitting an alteration by a regular algebraic space is a finite module over it. This is clause (2) of [Stacks, Tag 0BHU]: A is N-1 (IsN1).

The alteration makes Spec A an integral algebraic space carrying a regular alteration, so [Stacks, Tag 0BHT] applies to it; Spec A is its own affine surjective étale scheme chart, the identity being surjective and étale, and along that chart AlgebraicGeometry.Space.NormalizationData.isFinite_normalization_chart_of_regular_alteration gives that the normalization morphism of the scheme Spec A is finite. By [Stacks, Tag 035P] that morphism is the spectrum map of A ⟶ integralClosure A (Frac A), so the integral closure is a finite A-module; that reading is AlgebraicGeometry.module_finite_integralClosure_of_isFinite_normalization, which takes the presenting ring of the scheme — here A itself — rather than its ring of global sections.

The source argues instead that C = Γ(X, 𝒪_X) is a finite A-module by [Stacks, Tag 08AR] and integrally closed, and that the integral closure embeds into C; the route above replaces that by Chow's lemma for algebraic spaces over the chart and the degree-zero case of [Stacks, Tag 02O6] for schemes, which is how [Stacks, Tag 0BHT] is proved here.

public theorem module_finite_integralClosure_of_isAlteration_of_isRegular
    (A : Type u) [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsLocalRing A]
    (B : BigFppfSite.{u}) (hA : B.Contains (Spec (.of A)))
    (X : (BigFppfOver B (Spec (.of A)) hA)ᵒᵖ ⥤ Type u)
    (g : X ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hA))))
    (hg : IsAlteration B (Spec (.of A)) hA g)
    (hreg : HasEtaleLocalProperty B (Spec (.of A)) hA X (fun T : Scheme.{u} => IsRegular T)) :
    Module.Finite A ↥(integralClosure A (FractionRing A))

AlgebraicGeometry.Space.isNormalRing_adicCompletion_integralClosure_of_isAlteration_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ImpliedProperties/RegularSpaceAlterationLocalDomain.lean, line 647. The attribute's comment: “part (3)”.

The completion of the integral closure of a Noetherian local domain admitting an alteration by a regular algebraic space is normal. This is part (3) of [Stacks, Tag 0BHU]. Let B be the integral closure of A in Frac(A) and C = Γ(X, 𝒪_X). Then C is a finite A-module and a normal domain containing A ([Stacks, Tag 0BH3]), so B ⊆ C, and Cˆ = Aˆ ⊗_A C is normal by AlgebraicGeometry.Space.globalFunctions_of_isAlteration_of_isRegular; [Stacks, Tag 0BGH] gives normality of Bˆ. Normality is IsNormalRing: every localization at a prime is a normal domain, which for the finite algebra Bˆ over the complete local Aˆ is normality of the completions of B at its maximal ideals.

public theorem isNormalRing_adicCompletion_integralClosure_of_isAlteration_of_isRegular
    (A : Type u) [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsLocalRing A]
    (B : BigFppfSite.{u}) (hA : B.Contains (Spec (.of A)))
    (X : (BigFppfOver B (Spec (.of A)) hA)ᵒᵖ ⥤ Type u)
    (g : X ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hA))))
    (hg : IsAlteration B (Spec (.of A)) hA g)
    (hreg : HasEtaleLocalProperty B (Spec (.of A)) hA X (fun T : Scheme.{u} => IsRegular T)) :
    IsNormalRing
      (AdicCompletion
        ((IsLocalRing.maximalIdeal A).map
          (algebraMap A ↥(integralClosure A (FractionRing A))))
        ↥(integralClosure A (FractionRing A)))

AlgebraicGeometry.Space.isRegularRing_genericFormalFibre_of_isAlteration_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ImpliedProperties/RegularSpaceAlterationLocalDomain.lean, line 694. The attribute's comment: “part (4)”. References: EGA IV (7.9.3), “special case”.

The generic formal fibre of a Noetherian local domain admitting an alteration by a regular algebraic space is regular. For an affine étale chart V of X through the generic point the ring Aˆ ⊗_A Γ(V, 𝒪_V) is regular, and the generic formal fibre is recovered by inverting A ∖ {0} and descending along the faithfully flat Frac(A)-algebra Frac(A) ⊗_A Γ(V, 𝒪_V) by [Stacks, Tag 07NG]. Regularity of the completed base change of the chart is part (3) of [Stacks, Tag 0BHQ], applied through AlgebraicGeometry.Space.exists_injective_isRegularRing_adicCompletion_tensorProduct.

public theorem isRegularRing_genericFormalFibre_of_isAlteration_of_isRegular
    (A : Type u) [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsLocalRing A]
    (B : BigFppfSite.{u}) (hA : B.Contains (Spec (.of A)))
    (X : (BigFppfOver B (Spec (.of A)) hA)ᵒᵖ ⥤ Type u)
    (g : X ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hA))))
    (hg : IsAlteration B (Spec (.of A)) hA g)
    (hreg : HasEtaleLocalProperty B (Spec (.of A)) hA X (fun T : Scheme.{u} => IsRegular T)) :
    IsRegularRing ((AdicCompletion (IsLocalRing.maximalIdeal A) A) ⊗[A] (FractionRing A))

Sources

LeanAlgebraicGeometry.Space.isFinite_normalization_of_regular_alteration · AlgebraicGeometry.Space.exists_isDenseOpenSubspace_hasEtaleLocalProperty_isRegular · AlgebraicGeometry.Space.NormalizationData.isFinite_hom_of_regular_alteration · AlgebraicGeometry.Space.exists_isRegularRing_localizationAway_of_regular_spaceAlteration · AlgebraicGeometry.Space.module_finite_integralClosure_of_regular_spaceAlteration · AlgebraicGeometry.Space.isNormalRing_adicCompletion_integralClosure_of_regular_spaceAlteration · AlgebraicGeometry.Space.isRegularRing_genericFormalFibre_of_regular_spaceAlteration · AlgebraicGeometry.Space.exists_isRegularRing_localizationAway_of_isAlteration_of_isRegular

Section89.8 Resolution #

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

Tag 0BHW, a definition

Tag 0BHW in the Stacks Project.

AlgebraicGeometry.Space.IsResolutionOfSingularities, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ResolutionOfSingularities.lean, line 62.

A resolution of singularities of a Noetherian integral algebraic space Y over S is a modification f : X ⟶ Y whose source X is regular.

abbrev IsResolutionOfSingularities {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (_hYnoeth : IsNoetherian B S hS hZ Y) (hYint : IsIntegralSpace B S hS Y)
    (_hdecentX : IsDecentSpace B S hS X)
    (_hdecentY : IsDecentSpace B S hS Y) (f : X ⟶ Y) : Prop

Tag 0BHX, a definition

Tag 0BHX in the Stacks Project.

AlgebraicGeometry.Space.HasResolutionByNormalizedBlowUps, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ResolutionByNormalizedBlowUps.lean, line 133.

Stacks 0BHX. A two-dimensional Noetherian integral algebraic space Y over S has a resolution of singularities by normalized blowups when the normalization of Y can be followed by finitely many normalizations of blowing ups at closed points, all of them proper over Y, so as to reach a regular algebraic space.

abbrev HasResolutionByNormalizedBlowUps (Y : AlgebraicSpaces B S hS)
    (_hYdim : dimension B S hS Y.obj Y.property = 2)
    (_hYnoeth : IsNoetherian B S hS hZ Y.obj)
    (_hYint : IsIntegralSpace B S hS Y.obj) : Prop

Tag 0BHY, a theorem

Tag 0BHY in the Stacks Project.

AlgebraicGeometry.Space.tfae_resolution_of_dimension_eq_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SurfaceResolutionTheorem.lean, line 64.

Stacks 0BHY. For a two-dimensional integral Noetherian algebraic space Y over S, the following are equivalent: (1) there is an alteration X ⟶ Y with X regular; (2) Y has a resolution of singularities; (3) Y has a resolution of singularities by normalized blowups; (4) the normalization Y^ν ⟶ Y is finite, Y^ν has finitely many singular points, and the completion of the henselian local ring of Y^ν at each of them is normal.

theorem tfae_resolution_of_dimension_eq_two (hZ : B.Contains (⊤_ Scheme.{u}))
    (Y : AlgebraicSpaces B S hS) (hYdim : dimension B S hS Y.obj Y.property = 2)
    (hYnoeth : IsNoetherian B S hS hZ Y.obj) (hYint : IsIntegralSpace B S hS Y.obj) :
    List.TFAE
      [∃ (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : X ⟶ Y.obj), IsAlteration B S hS f ∧
          HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsRegular T),
        ∃ (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
          (hdecentX : IsDecentSpace B S hS X) (f : X ⟶ Y.obj),
          IsResolutionOfSingularities B S hS hZ hX Y.property hYnoeth hYint hdecentX
            (hYint.isDecentSpace B S hS Y.obj) f,
        HasResolutionByNormalizedBlowUps B S hS hZ Y hYdim hYnoeth hYint,
        ∀ D : NormalizationData B S hS Y.obj,
          D.IsSurfaceResolutionCriterion Y.property (hYint.isDecentSpace B S hS Y.obj)]

Sources

LeanAlgebraicGeometry.Space.IsResolutionOfSingularities · AlgebraicGeometry.Space.HasResolutionByNormalizedBlowUps · AlgebraicGeometry.Space.tfae_resolution_of_dimension_eq_two

Section89.9 Examples #

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

Tag 0AE9, an example

Tag 0AE9 in the Stacks Project.

Stacks.Resolution.trinomial_irreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/TrinomialHypersurface.lean, line 183. The attribute's comment: “irreducibility”.

The defining trinomial is irreducible for positive pairwise coprime exponents.

theorem trinomial_irreducible (k : Type u) [Field k]
    (r s t : ℕ) (_hr : 0 < r) (_hs : 0 < s) (ht : 0 < t)
    (hrs : r.Coprime s) (_hrt : r.Coprime t) (_hst : s.Coprime t) :
    Irreducible (MvPolynomial.X (0 : Fin 3) ^ r +
      MvPolynomial.X (1 : Fin 3) ^ s +
      MvPolynomial.X (2 : Fin 3) ^ t : MvPolynomial (Fin 3) k)

Stacks.Resolution.trinomialRing_isDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/TrinomialHypersurface.lean, line 201. The attribute's comment: “integrality”.

The trinomial hypersurface is integral.

theorem trinomialRing_isDomain (k : Type u) [Field k]
    (r s t : ℕ) (hr : 0 < r) (hs : 0 < s) (ht : 0 < t)
    (hrs : r.Coprime s) (hrt : r.Coprime t) (hst : s.Coprime t) :
    IsDomain (trinomialRing k r s t)

Stacks.Resolution.trinomialRing_z_isPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/TrinomialHypersurface.lean, line 263. The attribute's comment: “the prime element z”.

The image of z generates a prime ideal in the hypersurface ring.

theorem trinomialRing_z_isPrime (k : Type u) [Field k]
    (r s t : ℕ) (_hr : 0 < r) (_hs : 0 < s) (ht : 0 < t)
    (hrs : r.Coprime s) :
    (Ideal.span ({Ideal.Quotient.mk _ (MvPolynomial.X (2 : Fin 3))} :
      Set (trinomialRing k r s t))).IsPrime

Stacks.Resolution.trinomialRing_localization_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/TrinomialHypersurface.lean, line 421. The attribute's comment: “localized polynomial presentation”.

When t = 1 + e r s, localization at z is the localization of a polynomial ring in x', y' at -((x') ^ r + (y') ^ s), with the stated coordinate formulas.

theorem trinomialRing_localization_equiv (k : Type u) [Field k]
    (r s e : ℕ) :
    ∃ φ : Localization.Away
        (Ideal.Quotient.mk _ (MvPolynomial.X (2 : Fin 3)) :
          trinomialRing k r s (1 + e * r * s)) ≃ₐ[k]
        Localization.Away (-(MvPolynomial.X (0 : Fin 2) ^ r +
          MvPolynomial.X (1 : Fin 2) ^ s) : MvPolynomial (Fin 2) k),
      φ (algebraMap (trinomialRing k r s (1 + e * r * s)) _
          (Ideal.Quotient.mk _ (MvPolynomial.X (0 : Fin 3)))) =
        algebraMap (MvPolynomial (Fin 2) k) _
          (MvPolynomial.X (0 : Fin 2) *
            (-(MvPolynomial.X (0 : Fin 2) ^ r +
              MvPolynomial.X (1 : Fin 2) ^ s)) ^ (e * s)) ∧
      φ (algebraMap (trinomialRing k r s (1 + e * r * s)) _
          (Ideal.Quotient.mk _ (MvPolynomial.X (1 : Fin 3)))) =
        algebraMap (MvPolynomial (Fin 2) k) _
          (MvPolynomial.X (1 : Fin 2) *
            (-(MvPolynomial.X (0 : Fin 2) ^ r +
              MvPolynomial.X (1 : Fin 2) ^ s)) ^ (e * r)) ∧
      φ (algebraMap (trinomialRing k r s (1 + e * r * s)) _
          (Ideal.Quotient.mk _ (MvPolynomial.X (2 : Fin 3)))) =
        algebraMap (MvPolynomial (Fin 2) k) _
          (-(MvPolynomial.X (0 : Fin 2) ^ r +
            MvPolynomial.X (1 : Fin 2) ^ s))

Stacks.Resolution.trinomialRing_localization_uniqueFactorizationMonoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/TrinomialHypersurface.lean, line 491. The attribute's comment: “factorial localization”.

In the explicit presentation, inverting z gives a unique factorization monoid.

theorem trinomialRing_localization_uniqueFactorizationMonoid (k : Type u) [Field k]
    (r s e : ℕ) :
    UniqueFactorizationMonoid
      (Localization.Away
        (Ideal.Quotient.mk _ (MvPolynomial.X (2 : Fin 3)) :
          trinomialRing k r s (1 + e * r * s)))

Stacks.Resolution.trinomialRing_uniqueFactorizationMonoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/TrinomialHypersurface.lean, line 710. The attribute's comment: “unique factorization”.

The trinomial hypersurface is a unique factorization domain.

theorem trinomialRing_uniqueFactorizationMonoid (k : Type u) [Field k]
    (r s t : ℕ) (hr : 0 < r) (hs : 0 < s) (ht : 0 < t)
    (hrs : r.Coprime s) (hrt : r.Coprime t) (hst : s.Coprime t) :
    UniqueFactorizationMonoid (trinomialRing k r s t)

Tag 0AEA, an example

Tag 0AEA in the Stacks Project.

Stacks.MvPowerSeries.Brieskorn.not_uniqueFactorizationMonoid_brieskornHypersurface, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MvPowerSeries/BrieskornHypersurface.lean, line 963. The attribute's comment: “the general nonfactoriality assertion”.

Apart from the E₈ triple (2, 3, 5), a Brieskorn hypersurface with ordered, pairwise coprime exponents greater than one is not factorial.

public theorem not_uniqueFactorizationMonoid_brieskornHypersurface
    {r s t : ℕ} (hr : 1 < r) (hrs : r < s) (hst : s < t)
    (hrs' : Nat.Coprime r s) (hrt' : Nat.Coprime r t) (hst' : Nat.Coprime s t)
    (hE8 : ¬ (r = 2 ∧ s = 3 ∧ t = 5)) :
    ¬ UniqueFactorizationMonoid (BrieskornHypersurface r s t)

Stacks.MvPowerSeries.Brieskorn.not_uniqueFactorizationMonoid_brieskornHypersurface_two_five_seven, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MvPowerSeries/BrieskornHypersurface.lean, line 973. The attribute's comment: “the explicit (2, 5, 7) example”.

The hypersurface ℂ⟦x,y,z⟧/(x²+y⁵+z⁷) is not factorial.

public theorem not_uniqueFactorizationMonoid_brieskornHypersurface_two_five_seven :
    ¬ UniqueFactorizationMonoid (BrieskornHypersurface 2 5 7)

Sources

LeanStacks.Resolution.trinomial_irreducible · Stacks.Resolution.trinomialRing_isDomain · Stacks.Resolution.trinomialRing_z_isPrime · Stacks.Resolution.trinomialRing_localization_equiv · Stacks.Resolution.trinomialRing_localization_uniqueFactorizationMonoid · Stacks.Resolution.trinomialRing_uniqueFactorizationMonoid · Stacks.MvPowerSeries.Brieskorn.not_uniqueFactorizationMonoid_brieskornHypersurface · Stacks.MvPowerSeries.Brieskorn.not_uniqueFactorizationMonoid_brieskornHypersurface_two_five_seven

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

89 Resolution of Surfaces Revisited

Section89.2 Modifications#

Tag 0AE2, an equation

Tag 0AE3, a lemma

Tag 0AGM, a lemma

Tag 0AYJ, a lemma

Tag 0AGN, a lemma

Sources

Section89.3 Strategy#

Tag 0BHA, an equation

Tag 0BHB, a lemma

Tag 0BHC, a lemma

Tag 0BHD, a lemma

Sources

Section89.4 Dominating by quadratic transformations#

Tag 0BHE, a definition

Tag 0BHF, a lemma

Tag 0BHG, a lemma

Tag 0BHH, a lemma

Sources

Section89.5 Dominating by normalized blowups#

Tag 0BHJ, a definition

Tag 0BHK, a lemma

Tag 0BHL, a lemma

Tag 0BHM, a lemma

Sources

Section89.6 Base change to the completion#

Tag 0BHP, a lemma

Tag 0BHQ, a lemma

Tag 0BHR, a lemma

Sources

Section89.7 Implied properties#

Tag 0BHT, a lemma

Tag 0BHU, a lemma

Sources

Section89.8 Resolution#

Tag 0BHW, a definition

Tag 0BHX, a definition

Tag 0BHY, a theorem

Sources

Section89.9 Examples#

Tag 0AE9, an example

Tag 0AEA, an example

Sources

Section89.2 Modifications #

Section89.3 Strategy #

Section89.4 Dominating by quadratic transformations #

Section89.5 Dominating by normalized blowups #

Section89.6 Base change to the completion #

Section89.7 Implied properties #

Section89.8 Resolution #

Section89.9 Examples #