71.17 Blowing up to 71.19 Admissible blowups

Section71.17 Blowing up#

Section 71.17 of the Stacks Project, Tag 085P. 12 tags here are carried by 28 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 085Q, a definition

Tag 085Q in the Stacks Project.

AlgebraicGeometry.Space.blowUpAlong', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupEquivalenceRelationClosed.lean, line 78. The attribute's comment: “the blowup of X along Z as the relative Proj of the Rees algebra, the same object as blowUpAlong with the descent datum's equivalence-relation field discharged rather than assumed; the three B.Contains side conditions on the relative Projs remain”.

Stacks 085Q. The blowing up of an algebraic space X along a closed subspace Z ⊆ X: the relative Proj Proj_X(⨁_{n ≥ 0} 𝓘_Zⁿ) of the Rees algebra of the defining ideal sheaf of Z, as an algebraic space over S.

This is AlgebraicGeometry.Space.blowUpAlong with its equivalence-relation parameter supplied by AlgebraicGeometry.Space.isEquivalenceRelation_post_reesProj rather than assumed.

def blowUpAlong' : AlgebraicSpaces B S hS

AlgebraicGeometry.Space.blowUpAlongHom', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupEquivalenceRelationClosed.lean, line 89. The attribute's comment: “the morphism b of the blowup, with the descent datum's equivalence-relation field discharged rather than assumed; the three B.Contains side conditions on the relative Projs remain”.

Stacks 085Q. The blowing up b : Proj_X(⨁_{n ≥ 0} 𝓘_Zⁿ) ⟶ X of an algebraic space X along a closed subspace Z ⊆ X, as a morphism of algebraic spaces over S, with the equivalence-relation field of the descent datum discharged.

def blowUpAlongHom' : blowUpAlong' Z P hcU hcR hcRR ⟶ X

AlgebraicGeometry.Space.exceptionalDivisor', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupEquivalenceRelationClosed.lean, line 100. The attribute's comment: “the exceptional divisor b⁻¹(Z) of the blowup and the centre Z, with the descent datum's equivalence-relation field discharged rather than assumed; the three B.Contains side conditions on the relative Projs remain”.

Stacks 085Q. The exceptional divisor b⁻¹(Z) of the blowing up of X along Z: the inverse image of the centre along the structure morphism of the blowup, as a closed subspace of the blowup, with the equivalence-relation field of the descent datum discharged.

def exceptionalDivisor' : ClosedSubspaces B S hS (blowUpAlong' Z P hcU hcR hcRR).obj

AlgebraicGeometry.Space.blowUpAlong, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupRelativeProj.lean, line 439. The attribute's comment: “the blowup as the relative Proj of the Rees algebra, with the descent datum's equivalence-relation field carried as a parameter; Φ and its invertibility and both pullback squares are supplied from the Rees comparison”.

The blowing up of an algebraic space X along a closed subspace Z ⊆ X: the relative Proj Proj_X(⨁_{n ≥ 0} 𝓘_Zⁿ) of the Rees algebra of the defining ideal sheaf of Z, as an algebraic space over S. The subspace Z is the centre.

def blowUpAlong : AlgebraicSpaces B S hS

AlgebraicGeometry.Space.blowUpAlongHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupRelativeProj.lean, line 446. The attribute's comment: “the morphism b of the blowup, with the descent datum's equivalence-relation field carried as a parameter”.

The blowing up b : Proj_X(⨁_{n ≥ 0} 𝓘_Zⁿ) ⟶ X of an algebraic space X along a closed subspace Z ⊆ X, as a morphism of algebraic spaces over S.

def blowUpAlongHom : blowUpAlong Z P hcU hcR heq ⟶ X

AlgebraicGeometry.Space.exceptionalDivisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupRelativeProj.lean, line 452. The attribute's comment: “the exceptional divisor b⁻¹(Z) of the blowup, and the centre Z”.

The exceptional divisor b⁻¹(Z) of the blowing up of X along Z: the inverse image of the centre along the structure morphism of the blowup, as a closed subspace of the blowup.

def exceptionalDivisor : ClosedSubspaces B S hS (blowUpAlong Z P hcU hcR heq).obj

Tag 085R, a lemma

Tag 085R in the Stacks Project.

AlgebraicGeometry.Space.exists_iso_proj_reesGrading_affineChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupAffineChartRees.lean, line 447. The attribute's comment: “the canonical isomorphism clause: for an affine scheme U = Spec A of the site étale over X, the fibre product U ×_X X' is the scheme Proj of the Rees algebra of the ideal I of A corresponding to the restriction of the centre's defining sheaf of ideals, by an isomorphism over U; the blowup b is named by the universal property of Stacks 085U, and the only side conditions are the three B.Contains conditions on the relative Projs of the chart's own presentation that the construction of Stacks 085Q already takes; the tag's affine open covering clause is a separate registration”.

Stacks 085R, the canonical isomorphism. Let S be a scheme, let X be an algebraic space over S, let Z ⊆ X be a closed subspace with quasi-coherent defining sheaf of ideals ℐ ⊆ 𝒪_X and let b : X' ⟶ X be the blowup of X in Z. Let U = Spec A be an affine scheme of the site étale over X and let I ⊆ A be the ideal corresponding to ℐ|_U. Then U ×_X X' is a scheme, and it is canonically isomorphic over U to the homogeneous spectrum Proj(⨁_{d ≥ 0} Iᵈ) of the Rees algebra of I in A.

The first isomorphism exhibits the fibre product as the algebraic space of a scheme of the site, namely the relative Proj P_U of the Rees algebra of ℐ|_U, compatibly with the projections to U; the second identifies that scheme over U with Proj of the Rees algebra of I, where I is the ideal of sections of ℐ|_U over A, which is the defining ideal of the centre on the chart by AlgebraicGeometry.Space.reesChartIdeal_selfPresentation_eq_ofIdealTop.

theorem exists_iso_proj_reesGrading_affineChart
    {X X' W : AlgebraicSpaces B S hS} {Z : ClosedSubspaces B S hS X.obj}
    {b : X' ⟶ X} (hb : IsBlowupAlong B S hS Z b)
    (V : BigFppfOver B S hS) [IsAffine ((BigFppfOver.toScheme B S hS).obj V)]
    {a : schemeSpace V ⟶ X} (ha : IsEtale B S hS a.hom)
    (hcU : B.Contains (reesChartSituation (centreIdeal (preimageClosedSubspace a Z))
      (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)).relativeProj)
    (hcR : B.Contains (reesRelationSituation (centreIdeal (preimageClosedSubspace a Z))
      (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)).relativeProj)
    (hcRR : B.Contains (reesDoubleSituation (centreIdeal (preimageClosedSubspace a Z))
      (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)).relativeProj)
    {q : W ⟶ schemeSpace V} {r : W ⟶ X'} (sq : IsPullback q r a b)
    (I : Ideal ↥Γ((BigFppfOver.toScheme B S hS).obj V,
      (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)).1))
    (hI : (reesChartIdeal (centreIdeal (preimageClosedSubspace a Z))
        (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)).ideal
        (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)) = I) :
    ∃ e : W ≅ schemeSpace (reesProjChart (centreIdeal (preimageClosedSubspace a Z))
        (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V) hcU),
      e.hom ≫ schemeSpaceMap (reesProjChartHom (centreIdeal (preimageClosedSubspace a Z))
          (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V) hcU) = q ∧
      ∃ f : AlgebraicGeometry.Proj (Stacks.Blowup.reesGrading I) ≅
          (BigFppfOver.toScheme B S hS).obj
            (reesProjChart (centreIdeal (preimageClosedSubspace a Z))
              (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V) hcU),
        f.hom ≫ (BigFppfOver.toScheme B S hS).map
            (reesProjChartHom (centreIdeal (preimageClosedSubspace a Z))
              (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V) hcU) =
          Stacks.Blowup.toSpec I ≫
            (Stacks.RelativeProj.isAffineOpen (Stacks.Blowup.topAffineOpen
              ((BigFppfOver.toScheme B S hS).obj V))).isoSpec.inv ≫
              (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)).1.ι

AlgebraicGeometry.Space.exists_iSup_opensRange_specAffineBlowupι_affineChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupAffineChartRees.lean, line 497. The attribute's comment: “the affine open covering clause: the scheme U ×_X X' is covered by the images of the open immersions Spec A[I/a] ⟶ U ×_X X', a ∈ I, out of the spectra of the affine blowup algebras; same hypotheses and same side conditions as the canonical-isomorphism clause”.

Stacks 085R, the affine open covering. In the situation of AlgebraicGeometry.Space.exists_iso_proj_reesGrading_affineChart, the scheme representing U ×_X X' has an affine open covering by the spectra of the affine blowup algebras A[I/a], a ∈ I: the morphisms Spec A[I/a] ⟶ U ×_X X' obtained by composing the standard chart Stacks.Blowup.specAffineBlowupι with the identification of the previous theorem -- the same isomorphism over U, whose compatibility with the projections to U is restated here -- are open immersions whose images have supremum the whole space.

The sources of the covering morphisms are the spectra of the affine blowup algebras Stacks.Blowup.affineBlowup I a by construction, so this is the tag's "Moreover" clause.

theorem exists_iSup_opensRange_specAffineBlowupι_affineChart
    {X X' W : AlgebraicSpaces B S hS} {Z : ClosedSubspaces B S hS X.obj}
    {b : X' ⟶ X} (hb : IsBlowupAlong B S hS Z b)
    (V : BigFppfOver B S hS) [IsAffine ((BigFppfOver.toScheme B S hS).obj V)]
    {a : schemeSpace V ⟶ X} (ha : IsEtale B S hS a.hom)
    (hcU : B.Contains (reesChartSituation (centreIdeal (preimageClosedSubspace a Z))
      (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)).relativeProj)
    (hcR : B.Contains (reesRelationSituation (centreIdeal (preimageClosedSubspace a Z))
      (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)).relativeProj)
    (hcRR : B.Contains (reesDoubleSituation (centreIdeal (preimageClosedSubspace a Z))
      (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)).relativeProj)
    {q : W ⟶ schemeSpace V} {r : W ⟶ X'} (sq : IsPullback q r a b)
    (I : Ideal ↥Γ((BigFppfOver.toScheme B S hS).obj V,
      (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)).1))
    (hI : (reesChartIdeal (centreIdeal (preimageClosedSubspace a Z))
        (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)).ideal
        (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)) = I) :
    ∃ e : W ≅ schemeSpace (reesProjChart (centreIdeal (preimageClosedSubspace a Z))
        (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V) hcU),
      e.hom ≫ schemeSpaceMap (reesProjChartHom (centreIdeal (preimageClosedSubspace a Z))
          (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V) hcU) = q ∧
      ∃ f : AlgebraicGeometry.Proj (Stacks.Blowup.reesGrading I) ≅
          (BigFppfOver.toScheme B S hS).obj
            (reesProjChart (centreIdeal (preimageClosedSubspace a Z))
              (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V) hcU),
        (f.hom ≫ (BigFppfOver.toScheme B S hS).map
            (reesProjChartHom (centreIdeal (preimageClosedSubspace a Z))
              (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V) hcU) =
          Stacks.Blowup.toSpec I ≫
            (Stacks.RelativeProj.isAffineOpen (Stacks.Blowup.topAffineOpen
              ((BigFppfOver.toScheme B S hS).obj V))).isoSpec.inv ≫
              (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)).1.ι) ∧
        (∀ c : I, _root_.AlgebraicGeometry.IsOpenImmersion
            (Stacks.Blowup.specAffineBlowupι I (c : _) c.2 ≫ f.hom)) ∧
          ⨆ c : I, (Stacks.Blowup.specAffineBlowupι I (c : _) c.2 ≫ f.hom).opensRange = ⊤

AlgebraicGeometry.Space.exists_iso_proj_reesGrading_affineChart_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupAffineChartReesUnconditional.lean, line 126. The attribute's comment: “the canonical isomorphism clause: for an affine scheme U = Spec A of the site étale over X, the fibre product U ×_X X' is the scheme Proj of the Rees algebra of the ideal I of A corresponding to the restriction of the centre's defining sheaf of ideals, by an isomorphism over U; the blowup b is named by the universal property of Stacks 085U; there are no side conditions, the three B.Contains conditions on the relative Projs of the chart's own presentation being proved here from the Rees size bound; the tag's affine open covering clause is a separate registration”.

Stacks 085R, the canonical isomorphism. Let S be a scheme, let X be an algebraic space over S, let Z ⊆ X be a closed subspace with quasi-coherent defining sheaf of ideals ℐ ⊆ 𝒪_X and let b : X' ⟶ X be the blowup of X in Z. Let U = Spec A be an affine scheme of the site étale over X and let I ⊆ A be the ideal corresponding to ℐ|_U. Then U ×_X X' is a scheme, and it is canonically isomorphic over U to the homogeneous spectrum Proj(⨁_{d ≥ 0} Iᵈ) of the Rees algebra of I in A.

The first isomorphism exhibits the fibre product as the algebraic space of a scheme of the site, namely the relative Proj P_U of the Rees algebra of ℐ|_U, compatibly with the projections to U; the second identifies that scheme over U with Proj of the Rees algebra of I, where I is the ideal of sections of ℐ|_U over A, which is the defining ideal of the centre on the chart by AlgebraicGeometry.Space.reesChartIdeal_selfPresentation_eq_ofIdealTop.

theorem exists_iso_proj_reesGrading_affineChart_unconditional
    {X X' W : AlgebraicSpaces B S hS} {Z : ClosedSubspaces B S hS X.obj}
    {b : X' ⟶ X} (hb : IsBlowupAlong B S hS Z b)
    (V : BigFppfOver B S hS) [IsAffine ((BigFppfOver.toScheme B S hS).obj V)]
    {a : schemeSpace V ⟶ X} (ha : IsEtale B S hS a.hom)
    {q : W ⟶ schemeSpace V} {r : W ⟶ X'} (sq : IsPullback q r a b)
    (I : Ideal ↥Γ((BigFppfOver.toScheme B S hS).obj V,
      (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)).1))
    (hI : (reesChartIdeal (centreIdeal (preimageClosedSubspace a Z))
        (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)).ideal
        (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)) = I) :
    ∃ e : W ≅ schemeSpace (reesProjChart (centreIdeal (preimageClosedSubspace a Z))
        (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)
        (contains_relativeProj_reesChartSituation_selfPresentation Z V a)),
      e.hom ≫ schemeSpaceMap (reesProjChartHom (centreIdeal (preimageClosedSubspace a Z))
          (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)
          (contains_relativeProj_reesChartSituation_selfPresentation Z V a)) = q ∧
      ∃ f : AlgebraicGeometry.Proj (Stacks.Blowup.reesGrading I) ≅
          (BigFppfOver.toScheme B S hS).obj
            (reesProjChart (centreIdeal (preimageClosedSubspace a Z))
              (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)
              (contains_relativeProj_reesChartSituation_selfPresentation Z V a)),
        f.hom ≫ (BigFppfOver.toScheme B S hS).map
            (reesProjChartHom (centreIdeal (preimageClosedSubspace a Z))
              (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)
              (contains_relativeProj_reesChartSituation_selfPresentation Z V a)) =
          Stacks.Blowup.toSpec I ≫
            (Stacks.RelativeProj.isAffineOpen (Stacks.Blowup.topAffineOpen
              ((BigFppfOver.toScheme B S hS).obj V))).isoSpec.inv ≫
              (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)).1.ι

AlgebraicGeometry.Space.exists_iSup_opensRange_specAffineBlowupι_affineChart_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupAffineChartReesUnconditional.lean, line 175. The attribute's comment: “the affine open covering clause: the scheme U ×_X X' is covered by the images of the open immersions Spec A[I/a] ⟶ U ×_X X', a ∈ I, out of the spectra of the affine blowup algebras; same hypotheses as the canonical-isomorphism clause and, like it, no side conditions”.

Stacks 085R, the affine open covering. In the situation of AlgebraicGeometry.Space.exists_iso_proj_reesGrading_affineChart_unconditional, the scheme representing U ×_X X' has an affine open covering by the spectra of the affine blowup algebras A[I/a], a ∈ I: the morphisms Spec A[I/a] ⟶ U ×_X X' obtained by composing the standard chart Stacks.Blowup.specAffineBlowupι with the identification of the previous theorem -- the same isomorphism over U, whose compatibility with the projections to U is restated here -- are open immersions whose images have supremum the whole space.

The sources of the covering morphisms are the spectra of the affine blowup algebras Stacks.Blowup.affineBlowup I a by construction, so this is the tag's "Moreover" clause.

