The ideal sheaf of an effective Cartier divisor is invertible

Let D ⊆ X be an effective Cartier divisor, given by an ideal sheaf I which near every point is generated, on an affine open U, by a single nonzerodivisor a of Γ(X, U). Then the ideal sheaf I ⊆ 𝒪_X (Scheme.IdealSheafData.sheaf) is an invertible sheaf: over U, multiplication by a is an isomorphism 𝒪_U ≅ I|_U.

No integrality assumption is made on X, so this applies to the relative effective Cartier divisors on the base changes X_T = T ×_S X, whatever the scheme T. The dual of this invertible sheaf is the line bundle 𝒪_X(D), the value of the Abel map on D.

Over an open V ⊆ U which is not affine, the sections of I are still the multiples of a (exists_mul_eq_of_ideal_eq_span): on the affine opens inside V they are, by the quasi-coherence of I, and the local quotients glue because a remains a nonzerodivisor on every open subset of U (AlgebraicGeometry.IsAffineOpen.isSMulRegular_map).

The converse, that a closed subscheme whose ideal sheaf is invertible is an effective Cartier divisor, is not proved here.

Main declarations

• Scheme.IdealSheafData.exists_mul_eq_of_ideal_eq_span: if I is generated by a nonzerodivisor a on an affine open U, then every section of I over an open V ⊆ U is a multiple of a, and Scheme.IdealSheafData.bijective_smul_map_sectionMk makes a a basis of I over V;
• Scheme.IdealSheafData.unitOverIsoOfIdealEqSpan: the resulting trivialization 𝒪_U ≅ I|_U, which is multiplication by a (sheafι_app_unitOverIsoOfIdealEqSpan_hom);
• Scheme.IdealSheafData.IsEffectiveCartier.isInvertible_sheaf: the ideal sheaf of an effective Cartier divisor is invertible, packaged as IsEffectiveCartier.toInvertibleSheaf.

References

• The Stacks Project, Divisors, Section Effective Cartier divisors (Tag 01WQ), where the ideal sheaf of an effective Cartier divisor is shown to be invertible.

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_mul_eq_of_ideal_eq_span {X : Scheme} (I : X.IdealSheafData) {U : ↑X.affineOpens} {a : ↑(X.presheaf.obj (Opposite.op ↑U))} (ha : IsSMulRegular (↑(X.presheaf.obj (Opposite.op ↑U))) a) (hIa : I.ideal U = Ideal.span {a}) {V : X.Opens} (hVU : V ≤ ↑U) {s : ↑(X.presheaf.obj (Opposite.op V))} (hs : s ∈ I.sections V) : ∃ (t : ↑(X.presheaf.obj (Opposite.op V))), (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE hVU).op)) a * t = s

If the ideal sheaf I is generated on an affine open U by a nonzerodivisor a, then over every open V ⊆ U the sections of I are the multiples of the restriction of a.

theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_sections_of_ideal_eq_span {X : Scheme} (I : X.IdealSheafData) {U : ↑X.affineOpens} {a : ↑(X.presheaf.obj (Opposite.op ↑U))} (hIa : I.ideal U = Ideal.span {a}) : a ∈ I.sections ↑U

If the ideal sheaf I is generated on an affine open U by a, then a is a section of I over U.

theorem AlgebraicGeometry.Scheme.IdealSheafData.bijective_smul_map_sectionMk {X : Scheme} (I : X.IdealSheafData) {U : ↑X.affineOpens} {a : ↑(X.presheaf.obj (Opposite.op ↑U))} (ha : IsSMulRegular (↑(X.presheaf.obj (Opposite.op ↑U))) a) (hIa : I.ideal U = Ideal.span {a}) {V : X.Opens} (hVU : V ≤ ↑U) : Function.Bijective fun (r : ↑(X.presheaf.obj (Opposite.op V))) => r • (CategoryTheory.ConcreteCategory.hom (I.sheaf.presheaf.map (CategoryTheory.homOfLE hVU).op)) (I.sectionMk a ⋯)

If the ideal sheaf I is generated on an affine open U by a nonzerodivisor a, then over every open V ⊆ U, multiplication by the restriction of a is a bijection from Γ(X, V) onto the sections of I over V.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.unitOverIsoOfIdealEqSpan {X : Scheme} (I : X.IdealSheafData) {U : ↑X.affineOpens} {a : ↑(X.presheaf.obj (Opposite.op ↑U))} (ha : IsSMulRegular (↑(X.presheaf.obj (Opposite.op ↑U))) a) (hIa : I.ideal U = Ideal.span {a}) : SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf ↑U) ≅ SheafOfModules.over I.sheaf ↑U

If the ideal sheaf I is generated on an affine open U by a nonzerodivisor a, then a is a global basis of I over U: multiplication by a is an isomorphism 𝒪_U ≅ I|_U.

Equations

• I.unitOverIsoOfIdealEqSpan ha hIa = CategoryTheory.asIso ((SheafOfModules.over I.sheaf ↑U).unitHomEquiv.symm ((SheafOfModules.overSectionsEquiv I.sheaf ↑U).symm (I.sectionMk a ⋯)))

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sheafι_app_unitOverIsoOfIdealEqSpan_hom {X : Scheme} (I : X.IdealSheafData) {U : ↑X.affineOpens} {a : ↑(X.presheaf.obj (Opposite.op ↑U))} (ha : IsSMulRegular (↑(X.presheaf.obj (Opposite.op ↑U))) a) (hIa : I.ideal U = Ideal.span {a}) {V : X.Opens} (hVU : V ≤ ↑U) (r : ↑(X.presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (Modules.Hom.app I.sheafι V)) ((CategoryTheory.ConcreteCategory.hom ((I.unitOverIsoOfIdealEqSpan ha hIa).hom.val.app (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.homOfLE hVU))))) r) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE hVU).op)) a * r

Over an open V ⊆ U, the trivialization unitOverIsoOfIdealEqSpan is multiplication by the local equation a: composed with the inclusion I ⟶ 𝒪_X, it sends a scalar r to a|_V * r.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.isInvertible_sheaf {X : Scheme} {I : X.IdealSheafData} (hI : I.IsEffectiveCartier) : TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X I.sheaf

The ideal sheaf of an effective Cartier divisor is invertible. Near every point, the ideal sheaf is generated on an affine open by a nonzerodivisor a, and multiplication by a trivializes it there.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.toInvertibleSheaf {X : Scheme} {I : X.IdealSheafData} (hI : I.IsEffectiveCartier) : TauCeti.AlgebraicGeometry.InvertibleSheaf X

The ideal sheaf of an effective Cartier divisor, as an invertible sheaf.

Equations

• hI.toInvertibleSheaf = { obj := I.sheaf, property := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.toInvertibleSheaf_obj {X : Scheme} {I : X.IdealSheafData} (hI : I.IsEffectiveCartier) : hI.toInvertibleSheaf.obj = I.sheaf

The underlying sheaf of IsEffectiveCartier.toInvertibleSheaf is the ideal sheaf.