31.25 Meromorphic functions and… to 31.37 Modifications
Section31.25 Meromorphic functions and sections; Noetherian case#
Section 31.25 of the Stacks Project, Tag 0EMG. 5 tags here are carried by 34 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 08I7, a lemma
Tag 08I7 in the Stacks Project.
AlgebraicGeometry.pow_mul_eq_zero_of_res_basicOpen_eq_zero, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/BasicOpenVanishing.lean, line 148.
A meromorphic function on a quasi-compact open which vanishes on the basic open of a regular function there is annihilated by a power of that regular function.
lemma pow_mul_eq_zero_of_res_basicOpen_eq_zero
(X : Scheme.{u}) {W : X.Opens} (hW : IsCompact (W : Set X)) (h : Γ(X, W))
(f : X.totalQuotientSheaf.presheaf.obj (op W))
(hf : X.totalQuotientSheaf.presheaf.map
(homOfLE (X.basicOpen_le h)).op f = 0) :
∃ n : ℕ,
(X.toTotalQuotientSheaf.hom.app (op W)).hom h ^ n * f = 0
AlgebraicGeometry.pow_mul_eq_zero_of_restrict_basicOpen_eq_zero, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/BasicOpenVanishing.lean, line 174.
A meromorphic function vanishing on the basic open of a global regular function is annihilated by a power of that regular function.
lemma pow_mul_eq_zero_of_restrict_basicOpen_eq_zero
(X : Scheme.{u}) [CompactSpace X] (h : Γ(X, ⊤))
(f : X.totalQuotientSheaf.presheaf.obj (op ⊤))
(hf : X.totalQuotientSheaf.presheaf.map
(homOfLE (X.basicOpen_le h)).op f = 0) :
∃ n : ℕ,
(X.toTotalQuotientSheaf.hom.app (op ⊤)).hom h ^ n * f = 0
Tag 02OV, a lemma
Tag 02OV in the Stacks Project.
AlgebraicGeometry.stalk_totalQuotientSheaf_isFractionRing_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/NoetherianSheafSections.lean, line 144. The attribute's comment: “part (1), for the sheaf”. References: EGA IV (21.6.7), “partial”.
At every point of a locally Noetherian scheme the stalk of the sheaf of meromorphic functions is the total quotient ring of the local ring.
theorem stalk_totalQuotientSheaf_isFractionRing_of_isLocallyNoetherian
(X : Scheme.{u}) [IsLocallyNoetherian X] (x : X) :
letI : Algebra (X.presheaf.stalk x) (X.totalQuotientSheaf.presheaf.stalk x) :=
((TopCat.Presheaf.stalkFunctor CommRingCat x).map
X.toTotalQuotientSheaf.hom).hom.toAlgebra
IsFractionRing (X.presheaf.stalk x) (X.totalQuotientSheaf.presheaf.stalk x)
AlgebraicGeometry.isLocalization_totalQuotientSheaf_obj_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/NoetherianSheafSections.lean, line 240. The attribute's comment: “part (2)”.
The sheaf of meromorphic functions on an affine open of a locally Noetherian scheme. The sections of
K_Xover an affine openUform the total quotient ring ofΓ(X, U).
theorem isLocalization_totalQuotientSheaf_obj_of_isLocallyNoetherian
(X : Scheme.{u}) [IsLocallyNoetherian X] (U : X.Opens) (hU : IsAffineOpen U) :
letI : Algebra Γ(X, U) (X.totalQuotientSheaf.presheaf.obj (op U)) :=
(X.toTotalQuotientSheaf.hom.app (op U)).hom.toAlgebra
IsLocalization Γ(X, U)⁰ (X.totalQuotientSheaf.presheaf.obj (op U))
AlgebraicGeometry.isLocalization_totalQuotientPresheaf_obj_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/Stalks.lean, line 57. The attribute's comment: “affine_total_quotient”.
On an affine open of a scheme, meromorphic functions form the total quotient ring of the ring of regular functions. No Noetherian hypothesis is needed: the denominator submonoid of the total quotient presheaf on an affine open is already all of
nonZeroDivisors Γ(X, U).
theorem isLocalization_totalQuotientPresheaf_obj_of_isAffineOpen
(X : Scheme.{u}) (U : X.Opens)
(hU : IsAffineOpen U) :
letI : Algebra Γ(X, U)
((X.presheaf.totalQuotientPresheaf).obj (Opposite.op U)) :=
(X.presheaf.toTotalQuotientPresheaf.app (Opposite.op U)).hom.toAlgebra
IsLocalization (nonZeroDivisors Γ(X, U))
((X.presheaf.totalQuotientPresheaf).obj (Opposite.op U))
AlgebraicGeometry.regularSectionGerms_eq_nonZeroDivisors_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/Stalks.lean, line 200. The attribute's comment: “regular_stalk”.
At a point of a locally Noetherian scheme, the germs of regular local sections are exactly the non-zero-divisors in the local ring.
theorem regularSectionGerms_eq_nonZeroDivisors_of_isLocallyNoetherian
(X : Scheme.{u}) [IsLocallyNoetherian X] (x : X) :
(⨆ (U : Opens X) (hx : x ∈ U),
((X.presheaf.submonoidPresheafOfStalk
(fun y ↦ nonZeroDivisors (X.presheaf.stalk y))).obj (Opposite.op U)).map
(X.presheaf.germ U x hx).hom) =
nonZeroDivisors (X.presheaf.stalk x)
AlgebraicGeometry.stalk_totalQuotientPresheaf_isFractionRing_of_isLocallyNoetherian, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/Stalks.lean, line 227. The attribute's comment: “stalk_total_quotient”. References: EGA IV (21.6.7), “partial”.
At every point of a locally Noetherian scheme, the stalk of the presheaf of meromorphic functions is the total quotient ring of the local ring.
lemma stalk_totalQuotientPresheaf_isFractionRing_of_isLocallyNoetherian
(X : Scheme.{u}) [IsLocallyNoetherian X] (x : X) :
letI : Algebra (X.presheaf.stalk x) (X.presheaf.totalQuotientPresheaf.stalk x) :=
((TopCat.Presheaf.stalkFunctor CommRingCat x).map
X.presheaf.toTotalQuotientPresheaf).hom.toAlgebra
IsFractionRing (X.presheaf.stalk x) (X.presheaf.totalQuotientPresheaf.stalk x)
Tag 0EMH, a lemma
Tag 0EMH in the Stacks Project.
Stacks.AlgebraicGeometry.GenericPointCoproduct.meromorphicFunctions_iso_coproduct_of_noEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericPointCoproduct/Decomposition.lean, line 116. The attribute's comment: “meromorphic functions as a direct sum”.
Stacks Project, Tag 0EMH. On a locally Noetherian scheme without embedded points, the
𝒪_X-module of meromorphic functions is the direct sum, over the generic points of the irreducible components, of the structure sheaves of the local schemes there, pushed forward toX.
theorem meromorphicFunctions_iso_coproduct_of_noEmbeddedPoints (X : Scheme.{u})
[IsLocallyNoetherian X] (hX : AlgebraicGeometry.HasNoEmbeddedPoints X) :
Nonempty (meromorphicFunctions X ≅
∐ fun η : genericPoints X ↦ genericPointStalkModule X η)
Stacks.AlgebraicGeometry.GenericPointProduct.meromorphicFunctions_iso_product_of_noEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericPointProduct/Decomposition.lean, line 108. The attribute's comment: “meromorphic functions as a product”.
Stacks Project, Tag 0EMH. On a locally Noetherian scheme without embedded points, the
𝒪_X-module of meromorphic functions is the product, over the generic points of the irreducible components, of the structure sheaves of the local schemes there, pushed forward toX.
theorem meromorphicFunctions_iso_product_of_noEmbeddedPoints (X : Scheme.{u})
[IsLocallyNoetherian X] (hX : AlgebraicGeometry.HasNoEmbeddedPoints X) :
Nonempty (meromorphicFunctions X ≅
∏ᶜ fun η : genericPoints X ↦ genericPointStalkModule X η)
AlgebraicGeometry.nonempty_meromorphicSections_iso_product_genericPointStalks_of_hasNoEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Globalization.lean, line 696. The attribute's comment: “meromorphic sections as a product”.
Stacks 0EMH, the product decomposition of the sheaf of meromorphic sections.
theorem nonempty_meromorphicSections_iso_product_genericPointStalks_of_hasNoEmbeddedPoints
(X : Scheme.{u}) [IsLocallyNoetherian X] (hX : HasNoEmbeddedPoints X)
(F : X.Modules) [F.IsQuasicoherent] :
Nonempty (meromorphicSections X F ≅
∏ᶜ fun η : genericPoints X ↦ genericPointStalkModuleOf X F η)
AlgebraicGeometry.nonempty_meromorphicSections_iso_coproduct_genericPointStalks_of_hasNoEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Globalization.lean, line 707. The attribute's comment: “meromorphic sections as a direct sum”.
Stacks 0EMH, the direct-sum decomposition of the sheaf of meromorphic sections.
theorem nonempty_meromorphicSections_iso_coproduct_genericPointStalks_of_hasNoEmbeddedPoints
(X : Scheme.{u}) [IsLocallyNoetherian X] (hX : HasNoEmbeddedPoints X)
(F : X.Modules) [F.IsQuasicoherent] :
Nonempty (meromorphicSections X F ≅
∐ fun η : genericPoints X ↦ genericPointStalkModuleOf X F η)
AlgebraicGeometry.meromorphicSections_isQuasicoherent_of_hasNoEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Globalization.lean, line 718. The attribute's comment: “quasi-coherence of meromorphic sections”.
Stacks 0EMH, quasi-coherence of the sheaf of meromorphic sections.
theorem meromorphicSections_isQuasicoherent_of_hasNoEmbeddedPoints
(X : Scheme.{u}) [IsLocallyNoetherian X] (hX : HasNoEmbeddedPoints X)
(F : X.Modules) [F.IsQuasicoherent] :
(meromorphicSections X F).IsQuasicoherent
Stacks.AlgebraicGeometry.MeromorphicQuasicoherent.meromorphicFunctions_isQuasicoherent_of_noEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicQuasicoherent/Criteria.lean, line 80. The attribute's comment: “quasi-coherence of meromorphic functions”.
Stacks Project, Tag 0EMH. On a locally Noetherian scheme without embedded points, the sheaf of meromorphic functions is quasi-coherent.
theorem meromorphicFunctions_isQuasicoherent_of_noEmbeddedPoints (X : Scheme.{u})
[IsLocallyNoetherian X] (hX : AlgebraicGeometry.HasNoEmbeddedPoints X) :
(meromorphicFunctions X).IsQuasicoherent
Stacks.AlgebraicGeometry.MeromorphicSectionsTensor.meromorphicSections_isQuasicoherent_of_noEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicSectionsTensor/Quasicoherent.lean, line 89. The attribute's comment: “quasi-coherence of meromorphic sections”.
Stacks Project, Tag 0EMH, quasi-coherence of meromorphic sections. On a locally Noetherian scheme without embedded points, the sheaf of meromorphic sections of a quasi-coherent
𝒪_X-module is quasi-coherent.
theorem meromorphicSections_isQuasicoherent_of_noEmbeddedPoints (X : Scheme.{u})
[IsLocallyNoetherian X] (hX : AlgebraicGeometry.HasNoEmbeddedPoints X) (F : X.Modules)
(hF : F.IsQuasicoherent) :
(meromorphicSections X F).IsQuasicoherent
AlgebraicGeometry.exists_commRing_rationalFunctions_ringEquiv_totalQuotientSheaf_top_of_hasNoEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RationalFunctions/Meromorphic.lean, line 661. The attribute's comment: “rational functions are meromorphic functions”. References: EGA I (7.1.3), “special case”.
[Stacks, Tag 0EMH]: on a locally Noetherian scheme without embedded points, the ring of rational functions is the ring of global meromorphic functions.
theorem exists_commRing_rationalFunctions_ringEquiv_totalQuotientSheaf_top_of_hasNoEmbeddedPoints
(X : Scheme.{u}) [IsLocallyNoetherian X] (hX : HasNoEmbeddedPoints X) :
∃ _ : CommRing X.rationalFunctions,
(∀ (U : X.Opens) (hU : Dense (U : Set X)),
∃ ψ : Γ(X, U) →+* X.rationalFunctions,
∀ s, ψ s = X.rationalFunctionOfSection U hU s) ∧
Nonempty (X.rationalFunctions ≃+* X.totalQuotientSheaf.presheaf.obj (op ⊤))
Tag 0EMI, a lemma
Tag 0EMI in the Stacks Project.
AlgebraicGeometry.exists_isRegularMeromorphicSection_of_hasNoEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/RegularSectionExistence.lean, line 450.
[Stacks, Tag 0EMI], which is case (3) of [Stacks, Tag 02OZ]. An invertible sheaf of modules on a locally Noetherian scheme without embedded points has a regular meromorphic section.
theorem exists_isRegularMeromorphicSection_of_hasNoEmbeddedPoints (X : Scheme.{u})
[IsLocallyNoetherian X] (hX : HasNoEmbeddedPoints X) (L : X.Modules)
[AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L] :
∃ s : MeromorphicSection X.sheaf L, IsRegularMeromorphicSection X.sheaf L s
Tag 02P2, a lemma
Tag 02P2 in the Stacks Project.
AlgebraicGeometry.denominatorIdealSmul, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DenominatorAction.lean, line 131. The attribute's comment: “the product of the denominator ideal and the module”.
The product
I · Fof the ideal of denominators ofsand the moduleF: the image of the action ofIonF.
def denominatorIdealSmul : X.Modules
AlgebraicGeometry.denominatorIdealSmulι, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DenominatorAction.lean, line 136. The attribute's comment: “the first canonical map”.
The first canonical map, the inclusion
I · F ⟶ F.
def denominatorIdealSmulι : denominatorIdealSmul X L F s ⟶ F
AlgebraicGeometry.denominatorIdealBadLocus_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DenominatorAction.lean, line 161. The attribute's comment: “the exceptional subset is closed”.
The exceptional subset is closed.
Both cokernels are quotients of modules of finite type — the structure sheaf and the invertible sheaf
L, both coherent on a locally Noetherian scheme — so both supports are closed.Regularity of
sis not used: the source assumes it throughout Tag 02P2, but of the exceptional subset's two properties only nowhere denseness needs it.
theorem denominatorIdealBadLocus_isClosed [IsLocallyNoetherian X]
(hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
X.ringCatSheaf.property L) :
IsClosed (denominatorIdealBadLocus X L s)
AlgebraicGeometry.denominatorIdealBadLocus_isNowhereDense, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DenominatorAction.lean, line 179. The attribute's comment: “the exceptional subset is nowhere dense”.
The exceptional subset is nowhere dense: each of its two pieces is contained in a closed nowhere dense subset by [Stacks, Tag 02P0].
theorem denominatorIdealBadLocus_isNowhereDense
(hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
X.ringCatSheaf.property L)
(hs : IsRegularMeromorphicSection X.sheaf L s) :
IsNowhereDense (denominatorIdealBadLocus X L s)
AlgebraicGeometry.denominatorIdealSmul_inclusion_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DenominatorAction.lean, line 191. The attribute's comment: “injectivity of the first map”.
The first canonical map is injective: it is the inclusion of the image of the action map, hence the kernel of a cokernel projection.
theorem denominatorIdealSmul_inclusion_mono : Mono (denominatorIdealSmulι X L F s)
AlgebraicGeometry.denominatorIdealSmul_inclusion_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DenominatorAction.lean, line 225. The attribute's comment: “support of the first cokernel”.
The cokernel of the first canonical map is supported on the exceptional subset.
Off the support of
𝒪_X / Ithe stalk map of the ideal inclusion is surjective; tensoring withFand composing with the left unit constraint keeps it so, and the action map factors throughI · F, so the stalk map of the inclusionI · F ⟶ Fis surjective there as well.
theorem denominatorIdealSmul_inclusion_support :
SheafOfModules.supp (cokernel (denominatorIdealSmulι X L F s)) ⊆
denominatorIdealBadLocus X L s
AlgebraicGeometry.denominatorIdealSmulMul, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DenominatorAction.lean, line 387. The attribute's comment: “the second canonical map”.
The second canonical map
I · F ⟶ F ⊗ L, multiplication by the meromorphic section on the productI · F, together with the identity characterising it: its composite with the factorisation of the action map through its image is multiplication bysonI ⊗ F. Since that factorisation is an epimorphism the identity determines the map, so this is the canonical map and not an arbitrary one.
def denominatorIdealSmulMul [IsLocallyNoetherian X]
(hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
X.ringCatSheaf.property L)
(hs : IsRegularMeromorphicSection X.sheaf L s)
[F.IsCoherent] (hF : AlgebraicGeometry.HasNoEmbeddedAssociatedPoints F)
(hSupp : SheafOfModules.supp F = Set.univ) :
{ f : denominatorIdealSmul X L F s ⟶ Scheme.Modules.tensorObj F L //
Abelian.factorThruImage (denominatorIdealTensorAction X L F s) ≫ f =
denominatorIdealTensorMul X L F s }
AlgebraicGeometry.denominatorIdealSmulMul_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DenominatorAction.lean, line 403. The attribute's comment: “injectivity of the second map”.
The second canonical map is injective: the two maps out of
I ⊗ Fhave the same kernel, so the descents of each along the other's image factorisation are mutually inverse.
theorem denominatorIdealSmulMul_mono [IsLocallyNoetherian X]
(hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
X.ringCatSheaf.property L)
(hs : IsRegularMeromorphicSection X.sheaf L s)
[F.IsCoherent] (hF : AlgebraicGeometry.HasNoEmbeddedAssociatedPoints F)
(hSupp : SheafOfModules.supp F = Set.univ) :
Mono (denominatorIdealSmulMul X L F s hL hs hF hSupp).val
AlgebraicGeometry.denominatorIdealSmulMul_cokernel_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DenominatorAction.lean, line 421. The attribute's comment: “support of the second cokernel”.
The cokernel of the second canonical map is supported on the exceptional subset.
Off the support of
L / s(I)the stalk map of multiplication byson the ideal is surjective; tensoring withFand composing with the symmetry keeps it so, and multiplication bysonI ⊗ Ffactors throughI · F, so the stalk map of the second canonical map is surjective there as well.
theorem denominatorIdealSmulMul_cokernel_support [IsLocallyNoetherian X]
(hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
X.ringCatSheaf.property L)
(hs : IsRegularMeromorphicSection X.sheaf L s)
[F.IsCoherent] (hF : AlgebraicGeometry.HasNoEmbeddedAssociatedPoints F)
(hSupp : SheafOfModules.supp F = Set.univ) :
SheafOfModules.supp (cokernel (denominatorIdealSmulMul X L F s hL hs hF hSupp).val) ⊆
denominatorIdealBadLocus X L s
AlgebraicGeometry.denominatorIdealTimesModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/IdealTimesModule.lean, line 405. The attribute's comment: “the product of the denominator ideal and the module”.
The product
I F, as a subobject ofF.
noncomputable def denominatorIdealTimesModule
(L F : SheafOfModules.{u} X.ringCatSheaf)
(s : MeromorphicSection X.sheaf L) :
SheafOfModules.{u} X.ringCatSheaf
AlgebraicGeometry.denominatorIdealTimesModuleι, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/IdealTimesModule.lean, line 413. The attribute's comment: “the first canonical map”.
The inclusion
I F ⟶ F.
noncomputable def denominatorIdealTimesModuleι
(L F : SheafOfModules.{u} X.ringCatSheaf)
(s : MeromorphicSection X.sheaf L) :
denominatorIdealTimesModule X L F s ⟶ F
AlgebraicGeometry.denominatorBadLocus_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/IdealTimesModule.lean, line 466. The attribute's comment: “the exceptional subset is closed”.
If
Lis invertible andsis a regular meromorphic section ofLon a locally Noetherian scheme, thendenominatorBadLocus X L sis closed.
theorem denominatorBadLocus_isClosed
(L : SheafOfModules.{u} X.ringCatSheaf)
(s : MeromorphicSection X.sheaf L)
[IsLocallyNoetherian X]
(hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L)
(hs : IsRegularMeromorphicSection X.sheaf L s) :
IsClosed (denominatorBadLocus X L s)
AlgebraicGeometry.denominatorBadLocus_isNowhereDense, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/IdealTimesModule.lean, line 499. The attribute's comment: “the exceptional subset is nowhere dense”.
If
Lis invertible andsis a regular meromorphic section ofLon a locally Noetherian scheme, thendenominatorBadLocus X L sis nowhere dense.
theorem denominatorBadLocus_isNowhereDense
(L : SheafOfModules.{u} X.ringCatSheaf)
(s : MeromorphicSection X.sheaf L)
[IsLocallyNoetherian X]
(hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L)
(hs : IsRegularMeromorphicSection X.sheaf L s) :
IsNowhereDense (denominatorBadLocus X L s)
AlgebraicGeometry.denominatorIdealTimesModuleMul, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/IdealTimesModule.lean, line 871. The attribute's comment: “the second canonical map”.
The canonical section action, specified by its value on local products.
noncomputable def denominatorIdealTimesModuleMul
(L F : SheafOfModules.{u} X.ringCatSheaf)
(s : MeromorphicSection X.sheaf L)
[IsLocallyNoetherian X]
(hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L)
(hs : IsRegularMeromorphicSection X.sheaf L s)
[F.IsCoherent]
(hF : HasNoEmbeddedAssociatedPoints F)
(hSupp : (AlgebraicGeometry.SheafOfModules.moduleSheafOfModules F).supp = Set.univ) :
{ f : denominatorIdealTimesModule X L F s ⟶
(((Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u}
⟨X.toRingedSpace.presheaf, X.toRingedSpace.IsSheaf⟩).obj F).obj L) //
Abelian.factorThruImage (denominatorIdealAction X L F s) ≫ f =
denominatorIdealSectionTensor X L F s }
AlgebraicGeometry.denominatorIdealTimesModuleι_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/IdealTimesModule.lean, line 894. The attribute's comment: “injectivity of the first map”.
The inclusion
I F ⟶ Fis a monomorphism, becauseI Fis by definition the image of the action ofIonF.
theorem denominatorIdealTimesModuleι_mono
(L F : SheafOfModules.{u} X.ringCatSheaf)
(s : MeromorphicSection X.sheaf L) :
Mono (denominatorIdealTimesModuleι X L F s)
AlgebraicGeometry.denominatorIdealTimesModuleMul_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/IdealTimesModule.lean, line 903. The attribute's comment: “injectivity of the second map”.
Under the hypotheses of
denominatorIdealTimesModuleMul, the second canonical mapI F ⟶ F ⊗ Lis a monomorphism.
theorem denominatorIdealTimesModuleMul_mono
(L F : SheafOfModules.{u} X.ringCatSheaf)
(s : MeromorphicSection X.sheaf L)
[IsLocallyNoetherian X]
(hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L)
(hs : IsRegularMeromorphicSection X.sheaf L s)
[F.IsCoherent]
(hF : HasNoEmbeddedAssociatedPoints F)
(hSupp : (AlgebraicGeometry.SheafOfModules.moduleSheafOfModules F).supp = Set.univ) :
Mono (denominatorIdealTimesModuleMul X L F s hL hs hF hSupp).val
AlgebraicGeometry.denominatorIdealTimesModuleι_cokernel_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/IdealTimesModule.lean, line 919. The attribute's comment: “support of the first cokernel”.
The cokernel of the inclusion
I F ⟶ Fis supported ondenominatorBadLocus X L s.
theorem denominatorIdealTimesModuleι_cokernel_support
(L F : SheafOfModules.{u} X.ringCatSheaf)
(s : MeromorphicSection X.sheaf L) :
(AlgebraicGeometry.SheafOfModules.moduleSheafOfModules
(cokernel (denominatorIdealTimesModuleι X L F s))).supp ⊆
denominatorBadLocus X L s
AlgebraicGeometry.denominatorIdealTimesModuleMul_cokernel_supp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/IdealTimesModule.lean, line 938. The attribute's comment: “support of the second cokernel”.
Under the hypotheses of
denominatorIdealTimesModuleMul, the cokernel of the second canonical mapI F ⟶ F ⊗ Lis supported ondenominatorBadLocus X L s.
theorem denominatorIdealTimesModuleMul_cokernel_supp
(L F : SheafOfModules.{u} X.ringCatSheaf)
(s : MeromorphicSection X.sheaf L)
[IsLocallyNoetherian X]
(hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L)
(hs : IsRegularMeromorphicSection X.sheaf L s)
[F.IsCoherent]
(hF : HasNoEmbeddedAssociatedPoints F)
(hSupp : (AlgebraicGeometry.SheafOfModules.moduleSheafOfModules F).supp = Set.univ) :
(AlgebraicGeometry.SheafOfModules.moduleSheafOfModules
(cokernel (denominatorIdealTimesModuleMul X L F s hL hs hF hSupp).val)).supp ⊆
denominatorBadLocus X L s
Sources
Section31.26 Meromorphic functions and sections; reduced case#
Section 31.26 of the Stacks Project, Tag 0EMJ. 4 tags here are carried by 26 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02OW, a lemma
Tag 02OW in the Stacks Project.
AlgebraicGeometry.IsAffineOpen.isLocalization_totalQuotientPresheaf_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/StalksReduced.lean, line 56. The attribute's comment: “part (5)”.
On an affine open of any scheme, the meromorphic functions form the total quotient ring of the ring of regular functions: the localization at all nonzerodivisors.
theorem IsAffineOpen.isLocalization_totalQuotientPresheaf_obj
{X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U) :
letI : Algebra Γ(X, U)
((X.presheaf.totalQuotientPresheaf).obj (Opposite.op U)) :=
(X.presheaf.toTotalQuotientPresheaf.app (Opposite.op U)).hom.toAlgebra
IsLocalization (nonZeroDivisors Γ(X, U))
((X.presheaf.totalQuotientPresheaf).obj (Opposite.op U))
AlgebraicGeometry.regularSectionGerms_eq_nonZeroDivisors_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/StalksReduced.lean, line 76. The attribute's comment: “part (3)”.
On a reduced scheme whose quasi-compact opens have finitely many irreducible components, the germs of regular sections at every point are exactly the nonzerodivisors in its local ring.
theorem regularSectionGerms_eq_nonZeroDivisors_of_isReduced (X : Scheme.{u}) [IsReduced X]
(hfinite : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
(x : X) :
(⨆ (U : Opens X) (hx : x ∈ U),
((X.presheaf.submonoidPresheafOfStalk
(fun y ↦ nonZeroDivisors (X.presheaf.stalk y))).obj (Opposite.op U)).map
(X.presheaf.germ U x hx).hom) =
nonZeroDivisors (X.presheaf.stalk x)
AlgebraicGeometry.stalk_totalQuotientPresheaf_isFractionRing_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/StalksReduced.lean, line 91. The attribute's comment: “part (4)”.
On a reduced scheme whose quasi-compact opens have finitely many irreducible components, the stalk of the presheaf of meromorphic functions at any point is the total quotient ring of the local ring there.
theorem stalk_totalQuotientPresheaf_isFractionRing_of_isReduced (X : Scheme.{u}) [IsReduced X]
(hfinite : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
(x : X) :
letI : Algebra (X.presheaf.stalk x) (X.presheaf.totalQuotientPresheaf.stalk x) :=
((TopCat.Presheaf.stalkFunctor CommRingCat x).map
X.presheaf.toTotalQuotientPresheaf).hom.toAlgebra
IsFractionRing (X.presheaf.stalk x) (X.presheaf.totalQuotientPresheaf.stalk x)
Stacks.AlgebraicGeometry.GenericPointCoproduct.meromorphicFunctions_iso_coproduct_genericPointStalks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericPointCoproduct/Decomposition.lean, line 104. The attribute's comment: “generic-point direct sum”.
Stacks Project, Tag 02OW. On a reduced scheme whose quasi-compact opens have finitely many irreducible components, the
𝒪_X-module of meromorphic functions is the direct sum, over the generic points of the irreducible components, of the structure sheaves of the local schemes there, pushed forward toX.
theorem meromorphicFunctions_iso_coproduct_genericPointStalks (X : Scheme.{u}) [IsReduced X]
(hfinite : GenericPointProduct.FiniteComponentsOnCompactOpens X) :
Nonempty (meromorphicFunctions X ≅
∐ fun η : genericPoints X ↦ genericPointStalkModule X η)
Stacks.AlgebraicGeometry.GenericPointProduct.meromorphicFunctions_iso_product_genericPointStalks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GenericPointProduct/Decomposition.lean, line 63. The attribute's comment: “generic-point product”.
Stacks Project, Tag 02OW. On a reduced scheme whose quasi-compact opens have finitely many irreducible components, the
𝒪_X-module of meromorphic functions is the product, over the generic points of the irreducible components, of the structure sheaves of the local schemes there, pushed forward toX.
theorem meromorphicFunctions_iso_product_genericPointStalks (X : Scheme.{u}) [IsReduced X]
(hfinite : FiniteComponentsOnCompactOpens X) :
Nonempty (meromorphicFunctions X ≅
∏ᶜ fun η : genericPoints X ↦ genericPointStalkModule X η)
AlgebraicGeometry.meromorphicFunctions_iso_coproduct_genericPointStalks_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Coproduct.lean, line 259. The attribute's comment: “generic-point direct sum”.
Stacks 02OW, displayed direct-sum decomposition. On a reduced scheme whose quasi-compact opens have finitely many irreducible components, the
𝒪_X-module of meromorphic functions is the direct sum of the generic-point contributions.
theorem meromorphicFunctions_iso_coproduct_genericPointStalks_of_isReduced (X : Scheme.{u})
[IsReduced X]
(hfinite : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
Nonempty (meromorphicFunctions X ≅
∐ fun η : genericPoints X ↦ genericPointStalkModule X η)
AlgebraicGeometry.nonempty_meromorphicSections_iso_product_genericPointStalks_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Globalization.lean, line 664. The attribute's comment: “part (2), product”.
Stacks 02OW, part (2), product decomposition. On a reduced scheme whose quasi-compact opens have finitely many irreducible components, the sheaf of meromorphic sections of a quasi-coherent module is the product over the generic points of the irreducible components of the generic-point contributions.
theorem nonempty_meromorphicSections_iso_product_genericPointStalks_of_isReduced
(X : Scheme.{u}) [IsReduced X]
(hfinite : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
(F : X.Modules) [F.IsQuasicoherent] :
Nonempty (meromorphicSections X F ≅
∏ᶜ fun η : genericPoints X ↦ genericPointStalkModuleOf X F η)
AlgebraicGeometry.nonempty_meromorphicSections_iso_coproduct_genericPointStalks_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Globalization.lean, line 675. The attribute's comment: “part (2), direct sum”.
Stacks 02OW, part (2), direct-sum decomposition.
theorem nonempty_meromorphicSections_iso_coproduct_genericPointStalks_of_isReduced
(X : Scheme.{u}) [IsReduced X]
(hfinite : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
(F : X.Modules) [F.IsQuasicoherent] :
Nonempty (meromorphicSections X F ≅
∐ fun η : genericPoints X ↦ genericPointStalkModuleOf X F η)
AlgebraicGeometry.meromorphicSections_isQuasicoherent_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Globalization.lean, line 686. The attribute's comment: “part (2), quasi-coherence”.
Stacks 02OW, part (2), quasi-coherence.
theorem meromorphicSections_isQuasicoherent_of_isReduced
(X : Scheme.{u}) [IsReduced X]
(hfinite : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
(F : X.Modules) [F.IsQuasicoherent] :
(meromorphicSections X F).IsQuasicoherent
Stacks.AlgebraicGeometry.MeromorphicQuasicoherent.meromorphicFunctions_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicQuasicoherent/Criteria.lean, line 71. The attribute's comment: “part (1)”.
Stacks Project, Tag 02OW, part (1). On a reduced scheme whose quasi-compact opens have finitely many irreducible components, the sheaf of meromorphic functions is quasi-coherent.
theorem meromorphicFunctions_isQuasicoherent (X : Scheme.{u}) [IsReduced X]
(hfinite : FiniteComponentsOnCompactOpens X) :
(meromorphicFunctions X).IsQuasicoherent
Stacks.AlgebraicGeometry.MeromorphicSectionsTensor.meromorphicSections_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicSectionsTensor/Quasicoherent.lean, line 78. The attribute's comment: “part (2), quasi-coherence”.
Stacks Project, Tag 02OW, part (2), quasi-coherence. On a reduced scheme whose quasi-compact opens have finitely many irreducible components, the sheaf of meromorphic sections of a quasi-coherent
𝒪_X-module is quasi-coherent.
theorem meromorphicSections_isQuasicoherent (X : Scheme.{u}) [IsReduced X]
(hfinite : GenericPointProduct.FiniteComponentsOnCompactOpens X)
(F : X.Modules) [F.IsQuasicoherent] :
(meromorphicSections X F).IsQuasicoherent
AlgebraicGeometry.exists_commRing_rationalFunctions_ringEquiv_totalQuotientSheaf_top_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RationalFunctions/Meromorphic.lean, line 647. The attribute's comment: “part (6)”. References: EGA IV (20.2.13), “(ii) global sections”; EGA I (7.1.3), “special case”.
Part (6) of [Stacks, Tag 02OW]. On a reduced scheme whose quasi-compact opens have finitely many irreducible components, the ring of rational functions is the ring of global meromorphic functions.
theorem exists_commRing_rationalFunctions_ringEquiv_totalQuotientSheaf_top_of_isReduced
(X : Scheme.{u}) [IsReduced X]
(hfinite : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
∃ _ : CommRing X.rationalFunctions,
(∀ (U : X.Opens) (hU : Dense (U : Set X)),
∃ ψ : Γ(X, U) →+* X.rationalFunctions,
∀ s, ψ s = X.rationalFunctionOfSection U hU s) ∧
Nonempty (X.rationalFunctions ≃+* X.totalQuotientSheaf.presheaf.obj (op ⊤))
Stacks.AlgebraicGeometry.ReducedTotalQuotient.regularSectionGerms_eq_nonZeroDivisors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ReducedTotalQuotient/Basic.lean, line 74. The attribute's comment: “part (3)”.
Germs of regular sections are precisely the nonzerodivisors.
theorem regularSectionGerms_eq_nonZeroDivisors
(X : Scheme.{u}) [IsReduced X]
(hfinite : FiniteComponentsOnCompactOpens X) (x : X) :
(⨆ (U : Opens X) (hx : x ∈ U),
((X.presheaf.submonoidPresheafOfStalk
(fun y ↦ nonZeroDivisors (X.presheaf.stalk y))).obj (Opposite.op U)).map
(X.presheaf.germ U x hx).hom) =
nonZeroDivisors (X.presheaf.stalk x)
Stacks.AlgebraicGeometry.ReducedTotalQuotient.stalk_totalQuotientPresheaf_isFractionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ReducedTotalQuotient/Basic.lean, line 87. The attribute's comment: “part (4)”.
A stalk of the meromorphic-function sheaf is the total quotient ring of the local ring.
theorem stalk_totalQuotientPresheaf_isFractionRing
(X : Scheme.{u}) [IsReduced X]
(hfinite : FiniteComponentsOnCompactOpens X) (x : X) :
letI : Algebra (X.presheaf.stalk x) (X.presheaf.totalQuotientPresheaf.stalk x) :=
((TopCat.Presheaf.stalkFunctor CommRingCat x).map
X.presheaf.toTotalQuotientPresheaf).hom.toAlgebra
IsFractionRing (X.presheaf.stalk x)
(X.presheaf.totalQuotientPresheaf.stalk x)
Stacks.AlgebraicGeometry.ReducedTotalQuotient.isLocalization_totalQuotientPresheaf_obj_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ReducedTotalQuotient/Basic.lean, line 100. The attribute's comment: “part (5)”.
Meromorphic functions on an affine open form the total quotient ring of its functions.
theorem isLocalization_totalQuotientPresheaf_obj_of_isAffineOpen
(X : Scheme.{u}) [IsReduced X]
(_hfinite : FiniteComponentsOnCompactOpens X)
(U : X.Opens) (hU : IsAffineOpen U) :
letI : Algebra Γ(X, U)
((X.presheaf.totalQuotientPresheaf).obj (Opposite.op U)) :=
(X.presheaf.toTotalQuotientPresheaf.app (Opposite.op U)).hom.toAlgebra
IsLocalization (nonZeroDivisors Γ(X, U))
((X.presheaf.totalQuotientPresheaf).obj (Opposite.op U))
Tag 035T, a lemma
Tag 035T in the Stacks Project.
AlgebraicGeometry.Scheme.normalizationGluedSpectrum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/MeromorphicRelativeSpec.lean, line 393. The attribute's comment: “the normalization carries the charts of the relative spectrum”. References: EGA II (7.4.6), “special case”.
Stacks Project, Tag 035T. The normalization of a reduced scheme whose quasi-compact opens have finitely many irreducible components, carrying the charts that present it as a relative spectrum of the integral closure of
𝒪_Xin the sheaf of meromorphic functions.
def normalizationGluedSpectrum (X : Scheme.{u}) [IsReduced X]
(hfinite : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
GluedSpectrum (X.meromorphicIntegralClosureSituation hfinite)
AlgebraicGeometry.Scheme.normalizationIsoMeromorphicSpectrum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/MeromorphicRelativeSpec.lean, line 407. The attribute's comment: “the comparison isomorphism”. References: EGA II (7.4.6), “special case”.
Stacks Project, Tag 035T. For a reduced scheme whose quasi-compact opens have finitely many irreducible components, the normalization is the relative spectrum of the integral closure
𝒪'of𝒪_Xin the sheaf of meromorphic functions.
def normalizationIsoMeromorphicSpectrum (X : Scheme.{u}) [IsReduced X]
(hfinite : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
X.normalizationScheme hfinite ≅
(gluedSpectrum (X.meromorphicIntegralClosureSituation hfinite)).scheme
AlgebraicGeometry.Scheme.normalizationIsoMeromorphicSpectrum_hom_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/MeromorphicRelativeSpec.lean, line 417. The attribute's comment: “the normalization is the structure morphism of the relative spectrum”.
Stacks Project, Tag 035T. The comparison isomorphism lies over
X: the normalization morphismν : X^ν ⟶ Xis the structure morphism of the relative spectrum of𝒪'.
theorem normalizationIsoMeromorphicSpectrum_hom_toBase (X : Scheme.{u}) [IsReduced X]
(hfinite : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
(normalizationIsoMeromorphicSpectrum X hfinite).hom ≫
(gluedSpectrum (X.meromorphicIntegralClosureSituation hfinite)).toBase =
X.normalization hfinite
Tag 01X5, a lemma
Tag 01X5 in the Stacks Project.
AlgebraicGeometry.totalQuotientSheafIsoConstant, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/ConstantOnIntegral.lean, line 628. The attribute's comment: “part (1)”. References: EGA I (7.3.6), “F = O_X, integral”.
An isomorphism between the sheaf of meromorphic functions on an integral scheme and the constant sheaf on its function field, carrying a regular section to the constant section determined by its germ at the generic point.
noncomputable def totalQuotientSheafIsoConstant (X : Scheme.{u}) [IsIntegral X] :
{ e : totalQuotientSheaf X.sheaf ≅
constantSheafOnSpace X CommRingCat.{u} X.functionField //
∀ (U : X.Opens) (s : X.presheaf.obj (Opposite.op U))
(h : genericPoint X ∈ U),
(e.hom.hom.app (Opposite.op U)).hom
((toTotalQuotientSheaf X.sheaf).hom.app (Opposite.op U) s) =
(toSheafify (Opens.grothendieckTopology X)
((Functor.const (Opens X)ᵒᵖ).obj X.functionField)).app (Opposite.op U)
(X.presheaf.germ U (genericPoint X) h s) }
AlgebraicGeometry.nonempty_meromorphicSectionSheafIsoConstant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MeromorphicSectionsConstant.lean, line 985. The attribute's comment: “part (2)”. References: EGA I (7.3.6), “integral case”.
On an integral scheme the sheaf of meromorphic sections of a quasi-coherent module
Fis the constant sheaf on the stalk ofFat the generic point, read as a sheaf of modules over the sheaf of meromorphic functions throughAlgebraicGeometry.totalQuotientSheafIsoConstant. For every adjunctionadjbetween extension and restriction of scalars, the isomorphism may be chosen to carry the image of a section under the unit ofadjto the constant section determined by its germ at the generic point.
theorem nonempty_meromorphicSectionSheafIsoConstant [F.IsQuasicoherent] :
Nonempty { e : meromorphicSectionSheaf X.sheaf F ≅
(SheafOfModules.restrictScalars
((sheafCompose (Opens.grothendieckTopology X)
(forget₂ CommRingCat RingCat.{u})).map
(totalQuotientSheafIsoConstant X).val.hom)).obj
(constantGenericStalkModuleSheaf X F) //
∀ (U : X.Opens) (m : F.val.obj (Opposite.op U))
(h : genericPoint X ∈ U),
(e.hom.val.app (Opposite.op U))
((adj.unit.app F).val.app (Opposite.op U) m) =
constantGenericStalkModuleSection X F U
(F.presheaf.germ U (genericPoint X) h m) }
Stacks.AlgebraicGeometry.MeromorphicConstant.totalQuotientSheafIsoConstant, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicConstant/Basic.lean, line 417. The attribute's comment: “part (1)”. References: EGA I (7.3.6), “F = O_X, integral”.
On an integral scheme the sheaf of meromorphic functions is the constant sheaf with value the function field, by an isomorphism carrying the image of a regular function to the constant section given by its germ at the generic point.
noncomputable def totalQuotientSheafIsoConstant :
{ e : totalQuotientSheaf X.sheaf ≅ constantSheafOnSpace X CommRingCat.{u} X.functionField //
∀ (U : X.Opens) (s : X.presheaf.obj (op U)) (h : genericPoint X ∈ U),
(e.hom.hom.app (op U)).hom
((toTotalQuotientSheaf X.sheaf).hom.app (op U) s) =
(toSheafify (Opens.grothendieckTopology X)
((Functor.const (Opens X)ᵒᵖ).obj X.functionField)).app (op U)
(X.presheaf.germ U (genericPoint X) h s) }
Stacks.AlgebraicGeometry.MeromorphicConstantModule.meromorphicSectionSheafIsoConstant, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicConstantModule/Basic.lean, line 572. The attribute's comment: “part (2)”.
Stacks Project, Tag 01X5, part (2). On an integral scheme the sheaf of meromorphic sections of a quasi-coherent module
Fis the constant sheaf of modules with value the stalk ofFat the generic point, over the sheaf of meromorphic functions, compatibly with the germ at the generic point.
noncomputable def meromorphicSectionSheafIsoConstant :
{ e : meromorphicSectionSheaf.{u, u} X.sheaf F ≅ constGenericStalkSheaf F //
∀ (U : X.Opens) (m : (pmod F).obj (op U)) (h : genericPoint X ∈ U),
(e.hom.val.app (op U)).hom (toMeromorphicSection F U m) =
constGenericStalkSection F U (F.presheaf.germ U (genericPoint X) h m) }
Tag 02OZ, a lemma
Tag 02OZ in the Stacks Project.
AlgebraicGeometry.exists_isRegularMeromorphicSection_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/RegularSectionExistence.lean, line 160. The attribute's comment: “part (1)”.
An invertible sheaf of modules on an integral scheme has a regular meromorphic section.
theorem exists_isRegularMeromorphicSection_of_isIntegral
[SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property F] :
∃ s : MeromorphicSection X.sheaf F, IsRegularMeromorphicSection X.sheaf F s
AlgebraicGeometry.exists_isRegularMeromorphicSection_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/RegularSectionExistenceReduced.lean, line 138. The attribute's comment: “part (2)”.
Stacks 02OZ, part (2). An invertible sheaf of modules on a reduced scheme every quasi-compact open of which has finitely many irreducible components has a regular meromorphic section.
theorem exists_isRegularMeromorphicSection_of_isReduced (X : Scheme.{u}) [IsReduced X]
(hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
(L : X.Modules) [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] :
∃ s : MeromorphicSection X.sheaf L, IsRegularMeromorphicSection X.sheaf L s
AlgebraicGeometry.exists_isRegularMeromorphicSection_of_noEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/RegularSectionExistenceReduced.lean, line 148. The attribute's comment: “part (3)”.
Stacks 02OZ, part (3). An invertible sheaf of modules on a locally Noetherian scheme without embedded points has a regular meromorphic section.
theorem exists_isRegularMeromorphicSection_of_noEmbeddedPoints (X : Scheme.{u})
[IsLocallyNoetherian X] (hX : HasNoEmbeddedPoints X) (L : X.Modules)
[SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] :
∃ s : MeromorphicSection X.sheaf L, IsRegularMeromorphicSection X.sheaf L s
AlgebraicGeometry.exists_isRegularMeromorphicSection_of_hasNoEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/RegularSectionExistence.lean, line 450. The attribute's comment: “case (3), X locally Noetherian without embedded points”.
[Stacks, Tag 0EMI], which is case (3) of [Stacks, Tag 02OZ]. An invertible sheaf of modules on a locally Noetherian scheme without embedded points has a regular meromorphic section.
theorem exists_isRegularMeromorphicSection_of_hasNoEmbeddedPoints (X : Scheme.{u})
[IsLocallyNoetherian X] (hX : HasNoEmbeddedPoints X) (L : X.Modules)
[AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L] :
∃ s : MeromorphicSection X.sheaf L, IsRegularMeromorphicSection X.sheaf L s
Sources
Section31.27 Weil divisors#
Section 31.27 of the Stacks Project, Tag 0BE0. 7 tags here are carried by 10 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0BE1, a lemma
Tag 0BE1 in the Stacks Project.
AlgebraicGeometry.locallyFinite_irreducibleComponents_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/WeilDivisors.lean, line 85.
Stacks 0BE1. The images of the irreducible components of a closed subscheme of a locally Noetherian scheme form a locally finite family in the ambient scheme.
theorem locallyFinite_irreducibleComponents_image
{X Z : Scheme} [IsLocallyNoetherian X] (i : Z ⟶ X) [IsClosedImmersion i] :
LocallyFinite (fun C : irreducibleComponents Z ↦ i '' (C : Set Z))
Tag 0BE2, a definition
Tag 0BE2 in the Stacks Project.
Stacks.Divisors.PrimeDivisor, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FirstChernClass/PrimeDivisor.lean, line 87. The attribute's comment: “part (1): prime divisors”.
Stacks 0BE2 (1). A prime divisor of
Xis an integral closed subscheme of codimension one, recorded by its ideal sheaf.
structure PrimeDivisor (X : Scheme.{u})
Stacks.Divisors.WeilDivisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FirstChernClass/PrimeDivisor.lean, line 180. The attribute's comment: “part (2): Weil divisors”.
Stacks 0BE2 (2). The group
Div(X)of Weil divisors: integer-valued coefficient families indexed by the prime divisors ofXwhose nonzero prime divisors form a locally finite collection of closed subsets ofX.
def WeilDivisor (X : Scheme.{u}) : AddSubgroup (PrimeDivisor X → ℤ)
AlgebraicGeometry.PrimeDivisor, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/PrimeDivisor.lean, line 58. The attribute's comment: “part (1): prime divisors”.
A prime divisor of a scheme is an integral closed subscheme of codimension one, presented by its ideal sheaf. The codimension is that of the closure in the ambient scheme of the image of the generic point of the subscheme.
structure PrimeDivisor (X : Scheme.{u})
AlgebraicGeometry.WeilDivisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/PrimeDivisor.lean, line 90. The attribute's comment: “part (2): Weil divisors”.
The Weil divisors of a scheme: the integral coefficient families indexed by prime divisors whose prime divisors with nonzero coefficient have locally finite supports. The additive group structure is the coefficientwise one.
def WeilDivisor (X : Scheme.{u}) : AddSubgroup (PrimeDivisor X → ℤ)
Tag 02RJ, a definition
Tag 02RJ in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.Scheme.ordregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch31.lean, line 30 (StacksFrontier): “the definition, indexed by the generic point ξ of Z (coheight ξ = 1)”.AlgebraicGeometry.Scheme.ord_eq_ordHom_of_coheight_eq_oneregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch31.lean, line 32 (StacksFrontier): “at a codimension-one point the value is ord of the stalk (Tag 02MD)”.irreducibleSetEquivPointsregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch31.lean, line 34 (StacksFrontier): “prime divisors Z correspond to their generic points ξ, codim Z = coheight ξ”.
Tag 02RL, a lemma
Tag 02RL in the Stacks Project.
Stacks.Chow.locallyFinite_closure_notMem_range_algebraMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Vocabulary/PrincipalCycle.lean, line 164. The attribute's comment: “the prime divisors with f ∉ O_{X,ξ}; no hypothesis f ≠ 0 needed”.
Stacks 02RL. On a locally Noetherian integral scheme the prime divisors at whose generic point
ξa rational functionfdoes not lie in the local ringO_{X,ξ}form a locally finite collection of closed subsets ofX. A prime divisor is indexed by its generic point, so the collection is the family of closures of the codimension-one pointszwithf ∉ O_{X,z}.
theorem locallyFinite_closure_notMem_range_algebraMap (X : Scheme.{u}) [IsIntegral X]
[IsLocallyNoetherian X] (f : X.functionField) :
LocallyFinite fun z : {z : X // coheight z = 1 ∧
f ∉ Set.range (algebraMap (X.presheaf.stalk z) X.functionField)} ↦
closure ({(z : X)} : Set X)
Stacks.Chow.locallyFiniteSupport_ord, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Vocabulary/PrincipalCycle.lean, line 185. The attribute's comment: “the prime divisors with ord_Z(f) ≠ 0”.
Stacks 02RL. On a locally Noetherian integral scheme the prime divisors along which a rational function
fhas nonzero order form a locally finite collection: the support ofz ↦ ord_z(f)meets a neighbourhood of every point in a finite set.
theorem locallyFiniteSupport_ord (X : Scheme.{u}) [IsIntegral X] [IsLocallyNoetherian X]
(f : X.functionField) : LocallyFiniteSupport (X.ord f)
Tag 0BE3, a definition
Tag 0BE3 in the Stacks Project.
Stacks.Chow.principalCycle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Vocabulary/PrincipalCycle.lean, line 208. References: EGA IV (21.6.7), “partial”.
Stacks 0BE3. The principal divisor
div(f) = ∑_Z ord_Z(f) [Z]of a rational function on a locally Noetherian integral scheme, as an algebraic cycle: the integral closed subschemeclosure {z}is indexed by its generic pointz, and carries the coefficientord_z(f). Local finiteness of the family of prime divisors involved is Stacks 02RL.
def principalCycle (X : Scheme.{u}) [IsIntegral X] [IsLocallyNoetherian X]
(f : X.functionField) : AlgebraicCycle X ℤ
Tag 02RP, a lemma
Tag 02RP in the Stacks Project.
Stacks.Chow.principalCycle_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Vocabulary/PrincipalCycle.lean, line 232. References: EGA IV (21.1.3), “(21.1.3.1)”.
Stacks 02RP. The principal divisor of a product of nonzero rational functions is the sum of the principal divisors.
theorem principalCycle_mul (X : Scheme.{u}) [IsIntegral X] [IsLocallyNoetherian X]
{f g : X.functionField} (hf : f ≠ 0) (hg : g ≠ 0) :
principalCycle X (f * g) = principalCycle X f + principalCycle X g
Tag 0BE4, a definition
Tag 0BE4 in the Stacks Project.
AlgebraicGeometry.weilDivisorClassGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/WeilDivisorClass/ClassGroup.lean, line 61.
The Weil divisor class group
Cl(X)of a locally Noetherian integral scheme: the group of Weil divisors modulo the subgroup of principal Weil divisors.
abbrev weilDivisorClassGroup : Type u
Sources
Section31.28 The Weil divisor class associated to an invertible module#
Section 31.28 of the Stacks Project, Tag 02SE. 8 tags here are carried by 22 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02SF, a definition
Tag 02SF in the Stacks Project.
Stacks.Divisors.orderOfVanishingMeromorphic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/MeromorphicCascade/OrderOfVanishing.lean, line 75. References: EGA IV (21.6.7), “o_x(f) = mult_x(div f)”.
The order of vanishing of a regular meromorphic section along a prime divisor, Stacks 02SF. The meromorphic section is a global section
sof the sheaf𝒦_X(L)of meromorphic sections ofL; its order alongZis the order of vanishing, in the local ring at the generic point ofZ, of the rational function expressing the generic value ofsin terms of a generator of the stalk ofLthere.
Stacks.Divisors.orderOfVanishingMeromorphic_eqis the characterization, and it is what should be used rather than this definition.
def orderOfVanishingMeromorphic (X : Scheme.{u}) [IsLocallyNoetherian X] [IsIntegral X]
(L : X.Modules)
[AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
(s : AlgebraicGeometry.MeromorphicSection X.sheaf L)
(_hs : AlgebraicGeometry.IsRegularMeromorphicSection X.sheaf L s)
(Z : PrimeDivisor X) : ℤ
AlgebraicGeometry.orderOfVanishingMeromorphicData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/OrderOfVanishingMeromorphic.lean, line 95.
A choice of the data provided by
AlgebraicGeometry.nonempty_orderOfVanishingMeromorphicData: the quasi-coherence ofL, the order of vanishing of the regular meromorphic sectionsalong the prime divisorZ, and its characterization as the order of the coordinate ofswith respect to any generator ofLat the generic point ofZ.
def orderOfVanishingMeromorphicData
(X : Scheme.{u}) [IsLocallyNoetherian X] [IsIntegral X]
(L : X.Modules)
[AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
(s : MeromorphicSection X.sheaf L)
(_hs : IsRegularMeromorphicSection X.sheaf L s)
(Z : PrimeDivisor X) :
{ q : PSigma (fun _ : L.IsQuasicoherent => ℤ) //
letI : L.IsQuasicoherent := q.1
let ξ := Z.genericPoint
let R := X.presheaf.stalk ξ
let K := X.functionField
letI : Module R (L.presheaf.stalk ξ) :=
PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
(R := X.presheaf) L.val ξ
letI : Module K (L.presheaf.stalk (genericPoint X)) :=
PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
(R := X.presheaf) L.val (genericPoint X)
let isCoordinate := fun (m : L.presheaf.stalk ξ) (a : K) =>
((meromorphicSectionSheafIsoConstant X L).val.hom.val.app
(op (⊤ : X.Opens))) (s.val (op ⊤)) =
constantGenericStalkModuleSection X L ⊤
(a • (L.presheaf.stalkSpecializes
((genericPoint_spec X).specializes trivial)) m)
(∃ m : L.presheaf.stalk ξ,
(Submodule.span R {m} = ⊤) ∧ (∃ a : K, isCoordinate m a)) ∧
(∀ (m : L.presheaf.stalk ξ)
(_ : Submodule.span R {m} = ⊤) (a : K),
isCoordinate m a → q.2 = X.ord a ξ) }
AlgebraicGeometry.orderOfVanishingMeromorphic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/OrderOfVanishingMeromorphic.lean, line 130.
The order of vanishing along a prime divisor
Zof a regular meromorphic sectionsof an invertible moduleLon a locally Noetherian integral scheme: the order in𝒪_{X, ξ}of the coordinate ofswith respect to a generator ofL_ξ, whereξis the generic point ofZ.
def orderOfVanishingMeromorphic
(X : Scheme.{u}) [IsLocallyNoetherian X] [IsIntegral X]
(L : X.Modules)
[AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
(s : MeromorphicSection X.sheaf L)
(hs : IsRegularMeromorphicSection X.sheaf L s)
(Z : PrimeDivisor X) : ℤ
Tag 02SG, a lemma
Tag 02SG in the Stacks Project.
AlgebraicGeometry.locallyFinite_primeDivisors_not_representedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/PoleLocus.lean, line 164. The attribute's comment: “nonintegral_stalk_locus”.
The prime divisors at whose generic point a meromorphic section of a quasi-coherent module on a locally Noetherian integral scheme is not an ordinary section form a locally finite collection of closed subsets.
theorem locallyFinite_primeDivisors_not_representedAt [IsLocallyNoetherian X] [IsIntegral X]
(L : X.Modules)
[L.IsQuasicoherent] (s : MeromorphicSection X.sheaf L) :
LocallyFinite
(fun Z : { Z : PrimeDivisor X // ¬ IsRepresentedAt L s Z.genericPoint } => Z.1.support)
AlgebraicGeometry.locallyFinite_primeDivisors_orderOfVanishingMeromorphic_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/PoleLocus.lean, line 198. The attribute's comment: “nonzero_order_locus”.
The prime divisors along which a regular meromorphic section of an invertible module on a locally Noetherian integral scheme has nonzero order of vanishing form a locally finite collection of closed subsets; equivalently, the orders are the coefficients of a Weil divisor.
theorem locallyFinite_primeDivisors_orderOfVanishingMeromorphic_ne_zero :
LocallyFinite (fun Z : PrimeDivisor X =>
if orderOfVanishingMeromorphic X L s hs Z = 0 then ∅ else Z.support)
Tag 02SH, a lemma
Tag 02SH in the Stacks Project.
AlgebraicGeometry.existsUnique_meromorphicSectionRatio, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/SectionRatio.lean, line 154. The attribute's comment: “ratio”. References: EGA IV (20.1.8), “partial”.
Two regular meromorphic sections of an invertible module on an integral scheme have a unique ratio in the units of the ring of rational functions.
theorem existsUnique_meromorphicSectionRatio
(hs : IsRegularMeromorphicSection X.sheaf L s)
(hs' : IsRegularMeromorphicSection X.sheaf L s') :
∃! f : (Stacks.Chow.rationalFunctions X)ˣ, IsMeromorphicSectionRatio X L s s' f
AlgebraicGeometry.meromorphicWeilDivisor_eq_add_principalDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/SectionRatio.lean, line 242. The attribute's comment: “divisor identity”.
The Weil divisors of two regular meromorphic sections of an invertible module on a locally Noetherian integral scheme differ by the principal divisor of their ratio.
theorem meromorphicWeilDivisor_eq_add_principalDivisor [IsLocallyNoetherian X]
(hs : IsRegularMeromorphicSection X.sheaf L s)
(hs' : IsRegularMeromorphicSection X.sheaf L s') :
weilDivisorOfMeromorphicSection X L s hs =
weilDivisorOfMeromorphicSection X L s' hs' +
principalDivisor X (meromorphicSectionRatio X L s s' hs hs')
Tag 0BE6, a definition
Tag 0BE6 in the Stacks Project.
AlgebraicGeometry.weilDivisorClassOfInvertibleSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DivisorClass.lean, line 47. The attribute's comment: “part (2): divisor class of an invertible sheaf”.
The Weil divisor class of an invertible sheaf on a locally Noetherian integral scheme: the class in
Cl(X)of the Weil divisor of a chosen regular meromorphic section ofL.
def weilDivisorClassOfInvertibleSheaf : weilDivisorClassGroup X
AlgebraicGeometry.weilDivisorClassOfInvertibleSheaf_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DivisorClass.lean, line 56. The attribute's comment: “part (2): independence of the meromorphic section”.
The Weil divisor of any regular meromorphic section of an invertible sheaf
Lhas classAlgebraicGeometry.weilDivisorClassOfInvertibleSheaf X LinCl(X).
theorem weilDivisorClassOfInvertibleSheaf_eq (s : MeromorphicSection X.sheaf L)
(hs : IsRegularMeromorphicSection X.sheaf L s) :
weilDivisorClassOfInvertibleSheaf X L =
((weilDivisorOfMeromorphicSection X L s hs : WeilDivisor X) :
weilDivisorClassGroup X)
AlgebraicGeometry.weilDivisorOfMeromorphicSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/PoleLocus.lean, line 241. The attribute's comment: “part (1): divisor of a meromorphic section”.
The Weil divisor
div_L(s) = ∑_Z ord_{Z, L}(s) [Z]of a regular meromorphic section of an invertible module on a locally Noetherian integral scheme.
def weilDivisorOfMeromorphicSection : WeilDivisor X
Tag 02SL, a lemma
Tag 02SL in the Stacks Project.
AlgebraicGeometry.tensorMeromorphicSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TensorSection.lean, line 179. The attribute's comment: “tensor product of meromorphic sections”.
Stacks 02SL: the tensor product of two meromorphic sections. The meromorphic section of
L ⊗_{𝒪_X} Nwhose generic value is the pure tensor of the generic values ofsandt. On an integral scheme this determines it, by Tag 01X5 part (2);AlgebraicGeometry.meromorphicSectionSheafIsoConstant_tensorMeromorphicSectionis the resulting description on pure tensors of honest sections.
def tensorMeromorphicSection [L.IsQuasicoherent] [N.IsQuasicoherent]
[(Scheme.Modules.tensorObj L N).IsQuasicoherent]
(s : MeromorphicSection X.sheaf L) (t : MeromorphicSection X.sheaf N) :
MeromorphicSection X.sheaf (Scheme.Modules.tensorObj L N)
AlgebraicGeometry.meromorphicSectionSheafIsoConstant_tensorMeromorphicSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TensorSection.lean, line 220. The attribute's comment: “pure-tensor characterization”.
Stacks 02SL: at the generic point the product is the pure tensor. If the meromorphic sections
sandtare, at the generic point, the germs of honest sectionsmofLandnofNover a neighbourhoodUof it, then their product is the germ of the pure tensorm ⊗ n. This fixes the product and not merely its divisor: a meromorphic section on an integral scheme is determined by its generic germ.
theorem meromorphicSectionSheafIsoConstant_tensorMeromorphicSection
[L.IsQuasicoherent] [N.IsQuasicoherent] [(Scheme.Modules.tensorObj L N).IsQuasicoherent]
(s : MeromorphicSection X.sheaf L) (t : MeromorphicSection X.sheaf N)
(U : X.Opens) (hU : genericPoint X ∈ U)
(m : L.val.obj (op U)) (n : N.val.obj (op U))
(hs : (meromorphicSectionSheafIsoConstant X L).val.hom.val.app (op (⊤ : X.Opens))
(s.val (op ⊤)) =
constantGenericStalkModuleSection X L ⊤ (L.presheaf.germ U (genericPoint X) hU m))
(ht : (meromorphicSectionSheafIsoConstant X N).val.hom.val.app (op (⊤ : X.Opens))
(t.val (op ⊤)) =
constantGenericStalkModuleSection X N ⊤ (N.presheaf.germ U (genericPoint X) hU n)) :
(meromorphicSectionSheafIsoConstant X (Scheme.Modules.tensorObj L N)).val.hom.val.app
(op (⊤ : X.Opens)) ((tensorMeromorphicSection X L N s t).val (op ⊤)) =
constantGenericStalkModuleSection X (Scheme.Modules.tensorObj L N) ⊤
(PresheafOfModules.tensorSheafGerm X.sheaf L N (genericPoint X) U hU m n)
AlgebraicGeometry.isRegularMeromorphicSection_tensorMeromorphicSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TensorSection.lean, line 269. The attribute's comment: “nonzero product”. References: EGA IV (20.1.10), “integral; tensor clause”.
Stacks 02SL: a product of nonzero meromorphic sections is nonzero. Regularity in the sense of Tag 02OX is injectivity of multiplication by the generic value. Writing the generic values of
sandtasaandbtimes stalk bases ofL_ηandN_η, the generic value of the product isa * btimes the product of those bases, which is a stalk basis of(L ⊗_{𝒪_X} N)_η; anda * bis nonzero in the function field.
theorem isRegularMeromorphicSection_tensorMeromorphicSection
[SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
[SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property N]
(s : MeromorphicSection X.sheaf L) (t : MeromorphicSection X.sheaf N)
(hs : IsRegularMeromorphicSection X.sheaf L s)
(ht : IsRegularMeromorphicSection X.sheaf N t) :
IsRegularMeromorphicSection X.sheaf (Scheme.Modules.tensorObj L N)
(tensorMeromorphicSection X L N s t)
AlgebraicGeometry.weilDivisorOfMeromorphicSection_tensorMeromorphicSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TensorSection.lean, line 357. The attribute's comment: “divisor additivity”.
Stacks 02SL: the divisor of a product is the sum of the divisors. The Weil divisor of Tag 0BE6 part (1) is additive in the product of regular meromorphic sections of invertible modules, coefficient by coefficient.
theorem weilDivisorOfMeromorphicSection_tensorMeromorphicSection
[SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
[SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property N]
(s : MeromorphicSection X.sheaf L) (t : MeromorphicSection X.sheaf N)
(hs : IsRegularMeromorphicSection X.sheaf L s)
(ht : IsRegularMeromorphicSection X.sheaf N t) :
weilDivisorOfMeromorphicSection X (Scheme.Modules.tensorObj L N)
(tensorMeromorphicSection X L N s t)
(isRegularMeromorphicSection_tensorMeromorphicSection X L N s t hs ht) =
weilDivisorOfMeromorphicSection X L s hs + weilDivisorOfMeromorphicSection X N t ht
AlgebraicGeometry.weilDivisorClassOfInvertibleSheaf_tensorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TensorSection.lean, line 378. The attribute's comment: “divisor-class additivity”.
Stacks 02SL: the divisor class of a tensor product is the sum of the divisor classes. The Weil divisor class of Tag 0BE6 part (2) is additive in the tensor product of invertible modules: a regular meromorphic section of each factor exists by Tag 02OZ part (1), their product is a regular meromorphic section of the tensor product, and its divisor is the sum of their divisors. This is the input Tag 0BE7 needs, and it is supplied to it in
AlgebraicGeometry.picardToWeilDivisorClassGroup.
theorem weilDivisorClassOfInvertibleSheaf_tensorObj
[SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
[SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property N] :
weilDivisorClassOfInvertibleSheaf X (Scheme.Modules.tensorObj L N) =
weilDivisorClassOfInvertibleSheaf X L + weilDivisorClassOfInvertibleSheaf X N
Tag 0BE7, an equation
Tag 0BE7 in the Stacks Project.
AlgebraicGeometry.picardToWeilDivisorClassGroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/WeilDivisorClass/FirstChernClass.lean, line 129.
Stacks 0BE7: the first Chern class. On a locally Noetherian integral scheme the Weil divisor class of an invertible module defines a homomorphism from the Picard group to the Weil divisor class group. Additivity is the divisor-class additivity of Tag 02SL,
AlgebraicGeometry.weilDivisorClassOfInvertibleSheaf_tensorObj, and well-definedness on isomorphism classes isAlgebraicGeometry.weilDivisorClassOfInvertibleSheaf_congr;AlgebraicGeometry.weilDivisorClassOfPicardClass_picardClassis the characterization of this homomorphism on the class of an invertible module.
def picardToWeilDivisorClassGroup :
Stacks.SheafOfModules.PicardGroup X.sheaf.obj X.ringCatSheaf.property →+
weilDivisorClassGroup X
Tag 0BE8, a lemma
Tag 0BE8 in the Stacks Project.
AlgebraicGeometry.picardToWeilDivisorClassGroup_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/WeilDivisorClass/FirstChernClassInjective.lean, line 466. References: EGA IV (21.6.10), “(i), integral case”; SGA 2 XI (3.8), “partial”.
Stacks 0BE8. On a normal locally Noetherian integral scheme the first Chern class
Pic(X) → Cl(X)of Tag 0BE7 is injective.The map is a group homomorphism, so it is enough that a Picard class in its kernel vanishes. Such a class is the Picard class of an invertible module
L, whose image is the Weil divisor class ofL, andAlgebraicGeometry.nonempty_iso_unit_of_weilDivisorClassOfInvertibleSheaf_eq_zerothen makesLisomorphic to𝒪_X, which is triviality of the Picard class.
theorem picardToWeilDivisorClassGroup_injective [IsNormal X] :
Function.Injective (picardToWeilDivisorClassGroup X)
Tag 0BE9, a lemma
Tag 0BE9 in the Stacks Project.
AlgebraicGeometry.isNormal_of_forall_uniqueFactorizationMonoid_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/WeilDivisorClass/FirstChernClassBijective.lean, line 63. The attribute's comment: “(1) → (2): factorial local rings give a normal scheme”.
A scheme whose local rings are unique factorization domains is normal: a unique factorization domain is integrally closed, which is Tag 0AFV.
Stacks 0BE9, the normality half of the implication from condition (1) to condition (2).
theorem isNormal_of_forall_uniqueFactorizationMonoid_stalk
(h : ∀ x : X, UniqueFactorizationMonoid (X.presheaf.stalk x)) : IsNormal X
AlgebraicGeometry.picardToWeilDivisorClassGroup_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/WeilDivisorClass/FirstChernClassBijective.lean, line 75. The attribute's comment: “final clause under (2): on a normal scheme a surjective c_1 is bijective”.
On a normal locally Noetherian integral scheme a surjective first Chern class
Pic(X) → Cl(X)is bijective, since it is injective by Tag 0BE8.Stacks 0BE9, the final clause under condition (2).
theorem picardToWeilDivisorClassGroup_bijective [IsNormal X]
(hsurj : Function.Surjective (picardToWeilDivisorClassGroup X)) :
Function.Bijective (picardToWeilDivisorClassGroup X)
AlgebraicGeometry.forall_uniqueFactorizationMonoid_stalk_iff_isNormal_and_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/WeilDivisorClass/FirstChernClassBijective.lean, line 105. The attribute's comment: “the equivalence of conditions (1) and (2)”. References: SGA 2 XI (3.8), “partial”.
Stacks 0BE9. For a locally Noetherian integral scheme the local rings are unique factorization domains exactly when the scheme is normal and the first Chern class
Pic(X) → Cl(X)of Tag 0BE7 is surjective.Forwards, normality is
AlgebraicGeometry.isNormal_of_forall_uniqueFactorizationMonoid_stalkand surjectivity isAlgebraicGeometry.picardToWeilDivisorClassGroup_surjective; backwards this isAlgebraicGeometry.uniqueFactorizationMonoid_stalk_of_surjective_picardToWeilDivisorClassGroup.
theorem forall_uniqueFactorizationMonoid_stalk_iff_isNormal_and_surjective :
(∀ x : X, UniqueFactorizationMonoid (X.presheaf.stalk x)) ↔
(IsNormal X ∧ Function.Surjective (picardToWeilDivisorClassGroup X))
AlgebraicGeometry.picardToWeilDivisorClassGroup_bijective_of_forall_uniqueFactorizationMonoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/WeilDivisorClass/FirstChernClassBijective.lean, line 123. The attribute's comment: “the isomorphism Pic(X) = Cl(X)”. References: EGA IV (21.6.10), “(i), injectivity, (ii)”; SGA 2 XI (3.7.1), “special case”; SGA 2 XI (3.8), “special case”.
Stacks 0BE9, the final clause. On a locally Noetherian integral scheme whose local rings are unique factorization domains the first Chern class
Pic(X) → Cl(X)is an isomorphism: factoriality makesXnormal, so Tag 0BE8 gives injectivity, andAlgebraicGeometry.picardToWeilDivisorClassGroup_surjectivegives surjectivity.
theorem picardToWeilDivisorClassGroup_bijective_of_forall_uniqueFactorizationMonoid
(h : ∀ x : X, UniqueFactorizationMonoid (X.presheaf.stalk x)) :
Function.Bijective (picardToWeilDivisorClassGroup X)
AlgebraicGeometry.forall_uniqueFactorizationMonoid_stalk_iff_isNormal_and_surjective_and_picardEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/WeilDivisorClass/FirstChernClassBijective.lean, line 155. The attribute's comment: “the full statement: (1) ⟺ (2), and in that case Pic(X) ≅ Cl(X)”. References: SGA 2 XI (3.7.1), “special case”; SGA 2 XI (3.8), “partial”.
Stacks 0BE9. Let
Xbe a locally Noetherian integral scheme and consider the first Chern classPic(X) → Cl(X)of Tag 0BE7. The following are equivalent:
- the local rings of
Xare unique factorization domains, andXis normal andPic(X) → Cl(X)is surjective.In this case
Pic(X) → Cl(X)is an isomorphism.The equivalence is
AlgebraicGeometry.forall_uniqueFactorizationMonoid_stalk_iff_isNormal_and_surjective, and the isomorphism isAlgebraicGeometry.picardEquivWeilDivisorClassGroupOfForallUniqueFactorizationMonoid, whose underlying map is the first Chern class.
theorem forall_uniqueFactorizationMonoid_stalk_iff_isNormal_and_surjective_and_picardEquiv :
((∀ x : X, UniqueFactorizationMonoid (X.presheaf.stalk x)) ↔
IsNormal X ∧ Function.Surjective (picardToWeilDivisorClassGroup X)) ∧
((∀ x : X, UniqueFactorizationMonoid (X.presheaf.stalk x)) →
∃ e : Stacks.SheafOfModules.PicardGroup X.sheaf.obj X.ringCatSheaf.property ≃+
weilDivisorClassGroup X, ∀ c, e c = picardToWeilDivisorClassGroup X c)
Sources
Section31.29 More on invertible modules#
Section 31.29 of the Stacks Project, Tag 0BD6. 5 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0BD7, a lemma
Tag 0BD7 in the Stacks Project.
Stacks.InvertiblePullback.exists_isInvertible_pullback_iso_of_isTrivial_genericFiber_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertiblePullbackFlat/LocalFamilyAgreement.lean, line 330.
Stacks Project, Tag 0BD7. Let
φ : X ⟶ Ybe a morphism of schemes andℒan invertible𝒪_X-module. AssumeXis locally Noetherian,Yis locally Noetherian, integral and normal,φis flat with integral fibres,φis quasi-compact or locally of finite type, andℒis trivial on the generic fibre ofφ. Thenℒ ≅ φ^*𝒩for an invertible𝒪_Y-module𝒩.The family of meromorphic multipliers of the penultimate paragraph of the source's proof is no longer a hypothesis: it is
Stacks.InvertiblePullback.exists_span_eq_top_isPullMeromorphicFamily.Invertibility of
ℒis the hypothesishLalone: the class instance thatFamilyDescent.leancarries beside it is the same statement in another spelling and is obtained fromhLinside the proof, so no hypothesis here is absent from [Stacks, Tag 0BD7].
theorem exists_isInvertible_pullback_iso_of_isTrivial_genericFiber_of_flat
[IsLocallyNoetherian X] [IsLocallyNoetherian Y]
[AlgebraicGeometry.IsIntegral Y] [IsNormal Y]
(hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
(Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf).property
L)
(hfibre : ∀ y : Y, AlgebraicGeometry.IsIntegral (f.fiber y))
(hfinite : QuasiCompact f ∨ LocallyOfFiniteType f)
(hgeneric : AlgebraicGeometry.SheafOfModules.IsTrivial
(f.fiber (genericPoint Y)).presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat)
(f.fiber (genericPoint Y)).IsSheaf)
((Scheme.Modules.pullback (f.fiberι (genericPoint Y))).obj L)) :
∃ N : Y.Modules,
AlgebraicGeometry.SheafOfModules.IsInvertible Y.presheaf
((Presheaf.isSheaf_iff_isSheaf_comp _ Y.presheaf
(forget₂ CommRingCat RingCat)).mp Y.IsSheaf) N ∧
Nonempty ((Scheme.Modules.pullback f).obj N ≅ L)
Tag 0BD8, a lemma
Tag 0BD8 in the Stacks Project.
AlgebraicGeometry.exists_isEffectiveCartierDivisor_comap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/UFDExtension.lean, line 377.
Stacks Project, Tag 0BD8. An effective Cartier divisor on an open subscheme of a locally Noetherian scheme extends to an effective Cartier divisor on the whole scheme, provided the local rings at the points outside the open are unique factorization domains. The extension is the scheme-theoretic image.
theorem exists_isEffectiveCartierDivisor_comap_eq {X : Scheme.{u}} [IsLocallyNoetherian X]
(U : X.Opens) (D : U.toScheme.IdealSheafData) (hD : IsEffectiveCartierDivisor D)
(hUFD : ∀ x : X, x ∉ U → UniqueFactorizationMonoid (X.presheaf.stalk x)) :
∃ D' : X.IdealSheafData, IsEffectiveCartierDivisor D' ∧ D'.comap U.ι = D
Tag 0BD9, a lemma
Tag 0BD9 in the Stacks Project.
AlgebraicGeometry.exists_isInvertible_pullback_iso_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/UFDExtensionInvertibleLocallyNoetherian.lean, line 676. The attribute's comment: “the locally Noetherian case, i.e. the tag itself”.
[Stacks, Tag 0BD9]. Let
Xbe a locally Noetherian scheme, letU ⊆ Xbe an open subscheme, and letLbe an invertible𝒪_U-module. If the local ring𝒪_{X, x}is a unique factorization domain at every pointxoutsideU, thenLis the restriction of an invertible𝒪_X-module.
theorem exists_isInvertible_pullback_iso_of_isLocallyNoetherian {X : Scheme.{u}}
[IsLocallyNoetherian X] (U : X.Opens) (L : U.toScheme.Modules)
[AlgebraicGeometry.SheafOfModules.IsInvertible U.toScheme.sheaf.obj
U.toScheme.ringCatSheaf.property L]
(hUFD : ∀ x : X, x ∉ U → UniqueFactorizationMonoid (X.presheaf.stalk x)) :
∃ L' : X.Modules,
AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L' ∧
Nonempty (L ≅ (Scheme.Modules.pullback U.ι).obj L')
Tag 0BDA, a lemma
Tag 0BDA in the Stacks Project.
Stacks.PicardUFD.subsingleton_picardGroup_open_spectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardGroup/OpenUFD.lean, line 205. The attribute's comment: “part (1)”. References: SGA 1 XI (6.5), “factorial-ring example”.
Stacks Project, Tag 0BDA, part (1). The Picard group of any open subscheme of the spectrum of a unique factorization domain is trivial.
The empty open is handled separately; for a nonempty one, prime avoidance gives two principal opens
D(f), D(g) ⊆ Uwhose union has trivial Picard group and across whose complement inUregular functions extend, so triviality descends toU.
theorem subsingleton_picardGroup_open_spectrum (R : Type u) [CommRing R] [IsDomain R]
[UniqueFactorizationMonoid R] (U : (Spec (.of R)).Opens) :
Subsingleton (PicardGroup U.toScheme.presheaf U.toScheme.ringCatSheaf.2)
Stacks.PicardUFD.subsingleton_picardGroup_open_affineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardGroup/OpenUFD.lean, line 229. The attribute's comment: “part (2)”. References: EGA I (2.4.8), “more general”.
Stacks Project, Tag 0BDA, part (2). The Picard group of any open subscheme of affine space over a unique factorization domain is trivial. In particular this holds over a field.
Affine space over
Ris the spectrum ofR[ι], which is again a unique factorization domain (Tag 0BC1, Mathlib's instance forMvPolynomial), so this is part (1) transported alongAlgebraicGeometry.AffineSpace.SpecIso.
theorem subsingleton_picardGroup_open_affineSpace (R : Type u) [CommRing R] [IsDomain R]
[UniqueFactorizationMonoid R] (ι : Type u) (U : (AffineSpace ι (Spec (.of R))).Opens) :
Subsingleton (PicardGroup U.toScheme.presheaf U.toScheme.ringCatSheaf.2)
Tag 0BXJ, a lemma
Tag 0BXJ in the Stacks Project.
Stacks.PicardUFD.twistPicardHom_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardUFD/ProjectiveSpace.lean, line 1037. The attribute's comment: “injectivity of m ↦ 𝒪(m), for 0 < n; the source states no restriction, but at n = 0 the map is the zero map into the trivial Picard group of ℙ⁰_R ≅ Spec R and is not injective”.
The homomorphism
ℤ ⟶ Pic(ℙⁿ_R),m ↦ 𝒪(m), is injective forRa domain and0 < n. A trivialization of𝒪(m)makes the transition unit(T₀ / T₁) ^ ma ratio of constants, which at the generic point readsT₀^{m⁺} T₁^{m⁻} · s = r · T₀^{m⁻} T₁^{m⁺}and forcesm⁺ = m⁻, hencem = 0.
theorem twistPicardHom_injective [IsDomain R] (hn : 0 < n) :
Function.Injective (twistPicardHom R n)
Stacks.PicardUFD.twistPicardHom_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardUFD/ProjectiveSpace.lean, line 1470. The attribute's comment: “surjectivity of m ↦ 𝒪(m) for the projective line, i.e. for n = 1”.
Stacks Project, Tag 0BXJ. The homomorphism
ℤ ⟶ Pic(ℙ¹_R),m ↦ 𝒪(m), is surjective forRa unique factorization domain: every invertible module on the projective line is a twist.
theorem twistPicardHom_surjective [IsDomain R] [UniqueFactorizationMonoid R] :
Function.Surjective (twistPicardHom R 1)
Stacks.PicardUFD.twistPicardHom_surjective_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardUFD/ProjectiveSpaceCocycle.lean, line 671. The attribute's comment: “surjectivity of m ↦ 𝒪(m), for every n”.
Stacks Project, Tag 0BXJ. The homomorphism
ℤ ⟶ Pic(ℙⁿ_R),m ↦ 𝒪(m), is surjective forRa unique factorization domain and everyn.
theorem twistPicardHom_surjective_general :
Function.Surjective (twistPicardHom R n)
Stacks.PicardUFD.twistPicardAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardUFD/ProjectiveSpaceCocycle.lean, line 693. The attribute's comment: “the isomorphism ℤ ≃+ Pic(ℙⁿ_R) carrying m to the class of 𝒪(m), for 0 < n”.
Stacks Project, Tag 0BXJ. The Picard group of
ℙⁿ_RisℤforRa unique factorization domain and0 < n, the isomorphism sendingmto the class of𝒪(m).
def twistPicardAddEquiv (hn : 0 < n) :
ℤ ≃+ (AlgebraicGeometry.Proj
(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)).picardGroup
Stacks.PicardUFD.not_injective_twistPicardHom_dim_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardUFD/ProjectiveSpaceCocycle.lean, line 726. The attribute's comment: “the n = 0 boundary case: m ↦ 𝒪(m) is the zero map into the trivial group Pic(ℙ⁰_R) and is not injective, so the unrestricted source statement fails there”.
The boundary case of Tag 0BXJ. The source states no restriction on
n, but atn = 0the Picard group ofℙ⁰_Ris trivial, som ↦ 𝒪(m)is the zero map and is not injective.
theorem not_injective_twistPicardHom_dim_zero :
¬ Function.Injective (twistPicardHom R 0)
Sources
Section31.30 Weil divisors on normal schemes#
Section 31.30 of the Stacks Project, Tag 0EBK. 6 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0EBL, a lemma
Tag 0EBL in the Stacks Project.
AlgebraicGeometry.CoherentReflexive.isIso_dualTensorHullToSheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/DualTensorInternalHom.lean, line 438. The attribute's comment: “the comparison (ℋom(ℱ, 𝒪_X) ⊗ 𝒢)^∨∨ → ℋom(ℱ, 𝒢) is an isomorphism”.
Let
Xbe an integral locally Noetherian normal scheme and letℱand𝒢be coherent reflexive𝒪_X-modules. Then the canonical map
(ℋom_{𝒪_X}(ℱ, 𝒪_X) ⊗_{𝒪_X} 𝒢)^∨∨ ⟶ ℋom_{𝒪_X}(ℱ, 𝒢)is an isomorphism.
theorem isIso_dualTensorHullToSheafHom (E F : X.Modules) [E.IsCoherent] [F.IsCoherent]
(hE : IsReflexive E) (hF : IsReflexive F) :
IsIso (dualTensorHullToSheafHom E F hF)
AlgebraicGeometry.CoherentReflexive.rankOneSkeletonMul_toSkeleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/RankOneTensorMonoid.lean, line 307. The attribute's comment: “the monoid law is the double dual of the tensor product”.
Stacks Project, Tag 0EBL. The product of two isomorphism classes of rank one coherent reflexive modules is the class of
(ℱ ⊗_{𝒪_X} 𝒢)^∨∨. This identifies the monoid law ofrankOneSkeletonCommMonoidwith the rule the tag states, so the two together assert that that rule is a commutative monoid law.
theorem rankOneSkeletonMul_toSkeleton (F G : RankOneReflexiveModules X) :
rankOneSkeletonMul (toSkeleton F) (toSkeleton G) = toSkeleton (rankOneTensorObj F G)
AlgebraicGeometry.CoherentReflexive.rankOneSkeletonCommMonoid, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/RankOneTensorMonoid.lean, line 357. The attribute's comment: “commutative monoid law on rank 1 coherent reflexive classes”.
Stacks Project, Tag 0EBL, the monoid part of the group law. On an integral locally Noetherian scheme the rule
ℱ, 𝒢 ↦ (ℱ ⊗_{𝒪_X} 𝒢)^∨∨is a commutative monoid law on the set of isomorphism classes of rank one coherent reflexive𝒪_X-modules, with the class of the structure sheaf as its unit. Inverses are not provided; see the implementation notes.
noncomputable def rankOneSkeletonCommMonoid (X : Scheme.{u}) [IsIntegral X]
[IsLocallyNoetherian X] : CommMonoid (Skeleton (RankOneReflexiveModules X))
AlgebraicGeometry.CoherentReflexive.rankOneSkeletonCommGroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/RankOneWeilClassSurjective.lean, line 104. The attribute's comment: “the abelian group law on isomorphism classes of rank 1 coherent reflexive modules”.
On an integral locally Noetherian normal scheme the rule
ℱ, 𝒢 ↦ (ℱ ⊗_{𝒪_X} 𝒢)^∨∨is an abelian group law on the set of isomorphism classes of rank one coherent reflexive𝒪_X-modules.Multiplication and unit are those of
AlgebraicGeometry.CoherentReflexive.rankOneSkeletonCommMonoid, and the inverse of[ℱ]is the class whose Weil divisor class is-[ℱ].
noncomputable def rankOneSkeletonCommGroup (X : Scheme.{u}) [IsIntegral X]
[IsLocallyNoetherian X] [IsNormal X] :
CommGroup (Skeleton (RankOneReflexiveModules X))
Tag 0EBM, a lemma
Tag 0EBM in the Stacks Project.
AlgebraicGeometry.nonempty_iso_of_weilDivisorClassOfInvertibleSheaf_restrict_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/DivisorClassFaithful.lean, line 166. The attribute's comment: “the injectivity clause, with the two modules compared directly”.
Stacks Project, Tag 0EBM, the injectivity clause. Let
Xbe an integral locally Noetherian normal scheme andU ⊆ Xan open subscheme whose complement has codimension at least two at every point. Two coherent reflexive𝒪_X-modules whose restrictions toUare invertible with the same Weil divisor class inCl(U)are isomorphic.This is the injectivity clause of the source's proof of Tag 0EBM, stated without the map that clause is about: the first Chern class of
Uis injective by [Stacks, Tag 0BE8], so the two restrictions are isomorphic, and restriction toUis an equivalence on coherent reflexive modules by [Stacks, Tag 0EBJ], so the two modules are isomorphic onX. The isomorphism that Tag 0EBM itself asserts — betweenCl(X)and the group of isomorphism classes of rank one coherent reflexive𝒪_X-modules — is not proved here and no declaration claims it; see the implementation notes for what is missing.
theorem nonempty_iso_of_weilDivisorClassOfInvertibleSheaf_restrict_eq {X : Scheme.{u}}
[IsIntegral X] [IsLocallyNoetherian X] [IsNormal X] (U : X.Opens)
(hU : ∀ x : X, x ∉ U → (2 : ℕ∞) ≤ codimension (IrreducibleCloseds.closureSingleton x))
(M N : X.Modules) (hM : _root_.SheafOfModules.IsCoherent M) (hMr : IsReflexive M)
(hN : _root_.SheafOfModules.IsCoherent N) (hNr : IsReflexive N)
[hMU : SheafOfModules.IsInvertible U.toScheme.sheaf.obj U.toScheme.ringCatSheaf.property
(M.restrict U.ι)]
[hNU : SheafOfModules.IsInvertible U.toScheme.sheaf.obj U.toScheme.ringCatSheaf.property
(N.restrict U.ι)]
(hc : haveI : IsIntegral U.toScheme := isIntegral_of_two_le_codimension_compl U hU
haveI : IsLocallyNoetherian U.toScheme := isLocallyNoetherian_of_isOpenImmersion U.ι
weilDivisorClassOfInvertibleSheaf U.toScheme (M.restrict U.ι) =
weilDivisorClassOfInvertibleSheaf U.toScheme (N.restrict U.ι)) :
Nonempty (M ≅ N)
AlgebraicGeometry.CoherentReflexive.rankOneSkeletonMulEquivWeilDivisorClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/RankOneWeilClassSurjective.lean, line 75.
On an integral locally Noetherian normal scheme the isomorphism classes of rank one coherent reflexive
𝒪_X-modules, under the monoid lawℱ, 𝒢 ↦ (ℱ ⊗_{𝒪_X} 𝒢)^∨∨of [Stacks, Tag 0EBL], are isomorphic to the Weil divisor class groupCl(X), written multiplicatively.The isomorphism is
AlgebraicGeometry.CoherentReflexive.rankOneSkeletonToWeilClass, which sends a module to the class of its restriction to an open subscheme whose complement has codimension at least two and on which it is invertible.
def rankOneSkeletonMulEquivWeilDivisorClass :
Skeleton (RankOneReflexiveModules X) ≃* Multiplicative (weilDivisorClassGroup X)
Tag 0EBN, a lemma
Tag 0EBN in the Stacks Project.
AlgebraicGeometry.CoherentReflexive.isOpen_sectionIsomorphismLocus_and_nonempty_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/ReflexivePowerColimit.lean, line 690.
Let
Xbe an integral locally Noetherian normal scheme,ℱa rank one coherent reflexive𝒪_X-module ands ∈ Γ(X, ℱ). The setU = {x ∈ X | s : 𝒪_{X, x} → ℱ_x is an isomorphism}is open, so thatj : U → Xis an open subscheme, and
j_*𝒪_U = colim (𝒪_X →ˢ ℱ →ˢ ℱ^{[2]} →ˢ ℱ^{[3]} →ˢ ⋯),where
ℱ^{[1]} = ℱandℱ^{[n + 1]} = (ℱ ⊗_{𝒪_X} ℱ^{[n]})^{**}: the coconeAlgebraicGeometry.CoherentReflexive.sectionIsomorphismOpenCoconeon the directed systemAlgebraicGeometry.CoherentReflexive.reflexivePowerModulesof reflexive powers under multiplication bys, with vertexj_*𝒪_U, is a colimit cocone.
theorem isOpen_sectionIsomorphismLocus_and_nonempty_isColimit (F : RankOneReflexiveModules X)
(s : F.module.sections) :
IsOpen (sectionIsomorphismLocus F.module s) ∧
Nonempty (IsColimit (sectionIsomorphismOpenCocone F.obj s))
Stacks.AlgebraicGeometry.ReflexivePowers.reflexivePower, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/ReflexivePowers.lean, line 81. The attribute's comment: “the reflexive powers ℱ^[1] = ℱ, ℱ^[n+1] = (ℱ ⊗ ℱ^[n])^{**}”.
The reflexive powers of
ℱ:ℱ^{[1]} = ℱandℱ^{[n + 1]} = (ℱ ⊗_{𝒪_X} ℱ^{[n]})^{**}; the value at0is𝒪_X, the first term of the system𝒪_X → ℱ → ℱ^{[2]} → ⋯.
noncomputable def reflexivePower (F : X.Modules) : ℕ → X.Modules
Tag 0EBP, a lemma
Tag 0EBP in the Stacks Project.
AlgebraicGeometry.exists_ringKrullDim_stalk_eq_one_of_maximal_irreducible_compl_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/SectionLocusCodimension.lean, line 246.
Assumptions and notation as in [Stacks, Tag 0EBN]:
Xis an integral locally Noetherian normal scheme,ℱis a coherent reflexive𝒪_X-module of rank one,sis a global section ofℱ, andU = sectionIsomorphismLocus F sis the open locus wheresinduces an isomorphism𝒪_{X, x} ⟶ ℱ_x. Ifsis nonzero then every irreducible componentZofX \ Uhas codimension one inX:Zis the closure of a pointξ, its generic point, and the local ring𝒪_{X, ξ}has Krull dimension one, which is the codimension ofZinXby [Stacks, Tag 02IZ].
theorem exists_ringKrullDim_stalk_eq_one_of_maximal_irreducible_compl_locus [IsIntegral X]
[IsLocallyNoetherian X] [IsNormal X] (F : X.Modules)
[_root_.SheafOfModules.IsCoherent F] (hF : IsReflexive F)
(hrank : Scheme.Modules.fiberRank F (genericPoint X) = 1)
(s : F.sections) (hs : s.eval (Opposite.op (⊤ : X.Opens)) ≠ 0) {Z : Set X}
(hZ : Maximal (fun Z : Set X =>
IsIrreducible Z ∧ Z ⊆ (sectionIsomorphismLocus F s)ᶜ) Z) :
∃ ξ : X, closure {ξ} = Z ∧ ringKrullDim (X.presheaf.stalk ξ) = 1
AlgebraicGeometry.codimension_eq_one_of_maximal_irreducible_compl_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/SectionLocusCodimension.lean, line 271. The attribute's comment: “every irreducible component of the complement of the isomorphism locus has codimension one in X”.
Let
Xbe an integral locally Noetherian normal scheme,ℱa coherent reflexive𝒪_X-module of rank one,sa nonzero global section, andU = sectionIsomorphismLocus ℱ sthe open locus of [Stacks, Tag 0EBN] wheresinduces an isomorphism𝒪_{X, x} ⟶ ℱ_x. Then every irreducible componentZofX \ Uhas codimension one inX, in the sense of [Stacks, Tag 02I3].
theorem codimension_eq_one_of_maximal_irreducible_compl_locus [IsIntegral X]
[IsLocallyNoetherian X] [IsNormal X] (F : X.Modules)
[_root_.SheafOfModules.IsCoherent F] (hF : IsReflexive F)
(hrank : Scheme.Modules.fiberRank F (genericPoint X) = 1)
(s : F.sections) (hs : s.eval (Opposite.op (⊤ : X.Opens)) ≠ 0)
(Z : IrreducibleCloseds X)
(hZ : Maximal (fun W : Set X =>
IsIrreducible W ∧ W ⊆ (sectionIsomorphismLocus F s)ᶜ) (Z : Set X)) :
codimension Z = 1
Tag 0EBQ, a remark
Tag 0EBQ in the Stacks Project.
AlgebraicGeometry.objective_0EBQ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/ReflexiveColimitSections.lean, line 125.
For
Aa Noetherian normal domain,Ma finite reflexiveA-module of rank one ands ∈ Mnonzero, the openUof [Stacks, Tag 0EBN] is the complement ofV(𝔭₁) ∪ ⋯ ∪ V(𝔭_r)for the height one primes𝔭ᵢofAin the support ofM ⧸ A·s, andΓ(U, 𝒪_U)is the colimit of the reflexive powersM^{[n]}.
theorem objective_0EBQ (hrank : Module.rank R M = 1) {s : M} (hs : s ≠ 0) :
((AlgebraicGeometry.sectionIsomorphismOpen (Spec R) (tilde M)
(tildeGlobalSection M s) : Set (Spec R)) =
(heightOneSupportZeroLocus R s)ᶜ) ∧
Nonempty (IsColimit (moduleColimitCocone R M hrank hs))
Stacks.AlgebraicGeometry.ReflexiveHeightOnePrimes.sectionIsomorphismPrimes_eq_compl_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/ReflexiveHeightOnePrimes.lean, line 176. The attribute's comment: “the open U of Lemma 31.30.3, on Spec(A), identified with the complement of the support of M/As; the identification of that support with V(p_1) ∪ … ∪ V(p_r) is Lemma 31.30.4 (Tag 0EBP)”.
For
Aa Noetherian normal domain,Ma finite reflexiveA-module ands ∈ Mnonzero, the set of primes at whichs : A_𝔭 → M_𝔭is an isomorphism is the complement of the support ofM ⧸ A·s.
theorem sectionIsomorphismPrimes_eq_compl_support [IsDomain A] [IsNoetherianRing A]
[IsIntegrallyClosed A] [Module.Finite A M] [Module.IsReflexive A M] {s : M} (hs : s ≠ 0) :
sectionIsomorphismPrimes A s = (Module.support A (M ⧸ (A ∙ s)))ᶜ
Stacks.AlgebraicGeometry.ReflexiveHeightOnePrimes.sectionIsomorphismPrimes_eq_compl_heightOneSupportZeroLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/ReflexiveHeightOnePrimes.lean, line 231. The attribute's comment: “the first display, U = Spec(A) \ (V(p_1) ∪ … ∪ V(p_r)), unconditionally; the colimit Γ(U, O_U) = colim M^[n] is AlgebraicGeometry.objective_0EBQ of Divisors/Reflexive/ReflexiveColimitSections.lean”.
For
Aa Noetherian normal domain,Ma finite reflexiveA-module of rank one ands ∈ Mnonzero,U = Spec(A) \ (V(𝔭₁) ∪ ⋯ ∪ V(𝔭_r)), whereUis the set of primes at whichs : A_𝔭 → M_𝔭is an isomorphism and𝔭₁, …, 𝔭_rare the height one primes ofAin the support ofM ⧸ A·s.
theorem sectionIsomorphismPrimes_eq_compl_heightOneSupportZeroLocus [IsDomain A]
[IsNoetherianRing A] [IsIntegrallyClosed A] [Module.Finite A M] [Module.IsReflexive A M]
(hrank : Module.rank A M = 1) {s : M} (hs : s ≠ 0) :
sectionIsomorphismPrimes A s = (heightOneSupportZeroLocus A s)ᶜ
Tag 0EBR, a lemma
Tag 0EBR in the Stacks Project.
Stacks.AlgebraicGeometry.SectionLocusAffine.exists_pos_sectionPowStalk_mem_smul_maximalIdeal_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/SectionLocusAffineTag.lean, line 172. The attribute's comment: “(1) ⇒ (2)”.
[Stacks, Tag 0EBR], (1) ⇒ (2). With
X,ℱ,sandUas in [Stacks, Tag 0EBN]: if the inclusionj : U → Xis affine, then for everyx ∈ X \ Uthere is ann > 0withsⁿ ∈ 𝔪_x ℱ^{[n]}_x.The hypotheses are the source's:
Xintegral, locally Noetherian and normal,ℱcoherent, reflexive (hF) and of rank one (hrank, the fibre rank at the generic point), andsa global section. The reflexive powers, the multiplication bysand the powersⁿare the constructed ones ofReflexivePowers.lean.If
s = 0thens¹ = 0lies in every submodule and there is nothing to prove. OtherwiseUcontains the generic point, so the colimit clause of [Stacks, Tag 0EBN] is available atx; the inverse imageU_xofUunderf_x : Spec 𝒪_{X, x} ⟶ Xis affine because affineness of a morphism is stable under base change, and it misses the closed point becausef_xcarries the closed point tox ∉ U; so𝔪_x Γ(U_x, 𝒪_{U_x})is the unit ideal, and the colimit argumentexists_pos_powElt_mem_smulextracts the positive power.
theorem exists_pos_sectionPowStalk_mem_smul_maximalIdeal_of_isAffineHom
(X : Scheme.{u}) [IsIntegral X] [IsLocallyNoetherian X] [IsNormal X]
(F : X.Modules) [F.IsCoherent] (hF : ReflexiveModules.IsReflexive F)
(hrank : Scheme.Modules.fiberRank F (genericPoint X) = 1) (s : F.sections)
(hj : IsAffineHom (AlgebraicGeometry.sectionIsomorphismOpen X F s).ι)
(x : X) (hx : x ∉ AlgebraicGeometry.sectionIsomorphismOpen X F s) :
∃ n, 0 < n ∧ sectionPowStalk X F s x n ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) •
(⊤ : Submodule ↑(X.presheaf.stalk x) (reflexivePowerStalk F x n))
Stacks.AlgebraicGeometry.SectionLocusAffine.isAffineHom_of_forall_exists_pos_sectionPowStalk_mem_smul_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/SectionLocusAffineTag.lean, line 216. The attribute's comment: “(2) ⇒ (1)”.
[Stacks, Tag 0EBR], (2) ⇒ (1). With
X,ℱ,sandUas in [Stacks, Tag 0EBN]: if for everyx ∈ X \ Uthere is ann > 0withsⁿ ∈ 𝔪_x ℱ^{[n]}_x, then the inclusionj : U → Xis affine.If
s = 0thenUis empty (isEmpty_sectionIsomorphismLocus_of_eval_eq_zero) and the inclusion of an empty open subscheme is affine. OtherwiseUcontains the generic point, the colimit clause of [Stacks, Tag 0EBN] identifies(j_*𝒪_U)_xwithcolim ℱ^{[n]}_x, andmem_smul_of_powElt_mem_smulcarries clause (2) over to1 ∈ 𝔪_x (j_*𝒪_U)_x, which is𝔪_x (j_*𝒪_U)_x = (j_*𝒪_U)_x, at every point offU. That is exactly the hypothesis ofAlgebraicGeometry.isAffineHom_of_forall_map_maximalIdeal_eq_top, the relative-spectrum form of the second half of the source's proof.
theorem isAffineHom_of_forall_exists_pos_sectionPowStalk_mem_smul_maximalIdeal
(X : Scheme.{u}) [IsIntegral X] [IsLocallyNoetherian X] [IsNormal X]
(F : X.Modules) [F.IsCoherent] (hF : ReflexiveModules.IsReflexive F)
(hrank : Scheme.Modules.fiberRank F (genericPoint X) = 1) (s : F.sections)
(h₂ : ∀ x : X, x ∉ AlgebraicGeometry.sectionIsomorphismOpen X F s →
∃ n, 0 < n ∧ sectionPowStalk X F s x n ∈
IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) •
(⊤ : Submodule ↑(X.presheaf.stalk x) (reflexivePowerStalk F x n))) :
IsAffineHom (AlgebraicGeometry.sectionIsomorphismOpen X F s).ι
Sources
Section31.31 Relative Proj#
Section 31.31 of the Stacks Project, Tag 07ZW. 7 tags here are carried by 13 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07ZX, a lemma
Tag 07ZX in the Stacks Project.
Stacks.RelativeProj.Situation.quasiCompact_relativeProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/WeilDivisorClass/RelativeProjQuasiCompact.lean, line 237. References: EGA II (3.4.1), “quasi-compactness”; EGA II (3.1.3), “partial”; EGA II (4.6.18), “partial”.
Stacks 07ZX. The structure morphism of the relative homogeneous spectrum of a quasi-coherent graded algebra is quasi-compact as soon as the algebra is of finite type over its degree-zero part, or generated by its degree-one piece, or has locally nilpotent positive part modulo a finite type quasi-coherent degree-zero submodule.
theorem quasiCompact_relativeProj
(h : IsFiniteTypeOverDegreeZero s ∨ IsFinitelyGeneratedInDegreeOne s ∨
HasNilpotentPositiveQuotient s) :
QuasiCompact (relativeProjToBase s)
Tag 07ZY, a lemma
Tag 07ZY in the Stacks Project.
Stacks.AlgebraicGeometry.RelativeProjFiniteType.locallyOfFiniteType_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjFiniteType/Basic.lean, line 146. The attribute's comment: “relative_proj_finite_type”. References: EGA II (2.7.1), “(ii)”; EGA II (4.6.18), “f of finite type”; EGA II (3.4.1), “locally of finite type”; EGA II (3.1.3), “locally of finite type”.
Stacks 07ZY, first assertion. The structure morphism of the relative homogeneous spectrum of a finite type quasi-coherent graded algebra is locally of finite type.
public theorem locallyOfFiniteType_toBase (hA : IsFiniteType A) :
LocallyOfFiniteType (relativeProj A).toBase
Stacks.AlgebraicGeometry.RelativeProjFiniteType.quasiCompact_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjFiniteType/Basic.lean, line 165. The attribute's comment: “relative_proj_finite_type”. References: EGA II (2.7.1), “(ii)”; EGA II (4.6.18), “f quasi-compact”; EGA II (3.4.1), “quasi-compactness”; EGA II (3.1.3), “quasi-compact”.
Stacks 07ZY, first assertion. The structure morphism of the relative homogeneous spectrum of a finite type quasi-coherent graded algebra is quasi-compact.
public theorem quasiCompact_toBase (hA : IsFiniteType A) :
QuasiCompact (relativeProj A).toBase
Stacks.AlgebraicGeometry.RelativeProjFiniteType.isFiniteType_relativeProjTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjFiniteType/GluedTwists.lean, line 44. The attribute's comment: “relative_proj_twist_finite_type”.
Every twist
𝒪_X(t)on the relative projective spectrumX = Proj_S(A)of a finite type quasi-coherent graded algebra is a finite-type module sheaf. The twists are the homogeneous pieces of the twist datumStacks.AlgebraicGeometry.GluedTwistAlgebra.twistDataOfGradedAlgebraofA.
public theorem isFiniteType_relativeProjTwist (hA : IsFiniteType A) (t : ℤ) :
SheafOfModules.IsFiniteType.{u, u, u}
((GluedTwistAlgebra.twistDataOfGradedAlgebra A).algebra.piece t)
Tag 07ZZ, a lemma
Tag 07ZZ in the Stacks Project.
Stacks.RelativeProj.Situation.universallyClosed_relativeProjToBase_of_isIntegralInDegreeZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/UniversallyClosed.lean, line 81.
Stacks 07ZZ. If the degree-zero part of the graded algebra of a relative
Projsituation is integral over the structure sheaf and the graded algebra is of finite type over its degree-zero part, then the structure morphism of the relative homogeneous spectrum is universally closed.
theorem universallyClosed_relativeProjToBase_of_isIntegralInDegreeZero
(hint : s.IsIntegralInDegreeZero)
(hft : s.IsFiniteTypeOverDegreeZero) :
UniversallyClosed (relativeProjToBase s)
Tag 0800, a lemma
Tag 0800 in the Stacks Project.
Stacks.RelativeProj.isProper_projectiveBundleToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/Proper.lean, line 387. The attribute's comment: “proper, for the projective bundle of a finite locally free module”.
The projection
π : 𝐏(ℰ) ⟶ Xof the projective bundle of a finite locally free sheaf of modules is proper.This is the properness clause of Stacks 0800 for the graded algebra
Sym(ℰ): its degree-zero part is the structure sheaf and it is generated in degree one byℰ, which is spanned by finitely many sections on a cover ofXby affine opens.
theorem isProper_projectiveBundleToBase
[SheafOfModules.IsFiniteLocallyFree.{u, u, u} E] :
IsProper (projectiveBundleToBase X E)
Stacks.RelativeProj.isProper_projectiveBundleToBase_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleProperFiniteType/Basic.lean, line 155. The attribute's comment: “proper, for the projective bundle of a quasi-coherent module of finite type”. References: EGA II (3.4.1), “special case”.
The projection
π : 𝐏(ℰ) ⟶ Xof the projective bundle of a quasi-coherent module of finite type is proper.This is the properness clause of Stacks 0800 for the graded algebra
Sym(ℰ), under the finiteness hypothesis of Tag 01W8 rather than finite local freeness. Both chartwise conditions ofStacks.RelativeProj.Situation.isProper_relativeProjToBasenow hold at every affine open of the base: the degree-zero one is unconditional, and the finite-type one follows from generation in degree one together withAlgebraicGeometry.SheafOfModules.exists_finset_span_of_isFiniteType.
theorem isProper_projectiveBundleToBase_of_isFiniteType [E.IsQuasicoherent] [E.IsFiniteType] :
IsProper (projectiveBundleToBase X E)
Stacks.RelativeProj.Situation.relativeProj_finiteType_iff_and_isLocallyProjective_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProj/DegreeZeroFiniteType.lean, line 221.
Stacks 0800. Let
𝒜be a quasi-coherent graded𝒪_S-algebra over a schemeSandp : Proj_S(𝒜) ⟶ Sits relative homogeneous spectrum. The conditions
𝒜_0is a finite type𝒪_S-module and𝒜is of finite type as an𝒜_0-algebra,𝒜_0is a finite type𝒪_S-module and𝒜is of finite type as an𝒪_S-algebraare equivalent, and under them
pis locally projective and in particular proper.Each condition is written out as the source defines it: finite type of
𝒜_0isSheafOfModules.IsFiniteType, and a quasi-coherent algebra is of finite type over𝒜_0, resp. over𝒪_S, when over every affine openUofSits algebra of sections𝒜(U)is a finite type𝒜_0(U)-algebra, resp. a finite type𝒪_S(U)-algebra.
theorem relativeProj_finiteType_iff_and_isLocallyProjective_isProper :
((SheafOfModules.IsFiniteType (s.algebra.piece 0) ∧
∀ U : s.base.Opens, IsAffineOpen U →
Algebra.FiniteType (s.sectionRingGrading U 0) (s.sectionRing U)) ↔
(SheafOfModules.IsFiniteType (s.algebra.piece 0) ∧
∀ U : s.base.Opens, IsAffineOpen U →
(show Γ(s.base, U) →+* s.sectionRing U from s.sectionRingBaseMap U).FiniteType)) ∧
((SheafOfModules.IsFiniteType (s.algebra.piece 0) ∧
∀ U : s.base.Opens, IsAffineOpen U →
Algebra.FiniteType (s.sectionRingGrading U 0) (s.sectionRing U)) →
IsLocallyProjective (relativeProjToBase s) ∧ IsProper (relativeProjToBase s))
Tag 0B3U, a lemma
Tag 0B3U in the Stacks Project.
AlgebraicGeometry.isProjective_relativeProj_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeVeryAmpleTwist/CanonicalSymSurjective.lean, line 281.
Stacks Project, Tag 0B3U. Let
Sbe a scheme and𝒜a quasi-coherent graded𝒪_S-algebra generated by𝒜_1over𝒜_0with𝒜_1of finite type. Then the projectionProj_S(𝒜) ⟶ Sis projective.The source's proof: the canonical graded-algebra map
Sym(𝒜_1) ⟶ 𝒜induces a closed immersionProj_S(𝒜) ⟶ 𝐏(𝒜_1)overSby Stacks Tag 07ZK (2), and𝐏(𝒜_1)is the projective bundle of a quasi-coherent module of finite type, so that closed immersion is exactly the condition of Stacks Tag 01W8.
theorem isProjective_relativeProj_toBase {S : Scheme.{u}}
(A : Stacks.AlgebraicGeometry.RelativeProjBridge.SheafGradedAlgebra.{u} S)
(hgen : Stacks.AlgebraicGeometry.ProjRepresentsF1.IsGeneratedInDegreeOne A)
(hfin : (A.piece 1).IsFiniteType) :
IsProjective (relativeProj A).toBase
Tag 0D4C, a lemma
Tag 0D4C in the Stacks Project.
Stacks.AlgebraicGeometry.RelativeProjFlat.flat_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjFlat/Basic.lean, line 92. The attribute's comment: “flatness of relative Proj”.
If the homogeneous piece
A_nof a quasi-coherent graded𝒪_S-algebra is a flat𝒪_S-module for every sufficiently largen, the structure morphism of the relative projective spectrum ofAis flat.
public theorem flat_toBase
(hflat : ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
IsFlatOver (𝟙 S : S ⟶ S).toLRSHom.toShHom (A.piece (n : ℤ))) :
Flat (relativeProj A).toBase
Stacks.AlgebraicGeometry.RelativeProjFlat.isFlatOver_twist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjFlat/Twists.lean, line 159. The attribute's comment: “relative flatness of the twists”.
Relative flatness of the twists on a relative projective spectrum.
If the homogeneous piece
A_nof a quasi-coherent graded𝒪_S-algebra is a flat𝒪_S-module for every sufficiently largen, then every homogeneous piece of the glued graded algebra of twists on the relative projective spectrum ofAis flat over the base.The twist data is a parameter, so this is the general form of the assertion, of which the statement for any particular glued family of twists is an instance — in particular for the canonical one,
Stacks.AlgebraicGeometry.GluedTwistAlgebra.twistDataOfGradedAlgebra, which Tag 01NR supplies unconditionally.The criterion used is the affine-open-covering criterion of
AlgebraicGeometry.isFlatOver_tfae, with the affine opens of the base downstairs and, over each of them, the images under the chart of the standard opens of the absoluteProjat homogeneous elements of positive degree.
public theorem isFlatOver_twist (D : TwistData A) (t : ℤ)
(hflat : ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
IsFlatOver (𝟙 S : S ⟶ S).toLRSHom.toShHom (A.piece (n : ℤ))) :
IsFlatOver (relativeProj A).toBase.toLRSHom.toShHom (D.algebra.piece t)
Tag 0D4D, a lemma
Tag 0D4D in the Stacks Project.
Stacks.AlgebraicGeometry.RelativeProjFinitePresentation.isFinitePresentation_relativeProjTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjFinitePresentation/GluedTwists.lean, line 54. The attribute's comment: “twists_finite_presentation”.
Every twist
𝒪_X(t)on the relative projective spectrumX = Proj_S(A)of a quasi-coherent graded algebra whose structure map is of finite presentation over every affine open of the base is a module sheaf of finite presentation. The twists are the homogeneous pieces of the twist datumStacks.AlgebraicGeometry.GluedTwistAlgebra.twistDataOfGradedAlgebraofA.
public theorem isFinitePresentation_relativeProjTwist
(hA : ∀ U : S.Opens, IsAffineOpen U → (A.strHom U).FinitePresentation) (t : ℤ) :
SheafOfModules.IsFinitePresentation.{u, u, u}
((GluedTwistAlgebra.twistDataOfGradedAlgebra A).algebra.piece t)
Stacks.AlgebraicGeometry.RelativeProjFinitePresentation.isFinitePresentation_twist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjFinitePresentation/TwistFinitePresentation.lean, line 97. The attribute's comment: “twists_finite_presentation”.
Stacks 0D4D, second assertion. Every twist on the relative homogeneous spectrum of a quasi-coherent graded algebra whose structure map is of finite presentation over every affine open of the base is a module of finite presentation.
The relative
Projis covered by the images under the charts of the standard opens of the absoluteProjs of the graded rings of sections, on each of which the glued twist is an absolute twist; that reduction isStacks.AlgebraicGeometry.RelativeProjFinitePresentation.isFinitePresentation_twist_of_charts, and the absolute statement it consumes isisFinitePresentation_twistingSheaf_grading.The twist data is a parameter, for the reason given in the implementation notes of this file.
public theorem isFinitePresentation_twist (D : TwistData A)
(hA : ∀ U : S.Opens, IsAffineOpen U → (A.strHom U).FinitePresentation) (t : ℤ) :
SheafOfModules.IsFinitePresentation.{u, u, u} (D.algebra.piece t)
Declarations registered for the tag:
Stacks.AlgebraicGeometry.RelativeProjFinitePresentation.finitePresentation_toBase, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/RelativeProjFinitePresentation/TwistFinitePresentation.lean, line 103 (StacksFrontier): “relative_proj_finite_presentation”.
Sources
Section31.32 Closed subschemes of relative proj#
Section 31.32 of the Stacks Project, Tag 084M. 6 tags here are carried by 29 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0801, a lemma
Tag 0801 in the Stacks Project.
Stacks.ClosedSubschemeProjQuotient.projQuotientIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedSubschemeProjQuotient/Saturation.lean, line 243. The attribute's comment: “the absolute case, over an affine base”. References: EGA II (2.9.2), “more general”.
The isomorphism
Z ≅ Proj (𝒮 / I(Z)). It is the lift ofithrough the closed immersionStacks.ClosedSubschemeProjQuotient.ambientHom, which is invertible because the two closed subschemes have the same ideal sheaf.
def projQuotientIso [CompactSpace (AlgebraicGeometry.Proj 𝒮)]
{Z : Scheme.{u}} (i : Z ⟶ Proj 𝒮) [IsClosedImmersion i] :
Z ≅ projQuotient 𝒮 i
Stacks.ClosedSubschemeProjQuotient.projQuotientIso_hom_comp_ambientHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedSubschemeProjQuotient/Saturation.lean, line 257. The attribute's comment: “the identification is over the ambient Proj; the absolute case, over an affine base”.
The isomorphism is canonical: it is compatible with the two morphisms to
Proj 𝒮, so it is an equality of closed subschemes ofProj 𝒮and not merely an abstract isomorphism.
theorem projQuotientIso_hom_comp_ambientHom [CompactSpace (AlgebraicGeometry.Proj 𝒮)]
{Z : Scheme.{u}} (i : Z ⟶ Proj 𝒮) [IsClosedImmersion i] :
(projQuotientIso 𝒮 i).hom ≫ ambientHom 𝒮 i = i
Stacks.AlgebraicGeometry.RelativeProjGradedIdeal.exists_iso_projQuotient_twistKer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjGradedIdeal/Identification.lean, line 316. References: EGA II (2.9.2), “more general”; EGA II (3.6.2), “more general”.
Stacks Tag 0801. Let
Sbe a scheme,𝒜a quasi-coherent graded𝒪_S-algebra,p : X = Proj_S(𝒜) ⟶ Sthe relative homogeneous spectrum andi : Z ⟶ Xa closed subscheme. Letℐ ⊆ 𝒜be the kernel of the canonical map𝒜 ⟶ ⨁_{d ≥ 0} p_*((i_*𝒪_Z)(d)). Ifpis quasi-compact thenZ = Proj_S(𝒜/ℐ).The ideal is
Stacks.AlgebraicGeometry.RelativeProjGradedIdeal.twistKerGradedIdeal, the degreewise kernel of the homogeneous-section map of Tag 01NR followed by the unit of the pullback–pushforward adjunction ati; the quotient isStacks.AlgebraicGeometry.RelativeProjGradedIdeal.quotAlgebraand the closed immersionProj_S(𝒜/ℐ) ⟶ Proj_S(𝒜)isprojQuotientHom. The equalityZ = Proj_S(𝒜/ℐ)of the source is read, as everywhere in this repository, as an isomorphism over the ambient relative Proj.The proof is
ker_eq_ker_projQuotientHom_twistKerfed toexists_iso_projQuotient_of_ker_eq, which produces the isomorphism from the equality of ideal sheaves byAlgebraicGeometry.IsClosedImmersion.liftandisIso_lift.
theorem exists_iso_projQuotient_twistKer [IsClosedImmersion i]
[QuasiCompact (relativeProj 𝒜).toBase] :
∃ e : Z ≅ (relativeProj (quotAlgebra 𝒜 (twistKerGradedIdeal 𝒜 D i))).scheme,
e.hom ≫ projQuotientHom 𝒜 (twistKerGradedIdeal 𝒜 D i) = i
Tag 0BXK, an example
Tag 0BXK in the Stacks Project.
Stacks.ClosedSubschemeProjQuotient.projQuotientIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedSubschemeProjQuotient/Saturation.lean, line 243. The attribute's comment: “the first assertion: for X = Proj 𝒮 quasi-compact, every closed subscheme Z ⊆ X has the form V₊(I(Z))”. References: EGA II (2.9.2), “more general”.
The isomorphism
Z ≅ Proj (𝒮 / I(Z)). It is the lift ofithrough the closed immersionStacks.ClosedSubschemeProjQuotient.ambientHom, which is invertible because the two closed subschemes have the same ideal sheaf.
def projQuotientIso [CompactSpace (AlgebraicGeometry.Proj 𝒮)]
{Z : Scheme.{u}} (i : Z ⟶ Proj 𝒮) [IsClosedImmersion i] :
Z ≅ projQuotient 𝒮 i
Stacks.ClosedSubschemeProjQuotient.projQuotientIso_hom_comp_ambientHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedSubschemeProjQuotient/Saturation.lean, line 257. The attribute's comment: “the first assertion: the identification Z = V₊(I(Z)) is one of closed subschemes of X = Proj 𝒮, not merely an abstract isomorphism”.
The isomorphism is canonical: it is compatible with the two morphisms to
Proj 𝒮, so it is an equality of closed subschemes ofProj 𝒮and not merely an abstract isomorphism.
theorem projQuotientIso_hom_comp_ambientHom [CompactSpace (AlgebraicGeometry.Proj 𝒮)]
{Z : Scheme.{u}} (i : Z ⟶ Proj 𝒮) [IsClosedImmersion i] :
(projQuotientIso 𝒮 i).hom ≫ ambientHom 𝒮 i = i
AlgebraicGeometry.ProjectiveSpectrum.Proj.mem_idealOfClosedSubscheme_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ProjClosedSubschemeKernel.lean, line 240. The attribute's comment: “ideal_of_a_closed_subscheme”.
An element of
Slies in the ideal of a closed subschemeZ ⊆ Proj 𝒮exactly when, for everyn, the section of𝒪(n)attached to its degree-nhomogeneous component pulls back to zero onZ.
theorem mem_idealOfClosedSubscheme_iff {Z : Scheme.{u}} (i : Z ⟶ Proj 𝒮)
[IsClosedImmersion i] (a : S) :
a ∈ idealOfClosedSubscheme 𝒮 i ↔
∀ n : ℕ, pullbackGlobalSections i (twistingSheaf 𝒮 (n : ℤ))
(degreeSection 𝒮 n (DirectSum.decompose 𝒮 a n)) = 0
AlgebraicGeometry.ProjectiveSpectrum.Proj.idealOfClosedSubscheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ProjIdealOfClosedSubscheme.lean, line 57. The attribute's comment: “ideal_of_a_closed_subscheme”.
The ideal of a closed subscheme of
Proj 𝒮, generated by the homogeneous elements whose canonical twisted sections vanish after pullback to the subscheme.
noncomputable def idealOfClosedSubscheme {Z : Scheme.{u}}
(i : Z ⟶ Proj 𝒮) [IsClosedImmersion i] : Ideal S
AlgebraicGeometry.ProjectiveSpectrum.Proj.idealOfClosedSubscheme_isHomogeneous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ProjIdealOfClosedSubscheme.lean, line 72. The attribute's comment: “ideal_of_a_closed_subscheme”.
The ideal of a closed subscheme is homogeneous: it is generated by homogeneous elements.
theorem idealOfClosedSubscheme_isHomogeneous {Z : Scheme.{u}} (i : Z ⟶ Proj 𝒮)
[IsClosedImmersion i] :
(idealOfClosedSubscheme 𝒮 i).IsHomogeneous 𝒮
Stacks.AlgebraicGeometry.IdealOfClosedSubscheme.idealOfClosedSubscheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealOfClosedSubscheme/Basic.lean, line 267. The attribute's comment: “ideal_of_a_closed_subscheme”.
Stacks 0BXK. The homogeneous ideal of a closed subscheme of
Proj 𝒮, generated by the homogeneous elements whose canonical twisted global section pulls back to zero on the subscheme.
public def idealOfClosedSubscheme {Z : Scheme.{u}} (i : Z ⟶ Proj 𝒮) [IsClosedImmersion i] :
Ideal S
Stacks.AlgebraicGeometry.IdealOfClosedSubscheme.mem_idealOfClosedSubscheme_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealOfClosedSubscheme/Basic.lean, line 278. The attribute's comment: “ideal_of_a_closed_subscheme”.
Stacks 0BXK. An element lies in the ideal of
Zexactly when the section attached to each of its homogeneous components pulls back to zero onZ.In particular the span of the homogeneous equations is the kernel of the canonical graded map to the twisted global sections, in every degree and also on inhomogeneous elements.
public theorem mem_idealOfClosedSubscheme_iff {Z : Scheme.{u}} (i : Z ⟶ Proj 𝒮)
[IsClosedImmersion i] (a : S) :
a ∈ idealOfClosedSubscheme 𝒮 i ↔
∀ n : ℕ, pullbackGlobalSections i (twistingSheaf 𝒮 (n : ℤ))
(degreeSection 𝒮 n ((DirectSum.decompose 𝒮 a) n)) = 0
Stacks.AlgebraicGeometry.IdealOfClosedSubscheme.idealOfClosedSubscheme_isHomogeneous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealOfClosedSubscheme/Basic.lean, line 306. The attribute's comment: “ideal_of_a_closed_subscheme”.
Stacks 0BXK. The ideal of a closed subscheme is homogeneous.
public theorem idealOfClosedSubscheme_isHomogeneous {Z : Scheme.{u}} (i : Z ⟶ Proj 𝒮)
[IsClosedImmersion i] : (idealOfClosedSubscheme 𝒮 i).IsHomogeneous 𝒮
AlgebraicGeometry.ProjectiveSpectrum.Proj.forall_degreeSection_quotientGradingMk_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSaturation/GeneralDegree.lean, line 275. The attribute's comment: “for d the lcm of the degrees of generators of A over A_0, I(V_+(I)) = {x ∈ A | A_{nd} x ⊂ I for all n ≫ 0}; 𝒪_{V_+(I)}(n) is the twisting sheaf of V_+(I) = Proj(A/I), the reading in which the source derives this from Cohomology of Schemes tag 0BXF applied to A/I”.
Stacks 0BXK for a graded ring that is not generated in degree one: the ideal of equations of
V₊(I)is the set of elements that𝒮 (n · d)carries intoIfor everyn ≫ 0, wheredis the least common multiple of the degrees of a finite family of homogeneous generators ofSover𝒮 0:
I(V₊(I)) = {x ∈ A | A_{nd} x ⊆ I for all n ≫ 0}.An element lies in
I(V₊(I)) = Ker(A ⟶ ⨁_{n ≥ 0} Γ(V₊(I), 𝒪_{V₊(I)}(n)))exactly when the twisted section attached to the class of each of its homogeneous components vanishes onV₊(I) = Proj (𝒮 ⧸ I); both sides of the formula are degreewise conditions, and the finitely many components are matched by taking the largest of their exponents.
theorem forall_degreeSection_quotientGradingMk_eq_zero_iff [IsNoetherianRing S] {ι : Type*}
[Fintype ι] (g : ι → S) (e : ι → ℕ) (he : ∀ j, 0 < e j) (hg : ∀ j, g j ∈ 𝒮 (e j))
(hgen : Algebra.adjoin (𝒮 0) (Set.range g) = ⊤) (x : S) :
(∀ n : ℕ, degreeSection (quotientGrading I) n
(quotientGradingMk I n (decompose 𝒮 x n)) = 0) ↔
∃ N : ℕ, ∀ m : ℕ, N ≤ m →
∀ y : S, y ∈ 𝒮 (m * Finset.univ.lcm e) → y * x ∈ I.toIdeal
AlgebraicGeometry.ProjectiveSpectrum.Proj.setOf_forall_degreeSection_quotientGradingMk_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSaturation/GeneralDegree.lean, line 312. The attribute's comment: “for d the lcm of the degrees of generators of A over A_0, I(V_+(I)) = {x ∈ A | A_{nd} x ⊂ I for all n ≫ 0}; 𝒪_{V_+(I)}(n) is the twisting sheaf of V_+(I) = Proj(A/I), the reading in which the source derives this from Cohomology of Schemes tag 0BXF applied to A/I”.
The same, as the equality of sets the source displays:
I(V₊(I)) = {x ∈ A | A_{nd} x ⊂ I for all n ≫ 0}.
theorem setOf_forall_degreeSection_quotientGradingMk_eq_zero [IsNoetherianRing S] {ι : Type*}
[Fintype ι] (g : ι → S) (e : ι → ℕ) (he : ∀ j, 0 < e j) (hg : ∀ j, g j ∈ 𝒮 (e j))
(hgen : Algebra.adjoin (𝒮 0) (Set.range g) = ⊤) :
{x : S | ∀ n : ℕ, degreeSection (quotientGrading I) n
(quotientGradingMk I n (decompose 𝒮 x n)) = 0} =
{x : S | ∃ N : ℕ, ∀ m : ℕ, N ≤ m →
∀ y : S, y ∈ 𝒮 (m * Finset.univ.lcm e) → y * x ∈ I.toIdeal}
AlgebraicGeometry.ProjectiveSpectrum.Proj.mem_idealOfClosedSubscheme_projMap_quotientMk_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSaturation/VPlus.lean, line 208. The attribute's comment: “standard_saturation”.
The saturation formula for the ideal of equations of
V₊(I). Over a Noetherian graded ring generated by𝒮 1over𝒮 0, an element ofSis an equation for the closed subschemeV₊(I) = Proj (𝒮 ⧸ I)exactly when one whole homogeneous component𝒮 Nmultiplies it intoI:
I(V₊(I)) = {x ∈ S | 𝒮 N · x ⊆ I for some N}.
theorem mem_idealOfClosedSubscheme_projMap_quotientMk_iff [IsNoetherianRing S]
(hgen : Algebra.adjoin (𝒮 0) ((𝒮 1 : Set S)) = ⊤) (x : S) :
x ∈ idealOfClosedSubscheme 𝒮 (Proj.map (quotientMk I) hq) ↔
∃ N : ℕ, ∀ y : S, y ∈ 𝒮 N → y * x ∈ I.toIdeal
AlgebraicGeometry.ProjectiveSpectrum.Proj.coe_idealOfClosedSubscheme_projMap_quotientMk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSaturation/VPlus.lean, line 244. The attribute's comment: “standard_saturation”.
The saturation formula as an equality of sets, the shape in which the source displays it:
I(V₊(I)) = {x ∈ S | 𝒮 N · x ⊆ I for some N ≥ 0}.
theorem coe_idealOfClosedSubscheme_projMap_quotientMk [IsNoetherianRing S]
(hgen : Algebra.adjoin (𝒮 0) ((𝒮 1 : Set S)) = ⊤) :
((idealOfClosedSubscheme 𝒮 (Proj.map (quotientMk I) hq) : Ideal S) : Set S) =
{x : S | ∃ N : ℕ, ∀ y : S, y ∈ 𝒮 N → y * x ∈ I.toIdeal}
AlgebraicGeometry.ProjectiveSpectrum.Proj.exists_closedImmersion_idealOfClosedSubscheme_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSaturation/VPlus.lean, line 269. The attribute's comment: “saturated_ideals”.
A homogeneous ideal is the ideal of equations of a closed subscheme of
Proj 𝒮exactly when it is saturated. One direction isAlgebraicGeometry.ProjectiveSpectrum.Proj.saturated_idealOfClosedSubscheme, that an ideal of equations is saturated; the other takesZ = V₊(I)and reads off the saturation formula."Saturated" is spelled as the source does, as the equality of
Iwith its own saturation.
theorem exists_closedImmersion_idealOfClosedSubscheme_eq_iff [IsNoetherianRing S]
(hgen : Algebra.adjoin (𝒮 0) ((𝒮 1 : Set S)) = ⊤) :
(∃ (Z : Scheme.{u}) (i : Z ⟶ Proj 𝒮) (_ : IsClosedImmersion i),
idealOfClosedSubscheme 𝒮 i = I.toIdeal) ↔
(I.toIdeal : Set S) = {x : S | ∃ N : ℕ, ∀ y : S, y ∈ 𝒮 N → y * x ∈ I.toIdeal}
Stacks.WeightedProjSaturation.X_one_dvd_of_mem_grading, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSaturation/WeightedExample.lean, line 141. The attribute's comment: “the counterexample of the last paragraph, A = ℚ[x, y] with deg x = 2 and deg y = 3: for homogeneous f with 6 ∣ deg (f y) one has y ∣ f”.
Stacks 0BXK, in the counterexample of its last paragraph: a homogeneous
fwith6 ∣ deg(f · y)is divisible byy. Every monomialx^a y^boffhas2a + 3b = nwithn + 3divisible by6, sonis odd, sobis odd and in particular nonzero.
theorem X_one_dvd_of_mem_grading (n : ℕ) (f : MvPolynomial (Fin 2) ℚ) (hf : f ∈ grading n)
(h6 : 6 ∣ n + 3) : (MvPolynomial.X 1 : MvPolynomial (Fin 2) ℚ) ∣ f
Stacks.WeightedProjSaturation.mul_X_one_mem_squareIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSaturation/WeightedExample.lean, line 151. The attribute's comment: “the counterexample of the last paragraph: for homogeneous f with 6 ∣ deg (f y) one has f y ∈ I = (y²)”.
Stacks 0BXK, in the counterexample of its last paragraph: hence
f · y ∈ I = (y²).
theorem mul_X_one_mem_squareIdeal (n : ℕ) (f : MvPolynomial (Fin 2) ℚ) (hf : f ∈ grading n)
(h6 : 6 ∣ n + 3) :
f * (MvPolynomial.X 1 : MvPolynomial (Fin 2) ℚ) ∈ squareIdeal
Stacks.WeightedProjSaturation.mem_squareIdeal_of_mem_span_X_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSaturation/WeightedExample.lean, line 164. The attribute's comment: “the counterexample of the last paragraph: (A y)_{6n} ⊆ I for I = (y²), the degreewise test y passes”.
The degreewise test of Stacks 0BXK's general formula, for
yin this ring:(A · y)_{6n} ⊆ Ifor everyn. An element of the ideal(y)that is homogeneous of a degree divisible by6already lies in(y²): divisibility byymakes the exponentbofyin every monomial positive, and2a + 3b = 6nmakes it even, so it is at least2.
theorem mem_squareIdeal_of_mem_span_X_one (n : ℕ) (z : MvPolynomial (Fin 2) ℚ)
(hz : z ∈ Ideal.span {(MvPolynomial.X 1 : MvPolynomial (Fin 2) ℚ)})
(hdeg : z ∈ grading (6 * n)) : z ∈ squareIdeal
Stacks.WeightedProjSaturation.X_zero_pow_mul_X_one_notMem_squareIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjSaturation/WeightedExample.lean, line 188. The attribute's comment: “the counterexample of the last paragraph: xⁿ y ∉ I for every n, with I = (y²)”.
Stacks 0BXK, in the counterexample of its last paragraph:
xⁿ · y ∉ Ifor everyn. The only monomial ofxⁿ ycarries the exponent1aty, which is less than2.
theorem X_zero_pow_mul_X_one_notMem_squareIdeal (n : ℕ) :
(MvPolynomial.X 0 : MvPolynomial (Fin 2) ℚ) ^ n * MvPolynomial.X 1 ∉ squareIdeal
Tag 0BXL, a lemma
Tag 0BXL in the Stacks Project.
AlgebraicGeometry.ProjectiveSpectrum.Proj.projectiveSpace_idealOfClosedSubscheme_isPrincipal_of_codimension_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CodimOneSubscheme/ProjHeightOne.lean, line 294.
Stacks Project, Tag 0BXL. Let
Rbe a Noetherian unique factorization domain and letZbe a closed subscheme ofP^n_R = Proj R[T₀, …, Tₙ]which has no embedded points and every irreducible component of which has codimension one inP^n_R. Then the homogeneous idealI(Z) ⊆ R[T₀, …, Tₙ]corresponding toZis principal.A polynomial ring over a Noetherian UFD is a Noetherian UFD and is generated in degree one, so this is the general
ProjstatementidealOfClosedSubscheme_isPrincipal_of_codimension_one. For the conclusion in the form of a single homogeneous equation seeprojectiveSpace_exists_homogeneous_eq_idealOfClosedSubscheme.
theorem projectiveSpace_idealOfClosedSubscheme_isPrincipal_of_codimension_one (R : Type u)
[CommRing R] [IsDomain R] [IsNoetherianRing R] [UniqueFactorizationMonoid R] (n : ℕ)
{Z : Scheme.{u}} (i : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R))
[IsClosedImmersion i] (hno : HasNoEmbeddedPoints Z)
(hcodim : ∀ W ∈ irreducibleComponents Z, ∀ x : Z,
IsGenericPoint x W → codimension (IrreducibleCloseds.closureSingleton (i.base x)) = 1) :
(idealOfClosedSubscheme
(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R) i).IsPrincipal
Tag 0802, a lemma
Tag 0802 in the Stacks Project.
Stacks.AlgebraicGeometry.RelativeProjTwists.exists_finiteType_degreeQuotientPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjGradedIdeal/FiniteTypeDegreeQuotientPresentation.lean, line 68.
Stacks Project, Tag 0802. A closed subscheme of finite presentation of a quasi-compact relative
Projover a quasi-compact quasi-separated base is the relativeProjof the quotient of𝒜by the graded ideal generated by a quasi-coherent finite type submoduleℱof a single homogeneous piece𝒜_dwithd > 0.The relative case of Tag 0801 — the graded-quotient presentation that
…RelativeProjGradedIdeal.exists_finiteType_degreeQuotientPresentationconsumes — is…RelativeProjTwists.gradedQuotientPresentation, so the statement carries no hypothesis beyond the tag's own.
public theorem exists_finiteType_degreeQuotientPresentation (A : SheafGradedAlgebra S)
{Z : Scheme.{u}} (i : Z ⟶ (relativeProj A).scheme)
[CompactSpace S] [QuasiSeparatedSpace S] [IsClosedImmersion i]
[QuasiCompact (relativeProj A).toBase]
(hi : AlgebraicGeometry.FinitePresentation i) :
∃ d : ℕ, 0 < d ∧ ∃ ℱ : (A.piece (d : ℤ)).Submodule,
ℱ.toSheafOfModules.IsQuasicoherent ∧
SheafOfModules.IsFiniteType.{u, u, u} ℱ.toSheafOfModules ∧
Nonempty (DegreeQuotientPresentation A i ℱ)
Tag 0803, a lemma
Tag 0803 in the Stacks Project.
Stacks.AlgebraicGeometry.RelativeProjGradedIdeal.exists_finiteType_presentation_supp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjGradedIdeal/DegreePresenter.lean, line 137.
Let
Sbe a quasi-compact and quasi-separated scheme,𝒜a quasi-coherent graded𝒪_S-algebra,p : X = Proj_S(𝒜) ⟶ Sthe relative homogeneous spectrum,i : Z ⟶ Xa closed subscheme andU ⊆ San open of the base. Assume
pis quasi-compact,iis of finite presentation,U ∩ p(i(Z)) = ∅,Uis quasi-compact, and- every graded piece
𝒜_nis a finite type𝒪_S-module.Then there are
d > 0and a quasi-coherent finite type𝒪_S-submoduleℱ ⊆ 𝒜_dsuch that(a)
Z = Proj_S(𝒜/ℱ𝒜), read as aDegreeQuotientPresentation— an identification ofZwith the relative Proj of the quotient of𝒜by the graded ideal generated byℱ, overProj_S(𝒜); and(b) the support of
𝒜_d/ℱdoes not meetU.
theorem exists_finiteType_presentation_supp (U : S.Opens)
[CompactSpace S] [QuasiSeparatedSpace S] [IsClosedImmersion i]
[QuasiCompact (relativeProj A).toBase]
(hi : AlgebraicGeometry.FinitePresentation i)
(hU : (U : Set S) ∩ Set.range (i ≫ (relativeProj A).toBase).base = ∅)
(hUc : IsCompact (U : Set S))
(hA : ∀ n : ℕ, SheafOfModules.IsFiniteType.{u, u, u} (A.piece (n : ℤ))) :
∃ d : ℕ, 0 < d ∧ ∃ ℱ : (A.piece (d : ℤ)).Submodule,
ℱ.toSheafOfModules.IsQuasicoherent ∧
SheafOfModules.IsFiniteType.{u, u, u} ℱ.toSheafOfModules ∧
(U : Set S) ∩ (⟨(cokernel ℱ.ι).val, (cokernel ℱ.ι).isSheaf⟩ :
RingedSpace.ModuleSheaf.{u} S.toRingedSpace).supp = ∅ ∧
Nonempty (DegreeQuotientPresentation A i ℱ)
Stacks.AlgebraicGeometry.RelativeProjTwists.exists_finiteType_presentation_supp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjGradedIdeal/FiniteTypePresentationOffSupport.lean, line 81.
Stacks Project, Tag 0803. Let
i : Z ⟶ Proj_S(𝒜)be a closed subscheme of finite presentation of a quasi-compact relativeProjover a quasi-compact quasi-separated base, letUbe a quasi-compact open of the base missing the image ofZ, and let every𝒜_nbe of finite type. ThenZis the relativeProjof the quotient of𝒜by the graded ideal generated by a quasi-coherent finite type submoduleℱof a single homogeneous piece𝒜_dwithd > 0, andℱmay be chosen so that the support of𝒜_d/ℱis disjoint fromU.The relative case of Tag 0801 — the vanishing-ideal presentation that
…RelativeProjGradedIdeal.exists_finiteType_presentation_supp_of_vanishingIdealconsumes — is…RelativeProjTwists.vanishingIdealPresentation, so the statement carries no hypothesis beyond the tag's own.
public theorem exists_finiteType_presentation_supp (A : SheafGradedAlgebra S) {Z : Scheme.{u}}
(i : Z ⟶ (relativeProj A).scheme) (U : S.Opens)
[CompactSpace S] [QuasiSeparatedSpace S] [IsClosedImmersion i]
[QuasiCompact (relativeProj A).toBase]
(hi : AlgebraicGeometry.FinitePresentation i)
(hU : (U : Set S) ∩ Set.range (i ≫ (relativeProj A).toBase).base = ∅)
(hUc : IsCompact (U : Set S))
(hA : ∀ n : ℕ, SheafOfModules.IsFiniteType.{u, u, u} (A.piece (n : ℤ))) :
∃ d : ℕ, 0 < d ∧ ∃ ℱ : (A.piece (d : ℤ)).Submodule,
ℱ.toSheafOfModules.IsQuasicoherent ∧
SheafOfModules.IsFiniteType.{u, u, u} ℱ.toSheafOfModules ∧
(U : Set S) ∩ (⟨(cokernel ℱ.ι).val, (cokernel ℱ.ι).isSheaf⟩ :
RingedSpace.ModuleSheaf.{u} S.toRingedSpace).supp = ∅ ∧
Nonempty (DegreeQuotientPresentation A i ℱ)
Tag 0B3V, a lemma
Tag 0B3V in the Stacks Project.
Stacks.RelativeProj.isClosedImmersion_of_section_projectiveBundleToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/Section.lean, line 61. The attribute's comment: “closed immersion”.
A section of the projection of a projective bundle is a closed immersion. Since
π : 𝐏(F) ⟶ Xis separated (Tag 01O2) andσ ≫ π = 𝟙 Xis an isomorphism,σis a closed immersion.
theorem isClosedImmersion_of_section_projectiveBundleToBase (X : Scheme.{u}) (F : X.Modules)
[F.IsQuasicoherent] (σ : X ⟶ projectiveBundle X F)
(hσ : σ ≫ projectiveBundleToBase X F = 𝟙 X) : IsClosedImmersion σ
Stacks.RelativeProj.sectionOfInvertibleQuotient, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/SectionOfQuotient.lean, line 339. The attribute's comment: “from an invertible quotient to a section: the construction”.
A surjection
q : E ⟶ ℒonto an invertible𝒪_X-module determines a section ofπ : 𝐏(E) ⟶ X. This is the direction of Tag 0B3V's bijection that produces a section:qdetermines a unital homomorphism(𝟙_X)^*Sym(E) ⟶ ⨁_n ℒ^{⊗ n}of sheaves of graded algebras whose degree-one component is surjective — a quadruple of Section 01NS of degree one over𝟙_X— and the representability of the functor of quadruples classifies that quadruple by a morphismX ⟶ 𝐏(E)overX.
def sectionOfInvertibleQuotient [Epi q] : X ⟶ projectiveBundle X E
Stacks.RelativeProj.sectionOfInvertibleQuotient_comp_projectiveBundleToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/SectionOfQuotient.lean, line 345. The attribute's comment: “from an invertible quotient to a section: it is a section of the projection”.
The morphism of
sectionOfInvertibleQuotientis a section ofπ : 𝐏(E) ⟶ X.
theorem sectionOfInvertibleQuotient_comp_projectiveBundleToBase [Epi q] :
sectionOfInvertibleQuotient X E L q ≫ projectiveBundleToBase X E = 𝟙 X
Stacks.RelativeProj.exists_iso_of_sectionOfInvertibleQuotient_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundle/SectionOfQuotient.lean, line 412. The attribute's comment: “from an invertible quotient to a section: the map is injective, i.e. a section determines the invertible quotient it comes from up to isomorphism of the quotient module”.
Two surjections onto invertible modules determining the same section of
πdiffer by an isomorphism of their targets. This is the injectivity of Tag 0B3V's map from invertible quotients to sections: the two quadruples are strictly equivalent, which gives an isomorphismβ : ℒ ≅ ℒ'carrying one twisting to the other, and in degree one that equation — precomposed with the pullback of the degree-one generator ofSym(E)and postcomposed with the identification(ℒ')^{⊗ 1} ≅ ℒ'— isq ≫ β = q'.
theorem exists_iso_of_sectionOfInvertibleQuotient_eq [Epi q]
(L' : SheafOfModules.{u} (structureRingSheaf X.toRingedSpace))
[Stacks.SheafOfModules.IsInvertible X.toRingedSpace.presheaf (isSheafStruct X) L']
(q' : E ⟶ L') [Epi q']
(h : sectionOfInvertibleQuotient X E L q = sectionOfInvertibleQuotient X E L' q') :
∃ α : L ≅ L', q ≫ α.hom = q'
Stacks.RelativeProj.projectiveBundle_sections_classification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleConormal/SectionsClause.lean, line 656. References: EGA II (4.2.10), “special case”; EGA II (4.2.3), “Case Y = X”; SGA 4 XVIII (1.3.3), “partial”.
[Stacks, Tag 0B3V]. Let
Xbe a scheme,ℰa quasi-coherent𝒪_X-module andπ : 𝐏(ℰ) ⟶ Xits projective bundle (projectiveBundle,projectiveBundleToBase), with tautological quotientπ^*ℰ ⟶ 𝒪(1)(tautologicalDatum ℰ). Then:
- the bijection:
projectiveBundleSectionsEquivis a bijection from the sectionsσofπonto the invertible quotientsq : ℰ → 𝓛up to isomorphism, sendingσto the class ofσ^*of the tautological quotient —σgoes to the class ofqexactly when there ise : σ^*𝒪(1) ≅ 𝓛carryingσ^*of the tautological quotient toq;- every section
σis a closed immersion;- the canonical isomorphism
projectiveBundleConormalIso : Ker(q) ⊗ 𝓛^{⊗ -1} ≅ 𝒞_{σ(X)/𝐏(ℰ)}forσmatched withqthroughe, whose underlying map is the canonical mapStacks.ProjectiveBundleConormal.conormalCanonicalMap(locallyk ⊗ s^{-1} ↦ k/s) read through the base-change map of conormal sheaves along the presentation comparisonbundlePresentationIsoof𝐏(ℰ);- compatibility with base change along any morphism
g : X' ⟶ X, for sections lying over each other alongprojectiveBundleBaseChange: the bijection sendsσ'to the base changeStacks.ProjectiveBundleQuotients.baseChangeClassof the class ofσ; and the square formed byg^*of the canonical isomorphism atσ, the canonical isomorphism atσ', the base changeStacks.Divisors.conormalSourceBaseChangeof the source and the base-change mapStacks.Conormal.conormalBaseChangeMapof conormal sheaves commutes.No hypothesis is placed on
X,X',g, or onℰbeyond quasi-coherence.
theorem projectiveBundle_sections_classification :
(∀ (σ : X ⟶ projectiveBundle X E) (hσ : σ ≫ projectiveBundleToBase X E = 𝟙 X)
(Q : Stacks.Divisors.InvertibleQuotient X E),
projectiveBundleSectionsEquiv ⟨σ, hσ⟩ =
Quotient.mk (Stacks.Divisors.invertibleQuotientSetoid X E) Q ↔
∃ e : (Scheme.Modules.pullback σ).obj (tautologicalDatum E).twist ≅ Q.L,
(tautologicalDatum E).pullbackQuotientMap σ hσ ≫ e.hom = Q.q) ∧
(∀ (σ : X ⟶ projectiveBundle X E), σ ≫ projectiveBundleToBase X E = 𝟙 X →
IsClosedImmersion σ) ∧
(∀ (Q : Stacks.Divisors.InvertibleQuotient X E) (σ : X ⟶ projectiveBundle X E)
(hσ : σ ≫ projectiveBundleToBase X E = 𝟙 X)
(e : (Scheme.Modules.pullback σ).obj (tautologicalDatum E).twist ≅ Q.L)
(hqe : (tautologicalDatum E).pullbackQuotientMap σ hσ ≫ e.hom = Q.q),
haveI := isClosedImmersion_of_section_projectiveBundleToBase X E σ hσ
(projectiveBundleConormalIso E Q hσ e hqe).hom =
conormalCanonicalMap E Q (presentationSection_comp_toBase E σ hσ)
(presentationClassifyingIso E Q e)
(sectionQuotientMap_comp_presentationClassifyingIso E Q hσ e hqe) ≫
(Scheme.Modules.pullbackId X).inv.app _ ≫
Stacks.Conormal.conormalBaseChangeMap (presentationSection_square E σ)) ∧
(∀ (X' : Scheme.{u}) (g : X' ⟶ X) (σ : X ⟶ projectiveBundle X E)
(hσ : σ ≫ projectiveBundleToBase X E = 𝟙 X)
(σ' : X' ⟶ projectiveBundle X' ((Scheme.Modules.pullback g).obj E))
(hσ' : σ' ≫ projectiveBundleToBase X' ((Scheme.Modules.pullback g).obj E) = 𝟙 X'),
σ' ≫ projectiveBundleBaseChange g E _ (Iso.refl _) = g ≫ σ →
projectiveBundleSectionsEquiv ⟨σ', hσ'⟩ =
Stacks.ProjectiveBundleQuotients.baseChangeClass g (Iso.refl _)
(projectiveBundleSectionsEquiv ⟨σ, hσ⟩)) ∧
(∀ (X' : Scheme.{u}) (g : X' ⟶ X) (E' : X'.Modules) [E'.IsQuasicoherent]
(hE : E' ≅ (Scheme.Modules.pullback g).obj E)
(Q : Stacks.Divisors.InvertibleQuotient X E)
(Q' : Stacks.Divisors.InvertibleQuotient X' E')
(hL : Q'.L ≅ (Scheme.Modules.pullback g).obj Q.L)
(hq : Q'.q ≫ hL.hom = hE.hom ≫ (Scheme.Modules.pullback g).map Q.q)
(σ : X ⟶ projectiveBundle X E) (hσ : σ ≫ projectiveBundleToBase X E = 𝟙 X)
(e : (Scheme.Modules.pullback σ).obj (tautologicalDatum E).twist ≅ Q.L)
(hqe : (tautologicalDatum E).pullbackQuotientMap σ hσ ≫ e.hom = Q.q)
(σ' : X' ⟶ projectiveBundle X' E') (hσ' : σ' ≫ projectiveBundleToBase X' E' = 𝟙 X')
(e' : (Scheme.Modules.pullback σ').obj (tautologicalDatum E').twist ≅ Q'.L)
(hqe' : (tautologicalDatum E').pullbackQuotientMap σ' hσ' ≫ e'.hom = Q'.q)
(comm : σ' ≫ projectiveBundleBaseChange g E E' hE = g ≫ σ),
haveI := isClosedImmersion_of_section_projectiveBundleToBase X E σ hσ
haveI := isClosedImmersion_of_section_projectiveBundleToBase X' E' σ' hσ'
(Stacks.Divisors.conormalSourceBaseChange g E E' hE Q Q' hL hq).hom ≫
(projectiveBundleConormalIso E' Q' hσ' e' hqe').hom =
(Scheme.Modules.pullback g).map (projectiveBundleConormalIso E Q hσ e hqe).hom ≫
Stacks.Conormal.conormalBaseChangeMap comm)
Sources
Section31.33 Blowing up#
Section 31.33 of the Stacks Project, Tag 01OF. 14 tags here are carried by 43 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01OG, a definition
Tag 01OG in the Stacks Project.
AlgebraicGeometry.blowUp, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/BlowUp.lean, line 63. The attribute's comment: “blowup morphism”. References: EGA II (8.1.3), “qcoh ideal case”; EGA IV (19.4.1), “X'=Proj(⊕J^n)”.
Stacks Project, Tag 01OG. The blowup of
Xin the quasi-coherent idealI: the relativeProjof the Rees algebra⨁ₙ Iⁿ.
public noncomputable abbrev blowUp {X : Scheme.{u}} (I : X.IdealSheafData) : Scheme.{u}
AlgebraicGeometry.blowUpToBase, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/BlowUp.lean, line 71. The attribute's comment: “blowup morphism”. References: EGA II (8.1.3), “qcoh ideal case”; EGA IV (19.4.1), “structural morphism f”.
Stacks Project, Tag 01OG. The blowup morphism: the structure morphism of the blowup of
XinItoX.
public noncomputable abbrev blowUpToBase {X : Scheme.{u}} (I : X.IdealSheafData) :
blowUp I ⟶ X
AlgebraicGeometry.exceptionalIdeal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/BlowUp.lean, line 77. The attribute's comment: “exceptional ideal sheaf”.
The inverse-image ideal defining the exceptional divisor.
public noncomputable abbrev exceptionalIdeal {X : Scheme.{u}} (I : X.IdealSheafData) :
(blowUp I).IdealSheafData
AlgebraicGeometry.exceptionalDivisor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/BlowUp.lean, line 84. The attribute's comment: “exceptional divisor scheme”. References: EGA IV (19.4.1), “Y'=f^{-1}(Y)”; SGA 7 XVIII (2.1).
Stacks Project, Tag 01OG. The exceptional divisor is the inverse image of the closed subscheme cut out by
I.
public noncomputable abbrev exceptionalDivisor {X : Scheme.{u}} (I : X.IdealSheafData) :
Scheme.{u}
Stacks.Blowup.exists_reesAlgebraData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebraSheaf.lean, line 805. The attribute's comment: “Rees algebra sheaf”.
Stacks Project, Tag 01OG. A graded sheaf with the canonical affine-local description of
⨁ₙ Iⁿexists.
public theorem exists_reesAlgebraData {X : Scheme.{u}} (I : X.IdealSheafData) :
Nonempty (ReesAlgebraData I)
Stacks.Blowup.blowUp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesSheafData.lean, line 233. The attribute's comment: “the blowup as a scheme”. References: EGA II (8.1.3); EGA IV (19.4.1); SGA 6 VII (1.8).
The blowup of a scheme
Sin a quasi-coherent sheaf of idealsℐ: the relativeProjof the Rees algebra⨁_{n ≥ 0} ℐⁿ.
def blowUp : Scheme.{u}
Stacks.Blowup.blowUpToBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesSheafData.lean, line 237. The attribute's comment: “the blowup morphism”.
The structure morphism of the blowup to its base.
def blowUpToBase : blowUp ℐ ⟶ S
Stacks.Blowup.isPullback_blowUpChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesSheafData.lean, line 256. The attribute's comment: “the affine charts of the blowup”.
The blowup restricted to an affine open
Uof the base isProjof the Rees algebra ofℐ(U): the chart overUis the preimage ofUunder the blowup morphism.
theorem isPullback_blowUpChart (U : S.affineOpens) :
IsPullback (Stacks.RelativeProj.chartToOpen (fun W : S.affineOpens ↦ reesGrading (ℐ.ideal W))
U (reesBase ℐ U)) (blowUpChart ℐ U) U.1.ι (blowUpToBase ℐ)
Stacks.Blowup.exceptionalIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesSheafData.lean, line 269. The attribute's comment: “the exceptional ideal sheaf”.
The ideal sheaf of the exceptional divisor: the inverse image of
ℐunder the blowup morphism.
def exceptionalIdeal : (blowUp ℐ).IdealSheafData
Stacks.Blowup.exceptionalDivisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesSheafData.lean, line 274. The attribute's comment: “the exceptional divisor”. References: SGA 7 XVIII (2.1).
The exceptional divisor of the blowup: the closed subscheme of the blowup cut out by the inverse image of
ℐ.
def exceptionalDivisor : Scheme.{u}
Tag 0804, a lemma
Tag 0804 in the Stacks Project.
Stacks.Blowup.reesAwayEquivAffineBlowup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/AffineChart.lean, line 229. The attribute's comment: “the chart D₊(a⁽¹⁾) is Spec of the affine blowup algebra”.
Stacks Project, Tag 0804. For
a ∈ Ithe standard affine chart ofProjof the Rees algebra at the degree-one elementa⁽¹⁾is the affine blowup algebraR[I/a]: the degree-zero part of the localization ofR[It]ata⁽¹⁾isR[I/a].This is the chart computation behind the second assertion of tag 0804; the covering statement itself is
Stacks.Blowup.iSup_opensRange_blowUpAffineChart.
def reesAwayEquivAffineBlowup (ha : a ∈ I) :
Away (reesGrading I) (reesDegOne I ha) ≃+* affineBlowup I a
Stacks.Blowup.iSup_opensRange_blowUpAffineChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/AffineChart.lean, line 409. The attribute's comment: “b⁻¹(U) is covered by the spectra of the affine blowup algebras”.
Stacks Project, Tag 0804, second assertion. Let
b : X' ⟶ Sbe the blowup of a schemeSin a quasi-coherent sheaf of idealsℐ, and letUbe an affine open ofS. Thenb⁻¹(U)is covered by the spectra of the affine blowup algebrasΓ(S, U)[ℐ(U)/a]fora ∈ ℐ(U): the morphismsStacks.Blowup.blowUpAffineChartare open immersions whose images have supremumb⁻¹(U).Together with the first assertion,
Stacks.Blowup.isPullback_blowUpChart, this completes tag 0804.
theorem iSup_opensRange_blowUpAffineChart (U : S.affineOpens) :
⨆ r : ℐ.ideal U, (blowUpAffineChart ℐ U r.2).opensRange
= blowUpToBase ℐ ⁻¹ᵁ (U : S.Opens)
AlgebraicGeometry.affineBlowupStandardOpenIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/AffineCharts.lean, line 539. The attribute's comment: “affine blowup algebra chart”.
The standard affine chart of the Rees projective spectrum is canonically the spectrum of the affine blowup algebra.
public noncomputable def affineBlowupStandardOpenIso {X : Scheme.{u}}
(I : X.IdealSheafData) (U : X.affineOpens) (a : I.ideal U) :
letI := (reesSituation I).sectionRingGradedRing U.1
letI := (reesSituation I).sectionRingGradingGradedRing U.1
Spec (.of <| affineBlowupAlgebra (I.ideal U) (a : X.presheaf.obj (.op U.1))
(Localization.Away (a : X.presheaf.obj (.op U.1)))) ≅
(Proj.basicOpen ((reesSituation I).sectionRingGrading U.1)
(reesDegreeOne I U a).1).toScheme
AlgebraicGeometry.affineBlowupStandardOpenIso_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/AffineCharts.lean, line 558. The attribute's comment: “affine blowup chart over the base”.
The affine blowup chart is an isomorphism over the affine base: its structure map is induced by the canonical inclusion of the ring into its blowup algebra.
public theorem affineBlowupStandardOpenIso_over {X : Scheme.{u}}
(I : X.IdealSheafData) (U : X.affineOpens) (a : I.ideal U) :
letI := (reesSituation I).sectionRingGradedRing U.1
letI := (reesSituation I).sectionRingGradingGradedRing U.1
(affineBlowupStandardOpenIso I U a).hom ≫
(Proj.basicOpen ((reesSituation I).sectionRingGrading U.1)
(reesDegreeOne I U a).1).ι ≫
Stacks.RelativeProj.Situation.projInclusionToOpen (reesSituation I) U.1 U.2 =
Spec.map (CommRingCat.ofHom
(algebraMap (X.presheaf.obj (.op U.1))
(affineBlowupAlgebra (I.ideal U) (a : X.presheaf.obj (.op U.1))
(Localization.Away (a : X.presheaf.obj (.op U.1)))))) ≫
U.2.isoSpec.inv
AlgebraicGeometry.affineBlowupStandardOpenIso_fraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/AffineCharts.lean, line 585. The attribute's comment: “canonical affine blowup fractions”.
On the standard chart at
a, a degree-one sectionbdivided byacorresponds to the generating fractionb/ain the affine blowup algebra.
public theorem affineBlowupStandardOpenIso_fraction {X : Scheme.{u}}
(I : X.IdealSheafData) (U : X.affineOpens) (a b : I.ideal U) :
letI := (reesSituation I).sectionRingGradedRing U.1
letI := (reesSituation I).sectionRingGradingGradedRing U.1
(((Spec.preimage
((affineBlowupStandardOpenIso I U a).hom ≫
(Proj.basicOpenIsoSpec
((reesSituation I).sectionRingGrading U.1)
(reesDegreeOne I U a).1 (reesDegreeOne I U a).2 (by omega)).hom)).hom
(HomogeneousLocalization.Away.mk
((reesSituation I).sectionRingGrading U.1)
(reesDegreeOne I U a).2 1 (reesDegreeOne I U b).1
(by simp)) :
affineBlowupAlgebra (I.ideal U) (a : X.presheaf.obj (.op U.1))
(Localization.Away (a : X.presheaf.obj (.op U.1)))) :
Localization.Away (a : X.presheaf.obj (.op U.1))) =
IsLocalization.mk' (Localization.Away (a : X.presheaf.obj (.op U.1)))
(b : X.presheaf.obj (.op U.1))
⟨(a : X.presheaf.obj (.op U.1)), Submonoid.mem_powers _⟩
AlgebraicGeometry.blownUpAffine_chart_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/AffineCharts.lean, line 699. The attribute's comment: “affine chart covering”.
Degree-one Rees elements give an affine open cover of the inverse image of an affine open under the blowup morphism.
public theorem blownUpAffine_chart_cover {X : Scheme.{u}} (I : X.IdealSheafData)
(U : X.affineOpens) :
letI := (reesSituation I).sectionRingGradedRing U.1
letI := (reesSituation I).sectionRingGradingGradedRing U.1
(⋃ a : I.ideal U,
Set.range ((Proj.basicOpen ((reesSituation I).sectionRingGrading U.1)
(reesDegreeOne I U a).1).ι ≫
Stacks.RelativeProj.Situation.relativeProjChart (reesSituation I) U)) =
(blowUpToBase I ⁻¹ᵁ U.1).1
Stacks.Blowup.isPullback_blowUpChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesSheafData.lean, line 256. The attribute's comment: “the canonical identification of b⁻¹(U) with Proj of the Rees algebra”.
The blowup restricted to an affine open
Uof the base isProjof the Rees algebra ofℐ(U): the chart overUis the preimage ofUunder the blowup morphism.
theorem isPullback_blowUpChart (U : S.affineOpens) :
IsPullback (Stacks.RelativeProj.chartToOpen (fun W : S.affineOpens ↦ reesGrading (ℐ.ideal W))
U (reesBase ℐ U)) (blowUpChart ℐ U) U.1.ι (blowUpToBase ℐ)
Declarations registered for the tag:
Stacks.RelativeProj.Situation.relativeProjChart_isPullback, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/AffineCharts.lean, line 56 (StacksFrontier): “canonical local projective-spectrum identification”.
Tag 0805, a lemma
Tag 0805 in the Stacks Project.
AlgebraicGeometry.exists_isPullback_blowUpToBase_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FlatBaseChange.lean, line 55.
Stacks Project, Tag 0805. Blowing up commutes with flat base change: for a flat
g : X₁ ⟶ X₂and a quasi-coherent idealIonX₂, the blowup ofX₁in the inverse image ofIsits in a cartesian square over the blowup ofX₂inI.
theorem exists_isPullback_blowUpToBase_comap {X₁ X₂ : Scheme.{u}} (g : X₁ ⟶ X₂) [Flat g]
(I : X₂.IdealSheafData) :
∃ h : blowUp (I.comap g) ⟶ blowUp I,
IsPullback (blowUpToBase (I.comap g)) h g (blowUpToBase I)
Tag 02OS, a lemma
Tag 02OS in the Stacks Project.
Stacks.Blowup.isEffectiveCartierDivisor_exceptionalIdeal, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ExceptionalCartier.lean, line 572. The attribute's comment: “exceptional_effective_cartier”. References: EGA IV (19.4.1).
Stacks Project, Tag 02OS part (2). For a scheme
Xand a quasi-coherent ideal sheafI, the exceptional divisor of the blowup ofXinI— the inverse image of the closed subscheme cut out byI— is an effective Cartier divisor on the blowup.Declared as an
instance, as the tagged statement has it: the head is the ideal sheaf of the exceptional divisor, so instance search is not widened.
instance isEffectiveCartierDivisor_exceptionalIdeal {X : Scheme.{u}} (I : X.IdealSheafData) :
Stacks.Divisors.IsEffectiveCartierDivisor (exceptionalIdeal I)
Stacks.Blowup.ideal_exceptionalIdeal_blowUpAffineChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ExceptionalChart.lean, line 259. The attribute's comment: “the exceptional ideal is generated by one section on an affine chart”.
Stacks Project, Tag 02OS, second assertion, affine-local form. On the affine open of the blowup underlying the chart
Spec Γ(S, U)[ℐ(U)/a], the exceptional ideal is generated byStacks.Blowup.exceptionalChartSection.This is the equation
IA' = aA'of the proof of Stacks tag 02OS, for the chart supplied by the second assertion of Stacks tag 0804, transported fromStacks.Blowup.ideal_comap_exceptionalIdeal_blowUpAffineChartacross the chart's identification of sections.
theorem ideal_exceptionalIdeal_blowUpAffineChart (U : S.affineOpens)
{a : Γ(S, U.1)} (ha : a ∈ ℐ.ideal U) :
(exceptionalIdeal ℐ).ideal ⟨blowUpAffineChart ℐ U ha ''ᵁ ⊤,
(isAffineOpen_top _).image_of_isOpenImmersion _⟩ =
Ideal.span {exceptionalChartSection ℐ U ha}
Stacks.Blowup.exceptionalChartSection_mem_nonZeroDivisors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ExceptionalChart.lean, line 280. The attribute's comment: “the generator on an affine chart is a nonzerodivisor”.
Stacks Project, Tag 02OS, second assertion, affine-local form. The generator of the exceptional ideal on an affine chart of the blowup is a nonzerodivisor.
This is the sentence "
amaps to a nonzerodivisor inA'" of the proof of Stacks tag 02OS.
theorem exceptionalChartSection_mem_nonZeroDivisors (U : S.affineOpens)
{a : Γ(S, U.1)} (ha : a ∈ ℐ.ideal U) :
exceptionalChartSection ℐ U ha ∈
nonZeroDivisors Γ(blowUp ℐ, blowUpAffineChart ℐ U ha ''ᵁ ⊤)
Stacks.Blowup.exists_span_eq_ideal_exceptionalIdeal_blowUpAffineChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ExceptionalChart.lean, line 299. The attribute's comment: “the exceptional ideal is generated by a nonzerodivisor on an affine chart”.
Stacks Project, Tag 02OS, second assertion, affine-local form. On the affine open of the blowup underlying the chart
Spec Γ(S, U)[ℐ(U)/a], the exceptional ideal is generated by a single section, and that section is a nonzerodivisor.This is the sentence "Then
IA' = aA'andamaps to a nonzerodivisor inA'" of the proof of Stacks tag 02OS, for the chart supplied by the second assertion of Stacks tag 0804. The generator isStacks.Blowup.exceptionalChartSection.
theorem exists_span_eq_ideal_exceptionalIdeal_blowUpAffineChart (U : S.affineOpens)
{a : Γ(S, U.1)} (ha : a ∈ ℐ.ideal U) :
∃ t ∈ nonZeroDivisors Γ(blowUp ℐ, blowUpAffineChart ℐ U ha ''ᵁ ⊤),
(exceptionalIdeal ℐ).ideal ⟨blowUpAffineChart ℐ U ha ''ᵁ ⊤,
(isAffineOpen_top _).image_of_isOpenImmersion _⟩ = Ideal.span {t}
Stacks.Blowup.isLocallyPrincipal_exceptionalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ExceptionalChart.lean, line 317. The attribute's comment: “the exceptional divisor is a locally principal closed subscheme”.
Stacks Project, Tag 02OS, second assertion, local principality. The exceptional divisor of the blowup of a scheme in a quasi-coherent sheaf of ideals is a locally principal closed subscheme: around every point of the blowup there is an affine open on which the exceptional ideal is generated by one element.
Every point of the blowup lies over an affine open
Uof the base, hence in one of the chartsSpec Γ(S, U)[ℐ(U)/a]by the second assertion of Stacks tag 0804 (Stacks.Blowup.iSup_opensRange_blowUpAffineChart), and on that chart the exceptional ideal is principal byStacks.Blowup.exists_span_eq_ideal_exceptionalIdeal_blowUpAffineChart.
theorem isLocallyPrincipal_exceptionalIdeal :
Stacks.Divisors.IsLocallyPrincipal (exceptionalIdeal ℐ)
AlgebraicGeometry.isIso_blowUp_restrict_compl_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/IsomorphismOffCenter/Basic.lean, line 234. The attribute's comment: “isomorphism_off_center”. References: SGA 7 XVIII (2.1), “more general”.
Stacks Project, Tag 02OS. The blowup of a scheme in a quasi-coherent ideal sheaf is an isomorphism over the open complement of the closed subscheme the ideal cuts out.
public theorem isIso_blowUp_restrict_compl_support (I : X.IdealSheafData) :
IsIso (blowUpToBase I ∣_ (⟨I.supportᶜ, I.support.isClosed.isOpen_compl⟩ : X.Opens))
AlgebraicGeometry.twistOneIsoExceptionalIdealModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/TwistOneExceptionalIdeal.lean, line 155. The attribute's comment: “part (3)”. References: EGA IV (19.4.1), “(1)”.
[Stacks, Tag 02OS] part (3). For a scheme
Xand a quasi-coherent sheaf of idealsℐon it, the twisting sheaf𝒪_{X'}(1)of the blowupb : X' ⟶ XofXinℐis the ideal sheaf of the exceptional divisor, the inverse imageℐ·𝒪_{X'}of the centre.No hypothesis is carried:
Xis an arbitrary scheme andℐan arbitrary quasi-coherent sheaf of ideals. Parts (1) and (2) of the tag areAlgebraicGeometry.isIso_blowUp_restrict_compl_supportandStacks.Blowup.isEffectiveCartierDivisor_exceptionalIdeal.
def twistOneIsoExceptionalIdealModule : blowUpTwist I 1 ≅ exceptionalIdealModule I
Tag 0806, a lemma
Tag 0806 in the Stacks Project.
Stacks.Blowup.isTerminal_blowUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ClassifyingMorphism.lean, line 478. References: EGA IV (19.4.1); SGA 6 XIII (7.1.4), “more general”.
Stacks Project, Tag 0806. The universal property of blowing up. The blowup of a scheme
Xin a quasi-coherent ideal sheafℐis a final object of the categoryCof schemes overXon which the inverse image of the centre is an effective Cartier divisor.Unconditional. The five geometric inputs of
Stacks.Blowup.exists_nonempty_isTerminal, which is the uniqueness half of the tag reduced to them, are now all theorems:
- separatedness of the blowup morphism is tag 01O2,
Stacks.RelativeProj.Situation.isSeparated_relativeProjToBase;- membership of the blowup in
Cis tag 02OS part (2),Stacks.Blowup.isEffectiveCartierDivisor_exceptionalIdeal;- the blowup is an isomorphism over the complement of the centre by tag 02OS part (1),
AlgebraicGeometry.isIso_blowUpToBase_restrict_compl_support;- scheme-theoretic density of the complement of an effective Cartier divisor is tag 07ZU,
Stacks.Divisors.isSchemeTheoreticallyDense_compl_of_isEffectiveCartierDivisor, transported along the open immersions of the gluing cover byAlgebraicGeometry.Scheme.Opens.isSchemeTheoreticallyDense_preimage_of_isOpenImmersion;- the existence of the classifying morphism, which the source deduces from the universal property of relative
Proj(Constructions, Section 01NS), isStacks.Blowup.exists_hom_blowUp_of_isEffectiveCartierDivisor.This supersedes
Stacks.Blowup.exists_nonempty_isTerminal_blowUp, which is the same statement with the last two of those as hypotheses.
theorem isTerminal_blowUp {X : Scheme.{u}} (I : X.IdealSheafData) :
∃ h : IsCartierOver I (Over.mk (AlgebraicGeometry.blowUpToBase I)),
Nonempty (IsTerminal
(⟨Over.mk (AlgebraicGeometry.blowUpToBase I), h⟩ : CartierOver I))
AlgebraicGeometry.existsUnique_lift_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowUpSquare/ChartBlowupUniversal.lean, line 87. The attribute's comment: “the terminality of the blowup read as a unique factorization: a morphism along which the inverse image of the centre is an effective Cartier divisor factors through the blowup in exactly one way”.
The universal property of blowing up, Stacks tag 0806, as a unique factorization. A morphism
f : Y ⟶ Xalong which the inverse image of the centre is an effective Cartier divisor factors through the blowup in exactly one way. This is the terminality statementStacks.Blowup.isTerminal_blowUpread as a∃!.
theorem existsUnique_lift_blowUpToBase {X : Scheme.{u}} (I : X.IdealSheafData) {Y : Scheme.{u}}
(f : Y ⟶ X) (hf : Stacks.Divisors.IsEffectiveCartierDivisor (I.comap f)) :
∃! k : Y ⟶ blowUp I, k ≫ blowUpToBase I = f
Tag 0BFL, a lemma
Tag 0BFL in the Stacks Project.
AlgebraicGeometry.mem_affineBlowupStandardOpen_iff_exceptionalIdeal_stalk_eq_span, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/ChartMembership.lean, line 360.
A point of a blowup lies in the standard affine chart at
aif and only if the image ofagenerates the exceptional ideal in its local ring.
public theorem mem_affineBlowupStandardOpen_iff_exceptionalIdeal_stalk_eq_span
{X : Scheme.{u}} (I : X.IdealSheafData) (U : X.affineOpens)
(a : I.ideal U) (x : (blowUp I))
(hx : (blowUpToBase I) x ∈ U.1) :
letI := (reesSituation I).sectionRingGradedRing U.1
letI := (reesSituation I).sectionRingGradingGradedRing U.1
x ∈ Set.range
((Proj.basicOpen ((reesSituation I).sectionRingGrading U.1)
(reesDegreeOne I U a).1).ι ≫
(Stacks.RelativeProj.Situation.relativeProjChart (reesSituation I) U)) ↔
AlgebraicGeometry.IdealSheafData.stalk (exceptionalIdeal I) x =
Ideal.span
{((blowUpToBase I).stalkMap x)
(X.presheaf.germ U.1 ((blowUpToBase I) x) hx
(a : X.presheaf.obj (.op U.1)))}
Tag 0807, a lemma
Tag 0807 in the Stacks Project.
Stacks.Blowup.isIso_blowUpToBase_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/CartierCentre.lean, line 56.
[Stacks, Tag 0807]. Blowing up a scheme in an effective Cartier divisor does not change it: the blowup morphism is an isomorphism.
The identity of
Xlies in the categoryCof [Stacks, Tag 0806] precisely becauseIis an effective Cartier divisor, and the blowup is a final object ofC(Stacks.Blowup.isTerminal_blowUp), so the classifying morphism of the identity is a two-sided inverse of the blowup morphism.
public theorem isIso_blowUpToBase_of_isEffectiveCartierDivisor {X : Scheme.{u}}
(I : X.IdealSheafData) (hI : Stacks.Divisors.IsEffectiveCartierDivisor I) :
IsIso (AlgebraicGeometry.blowUpToBase I)
Tag 0808, a lemma
Tag 0808 in the Stacks Project.
AlgebraicGeometry.isReduced_blowUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/Reduced.lean, line 53.
Stacks Project, Tag 0808. The blowup of a reduced scheme in a quasi-coherent ideal is reduced.
theorem isReduced_blowUp [IsReduced X] : IsReduced (blowUp I)
Tag 02ND, a lemma
Tag 02ND in the Stacks Project.
AlgebraicGeometry.isIntegral_blowUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/Integral.lean, line 134. References: EGA II (8.1.4), “(i) integrality, blowup”.
Stacks Project, Tag 02ND. The blowup of an integral scheme in a nonzero quasi-coherent ideal is integral.
theorem isIntegral_blowUp (hI : I ≠ ⊥) : IsIntegral (blowUp I)
Tag 0BFM, a lemma
Tag 0BFM in the Stacks Project.
AlgebraicGeometry.bijOn_genericPoints_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/GenericPoints.lean, line 82.
The blowup morphism restricts to a bijection from the generic points of the irreducible components of the blowup onto the generic points of those irreducible components of the base that are not contained in the centre.
theorem bijOn_genericPoints_blowUpToBase {X : Scheme.{u}} (I : X.IdealSheafData) :
Set.BijOn (blowUpToBase I) (genericPoints (blowUp I)) (genericPoints X \ I.supportSet)
Tag 0809, a lemma
Tag 0809 in the Stacks Project.
AlgebraicGeometry.isPullbackDefined_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/RegularPullback.lean, line 293. The attribute's comment: “effective Cartier divisors”. References: SGA 7 X (2.6), “partial”.
Stacks Project, Tag 0809. Every effective Cartier divisor on a scheme has a defined pullback along the blowup of the scheme in any quasi-coherent ideal.
theorem isPullbackDefined_blowUpToBase (D : X.IdealSheafData)
(hD : Stacks.Divisors.IsEffectiveCartierDivisor D) :
Stacks.Divisors.IsPullbackDefined (blowUpToBase I) D
AlgebraicGeometry.pullbacksMeromorphicSections_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/RegularPullback.lean, line 334. The attribute's comment: “meromorphic functions”.
Stacks Project, Tag 0809. Pullbacks of meromorphic functions are defined along the blowup of a scheme in any quasi-coherent ideal.
theorem pullbacksMeromorphicSections_blowUpToBase :
PullbacksMeromorphicSections (blowUpToBase I).toLRSHom
Tag 080A, a lemma
Tag 080A in the Stacks Project.
AlgebraicGeometry.blowUpMulIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/Product.lean, line 139. The attribute's comment: “canonical isomorphism”.
Stacks Project, Tag 080A. Blowing up
XinIand then in the inverse image ofJis canonically, overX, the blowup ofXinI * J.
def blowUpMulIso :
Over.mk (blowUpToBase (J.comap (blowUpToBase I)) ≫ blowUpToBase I) ≅
Over.mk (blowUpToBase (I * J))
AlgebraicGeometry.blowUpMulIso_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/Product.lean, line 149. The attribute's comment: “uniqueness”.
The isomorphism of Stacks tag 080A is the unique isomorphism of these two blowups over
X: both are terminal in the same category.
theorem blowUpMulIso_unique
(e : Over.mk (blowUpToBase (J.comap (blowUpToBase I)) ≫ blowUpToBase I) ≅
Over.mk (blowUpToBase (I * J))) : e = blowUpMulIso I J
Tag 02NS, a lemma
Tag 02NS in the Stacks Project.
AlgebraicGeometry.exists_isInvertibleModule_isRelativelyAmple_blowUpTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/BlowupTwist.lean, line 88. The attribute's comment: “part (2): 𝒪_{X'}(1) is a b-relatively ample invertible sheaf”. References: EGA II (4.6.18), “special case”; EGA III (2.3.4), “(i), special case”.
Stacks Project, Tag 02NS, part (2). Let
ℐ ⊆ 𝒪_Xbe a quasi-coherent sheaf of ideals of finite type andb : X' ⟶ Xthe blowup ofXinℐ. Then𝒪_{X'}(1)is ab-relatively ample invertible sheaf: it is invertible, and with that invertibility it is ample relative tobin the sense of Tag 01VH.Invertibility is stated, not presupposed: it is the witness of the existential, and the relative ampleness that follows is read with it. The twist
𝒪_{X'}(1)isAlgebraicGeometry.blowUpTwist, the twisting sheaf of the relativeProjof the Rees algebra glued along the transition datumStacks.RelativeProj.Situation.twistTransition.
public theorem exists_isInvertibleModule_isRelativelyAmple_blowUpTwist (hI : I.IsFiniteType) :
∃ _ : Stacks.Ample.IsInvertibleModule (blowUp I) (blowUpTwist I 1),
Stacks.RelativeAmple.IsRelativelyAmple (blowUpToBase I) (blowUpTwist I 1)
AlgebraicGeometry.isProjective_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/Projective.lean, line 76. The attribute's comment: “part (1): b : X' ⟶ X is a projective morphism”. References: EGA IV (19.4.1).
The blowup of a scheme in a quasi-coherent sheaf of ideals of finite type is a projective morphism.
public theorem isProjective_blowUpToBase (hI : I.IsFiniteType) :
IsProjective (blowUpToBase I)
AlgebraicGeometry.isRelativelyAmple_twist_reesSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ReesAlgebra/TwistAmple.lean, line 152. The attribute's comment: “part (2): 𝒪_{X'}(1) is a b-relatively ample invertible sheaf, for the twist glued from the chart twists along a transition datum for Tag 01NO (3) and (4), which is carried as the hypothesis Stacks.RelativeProj.Situation.TwistTransition”.
Stacks Project, Tag 02NS, part (2). The twisting sheaf
𝒪_{X'}(1)of the blowup of a scheme in a quasi-coherent sheaf of ideals of finite type is a relatively ample invertible sheaf for the blowup morphism: over an affine openVof the base the blowup is theProjof the Rees algebra ofℐ(V), the twist restricts there to the absolute𝒪(1), and that is ample.
public theorem isRelativelyAmple_twist_reesSituation (hI : I.IsFiniteType)
(t : (reesSituation I).TwistTransition 1) :
Stacks.RelativeAmple.IsRelativelyAmple (blowUpToBase I) (Situation.twist t)
Tag 080B, a lemma
Tag 080B in the Stacks Project.
AlgebraicGeometry.finitePresentation_mul_subschemeι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/CompositeCentre.lean, line 137. The attribute's comment: “the centre Y is of finite presentation. Y is the explicit product I * J of the first centre with the second-centre ideal that Stacks Lemma 31.32.5, Tag 0803, supplies, and a product of a finitely presented centre with a centre of finite type is finitely presented”.
The product of a finitely presented centre with a centre of finite type is again a finitely presented centre: by [Stacks, Tag 01TV] both statements say that the ideal is finitely generated over every affine open, and the ideal of
I * Jthere is the product of the two ideals.This is the finite-presentation clause of [Stacks, Tag 080B].
theorem finitePresentation_mul_subschemeι (I J : X.IdealSheafData)
(hI : FinitePresentation I.subschemeι) (hJ : ∀ U : X.affineOpens, (J.ideal U).FG) :
FinitePresentation (I * J).subschemeι
AlgebraicGeometry.exists_centre_supportSet_eq_and_nonempty_blowUpCompositionIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/CompositeCentreExistence.lean, line 74.
Stacks Project, Tag 080B. Let
Xbe a quasi-compact and quasi-separated scheme, letIbe a finitely presented centre onXwith blowupb : X' ⟶ X, and letZ'be a finitely presented centre onX'. Then there is a finitely presented centreYonXwhose support isSupp I ∪ b(Supp Z')and for which the two-step blowupBl_{Z'}(X') ⟶ X' ⟶ Xis the blowup ofXinY, overX.The centre is the product
I · JofIwith the second-centre ideal thatStacks.Blowup.exists_secondCentreproduces fromZ'.
theorem exists_centre_supportSet_eq_and_nonempty_blowUpCompositionIso
[CompactSpace X] [QuasiSeparatedSpace X] (I : X.IdealSheafData)
(hI : FinitePresentation I.subschemeι) (Z' : (blowUp I).IdealSheafData)
(hfp : FinitePresentation Z'.subschemeι) :
∃ Y : X.IdealSheafData, FinitePresentation Y.subschemeι ∧
Y.supportSet = I.supportSet ∪ (blowUpToBase I).base '' Z'.supportSet ∧
Nonempty (Over.mk (blowUpToBase Z' ≫ blowUpToBase I) ≅ Over.mk (blowUpToBase Y))
AlgebraicGeometry.exists_centre_supportSet_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/CompositeCentreExistence.lean, line 90. The attribute's comment: “part (1), the support of the centre”.
The support of the centre of [Stacks, Tag 080B]. There is a finitely presented centre
YonXwithSupp Y = Supp I ∪ b(Supp Z').
theorem exists_centre_supportSet_eq [CompactSpace X] [QuasiSeparatedSpace X]
(I : X.IdealSheafData) (hI : FinitePresentation I.subschemeι)
(Z' : (blowUp I).IdealSheafData) (hfp : FinitePresentation Z'.subschemeι) :
∃ Y : X.IdealSheafData, FinitePresentation Y.subschemeι ∧
Y.supportSet = I.supportSet ∪ (blowUpToBase I).base '' Z'.supportSet
AlgebraicGeometry.exists_centre_nonempty_blowUpCompositionIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/CompositeCentreExistence.lean, line 103. The attribute's comment: “part (2), the composite of the two blowups is the blowup in the centre”.
The composite of two blowups is a blowup, [Stacks, Tag 080B]. There is a finitely presented centre
YonXfor which blowingXup inYis the two-step blowupBl_{Z'}(X') ⟶ X' ⟶ X, overX.
theorem exists_centre_nonempty_blowUpCompositionIso [CompactSpace X] [QuasiSeparatedSpace X]
(I : X.IdealSheafData) (hI : FinitePresentation I.subschemeι)
(Z' : (blowUp I).IdealSheafData) (hfp : FinitePresentation Z'.subschemeι) :
∃ Y : X.IdealSheafData, FinitePresentation Y.subschemeι ∧
Nonempty (Over.mk (blowUpToBase Z' ≫ blowUpToBase I) ≅ Over.mk (blowUpToBase Y))
Sources
Section31.34 Strict transform#
Section 31.34 of the Stacks Project, Tag 080C. 7 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 080D, a definition
Tag 080D in the Stacks Project.
Stacks.Blowup.strictTransformSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/StrictTransform.lean, line 164. The attribute's comment: “strict transform of a module”.
The strict transform of an
𝒪_X-moduleℱalong the blowup of the base inℐ: the quotient of the pullback ofℱtoX ×_S S'by the submodule of sections supported on the inverse image of the exceptional divisor.
abbrev strictTransformSheaf (ℱ : X.Modules) : (blowUpPullback f ℐ).Modules
Stacks.Blowup.strictTransformIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/StrictTransform.lean, line 172. The attribute's comment: “ideal of the strict transform of a scheme”.
The quasi-coherent ideal of sections of
𝒪_{X ×_S S'}supported on the inverse image of the exceptional divisor, assembled from its modules of sections over the affine opens ofX ×_S S'.
def strictTransformIdeal : (blowUpPullback f ℐ).IdealSheafData
Stacks.Blowup.strictTransform, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/StrictTransform.lean, line 210. The attribute's comment: “strict transform of a scheme”.
The strict transform of
Xalong the blowup of the base inℐ: the closed subscheme ofX ×_S S'cut out by the ideal of sections supported on the inverse image of the exceptional divisor.
abbrev strictTransform : Scheme.{u}
Stacks.Blowup.ideal_strictTransformIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/StrictTransformRetrocompact.lean, line 130. The attribute's comment: “the defining ideal of the strict transform of a scheme, with no hypothesis”.
Stacks Project, Tag 080D, part (2). On an affine open, the defining ideal of the strict transform of
Xconsists of exactly the sections of𝒪_{X ×_S S'}supported onpr_{S'}⁻¹ E. This isStacks.Blowup.ideal_strictTransformIdeal_of_quasiCompactwith its retrocompactness hypothesis discharged, so it is the equality that tag 080D's definition asserts.
theorem ideal_strictTransformIdeal (U : (blowUpPullback f ℐ).affineOpens) :
(strictTransformIdeal f ℐ).ideal U =
(SheafOfModules.supportedSectionsSubmodule (exceptionalPullbackSet f ℐ)
(SheafOfModules.unit (blowUpPullback f ℐ).ringCatSheaf)).toSubmodule.obj
(Opposite.op U.1)
Stacks.Blowup.isQuasicoherent_strictTransformSheaf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/StrictTransformRetrocompact.lean, line 142. The attribute's comment: “the strict transform of a quasi-coherent module is quasi-coherent”.
Stacks Project, Tag 080D, part (1). The strict transform of a quasi-coherent module is quasi-coherent on
X ×_S S', with no hypothesis. Recorded as an instance because the strict transform of a strict transform is formed by instance search on the quasi-coherence of the first.
instance isQuasicoherent_strictTransformSheaf (ℱ : X.Modules) [ℱ.IsQuasicoherent] :
(strictTransformSheaf f ℐ ℱ).IsQuasicoherent
Stacks.StrictTransform.sheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/StrictTransform/Basic.lean, line 256. The attribute's comment: “strict transform of a module”.
Stacks Project, Tag 080D (1). The strict transform of a sheaf of
𝒪_X-modulesF: the quotient ofpr_X^* Fby the submodule of sections supported onpr_{S'}^{-1}(Supp E).
public abbrev sheaf (F : X.Modules) : (baseChange f b).Modules
Stacks.StrictTransform.ideal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/StrictTransform/Basic.lean, line 297. The attribute's comment: “ideal of the strict transform of a scheme”.
The quasi-coherent ideal of sections of
𝒪_{X ×_S S'}supported onpr_{S'}^{-1}(Supp E), assembled from its values on affine opens.
public def ideal : (baseChange f b).IdealSheafData
Stacks.StrictTransform.scheme, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/StrictTransform/Basic.lean, line 305. The attribute's comment: “strict transform of a scheme”. References: SGA 7 X (2.4), “more general”.
Stacks Project, Tag 080D (2). The strict transform of
X: the closed subscheme ofX ×_S S'cut out by the ideal of sections supported onpr_{S'}^{-1}(Supp E).
public abbrev scheme : Scheme.{u}
Tag 080E, a lemma
Tag 080E in the Stacks Project.
AlgebraicGeometry.strictTransformBlowUpIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/InverseImageCentre.lean, line 255. The attribute's comment: “scheme”. References: SGA 5 VII (9.5), “First clause only”.
The strict transform of
Xunder the blowup ofSinℐis the blowup ofXin the inverse image ofℐ, canonically asX-schemes.
def strictTransformBlowUpIso :
Over.mk ((Stacks.StrictTransform.ideal f (blowUpToBase ℐ) (exceptionalIdeal ℐ)).subschemeι ≫
pullback.fst f (blowUpToBase ℐ)) ≅ Over.mk (blowUpToBase (ℐ.comap f))
AlgebraicGeometry.strictTransformSheafBlowUpIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/InverseImageCentre.lean, line 530. The attribute's comment: “sheaf”.
For a sheaf of
𝒪_X-modulesF, the strict transform ofFunder the blowup ofSinℐis canonically the direct image, along the closed immersionX' ⟶ X ×_S S'of part (1), of the strict transform ofFrelative to the blowup ofXin the inverse imageℐ·𝒪_X. The sheafFis not assumed quasi-coherent.
def strictTransformSheafBlowUpIso (F : X.Modules) :
sheaf f (blowUpToBase ℐ) (exceptionalIdeal ℐ) F ≅
(Scheme.Modules.pushforward (strictTransformBlowUpι f ℐ)).obj
(sheaf (𝟙 X) (blowUpToBase (ℐ.comap f)) (exceptionalIdeal (ℐ.comap f)) F)
Tag 080F, a lemma
Tag 080F in the Stacks Project.
AlgebraicGeometry.strictTransformIdeal_eq_bot_of_flat_at_exceptional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/Flat.lean, line 220. The attribute's comment: “part (1)”.
Stacks Project, Tag 080F (1). If
Xis flat overSat every point lying over the centre of the blowup, then the strict transform ofXis the whole base changeX ×_S S': the ideal cutting it out is zero.
public theorem strictTransformIdeal_eq_bot_of_flat_at_exceptional
{X S : Scheme.{u}} (f : X ⟶ S) (I : S.IdealSheafData)
(hflat : ∀ x : X, f x ∈ I.support → IsFlatAt f.toLRSHom.toShHom x) :
Stacks.StrictTransform.ideal f (blowUpToBase I) (exceptionalIdeal I) = ⊥
AlgebraicGeometry.isIso_strictTransformSheaf_quotient_of_flat_at_exceptional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/Flat.lean, line 242. The attribute's comment: “part (2)”.
Stacks Project, Tag 080F (2). If a quasi-coherent
𝒪_X-moduleFis flat overSat every point lying over the centre of the blowup, then the canonical quotient map frompr_X^* Fonto the strict transform ofFis an isomorphism.
public theorem isIso_strictTransformSheaf_quotient_of_flat_at_exceptional
{X S : Scheme.{u}} (f : X ⟶ S) (I : S.IdealSheafData) (F : X.Modules) [F.IsQuasicoherent]
(hflat : ∀ x : X, f x ∈ I.support → IsFlatOverAt f.toLRSHom.toShHom F x) :
IsIso (Stacks.StrictTransform.π f (blowUpToBase I) (exceptionalIdeal I) F)
Tag 080G, a lemma
Tag 080G in the Stacks Project.
AlgebraicGeometry.strictTransformSheafPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/AffinePushforward.lean, line 379.
Stacks Project, Tag 080G. Let
b : S' ⟶ Sbe the blowup ofSin a closed subscheme cut out by the quasi-coherent ideal sheafI, letg : X ⟶ Ybe an affine morphism of schemes overS, letFbe a quasi-coherent𝒪_X-module and letg' : X ×_S S' ⟶ Y ×_S S'be the base change ofg. Theng'_*of the strict transform ofFrelative tobis the strict transform ofg_* F.
def strictTransformSheafPushforwardIso {X Y S : Scheme.{u}}
(g : X ⟶ Y) (f : Y ⟶ S) (I : S.IdealSheafData)
(F : X.Modules) [IsAffineHom g] [F.IsQuasicoherent] :
let g' : Stacks.StrictTransform.baseChange (g ≫ f) (blowUpToBase I) ⟶
Stacks.StrictTransform.baseChange f (blowUpToBase I) :=
pullback.lift
(pullback.fst (g ≫ f) (blowUpToBase I) ≫ g)
(pullback.snd (g ≫ f) (blowUpToBase I))
(by rw [Category.assoc]; exact pullback.condition)
(Scheme.Modules.pushforward g').obj
(Stacks.StrictTransform.sheaf (g ≫ f) (blowUpToBase I) (exceptionalIdeal I) F) ≅
Stacks.StrictTransform.sheaf f (blowUpToBase I) (exceptionalIdeal I)
((Scheme.Modules.pushforward g).obj F)
Tag 080H, a lemma
Tag 080H in the Stacks Project.
AlgebraicGeometry.blowUpProductIso_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/CartierProduct.lean, line 205. The attribute's comment: “part (1): isomorphism of blowups”.
Stacks Project, Tag 080H, part (1). Let
Dbe an effective Cartier divisor onSand letIbe any quasi-coherent ideal sheaf. The blowup ofSinI * Dis the blowup ofSinI, asS-schemes.
theorem blowUpProductIso_exists {S : Scheme.{u}} (I D : S.IdealSheafData)
(hD : Stacks.Divisors.IsEffectiveCartierDivisor D) :
Nonempty (Over.mk (blowUpToBase I) ≅ Over.mk (blowUpToBase (I * D)))
Stacks.StrictTransform.exists_baseChange_iso_sheaf_iso_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/StrictTransform/DifferentCentres.lean, line 391. The attribute's comment: “part (2): strict transforms of modules”.
[Stacks, Tag 080H] part (2). Let
Dbe an effective Cartier divisor onSand letFbe a sheaf of𝒪_X-modules with no nonzero local sections supported inf^{-1}D. Given an isomorphismeof the blowup ofSinIwith the blowup ofSinI * DoverS— part (1) of the tag — the induced isomorphism of the two base changes, specified by both its projections, carries the strict transform ofFfor the centreI * Dto the strict transform for the centreI.Part (1) of the tag, which supplies
e, is not in the repository; see the implementation notes of this file. Everything else here is unconditional, [Stacks, Tag 02OS] part (1) being the instanceAlgebraicGeometry.isIso_blowUpToBase_restrict_compl_support.The hypothesis
_hDthatDis an effective Cartier divisor is the tag's, and is retained so that the statement is the tag's; it is used only throughe, which part (1) deduces from it, so the conclusion in fact holds for anyDadmitting such ane.
public theorem exists_baseChange_iso_sheaf_iso_mul (f : X ⟶ S) (I D : S.IdealSheafData)
(_hD : Stacks.Divisors.IsEffectiveCartierDivisor D) (F : X.Modules)
(hF : ∀ (U : X.Opens) (s : Γ(F, U)),
s ∈ (supportedSectionsSubmodule (f.base ⁻¹' D.supportSet) F).toSubmodule.obj (op U) →
s = 0)
(e : Over.mk (AlgebraicGeometry.blowUpToBase I) ≅
Over.mk (AlgebraicGeometry.blowUpToBase (I * D))) :
∃ g : baseChange f (AlgebraicGeometry.blowUpToBase I) ≅
baseChange f (AlgebraicGeometry.blowUpToBase (I * D)),
(g.hom ≫ pullback.fst f (AlgebraicGeometry.blowUpToBase (I * D)) =
pullback.fst f (AlgebraicGeometry.blowUpToBase I)) ∧
(g.hom ≫ pullback.snd f (AlgebraicGeometry.blowUpToBase (I * D)) =
pullback.snd f (AlgebraicGeometry.blowUpToBase I) ≫ e.hom.left) ∧
Nonempty ((Scheme.Modules.pullback g.hom).obj
(sheaf f (AlgebraicGeometry.blowUpToBase (I * D))
(AlgebraicGeometry.exceptionalIdeal (I * D)) F) ≅
sheaf f (AlgebraicGeometry.blowUpToBase I)
(AlgebraicGeometry.exceptionalIdeal I) F)
Tag 080I, a lemma
Tag 080I in the Stacks Project.
Stacks.StrictTransform.strictTransformSheaf_comp_blowUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/StrictTransform/CompositionBlowUp.lean, line 191. The attribute's comment: “part (1): strict transform of a module”.
[Stacks, Tag 080I] part (1). For
bthe blowup ofSinI,cthe blowup of the blowup inJ, anddthe blowup ofSin a third centreKwhose support isSupp I ∪ b(Supp J), the iterated strict transform ofFagrees with the strict transform in the composite centre, compatibly with both projections and with the quotient maps.This is
Stacks.StrictTransform.exists_baseChange_iso_sheaf_iso_comp_blowUpwith its one hypothesishQJdischarged byStacks.StrictTransform.supportedSections_sheaf_blowUp_union_eq_zero, applied on the first base change over the first blowup with centreJand divisorAlgebraicGeometry.exceptionalIdeal I, whose own hypothesis is the defining propertyStacks.StrictTransform.supportedSections_sheaf_eq_zeroof the first strict transform. Unconditional.
public theorem strictTransformSheaf_comp_blowUp (f : X ⟶ S) (I K : S.IdealSheafData)
(J : (AlgebraicGeometry.blowUp I).IdealSheafData)
(hK : K.supportSet = I.supportSet ∪
(AlgebraicGeometry.blowUpToBase I).base '' J.supportSet)
(e : Over.mk (AlgebraicGeometry.blowUpToBase J ≫ AlgebraicGeometry.blowUpToBase I) ≅
Over.mk (AlgebraicGeometry.blowUpToBase K))
(F : X.Modules) :
let b := AlgebraicGeometry.blowUpToBase I
let f₁ : baseChange f b ⟶ AlgebraicGeometry.blowUp I := pullback.snd f b
let c := AlgebraicGeometry.blowUpToBase J
let d := AlgebraicGeometry.blowUpToBase K
let pK := pullback.fst f d
let pI := pullback.fst f b
let pJ := pullback.fst f₁ c
let FK := (Scheme.Modules.pullback pK).obj F
let FI := (Scheme.Modules.pullback pI).obj F
let QK := sheaf f d (AlgebraicGeometry.exceptionalIdeal K) F
let QI := sheaf f b (AlgebraicGeometry.exceptionalIdeal I) F
let QJ := sheaf f₁ c (AlgebraicGeometry.exceptionalIdeal J) QI
∃ (g : baseChange f₁ c ≅ baseChange f d) (hg : g.hom ≫ pK = pJ ≫ pI),
(g.hom ≫ pullback.snd f d = pullback.snd f₁ c ≫ e.hom.left) ∧
∃ s : (Scheme.Modules.pullback g.hom).obj QK ≅ QJ,
let t : (Scheme.Modules.pullback g.hom).obj FK ≅ (Scheme.Modules.pullback pJ).obj FI :=
((Scheme.Modules.pullbackComp g.hom pK).app F) ≪≫
((Scheme.Modules.pullbackCongr hg).app F) ≪≫
((Scheme.Modules.pullbackComp pJ pI).symm.app F)
let qK : FK ⟶ QK := π f d (AlgebraicGeometry.exceptionalIdeal K) F
let qI : FI ⟶ QI := π f b (AlgebraicGeometry.exceptionalIdeal I) F
let qJ : (Scheme.Modules.pullback pJ).obj QI ⟶ QJ :=
π f₁ c (AlgebraicGeometry.exceptionalIdeal J) QI
(Scheme.Modules.pullback g.hom).map qK ≫ s.hom =
t.hom ≫ (Scheme.Modules.pullback pJ).map qI ≫ qJ
Stacks.StrictTransform.strictTransform_comp_blowUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/StrictTransform/CompositionScheme.lean, line 322. The attribute's comment: “part (2): strict transform of a scheme”.
[Stacks, Tag 080I] part (2). For
bthe blowup ofSinI,cthe blowup of the blowup inJ, anddthe blowup ofSin a third centreKwhose support isSupp I ∪ b(Supp J), the strict transform alongcof the strict transform ofXalongbagrees with the strict transform ofXalongd, compatibly with both projections.Unconditional: the support identity is
Stacks.StrictTransform.iso_preimage_exceptionalPreimage_blowUpand the open immersion away from the second exceptional divisor isStacks.StrictTransform.isOpenImmersion_exceptionalComplement_ι_comp_fst, both of which are theorems now that [Stacks, Tag 02OS] part (1) is the instanceAlgebraicGeometry.isIso_blowUpToBase_restrict_compl_support.
public theorem strictTransform_comp_blowUp (f : X ⟶ S) (I K : S.IdealSheafData)
(J : (AlgebraicGeometry.blowUp I).IdealSheafData)
(hK : K.supportSet = I.supportSet ∪
(AlgebraicGeometry.blowUpToBase I).base '' J.supportSet)
(e : Over.mk (AlgebraicGeometry.blowUpToBase J ≫ AlgebraicGeometry.blowUpToBase I) ≅
Over.mk (AlgebraicGeometry.blowUpToBase K)) :
let X₁ := scheme f (AlgebraicGeometry.blowUpToBase I) (AlgebraicGeometry.exceptionalIdeal I)
let f₁ : X₁ ⟶ AlgebraicGeometry.blowUp I :=
(ideal f (AlgebraicGeometry.blowUpToBase I)
(AlgebraicGeometry.exceptionalIdeal I)).subschemeι ≫
pullback.snd f (AlgebraicGeometry.blowUpToBase I)
∃ g : scheme f₁ (AlgebraicGeometry.blowUpToBase J) (AlgebraicGeometry.exceptionalIdeal J) ≅
scheme f (AlgebraicGeometry.blowUpToBase K) (AlgebraicGeometry.exceptionalIdeal K),
(g.hom ≫ (ideal f (AlgebraicGeometry.blowUpToBase K)
(AlgebraicGeometry.exceptionalIdeal K)).subschemeι ≫
pullback.fst f (AlgebraicGeometry.blowUpToBase K) =
(ideal f₁ (AlgebraicGeometry.blowUpToBase J)
(AlgebraicGeometry.exceptionalIdeal J)).subschemeι ≫
pullback.fst f₁ (AlgebraicGeometry.blowUpToBase J) ≫
(ideal f (AlgebraicGeometry.blowUpToBase I)
(AlgebraicGeometry.exceptionalIdeal I)).subschemeι ≫
pullback.fst f (AlgebraicGeometry.blowUpToBase I)) ∧
(g.hom ≫ (ideal f (AlgebraicGeometry.blowUpToBase K)
(AlgebraicGeometry.exceptionalIdeal K)).subschemeι ≫
pullback.snd f (AlgebraicGeometry.blowUpToBase K) =
(ideal f₁ (AlgebraicGeometry.blowUpToBase J)
(AlgebraicGeometry.exceptionalIdeal J)).subschemeι ≫
pullback.snd f₁ (AlgebraicGeometry.blowUpToBase J) ≫ e.hom.left)
Tag 080W, a lemma
Tag 080W in the Stacks Project.
AlgebraicGeometry.strictTransformSheaf_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/ShortExact.lean, line 590.
Stacks Project, Tag 080W. A short exact sequence of quasi-coherent
𝒪_X-modules which remains short exact after every base change of the base schemeShas short exact strict transforms along the blowup ofSin any quasi-coherent ideal, with the three maps determined by the quotient maps onto the strict transforms.
public theorem strictTransformSheaf_shortExact {X S : Scheme.{u}} (f : X ⟶ S)
(I : S.IdealSheafData) (C : ShortComplex X.Modules)
[C.X₁.IsQuasicoherent] [C.X₂.IsQuasicoherent] [C.X₃.IsQuasicoherent]
(hC : ∀ {T : Scheme.{u}} (g : T ⟶ S),
(C.map (Scheme.Modules.pullback (pullback.fst f g))).ShortExact) :
let b := blowUpToBase I
let E := exceptionalIdeal I
let p := pullback.fst f b
let F₁ := (Scheme.Modules.pullback p).obj C.X₁
let F₂ := (Scheme.Modules.pullback p).obj C.X₂
let F₃ := (Scheme.Modules.pullback p).obj C.X₃
let q₁ : F₁ ⟶ Stacks.StrictTransform.sheaf f b E C.X₁ := Stacks.StrictTransform.π f b E C.X₁
let q₂ : F₂ ⟶ Stacks.StrictTransform.sheaf f b E C.X₂ := Stacks.StrictTransform.π f b E C.X₂
let q₃ : F₃ ⟶ Stacks.StrictTransform.sheaf f b E C.X₃ := Stacks.StrictTransform.π f b E C.X₃
∃ (f' : Stacks.StrictTransform.sheaf f b E C.X₁ ⟶ Stacks.StrictTransform.sheaf f b E C.X₂)
(g' : Stacks.StrictTransform.sheaf f b E C.X₂ ⟶ Stacks.StrictTransform.sheaf f b E C.X₃)
(w : f' ≫ g' = 0),
(ShortComplex.mk f' g' w).ShortExact ∧
(q₁ ≫ f' = (Scheme.Modules.pullback p).map C.f ≫ q₂) ∧
(q₂ ≫ g' = (Scheme.Modules.pullback p).map C.g ≫ q₃)
Sources
Section31.35 Admissible blowups#
Section 31.35 of the Stacks Project, Tag 080J. 6 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 080K, a definition
Tag 080K in the Stacks Project.
Stacks.Blowup.IsAdmissibleBlowup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Admissible.lean, line 80.
A morphism
f : X' ⟶ Xis aU-admissible blowup if there is a quasi-coherent sheaf of idealsIonXwhose closed subscheme is of finite presentation overXand supported away fromU, together with an isomorphism ofX'with the blowup ofXinIcarrying the blowup morphism tof.
abbrev IsAdmissibleBlowup (U : X.Opens) (f : X' ⟶ X) : Prop
Tag 080L, a lemma
Tag 080L in the Stacks Project.
Stacks.Blowup.IsAdmissibleBlowup.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/AdmissibleComposition.lean, line 262.
Stacks Project, Tag 080L. Let
Xbe a quasi-compact and quasi-separated scheme andU ⊆ Xan open subscheme. Ifb : X' ⟶ Xis aU-admissible blowup andb' : X'' ⟶ X'is ab⁻¹(U)-admissible blowup, then the compositeb' ≫ b : X'' ⟶ Xis aU-admissible blowup.The single centre is the product of the first centre with the second-centre ideal of
Stacks.Blowup.exists_secondCentre, and the two halves of [Stacks, Tag 080B] do the rest. The support clause that…comp_of_secondCentreIdealasks for comes fromAlgebraicGeometry.supportSet_mul_eq_union_imagetogether withAlgebraicGeometry.Scheme.IdealSheafData.support_mul: the support of the product centre is the support of the first centre together with the image of the support of the second, and it contains the support ofJ.
theorem IsAdmissibleBlowup.comp [CompactSpace X] [QuasiSeparatedSpace X]
(U : X.Opens) (b : X' ⟶ X) (b' : X'' ⟶ X')
(hb : IsAdmissibleBlowup U b) (hb' : IsAdmissibleBlowup (b ⁻¹ᵁ U) b') :
IsAdmissibleBlowup U (b' ≫ b)
Tag 080M, a lemma
Tag 080M in the Stacks Project.
Stacks.Blowup.exists_admissibleBlowup_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/AdmissibleExtension.lean, line 402.
Stacks Project, Tag 080M. A blowup admissible over the intersection of two quasi-compact opens extends to a blowup of the ambient scheme admissible over the first open, with its restriction to the second open given by a cartesian square.
public theorem exists_admissibleBlowup_isPullback
{X V' : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
(U V : X.Opens) (hU : IsCompact (U : Set X))
(hV : IsCompact (V : Set X)) (b : V' ⟶ V.toScheme)
(hb : IsAdmissibleBlowup (V.ι ⁻¹ᵁ U) b) :
∃ (X' : Scheme.{u}) (f : X' ⟶ X),
IsAdmissibleBlowup U f ∧ ∃ g : V' ⟶ X', IsPullback b g V.ι f
Tag 080N, a lemma
Tag 080N in the Stacks Project.
Stacks.Blowup.exists_admissibleBlowup_dominating, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/AdmissibleDominating.lean, line 437.
Stacks Project, Tag 080N. Let
Ube an open subscheme of a schemeXand letb_i : Y_i ⟶ X,i ∈ ι, be a finite family ofU-admissible blowups. There is aU-admissible blowupb : X' ⟶ Xwhich factors through everyb_i, with each factor mapX' ⟶ Y_iitself ab_i⁻¹(U)-admissible blowup.Take
X'to be the blowup ofXin the productI = ∏ I_iof the centres. The product is again of finite type and supported away fromU, sobisU-admissible. WritingI = I_i · J_i, blowing up a product is blowing up the factors in succession (Stacks tag 080A), soX'is the blowup ofY_iin the inverse image ofJ_i; flat base change along the isomorphismY_i ≅ Bl_{I_i}(X)(Stacks tag 0805) identifies that inverse image taken onY_iwith the one taken onBl_{I_i}(X). The inverse image ofJ_ionY_iis again of finite type and supported away fromb_i⁻¹(U), so the factor map isb_i⁻¹(U)-admissible.
theorem exists_admissibleBlowup_dominating {X : Scheme.{u}} (U : X.Opens)
{ι : Type*} [Finite ι] (Y : ι → Scheme.{u})
(f : ∀ i, Y i ⟶ X)
(hf : ∀ i, IsAdmissibleBlowup U (f i)) :
∃ (X' : Scheme.{u}) (b : X' ⟶ X),
IsAdmissibleBlowup U b ∧
∃ g : ∀ i, X' ⟶ Y i,
(∀ i, g i ≫ f i = b) ∧
(∀ i, IsAdmissibleBlowup (f i ⁻¹ᵁ U) (g i))
Tag 080P, a lemma
Tag 080P in the Stacks Project.
Stacks.Blowup.exists_admissibleBlowup_disjoint_open_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/AdmissibleSeparation.lean, line 375.
Stacks Project, Tag 080P. Let
Xbe a quasi-compact and quasi-separated scheme and letU, Vbe disjoint quasi-compact open subschemes ofX. Then there is aU ∪ V-admissible blowupb : X' ⟶ Xsuch thatX'is the disjoint union of two open subschemesX' = X'₁ ⨿ X'₂withb⁻¹(U) ⊆ X'₁andb⁻¹(V) ⊆ X'₂.
theorem exists_admissibleBlowup_disjoint_open_cover
(X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
(U V : X.Opens) (hU : IsCompact (U : Set X))
(hV : IsCompact (V : Set X)) (hUV : Disjoint U V) :
∃ (X' : Scheme.{u}) (b : X' ⟶ X) (U₁ U₂ : X'.Opens),
IsAdmissibleBlowup (U ⊔ V) b ∧
Disjoint U₁ U₂ ∧ U₁ ⊔ U₂ = ⊤ ∧
b ⁻¹ᵁ U ≤ U₁ ∧ b ⁻¹ᵁ V ≤ U₂
Stacks.Blowup.exists_admissibleBlowup_pairwise_disjoint_open_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/AdmissibleSeparation.lean, line 476. The attribute's comment: “stated for a finite family of pairwise disjoint quasi-compact opens; the source's two-piece statement is the case of a two-element index type”.
Stacks Project, Tag 080P for a finite family. Let
Xbe a quasi-compact and quasi-separated scheme and letU_i,i ∈ ι, be a finite family of pairwise disjoint quasi-compact open subschemes ofX. Then there is a⋃ U_i-admissible blowupb : X' ⟶ Xsuch thatX'is the disjoint union of open subschemesX'_i,i ∈ ι, withb⁻¹(U_i) ⊆ X'_i.This is the form in which the source iterates Tag 080P: the decomposition of
Uinto the finitely many loci where a locally constant invariant takes a fixed value is separated by a single blowup. The proof is that of the two-piece case verbatim. Choose quasi-coherent sheaves of idealsℐ_iof finite type withX ∖ U_i = V(ℐ_i)and blow up∑ ℐ_i; the pieceX'_iis the union of the affine charts of Stacks tag 0804 attached to the sections ofℐ_i. Two such pieces are disjoint becauseℐ_iℐ_jis contained in the nilradical fori ≠ j, and they cover because over an affine open every section of(∑ ℐ_i)(W)is a sum of sections of theℐ_i(W).
theorem exists_admissibleBlowup_pairwise_disjoint_open_cover
(X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
{ι : Type*} [Finite ι] (U : ι → X.Opens) (hU : ∀ i, IsCompact (U i : Set X))
(hUd : Pairwise fun i j => Disjoint (U i) (U j)) :
∃ (X' : Scheme.{u}) (b : X' ⟶ X) (V : ι → X'.Opens),
IsAdmissibleBlowup (⨆ i, U i) b ∧
(Pairwise fun i j => Disjoint (V i) (V j)) ∧ ⨆ i, V i = ⊤ ∧
∀ i, b ⁻¹ᵁ U i ≤ V i
Tag 0ESL, a lemma
Tag 0ESL in the Stacks Project.
Stacks.DenominatorBlowup.isAdmissibleBlowup_denominatorIdealData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/DenominatorAdmissible.lean, line 210. The attribute's comment: “the blowup in the ideal of denominators is U-admissible”.
Let
Xbe a locally Noetherian scheme,Lan invertible𝒪_X-module andsa regular meromorphic section ofL. LetU ⊆ Xbe the maximal open subscheme such thatscorresponds to a section ofLoverU. Then the blowupb : X' ⟶ XofXin the ideal of denominators ofsisU-admissible.
theorem isAdmissibleBlowup_denominatorIdealData [IsLocallyNoetherian X]
(_hs : IsRegularMeromorphicSection X.sheaf L s) :
Stacks.Blowup.IsAdmissibleBlowup (sectionOpens L s)
(Stacks.Blowup.blowUpToBase (denominatorIdealData X L s))
Stacks.DenominatorBlowup.isSectionOver_and_isAdmissibleBlowup_and_exists_differenceTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/DenominatorExceptionalDivisor.lean, line 303. The attribute's comment: “the whole statement: U is maximal, the blowup in the ideal of denominators is U-admissible, and there is an effective Cartier divisor D with b^ L = O(D - E) carrying the last clause in the form the source's own proof gives it, that b^ s is the regular global section of b^* L(E) whose zero scheme is D”.
Stacks Project, Tag 0ESL. Let
Xbe a locally Noetherian scheme,Lan invertible𝒪_X-module andsa regular meromorphic section ofL. LetU ⊆ Xbe the maximal open subscheme such thatscorresponds to a section ofLoverU. Then:
Ureally is maximal —scorresponds to a section ofLoverU, and every open subscheme over whichscorresponds to a section ofLis contained inU;- the blowup
b : X' ⟶ XofXin the ideal of denominators ofsisU-admissible;- there is an effective Cartier divisor
D ⊆ X'and an isomorphismb^* L ≅ 𝒪_{X'}(D - E), whereE ⊆ X'is the exceptional divisor, through which the meromorphic sectionb^* scorresponds to the meromorphic section1_D ⊗ (1_E)^{-1}.The three clauses are
Stacks.DenominatorBlowup.isSectionOver_sectionOpenstogether withStacks.DenominatorBlowup.le_sectionOpens,Stacks.DenominatorBlowup.isAdmissibleBlowup_denominatorIdealDatacarried fromStacks.Blowup.blowUptoAlgebraicGeometry.blowUpalongAlgebraicGeometry.blowUpIso— the two constructions of the blowup are isomorphic overX, so the morphismbof the admissibility clause is the morphismbof the divisor clause — andStacks.DenominatorBlowup.exists_isEffectiveCartierDivisor_pullL_iso_differenceTwist.The last clause is stated as in that theorem, as the conjunction of the identities that pin down
D, the isomorphism andb^* stogether; see its docstring and the implementation notes ofStacksFrontier/AlgebraicGeometry/Blowup/DenominatorExceptional.lean.
theorem isSectionOver_and_isAdmissibleBlowup_and_exists_differenceTwist
[IsLocallyNoetherian X] (hs : IsRegularMeromorphicSection X.sheaf L s) :
(IsSectionOver L s (sectionOpens L s) ∧
∀ V : Opens X, IsSectionOver L s V → V ≤ sectionOpens L s) ∧
Stacks.Blowup.IsAdmissibleBlowup (sectionOpens L s) (blowHom L s) ∧
∃ D : (blow L s).IdealSheafData, Stacks.Divisors.IsEffectiveCartierDivisor D ∧
∃ (i : pullL L s ≅ Stacks.Divisors.differenceTwist D (exceptional L s))
(e : Stacks.Divisors.invertibleSheaf' D ≅ pullLTensorExceptionalTwist L s),
i = untwistExceptional L s e ∧
Scheme.Modules.Hom.app e.hom ⊤
((Stacks.Divisors.canonicalSection' D).eval (op ⊤)) =
exceptionalTensorSection L s hL ∧
((pullLTensorExceptionalTwistIso L s).hom.val.app (op ⊤))
(exceptionalTensorSection L s hL) = exceptionalHomSection L s hL ∧
exceptionalToPullL L s hL ≫ DenominatorIdeal.toK (blow L s) (pullL L s) =
exceptionalι L s ≫
DenominatorIdeal.sectionMap (blow L s) (pullL L s) (pullS L s)
Sources
Section31.36 Blowing up and flatness#
Section 31.36 of the Stacks Project, Tag 0F84. 3 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0CZP, a lemma
Tag 0CZP in the Stacks Project.
AlgebraicGeometry.strictTransformSheaf_isGeneratedByNear, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/StrictTransformFitting/Generators.lean, line 335.
Stacks Project, Tag 0CZP. The strict transform of a finite type quasi-coherent module on the blowup of its
k-th Fitting ideal is locally generated by at mostksections.
theorem strictTransformSheaf_isGeneratedByNear
{S : Scheme.{u}} (F : S.Modules) [F.IsFiniteType] [F.IsQuasicoherent]
(k : ℕ) (s : Stacks.StrictTransform.baseChange (𝟙 S)
(blowUpToBase (fittingIdeal F (k : ℤ)))) :
IsGeneratedByNear
(Stacks.StrictTransform.sheaf (𝟙 S) (blowUpToBase (fittingIdeal F (k : ℤ)))
(exceptionalIdeal (fittingIdeal F (k : ℤ))) F)
k s
Tag 0CZQ, a lemma
Tag 0CZQ in the Stacks Project.
AlgebraicGeometry.isFiniteLocallyFreeOfRank_strictTransform_fittingBlowUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/StrictTransformFitting/Rank.lean, line 165.
Stacks Project, Tag 0CZQ. Blowing up the
k-th Fitting ideal and taking the strict transform makes a generically rank-kmodule finite locally free of rankk.
theorem isFiniteLocallyFreeOfRank_strictTransform_fittingBlowUp
{S : Scheme.{u}} (F : S.Modules) [F.IsFiniteType] [F.IsQuasicoherent]
(k : ℕ)
(h : let I := fittingIdeal F (k : ℤ)
let U : S.Opens := ⟨I.supportᶜ, I.support.isClosed.isOpen_compl⟩
SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
((Scheme.Modules.pullback U.ι).obj F) k) :
SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
(Stacks.StrictTransform.sheaf (𝟙 S) (blowUpToBase (fittingIdeal F (k : ℤ)))
(exceptionalIdeal (fittingIdeal F (k : ℤ))) F) k
Tag 0ESN, a lemma
Tag 0ESN in the Stacks Project.
AlgebraicGeometry.isAdmissibleBlowup_fittingIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingFlatten.lean, line 134. The attribute's comment: “admissible”.
Stacks Project, Tag 0ESN, part (1). The blowup of the
r-th Fitting ideal of a finitely presented module isU-admissible, for any openUon which the module is finite locally free of rankr. Scheme-theoretic density ofUis not needed.
theorem isAdmissibleBlowup_fittingIdeal [F.IsFinitePresentation] (U : X.Opens) (r : ℕ)
(hrank : SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
((Scheme.Modules.pullback U.ι).obj F) r) :
Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase (fittingIdeal F (r : ℤ)))
AlgebraicGeometry.isFiniteLocallyFreeOfRank_strictTransform_of_dense, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingFlatten.lean, line 150. The attribute's comment: “strict_transform_free”.
Stacks Project, Tag 0ESN, part (2). The strict transform of a finitely presented module along the blowup of its
r-th Fitting ideal is finite locally free of rankr, provided the module has rankron a scheme-theoretically dense open.
theorem isFiniteLocallyFreeOfRank_strictTransform_of_dense [F.IsFiniteType] [F.IsQuasicoherent]
(U : X.Opens) (r : ℕ) (hU : Scheme.Opens.IsSchemeTheoreticallyDense U)
(hrank : SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
((Scheme.Modules.pullback U.ι).obj F) r) :
SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
(Stacks.StrictTransform.sheaf (𝟙 X) (blowUpToBase (fittingIdeal F (r : ℤ)))
(exceptionalIdeal (fittingIdeal F (r : ℤ))) F) r
AlgebraicGeometry.strictTransformKernel_restrict_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingKernel.lean, line 115. The attribute's comment: “kernel”.
Stacks Project, Tag 0ESN, part (3). The kernel of the canonical surjection onto the strict transform vanishes over the open on which the module is finite locally free of rank
r: away from the exceptional divisor the surjection is an isomorphism.
theorem strictTransformKernel_restrict_isZero {X : Scheme.{u}} (F : X.Modules)
[F.IsFinitePresentation] (U : X.Opens) (r : ℕ)
(hrank : SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
((Scheme.Modules.pullback U.ι).obj F) r) :
IsZero ((Scheme.Modules.pullback
((Limits.pullback.fst (𝟙 X) (blowUpToBase (fittingIdeal F (r : ℤ)))) ⁻¹ᵁ U).ι).obj
(strictTransformKernel F r))
AlgebraicGeometry.strictTransformKernel_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingKernel.lean, line 450. The attribute's comment: “kernel”.
Stacks Project, Tag 0ESN, part (3). The kernel of the canonical surjection onto the strict transform is finitely presented: the strict transform is finite locally free, so the surjection splits locally, and the pullback of a finitely presented module is finitely presented (Stacks tag 01BQ).
theorem strictTransformKernel_isFinitePresentation {X : Scheme.{u}} (F : X.Modules)
[F.IsFinitePresentation] (U : X.Opens)
(hU : Scheme.Opens.IsSchemeTheoreticallyDense U) (r : ℕ)
(hrank : SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
((Scheme.Modules.pullback U.ι).obj F) r) :
(strictTransformKernel F r).IsFinitePresentation
AlgebraicGeometry.isPerfect_modulePullback_pullbackFst_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingNormalForm.lean, line 360. The attribute's comment: “the pullback is perfect”.
Perfectness transported from the blowup to its base change along the identity. The pullback of a perfect
𝒪_X-module of Tor dimension at most one to the base change of the blowup ofIalong the identity ofXis perfect.This is tag 0ESS, which is stated on the blowup itself, moved along the isomorphism of the base change with the blowup; the hypotheses are the ones tag 0ESS makes, on
ℱoverX, andIis an arbitrary ideal sheaf. Part (4) of tag 0ESN is a different statement, about the blowup of the Fitting ideal and assuming only thatℱis finitely presented; it is carried at those hypotheses byAlgebraicGeometry.isPerfect_modulePullback_fittingBlowUpFstandAlgebraicGeometry.isPerfect_strictTransformKernel_of_isFinitePresentationinStacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingPerfectTransform.lean.The registration below records that this statement is the base-change spelling used in the proof of part (4); it is not a claim that it is part (4).
theorem isPerfect_modulePullback_pullbackFst_blowUpToBase (F : OXMod.{u, u} X.toRingedSpace)
(hperfect : IsPerfect.{u, u, u + 1}
((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj F))
(htor : HasTorAmplitude X.toRingedSpace
((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj F) (-1) 0) :
IsPerfect.{u, u, u + 1} ((DerivedCategory.singleFunctor
(OXMod.{u, u} (Stacks.StrictTransform.baseChange (𝟙 X) (blowUpToBase I)).toRingedSpace)
0).obj
((Scheme.Modules.pullback (pullback.fst (𝟙 X) (blowUpToBase I))).obj F))
AlgebraicGeometry.hasTorAmplitude_modulePullback_pullbackFst_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingNormalForm.lean, line 386. The attribute's comment: “the Tor dimension of the pullback”.
Tor amplitude transported from the blowup to its base change along the identity. The pullback of an
𝒪_X-module of Tor dimension at most one to the base change of the blowup ofIalong the identity ofXagain has Tor dimension at most one.As above this is the base-change spelling of tag 0ESS, at the hypotheses tag 0ESS makes and for an arbitrary ideal sheaf
I, not part (4) of tag 0ESN. The latter isAlgebraicGeometry.hasTorAmplitude_modulePullback_fittingBlowUpFstandAlgebraicGeometry.hasTorAmplitude_strictTransformKernel_of_isFinitePresentationinStacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingPerfectTransform.lean, which assume only thatℱis finitely presented.As above, the registration below records the base-change spelling used in the proof of part (4), not part (4) itself.
theorem hasTorAmplitude_modulePullback_pullbackFst_blowUpToBase
(F : OXMod.{u, u} X.toRingedSpace)
(htor : HasTorAmplitude X.toRingedSpace
((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj F) (-1) 0) :
HasTorAmplitude
(Stacks.StrictTransform.baseChange (𝟙 X) (blowUpToBase I)).toRingedSpace
((DerivedCategory.singleFunctor
(OXMod.{u, u} (Stacks.StrictTransform.baseChange (𝟙 X)
(blowUpToBase I)).toRingedSpace) 0).obj
((Scheme.Modules.pullback (pullback.fst (𝟙 X) (blowUpToBase I))).obj F)) (-1) 0
AlgebraicGeometry.isPerfect_modulePullback_fittingBlowUpFst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingPerfectTransform.lean, line 146. The attribute's comment: “the pullback along the Fitting blowup is perfect”.
Stacks Project, Tag 0ESN, part (4), for the pullback. Let
ℱbe a finitely presented module onXwhich is finite locally free of constant rankron a scheme-theoretically dense openU. The pullback ofℱalong the blowup of ther-th Fitting ideal ofℱ, written as the base change of that blowup along the identity ofX, is a perfect𝒪_{X'}-module.No hypothesis on
ℱbeyond finite presentation is needed:AlgebraicGeometry.isPerfect_and_hasTorAmplitude_modulePullback_fittingBlowUp, the globalization of Stacks 0F7M, gives perfectness on the blowup itself, and the transport above moves it into the base-change spelling.
theorem isPerfect_modulePullback_fittingBlowUpFst [F.IsFinitePresentation] (U : X.Opens)
(hU : Scheme.Opens.IsSchemeTheoreticallyDense U)
(hrank : SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
((Scheme.Modules.pullback U.ι).obj F) r) :
IsPerfect.{u, u, u + 1} ((DerivedCategory.singleFunctor
(OXMod.{u, u} (Stacks.StrictTransform.baseChange (𝟙 X)
(blowUpToBase (fittingIdeal F (r : ℤ)))).toRingedSpace) 0).obj
((Scheme.Modules.pullback
(pullback.fst (𝟙 X) (blowUpToBase (fittingIdeal F (r : ℤ))))).obj F))
AlgebraicGeometry.hasTorAmplitude_modulePullback_fittingBlowUpFst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingPerfectTransform.lean, line 165. The attribute's comment: “the Tor dimension of the pullback along the Fitting blowup”.
Stacks Project, Tag 0ESN, part (4), for the pullback. Let
ℱbe a finitely presented module onXwhich is finite locally free of constant rankron a scheme-theoretically dense openU. The pullback ofℱalong the blowup of ther-th Fitting ideal ofℱ, placed in degree0, has Tor amplitude in[-1, 0].As above, finite presentation is all that is used.
theorem hasTorAmplitude_modulePullback_fittingBlowUpFst [F.IsFinitePresentation] (U : X.Opens)
(hU : Scheme.Opens.IsSchemeTheoreticallyDense U)
(hrank : SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
((Scheme.Modules.pullback U.ι).obj F) r) :
HasTorAmplitude (Stacks.StrictTransform.baseChange (𝟙 X)
(blowUpToBase (fittingIdeal F (r : ℤ)))).toRingedSpace
((DerivedCategory.singleFunctor
(OXMod.{u, u} (Stacks.StrictTransform.baseChange (𝟙 X)
(blowUpToBase (fittingIdeal F (r : ℤ)))).toRingedSpace) 0).obj
((Scheme.Modules.pullback
(pullback.fst (𝟙 X) (blowUpToBase (fittingIdeal F (r : ℤ))))).obj F)) (-1) 0
AlgebraicGeometry.isPerfect_strictTransformKernel_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingPerfectTransform.lean, line 208. The attribute's comment: “the kernel is perfect”.
Stacks Project, Tag 0ESN, part (4), for the kernel. For a finitely presented module
ℱwhich is finite locally free of constant rankron a scheme-theoretically dense openU, the kernel of the canonical surjection fromb^*ℱonto the strict transform ofℱis a perfect𝒪_{X'}-module.The kernel sequence gives a distinguished triangle
𝒦 ⟶ b^*ℱ ⟶ 𝒬 ⟶ 𝒦[1];b^*ℱis perfect byAlgebraicGeometry.isPerfect_modulePullback_fittingBlowUpFstand𝒬is perfect because it is finite locally free of rankrby tag 0ESN (2), so the first vertex is perfect by tag 08CR.This is
AlgebraicGeometry.isPerfect_strictTransformKernelwith no hypothesis onℱbeyond finite presentation, which is as far as tag 0ESN assumes: the perfectness ofb^*ℱthat the triangle consumes is itself a consequence of finite presentation.
theorem isPerfect_strictTransformKernel_of_isFinitePresentation [F.IsFinitePresentation]
(U : X.Opens) (hU : Scheme.Opens.IsSchemeTheoreticallyDense U)
(hrank : SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
((Scheme.Modules.pullback U.ι).obj F) r) :
IsPerfect.{u, u, u + 1} ((DerivedCategory.singleFunctor
(OXMod.{u, u} (Stacks.StrictTransform.baseChange (𝟙 X)
(blowUpToBase (fittingIdeal F (r : ℤ)))).toRingedSpace) 0).obj
(strictTransformKernel F r))
AlgebraicGeometry.hasTorAmplitude_strictTransformKernel_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingPerfectTransform.lean, line 241. The attribute's comment: “the Tor dimension of the kernel”.
Stacks Project, Tag 0ESN, part (4), for the kernel. For a finitely presented module
ℱwhich is finite locally free of constant rankron a scheme-theoretically dense openU, the kernel of the canonical surjection fromb^*ℱonto the strict transform ofℱ, placed in degree0, has Tor amplitude in[-1, 0].The kernel sequence gives a distinguished triangle
𝒦 ⟶ b^*ℱ ⟶ 𝒬 ⟶ 𝒦[1]. Hereb^*ℱhas Tor amplitude in[-1, 0]byAlgebraicGeometry.hasTorAmplitude_modulePullback_fittingBlowUpFstand𝒬in[0, 0], being finite locally free hence flat, so tag 08CJ (3) puts𝒦in[-1, 1]. A module in degree0has no Tor in positive degrees, which removes degree1.This is
AlgebraicGeometry.hasTorAmplitude_strictTransformKernelwith no bound assumed onℱ, which is as far as tag 0ESN assumes: the bound onb^*ℱthat the triangle consumes already follows from finite presentation.
theorem hasTorAmplitude_strictTransformKernel_of_isFinitePresentation [F.IsFinitePresentation]
(U : X.Opens) (hU : Scheme.Opens.IsSchemeTheoreticallyDense U)
(hrank : SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
((Scheme.Modules.pullback U.ι).obj F) r) :
HasTorAmplitude (Stacks.StrictTransform.baseChange (𝟙 X)
(blowUpToBase (fittingIdeal F (r : ℤ)))).toRingedSpace
((DerivedCategory.singleFunctor
(OXMod.{u, u} (Stacks.StrictTransform.baseChange (𝟙 X)
(blowUpToBase (fittingIdeal F (r : ℤ)))).toRingedSpace) 0).obj
(strictTransformKernel F r)) (-1) 0
Sources
Section31.37 Modifications#
Section 31.37 of the Stacks Project, Tag 0AYN. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0AYP, a lemma
Tag 0AYP in the Stacks Project.
Stacks.ProjectiveBundleSplitting.exists_modification_hasInvertibleFiltration', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleSplitting/InvertibleFiltration.lean, line 47.
Stacks Project, Tag 0AYP. Let
Xbe an integral scheme andℰa finite locally free𝒪_X-module of rankr. There is a modificationf : X' ⟶ Xsuch thatf^*ℰhas a filtration0 = ℰ_0 ⊆ ℰ_1 ⊆ … ⊆ ℰ_r = f^*ℰby finite locally free submodules whose successive quotients are invertible𝒪_{X'}-modules.This is
exists_modification_hasInvertibleFiltration_of_epiwith its one input, the epimorphy of the tautological map of a projective bundle, supplied byepi_tautologicalMap.
theorem exists_modification_hasInvertibleFiltration' (r : ℕ) (X : Scheme.{u}) [IsIntegral X]
(E : X.Modules)
(hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r) :
∃ (X' : Scheme.{u}) (f : X' ⟶ X), IsModification f ∧
HasInvertibleFiltration X' ((Scheme.Modules.pullback f).obj E) r
Tag 0C4V, a lemma
Tag 0C4V in the Stacks Project.
Stacks.Divisors.exists_proper_modification_resolving_partialMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Modification/RationalMap.lean, line 63.
Stacks Project, Tag 0C4V. An
S-rational map from a Noetherian scheme to a scheme proper overSextends to anS-morphism after a proper modification which is unchanged over the rational map's domain.
theorem exists_proper_modification_resolving_partialMap
{S X Y : Scheme.{u}} [X.Over S] [Y.Over S] [IsNoetherian X]
[IsProper (Y ↘ S)] (f : X.PartialMap Y) [f.IsOver S] :
∃ (X' : Scheme.{u}) (p : X' ⟶ X) (f' : X' ⟶ Y),
IsProper p ∧
f' ≫ (Y ↘ S) = p ≫ (X ↘ S) ∧
IsIso (pullback.snd p f.domain.ι) ∧
pullback.fst p f.domain.ι ≫ f' = pullback.snd p f.domain.ι ≫ f.hom
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.