theorem exists_iSup_opensRange_specAffineBlowupι_affineChart_unconditional
    {X X' W : AlgebraicSpaces B S hS} {Z : ClosedSubspaces B S hS X.obj}
    {b : X' ⟶ X} (hb : IsBlowupAlong B S hS Z b)
    (V : BigFppfOver B S hS) [IsAffine ((BigFppfOver.toScheme B S hS).obj V)]
    {a : schemeSpace V ⟶ X} (ha : IsEtale B S hS a.hom)
    {q : W ⟶ schemeSpace V} {r : W ⟶ X'} (sq : IsPullback q r a b)
    (I : Ideal ↥Γ((BigFppfOver.toScheme B S hS).obj V,
      (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)).1))
    (hI : (reesChartIdeal (centreIdeal (preimageClosedSubspace a Z))
        (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)).ideal
        (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)) = I) :
    ∃ e : W ≅ schemeSpace (reesProjChart (centreIdeal (preimageClosedSubspace a Z))
        (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)
        (contains_relativeProj_reesChartSituation_selfPresentation Z V a)),
      e.hom ≫ schemeSpaceMap (reesProjChartHom (centreIdeal (preimageClosedSubspace a Z))
          (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)
          (contains_relativeProj_reesChartSituation_selfPresentation Z V a)) = q ∧
      ∃ f : AlgebraicGeometry.Proj (Stacks.Blowup.reesGrading I) ≅
          (BigFppfOver.toScheme B S hS).obj
            (reesProjChart (centreIdeal (preimageClosedSubspace a Z))
              (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)
              (contains_relativeProj_reesChartSituation_selfPresentation Z V a)),
        (f.hom ≫ (BigFppfOver.toScheme B S hS).map
            (reesProjChartHom (centreIdeal (preimageClosedSubspace a Z))
              (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)
              (contains_relativeProj_reesChartSituation_selfPresentation Z V a)) =
          Stacks.Blowup.toSpec I ≫
            (Stacks.RelativeProj.isAffineOpen (Stacks.Blowup.topAffineOpen
              ((BigFppfOver.toScheme B S hS).obj V))).isoSpec.inv ≫
              (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)).1.ι) ∧
        (∀ c : I, _root_.AlgebraicGeometry.IsOpenImmersion
            (Stacks.Blowup.specAffineBlowupι I (c : _) c.2 ≫ f.hom)) ∧
          ⨆ c : I, (Stacks.Blowup.specAffineBlowupι I (c : _) c.2 ≫ f.hom).opensRange = ⊤

Tag 085S, a lemma

Tag 085S in the Stacks Project.

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

Stacks 085S. Let g : X₁ ⟶ X₂ be a flat morphism of algebraic spaces over S, let Z₂ ⊆ X₂ be a closed subspace and let b₂ : X₂' ⟶ X₂ be the blowup of X₂ in Z₂. Then for any cartesian square with legs q : W ⟶ X₁ and r : W ⟶ X₂' over g and b₂, the projection q is the blowup of X₁ in the inverse image of Z₂.

So the square expressing W = X₁ ×_{X₂} X₂' is the cartesian square of the source, with W = X₁'.

Flatness enters only to see that the inverse image of the centre in W — which is the inverse image along r of the exceptional divisor of b₂ — is an effective Cartier divisor; the universal property of q holds for an arbitrary g.

