Ideal sheaves of sums of effective Cartier divisors

The sum of two effective Cartier divisors D and E on a scheme X is cut out by the product I_D * I_E of their ideal sheaves. Multiplication of local functions sends sections of I and J to sections of I * J (Scheme.IdealSheafData.sectionsMul), and when J is the ideal sheaf of an effective Cartier divisor this gives an isomorphism I ⊗ J ≅ I * J of 𝒪_X-modules, for an arbitrary ideal sheaf I. Over an affine open on which J is generated by a nonzerodivisor b, every section of I ⊗ J is a pure tensor s ⊗ b, which multiplication sends to s * b; this is injective because b is a nonzerodivisor, and surjective because (I * J)(V) = I(V) * (b).

No integrality or noetherian hypothesis is placed on X, so this applies to the relative effective Cartier divisors on the base changes X_T = T ×_S X for every scheme T. In the Picard group it says that the class of 𝒪_X(-D) = I_D is additive in D; since 𝒪_X(D) is the dual of I_D, inverting gives [𝒪_X(D + E)] = [𝒪_X(D)] * [𝒪_X(E)], which is what makes the Abel map D ↦ 𝒪_X(D) on effective Cartier divisors additive.

Main declarations

• Scheme.IdealSheafData.tensorProductSheafIso: I ⊗ J ≅ I * J when J is effective Cartier, with Scheme.IdealSheafData.tensorProductSheafIso_hom_tmul computing it on pure tensors;
• TauCeti.AlgebraicGeometry.LineBundleClass.mk_toInvertibleSheaf_congr: the line-bundle class of an effective Cartier divisor depends only on its ideal sheaf;
• TauCeti.AlgebraicGeometry.LineBundleClass.mk_toInvertibleSheaf_mul: the line-bundle class of the ideal sheaf of D + E is the product of the classes of the ideal sheaves of D and E. TauCeti.AlgebraicGeometry.LineBundleClass.mk_toInvertibleSheaf_top, TauCeti.AlgebraicGeometry.LineBundleClass.mk_toInvertibleSheaf_pow and TauCeti.AlgebraicGeometry.LineBundleClass.mk_toInvertibleSheaf_prod extend this to the empty divisor, to multiples n D and to finite sums ∑ᵢ Dᵢ.

References

• The Stacks Project, Divisors, Section Effective Cartier divisors (Tag 01WQ): the sum D + E is cut out by I_D I_E, and 𝒪_X(D + E) ≅ 𝒪_X(D) ⊗ 𝒪_X(E).
• The construction of the multiplication map follows the Cartier divisor version Scheme.CartierDivisor.tensorProductSheafIso in TauCeti/AlgebraicGeometry/CartierDivisor/TensorProduct.lean.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.tensorProductSheafIso {X : Scheme} (I : X.IdealSheafData) {J : X.IdealSheafData} (hJ : J.IsEffectiveCartier) : TauCeti.SheafOfModules.tensorProduct X.sheaf I.sheaf J.sheaf ≅ (I * J).sheaf

The ideal sheaf of a sum of divisors. If J is the ideal sheaf of an effective Cartier divisor, multiplication of local functions is an isomorphism I ⊗ J ≅ I * J for every ideal sheaf I.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.tensorProductSheafIso_hom_tmul {X : Scheme} (I : X.IdealSheafData) {J : X.IdealSheafData} (hJ : J.IsEffectiveCartier) (U : X.Opens) (s : ↑(I.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(J.sheaf.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (Modules.Hom.app (CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.tensorProductIso X.sheaf I.sheaf J.sheaf).inv (I.tensorProductSheafIso hJ).hom) U)) ((CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).unit.app (PresheafOfModulesOfCommRing.Monoidal.tensorObj I.sheaf.val J.sheaf.val)).app (Opposite.op U))) (s ⊗ₜ[↑(X.sheaf.obj.obj (Opposite.op U))] t)) = I.sectionsMul J U s t

On a pure tensor of local sections, the isomorphism I ⊗ J ≅ I * J multiplies the two functions. The sheafification unit sends the sectionwise pure tensor into the tensor product sheaf.

theorem TauCeti.AlgebraicGeometry.LineBundleClass.mk_toInvertibleSheaf_congr {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (hI : I.IsEffectiveCartier) (hJ : J.IsEffectiveCartier) (e : I = J) : mk hI.toInvertibleSheaf = mk hJ.toInvertibleSheaf

The line-bundle class of an effective Cartier divisor depends only on its ideal sheaf.

theorem TauCeti.AlgebraicGeometry.LineBundleClass.mk_toInvertibleSheaf_mul {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (hI : I.IsEffectiveCartier) (hJ : J.IsEffectiveCartier) : mk ⋯.toInvertibleSheaf = mk hI.toInvertibleSheaf * mk hJ.toInvertibleSheaf

The line-bundle class of the ideal sheaf of a sum D + E of effective Cartier divisors is the product of the classes of the ideal sheaves of D and E.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.mk_toInvertibleSheaf_top {X : AlgebraicGeometry.Scheme} : mk ⋯.toInvertibleSheaf = 1

The ideal sheaf of the empty effective Cartier divisor is the structure sheaf, whose line-bundle class is trivial.

theorem TauCeti.AlgebraicGeometry.LineBundleClass.mk_toInvertibleSheaf_pow {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} (hI : I.IsEffectiveCartier) (n : ℕ) : mk ⋯.toInvertibleSheaf = mk hI.toInvertibleSheaf ^ n

The line-bundle class of the ideal sheaf of n D is the n-th power of the class of the ideal sheaf of the effective Cartier divisor D.

theorem TauCeti.AlgebraicGeometry.LineBundleClass.mk_toInvertibleSheaf_prod {X : AlgebraicGeometry.Scheme} {ι : Type u_1} (s : Finset ι) {I : ι → X.IdealSheafData} (hI : ∀ i ∈ s, (I i).IsEffectiveCartier) : mk ⋯.toInvertibleSheaf = ∏ i ∈ s.attach, mk ⋯.toInvertibleSheaf

The line-bundle class of the ideal sheaf of a finite sum ∑ᵢ Dᵢ of effective Cartier divisors is the product of the classes of the ideal sheaves of the Dᵢ.