theorem isBlowupAlong_preimage_of_isPullback_of_isFlat
    {X₁ X₂ X₂' W : AlgebraicSpaces B S hS} {g : X₁ ⟶ X₂} (hg : IsFlat B S hS g.hom)
    {Z₂ : ClosedSubspaces B S hS X₂.1} {b₂ : X₂' ⟶ X₂}
    (hb₂ : IsBlowupAlong B S hS Z₂ b₂) {q : W ⟶ X₁} {r : W ⟶ X₂'}
    (sq : IsPullback q r g b₂) :
    IsBlowupAlong B S hS (preimageClosedSubspace g Z₂) q

AlgebraicGeometry.Space.isBlowupAlong_pullbackFst_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupFlatBaseChange.lean, line 159.

Stacks 085S for the chosen fibre product. The first projection of the fibre product X₁ ×_{X₂} X₂' of a flat morphism g : X₁ ⟶ X₂ with the blowup b₂ : X₂' ⟶ X₂ of X₂ in a closed subspace Z₂ is the blowup of X₁ in the inverse image of Z₂.

theorem isBlowupAlong_pullbackFst_of_isFlat
    {X₁ X₂ X₂' : AlgebraicSpaces B S hS} {g : X₁ ⟶ X₂} (hg : IsFlat B S hS g.hom)
    {Z₂ : ClosedSubspaces B S hS X₂.1} {b₂ : X₂' ⟶ X₂}
    (hb₂ : IsBlowupAlong B S hS Z₂ b₂) :
    IsBlowupAlong B S hS (preimageClosedSubspace g Z₂) (pullback.fst g b₂)

AlgebraicGeometry.Space.exists_isPullback_blowup_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupFlatBaseChange.lean, line 183.

Stacks 085S in the source's phrasing. For a flat morphism g : X₁ ⟶ X₂ of algebraic spaces over S, a closed subspace Z₂ ⊆ X₂ with inverse image Z₁ ⊆ X₁, the blowup b₁ : X₁' ⟶ X₁ of X₁ in Z₁ and the blowup b₂ : X₂' ⟶ X₂ of X₂ in Z₂, there is a morphism X₁' ⟶ X₂' making the square

X₁' ⟶ X₂'
 ↓      ↓
X₁ ⟶  X₂

cartesian.

The fibre product X₁ ×_{X₂} X₂' is a blowup of X₁ in Z₁ by AlgebraicGeometry.Space.isBlowupAlong_pullbackFst_of_isFlat, and any two blowups of X₁ in Z₁ are isomorphic over X₁, so X₁' is itself a fibre product.

theorem exists_isPullback_blowup_of_isFlat
    {X₁ X₂ X₁' X₂' : AlgebraicSpaces B S hS} {g : X₁ ⟶ X₂} (hg : IsFlat B S hS g.hom)
    {Z₂ : ClosedSubspaces B S hS X₂.1} {b₂ : X₂' ⟶ X₂}
    (hb₂ : IsBlowupAlong B S hS Z₂ b₂) {b₁ : X₁' ⟶ X₁}
    (hb₁ : IsBlowupAlong B S hS (preimageClosedSubspace g Z₂) b₁) :
    ∃ m : X₁' ⟶ X₂', IsPullback b₁ m g b₂

Tag 085T, a lemma

Tag 085T in the Stacks Project.

AlgebraicGeometry.Space.isEffectiveCartierDivisor_exceptionalDivisor_blowUpAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupExceptionalCartier.lean, line 124. The attribute's comment: “part (2), the exceptional divisor b⁻¹(Z) of the blowup of an algebraic space along a closed subspace is an effective Cartier divisor on the blowup”.

Stacks 085T part (2). Let X be an algebraic space over a scheme S, let Z ⊆ X be a closed subspace and let b : X' ⟶ X be the blowing up of X along Z of Stacks 085Q, the relative Proj of the Rees algebra ⨁_{n ≥ 0} 𝓘_Zⁿ. Then the exceptional divisor b⁻¹(Z) is an effective Cartier divisor on X'.

By Stacks 083C (2) ⟹ (1) it is enough to see this on one surjective étale scheme chart of X', and the construction supplies one: the relative Proj P_U of the Rees algebra on the presenting scheme U of the étale presentation, whose composite with b is P_U ⟶ U ⟶ X. The inverse image of b⁻¹(Z) there is therefore the inverse image along P_U ⟶ U of the closed subscheme Z ×_X U of U, whose ideal sheaf is the sheaf of ideals 𝓘_Z|_U the Rees algebra is formed from, and for a scheme that inverse image is an effective Cartier divisor by Stacks 02OS (2).

The parameters hcU, hcR and heq are the ones the blowup of Stacks 085Q is built from: two containment conditions on the big fppf site and the normalisation and cocycle conditions making the two projections of the relative Projs an internal equivalence relation.

theorem isEffectiveCartierDivisor_exceptionalDivisor_blowUpAlong :
    IsEffectiveCartierDivisor B S hS (blowUpAlong Z P hcU hcR heq)
      (exceptionalDivisor Z P hcU hcR heq)

AlgebraicGeometry.Space.IsBlowupAlong.isIso_and_isEffectiveCartierDivisor_and_twist_neg_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupExceptionalTwist.lean, line 209. The attribute's comment: “all three parts, for any blowup b of X in a closed subspace Z in the sense of the Stacks 085U universal property: (1) b is an isomorphism over the complement of Z, (2) the exceptional divisor is an effective Cartier divisor, (3) O(E) = O(-1), read as in Stacks 084D on every affine scheme V etale over X, where V x_X X' = Proj of the Rees algebra (Stacks 085R) and the base change of O(E) is the twist O(-1); no other hypothesis”.

Stacks 085T. Let S be a scheme, let X be an algebraic space over S, let Z ⊆ X be a closed subspace and let b : X' ⟶ X be the blowing up of X in Z, in the sense of the universal property of Stacks 085U. Then

1. the restriction b⁻¹(X ∖ Z) ⟶ X ∖ Z of b is an isomorphism;
2. the exceptional divisor E = b⁻¹(Z) is an effective Cartier divisor on X';
3. 𝒪_{X'}(E) = 𝒪_{X'}(-1): for every affine scheme V = Spec A étale over X, with I ⊆ A the ideal of Z on V, the fibre product V ×_X X' is identified over V with the scheme Proj(⨁_{d ≥ 0} Iᵈ) (by e and f, as in Stacks 085R), and under that identification the base change of the invertible sheaf 𝒪_{X'}(E) of Stacks 0841 is the twist 𝒪(-1).

Part (3) is the characterization of the twists of the relative Proj in Stacks 084D (their base change to schemes over X are the twists of Stacks 01NR), applied to the affine schemes étale over X, which cover it.

theorem isIso_and_isEffectiveCartierDivisor_and_twist_neg_one
    {X X' : AlgebraicSpaces B S hS} {Z : ClosedSubspaces B S hS X.1} {b : X' ⟶ X}
    (hb : IsBlowupAlong B S hS Z b) :
    IsIso ((openComplementOfClosedSubspace B S hS X Z).1.fromPreimage b.hom) ∧
      IsEffectiveCartierDivisor B S hS X' (preimageClosedSubspace b Z) ∧
      ∀ (V : BigFppfOver B S hS) [IsAffine ((BigFppfOver.toScheme B S hS).obj V)]
        (a : schemeSpace V ⟶ X), IsEtale B S hS a.hom →
        ∀ (I : Ideal ↥Γ((BigFppfOver.toScheme B S hS).obj V,
            (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)).1)),
          (reesChartIdeal (centreIdeal (preimageClosedSubspace a Z))
            (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)).ideal
            (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)) = I →
        ∀ {W : AlgebraicSpaces B S hS} {q : W ⟶ schemeSpace V} {r : W ⟶ X'},
          IsPullback q r a b →
        ∃ e : W ≅ schemeSpace (reesProjChart (centreIdeal (preimageClosedSubspace a Z))
            (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)
            (contains_relativeProj_reesChartSituation_selfPresentation Z V a)),
          e.hom ≫ schemeSpaceMap (reesProjChartHom (centreIdeal (preimageClosedSubspace a Z))
              (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)
              (contains_relativeProj_reesChartSituation_selfPresentation Z V a)) = q ∧
          ∃ f : AlgebraicGeometry.Proj (Stacks.Blowup.reesGrading I) ≅
              (BigFppfOver.toScheme B S hS).obj
                (reesProjChart (centreIdeal (preimageClosedSubspace a Z))
                  (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)
                  (contains_relativeProj_reesChartSituation_selfPresentation Z V a)),
            f.hom ≫ (BigFppfOver.toScheme B S hS).map
                (reesProjChartHom (centreIdeal (preimageClosedSubspace a Z))
                  (isCartesianOnAffineCharts_centreIdeal _) (selfPresentation B S hS V)
                  (contains_relativeProj_reesChartSituation_selfPresentation Z V a)) =
              Stacks.Blowup.toSpec I ≫
                (Stacks.RelativeProj.isAffineOpen (Stacks.Blowup.topAffineOpen
                  ((BigFppfOver.toScheme B S hS).obj V))).isoSpec.inv ≫
                  (Stacks.Blowup.topAffineOpen ((BigFppfOver.toScheme B S hS).obj V)).1.ι ∧
            Nonempty ((Scheme.Modules.pullback f.hom).obj
                (baseChangeModule B S hS (associatedInvertibleSheaf B S hS X'
                  (preimageClosedSubspace b Z) hb.isPullbackDefined) _ (e.inv ≫ r).hom) ≅
              twistingSheaf (Stacks.Blowup.reesGrading I) (-1))

AlgebraicGeometry.Space.isIso_fromPreimage_openComplement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupIsomorphismOffCentre.lean, line 200. The attribute's comment: “part (1): the blowup is an isomorphism away from the centre”.

Stacks 085T, part (1). The blowup b : X' ⟶ X of an algebraic space X in a closed subspace Z is an isomorphism over the open complement of Z: the restriction b⁻¹(X ∖ Z) ⟶ X ∖ Z of b is an isomorphism.

Both X ∖ Z and b⁻¹(X ∖ Z) are algebraic spaces over X on which the inverse image of Z has no points, hence is an effective Cartier divisor, so each admits a unique morphism to X' over X by the universal property of Stacks 085U. The morphism out of X ∖ Z lands in b⁻¹(X ∖ Z) and is inverse to the restriction of b, the two composites being identified with the identities by the uniqueness of those lifts.

theorem isIso_fromPreimage_openComplement {X X' : AlgebraicSpaces B S hS}
    {Z : ClosedSubspaces B S hS X.1} {b : X' ⟶ X} (hb : IsBlowupAlong B S hS Z b) :
    IsIso ((openComplementOfClosedSubspace B S hS X Z).1.fromPreimage b.hom)

AlgebraicGeometry.Space.blowUpTwistSpaceNegOneIsoAssociatedInvertibleSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupTwistDescentCanonical.lean, line 869. The attribute's comment: “part (3): the canonical isomorphism O_{X'}(-1) = O_{X'}(E) on the blowup of an algebraic space, O_{X'}(1) being descended along the unique transition compatible with the canonical map O(1) → O”. References: EGA II (8.1.8), “partial”.

Stacks 085T, part (3): the canonical isomorphism 𝒪_{X'}(-1) ≅ 𝒪_{X'}(E). Let b : X' ⟶ X be the blowing up of an algebraic space X along a closed subspace Z (Stacks 085Q, AlgebraicGeometry.Space.blowUpAlong', with the equivalence-relation field of its descent datum discharged by AlgebraicGeometry.Space.isEquivalenceRelation_post_reesProj), with exceptional divisor E = b⁻¹(Z), an effective Cartier divisor by part (2). Then the twisting sheaf 𝒪_{X'}(-1) is isomorphic to the invertible sheaf 𝒪_{X'}(E) of Stacks 0841 (1).

Here 𝒪_{X'}(n) is the nth tensor power (Stacks 01CU) of the invertible sheaf 𝒪_{X'}(1) obtained by descending, along the étale presentation P_R ⇉ P_U of X' and the equivalence of Stacks 03M3, the twisting sheaf 𝒪_{P_U}(1) of the blowup P_U of the presenting scheme U in 𝓘_Z|_U, with transition morphism α' (AlgebraicGeometry.Space.blowUpTwistDescentDatum).

Why the isomorphism is canonical. The descent datum of 𝒪_{X'}(1) is characterised without reference to E (AlgebraicGeometry.Space.eq_blowUpTwistDescentDatum_alpha_iff): a morphism β : t^*𝒪_{P_U}(1)^a ⟶ s^*𝒪_{P_U}(1)^a is the transition α' if and only if β ≫ s^*c = t^*c ≫ α_𝒪, where α_𝒪 is the canonical descent datum of 𝒪_{X'} and c = (blowUpChartTwistOneToUnit)^a ≫ u⁻¹, built from the canonical map 𝒪(1) ⟶ 𝒪 of the scheme blowup P_U (AlgebraicGeometry.Space.blowUpChartTwistOneToUnit: Stacks 02OS (3) followed by the inclusion into 𝒪, which on the standard chart at a ∈ 𝓘(U) is t ↦ (t / a⁽¹⁾) · b^♯(a), the map induced by the shift A(1) ⟶ A of the Rees algebra, AlgebraicGeometry.incl_app_twistOneIsoExceptionalIdealModule_hom) and the identification u : φ^*𝒪_{X'} ≅ 𝒪_{P_U}^a of AlgebraicGeometry.Space.modulePullbackPresentationAtlasUnitIso, built from 𝒪 alone. That lemma combines the uniqueness of the transition (AlgebraicGeometry.Space.eq_blowUpTwistDescentDatum_alpha), its computation at the atlas (AlgebraicGeometry.Space.blowUpAtlasMapComputes_idealSheaf) and on the chart (AlgebraicGeometry.Space.blowUpChartTwistOneIsoIdealSheaf_hom_comp_ι). So 𝒪_{X'}(1) is the descent of 𝒪_{P_U}(1) along the unique datum compatible with 𝒪(1) ⟶ 𝒪, and the isomorphism below is AlgebraicGeometry.Space.blowUpTwistSpaceNegOneIso, the inverse of the descended 𝒪_{X'}(1) ≅ 𝓘_E of Stacks 02OS (3).

The parameters hcU, hcR and hcRR are the containment conditions on the big fppf site under which the relative Projs of the blowup are objects of the site.

def blowUpTwistSpaceNegOneIsoAssociatedInvertibleSheaf (Z : ClosedSubspaces B S hS X.obj)
    (P : Presentation B S hS X.obj X.property)
    (hcU : B.Contains (reesChartSituation (centreIdeal Z)
      (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    (hcR : B.Contains (reesRelationSituation (centreIdeal Z)
      (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    (hcRR : B.Contains (reesDoubleSituation (centreIdeal Z)
      (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj) :
    blowUpTwistSpace Z P hcU hcR (isEquivalenceRelation_post_reesProj (centreIdeal Z)
        (isCartesianOnAffineCharts_centreIdeal Z) P hcU hcR hcRR) (-1) ≅
      associatedInvertibleSheaf B S hS (blowUpAlong Z P hcU hcR
          (isEquivalenceRelation_post_reesProj (centreIdeal Z)
            (isCartesianOnAffineCharts_centreIdeal Z) P hcU hcR hcRR))
        (exceptionalDivisor Z P hcU hcR (isEquivalenceRelation_post_reesProj (centreIdeal Z)
          (isCartesianOnAffineCharts_centreIdeal Z) P hcU hcR hcRR))
        (isEffectiveCartierDivisor_exceptionalDivisor_blowUpAlong Z P hcU hcR
          (isEquivalenceRelation_post_reesProj (centreIdeal Z)
            (isCartesianOnAffineCharts_centreIdeal Z) P hcU hcR hcRR))

Tag 085U, a lemma

Tag 085U in the Stacks Project.

AlgebraicGeometry.Space.isBlowupAlong_blowUpAlongHom', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupFinality.lean, line 441. The attribute's comment: “the blowup of an algebraic space along a closed subspace is a final object of the category of those Y over X whose inverse image of the centre is an effective Cartier divisor; both halves, membership and finality”.

Stacks 085U. The blowing up b : X' ⟶ X of an algebraic space X along a closed subspace Z ⊆ X is a final object of the category 𝒞 of algebraic spaces over X on which the inverse image of Z is an effective Cartier divisor.

Membership in 𝒞 is AlgebraicGeometry.Space.isEffectiveCartierDivisor_exceptionalDivisor' and finality is AlgebraicGeometry.Space.existsUnique_hom_blowUpAlong'; the two are assembled by AlgebraicGeometry.Space.isBlowupAlong_of_existsUnique_lift. The hypotheses are exactly the data the construction of Tag 085Q itself takes — an étale presentation P of X, the universe choice HasSheafify for the quotient presheaf, and the three B.Contains side conditions on the relative Projs which AlgebraicGeometry.Space.relativeProjChartOfSituation already asks for; nothing is assumed about Z beyond being a closed subspace, and in particular no separatedness or density input is used.

This declaration alone carries Tag 085U. Both halves are recovered from it by projection — membership as AlgebraicGeometry.Space.IsBlowupAlong.isPullbackDefined, which is AlgebraicGeometry.Space.isEffectiveCartierDivisor_exceptionalDivisor' up to unfolding AlgebraicGeometry.Space.exceptionalDivisor', and finality as AlgebraicGeometry.Space.IsBlowupAlong.existsUnique_lift, which is AlgebraicGeometry.Space.existsUnique_lift_blowUpAlongHom' — so neither of those two is registered.

theorem isBlowupAlong_blowUpAlongHom' :
    IsBlowupAlong B S hS Z (blowUpAlongHom' Z P hcU hcR hcRR)

Tag 085V, a lemma

Tag 085V in the Stacks Project.

AlgebraicGeometry.Space.isBlowupAlong_id_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupOfEffectiveCartierDivisor.lean, line 92.

Stacks 085V. Let S be a scheme, let X be an algebraic space over S and let Z ⊆ X be an effective Cartier divisor. The blowup of X in Z is the identity morphism of X.

Being the blowup of X in Z is the universal property of Tag 085U, which AlgebraicGeometry.Space.IsBlowupAlong records: terminality in the category 𝒞 of algebraic spaces over X on which the inverse image of Z is an effective Cartier divisor. The identity of X is an object of 𝒞 precisely because Z is an effective Cartier divisor, and it is terminal in 𝒞 because it is already terminal in all of Spaces/X and 𝒞 is a full subcategory. Since terminal objects are unique up to unique isomorphism over X, this says that the blowup of X in Z exists and is the identity of X; see AlgebraicGeometry.Space.IsBlowupAlong.isIso_of_isEffectiveCartierDivisor.

theorem isBlowupAlong_id_of_isEffectiveCartierDivisor (X : AlgebraicSpaces B S hS)
    (Z : ClosedSubspaces B S hS X.1) (hZ : IsEffectiveCartierDivisor B S hS X Z) :
    IsBlowupAlong B S hS Z (𝟙 X)

Tag 085W, a lemma

Tag 085W in the Stacks Project.

AlgebraicGeometry.Space.isReduced_of_isBlowupAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupReduced.lean, line 120. The attribute's comment: “given the étale-chart representability of the blowup supplied by Stacks 085Q”.

Stacks 085W, with the étale-chart representability of Stacks 085Q carried as a hypothesis.

Let X be a reduced algebraic space over S, let Z ⊆ X be the closed subspace cut out by a quasi-coherent sheaf of ideals and let b : X' ⟶ X be the blowup of X in Z. Then X' is reduced.

The chart datum is the source's: a surjective étale morphism a : U ⟶ X from a scheme U of the site, and the fibre product W = U ×_X X' as a cartesian square. The hypothesis hrep supplies what Stacks 085Q would: some blowup of U in the inverse image of Z is representable by a scheme isomorphic to a scheme blowup of U. See the module documentation for why that hypothesis is upstream of this conclusion.

theorem isReduced_of_isBlowupAlong
    {X X' W : AlgebraicSpaces B S hS} {Z : ClosedSubspaces B S hS X.1} {b : X' ⟶ X}
    (hb : IsBlowupAlong B S hS Z b)
    (hX : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsReduced T))
    (V : BigFppfOver B S hS) (a : schemeSpace V ⟶ X)
    (haE : IsEtale B S hS a.hom) (haS : IsSurjective B S hS a.hom)
    {q : W ⟶ schemeSpace V} {r : W ⟶ X'} (sq : IsPullback q r a b)
    (hrep : ∃ (Y : AlgebraicSpaces B S hS) (p : Y ⟶ schemeSpace V),
      IsBlowupAlong B S hS (preimageClosedSubspace a Z) p ∧
      ∃ (V' : BigFppfOver B S hS) (_ : Y.1 ≅ yoneda.obj V')
        (I : ((BigFppfOver.toScheme B S hS).obj V).IdealSheafData),
        Nonempty ((BigFppfOver.toScheme B S hS).obj V' ≅ blowUp I)) :
    HasEtaleLocalProperty B S hS X'.1 (fun T : Scheme.{u} => IsReduced T)

AlgebraicGeometry.Space.isReduced_of_isBlowupAlong_of_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupReducedPresentation.lean, line 90. The attribute's comment: “the blowup of a reduced algebraic space in a closed subspace is reduced, with no assumed inputs beyond the Stacks 085Q construction data — the étale presentation P of the space, the HasSheafify universe choice for the quotient presheaf, and the three B.Contains size conditions on the relative Projs of the chart, relation and double situations — none of which occurs in the conclusion”.

Stacks 085W. Let X be an algebraic space over S and let Z ⊆ X be the closed subspace cut out by a quasi-coherent sheaf of ideals. If X is reduced then so is the blowup b : X' ⟶ X of X in Z.

Nothing about the blowup is assumed beyond its universal property, Stacks 085U: the étale chart of X' the proof runs on is the one the construction of Stacks 085Q supplies, namely the relative Proj P_U of the Rees algebra of the chart ideal on the presenting scheme U of the presentation P. That scheme is the blowup of the scheme U, by Stacks.Blowup.reesSituationBlowUpIso, so it is reduced by Stacks 0808; P_U ⟶ X' is surjective étale, so Stacks 06MI carries reducedness to the constructed blowup, and from there to b along the isomorphism of any two blowups in the same centre.

Besides Z, the blowup b and reducedness of X the statement takes only the data the construction of Stacks 085Q itself takes: the presentation P, the universe choice HasSheafify for the quotient presheaf, and the three B.Contains side conditions on the relative Projs which AlgebraicGeometry.Space.relativeProjChartOfSituation already asks for. None of that appears in the conclusion.

theorem isReduced_of_isBlowupAlong_of_presentation
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    {X X' : AlgebraicSpaces B S hS} (Z : ClosedSubspaces B S hS X.obj)
    (P : Presentation B S hS X.obj X.property)
    (hcU : B.Contains (reesChartSituation (centreIdeal Z)
        (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    (hcR : B.Contains (reesRelationSituation (centreIdeal Z)
        (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    (hcRR : B.Contains (reesDoubleSituation (centreIdeal Z)
        (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    {b : X' ⟶ X} (hb : IsBlowupAlong B S hS Z b)
    (hX : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsReduced T)) :
    HasEtaleLocalProperty B S hS X'.1 (fun T : Scheme.{u} => IsReduced T)

Tag 0BH1, a lemma

Tag 0BH1 in the Stacks Project.

AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_of_isBlowupAlong_of_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupLocallyFiniteIrreducibleComponents.lean, line 127. The attribute's comment: “the blowup of an algebraic space satisfying the equivalent conditions of Stacks 0BB1 in a closed subspace satisfies them too, with no assumed inputs beyond the Stacks 085Q construction data for the centre -- a presentation P, the HasSheafify universe choice, and the three B.Contains side conditions hcU, hcR and hcRR on the relative Projs -- none of which occurs in the conclusion”.

Stacks 0BH1. Let X be an algebraic space over S and let Z ⊆ X be the closed subspace cut out by a quasi-coherent sheaf of ideals. If X satisfies the equivalent conditions of Stacks 0BB1 — here its condition (2), AlgebraicGeometry.Space.HasLocallyFiniteIrreducibleComponents — then so does the blowup b : X' ⟶ X of X in Z.

Nothing about the blowup is assumed beyond its universal property, Stacks 085U: the étale chart of X' the proof runs on is the one the construction of Stacks 085Q supplies, namely the relative Proj P_U of the Rees algebra of the chart ideal on the presenting scheme U of the presentation P. That scheme is the blowup of the scheme U, by Stacks.Blowup.reesSituationBlowUpIso, so every quasi-compact open of it has finitely many irreducible components by AlgebraicGeometry.finite_irreducibleComponents_of_isCompact_blowUp; P_U ⟶ X' is surjective étale, so conditions (1) and (2) of Stacks 0BB1 carry the condition to the constructed blowup, and from there to b along the isomorphism of any two blowups in the same centre.

Besides Z, the blowup b and the hypothesis on X the statement takes only the data the construction of Stacks 085Q itself takes: the presentation P, the universe choice HasSheafify for the quotient presheaf, and the three B.Contains side conditions on the relative Projs which AlgebraicGeometry.Space.relativeProjChartOfSituation already asks for. None of that appears in the conclusion.

theorem hasLocallyFiniteIrreducibleComponents_of_isBlowupAlong_of_presentation
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    {X X' : AlgebraicSpaces B S hS} (Z : ClosedSubspaces B S hS X.obj)
    (P : Presentation B S hS X.obj X.property)
    (hcU : B.Contains (reesChartSituation (centreIdeal Z)
        (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    (hcR : B.Contains (reesRelationSituation (centreIdeal Z)
        (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    (hcRR : B.Contains (reesDoubleSituation (centreIdeal Z)
        (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    {b : X' ⟶ X} (hb : IsBlowupAlong B S hS Z b)
    (hX : HasLocallyFiniteIrreducibleComponents B S hS X.1) :
    HasLocallyFiniteIrreducibleComponents B S hS X'.1

Tag 085X, a lemma

Tag 085X in the Stacks Project.

AlgebraicGeometry.Space.isPullbackDefined_blowUpAlongHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupDivisorPullback.lean, line 203. The attribute's comment: “for the blowup of Stacks 085Q: with no assumed inputs beyond the construction data P, hcU, hcR and heq naming the blowup, every effective Cartier divisor on an algebraic space has a defined pullback along it”.

Stacks 085X. Let X be an algebraic space over a scheme S, let Z ⊆ X be a closed subspace and let b : X' ⟶ X be the blowing up of X along Z of Stacks 085Q. Then for every effective Cartier divisor D on X the pullback b⁻¹(D) is defined in the sense of Stacks 083Y: the inverse image of D along b is again an effective Cartier divisor, on X'.

By Stacks 083C (2) ⟹ (1) it is enough to see this on one surjective étale scheme chart of X', and the construction supplies one: the relative Proj P_U of the Rees algebra of 𝓘_Z|_U on the presenting scheme U of the étale presentation, whose composite with b is P_U ⟶ U ⟶ X. The inverse image of b⁻¹(D) there is therefore the inverse image along P_U ⟶ U of the closed subscheme D ×_X U of U, which is an effective Cartier divisor on U by Stacks 083C (1) ⟹ (3); and for a scheme the inverse image of an effective Cartier divisor along a blowup is an effective Cartier divisor by Stacks 0809.

The parameters P, hcU, hcR and heq are the ones the blowup of Stacks 085Q is built from and only name the blowup; the hypothesis on D is the source's own.

theorem isPullbackDefined_blowUpAlongHom (D : ClosedSubspaces B S hS X.obj)
    (hD : IsEffectiveCartierDivisor B S hS X D) :
    IsPullbackDefined B S hS (blowUpAlongHom Z P hcU hcR heq) D

AlgebraicGeometry.Space.isPullbackDefined_of_isBlowupAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupDivisorPullback.lean, line 266. The attribute's comment: “the source statement, for any b which is a blowup of X in a closed subspace in the sense of the Stacks 085U universal property; with no assumed inputs apart from the Stacks 085Q construction data P, hcU, hcR and hcRR, which does not occur in the conclusion”.

Stacks 085X, for an arbitrary blowup. Let X be an algebraic space over a scheme S, let Z ⊆ X be a closed subspace and let b : X' ⟶ X be a blowup of X in Z, in the sense of the universal property of Stacks 085U. Then for every effective Cartier divisor D on X the pullback b⁻¹(D) is defined in the sense of Stacks 083Y.

This is the source's statement: nothing distinguishes b beyond being a blowup of X in a closed subspace, and D is an arbitrary effective Cartier divisor. A blowup in a fixed centre is unique up to isomorphism over the base, AlgebraicGeometry.Space.IsBlowupAlong.exists_iso, and the blowup of Stacks 085Q is one, AlgebraicGeometry.Space.isBlowupAlong_blowUpAlongHom' (Stacks 085U); so b is isomorphic over X to the constructed blowup, for which AlgebraicGeometry.Space.isPullbackDefined_blowUpAlongHom gives the conclusion; and that conclusion crosses the isomorphism by AlgebraicGeometry.Space.isPullbackDefined_of_iso_over.

The parameters P, hcU, hcR and hcRR are those of the construction of Stacks 085Q, used only to produce the blowup b is compared against; none of them occurs in the conclusion.

theorem isPullbackDefined_of_isBlowupAlong {X' : AlgebraicSpaces B S hS} {b : X' ⟶ X}
    (hb : IsBlowupAlong B S hS Z b) (D : ClosedSubspaces B S hS X.obj)
    (hD : IsEffectiveCartierDivisor B S hS X D) :
    IsPullbackDefined B S hS b D

AlgebraicGeometry.Space.isPullbackDefined_of_exists_isBlowupAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupDivisorPullbackAnyBlowup.lean, line 49. The attribute's comment: “the full statement, for every morphism b which is a blowup of X in some closed subspace (Stacks 085U universal property) and every effective Cartier divisor D on X; no construction data and no size condition on the site among the hypotheses”.

Stacks 085X. Let S be a scheme, let X be an algebraic space over S and let b : X' ⟶ X be a blowup of X in a closed subspace. Then for every effective Cartier divisor D on X the pullback b⁻¹(D) is defined in the sense of Stacks 083Y: the inverse image of D along b is an effective Cartier divisor on X'.

"A blowup of X in a closed subspace" is ∃ Z, IsBlowupAlong B S hS Z b: b is a final object of the category of algebraic spaces over X on which the inverse image of the closed subspace Z is an effective Cartier divisor (Stacks 085U), so b is isomorphic over X to the blowing up of X along Z of Stacks 085Q.

theorem isPullbackDefined_of_exists_isBlowupAlong {X X' : AlgebraicSpaces B S hS}
    (b : X' ⟶ X) (hb : ∃ Z : ClosedSubspaces B S hS X.1, IsBlowupAlong B S hS Z b) :
    ∀ D : ClosedSubspaces B S hS X.1, IsEffectiveCartierDivisor B S hS X D →
      IsPullbackDefined B S hS b D

Tag 085Y, a lemma

Tag 085Y in the Stacks Project.

AlgebraicGeometry.Space.isBlowupAlong_comp_of_isBlowupAlong', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupComposite.lean, line 218. The attribute's comment: “with no assumed inputs beyond the Stacks 085Q construction data P, hcU, hcR and hcRR for the second centre, which does not occur in the conclusion: for b a blowup of X in Z and b' a blowup of X' in the inverse image of Y, both in the sense of the Stacks 085U universal property, the composite b' followed by b is the blowup of X in the sum Z + Y”.

Stacks 085Y. Let S be a scheme, let X be an algebraic space over S and let Z, Y ⊆ X be closed subspaces. Let b : X' ⟶ X be a blowup of X in Z and let b' : X'' ⟶ X' be a blowup of X' in the inverse image b⁻¹(Y), both in the sense of the universal property of Stacks 085U. Then the composite b' ≫ b is the blowup of X in the sum Z + Y, the closed subspace cut out by the product of the two defining ideals (Stacks 083U).

Read through that universal property, which is how AlgebraicGeometry.Space.IsBlowupAlong says "is the blowup", the conclusion asserts both that the blowup of X in Z + Y exists and that it is b' ≫ b; that is the source's "X'' ⟶ X is canonically isomorphic to the blowing up of X in 𝓘𝓙", and the isomorphism itself is AlgebraicGeometry.Space.exists_iso_blowup_comp_of_isBlowupAlong'.

The hypotheses on the two blowups are the source's own: each is named only by being a blowup of its centre. What is carried beyond them is the construction data of Stacks 085Q for the second centre b⁻¹(Y) — an étale presentation P of X', the HasSheafify universe choice, and the three B.Contains side conditions on the relative Projs which AlgebraicGeometry.Space.relativeProjChartOfSituation already asks for. That data produces the constructed blowup of X' in b⁻¹(Y), which is what Stacks 085X is proved for; none of it occurs in the conclusion, and no input of Stacks 085Y is assumed.

The proof is AlgebraicGeometry.Space.isBlowupAlong_comp_of_isBlowupAlong with its Tag 085X hypothesis discharged by AlgebraicGeometry.Space.isPullbackDefined_of_isBlowupAlong, applied to the effective Cartier divisor b⁻¹(Z) on X' — effective Cartier because b is the blowup of Z, so this is AlgebraicGeometry.Space.IsBlowupAlong.isPullbackDefined of hb.

theorem isBlowupAlong_comp_of_isBlowupAlong'
    {Z Y : ClosedSubspaces B S hS X.1} {b : X' ⟶ X} (hb : IsBlowupAlong B S hS Z b)
    {b' : X'' ⟶ X'} (hb' : IsBlowupAlong B S hS (preimageClosedSubspace b Y) b')
    (P : Presentation B S hS X'.obj X'.property)
    (hcU : B.Contains (reesChartSituation (centreIdeal (preimageClosedSubspace b Y))
      (isCartesianOnAffineCharts_centreIdeal (preimageClosedSubspace b Y)) P).relativeProj)
    (hcR : B.Contains (reesRelationSituation (centreIdeal (preimageClosedSubspace b Y))
      (isCartesianOnAffineCharts_centreIdeal (preimageClosedSubspace b Y)) P).relativeProj)
    (hcRR : B.Contains (reesDoubleSituation (centreIdeal (preimageClosedSubspace b Y))
      (isCartesianOnAffineCharts_centreIdeal (preimageClosedSubspace b Y)) P).relativeProj) :
    IsBlowupAlong B S hS (sumClosedSubspaces B S hS X Z Y) (b' ≫ b)

Tag 085Z, a lemma

Tag 085Z in the Stacks Project.

AlgebraicGeometry.Space.isProper_of_isBlowupAlong_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupPropernessReesChart.lean, line 244. The attribute's comment: “the blowup b : X' -> X of an algebraic space X in a closed subspace Z whose closed immersion is of finite presentation (equivalently, whose quasi-coherent ideal sheaf is of finite type) is a proper morphism, at the source's hypotheses: the relative Proj charts the proof reads are shown to lie in the site by hasReesProjChartInSite_of_isFinitePresentation”.

Stacks 085Z. Let X be an algebraic space over a scheme S and let Z ⊆ X be a closed subspace whose closed immersion is of finite presentation — equivalently, whose quasi-coherent sheaf of ideals 𝓘 is of finite type. Then every blowup b : X' ⟶ X of X in Z (in 𝓘) is a proper morphism.

The source's proof: properness is étale local on the target (Stacks 083R), blowing up commutes with flat base change (Stacks 085S), and over a scheme chart the blowup is proper because 𝓘 is of finite type there (Stacks 02NS, 01WC). That is AlgebraicGeometry.Space.isProper_of_isBlowupAlong_of_hasReesProjChartInSite, applied on the chart of an étale presentation of X, on which the relative Projs the argument reads lie in the site by AlgebraicGeometry.Space.hasReesProjChartInSite_of_isFinitePresentation.

The only argument beyond the source's is the instance HasSheafify for the big fppf topology: the existence of sheafification of Type u-valued presheaves on the site, which this library's construction of blowups of algebraic spaces (Stacks 085Q) and its chart description (Stacks 085R) are stated with.

theorem isProper_of_isBlowupAlong_of_isFinitePresentation (Z : ClosedSubspaces B S hS X.1)
    (b : X' ⟶ X) (hfp : IsFinitePresentation B S hS Z.1.ι) (hb : IsBlowupAlong B S hS Z b) :
    IsProper B S hS b.hom

Tag 0860, a lemma

Tag 0860 in the Stacks Project.

AlgebraicGeometry.Space.exists_isCompositeCentre_isBlowupAlong_of_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupCompositeCentre.lean, line 466.

Stacks 0860. Let S be a scheme and let X be a quasi-compact and quasi-separated algebraic space over S. Let Z ⊆ X be a closed subspace of finite presentation and let b : X' ⟶ X be the blowing up of X in Z. Let Z' ⊆ X' be a closed subspace of finite presentation and let c : X'' ⟶ X' be the blowing up of X' in Z'. Then there exists a closed subspace Y ⊆ X of finite presentation such that |Y| = |Z| ∪ |b|(|Z'|) and c ≫ b : X'' ⟶ X is isomorphic to the blowing up of X in Y.

The blowups are named by their universal property, Stacks 085U (AlgebraicGeometry.Space.IsBlowupAlong), so "isomorphic to the blowing up of X in Y" is IsBlowupAlong B S hS Y (c ≫ b), and |Y| = |Z| ∪ |b|(|Z'|) is AlgebraicGeometry.Space.IsCompositeCentre. Quasi-separatedness of X is absolute quasi-separatedness, which needs the terminal scheme in the site (hZ).

This is AlgebraicGeometry.Space.exists_isCompositeCentre_isBlowupAlong with its second centre supplied by AlgebraicGeometry.Space.hasSecondCentre; see the module documentation for how that replaces the source's appeal to Stacks 085N.

theorem exists_isCompositeCentre_isBlowupAlong_of_isQuasiCompactSpace
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    (hZ : B.Contains (⊤_ Scheme.{u})) (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    {Z : ClosedSubspaces B S hS X.1} {b : X' ⟶ X} (hb : IsBlowupAlong B S hS Z b)
    (hZfp : IsFinitePresentation B S hS Z.1.ι)
    {Z' : ClosedSubspaces B S hS X'.1} {c : X'' ⟶ X'} (hc : IsBlowupAlong B S hS Z' c)
    (hZ'fp : IsFinitePresentation B S hS Z'.1.ι) :
    ∃ Y : ClosedSubspaces B S hS X.1, IsFinitePresentation B S hS Y.1.ι ∧
      IsCompositeCentre B S hS b Z Z' Y ∧ IsBlowupAlong B S hS Y (c ≫ b)

Sources

• Section 71.17, Tag 085P
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.blowUpAlong' · AlgebraicGeometry.Space.blowUpAlongHom' · AlgebraicGeometry.Space.exceptionalDivisor' · AlgebraicGeometry.Space.blowUpAlong · AlgebraicGeometry.Space.blowUpAlongHom · AlgebraicGeometry.Space.exceptionalDivisor · AlgebraicGeometry.Space.exists_iso_proj_reesGrading_affineChart · AlgebraicGeometry.Space.exists_iSup_opensRange_specAffineBlowupι_affineChart

Section71.18 Strict transform#

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

Tag 0862, a definition

Tag 0862 in the Stacks Project.

AlgebraicGeometry.Space.strictTransformSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransform.lean, line 252. The attribute's comment: “strict transform of a module”.

Stacks 0862, part (1). The strict transform of an 𝒪_X-module F along a morphism b : A' ⟶ A relative to a subspace E ⊆ A': pull F back to X ×_A A' along pr_X and divide out the submodule of those sections that are supported on |pr_{A'}^{-1}E|.

Stated for an arbitrary morphism b together with an arbitrary subspace E of its source, this specializes to the strict transform with respect to the blowup of A in a closed subspace Z ⊆ A on taking b that blowup and E = b^{-1}Z its exceptional divisor. Stacks 0862 states the construction for a quasi-coherent F, which is the case it is applied in; the construction itself uses nothing of F, so no quasi-coherence hypothesis is carried here.

Quasi-coherence of the strict transform is not asserted: it would need the preamble of the section containing Stacks 0862 — that E is an effective Cartier divisor, that its preimage is locally principal, and that the complement of the latter has an affine inclusion — none of which is available for algebraic spaces, together with quasi-coherence of a cokernel on the small étale site. See the module documentation.

noncomputable def strictTransformSheaf (E : Subfunctor A'.1)
    (F : Modules.{u, u} B S hS X.1 X.2) :
    Modules.{u, u} B S hS (strictTransformPullback B S hS f b).1
      (strictTransformPullback B S hS f b).2

AlgebraicGeometry.Space.strictTransform, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransform.lean, line 316. The attribute's comment: “strict transform of a space”.

Stacks 0862, part (2). The strict transform of an algebraic space f : X ⟶ A over A along a morphism b : A' ⟶ A relative to a subspace E ⊆ A': the closed subspace of X ×_A A' determined by the ideal of those sections of 𝒪_{X ×_A A'} that are supported on |pr_{A'}^{-1}E|.

Stated for an arbitrary morphism b together with an arbitrary subspace E of its source, this specializes to the strict transform with respect to the blowup of A in a closed subspace Z ⊆ A on taking b that blowup and E = b^{-1}Z its exceptional divisor.

The closed subspace is realized as the infimum of those closed subspaces whose defining ideal is dominated by that ideal of supported sections, which is a closed subspace unconditionally, and which coincides with the closed subspace cut out by the ideal whenever the latter exists, by AlgebraicGeometry.Space.strictTransformSubfunctor_eq_of_definingIdealSheaf_eq.

Quasi-coherence of the defining ideal is not asserted: it would need the preamble of the section containing Stacks 0862 — that E is an effective Cartier divisor, that its preimage is locally principal, and that the complement of the latter has an affine inclusion — none of which is available for algebraic spaces. See the module documentation.

noncomputable def strictTransform (E : Subfunctor A'.1) :
    ClosedSubspaces B S hS (strictTransformPullback B S hS f b).1

Tag 0863, a lemma

Tag 0863 in the Stacks Project.

AlgebraicGeometry.Space.isEtale_baseChange_blowup_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupEtaleLocalization.lean, line 160. The attribute's comment: “part (1): the blowup localizes étale-locally, and the induced morphisms are étale”.

Stacks 0863, part (1). Let Z ⊆ 𝔅 be a closed subspace of an algebraic space over S, let b : 𝔅' ⟶ 𝔅 be the blowup of 𝔅 in Z and let f : X ⟶ 𝔅 be an algebraic space over 𝔅. Let

U ⟶ X
↓     ↓
𝒱 ⟶ 𝔅

be a commutative square with étale horizontal arrows, and let v' : 𝒱' ⟶ 𝒱 be the blowup of 𝒱 in the inverse image Z ×_𝔅 𝒱 of Z. Then:

• 𝒱' = 𝒱 ×_𝔅 𝔅', by a cartesian square over v and b;
• the resulting morphism m : 𝒱' ⟶ 𝔅' is étale;
• the induced morphism U ×_𝒱 𝒱' ⟶ X ×_𝔅 𝔅' is étale.

The first assertion is Stacks 085S applied to v, which is flat because it is étale. The second is the base change of an étale morphism along b. For the third, U ×_𝒱 𝒱' = (X ×_𝔅 𝔅') ×_X U, so the morphism is a base change of the étale morphism u : U ⟶ X.

theorem isEtale_baseChange_blowup_of_isEtale
    {𝔅 X 𝒱 U B' V' W W' : AlgebraicSpaces B S hS}
    {Z : ClosedSubspaces B S hS 𝔅.1} {b : B' ⟶ 𝔅} (hb : IsBlowupAlong B S hS Z b)
    {f : X ⟶ 𝔅} {v : 𝒱 ⟶ 𝔅} (hv : IsEtale B S hS v.hom)
    {u : U ⟶ X} (hu : IsEtale B S hS u.hom) {w : U ⟶ 𝒱} (hcomm : u ≫ f = w ≫ v)
    {v' : V' ⟶ 𝒱} (hv' : IsBlowupAlong B S hS (preimageClosedSubspace v Z) v')
    {pX : W ⟶ X} {pB' : W ⟶ B'} (sq : IsPullback pX pB' f b)
    {qU : W' ⟶ U} {qV' : W' ⟶ V'} (sq' : IsPullback qU qV' w v') :
    ∃ m : V' ⟶ B', IsPullback v' m v b ∧ IsEtale B S hS m.hom ∧
      ∃ can : W' ⟶ W, can ≫ pX = qU ≫ u ∧ can ≫ pB' = qV' ≫ m ∧
        IsEtale B S hS can.hom

AlgebraicGeometry.Space.exists_isEtale_strictTransformSheaf_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupEtaleLocalization.lean, line 241. The attribute's comment: “part (3): the strict transform of a module restricts to the strict transform of its restriction; stated for an arbitrary module, the source's quasi-coherence being unused”.

Stacks 0863, part (3). In the situation of part (1), let F be an 𝒪_X-module. Then there are m : 𝒱' ⟶ 𝔅' presenting 𝒱' = 𝒱 ×_𝔅 𝔅' and a morphism can : U ×_𝒱 𝒱' ⟶ X ×_𝔅 𝔅' over u : U ⟶ X and over m, and can is étale and pulls the strict transform of F relative to the blowup b : 𝔅' ⟶ 𝔅 of 𝔅 in Z back to the strict transform of F|_U relative to the blowup v' : 𝒱' ⟶ 𝒱 of 𝒱 in Z ×_𝔅 𝒱.

The two commutations can ≫ pr_X = pr_U ≫ u and can ≫ pr_{𝔅'} = pr_{𝒱'} ≫ m say that can is the canonical morphism of the tag, the universal property of X ×_𝔅 𝔅' determining it from them; so pulling back along it is the restriction to U ×_𝒱 𝒱' that the tag speaks of.

Here the strict transform is the one of Stacks 0862, AlgebraicGeometry.Space.strictTransformSheaf, taken with respect to the blowup together with its exceptional divisor b^{-1}Z, respectively v'^{-1}(v^{-1}Z); the fibre products are the ones of AlgebraicGeometry.AlgebraicSpaces.fiberProduct, and F|_U is the pullback u^*F of Stacks 03LU, which for the étale u is restriction of sections by Stacks 03LW.

m, can and their properties come from part (1), AlgebraicGeometry.Space.isEtale_baseChange_blowup_of_isEtale, applied to the two canonical cartesian squares; the identification of the strict transforms is AlgebraicGeometry.Space.strictTransformSheafEtaleRestrictionIso, whose hypothesis on the exceptional divisors is AlgebraicGeometry.Space.range_pointsMap_preimage_exceptional.

No quasi-coherence of F is assumed: the source assumes it because that is the case the tag is applied in, and neither the construction of the strict transform nor this comparison uses it.

theorem exists_isEtale_strictTransformSheaf_restriction
    {𝔅 X 𝒱 U B' V' : AlgebraicSpaces B S hS}
    {Z : ClosedSubspaces B S hS 𝔅.1} {b : B' ⟶ 𝔅} (hb : IsBlowupAlong B S hS Z b)
    {f : X ⟶ 𝔅} {v : 𝒱 ⟶ 𝔅} (hv : IsEtale B S hS v.hom)
    {u : U ⟶ X} (hu : IsEtale B S hS u.hom) {w : U ⟶ 𝒱} (hcomm : u ≫ f = w ≫ v)
    {v' : V' ⟶ 𝒱} (hv' : IsBlowupAlong B S hS (preimageClosedSubspace v Z) v')
    (F : Modules.{u, u} B S hS X.1 X.2) :
    ∃ (m : V' ⟶ B') (can : strictTransformPullback B S hS w v' ⟶
        strictTransformPullback B S hS f b),
      IsPullback v' m v b ∧ IsEtale B S hS can.hom ∧
        can ≫ strictTransformPullbackToSource B S hS f b =
          strictTransformPullbackToSource B S hS w v' ≫ u ∧
        can ≫ strictTransformPullbackToBlowUp B S hS f b =
          strictTransformPullbackToBlowUp B S hS w v' ≫ m ∧
        Nonempty ((modulePullback B S hS can).obj
            (strictTransformSheaf B S hS f b (preimageClosedSubspace b Z).1 F) ≅
          strictTransformSheaf B S hS w v'
            (preimageClosedSubspace v' (preimageClosedSubspace v Z)).1
            ((modulePullback B S hS u).obj F))

AlgebraicGeometry.Space.exists_strictTransform_eq_preimage_of_isBlowupAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupStrictTransformSpaceEtale.lean, line 359. The attribute's comment: “part (2), for the blowups of 085Q themselves: the strict transform of an étale chart U is the base change along u of the strict transform of X”.

Stacks 0863, part (2). Let Z ⊆ 𝔅 be a closed subspace of an algebraic space over S, let b : 𝔅' ⟶ 𝔅 be the blowup of 𝔅 in Z, let f : X ⟶ 𝔅 be an algebraic space over 𝔅, let

U ⟶ X
↓     ↓
𝒱 ⟶ 𝔅

be a commutative square with étale horizontal arrows and let v' : 𝒱' ⟶ 𝒱 be the blowup of 𝒱 in the inverse image Z ×_𝔅 𝒱. Then the strict transform U' of U with respect to v' is X' ×_X U, where X' is the strict transform of X with respect to b.

Precisely: there are m : 𝒱' ⟶ 𝔅' presenting 𝒱' = 𝒱 ×_𝔅 𝔅' and an étale can : U ×_𝒱 𝒱' ⟶ X ×_𝔅 𝔅' over u and over m, sitting in a cartesian square that presents U ×_𝒱 𝒱' = (X ×_𝔅 𝔅') ×_X U, and U' is the inverse image of X' along can — which under that presentation is the base change of X' along u.

No hypothesis beyond the source's is carried, and in particular being a blowup is not assumed. The two blowups are the ones Tag 085Q constructs, AlgebraicGeometry.Space.blowUpAlongHom' for 𝔅 in Z and for 𝒱 in Z ×_𝔅 𝒱; that each of them is the blowup, in the sense of the universal property of Stacks 085U, is AlgebraicGeometry.Space.isBlowupAlong_blowUpAlongHom'. The arguments P, P' and the six B.Contains side conditions are the construction data Tag 085Q itself takes — an étale presentation of the space being blown up and the set-theoretic conditions on the three relative Projs that AlgebraicGeometry.Space.relativeProjChartOfSituation asks for — and nothing is assumed about Z beyond being a closed subspace.

The two halves of the argument are as in AlgebraicGeometry.Space.exists_strictTransform_eq_preimage_of_isEtale: the étale comparison of the ideals of supported sections, and that the strict transform of X is honestly cut out by that ideal, which comes from the exceptional divisor b^{-1}Z being an effective Cartier divisor — one half of the universal property of Stacks 085U.

theorem exists_strictTransform_eq_preimage_of_isBlowupAlong
    {Z : ClosedSubspaces B S hS Bl.obj} (P : Presentation B S hS Bl.obj Bl.property)
    (hcU : B.Contains (reesChartSituation (centreIdeal Z)
      (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    (hcR : B.Contains (reesRelationSituation (centreIdeal Z)
      (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    (hcRR : B.Contains (reesDoubleSituation (centreIdeal Z)
      (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    {f : X ⟶ Bl} {v : Vv ⟶ Bl} (hv : IsEtale B S hS v.hom)
    {u : U ⟶ X} (hu : IsEtale B S hS u.hom) {w : U ⟶ Vv} (hcomm : u ≫ f = w ≫ v)
    (P' : Presentation B S hS Vv.obj Vv.property)
    (hcU' : B.Contains (reesChartSituation (centreIdeal (preimageClosedSubspace v Z))
      (isCartesianOnAffineCharts_centreIdeal (preimageClosedSubspace v Z)) P').relativeProj)
    (hcR' : B.Contains (reesRelationSituation (centreIdeal (preimageClosedSubspace v Z))
      (isCartesianOnAffineCharts_centreIdeal (preimageClosedSubspace v Z)) P').relativeProj)
    (hcRR' : B.Contains (reesDoubleSituation (centreIdeal (preimageClosedSubspace v Z))
      (isCartesianOnAffineCharts_centreIdeal (preimageClosedSubspace v Z)) P').relativeProj) :
    ∃ (m : blowUpAlong' (preimageClosedSubspace v Z) P' hcU' hcR' hcRR' ⟶
        blowUpAlong' Z P hcU hcR hcRR)
      (can : strictTransformPullback B S hS w
          (blowUpAlongHom' (preimageClosedSubspace v Z) P' hcU' hcR' hcRR') ⟶
        strictTransformPullback B S hS f (blowUpAlongHom' Z P hcU hcR hcRR)),
      IsPullback (blowUpAlongHom' (preimageClosedSubspace v Z) P' hcU' hcR' hcRR') m v
          (blowUpAlongHom' Z P hcU hcR hcRR) ∧
        IsEtale B S hS can.hom ∧
        can ≫ strictTransformPullbackToSource B S hS f (blowUpAlongHom' Z P hcU hcR hcRR) =
          strictTransformPullbackToSource B S hS w
            (blowUpAlongHom' (preimageClosedSubspace v Z) P' hcU' hcR' hcRR') ≫ u ∧
        can ≫ strictTransformPullbackToBlowUp B S hS f (blowUpAlongHom' Z P hcU hcR hcRR) =
          strictTransformPullbackToBlowUp B S hS w
            (blowUpAlongHom' (preimageClosedSubspace v Z) P' hcU' hcR' hcRR') ≫ m ∧
        IsPullback can
          (strictTransformPullbackToSource B S hS w
            (blowUpAlongHom' (preimageClosedSubspace v Z) P' hcU' hcR' hcRR'))
          (strictTransformPullbackToSource B S hS f (blowUpAlongHom' Z P hcU hcR hcRR)) u ∧
        strictTransformSubfunctor B S hS w
            (blowUpAlongHom' (preimageClosedSubspace v Z) P' hcU' hcR' hcRR')
            (preimageClosedSubspace
              (blowUpAlongHom' (preimageClosedSubspace v Z) P' hcU' hcR' hcRR')
              (preimageClosedSubspace v Z)).1 =
          (strictTransformSubfunctor B S hS f (blowUpAlongHom' Z P hcU hcR hcRR)
            (preimageClosedSubspace (blowUpAlongHom' Z P hcU hcR hcRR) Z).1).preimage
            can.hom

AlgebraicGeometry.Space.exists_strictTransform_eq_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupStrictTransformSpaceEtaleUnconditional.lean, line 122. The attribute's comment: “part (2): the strict transform of an étale chart U is the base change along u of the strict transform of X, for an arbitrary blowup and with no assumed inputs”.

Stacks 0863, part (2). Let Z ⊆ 𝔅 be a closed subspace of an algebraic space over S, let b : 𝔅' ⟶ 𝔅 be the blowup of 𝔅 in Z, let f : X ⟶ 𝔅 be an algebraic space over 𝔅, let

U ⟶ X
↓     ↓
𝒱 ⟶ 𝔅

be a commutative square with étale horizontal arrows and let v' : 𝒱' ⟶ 𝒱 be the blowup of 𝒱 in the inverse image Z ×_𝔅 𝒱. Then the strict transform U' of U with respect to v' is X' ×_X U, where X' is the strict transform of X with respect to b.

Precisely: there are m : 𝒱' ⟶ 𝔅' presenting 𝒱' = 𝒱 ×_𝔅 𝔅' and an étale can : U ×_𝒱 𝒱' ⟶ X ×_𝔅 𝔅' over u and over m, sitting in a cartesian square that presents U ×_𝒱 𝒱' = (X ×_𝔅 𝔅') ×_X U, and U' is the inverse image of X' along can — which under that presentation is the base change of X' along u.

No hypothesis beyond the source's is carried. The existence of a closed subspace cut out by the ideal of sections supported on the exceptional preimage, which is all that AlgebraicGeometry.Space.exists_strictTransform_eq_preimage_of_isEtale asks for beyond the étale comparison of those ideals, comes from the exceptional divisor b^{-1}Z being an effective Cartier divisor on 𝔅'; and that is one half of the universal property of Stacks 085U, so hb supplies it.

theorem exists_strictTransform_eq_preimage
    {Z : ClosedSubspaces B S hS Bl.1} {b : B' ⟶ Bl} (hb : IsBlowupAlong B S hS Z b)
    {f : X ⟶ Bl} {v : Vv ⟶ Bl} (hv : IsEtale B S hS v.hom)
    {u : U ⟶ X} (hu : IsEtale B S hS u.hom) {w : U ⟶ Vv} (hcomm : u ≫ f = w ≫ v)
    {v' : V' ⟶ Vv} (hv' : IsBlowupAlong B S hS (preimageClosedSubspace v Z) v') :
    ∃ (m : V' ⟶ B') (can : strictTransformPullback B S hS w v' ⟶
        strictTransformPullback B S hS f b),
      IsPullback v' m v b ∧ IsEtale B S hS can.hom ∧
        can ≫ strictTransformPullbackToSource B S hS f b =
          strictTransformPullbackToSource B S hS w v' ≫ u ∧
        can ≫ strictTransformPullbackToBlowUp B S hS f b =
          strictTransformPullbackToBlowUp B S hS w v' ≫ m ∧
        IsPullback can (strictTransformPullbackToSource B S hS w v')
          (strictTransformPullbackToSource B S hS f b) u ∧
        strictTransformSubfunctor B S hS w v'
            (preimageClosedSubspace v' (preimageClosedSubspace v Z)).1 =
          (strictTransformSubfunctor B S hS f b
            (preimageClosedSubspace b Z).1).preimage can.hom

AlgebraicGeometry.Space.exists_strictTransform_eq_preimage_strictTransformSheaf_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupStrictTransformSpaceEtaleUnconditional.lean, line 163. The attribute's comment: “parts (2) and (3) for one and the same comparison morphism, for an arbitrary blowup and with no assumed inputs”.

Stacks 0863, parts (2) and (3). In the situation of part (1) there are m : 𝒱' ⟶ 𝔅' presenting 𝒱' = 𝒱 ×_𝔅 𝔅' and an étale can : U ×_𝒱 𝒱' ⟶ X ×_𝔅 𝔅' over u and over m, sitting in a cartesian square that presents U ×_𝒱 𝒱' = (X ×_𝔅 𝔅') ×_X U, such that

• the strict transform U' of U with respect to v' is the inverse image of the strict transform X' of X with respect to b along can, which is part (2); and
• for every 𝒪_X-module F the pullback along can of the strict transform of F with respect to b is the strict transform of F|_U with respect to v', which is part (3).

Both for the same m and the same can: the two parts are read off the single comparison morphism that part (1), AlgebraicGeometry.Space.isEtale_baseChange_blowup_of_isEtale, returns for the two canonical cartesian squares. This is what a consumer of the tag needs, the two parts separately leaving the two copies of can unidentified.

No hypothesis beyond the source's is carried, and no quasi-coherence of F; see AlgebraicGeometry.Space.exists_strictTransform_eq_preimage and AlgebraicGeometry.Space.exists_isEtale_strictTransformSheaf_restriction.

theorem exists_strictTransform_eq_preimage_strictTransformSheaf_iso
    {Z : ClosedSubspaces B S hS Bl.1} {b : B' ⟶ Bl} (hb : IsBlowupAlong B S hS Z b)
    {f : X ⟶ Bl} {v : Vv ⟶ Bl} (hv : IsEtale B S hS v.hom)
    {u : U ⟶ X} (hu : IsEtale B S hS u.hom) {w : U ⟶ Vv} (hcomm : u ≫ f = w ≫ v)
    {v' : V' ⟶ Vv} (hv' : IsBlowupAlong B S hS (preimageClosedSubspace v Z) v') :
    ∃ (m : V' ⟶ B') (can : strictTransformPullback B S hS w v' ⟶
        strictTransformPullback B S hS f b),
      IsPullback v' m v b ∧ IsEtale B S hS can.hom ∧
        can ≫ strictTransformPullbackToSource B S hS f b =
          strictTransformPullbackToSource B S hS w v' ≫ u ∧
        can ≫ strictTransformPullbackToBlowUp B S hS f b =
          strictTransformPullbackToBlowUp B S hS w v' ≫ m ∧
        IsPullback can (strictTransformPullbackToSource B S hS w v')
          (strictTransformPullbackToSource B S hS f b) u ∧
        strictTransformSubfunctor B S hS w v'
            (preimageClosedSubspace v' (preimageClosedSubspace v Z)).1 =
          (strictTransformSubfunctor B S hS f b
            (preimageClosedSubspace b Z).1).preimage can.hom ∧
        ∀ F : Modules.{u, u} B S hS X.1 X.2,
          Nonempty ((modulePullback B S hS can).obj
              (strictTransformSheaf B S hS f b (preimageClosedSubspace b Z).1 F) ≅
            strictTransformSheaf B S hS w v'
              (preimageClosedSubspace v' (preimageClosedSubspace v Z)).1
              ((modulePullback B S hS u).obj F))

Tag 0864, a lemma

Tag 0864 in the Stacks Project.

AlgebraicGeometry.Space.isBlowupAlong_strictTransform, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformIsBlowup.lean, line 347. The attribute's comment: “part (1): the strict transform of X is the blowup of X in the inverse image of the centre, for an arbitrary blowup of the base and with no assumed inputs”.

Stacks 0864, clause (1). Let S be a scheme, let A be an algebraic space over S, let Z ⊆ A be a closed subspace, let b : A' ⟶ A be the blowup of A in Z and let f : X ⟶ A be an algebraic space over A. Then the strict transform X' of X — the closed subspace of X ×_A A' of Stacks 0862, clause (2) — with its morphism X' ⟶ X ×_A A' ⟶ X, is the blowup of X in the inverse image f⁻¹Z.

No hypothesis beyond b being the blowup of A in Z is carried: in particular no second blowup is assumed to exist, and nothing is assumed of f.

Both halves of the universal property of Stacks 085U are checked. Membership in the category 𝒞 is AlgebraicGeometry.Space.isPullbackDefined_strictTransform_of_isBlowupAlong. For finality, an object y : Y ⟶ X of 𝒞 gives a morphism Y ⟶ X ×_A A' with components y and the classifying morphism of b, which factors through X' by AlgebraicGeometry.Space.exists_comp_eq_strictTransformSpaceι; and the factorization is unique because X' ⟶ X ×_A A' is a monomorphism, X ×_A A' is a fibre product and the classifying morphism of b is unique.

theorem isBlowupAlong_strictTransform (hb : IsBlowupAlong B S hS Z b) :
    IsBlowupAlong B S hS (preimageClosedSubspace f Z)
      (strictTransformSpaceι B S hS f b (preimageClosedSubspace b Z).1 ≫
        strictTransformPullbackToSource B S hS f b)

AlgebraicGeometry.Space.exists_strictTransformSheafIso_modulePushforward_strictTransformSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformSheafBlowupComparison.lean, line 639. The attribute's comment: “part (2): the strict transform of a module is the direct image, along the closed immersion of the strict transform of X into X ×_A A', of the strict transform of that module relative to the blowup X' ⟶ X, by the isomorphism carrying the quotient map onto the first to the canonical comparison; for an arbitrary blowup of the base, an arbitrary module, and with no assumed inputs”.

Stacks 0864, clause (2). Let S be a scheme, let A be an algebraic space over S, let Z ⊆ A be a closed subspace, let b : A' ⟶ A be the blowup of A in Z, let f : X ⟶ A be an algebraic space over A and let F be an 𝒪_X-module. Then the strict transform F' of F — the quotient of pr_X^*F by its sections supported on the exceptional preimage — is the direct image, along the closed immersion X' ⟶ X ×_A A' of the strict transform of X, of the strict transform of F relative to the blowup X' ⟶ X of X in f⁻¹Z.

The isomorphism carries the quotient map onto F' to the canonical comparison AlgebraicGeometry.Space.strictTransformSheafPushforwardComparison, and since that quotient map is an epimorphism there is exactly one isomorphism which does; that is the sense in which the isomorphism of clause (2) is canonical.

That X' ⟶ X is the blowup of X in f⁻¹Z, which is what makes the strict transform of F relative to it the one clause (2) speaks of, is clause (1), AlgebraicGeometry.Space.isBlowupAlong_strictTransform; the statement is otherwise AlgebraicGeometry.Space.exists_strictTransformSheafIso_modulePushforward_of_isBlowupAlong at i the closed immersion of the strict transform.

No hypothesis beyond b being the blowup of A in Z is carried: in particular no second blowup is assumed to exist, nothing is assumed of f, and F is an arbitrary 𝒪_X-module — the Stacks Project states clause (2) for a quasi-coherent F, and the argument uses nothing of F. See the module documentation.

theorem exists_strictTransformSheafIso_modulePushforward_strictTransformSpace
    (hb : IsBlowupAlong B S hS Z b) (F : Modules.{u, u} B S hS X.1 X.2) :
    ∃ e : strictTransformSheaf B S hS f b (preimageClosedSubspace b Z).1 F ≅
        (modulePushforward B S hS
            (strictTransformSpaceι B S hS f b (preimageClosedSubspace b Z).1)).obj
          (strictTransformSheafOver B S hS
            (strictTransformSpaceι B S hS f b (preimageClosedSubspace b Z).1 ≫
              strictTransformPullbackToSource B S hS f b)
            (preimageClosedSubspace
              (strictTransformSpaceι B S hS f b (preimageClosedSubspace b Z).1 ≫
                strictTransformPullbackToSource B S hS f b)
              (preimageClosedSubspace f Z)) F),
      strictTransformSheafQuotient B S hS f b (preimageClosedSubspace b Z).1 F ≫ e.hom =
        strictTransformSheafPushforwardComparison B S hS f b Z
          (strictTransformSpaceι B S hS f b (preimageClosedSubspace b Z).1) F

Tag 0865, a lemma

Tag 0865 in the Stacks Project.

AlgebraicGeometry.Space.strictTransformSubfunctor_eq_top_of_isFlatAt_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformFlatCompositionUnassumed.lean, line 101. The attribute's comment: “part (1), with no assumed inputs”.

Stacks 0865, part (1). Let Z ⊆ A be a closed subspace of an algebraic space over S, let b : A' ⟶ A be the blowup of A in Z and let f : X ⟶ A be an algebraic space over A. If X is flat over A at every point lying over Z, then the strict transform of X with respect to b is the whole base change X ×_A A'.

The hypotheses are the source's and nothing else. The ideal of sections of 𝒪_{X ×_A A'} supported on the exceptional preimage vanishes on every étale chart, AlgebraicGeometry.Space.strictTransformIdealSubmodule_eq_bot_of_isFlatAt; the strict transform is then the whole base change by Stacks 03MB, in the form AlgebraicGeometry.Space.strictTransformSubfunctor_eq_top_of_forall_definingIdealAt_eq_bot.

The source reduces part (1) to the case of schemes by étale localization, Stacks 0863 parts (2) and (3), which this library does not have; the route taken instead is native to algebraic spaces and runs through the étale charts of the fibre product. See the module documentation of StacksFrontier/AlgebraicGeometry/Spaces/FlatAtPointBaseChange.lean.

The conditional form of this statement in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformProperties.lean keeps the name without the suffix _unconditional; the suffix marks the same conclusion with that form's assumed input discharged, and the tag is registered here.

theorem strictTransformSubfunctor_eq_top_of_isFlatAt_unconditional (Z : ClosedSubspaces B S hS A.1)
    (hb : IsBlowupAlong B S hS Z b)
    (hflat : ∀ x : points B S hS X.1,
      pointsMap B S hS X.1 f.hom x ∈ Set.range (pointsMap B S hS Z.1.toFunctor Z.1.ι) →
        IsFlatAt B S hS f.hom x) :
    strictTransformSubfunctor B S hS f b (Z.1.preimage b.hom) = ⊤

AlgebraicGeometry.Space.isIso_strictTransformSheafQuotient_of_isFlatOverAtGeometricPoint_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformFlatCompositionUnassumed.lean, line 136. The attribute's comment: “part (2), with no assumed inputs”.

Stacks 0865, part (2). In the situation of part (1), let F be a quasi-coherent 𝒪_X-module which is flat over A at every point lying over Z. Then the canonical quotient map pr_X^*F ⟶ F' onto the strict transform of F is an isomorphism, so the strict transform of F is pr_X^*F.

The hypotheses are the source's and nothing else: b is the blowup of A in Z in the sense of the universal property of Stacks 085U, F is quasi-coherent, and F is flat over A at the points above Z — read at geometric points, condition (2) of Stacks 05VU, AlgebraicGeometry.Space.IsFlatOverAtGeometricPoint, a geometric point lying over Z when its underlying point of |X| does.

The submodule of sections of pr_X^*F supported on the exceptional preimage vanishes, Space.supportedSections_exceptionalPreimage_ι_eq_zero_of_isFlatOverAtGeometricPoint; the strict transform is the cokernel of its inclusion, so the quotient map is the cokernel projection of a zero morphism and hence invertible.

The source reduces part (2) to the case of schemes by étale localization, Stacks 0863 parts (2) and (3); the route taken instead is native to algebraic spaces and runs through the étale charts of the fibre product, exactly as for part (1). See the module documentation of StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleSupportedSections.lean.

The conditional form of this statement in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformProperties.lean keeps the name without the suffix _unconditional; the suffix marks the same conclusion with that form's assumed input discharged, and the tag is registered here.

theorem isIso_strictTransformSheafQuotient_of_isFlatOverAtGeometricPoint_unconditional
    (Z : ClosedSubspaces B S hS A.1) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) (hb : IsBlowupAlong B S hS Z b)
    (hflat : ∀ xbar : GeometricPoint B S hS X.1,
      pointsMap B S hS X.1 f.hom xbar.image ∈
          Set.range (pointsMap B S hS Z.1.toFunctor Z.1.ι) →
        IsFlatOverAtGeometricPoint B S hS f F xbar) :
    IsIso (strictTransformSheafQuotient B S hS f b (Z.1.preimage b.hom) F)

Tag 0866, a lemma

Tag 0866 in the Stacks Project.

AlgebraicGeometry.Space.exists_modulePushforward_strictTransformSheaf_iso_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformAffinePushforward.lean, line 108. The attribute's comment: “the hypotheses are the tag's own -- a blowup of the ambient space along a closed subspace, an affine morphism of algebraic spaces over it, and a quasi-coherent module -- and the base-change isomorphism of the base-change clause of Stacks 07U8, Stacks 02KG for an affine morphism of algebraic spaces, is proved on the way”.

Stacks 0866. Let Z ⊆ A be a closed subspace of an algebraic space over S, let b : A' ⟶ A be the blowup of A in Z, let g : X ⟶ Y be an affine morphism of algebraic spaces over A, let F be an 𝒪_X-module and let g' : X ×_A A' ⟶ Y ×_A A' be the base change of g. Then g'_* of the strict transform of F relative to b is the strict transform of g_* F, compatibly with the two quotient maps and the base-change comparison.

F is quasi-coherent, which is the tag's own hypothesis on it.

The hypotheses are the tag's own, and the three inputs the argument runs on are all proved.

The base-change isomorphism α : g'_* pr_X^*F ≅ pr_Y^* g_*F — the base-change clause of Stacks 07U8, that is Stacks 02KG for an affine morphism of algebraic spaces — is AlgebraicGeometry.Space.nonempty_iso_modulePushforward_modulePullback_of_isAffineHom at the cartesian square of the two ambient base changes along b.

The identification β of the direct image of the sections supported on the exceptional preimage with the sections of pr_Y^*(g_*F) supported there, compatibly with α, is Stacks 085B transported along α, AlgebraicGeometry.Space.exists_iso_modulePushforward_supportedSectionsSubmodule_of_eq_preimage, together with the identification of the exceptional preimage upstairs as the inverse image of the one downstairs, AlgebraicGeometry.Space.exceptionalPreimageSet_comp_eq_preimage.

Right exactness of g'_* on the sequence at hand — that the direct image along the affine morphism g' preserves the cokernel defining the strict transform, which is the use the Stacks Project makes of Stacks 01SB — is AlgebraicGeometry.Space.preservesCokernel_submoduleι_modulePushforward_of_isAffineHom, applied to the base change g' of g, which is affine by Stacks 03WI; its two quasi-coherence inputs are quasi-coherence of pr_X^*F, which is Stacks 03GA, and quasi-coherence of the submodule of sections supported on the exceptional preimage, which is AlgebraicGeometry.Space.isQuasicoherentOnSite_supportedSections_exceptionalPreimage above, the exceptional divisor of a blowup being an effective Cartier divisor and hence locally principal.

What this proof does is the argument of the Stacks Project: the strict transform is a cokernel, right exactness of the affine direct image carries it through g'_*, and α identifies the resulting cokernel with the cokernel defining the strict transform of g_* F.

theorem exists_modulePushforward_strictTransformSheaf_iso_unconditional
    (Z : ClosedSubspaces B S hS A.1)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (hb : IsBlowupAlong B S hS Z b) (hg : IsAffineHom B S hS g.hom) :
    ∃ (α : (modulePushforward B S hS (strictTransformPullbackMap B S hS g f b)).obj
              ((modulePullback B S hS
                (strictTransformPullbackToSource B S hS (g ≫ f) b)).obj F) ≅
            (modulePullback B S hS (strictTransformPullbackToSource B S hS f b)).obj
              ((modulePushforward B S hS g).obj F))
        (e : (modulePushforward B S hS (strictTransformPullbackMap B S hS g f b)).obj
              (strictTransformSheaf B S hS (g ≫ f) b (Z.1.preimage b.hom) F) ≅
            strictTransformSheaf B S hS f b (Z.1.preimage b.hom)
              ((modulePushforward B S hS g).obj F)),
      (modulePushforward B S hS (strictTransformPullbackMap B S hS g f b)).map
            (strictTransformSheafQuotient B S hS (g ≫ f) b (Z.1.preimage b.hom) F) ≫ e.hom =
        α.hom ≫ strictTransformSheafQuotient B S hS f b (Z.1.preimage b.hom)
          ((modulePushforward B S hS g).obj F)

Tag 0867, a lemma

Tag 0867 in the Stacks Project.

AlgebraicGeometry.Space.isBlowupAlong_sumClosedSubspaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupCentreEnlargedByDivisor.lean, line 130. The attribute's comment: “part (1): granted, as the hypotheses h0809 and h083V, that the inverse image of D along the blowup is an effective Cartier divisor and that the inverse image of Z + D along a morphism is one exactly when those of Z and of D are”.

Stacks 0867, part (1). Let Z ⊆ 𝔅 and D ⊆ 𝔅 be closed subspaces of an algebraic space over S with D an effective Cartier divisor, and let Z + D be the closed subspace cut out by the product of their defining ideals. A morphism b : B' ⟶ 𝔅 which is the blowup of 𝔅 in Z is also the blowup of 𝔅 in Z + D.

Granted as hypotheses: that the inverse image of D along b is an effective Cartier divisor (Stacks 0809 for algebraic spaces), and that the inverse image of Z + D along a morphism is an effective Cartier divisor exactly when those of Z and of D are (Stacks 083V for algebraic spaces, and its converse). See the module documentation.

theorem isBlowupAlong_sumClosedSubspaces {𝔅 B' : AlgebraicSpaces B S hS}
    (Z D : ClosedSubspaces B S hS 𝔅.1)
    (_hD : IsEffectiveCartierDivisor B S hS 𝔅 D)
    {b : B' ⟶ 𝔅} (hb : IsBlowupAlong B S hS Z b)
    (h0809 : IsPullbackDefined B S hS b D)
    (h083V : ∀ {Y : AlgebraicSpaces B S hS} (g : Y ⟶ 𝔅),
      IsPullbackDefined B S hS g (sumClosedSubspaces B S hS 𝔅 Z D) ↔
        IsPullbackDefined B S hS g Z ∧ IsPullbackDefined B S hS g D) :
    IsBlowupAlong B S hS (sumClosedSubspaces B S hS 𝔅 Z D) b

AlgebraicGeometry.Space.isBlowupAlong_sumClosedSubspaces_of_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupCentreEnlargedByDivisorConstructed.lean, line 134. The attribute's comment: “part (1): the blowup of the space in Z is the blowup of the space in Z + D, with no assumed inputs beyond the Stacks 085Q construction data — the étale presentation P of the base, the HasSheafify universe choice for the quotient presheaf, and the three B.Contains size conditions on the relative Projs of the chart, relation and double situations — none of which occurs in the conclusion”.

Stacks 0867, part (1). Let Z ⊆ 𝔅 and D ⊆ 𝔅 be closed subspaces of an algebraic space over S with D an effective Cartier divisor, and let Z + D be the closed subspace cut out by the product of their defining ideals. A morphism b : B' ⟶ 𝔅 which is the blowup of 𝔅 in Z is also the blowup of 𝔅 in Z + D.

Nothing is granted: the input h0809 of AlgebraicGeometry.Space.isBlowupAlong_sumClosedSubspaces — that the inverse image of D along b is an effective Cartier divisor — is Stacks 085X, the algebraic-space counterpart of Stacks 0809, AlgebraicGeometry.Space.isPullbackDefined_of_isBlowupAlong. Its proof goes through the blowup constructed in Stacks 085Q, so the construction data of that tag — an étale presentation P of 𝔅 and the three size conditions on the relative Projs — is carried here; it does not appear in the conclusion.

theorem isBlowupAlong_sumClosedSubspaces_of_presentation {𝔅 B' : AlgebraicSpaces B S hS}
    (Z D : ClosedSubspaces B S hS 𝔅.obj)
    (hD : IsEffectiveCartierDivisor B S hS 𝔅 D)
    (P : Presentation B S hS 𝔅.obj 𝔅.property)
    (hcU : B.Contains (reesChartSituation (centreIdeal Z)
        (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    (hcR : B.Contains (reesRelationSituation (centreIdeal Z)
        (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    (hcRR : B.Contains (reesDoubleSituation (centreIdeal Z)
        (isCartesianOnAffineCharts_centreIdeal Z) P).relativeProj)
    {b : B' ⟶ 𝔅} (hb : IsBlowupAlong B S hS Z b) :
    IsBlowupAlong B S hS (sumClosedSubspaces B S hS 𝔅 Z D) b

AlgebraicGeometry.Space.strictTransformSheaf_preimage_sumClosedSubspaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupCentreEnlargedByDivisorConstructed.lean, line 244. The attribute's comment: “part (2), with no assumed inputs”.

Stacks 0867, part (2). Let Z, D ⊆ 𝔅 be closed subspaces with D an effective Cartier divisor, let b : B' ⟶ 𝔅 be the blowup of 𝔅 in Z — hence also the blowup of 𝔅 in Z + D, by part (1) — let f : X ⟶ 𝔅 be an algebraic space over 𝔅 and let F be an 𝒪_X-module whose subsheaf of sections supported on |f^{-1}D| is zero. Then the strict transform of F with respect to the blowup of 𝔅 in Z and the strict transform of F with respect to the blowup of 𝔅 in Z + D agree.

Both strict transforms live on the same X ×_𝔅 B', the two blowups being the same morphism b, and both are the quotient of pr_X^*F by its sections supported on the respective exceptional preimage. Those two sets of points differ by the inverse image of |D| (AlgebraicGeometry.Space.exceptionalPreimageSet_preimage_sumClosedSubspaces), and enlarging the supported set by it changes the supported sections not at all, AlgebraicGeometry.Space.supportedSectionsSubmodule_union_eq.

Nothing is granted: the source's hypothesis hW, that pr_X^*F has no nonzero sections supported on the inverse image of |f^{-1}D| over étale charts of X ×_𝔅 B' avoiding the exceptional preimage, is derived here from the hypothesis on F rather than assumed. Away from the exceptional preimage the projection pr_X : X ×_𝔅 B' ⟶ X restricts to an isomorphism onto an open subspace P of X ×_𝔅 B', by Stacks 085T part (1) (AlgebraicGeometry.Space.isIso_fromPreimage_openComplement) applied to the open complement of Z in 𝔅 and transported across the pullback square defining the base change (CategoryTheory.Subfunctor.isIso_fromPreimage_of_isPullback); in particular the inclusion of P is étale. A chart of X ×_𝔅 B' whose points avoid the exceptional preimage then factors through P, and AlgebraicGeometry.Space.sectionSupportedIn_etaleModulePullback_iff, applied once to the inclusion of P and once to its composite with pr_X, transports the vanishing of sections of F supported on |f^{-1}D| to that chart.

theorem strictTransformSheaf_preimage_sumClosedSubspaces
    (Z D : ClosedSubspaces B S hS 𝔅.1)
    (hD : IsEffectiveCartierDivisor B S hS 𝔅 D)
    {b : B' ⟶ 𝔅} (hb : IsBlowupAlong B S hS Z b) (f : X ⟶ 𝔅)
    (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : HasNoSectionsSupportedIn B S hS X
      (pointsMap B S hS X.1 f.hom ⁻¹' subspacePointSet B S hS 𝔅.1 D.1) F) :
    strictTransformSheaf B S hS f b
        (preimageClosedSubspace b (sumClosedSubspaces B S hS 𝔅 Z D)).1 F =
      strictTransformSheaf B S hS f b (preimageClosedSubspace b Z).1 F

Tag 0868, a lemma

Tag 0868 in the Stacks Project.

AlgebraicGeometry.Space.exists_strictTransformSheaf_comp_iso_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformFlatCompositionUnassumed.lean, line 211. The attribute's comment: “part (1): the strict transform of a module for the blowup of the base in the composite centre is the strict transform along the second blowup of the strict transform along the first, by the isomorphism carrying the pullback of the quotient map onto the former to the composite of the two quotient maps onto the latter, over the identification of the two ambient base changes and the identification of the two pullbacks of the module it induces; for an arbitrary module and with no assumed inputs”.

Stacks 0868, part (1). Let Z ⊆ A be a closed subspace of an algebraic space over S, let b : A' ⟶ A be the blowup of A in Z, let Z' ⊆ A' be a closed subspace and let c : A'' ⟶ A' be the blowup of A' in Z'. Let Y ⊆ A be a closed subspace with |Y| = |Z| ∪ |b|(|Z'|) and such that the composition A'' ⟶ A is the blowup of A in Y. Then for any algebraic space f : X ⟶ A over A and any 𝒪_X-module F, the strict transform of F with respect to c of the strict transform of F with respect to b is the strict transform of F with respect to A'' ⟶ A, compatibly with the identification of the two ambient base changes and with the quotient maps onto the two strict transforms.

The identification of the ambient base changes (X ×_A A') ×_{A'} A'' ≅ X ×_A A'', together with its compatibility with the projections to X and to A'' — the two equations of the conclusion, the first of which the comparison of the modules is stated relative to — is AlgebraicGeometry.Space.iteratedStrictTransformPullbackIso, and is proved here unconditionally.

The comparison of the modules themselves, the last conjunct, is produced with its compatibility with the two quotient maps onto the strict transforms: pulled back along the identification of the ambient base changes, the quotient map pr_X^*F ⟶ F' for the composite blowup becomes, over the induced identification of the two pullbacks of F (AlgebraicGeometry.Space.strictTransformInnerModulePullbackIso), the composite of the pullback of the first quotient map with the second. Since the first of those is an epimorphism, there is exactly one isomorphism which does that; that is the sense in which the comparison is canonical.

Its two halves are AlgebraicGeometry.Space.exists_iteratedStrictTransformSheaf_iso of StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformComposition.lean — which carries the compatibility of the iterated quotient with the two projections — and the universal property of the quotient by the supported sections, AlgebraicGeometry.Space.exists_strictTransformSheafIso, applied to the pullback of the quotient map for the composite blowup along the ambient identification. That pullback is an epimorphism because the pullback of modules is a left adjoint; it kills only the sections supported on the exceptional preimage of (c ≫ b)⁻¹Y because over the part of (X ×_A A') ×_{A'} A'' lying off that set it is invertible (AlgebraicGeometry.Space.isIso_modulePullback_map_cokernelπ_supportedSectionsSubmodule, the points there missing the exceptional preimage downstairs), which is AlgebraicGeometry.Space.kernelSectionsSupportedIn_of_mono_modulePullback_map; and its target has no nonzero local section supported there because the restriction of the strict transform along that identification is the strict transform of the restriction, Stacks 0863 part (3) in its geometry-free form AlgebraicGeometry.Space.strictTransformSheafEtaleRestrictionIso — applicable because the identification is an isomorphism, hence étale.

The hypothesis of the iterated comparison on the supported sets is AlgebraicGeometry.Space.exceptionalPreimageSet_compositeCentre, which is where hY and the blowup b are used: a blowup is injective on the points off its centre, so the exceptional preimage of (c ≫ b)⁻¹Y splits as the inverse image of the first exceptional preimage together with the exceptional preimage of c⁻¹Z'.

The conditional form of this statement in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformProperties.lean keeps the name without the suffix _unconditional; the suffix marks the same conclusion with that form's assumed input discharged, and the tag is registered here.

theorem exists_strictTransformSheaf_comp_iso_unconditional (Z : ClosedSubspaces B S hS A.1)
    (Z' : ClosedSubspaces B S hS A'.1) (Y : ClosedSubspaces B S hS A.1)
    (F : Modules.{u, u} B S hS X.1 X.2)
    (hb : IsBlowupAlong B S hS Z b) (hc : IsBlowupAlong B S hS Z' c)
    (hY : IsCompositeCentre B S hS b Z Z' Y) (_hd : IsBlowupAlong B S hS Y (c ≫ b)) :
    ∃ e : strictTransformPullback B S hS (strictTransformPullbackToBlowUp B S hS f b) c ≅
        strictTransformPullback B S hS f (c ≫ b),
      ∃ hsrc : e.hom ≫ strictTransformPullbackToSource B S hS f (c ≫ b) =
          strictTransformPullbackToSource B S hS
              (strictTransformPullbackToBlowUp B S hS f b) c ≫
            strictTransformPullbackToSource B S hS f b,
      (e.hom ≫ strictTransformPullbackToBlowUp B S hS f (c ≫ b) =
        strictTransformPullbackToBlowUp B S hS
          (strictTransformPullbackToBlowUp B S hS f b) c) ∧
      ∃ cmp : (modulePullback B S hS e.hom).obj
            (strictTransformSheaf B S hS f (c ≫ b) (Y.1.preimage (c ≫ b).hom) F) ≅
          strictTransformSheaf B S hS (strictTransformPullbackToBlowUp B S hS f b) c
            (Z'.1.preimage c.hom) (strictTransformSheaf B S hS f b (Z.1.preimage b.hom) F),
        (modulePullback B S hS e.hom).map
              (strictTransformSheafQuotient B S hS f (c ≫ b)
                (Y.1.preimage (c ≫ b).hom) F) ≫ cmp.hom =
          (strictTransformInnerModulePullbackIso B S hS f (c ≫ b)
              (strictTransformPullbackToSource B S hS f b)
              (strictTransformPullbackToBlowUp B S hS f b) c e.hom hsrc F).hom ≫
            (modulePullback B S hS (strictTransformPullbackToSource B S hS
                  (strictTransformPullbackToBlowUp B S hS f b) c)).map
                (strictTransformSheafQuotient B S hS f b (Z.1.preimage b.hom) F) ≫
              strictTransformSheafQuotient B S hS
                (strictTransformPullbackToBlowUp B S hS f b) c (Z'.1.preimage c.hom)
                (strictTransformSheaf B S hS f b (Z.1.preimage b.hom) F)

AlgebraicGeometry.Space.exists_strictTransformSpace_comp_iso_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformFlatCompositionUnassumed.lean, line 473. The attribute's comment: “part (2): strict transform of a space”.

Stacks 0868, part (2). In the situation of part (1), the strict transform of X with respect to c of the strict transform of X with respect to b is the strict transform of X with respect to A'' ⟶ A: the two closed subspaces are isomorphic over the ambient base change X ×_A A''.

The morphism X' ×_{A'} A'' ⟶ X ×_A A'' of ambient base changes along which the comparison is made is AlgebraicGeometry.Space.iteratedStrictTransformSpaceMap; X' here is the first strict transform, the ambient base change of the second being taken over A' and not over X ×_A A'. Its two triangles over X and over A'' are the first two conjuncts of the conclusion and hold with no hypothesis at all.

The comparison of the two closed subspaces is AlgebraicGeometry.Space.exists_iteratedStrictTransformSpace_iso of StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformSpaceComposition.lean. Its route is the source's own, read on ideals: the image of the second strict transform in (X ×_A A') ×_{A'} A'' is a closed subspace whose defining ideal is exactly the ideal of functions supported on the exceptional preimage of (c ≫ b)^{-1}Y, so it is the strict transform of X with respect to the composite by AlgebraicGeometry.Space.strictTransformSubfunctor_eq_of_definingIdealSheaf_eq, and the identification of the two ambient base changes transports that across Stacks 0863 part (2). One inclusion of ideals is the geometry of the two blowups (Stacks 085T through AlgebraicGeometry.Space.exceptionalPreimageSet_compositeCentre, and Stacks 0862 off the exceptional divisor); the other is Stacks 082Z together with the fact that the second strict transform has no nonzero local function supported there, which is Stacks 083S for the two exceptional divisors it is built from.

The conditional form of this statement in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformProperties.lean keeps the name without the suffix _unconditional; the suffix marks the same conclusion with that form's assumed input discharged, and the tag is registered here.

theorem exists_strictTransformSpace_comp_iso_unconditional (Z : ClosedSubspaces B S hS A.1)
    (Z' : ClosedSubspaces B S hS A'.1) (Y : ClosedSubspaces B S hS A.1)
    (hb : IsBlowupAlong B S hS Z b) (hc : IsBlowupAlong B S hS Z' c)
    (hY : IsCompositeCentre B S hS b Z Z' Y) (hd : IsBlowupAlong B S hS Y (c ≫ b)) :
    ∃ (k : strictTransformPullback B S hS
          (strictTransformSpaceToBlowUp B S hS f b (Z.1.preimage b.hom)) c ⟶
        strictTransformPullback B S hS f (c ≫ b))
      (j : strictTransformSpace B S hS
          (strictTransformSpaceToBlowUp B S hS f b (Z.1.preimage b.hom)) c
          (Z'.1.preimage c.hom) ≅
        strictTransformSpace B S hS f (c ≫ b) (Y.1.preimage (c ≫ b).hom)),
      (k ≫ strictTransformPullbackToSource B S hS f (c ≫ b) =
        strictTransformPullbackToSource B S hS
            (strictTransformSpaceToBlowUp B S hS f b (Z.1.preimage b.hom)) c ≫
          strictTransformSpaceι B S hS f b (Z.1.preimage b.hom) ≫
            strictTransformPullbackToSource B S hS f b) ∧
      (k ≫ strictTransformPullbackToBlowUp B S hS f (c ≫ b) =
        strictTransformPullbackToBlowUp B S hS
          (strictTransformSpaceToBlowUp B S hS f b (Z.1.preimage b.hom)) c) ∧
      j.hom ≫ strictTransformSpaceι B S hS f (c ≫ b) (Y.1.preimage (c ≫ b).hom) =
        strictTransformSpaceι B S hS
            (strictTransformSpaceToBlowUp B S hS f b (Z.1.preimage b.hom)) c
            (Z'.1.preimage c.hom) ≫ k

Tag 0869, a lemma

Tag 0869 in the Stacks Project.

AlgebraicGeometry.Space.exists_strictTransformSheaf_shortComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformShortExact.lean, line 500. The attribute's comment: “partial: the short complex of strict transforms with its two maps pinned down by the quotient maps, monomorphic on the left and epimorphic on the right, all unconditional; exactness in the middle is NOT proved and is instead reduced, as an equivalence, to epimorphy of the induced map on the subsheaves of sections supported on the exceptional preimage — the statement that Stacks 0863 parts (2) and (3) together with the scheme-level Stacks 080W would supply and that this library cannot reach”.

Stacks 0869, as far as this library reaches it. In the situation of Stacks 0862, let 0 ⟶ F₁ ⟶ F₂ ⟶ F₃ ⟶ 0 be a sequence of 𝒪_X-modules which is short exact after every base change Y ⟶ A. Then the strict transforms of the Fᵢ relative to (b, E) form a short complex whose two maps are determined by the quotient maps onto the strict transforms; the left-hand map is a monomorphism and the right-hand map is an epimorphism, and exactness in the middle is equivalent to epimorphy of the morphism induced on the subsheaves of sections supported on the exceptional preimage.

Everything asserted here is unconditional. Exactness in the middle — the heart of the tag — is not proved; the last conjunct is the exact reduction of it, and the module documentation records what would discharge the reduced statement and why that input is absent.

theorem exists_strictTransformSheaf_shortComplex
    (hC : ∀ (Y P : AlgebraicSpaces B S hS) (t : Y ⟶ A) (pX : P ⟶ X) (pY : P ⟶ Y),
      IsPullback pX pY f t → (C.map (modulePullback B S hS pX)).ShortExact) :
    ∃ (f' : strictTransformSheaf B S hS f b E C.X₁ ⟶ strictTransformSheaf B S hS f b E C.X₂)
      (g' : strictTransformSheaf B S hS f b E C.X₂ ⟶ strictTransformSheaf B S hS f b E C.X₃)
      (w : f' ≫ g' = 0),
      Mono f' ∧ Epi g' ∧
      (strictTransformSheafQuotient B S hS f b E C.X₁ ≫ f' =
        (modulePullback B S hS (strictTransformPullbackToSource B S hS f b)).map C.f ≫
          strictTransformSheafQuotient B S hS f b E C.X₂) ∧
      (strictTransformSheafQuotient B S hS f b E C.X₂ ≫ g' =
        (modulePullback B S hS (strictTransformPullbackToSource B S hS f b)).map C.g ≫
          strictTransformSheafQuotient B S hS f b E C.X₃) ∧
      ((ShortComplex.mk f' g' w).Exact ↔
        Epi (supportedSectionsMap (exceptionalPreimageSet B S hS f b E)
          ((modulePullback B S hS (strictTransformPullbackToSource B S hS f b)).map C.g)))

AlgebraicGeometry.Space.exists_strictTransformSheaf_shortComplex_of_isBlowupAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformShortExactBlowup.lean, line 89. The attribute's comment: “the strict transforms of a short exact sequence of quasi-coherent modules which stays short exact after every base change again form a short exact sequence, with its two maps pinned down by the quotient maps onto the strict transforms”.

Stacks 0869. In the situation of Stacks 0862 — a blowup b : A' ⟶ A of an algebraic space A in a closed subspace Z, with exceptional divisor E = b^{-1}Z, and an algebraic space f : X ⟶ A over A — let 0 ⟶ F₁ ⟶ F₂ ⟶ F₃ ⟶ 0 be a sequence of quasi-coherent 𝒪_X-modules which is short exact after every base change Y ⟶ A. Then the strict transforms of the Fᵢ form a short complex whose two maps are determined by the quotient maps onto the strict transforms, the left-hand map is a monomorphism, the right-hand map is an epimorphism, and the complex is exact in the middle: the strict transforms form a short exact sequence.

The strict transform is the one of Stacks 0862, AlgebraicGeometry.Space.strictTransformSheaf, and "being the blowup of A in Z" is AlgebraicGeometry.Space.IsBlowupAlong, the universal property of Stacks 085U, since Stacks 085Q constructs no blowup of an algebraic space in this library.

theorem exists_strictTransformSheaf_shortComplex_of_isBlowupAlong {Z : ClosedSubspaces B S hS A.1}
    {b : A' ⟶ A}
    (hb : IsBlowupAlong B S hS Z b) (C : ShortComplex (Modules.{u, u} B S hS X.1 X.2))
    (hqc₁ : C.X₁.IsQuasicoherentOnSite) (hqc₂ : C.X₂.IsQuasicoherentOnSite)
    (hqc₃ : C.X₃.IsQuasicoherentOnSite)
    (hC : ∀ (Y P : AlgebraicSpaces B S hS) (t : Y ⟶ A) (pX : P ⟶ X) (pY : P ⟶ Y),
      IsPullback pX pY f t → (C.map (modulePullback B S hS pX)).ShortExact) :
    ∃ (f' : strictTransformSheaf B S hS f b (Z.1.preimage b.hom) C.X₁ ⟶
          strictTransformSheaf B S hS f b (Z.1.preimage b.hom) C.X₂)
      (g' : strictTransformSheaf B S hS f b (Z.1.preimage b.hom) C.X₂ ⟶
          strictTransformSheaf B S hS f b (Z.1.preimage b.hom) C.X₃)
      (w : f' ≫ g' = 0),
      Mono f' ∧ Epi g' ∧
      (strictTransformSheafQuotient B S hS f b (Z.1.preimage b.hom) C.X₁ ≫ f' =
        (modulePullback B S hS (strictTransformPullbackToSource B S hS f b)).map C.f ≫
          strictTransformSheafQuotient B S hS f b (Z.1.preimage b.hom) C.X₂) ∧
      (strictTransformSheafQuotient B S hS f b (Z.1.preimage b.hom) C.X₂ ≫ g' =
        (modulePullback B S hS (strictTransformPullbackToSource B S hS f b)).map C.g ≫
          strictTransformSheafQuotient B S hS f b (Z.1.preimage b.hom) C.X₃) ∧
      (ShortComplex.mk f' g' w).Exact

Tag 0D0P, a lemma

Tag 0D0P in the Stacks Project.

AlgebraicGeometry.Space.strictTransformSheaf_isLocallyGeneratedByOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformLocalGenerators.lean, line 922.

Let F be a finite type quasi-coherent module on an algebraic space Bsp, let Z ⊆ Bsp be the closed subspace cut out by the k-th Fitting ideal sheaf of F, and let b : Bsp' ⟶ Bsp be the blowup of Bsp in Z. Then the strict transform of F can locally be generated by k sections.

theorem strictTransformSheaf_isLocallyGeneratedByOnSite
    {Bsp Bsp' : AlgebraicSpaces B S hS} (F : Modules.{u, u} B S hS Bsp.1 Bsp.2) (k : ℕ)
    (Z : ClosedSubspaces B S hS Bsp.1)
    (hZ : definingIdealSheaf B S hS Bsp Z = fittingIdeal B S hS Bsp.1 Bsp.2 F k)
    {b : Bsp' ⟶ Bsp} (hb : IsBlowupAlong B S hS Z b) (hFqc : F.IsQuasicoherentOnSite)
    (hFfin : ∀ W : SmallEtale B S hS Bsp.1,
      IsAffine ((SmallEtale.toOver B S hS Bsp.1 ⋙ BigFppfOver.toScheme B S hS).obj W) →
        Module.Finite (chartRing B S hS Bsp.1 Bsp.2 W) (F.val.obj (op W))) :
    SheafOfModules.IsLocallyGeneratedByOnSite
      (strictTransformSheaf B S hS (𝟙 Bsp) b (preimageClosedSubspace b Z).1 F) k

Tag 0D0Q, a lemma

Tag 0D0Q in the Stacks Project.

AlgebraicGeometry.Space.isFiniteLocallyFreeOfRank_strictTransformSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformFittingRank.lean, line 518.

Let F be a finite type quasi-coherent module on an algebraic space Bsp, let Z ⊆ Bsp be the closed subspace cut out by the k-th Fitting ideal sheaf of F, let b : Bsp' ⟶ Bsp be the blowup of Bsp in Z, and assume that F is locally free of rank k on the open complement Bsp ∖ Z. Then the strict transform of F is locally free of rank k.

theorem isFiniteLocallyFreeOfRank_strictTransformSheaf
    {Bsp Bsp' : AlgebraicSpaces B S hS} (F : Modules.{u, u} B S hS Bsp.1 Bsp.2) (k : ℕ)
    (Z : ClosedSubspaces B S hS Bsp.1)
    (hZ : definingIdealSheaf B S hS Bsp Z = fittingIdeal B S hS Bsp.1 Bsp.2 F k)
    {b : Bsp' ⟶ Bsp} (hb : IsBlowupAlong B S hS Z b) (hFqc : F.IsQuasicoherentOnSite)
    (hFfin : ∀ W : SmallEtale B S hS Bsp.1,
      IsAffine ((SmallEtale.toOver B S hS Bsp.1 ⋙ BigFppfOver.toScheme B S hS).obj W) →
        Module.Finite (chartRing B S hS Bsp.1 Bsp.2 W) (F.val.obj (op W)))
    (h : RingedSite.IsFiniteLocallyFreeOfRank
      (smallEtaleRingedSite B S hS (openComplementSpace B S hS Bsp Z).1
        (openComplementSpace B S hS Bsp Z).2)
      ((modulePullback B S hS (openComplementHom B S hS Bsp Z)).obj F) k) :
    RingedSite.IsFiniteLocallyFreeOfRank
      (smallEtaleRingedSite B S hS (strictTransformPullback B S hS (𝟙 Bsp) b).1
        (strictTransformPullback B S hS (𝟙 Bsp) b).2)
      (strictTransformSheaf B S hS (𝟙 Bsp) b (preimageClosedSubspace b Z).1 F) k

Sources

• Section 71.18, Tag 0861
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.strictTransformSheaf · AlgebraicGeometry.Space.strictTransform · AlgebraicGeometry.Space.isEtale_baseChange_blowup_of_isEtale · AlgebraicGeometry.Space.exists_isEtale_strictTransformSheaf_restriction · AlgebraicGeometry.Space.exists_strictTransform_eq_preimage_of_isBlowupAlong · AlgebraicGeometry.Space.exists_strictTransform_eq_preimage · AlgebraicGeometry.Space.exists_strictTransform_eq_preimage_strictTransformSheaf_iso · AlgebraicGeometry.Space.isBlowupAlong_strictTransform

Section71.19 Admissible blowups#

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

Tag 086B, a definition

Tag 086B in the Stacks Project.

AlgebraicGeometry.Space.IsAdmissibleBlowup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AdmissibleBlowup.lean, line 229.

Stacks 086B. A morphism f : X' ⟶ X of algebraic spaces over S is a U-admissible blowup, for an open subspace U ⊆ X, when there is a closed subspace Z ⊆ X whose closed immersion into X is of finite presentation and whose points are disjoint from those of U, such that f exhibits X' as the blowup of X in Z.

Being the blowup of X in Z is AlgebraicGeometry.Space.IsBlowupAlong, the universal property of Tag 085U: f is a terminal object of the category of algebraic spaces over X on which the inverse image of Z is an effective Cartier divisor. Since terminal objects are unique up to unique isomorphism and the blowup of X in Z is such a terminal object, this is the source's "X' is isomorphic to the blowup of X in Z"; see the module documentation, and AlgebraicGeometry.Space.IsAdmissibleBlowup.exists_iso_blowup for that reading as a theorem.

abbrev IsAdmissibleBlowup (U : OpenSubspaces B S hS X.1) (f : X' ⟶ X) : Prop

Tag 086C, a lemma

Tag 086C in the Stacks Project.

AlgebraicGeometry.Space.isAdmissibleBlowup_comp_of_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AdmissibleBlowupComposition.lean, line 47.

Let S be a scheme, let X be a quasi-compact and quasi-separated algebraic space over S and let U ⊆ X be an open subspace. Let b : X' ⟶ X be a U-admissible blowup and let c : X'' ⟶ X' be a U-admissible blowup. Then the composition c ≫ b : X'' ⟶ X is a U-admissible blowup.

Since b is an isomorphism over U, the source regards U as an open subspace of X' as well; as a subspace of X' it is the inverse image b⁻¹(U), which is how the admissibility of c is stated. Quasi-separatedness of X is absolute quasi-separatedness, which needs the terminal scheme in the site (hZ). The source also takes U quasi-compact; that hypothesis is not needed and is omitted.

theorem isAdmissibleBlowup_comp_of_isQuasiCompactSpace
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    (hZ : B.Contains (⊤_ Scheme.{u})) (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (U : OpenSubspaces B S hS X.1) {b : X' ⟶ X} {c : X'' ⟶ X'}
    (hb : IsAdmissibleBlowup B S hS U b)
    (hc : IsAdmissibleBlowup B S hS
      ⟨U.1.preimage b.hom, isOpenSubspace_preimage B S hS b.hom U.1 X.2 X'.2 U.2⟩ c) :
    IsAdmissibleBlowup B S hS U (c ≫ b)

Tag 086D, a lemma

Tag 086D in the Stacks Project.

AlgebraicGeometry.Space.IsBlowupAlong.exists_restrictionToOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AdmissibleBlowupExtension.lean, line 201. The attribute's comment: “unconditional: the restriction over an open subspace V of the blowup of X in Z is the blowup of V in Z ∩ V”.

The blowup of X in a closed subspace Z restricts, over an open subspace V ⊆ X, to the blowup of V in Z ∩ V. This is the clause "whose restriction to V is V'" of Tag 086D, and the one step of its proof that the universal property of Tag 085U supplies on its own.

The inverse image f⁻¹(V) is an open subspace of X' and exhibits a cartesian square over V ⊆ X by Tag 083Q; the inclusion of an open subspace is étale, hence flat, so AlgebraicGeometry.Space.IsBlowupAlong.of_isPullback_of_isFlat applies.

theorem IsBlowupAlong.exists_restrictionToOpen {X X' : AlgebraicSpaces B S hS} {f : X' ⟶ X}
    (V : OpenSubspaces B S hS X.1) (Z : ClosedSubspaces B S hS X.1)
    (hf : IsBlowupAlong B S hS Z f) :
    ∃ (P : AlgebraicSpaces B S hS) (p : P ⟶ openSubspace B S hS X V) (q : P ⟶ X'),
      IsPullback p q (openSubspaceι B S hS X V) f ∧
        IsBlowupAlong B S hS (closedSubspaceRestrict B S hS X V Z) p

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

Stacks 086D. Let X be a quasi-compact and quasi-separated algebraic space over S, let U, V ⊆ X be quasi-compact open subspaces and let b : V' ⟶ V be a U ∩ V-admissible blowup. Then there is a U-admissible blowup f : X' ⟶ X whose restriction to V is V', the restriction being recorded as a cartesian square.

The extension of the centre is AlgebraicGeometry.Space.exists_closedSubspace_extension_disjoint: the centre W ⊆ V of b, together with the empty closed subspace on U, extends to a finitely presented Z ⊆ X whose points avoid those of U and with Z ∩ V = W, by the induction principle of Stacks 08GP. The blowup of X in Z exists by AlgebraicGeometry.Space.exists_isBlowupAlong_of_isFinitePresentation, it is U-admissible, and by AlgebraicGeometry.Space.IsBlowupAlong.exists_restrictionToOpen its restriction to V is the blowup of V in Z ∩ V = W, hence isomorphic over V to V'.

theorem exists_isAdmissibleBlowup_isPullback'
    (hZ : B.Contains (⊤_ Scheme.{u})) {X V' : AlgebraicSpaces B S hS}
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (U V : OpenSubspaces B S hS X.1)
    (hUqc : IsQuasiCompactSpace B S hS U.1.toFunctor)
    (hVqc : IsQuasiCompactSpace B S hS V.1.toFunctor)
    (b : V' ⟶ openSubspace B S hS X V)
    (hb : IsAdmissibleBlowup B S hS (openSubspaceRestrict B S hS X V U) b) :
    ∃ (X' : AlgebraicSpaces B S hS) (f : X' ⟶ X), IsAdmissibleBlowup B S hS U f ∧
      ∃ e : V' ⟶ X', IsPullback b e (openSubspaceι B S hS X V) f

Tag 086E, a lemma

Tag 086E in the Stacks Project.

AlgebraicGeometry.Space.exists_isAdmissibleBlowup_factoring, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AdmissibleBlowupDominating.lean, line 425. The attribute's comment: “clause (a): a U-admissible blowup factoring through each member of a finite family of U-admissible blowups, with no assumed inputs beyond the Stacks 085Q construction data for X -- a presentation P, the HasSheafify universe choice, and the three B.Contains side conditions on the relative Projs, asked for EVERY closed subspace of X because the centre is the sum of the given centres and is built inside the proof, so it cannot be named in advance -- none of which occurs in the conclusion”.

Stacks 086E, clause (a). Let S be a scheme, let X be a quasi-compact and quasi-separated algebraic space over S, let U ⊆ X be a quasi-compact open subspace and let b i : X i ⟶ X, i : ι with ι finite, be U-admissible blowups. There is a U-admissible blowup c : X' ⟶ X which factors as X' ⟶ X i ⟶ X for every i.

Take for X' the blowup of X in the sum Z i₀ + Z i₁ + ⋯ of the centres of the given blowups, Stacks 083U; the sum of finitely many finitely presented centres disjoint from U is again finitely presented (AlgebraicGeometry.Space.isFinitePresentation_ι_sumClosedSubspaces) and disjoint from U (AlgebraicGeometry.Space.subspacePointSet_sumClosedSubspaces), so c is U-admissible. The inverse image of the sum along c is an effective Cartier divisor, hence so is the inverse image of each summand Z i by Stacks 083W, and the universal property of b i, Stacks 085U, then produces the factorisation through b i. For the empty family the identity of X is a U-admissible blowup, being the blowup in the empty closed subspace.

The hypotheses beyond the source's are the construction data of Stacks 085Q for the blowup of X: an étale presentation P of X, the universe choice HasSheafify for the quotient presheaf, and the three B.Contains smallness side conditions on the relative Projs, asked for every closed subspace of X since the centre is built inside the proof. None of these says anything about blowups; they are exactly what AlgebraicGeometry.Space.isBlowupAlong_blowUpAlongHom' takes.

theorem exists_isAdmissibleBlowup_factoring
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    (hZtop : B.Contains (⊤_ Scheme.{u})) (X : AlgebraicSpaces B S hS)
    (_hXqc : IsQuasiCompactSpace B S hS X.1)
    (_hXqs : IsAbsolutelyQuasiSeparated B S hS hZtop X.1)
    (U : OpenSubspaces B S hS X.1)
    (_hUqc : IsQuasiCompactSpace B S hS U.1.toFunctor)
    {ι : Type v} [Finite ι] (Xi : ι → AlgebraicSpaces B S hS) (b : ∀ i, Xi i ⟶ X)
    (hb : ∀ i, IsAdmissibleBlowup B S hS U (b i))
    (P : Presentation B S hS X.obj X.property)
    (hc : ∀ K : ClosedSubspaces B S hS X.obj,
      B.Contains (reesChartSituation (centreIdeal K)
          (isCartesianOnAffineCharts_centreIdeal K) P).relativeProj ∧
        B.Contains (reesRelationSituation (centreIdeal K)
          (isCartesianOnAffineCharts_centreIdeal K) P).relativeProj ∧
          B.Contains (reesDoubleSituation (centreIdeal K)
            (isCartesianOnAffineCharts_centreIdeal K) P).relativeProj) :
    ∃ (X' : AlgebraicSpaces B S hS) (c : X' ⟶ X), IsAdmissibleBlowup B S hS U c ∧
      ∃ g : ∀ i, X' ⟶ Xi i, ∀ i, g i ≫ b i = c

AlgebraicGeometry.Space.exists_isAdmissibleBlowup_factoring_isAdmissibleBlowup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AdmissibleBlowupDominating.lean, line 497. The attribute's comment: “clause (b): the factor morphisms of the dominating blowup are themselves admissible blowups, with no assumed inputs beyond the Stacks 085Q construction data for X and for the X i -- presentations P and Pi, the HasSheafify universe choice, and the B.Contains side conditions on the relative Projs, asked for EVERY closed subspace of X and of each X i because the centres are built inside the proof and cannot be named in advance -- none of which occurs in the conclusion”.

Stacks 086E, clause (b). In the situation of clause (a) the dominating U-admissible blowup c : X' ⟶ X can be chosen so that, in addition, each factor morphism g i : X' ⟶ X i is itself a b i⁻¹(U)-admissible blowup.

Writing the centre of c as Z i + J i — every member of the family is a summand of the sum, AlgebraicGeometry.Space.exists_eq_sumClosedSubspaces_of_mem — the blowup c i of X i in the inverse image of J i exists by Stacks 085Q and 085U, and Stacks 085Y identifies the composite c i ≫ b i with the blowup of X in Z i + J i, the input it needs being Stacks 085X for c i and the exceptional divisor of b i (AlgebraicGeometry.Space.isPullbackDefined_of_isBlowupAlong). Blowups in a fixed centre are isomorphic over the base, so X' is isomorphic over X to the source of c i ≫ b i, and the factor morphism transported along that isomorphism is again the blowup of X i in the inverse image of J i. That centre is finitely presented (a base change of J i) and disjoint from b i⁻¹(U) (the inverse image of a disjointness), so the factor morphism is b i⁻¹(U)-admissible. For the empty family the identity of X is the blowup in the empty closed subspace and there is nothing to factor.

The hypotheses beyond the source's are the construction data of Stacks 085Q, now also for each X i because the second blowup of the tower is formed there: étale presentations P of X and Pi i of X i, the universe choice HasSheafify, and the B.Contains smallness side conditions on the relative Projs. None of them occurs in the conclusion, and none says anything about blowups.

theorem exists_isAdmissibleBlowup_factoring_isAdmissibleBlowup
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    (hZtop : B.Contains (⊤_ Scheme.{u})) (X : AlgebraicSpaces B S hS)
    (_hXqc : IsQuasiCompactSpace B S hS X.1)
    (_hXqs : IsAbsolutelyQuasiSeparated B S hS hZtop X.1)
    (U : OpenSubspaces B S hS X.1)
    (_hUqc : IsQuasiCompactSpace B S hS U.1.toFunctor)
    {ι : Type v} [Finite ι] (Xi : ι → AlgebraicSpaces B S hS) (b : ∀ i, Xi i ⟶ X)
    (hb : ∀ i, IsAdmissibleBlowup B S hS U (b i))
    (P : Presentation B S hS X.obj X.property)
    (hc : ∀ K : ClosedSubspaces B S hS X.obj,
      B.Contains (reesChartSituation (centreIdeal K)
          (isCartesianOnAffineCharts_centreIdeal K) P).relativeProj ∧
        B.Contains (reesRelationSituation (centreIdeal K)
          (isCartesianOnAffineCharts_centreIdeal K) P).relativeProj ∧
          B.Contains (reesDoubleSituation (centreIdeal K)
            (isCartesianOnAffineCharts_centreIdeal K) P).relativeProj)
    (Pi : ∀ i, Presentation B S hS (Xi i).obj (Xi i).property)
    (hci : ∀ (i : ι) (K : ClosedSubspaces B S hS (Xi i).obj),
      B.Contains (reesChartSituation (centreIdeal K)
          (isCartesianOnAffineCharts_centreIdeal K) (Pi i)).relativeProj ∧
        B.Contains (reesRelationSituation (centreIdeal K)
          (isCartesianOnAffineCharts_centreIdeal K) (Pi i)).relativeProj ∧
          B.Contains (reesDoubleSituation (centreIdeal K)
            (isCartesianOnAffineCharts_centreIdeal K) (Pi i)).relativeProj) :
    ∃ (X' : AlgebraicSpaces B S hS) (c : X' ⟶ X), IsAdmissibleBlowup B S hS U c ∧
      ∃ g : ∀ i, X' ⟶ Xi i, (∀ i, g i ≫ b i = c) ∧
        ∀ i, IsAdmissibleBlowup B S hS
          ⟨U.1.preimage (b i).hom,
            isOpenSubspace_preimage B S hS (b i).hom U.1 X.2 (Xi i).2 U.2⟩ (g i)

Tag 086F, a lemma

Tag 086F in the Stacks Project.

AlgebraicGeometry.Space.exists_isAdmissibleBlowup_disjoint_openSubspace_decomposition', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AdmissibleBlowupSeparationQuasiCompact.lean, line 117.

Stacks 086F. Let S be a scheme, let X be a quasi-compact and quasi-separated algebraic space over S and let U, V ⊆ X be quasi-compact open subspaces with disjoint sets of points. Then there is a U ∪ V-admissible blowup b : X' ⟶ X such that X' is the disjoint union of two open subspaces X' = X'₁ ⊔ X'₂ with b⁻¹(U) ⊆ X'₁ and b⁻¹(V) ⊆ X'₂.

"X' is the disjoint union of X'₁ and X'₂" is recorded as follows: the two are open and closed subspaces with complementary sets of points, whose join sheafifies to X' and whose meet is the sheafification of the bottom subfunctor.

Two finitely presented closed subspaces Z₁, Z₂ with |Z₁| ∩ |U| = ∅, |Z₂| ∩ |V| = ∅ and |Z₁| ∪ |Z₂| = |X| are produced by two applications of AlgebraicGeometry.Space.exists_closedSubspace_disjoint_superset, the second to V and the quasi-compact open complement of Z₁; the blowup in Z₁ ∩ Z₂ is then the one sought, by exists_isAdmissibleBlowup_disjoint_openSubspace_decomposition_of_closedSubspaces.

theorem exists_isAdmissibleBlowup_disjoint_openSubspace_decomposition'
    (hZ : B.Contains (⊤_ Scheme.{u})) {X : AlgebraicSpaces B S hS}
    (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (U V : OpenSubspaces B S hS X.1)
    (hUqc : IsQuasiCompactSpace B S hS U.1.toFunctor)
    (hVqc : IsQuasiCompactSpace B S hS V.1.toFunctor)
    (hUV : Disjoint (subspacePointSet B S hS X.1 U.1) (subspacePointSet B S hS X.1 V.1)) :
    ∃ (X' : AlgebraicSpaces B S hS) (b : X' ⟶ X) (X'₁ X'₂ : OpenSubspaces B S hS X'.1),
      IsAdmissibleBlowup B S hS (openSubspaceUnion B S hS X U V) b ∧
        IsClosedSubspace B S hS X'₁.1 ∧ IsClosedSubspace B S hS X'₂.1 ∧
          Disjoint (subspacePointSet B S hS X'.1 X'₁.1)
            (subspacePointSet B S hS X'.1 X'₂.1) ∧
            subspacePointSet B S hS X'.1 X'₁.1 ∪ subspacePointSet B S hS X'.1 X'₂.1
                = Set.univ ∧
              (X'₁.1 ⊔ X'₂.1).sheafify (BigFppfOver.topology B S hS) = ⊤ ∧
                X'₁.1 ⊓ X'₂.1
                    = (⊥ : Subfunctor X'.1).sheafify (BigFppfOver.topology B S hS) ∧
                  U.1.preimage b.hom ≤ X'₁.1 ∧ V.1.preimage b.hom ≤ X'₂.1

Sources

• Section 71.19, Tag 086A
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsAdmissibleBlowup · AlgebraicGeometry.Space.isAdmissibleBlowup_comp_of_isQuasiCompactSpace · AlgebraicGeometry.Space.IsBlowupAlong.exists_restrictionToOpen · AlgebraicGeometry.Space.exists_isAdmissibleBlowup_isPullback' · AlgebraicGeometry.Space.exists_isAdmissibleBlowup_factoring · AlgebraicGeometry.Space.exists_isAdmissibleBlowup_factoring_isAdmissibleBlowup · AlgebraicGeometry.Space.exists_isAdmissibleBlowup_disjoint_openSubspace_decomposition'

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.